Lambda calculus and various results on typing and evaluation

Executable Specification

[View eval.sig] [View eval.mod]
sig eval.

kind    tm, ty                 type.

type    app                    tm -> tm -> tm.
type    abs                    (tm -> tm) -> tm.

type    arrow                  ty -> ty -> ty.

type    of                     tm -> ty -> o.
type    eval, step, nstep      tm -> tm -> o.

module eval.

of (abs R) (arrow T U) :- pi x\ (of x T => of (R x) U).
of (app M N) T :- of M (arrow U T), of N U.

eval (abs R) (abs R).
eval (app M N) V :- eval M (abs R), eval (R N) V.

step (app (abs R) M) (R M).
step (app M N) (app M' N) :- step M M'.

nstep A A.
nstep A C :- step A B, nstep B C.

Reasoning

[View eval.thm]

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

%%
%% Even though we use higher-order abstract syntax here, we do not need
%% to define a meta-level context predicate because all contexts are
%% empty in the inductions.

Specification "eval".

%%
%% Determinancy
%%

Theorem eval_det :
  forall E V1 V2, {eval E V1} -> {eval E V2} -> V1 = V2.

Theorem step_det :
  forall E1 E2 E3, {step E1 E2} -> {step E1 E3} -> E2 = E3.

Theorem nstep_det :
  forall E R1 R2, {nstep E (abs R1)} -> {nstep E (abs R2)} -> R1 = R2.

%%
%% Equivalence of semantics
%%

Theorem nstep_lemma :
  forall M N R V, {nstep M (abs R)} -> {nstep (R N) V} -> {nstep (app M N) V}.

Theorem eval_nstep :
  forall E V, {eval E V} -> {nstep E V}.

Theorem step_eval_lemma :
  forall A B C, {step A B} -> {eval B C} -> {eval A C}.

Theorem nstep_eval :
  forall E R, {nstep E (abs R)} -> {eval E (abs R)}.


%%
%% Subject reduction
%%

Theorem sr_eval :
  forall E V T, {eval E V} -> {of E T} -> {of V T}.

Theorem sr_step :
  forall E1 E2 T, {step E1 E2} -> {of E1 T} -> {of E2 T}.

Theorem sr_nstep :
  forall E1 E2 T, {nstep E1 E2} -> {of E1 T} -> {of E2 T}.


%%
%% Misc
%%

% A cut property for typing judgments
Theorem type_subst : forall L E E' T T', nabla x,
  {L, of x T' |- of (E x) T} -> {L |- of E' T'} ->
    {L |- of (E E') T}.

% Self application cannot be simply-typed
Theorem of_self_app_absurd : forall T,
  {of (abs (x\ app x x)) T} -> false.

% The term (lambda x . x x) (lambda x . x x) does not evaluate to a value
Theorem no_eval : forall V,
  {eval (app (abs x\ app x x) (abs x\ app x x)) V} -> false.

% We can also define divergence coinductivly to prove that
% (lambda x . x x) (lambda x . x x) diverges

CoDefine diverge : tm -> prop by
  diverge (app M N) := diverge M ;
  diverge (app M N) := exists R, {eval M (abs R)} /\ diverge (R N).

Theorem omega_diverge :
  diverge (app (abs x\ app x x) (abs x\ app x x)).

% More generally we can prove that evaluation and divergence are
% mutually exclusive
Theorem eval_diverge_absurd : forall M V,
  {eval M V} -> diverge M -> false.