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

  (* 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))

  lemma red_left:
    forall t1 t2 t: term. t1 --> t2 -> App t1 t --> App t2 t

  lemma red_right:
    forall v t1 t2: term. is_value v -> t1 --> t2 -> App v t1 --> App v t2

  clone import relations.ReflTransClosure
    with type t = term, predicate rel = (-->)
  predicate (-->*) (t1 t2: term) = relTR t1 t2

  lemma red_star_left:
    forall t1 t2 t: term. t1 -->* t2 -> App t1 t -->* App t2 t

  lemma red_star_right:
    forall v t1 t2: term. is_value v -> t1 -->* t2 -> App v t1 -->* App v t2

  (* task 1: implement CBV reduction *)

  let rec reduction (t: term) : term
    diverges (* there are non-normalizable terms... *)
    ensures { t -->* result /\ is_value result }
  = match t with
    | S -> S
    | K -> K
    | App t1 t2 -> match reduction t1 with
      | K -> App K (reduction t2)
      | S -> App S (reduction t2)
      | App K v1 -> let _ = reduction t2 in v1
      | App S v1 -> App (App S v1) (reduction t2)
      | App (App S v1) v2 ->
          let v3 = reduction t2 in reduction (App (App v1 v3) (App v2 v3))
      | _ -> absurd
      end
    end

  exception BenchFailure

  constant i : term = App (App S K) K

  let test_SKK ()
    diverges (* would be hard to prove terminating *)
    raises { BenchFailure -> true }
  = let t1 = reduction (App i i) in
    if t1 <> i then raise BenchFailure;
    let t2 = reduction (App (App (App (App K K) K) K) K) in
    if t2 <> K then raise BenchFailure;
    (t1, t2)

  (* an irreducible term is a value *)

  lemma reducible_or_value:
    forall t: term. (exists t': term. t-->t') \/ is_value t

  predicate irreducible (t: term) = forall t': term. not (t-->t')

  lemma irreducible_is_value:
    forall t: term. irreducible t <-> is_value t

  (* task 2 *)

  use import 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)

  lemma only_K_reduces:
    forall t: term. only_K t ->
    exists v: term. t -->* v /\ is_value v /\ only_K v

  function size (t: term) : int = match t with
    | K | S -> 0
    | App t1 t2 -> 1 + size t1 + size t2
  end

  lemma size_nonneg: forall t: term. size t >= 0

  let rec reduction2 (t: term) : term variant { t }
    requires { only_K t }
    ensures { only_K result /\ is_value result }
  = match t with
    | S -> S
    | K -> K
    | App t1 t2 -> match reduction2 t1 with
      | K -> App K (reduction2 t2)
      | S -> App S (reduction2 t2)
      | App K v1 -> let _ = reduction2 t2 in v1
      | App S v1 -> App (App S v1) (reduction2 t2)
      | App (App S v1) v2 ->
          let v3 = reduction2 t2 in reduction2 (App (App v1 v3) (App v2 v3))
      | _ -> absurd
      end
    end

  (* task 3 *)

  function ks (n: int) : term

  axiom ksO: ks 0 = K
  axiom ksS: forall n: int. n >= 0 -> ks (n+1) = App (ks n) K

  lemma ks1: ks 1 = App K K

  lemma only_K_ks: forall n: int. n >= 0 -> only_K (ks n)

  lemma ks_inversion: forall n: int. n >= 0 ->
    n = 0 \/ n > 0 /\ ks n = App (ks (n-1)) K

  lemma ks_injective:
    forall n1 n2: int. n1 >= 0 -> n2 >= 0 -> ks n1 = ks n2 -> n1 = n2

  use import int.Div2

  let rec reduction3 (t: term) : term
    requires { exists n: int. n >= 0 /\ t = ks n }
    diverges (* TODO: prove termination ... *)
    ensures { is_value result /\
      forall n: int. n >= 0 -> (t = ks (2*n)   -> result = K)
                            /\ (t = ks (2*n+1) -> result = App K K) }
  = match t with
    | S -> S
    | K -> K
    | App t1 t2 -> match reduction3 t1 with
      | K -> App K (reduction3 t2)
      | S -> App S (reduction3 t2)
      | App K v1 -> let _ = reduction3 t2 in v1
      | App S v1 -> App (App S v1) (reduction3 t2)
      | App (App S v1) v2 ->
          let v3 = reduction3 t2 in reduction3 (App (App v1 v3) (App v2 v3))
      | _ -> absurd
      end
    end

   lemma ks_value:
     forall n: int. 0 <= n -> is_value (ks n) -> 0 <= n <= 1

   lemma ks_even_odd:
    forall n: int. 0 <= n -> ks (2*n)   -->* K
                          /\ ks (2*n+1) -->* App K K

end

Why3 Proof Results for Project "vstte12_combinators"

Theory "vstte12_combinators.Combinators": fully verified in 37.50 s

ObligationsAlt-Ergo (0.99.1)CVC3 (2.4.1)Coq (8.4pl6)Eprover (1.8-001)Spass (3.7)Vampire (0.6)Z3 (3.2)
red_left------------------3.80
red_right------------------3.82
red_star_left------0.82------------
red_star_right------0.81------------
VC for reduction---------------------
split_goal_wp
  1. postcondition0.01------------------
2. postcondition0.01------------------
3. postcondition---------------------
split_goal_wp
  1. VC for reduction------0.87---0.030.04---
2. VC for reduction0.00------------------
4. postcondition---------------------
split_goal_wp
  1. VC for reduction------0.80---0.030.06---
2. VC for reduction0.00------------------
5. postcondition---------------------
split_goal_wp
  1. VC for reduction------0.83---0.070.03---
2. VC for reduction0.01------------------
6. postcondition---------------------
split_goal_wp
  1. VC for reduction------0.850.040.040.08---
2. VC for reduction0.02------------------
7. postcondition---------------------
split_goal_wp
  1. VC for reduction------0.86------0.32---
2. VC for reduction0.01------------------
8. unreachable point0.04------------------
VC for test_SKK0.01------------------
reducible_or_value------1.48------------
irreducible_is_value------2.73------------
only_K_reduces------1.43------------
size_nonneg------0.85------------
VC for reduction2---------------------
split_goal_wp
  1. postcondition0.01------------------
2. postcondition0.01------------------
3. variant decrease0.02------------------
4. precondition0.04------------------
5. variant decrease0.01------------------
6. precondition0.10------------------
7. postcondition0.02------------------
8. variant decrease0.03------------------
9. precondition0.02------------------
10. postcondition0.01------------------
11. variant decrease0.02------------------
12. precondition0.02------------------
13. postcondition0.04------------------
14. variant decrease0.03------------------
15. precondition0.03------------------
16. postcondition0.04------------------
17. variant decrease0.03------------------
18. precondition0.04------------------
19. variant decrease---------------------
split_goal_wp
  1. VC for reduction2---0.02---0.01---------
2. VC for reduction2---0.02---0.05---------
3. VC for reduction2---0.16---0.58---------
20. precondition---------------------
split_goal_wp
  1. precondition---0.070.860.61---------
21. postcondition0.01------------------
22. unreachable point0.08------------------
ks10.01------------------
only_K_ks------0.84------------
ks_inversion0.01------------------
ks_injective------1.36------------
VC for reduction3---------------------
split_goal_wp
  1. postcondition0.07------------------
2. postcondition---------------------
split_goal_wp
  1. VC for reduction30.010.01------------0.00
2. VC for reduction30.01------------------
3. precondition---0.02---------------
4. precondition---0.06---------------
5. postcondition---------------------
split_goal_wp
  1. VC for reduction30.01------------------
2. VC for reduction3------2.52------------
3. VC for reduction3------1.67------------
6. precondition---0.05---------------
7. postcondition------1.76------------
8. precondition---0.09---------------
9. postcondition---------------------
split_goal_wp
  1. VC for reduction30.060.02------------0.13
2. VC for reduction3------1.58------------
3. VC for reduction30.10------------------
10. precondition---0.07---------------
11. postcondition------2.74------------
12. precondition---0.08---------------
13. precondition------1.62------------
14. postcondition------1.92------------
15. unreachable point0.080.02------------0.04
ks_value------0.92------------
ks_even_odd------0.90------------