Wiki Agenda Contact Version française

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

ObligationsAlt-Ergo 2.0.0CVC4 1.5Z3 4.4.1
VC eq0.01------
VC subst_c0.01------
subst_c_commute---------
induction_ty_lex
subst_c_commute.00.01------
VC reduction---------
split_goal_right
VC reduction.00.01------
VC reduction.10.01------
VC reduction.20.00------
VC reduction.30.01------
VC reduction.40.01------
VC reduction.50.01------
VC reduction.60.23------
VC reduction.70.01------
VC reduction.80.22------
VC reduction.90.01------
VC reduction.100.15------
VC reduction.110.02------
VC reduction.12------0.90
VC reduction.130.01------
VC reduction.140.01------
VC reduction.15------0.20
VC reduction.160.01------
VC reduction.170.04------
VC i0.01------
VC test_SKK0.00------
VC reduce_step0.08------
VC value_in_context---------
split_vc
VC value_in_context.0---0.02---
VC value_in_context.1---------
destruct_alg_subst (subst c t)
VC value_in_context.1.0---0.04---
VC value_in_context.1.1---0.04---
VC value_in_context.1.2---------
destruct_alg_subst x3
VC value_in_context.1.2.0---0.02---
VC value_in_context.1.2.1---0.02---
VC value_in_context.1.2.2---------
destruct_alg_subst x4
VC value_in_context.1.2.2.0---0.04---
VC value_in_context.1.2.2.1---0.02---
VC value_in_context.1.2.2.2---0.02---
VC value_in_context.2---0.03---
VC value_in_context.3---------
destruct_alg_subst (subst c t)
VC value_in_context.3.0---0.03---
VC value_in_context.3.1---0.02---
VC value_in_context.3.2---------
destruct_alg_subst x3
VC value_in_context.3.2.0---0.04---
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.02---
VC value_in_context.3.2.2.1---0.01---
VC value_in_context.3.2.2.2---0.02---
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_value0.01------
VC reduction2---------
split_goal_right
VC reduction2.00.02------
VC reduction2.10.02------
VC reduction2.20.03------
VC reduction2.30.03------
VC reduction2.40.20------
VC reduction2.50.04------
VC reduction2.60.01------
VC reduction2.70.11------
VC reduction2.8---------
split_goal_right
VC reduction2.8.00.01------
VC reduction2.8.1------0.42
VC ks0.01------
VC reduction3---------
split_goal_right
VC reduction3.00.01------
VC reduction3.10.02------
VC reduction3.20.02------
VC reduction3.3------0.02
VC reduction3.40.07------
VC reduction3.50.03------
VC reduction3.60.02------
VC reduction3.7------0.24
VC reduction3.80.11------
VC reduction3.90.06------
VC reduction3.10------0.03
VC ks_even_odd0.09------