Axiomatize CPOs, begin work on interpretation

This commit is contained in:
Théophile Bastian 2017-11-09 14:50:33 +01:00
parent 94bc771b16
commit 98286d1ad8

88
wp.v
View file

@ -5,7 +5,7 @@
Require Import ZArith.BinInt. Require Import ZArith.BinInt.
Import Z. Import Z.
Parameter Var: Type. Definition Var := nat.
Definition Mem := Var -> Z. Definition Mem := Var -> Z.
Definition Expr:= Mem -> Z. Definition Expr:= Mem -> Z.
@ -16,3 +16,89 @@ Inductive Instr : Type :=
| seq: Instr -> Instr -> Instr | seq: Instr -> Instr -> Instr
| ifelse: Expr -> Instr -> Instr -> Instr | ifelse: Expr -> Instr -> Instr -> Instr
| while: Expr -> Instr -> Instr. | while: Expr -> Instr -> Instr.
Definition ifonly (exp: Expr) (inst: Instr) : Instr :=
ifelse exp inst skip.
(***** CPO *******************************************************************)
Fixpoint nat_eq x y :=
match x, y with
| 0, 0 => true
| 0, S _ => false
| S _, 0 => false
| S x0, S y0 => nat_eq x0 y0
end.
Definition Sequence (S: Type) := nat -> S.
Inductive cpo (T: Type): Type :=
| CpoError: (cpo T)
| CpoElem: T -> (cpo T).
Definition cpo_leq: forall (T: Type), cpo T -> cpo T -> Prop :=
fun T x y => match x, y with
| CpoError _, _ => True
| CpoElem _ x0, CpoElem _ y0 => x0 = y0
| _, _ => False
end.
Arguments cpo_leq {T} _ _.
Infix "cpo<=" := cpo_leq (at level 100).
Definition is_chain: forall (T: Type), Sequence (cpo T) -> Prop :=
fun T chain => forall (n: nat), (chain n) cpo<= (chain (S n)).
Arguments is_chain {T} _.
Definition is_lub_of: forall (T: Type), Sequence (cpo T) -> cpo T -> Prop :=
fun T chain elt => forall (n: nat), (chain n) cpo<= elt.
Arguments is_lub_of {T} _ _.
Axiom find_lub: forall (T: Type), Sequence (cpo T) -> cpo T.
Arguments find_lub {T} _.
Axiom find_lub_correct:
forall (T: Type), forall (chain: Sequence (cpo T)),
is_chain chain -> is_lub_of chain (find_lub chain).
Arguments find_lub_correct {T} {chain} _.
(***** Interpretation ********************************************************)
Definition subst: Mem -> Var -> Z -> Mem :=
fun (m: Mem) (v: Var) (z: Z) (v2: Var) =>
if nat_eq v v2 then z else m v2.
Definition MemCpo := cpo Mem.
Definition MemError := CpoError Mem.
Definition MemElem := CpoElem Mem.
Fixpoint repeat_n (n: nat) (inst: Instr) :=
let aux := (fix aux (n: nat) (inst: Instr) (acc: Instr) :=
match n with
| 0 => skip
| S n => aux n inst (seq acc inst) end) in
aux n inst (skip).
Definition while_sem_n: Expr -> Instr -> nat -> Instr :=
fun guard inst n =>
seq (repeat_n n (ifonly guard inst)) (ifonly guard abort).
Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
match mem with
| CpoError _ => MemError
| CpoElem _ mem0 =>
match inst with
| skip => MemElem mem0
| abort => MemError
| assign v e => (MemElem (subst mem0 v (e mem0)))
| seq instr1 instr2 => interp instr2 (interp instr1 (MemElem mem0))
| ifelse exp instrIf instrElse =>
if ((exp mem0) =? 0) % Z
then interp instrIf (MemElem mem0)
else interp instrElse (MemElem mem0)
| while guard instr =>
let fix while_chain (guard: Expr) (inst: Instr)
(mem: MemCpo) : (Sequence MemCpo) :=
fun n => interp (while_sem_n guard inst n) mem
in find_lub (while_chain guard instr (MemElem mem0))
end
end.