(*
Autor(s):
Andrej Dudenhefner (1)
Affiliation(s):
(1) Saarland University, Saarbrücken, Germany
*)
(*
Definition(s):
Confluent Simple Stack Machines (cssm)
Problems(s):
Uniform Boundedness of Confluent Simple Stack Machines (CSSM_UB)
*)
Require Import List Relation_Operators.
Definition stack : Set := list bool.
Definition state : Set := nat.
(* configuration: left stack, right stack, state *)
Definition config : Set := stack * stack * state.
(* direction: true = move left, false = move right *)
Definition dir : Set := bool.
(* stack symbol: true = 1, false = 0 *)
Definition symbol : Set := bool.
(* instruction:
(x, y, a, b, true ) = ax -> by
(x, y, b, a, false ) = xb -> ay *)
Definition instruction : Set := state * state * symbol * symbol * dir.
(* simple stack machine: list of instructions *)
Definition ssm : Set := list instruction.
Inductive step (M : ssm) : config -> config -> Prop :=
(* transition AaxB -> AybB *)
| step_l (x y: state) (a b: symbol) (A B: stack) :
In (x, y, a, b, true) M -> step M (a::A, B, x) (A, b::B, y)
(* transition AxbB -> AayB *)
| step_r (x y: state) (a b: symbol) (A B: stack) :
In (x, y, b, a, false) M -> step M (A, b::B, x) (a::A, B, y).
(* reflexive transitive closure of step *)
Definition reachable (M: ssm) : config -> config -> Prop := clos_refl_trans config (step M).
(* step is confluent *)
Definition confluent (M: ssm) := forall (X Y1 Y2: config), reachable M X Y1 -> reachable M X Y2 ->
exists (Z: config), reachable M Y1 Z /\ reachable M Y2 Z.
(* confluent simple stack machine *)
Definition cssm := { M : ssm | confluent M }.
(* uniform bound for the number of reachable configurations *)
Definition bounded (M: ssm) (n: nat) : Prop :=
forall (X: config), exists (L: list config), (forall (Y: config), reachable M X Y -> In Y L) /\ length L <= n.
(* given a confluent simple stack machine M,
is M uniformly bounded by some n? *)
Definition CSSM_UB (M : cssm) := exists (n: nat), bounded (proj1_sig M) n.
Autor(s):
Andrej Dudenhefner (1)
Affiliation(s):
(1) Saarland University, Saarbrücken, Germany
*)
(*
Definition(s):
Confluent Simple Stack Machines (cssm)
Problems(s):
Uniform Boundedness of Confluent Simple Stack Machines (CSSM_UB)
*)
Require Import List Relation_Operators.
Definition stack : Set := list bool.
Definition state : Set := nat.
(* configuration: left stack, right stack, state *)
Definition config : Set := stack * stack * state.
(* direction: true = move left, false = move right *)
Definition dir : Set := bool.
(* stack symbol: true = 1, false = 0 *)
Definition symbol : Set := bool.
(* instruction:
(x, y, a, b, true ) = ax -> by
(x, y, b, a, false ) = xb -> ay *)
Definition instruction : Set := state * state * symbol * symbol * dir.
(* simple stack machine: list of instructions *)
Definition ssm : Set := list instruction.
Inductive step (M : ssm) : config -> config -> Prop :=
(* transition AaxB -> AybB *)
| step_l (x y: state) (a b: symbol) (A B: stack) :
In (x, y, a, b, true) M -> step M (a::A, B, x) (A, b::B, y)
(* transition AxbB -> AayB *)
| step_r (x y: state) (a b: symbol) (A B: stack) :
In (x, y, b, a, false) M -> step M (A, b::B, x) (a::A, B, y).
(* reflexive transitive closure of step *)
Definition reachable (M: ssm) : config -> config -> Prop := clos_refl_trans config (step M).
(* step is confluent *)
Definition confluent (M: ssm) := forall (X Y1 Y2: config), reachable M X Y1 -> reachable M X Y2 ->
exists (Z: config), reachable M Y1 Z /\ reachable M Y2 Z.
(* confluent simple stack machine *)
Definition cssm := { M : ssm | confluent M }.
(* uniform bound for the number of reachable configurations *)
Definition bounded (M: ssm) (n: nat) : Prop :=
forall (X: config), exists (L: list config), (forall (Y: config), reachable M X Y -> In Y L) /\ length L <= n.
(* given a confluent simple stack machine M,
is M uniformly bounded by some n? *)
Definition CSSM_UB (M : cssm) := exists (n: nat), bounded (proj1_sig M) n.