Evaluation by explicit substitution

Executable Specification

[View ees.sig] [View ees.mod]
sig ees.

% Natural numbers
kind natural    type.
type z          natural.
type s          natural -> natural.

% Syntactic category of types
kind typ        type.
type nat        typ.
type arr        typ -> typ -> typ.

% Syntactic category of expressions
kind exp        type.
type num        natural -> exp.
type plus       exp -> exp -> exp.
type lam        typ -> (exp -> exp) -> exp.
type app        exp -> exp -> exp.

% Static semantics
type natural    natural -> o.
type typ        typ -> o.
type of         exp -> typ -> o.

% Dynamic (evaluation) semantics
type sum        natural -> natural -> natural -> o.
type val        exp -> o.
type eval       exp -> exp -> o.

module ees.

% The system L_{+,->}

% Closed natural numbers
natural z.
natural (s N) :- natural N.

% Closed types
typ nat.
typ (arr T1 T2) :- typ T1, typ T2.

% Static semantics
of (num N) nat :- natural N.
of (plus E1 E2) nat :- of E1 nat, of E2 nat.
of (lam T1 E2) (arr T1 T2) :- typ T1, pi x\ of x T1 => of (E2 x) T2.
of (app E1 E2) T :- of E1 (arr T2 T), of E2 T2.

% Primitive addition operation
sum z N2 N2 :- natural N2.
sum (s N1) N2 (s N3) :- sum N1 N2 N3.

% Values
val (num N) :- natural N.
val (lam T1 E2).

% Evaluation
eval (num N) (num N) :- natural N.
eval (plus E1 E2) (num N) :- eval E1 (num N1), eval E2 (num N2), sum N1 N2 N.
eval (lam T1 E2) (lam T1 E2).
eval (app E1 E2) V :- eval E1 (lam T E), eval E2 V2, eval (E V2) V.

Reasoning

[View ees.thm]

Click on a command or tactic to see a detailed view of its use.

%
% We formulate an environment semantics for L_{+,->} where the
% environment is a top-level explicit substitution, and where the
% evaluation relation is between such substituted expressions.  We
% prove its equivalence with the substitution-based (or big-step)
% evaluation semantics.
%
% Author: J. Todd Wilson

Specification "ees".
Close natural, typ, exp.

% Nominals

Theorem member_prune : forall G E, nabla (x:exp),
  member (E x) G ->
    exists E', E = y\E'.


% List operations

Define insert : o -> olist -> olist -> prop by
  insert E L (E :: L) ;
  insert E (F :: L) (F :: L') := insert E L L'.

Theorem member_insert : forall E1 E2 L L',
  insert E1 L L' -> member E2 L' ->
    E1 = E2 \/ member E2 L.

Theorem insert_prune : forall E L1 L2, nabla (x:exp),
  insert (E x) (L1 x) L2 ->
    exists E' L1', E = x\E' /\ L1 = x\L1'.


% Basic lemmas for L_{+,->}

Theorem sum_type : forall N1 N2 N,
  {sum N1 N2 N} ->
    {natural N1} /\ {natural N2} /\ {natural N}.


% The definitions of sexp and force below are given wrt an unordered
% list of distinct free value variables (hence, insert instead of ::)

Define vals : olist -> prop by
  vals nil ;
  nabla x, vals (val x :: H) := vals H.

Theorem insert_vals : forall E H H', insert E H H' -> vals H' -> vals H.


% Substituted expressions (sexp), substitutions (sub), and extended
% values (xval) are defined by mutual induction.  Essentially, an sexp
% is a pair (S,E), where S is a sub and E is an exp; a sub is a list
% of pairs (x,V), where x is a nominal and V is an xval; and an xval
% is a substituted expression (s,V) where V is a val.  An sexp (S,E)
% is defined wrt a list of value variables H; we require all the free
% variables of E to appear in either S or H and all type annotations
% on lambda terms to be closed.

Kind sexp type.

Type rep  exp -> sexp -> o.      % rep x V ("replace") is the substitution [V/x]
Type sb   olist -> exp -> sexp.  % sb S E is the sexp (S,E)

Define sexp : olist -> sexp -> prop, sub : olist -> prop, xval : sexp -> prop by
  nabla x, sexp (H x) (sb (S x) x) :=
    nabla x, vals (H x) /\ sub (S x) /\ member (val x) (H x) ;
  nabla x, sexp (H x) (sb (S x) x) :=
    nabla x, vals (H x) /\ sub (S x) /\ exists V, member (rep x V) (S x) ;
  sexp H (sb S (num N)) := vals H /\ sub S /\ {natural N} ;
  sexp H (sb S (plus E1 E2)) := sexp H (sb S E1) /\ sexp H (sb S E2) ;
  sexp H (sb S (lam T1 E2)) :=
    {typ T1} /\ nabla x, sexp (val x :: H) (sb S (E2 x)) ;
  sexp H (sb S (app E1 E2)) := sexp H (sb S E1) /\ sexp H (sb S E2) ;

  sub nil ;
  nabla x, sub (rep x V :: S) := xval V /\ sub S ;

  xval (sb nil (num N)) := {natural N} ;
  xval (sb S (lam T1 E2)) := sexp nil (sb S (lam T1 E2)).


% Invariants of the above definition

Theorem sexp_type : forall H E',
  sexp H E' ->
    exists S E, E' = sb S E /\ vals H /\ sub S.

Theorem sexp_abs : forall H H' S E V, nabla x,
  insert (val x) H' (H x) -> sexp (H x) (sb S (E x)) -> xval V ->
    sexp H' (sb (rep x V :: S) (E x)).

Theorem sub_xval : forall S X V, sub S -> member (rep X V) S -> xval V.

Theorem sub_uniq : forall S V1 V2, nabla x,
  sub (S x) -> member (rep x V1) (S x) -> member (rep x V2) (S x) ->
    V1 = V2.


% Evaluation by explicit subsitution (environment semantics).  Note
% that, in the app case, the "output" argument of ees contains an
% arbitrary new nominal, needed because the substitution is extended.
% This means, in particular, that ees is not deterministic.

Define ees : sexp -> sexp -> prop by
  nabla x, ees (sb (S x) x) V :=
     nabla x, member (rep x V) (S x) ;
  ees (sb S (num N)) (sb nil (num N)) := {natural N} ;
  ees (sb S (plus E1 E2)) (sb nil (num N)) := exists N1 N2,
     ees (sb S E1) (sb nil (num N1)) /\
     ees (sb S E2) (sb nil (num N2)) /\
     {sum N1 N2 N} ;
  ees (sb S (lam T1 E2)) (sb S (lam T1 E2)) ;
  nabla x, ees (sb S (app E1 E2)) (V x) := exists S' T E V2,
     ees (sb S E1) (sb S' (lam T E)) /\
     ees (sb S E2) V2 /\
     nabla x, ees (sb (rep x V2 :: S') (E x)) (V x).

Theorem ees_type : forall E V, sexp nil E -> ees E V -> xval V.


% Forcing of an explicit/delayed substitution, defined structurally

Define force : olist -> sexp -> exp -> prop by
  nabla x, force (H x) (sb (S x) x) x  :=
    nabla x, member (val x) (H x) ;
  nabla x, force (H x) (sb (S x) x) V' :=
    exists V, nabla x, member (rep x V) (S x) /\ force nil V V' ;
  force H (sb S (num N)) (num N) ;
  force H (sb S (plus E1 E2)) (plus E1' E2') :=
    force H (sb S E1) E1' /\ force H (sb S E2) E2' ;
  force H (sb S (lam T1 E2)) (lam T1 E2') :=
    nabla x, force (val x :: H) (sb S (E2 x)) (E2' x) ;
  force H (sb S (app E1 E2)) (app E1' E2') :=
    force H (sb S E1) E1' /\ force H (sb S E2) E2'.

Theorem force_prune : forall H E E', nabla (x:exp),
  force (H x) E (E' x) ->
    exists E'', E' = x\E''.

Theorem force_abs : forall H H' S E E' V V', nabla x,
  insert (val x) H' (H x) -> sexp (H x) (sb S (E x)) ->
  force (H x) (sb S (E x)) (E' x)  -> xval V -> force nil V V' ->
    force H' (sb (rep x V :: S) (E x)) (E' V').

Theorem force_inv : forall V V',
  force nil V V' -> xval V ->
    (exists N, V = sb nil (num N) /\ V' = num N /\ {natural N}) \/
    (exists S T E E', V = sb S (lam T E) /\ V' = lam T E').



%%%%%%%%%%%%%%%% Main Theorem
%
% We have defined two (big-step) evaluation systems: L_{+,->} under
% eval, and sexps under ees.  The main theorem is that force is a
% strong bisimulation between these two systems.

% Only-if direction

Theorem ees_eval : forall E V E',
  sexp nil E -> force nil E E' -> ees E V ->
    exists V', force nil V V' /\ {eval E' V'}.


% If direction

Theorem eval_ees : forall E E' V',
  sexp nil E -> force nil E E' -> {eval E' V'} ->
    exists V, force nil V V' /\ ees E V.


% Consider the subsets X(H) of sexp and E(H) of exp defined by
%    X(H) = { E  | sexp H E /\ exists E', E = sb nil E'},
%    E(H) = { E' | sexp H (sb nil E') }.
% We show that, for any H, (force H - -) is a bijection (and thus, by
% strong bisimulation, an isomorphism when H = nil) between X(H) and
% E(H).

Theorem force_bij_exst : forall H E, sexp H (sb nil E) -> force H (sb nil E) E.

Theorem force_bij_uniq : forall H E E1 E2,
  sexp H (sb nil E) -> force H (sb nil E) E1 -> force H (sb nil E) E2 ->
    E1 = E2.

Theorem force_bij_uniq' : forall H E E1 E2,
  sexp H (sb nil E) -> force H (sb nil E1) E -> force H (sb nil E2) E ->
    E1 = E2.