Commit a2b80280 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

defunctionalization example continued, a few termination proofs missing

parent 087f90ad
(**
(**
{1 Defunctionalization}
This is inspired from student exercises proposed by
This is inspired from student exercises proposed by
{h <a href="http://cs.au.dk/~danvy/">Olivier Danvy</a>}
at the {h <a href="http://jfla.inria.fr/2014/">JFLA 2014 conference</a>}
*)
(**{h }*)
(** {h } *)
(** {2 Simple Arithmetic Expressions} *)
......@@ -17,7 +17,7 @@ module Expr
use export int.Int
(** Grammar of expressions
(** Grammar of expressions
{h <blockquote><pre>
n : int
......@@ -25,7 +25,7 @@ e : expression
e ::= n | e - e
p : program
p ::= e
p ::= e
</pre></blockquote>}
*)
......@@ -109,17 +109,18 @@ function interpret_0 (p:prog) : int = eval_0 p
(** Tests, can be replayed using
{h <blockquote><pre>
why3 defunctionalization.mlw --exec DirectSem.t0
why3 defunctionalization.mlw --exec DirectSem.test
</pre></blockquote>}
resp. [DirectSem.t1], [DirectSem.t2], etc. (Why3 version at least 0.82 required)
(Why3 version at least 0.82 required)
*)
let t0 () = interpret_0 p0
let t1 () = interpret_0 p1
let t2 () = interpret_0 p2
let t3 () = interpret_0 p3
let t4 () = interpret_0 p4
let test () =
(interpret_0 p0,
interpret_0 p1,
interpret_0 p2,
interpret_0 p3,
interpret_0 p4)
end
......@@ -143,7 +144,7 @@ use import Expr
*)
use HighOrd (* import not needed, but why ? *)
use HighOrd
function eval_1 (e:expr) (k:int -> 'a) : 'a =
match e with
......@@ -291,11 +292,12 @@ let interpret_2 (p:prog) : int
ensures { result = eval_0 p }
= eval_2 p I
let u0 () = interpret_2 p0
let u1 () = interpret_2 p1
let u2 () = interpret_2 p2
let u3 () = interpret_2 p3
let u4 () = interpret_2 p4
let test () =
(interpret_2 p0,
interpret_2 p1,
interpret_2 p2,
interpret_2 p3,
interpret_2 p4)
end
......@@ -380,11 +382,6 @@ function eval_0 (e:expr) : value =
function interpret_0 (p:prog) : value = eval_0 p
let t0 () = interpret_0 p0
let t1 () = interpret_0 p1
let t2 () = interpret_0 p2
let t3 () = interpret_0 p3
let t4 () = interpret_0 p4
(** {4 Exercise 1.1}
......@@ -437,7 +434,7 @@ lemma cps_correct: forall p. interpret_1 p = interpret_0 p
{h <blockquote><pre>
expressible_value -> 'a
</pre></blockquote>}
in two:
in two:
{h <blockquote><pre>
(value -> 'a) * (error -> 'a)
</pre></blockquote>}
......@@ -477,7 +474,7 @@ with eval_2b (v1:int) (k:int -> 'a) (kerr : unit -> 'a) : int -> 'a =
function interpret_2 (p : prog) : value =
function interpret_2 (p : prog) : value =
eval_2 p (\ n. Vnum n) (\ u. Underflow)
let rec lemma cps2_correct_expr (e:expr) (kerr:unit -> 'a): unit
......@@ -565,8 +562,8 @@ type cont = I | A expr cont | B int cont
(**
One would want to write in Why:
[function eval_cont (c:cont) (v:value) : value =
{h <blockquote><pre>
function eval_cont (c:cont) (v:value) : value =
match v with
| Underflow -> Underflow
| Vnum v ->
......@@ -574,8 +571,8 @@ One would want to write in Why:
| A e2 k -> eval_cont (B (Vnum v) k) (eval_0 e2)
| B v1 k -> eval_cont k (if v1 >= v then Vnum (v1 - v) else Underflow)
| I -> Vnum v (* v >= 0 by construction *)
end]
end
</pre></blockquote>}
But since the recursion is not structural, Why3 kernel rejects it
(definitions in the logic part of the language must be total)
......@@ -591,7 +588,7 @@ inductive eval_cont cont value value =
eval_cont (B v k) (eval_0 e2) r -> eval_cont (A e2 k) (Vnum v) r
| a2 :
forall v1:int, k:cont, v:int, r:value.
eval_cont k (if v1 >= v then Vnum (v1 - v) else Underflow) r
eval_cont k (if v1 >= v then Vnum (v1 - v) else Underflow) r
-> eval_cont (B v1 k) (Vnum v) r
| a3 :
forall v:int. eval_cont I (Vnum v) (Vnum v)
......@@ -657,12 +654,13 @@ let interpret_4 (p:prog) : value
ensures { result = eval_0 p }
= eval_4 p I
let u0 () = interpret_4 p0
let u1 () = interpret_4 p1
let u2 () = interpret_4 p2
let u3 () = interpret_4 p3
let u4 () = interpret_4 p4
let test () =
(interpret_4 p0,
interpret_4 p1,
interpret_4 p2,
interpret_4 p3,
interpret_4 p4)
end
......@@ -671,21 +669,18 @@ end
(** {2 Reduction Semantics} *)
module R
use import Expr
use import DirectSem
module ReductionSemantics
(**
A small step semantics, defined iteratively with reduction contexts
*)
"Reduction semantics" pour les expressions arithmetiques
--------------------------------------------------------
use import Expr
use import DirectSem
(**
Expressions:
{h <blockquote><pre>
n : int
e : expression
......@@ -693,52 +688,49 @@ e ::= n | e - e
p : program
p ::= e
Exemples:
p0 = 0
p1 = 10 - 6
p2 = (10 - 6) - (7 - 2)
p3 = (7 - 2) - (10 - 6)
p4 = 10 - (2 - 3)
</pre></blockquote>}
Values:
{h <blockquote><pre>
v : value
v ::= n
</pre></blockquote>}
Redexes potentiels:
Potential Redexes:
{h <blockquote><pre>
rp ::= n1 - n2
</pre></blockquote>}
Regle de reduction:
Reduction Rule:
{h <blockquote><pre>
n1 - n2 -> n3
</pre></blockquote>}
(in the case of relative integers Z, all potential redexes are true redexes;
but for natural numbers, not all of them are true ones:
{h <blockquote><pre>
n1 - n2 -> n3 if n1 >= n2
</pre></blockquote>}
a potential redex that is not a true one is stuck.)
(pour les entiers Z, tous les redexes potentiels sont de vrais redexes;
pour les entiers naturels, pas tous ne le sont:
n1 - n2 -> n3 si n1 >= n2
un redex potentiel qui n'en est pas un vrai est "coince" (stuck).)
Fonction de contraction:
contracte : redex_potentiel -> expression + stuck
contracte (n1 - n2) = n3 si n3 = n1 - n2
Contraction Function:
{h <blockquote><pre>
contract : redex_potentiel -> expression + stuck
contract (n1 - n2) = n3 si n3 = n1 - n2
</pre></blockquote>}
and if there are only non-negative numbers:
{h <blockquote><pre>
contract (n1 - n2) = n3 if n1 >= n2 and n3 = n1 - n2
contract (n1 - n2) = stuck if n1 < n2
</pre></blockquote>}
*)
predicate is_a_redex (e:expr) =
match e with
| Sub (Cte _) (Cte _) -> true
| _ -> false
end
let contracte (e:expr) : expr
let contract (e:expr) : expr
requires { is_a_redex e }
ensures { eval_0 result = eval_0 e }
=
......@@ -748,16 +740,11 @@ let contracte (e:expr) : expr
end
(*
et si on n'a que des entiers naturels,
contracte (n1 - n2) = n3 si n1 >= n2 et n3 = n1 - n2
contracte (n1 - n2) = stuck si n1 < n2
Contextes de reduction:
Reduction Contexts:
{h <blockquote><pre>
C : cont
C ::= [] | [C e] | [v C]
</pre></blockquote>}
*)
type context = Empty | Left context expr | Right int context
......@@ -788,14 +775,14 @@ let rec lemma recompose_values (c:context) (e1 e2:expr) : unit
| Right n c -> recompose_values c (Sub (Cte n) e1) (Sub (Cte n) e2)
end
let rec lemma recompose_inversion (c:context) (e:expr)
requires {
match c with Empty -> false | _ -> true end \/
let rec lemma recompose_inversion (c:context) (e:expr)
requires {
match c with Empty -> false | _ -> true end \/
match e with Cte _ -> false | Sub _ _ -> true end }
variant { c }
ensures { match recompose c e with
ensures { match recompose c e with
Cte _ -> false | Sub _ _ -> true end }
= match c with
= match c with
| Empty -> ()
| Left c e2 -> recompose_inversion c (Sub e e2)
| Right n1 c -> recompose_inversion c (Sub (Cte n1) e)
......@@ -803,25 +790,26 @@ let rec lemma recompose_inversion (c:context) (e:expr)
(*
Decomposition:
dec_ou_val = (C, rp) | v
fonction de decomposition:
decompose_term : expression * cont -> dec_ou_val
{h <blockquote><pre>
dec_or_val = (C, rp) | v
</pre></blockquote>}
Decomposition function:
{h <blockquote><pre>
decompose_term : expression * cont -> dec_or_val
decompose_term (n, C) = decompose_cont (C, n)
decompose_term (e1 - e2, C) = decompose_term (e1, [C e2])
decompose_cont : cont * value -> dec_ou_val
decompose_cont : cont * value -> dec_or_val
decompose_cont ([], n) = n
decompose_cont ([C e], n) = decompose_term (e, [n c])
decompose_term ([n1 C], n2) = (C, n1 - n2)
decompose : expression -> dec_ou_val
decompose : expression -> dec_or_val
decompose e = decompose_term (e, [])
</pre></blockquote>}
*)
exception NoRedex
exception Stuck
predicate is_a_value (e:expr) =
match e with
......@@ -834,7 +822,7 @@ let rec decompose_term (e:expr) (c:context) : (context, expr)
recompose c1 e1 = recompose c e /\
is_a_redex e1 }
diverges
raises { NoRedex -> is_a_value (recompose c e) }
raises { Stuck -> is_a_value (recompose c e) }
=
match e with
| Cte n -> decompose_cont c n
......@@ -846,10 +834,10 @@ with decompose_cont (c:context) (n:int) : (context, expr)
recompose c1 e1 = recompose c (Cte n) /\
is_a_redex e1 }
diverges
raises { NoRedex -> is_a_value (recompose c (Cte n)) }
raises { Stuck -> is_a_value (recompose c (Cte n)) }
=
match c with
| Empty -> raise NoRedex
| Empty -> raise Stuck
| Left c e -> decompose_term e (Right n c)
| Right n1 c -> (c, Sub (Cte n1) (Cte n))
end
......@@ -858,27 +846,26 @@ let decompose (e:expr) : (context, expr)
ensures { let (c1,e1) = result in recompose c1 e1 = e /\
is_a_redex e1 }
diverges
raises { NoRedex -> is_a_value e }
raises { Stuck -> is_a_value e }
=
decompose_term e Empty
(*
One reduction step:
{h <blockquote><pre>
reduce : expression -> expression + stuck
Un pas de reduction:
reduis : expression -> expression + stuck
si decompose e = v
alors reduis e = stuck
si decompose e = (C, rp)
et contracte rp = stuck
alors reduis e = stuck
if decompose e = v
then reduce e = stuck
si decompose e = (C, rp)
et contracte rp = c
alors reduis e = recompose (C, c)
if decompose e = (C, rp)
and contract rp = stuck
then reduce e = stuck
if decompose e = (C, rp)
and contract rp = c
then reduce e = recompose (C, c)
</pre></blockquote>}
*)
(** {4 Exercise 2.0}
......@@ -886,26 +873,27 @@ alors reduis e = recompose (C, c)
*)
let reduis (e:expr) : expr
let reduce (e:expr) : expr
ensures { eval_0 result = eval_0 e }
diverges
raises { NoRedex -> is_a_value e }
raises { Stuck -> is_a_value e }
=
let (c,r) = decompose e in
recompose c (contracte r)
recompose c (contract r)
(*
Evaluation basee sur la reduction iteree:
Evaluation based on iterated reduction:
{h <blockquote><pre>
itere : red_ou_val -> value + erreur
itere v = v
si contracte rp = stuck
alors itere (C, rp) = stuck
if contract rp = stuck
then itere (C, rp) = stuck
si contracte rp = c
alors itere (C, rp) = itere (decompose (recompose (C, c)))
if contract rp = c
then itere (C, rp) = itere (decompose (recompose (C, c)))
</pre></blockquote>}
*)
......@@ -914,9 +902,9 @@ let rec itere (e:expr) : int
ensures { eval_0 e = result }
=
try
let e' = reduis e in
let e' = reduce e in
itere e'
with NoRedex ->
with Stuck ->
match e with
| Cte n -> n
| _ -> absurd
......@@ -934,7 +922,7 @@ let refocus c e
ensures { let (c1,e1) = result in
recompose c1 e1 = recompose c e /\
is_a_redex e1 }
raises { NoRedex -> is_a_value (recompose c e) }
raises { Stuck -> is_a_value (recompose c e) }
= decompose_term e c
let rec itere_opt (c:context) (e:expr) : int
......@@ -943,8 +931,8 @@ let rec itere_opt (c:context) (e:expr) : int
=
try
let (c,r) = refocus c e in
itere_opt c (contracte r)
with NoRedex ->
itere_opt c (contract r)
with Stuck ->
match recompose c e with
| Cte n -> n
| _ -> absurd
......@@ -962,7 +950,130 @@ let rec normalize (e:expr)
Derive an abstract machine
*)
(* TODO *)
(*
(c,Cte n)_1 -> (c,n)_2
(c,Sub e1 e2)_1 -> (Left c e2,e1)_1
(Empty,n)_2 -> stop with result = n
(Left c e,n)_2 -> (Right n c,e)_1
(Right n1 c,n)_2 -> (c,Cte (n1 - n))_1
*)
let rec eval_1 c e
diverges
ensures { result = eval_0 (recompose c e) }
= match e with
| Cte n -> eval_2 c n
| Sub e1 e2 -> eval_1 (Left c e2) e1
end
with eval_2 c n
diverges
ensures { result = eval_0 (recompose c (Cte n)) }
= match c with
| Empty -> n
| Left c e -> eval_1 (Right n c) e
| Right n1 c -> eval_1 c (Cte (n1 - n))
end
let interpret p
diverges
ensures { result = eval_0 p }
= eval_1 Empty p
let test () diverges =
(interpret p0,
interpret p1,
interpret p2,
interpret p3,
interpret p4)
end
module RWithError
use import Expr
use import SemWithError
(** {4 Exercise 2.3}
An abstract machine for the case with errors
*)
(*
(c,Cte n)_1 -> (c,n)_2
(c,Sub e1 e2)_1 -> (Left c e2,e1)_1
(Empty,n)_2 -> stop with result = n
(Left c e,n)_2 -> (Right n c,e)_1
(Right n1 c,n)_2 -> stop with Underflow if n1 < n
(Right n1 c,n)_2 -> (c,Cte (n1 - n))_1 if n1 >= n
*)
type context = Empty | Left context expr | Right int context
function recompose (c:context) (e:expr) : expr =
match c with
| Empty -> e
| Left c e2 -> recompose c (Sub e e2)
| Right n1 c -> recompose c (Sub (Cte n1) e)
end
let rec lemma recompose_values (c:context) (e1 e2:expr) : unit
requires { eval_0 e1 = eval_0 e2 }
variant { c }
ensures { eval_0 (recompose c e1) = eval_0 (recompose c e2) }
= match c with
| Empty -> ()
| Left c e -> recompose_values c (Sub e1 e) (Sub e2 e)
| Right n c -> recompose_values c (Sub (Cte n) e1) (Sub (Cte n) e2)
end
let rec lemma recompose_underflow (c:context) (e:expr) : unit
requires { eval_0 e = Underflow }
variant { c }
ensures { eval_0 (recompose c e) = Underflow }
= match c with
| Empty -> ()
| Left c e1 -> recompose_underflow c (Sub e e1)
| Right n c -> recompose_underflow c (Sub (Cte n) e)
end
let rec eval_1 c e
diverges
ensures { result = eval_0 (recompose c e) }
= match e with
| Cte n -> if n >= 0 then eval_2 c n else Underflow
| Sub e1 e2 -> eval_1 (Left c e2) e1
end
with eval_2 c n
requires { n >= 0 }
diverges
ensures { result = eval_0 (recompose c (Cte n)) }
= match c with
| Empty -> Vnum n
| Left c e -> eval_1 (Right n c) e
| Right n1 c -> if n1 >= n then eval_1 c (Cte (n1 - n)) else Underflow
end
let interpret p
diverges
ensures { result = eval_0 p }
= eval_1 Empty p
let test () diverges =
(interpret p0,
interpret p1,
interpret p2,
interpret p3,
interpret p4)
end
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment