Wiki Agenda Contact English version

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.


Auteurs: Jean-Christophe Filliâtre / Andrei Paskevich

Catégories: Semantics of languages

Outils: Why3

Références: 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

ObligationsCVC4 1.8CVC5 1.0.5
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 reduction0.05---
VC for test_SKK---0.01
VC for reduce_step0.09---
VC for value_in_context---0.03
VC for irreducible_is_value---3.49
VC for reduction2------
split_vc
variant decrease0.04---
precondition0.04---
variant decrease0.05---
precondition0.04---
unreachable point0.08---
unreachable point0.05---
unreachable point0.04---
postcondition---0.05
postcondition------
split_vc
postcondition0.04---
postcondition0.08---
VC for ks---0.02
VC for reduction30.19---
VC for ks_even_odd---0.03