User:Rsimmons/CR2

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

Syntax

exp : type.  %name exp E.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.

When we use this %block, it expresses that we can be working in a context with arbitrary expression variables.

%block exps : block {x: exp}.
%worlds (exps) (exp).

Reduction

We can reduce under binders and reduce both sides of an application "in parallel." If we have a β-redex (λx.ea) eb, then after reducing ea (with x free) to ea' (with x free) and reducing eb to eb', we can return [eb'/x]ea', the substitution of eb' into ea'. When we introduce a new variable, we always add in the fact that it can evaluate to itself.

The %block exps_id explicitly states that we will be reducing in a setting with free variables, with the invariant that every variable is added with the invariant that it can evaluate to itself.

reduce : exp -> exp -> type.
%mode reduce +E -E'.

%block exps_id : block {x: exp}{d: reduce x x}.

reduce/lam : reduce (lam E) (lam E')
              <- ({x:exp} reduce x x -> reduce (E x) (E' x)).

reduce/app : reduce (app E1 E2) (app E1' E2')
              <- reduce E1 E1'
              <- reduce E2 E2'.

reduce/beta : reduce (app (lam E1) E2) (E1' E2')
              <- ({x:exp} reduce x x -> reduce (E1 x) (E1' x))
              <- reduce E2 E2'.

%worlds (exps_id) (reduce _ _).
%total E (reduce E _).

Substitution

The substitution theorem says that if we have a term e with x free that reduces to e' (with x still free) and earg reduces to e'arg, then [earg/x]e reduces to [e'arg/x]e'.

The proof is by induction on the structure of the term with the free variable.

substitute 
   : ({x: exp} reduce x x -> reduce (E x) (E' x))
      -> reduce Earg Earg'
      -> reduce (E Earg) (E' Earg') -> type.
%mode substitute +D +Darg -D'.

We actually need to think about what block this theorem will take place in. The "variable case" of our lemma is one where the first argument is [x: exp] [idx: red x x] y, where y is not equal to x. In this case, we will need to insert into the context the lemma that, if

%block exp_subst 
   : block {x: exp}{idx: reduce x x}
      {subst
         : {z: exp}{z': exp}{red: reduce z z'} substitute ([_][_] idx) red idx}.

- : substitute
     ([x] [idx: reduce x x] idx)
     (D : reduce Earg Earg') D.

- : substitute 
     ([x] [idx: reduce x x] 
        reduce/lam 
        (D x idx : {y} reduce y y -> reduce (E x y) (E' x y)))            
     (Darg: reduce Earg Earg')
     (reduce/lam D'
        : reduce (lam ([y] (E Earg) y)) (lam ([y] (E' Earg') y)))
     <- ({y} {idy: reduce y y}
           ({z}{z'}{red_z: reduce z z'} substitute ([_] [_] idy) red_z idy)
           -> substitute ([x] [idx: reduce x x] D x idx y idy) Darg 
              (D' y idy : reduce (E Earg y) (E' Earg' y))).

- : substitute
     ([x] [idx: reduce x x]
        reduce/app
        (Db x idx : reduce (Eb x) (Eb' x))
        (Da x idx : reduce (Ea x) (Ea' x)))
     (Darg: reduce Earg Earg')
     (reduce/app Db' Da' 
        : reduce (app (Ea Earg) (Eb Earg)) (app (Ea' Earg') (Eb' Earg')))
     <- substitute Da Darg (Da': reduce (Ea Earg) (Ea' Earg'))
     <- substitute Db Darg (Db': reduce (Eb Earg) (Eb' Earg')).

- : substitute
     ([x] [idx: reduce x x]
        reduce/beta
        (Db x idx : reduce (Eb x) (Eb' x))
        (Da x idx : {y} reduce y y -> reduce (Ea x y) (Ea' x y)))
     (Darg: reduce Earg Earg')
     (reduce/beta Db' Da'
        : reduce (app (lam (Ea Earg)) (Eb Earg)) ((Ea' Earg') (Eb' Earg')))
     <- ({y} {idy: reduce y y}
           ({z}{z'}{red_z: reduce z z'} substitute ([_] [_] idy) red_z idy)
           -> substitute ([x] [idx: reduce x x] Da x idx y idy) Darg 
              (Da' y idy : reduce (Ea Earg y) (Ea' Earg' y)))
     <- substitute Db Darg (Db': reduce (Eb Earg) (Eb' Earg')).

%worlds (exp_subst) (substitute _ _ _).
%total D (substitute D _ _).