## Call-by-value reduction of SK terms

Problem 2 of the second verified software competition.

The ZIP file below contains both the source code, the Why3 proof session file and the Coq scripts of the proofs made in Coq. The Why3 source code is then displayed, followed by a summary of the proofs.

**Authors:** Jean-Christophe Filliâtre / Andrei Paskevich

**Topics:** Semantics of languages

**Tools:** Why3

**References:** The 2nd Verified Software Competition

see also the index (by topic, by tool, by reference, by year)

download ZIP archive

(* The 2nd Verified Software Competition (VSTTE 2012) https://sites.google.com/site/vstte2012/compet Problem 2: Combinators S and K *) module Combinators type term = S | K | App term term let rec predicate eq (x y : term) ensures { result <-> x = y } = match x, y with | S, S -> True | K, K -> True | App x1 x2, App y1 y2 -> eq x1 y1 && eq x2 y2 | _, _ -> False end (* specification of the CBV reduction *) predicate is_value (t: term) = match t with | K | S -> true | App K v | App S v -> is_value v | App (App S v1) v2 -> is_value v1 /\ is_value v2 | _ -> false end (* contexts *) type context = Hole | Left context term | Right term context predicate is_context (c: context) = match c with | Hole -> true | Left c _ -> is_context c | Right v c -> is_value v && is_context c end function subst (c: context) (t: term) : term = match c with | Hole -> t | Left c1 t2 -> App (subst c1 t) t2 | Right v1 c2 -> App v1 (subst c2 t) end (* one step reduction (the notion of context is inlined in the following definition) *) inductive (-->) (t1 t2: term) = | red_K: forall c: context. is_context c -> forall v1 v2: term. is_value v1 -> is_value v2 -> subst c (App (App K v1) v2) --> subst c v1 | red_S: forall c: context. is_context c -> forall v1 v2 v3: term. is_value v1 -> is_value v2 -> is_value v3 -> subst c (App (App (App S v1) v2) v3) --> subst c (App (App v1 v3) (App v2 v3)) clone relations.ReflTransClosure with type t = term, predicate rel = (-->) predicate (-->*) (t1 t2: term) = relTR t1 t2 type zipper = ZHole | ZLeft context term | ZRight term context let rec function subst_c (c ct:context) : context ensures { is_context c /\ is_context ct -> is_context result } = match c with | Hole -> ct | Left c1 t2 -> Left (subst_c c1 ct) t2 | Right v1 c2 -> Right v1 (subst_c c2 ct) end lemma subst_c_commute : forall c [@induction] ct t. subst c (subst ct t) = subst (subst_c c ct) t (* task 1: implement CBV reduction *) let rec reduction (ghost c:context) (t: term) : term diverges (* there are non-normalizable terms... *) requires { is_context c } ensures { subst c t -->* subst c result } ensures { is_value result } = match t with | S -> S | K -> K | App t1 t2 -> let v1 = reduction (subst_c c (Left Hole t2)) t1 in let v2 = reduction (subst_c c (Right v1 Hole)) t2 in match v1 with | K | S | App S _ -> App v1 v2 | App K v3 -> v3 | App (App S v3) v4 -> reduction c (App (App v3 v2) (App v4 v2)) | _ -> absurd end end exception BenchFailure let constant i = App (App S K) K let test_SKK () diverges (* would be hard to prove terminating *) raises { BenchFailure -> true } = let t1 = reduction Hole (App i i) in if not (eq t1 i) then raise BenchFailure; let t2 = reduction Hole (App (App (App (App K K) K) K) K) in if not (eq t2 K) then raise BenchFailure; t1, t2 (* an irreducible term is a value *) predicate irreducible (t: term) = forall t': term. not (t-->t') exception Fail let rec ghost reduce_step (c:context) (t:term) : term requires { is_context c } ensures { subst c t --> subst c result } raises { Fail -> is_value t } variant { t } = match t with | App t1 t2 -> try App (reduce_step (subst_c c (Left Hole t2)) t1) t2 with Fail -> try App t1 (reduce_step (subst_c c (Right t1 Hole)) t2) with Fail -> match t1 with | App K v -> v | App (App S v1) v2 -> App (App v1 t2) (App v2 t2) | _ -> raise Fail end end end | _ -> raise Fail end let rec lemma value_in_context (c:context) (t:term) : unit requires { is_value (subst c t) } ensures { is_value t } variant { c } = match c with | Hole -> () | Left cl _ -> value_in_context cl t | Right _ cr -> value_in_context cr t end let lemma irreducible_is_value (t:term) : unit ensures { irreducible t <-> is_value t } = try let _ = reduce_step Hole t in () with Fail -> () end (* task 2 *) use int.Int inductive only_K (t: term) = | only_K_K: only_K K | only_K_App: forall t1 t2: term. only_K t1 -> only_K t2 -> only_K (App t1 t2) let rec reduction2 (ghost c:context) (t: term) : term requires { only_K t /\ is_context c } ensures { only_K result /\ is_value result } ensures { subst c t -->* subst c result } variant { t } = match t with | K -> K | App t1 t2 -> let v1 = reduction2 (subst_c c (Left Hole t2)) t1 in let v2 = reduction2 (subst_c c (Right v1 Hole)) t2 in match v1 with | K -> App v1 v2 | App K v3 -> v3 | _ -> absurd end | _ -> absurd end (* task 3 *) let rec function ks (n: int) : term requires { n >= 0 } ensures { only_K result } variant { n } = if n = 0 then K else App (ks (n-1)) K use number.Parity let rec reduction3 (ghost c:context) (ghost n:int) (t: term) : term requires { n >= 0 /\ t = ks n /\ is_context c } variant { n } ensures { subst c t -->* subst c result } ensures { is_value result } ensures { even n -> result = K } ensures { odd n -> result = App K K } = match t with | K -> K | App t1 t2 -> let v1 = reduction3 (subst_c c (Left Hole t2)) (n-1) t1 in let v2 = reduction3 (subst_c c (Right v1 Hole)) 0 t2 in match v1 with | K -> App v1 v2 | App K v3 -> v3 | _ -> absurd end | _ -> absurd end let lemma ks_even_odd (n:int) : unit requires { n >= 0 } ensures { ks (2*n) -->* K } ensures { ks (2*n+1) -->* App K K } = let _ = reduction3 Hole (2*n) (ks (2*n)) in let _ = reduction3 Hole (2*n+1) (ks (2*n+1)) in () end

# Why3 Proof Results for Project "vstte12_combinators"

## Theory "vstte12_combinators.Combinators": fully verified

Obligations | Alt-Ergo 2.0.0 | CVC4 1.5 | CVC4 1.6 | Z3 4.4.1 | ||||

VC eq | 0.01 | --- | --- | --- | ||||

VC subst_c | 0.01 | --- | --- | --- | ||||

subst_c_commute | --- | --- | --- | --- | ||||

induction_ty_lex | ||||||||

subst_c_commute.0 | 0.01 | --- | --- | --- | ||||

VC reduction | --- | --- | --- | --- | ||||

split_goal_right | ||||||||

VC reduction.0 | 0.01 | --- | --- | --- | ||||

VC reduction.1 | 0.01 | --- | --- | --- | ||||

VC reduction.2 | 0.00 | --- | --- | --- | ||||

VC reduction.3 | 0.01 | --- | --- | --- | ||||

VC reduction.4 | 0.01 | --- | --- | --- | ||||

VC reduction.5 | 0.01 | --- | --- | --- | ||||

VC reduction.6 | 0.23 | --- | --- | --- | ||||

VC reduction.7 | 0.01 | --- | --- | --- | ||||

VC reduction.8 | 0.22 | --- | --- | --- | ||||

VC reduction.9 | 0.01 | --- | --- | --- | ||||

VC reduction.10 | 0.15 | --- | --- | --- | ||||

VC reduction.11 | 0.02 | --- | --- | --- | ||||

VC reduction.12 | --- | --- | --- | 0.90 | ||||

VC reduction.13 | 0.01 | --- | --- | --- | ||||

VC reduction.14 | 0.01 | --- | --- | --- | ||||

VC reduction.15 | --- | --- | --- | 0.20 | ||||

VC reduction.16 | 0.01 | --- | --- | --- | ||||

VC reduction.17 | 0.04 | --- | --- | --- | ||||

VC test_SKK | 0.00 | --- | --- | --- | ||||

VC reduce_step | 0.08 | --- | --- | --- | ||||

VC value_in_context | --- | --- | --- | --- | ||||

split_vc | ||||||||

VC value_in_context.0 | --- | 0.03 | --- | --- | ||||

VC value_in_context.1 | --- | --- | --- | --- | ||||

destruct_alg_subst (subst x1 t) | ||||||||

VC value_in_context.1.0 | --- | --- | 0.03 | --- | ||||

VC value_in_context.1.1 | --- | --- | 0.03 | --- | ||||

VC value_in_context.1.2 | --- | --- | --- | --- | ||||

destruct_alg_subst x2 | ||||||||

VC value_in_context.1.2.0 | --- | --- | 0.04 | --- | ||||

VC value_in_context.1.2.1 | --- | --- | 0.04 | --- | ||||

VC value_in_context.1.2.2 | --- | --- | 0.04 | --- | ||||

VC value_in_context.2 | --- | 0.02 | --- | --- | ||||

VC value_in_context.3 | --- | --- | --- | --- | ||||

destruct_alg_subst (subst x t) | ||||||||

VC value_in_context.3.0 | --- | --- | 0.03 | --- | ||||

VC value_in_context.3.1 | --- | --- | 0.03 | --- | ||||

VC value_in_context.3.2 | --- | --- | --- | --- | ||||

destruct_alg_subst x3 | ||||||||

VC value_in_context.3.2.0 | --- | --- | 0.03 | --- | ||||

VC value_in_context.3.2.1 | --- | --- | 0.04 | --- | ||||

VC value_in_context.3.2.2 | --- | --- | --- | --- | ||||

destruct_alg_subst x4 | ||||||||

VC value_in_context.3.2.2.0 | --- | --- | 0.03 | --- | ||||

VC value_in_context.3.2.2.1 | --- | --- | 0.04 | --- | ||||

VC value_in_context.3.2.2.2 | --- | --- | 0.04 | --- | ||||

VC value_in_context.4 | --- | --- | --- | --- | ||||

destruct_alg_subst c | ||||||||

VC value_in_context.4.0 | --- | 0.02 | --- | --- | ||||

VC value_in_context.4.1 | --- | 0.01 | --- | --- | ||||

VC value_in_context.4.2 | --- | 0.01 | --- | --- | ||||

VC irreducible_is_value | 0.01 | --- | --- | --- | ||||

VC reduction2 | --- | --- | --- | --- | ||||

split_goal_right | ||||||||

VC reduction2.0 | 0.02 | --- | --- | --- | ||||

VC reduction2.1 | 0.02 | --- | --- | --- | ||||

VC reduction2.2 | 0.03 | --- | --- | --- | ||||

VC reduction2.3 | 0.03 | --- | --- | --- | ||||

VC reduction2.4 | 0.20 | --- | --- | --- | ||||

VC reduction2.5 | 0.04 | --- | --- | --- | ||||

VC reduction2.6 | 0.01 | --- | --- | --- | ||||

VC reduction2.7 | 0.11 | --- | --- | --- | ||||

VC reduction2.8 | --- | --- | --- | --- | ||||

split_goal_right | ||||||||

VC reduction2.8.0 | 0.01 | --- | --- | --- | ||||

VC reduction2.8.1 | --- | --- | --- | 0.42 | ||||

VC ks | 0.01 | --- | --- | --- | ||||

VC reduction3 | --- | --- | --- | --- | ||||

split_goal_right | ||||||||

VC reduction3.0 | 0.01 | --- | --- | --- | ||||

VC reduction3.1 | 0.02 | --- | --- | --- | ||||

VC reduction3.2 | 0.02 | --- | --- | --- | ||||

VC reduction3.3 | --- | --- | --- | 0.02 | ||||

VC reduction3.4 | 0.07 | --- | --- | --- | ||||

VC reduction3.5 | 0.03 | --- | --- | --- | ||||

VC reduction3.6 | 0.02 | --- | --- | --- | ||||

VC reduction3.7 | --- | --- | --- | 0.24 | ||||

VC reduction3.8 | 0.11 | --- | --- | --- | ||||

VC reduction3.9 | 0.06 | --- | --- | --- | ||||

VC reduction3.10 | --- | --- | --- | 0.03 | ||||

VC ks_even_odd | 0.09 | --- | --- | --- |