executionplan.v

Inductive expr : Set :=
| lit : nat -> expr
| add : expr -> expr -> expr.

(* Define the type of big step semantics *)
Inductive big : expr -> nat -> Prop :=
| big_lit : forall x, big (lit x) x
| big_add : forall x y a b, big x a -> big y b -> big (add x y) (a + b).

(* A step maps a state to a state *)
Definition step_sem a := a -> a -> Set.
(* We can take the free path category of state transitions *)
Inductive path a (s : step_sem a) : a -> a -> Type :=
| id : forall A, path a s A A
| compose : forall A B C, path a s B C -> s A B -> path a s A C.

(* Such steps form a smallstep semantics for our big steps semantics "big" if
we can map to an explicit execution plan of a path of steps from (inject x) to (halt y) *)
Definition small_sem state (step : step_sem state) (inject : expr -> state) (halt : nat -> state) :=
   forall x y,
   path state step (inject x) (halt y) -> 
   big x y.

Axiom state : Set.
Axiom inject : expr -> state.
Axiom halt : nat -> state.
Axiom step : state -> state -> Set.
Axiom maps_to_big : small_sem state step inject halt.