## 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.

Topics: Semantics of languages

Tools: Why3

References: The 2nd Verified Software Competition

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

```(* The 2nd Verified Software Competition (VSTTE 2012)

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

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

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 CVC4 1.8 CVC5 1.0.0 VC for eq --- 0.01 VC for subst_c --- 0.02 subst_c_commute --- --- induction_ty_lex subst_c_commute.0 --- 0.02 VC for reduction 0.05 --- VC for test_SKK --- 0.01 VC for reduce_step --- 0.97 VC for value_in_context --- 0.03 VC for irreducible_is_value --- 0.86 VC for reduction2 0.23 --- VC for ks --- 0.02 VC for reduction3 --- 1.04 VC for ks_even_odd --- 0.03