Ralph Loader's proof of standardization

Executable Specification

[View sred.sig] [View sred.mod]
%% Ralph Loader's proof of standardization
%% See his Lecture Notes on Typed Lambda Calculus
%%
%% Abella proof by Andreas Abel (October 2009)

sig sred.

kind    tm                          type.

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

type    tm                          tm -> o.
type    beta, betas, wh, sred       tm -> tm -> o.

%% Ralph Loader's proof of standardization
%%   (Notes on Simply Typed Lambda Calculus, ECS-LFCS-98-381)
%% an adaption of Hongwei Xi's arithmetical proof
%%   (Upper bounds for standardizations and an application, JSL 1999)
%% to Gordon Plotkin's inductive formulation of standard reduction.
%%   (Call-by-name, Call-by-value and the Lambda-Calculus, TCS 1975)
%%
%% Abella proof by Andreas Abel (October 2009)

module sred.

% pure lambda terms
tm (app M N) :- tm M, tm N.
tm (abs R) :- pi x\ tm x => tm (R x).

% ordinary one-step beta reduction
beta (app M N) (app M' N) :- beta M M'.
beta (app M N) (app M N') :- beta N N'.
beta (abs S1) (abs S2) :- pi x\ beta (S1 x) (S2 x).
beta (app (abs R) M) (R M).

% beta sequences as snoc lists
betas M M.
betas M N :- betas M P, beta P N.

% one-step weak head reduction
wh (app (abs R) M) (R M).
wh (app M N) (app M' N) :- wh M M'.

% Plotkin's standard reduction
sred M1 M3 :- wh M1 M2, sred M2 M3.
sred (app M1 N1) (app M2 N2) :- sred M1 M2, sred N1 N2.
sred (abs R1) (abs R2) :- pi x\ sred x x => sred (R1 x) (R2 x).

Reasoning

[View sred.thm]

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

%%   (Notes on Simply Typed Lambda Calculus, ECS-LFCS-98-381)
%% an adaption of Hongwei Xi's arithmetical proof
%%   (Upper bounds for standardizations and an application, JSL 1999)
%% to Gordon Plotkin's inductive formulation of standard reduction.
%%   (Call-by-name, Call-by-value and the Lambda-Calculus, TCS 1975)
%%
%% Abella proof by Andreas Abel (October 2009)

Specification "sred".

%% Technical lemma about fresh variables.
Theorem member_prune : forall E L, nabla (x:tm),
  member (E x) L -> exists F, E = y\F.

%% Matching contexts of term variables x and x -->s x.
Define ctx : olist -> olist -> prop by
  ctx nil nil ;
  nabla x, ctx (tm x :: C) (sred x x :: D) := ctx C D.

Theorem ctx_member1 : forall C D H,
  ctx C D -> member H C -> exists X, H = tm X /\ member (sred X X) D.

Theorem ctx_member2 : forall C D H,
  ctx C D -> member H D -> exists X, H = sred X X /\ member (tm X) C.

%% Technical lemma: weak head reduction is independent of context.
Theorem wh_ctx : forall C D T T',
  ctx C D -> {D |- wh T T'} -> {wh T T'}.

%% Standard reduction is reflexive.
Theorem srefl : forall C D T,
  ctx C D -> {C |- tm T} -> {D |- sred T T}.

%% Standard reduction is closed under substitution.
Theorem ssubst : forall C D T T' S S', nabla x, ctx C D ->
  {D, sred x x |- sred (T x) (T' x)} -> {D |- sred S S'} ->
  {D |- sred (T S) (T' S')}.

%% Variables do not beta reduce.
Theorem name_not_beta : forall T, nabla x, {beta x T} -> false.

Theorem var_not_beta : forall C D T T', ctx C D ->
  member (tm T) C -> {beta T T'} -> false.

%% Variables are not abstractions.
Theorem var_not_abs : forall C D R, ctx C D ->
  member (tm (abs R)) C -> false.

%% Applying a sred which ends in a lambda, removing the resulting redex.
Theorem sred_beta : forall C D M N N' R, ctx C D ->
  {D |- sred M (abs R)} -> {D |- sred N N'} -> {D |- sred (app M N) (R N')}.

%% Main Lemma:
%% Standard reduction is closed under appending a beta step.
Theorem sappend : forall C D T T' T'', ctx C D ->
  {D |- sred T T'} -> {beta T' T''} -> {D |- sred T T''}.
induction on 2. intros. case H2. % weak head step case apply IH to H1 H5 H3. search. % application case case H3. % cases on beta step. % subcase reduction in function part apply IH to H1 H4 H6. search. % subcase reduction in argument part apply IH to H1 H5 H6. search. % subcase beta-contraction apply sred_beta to H1 H4 H5. search. % abstraction case case H3. apply IH to _ H4 H5. search. % variable case apply ctx_member2 to H1 H5. case H4. apply var_not_beta to H1 H6 H3.
%% QED ! %% Theorem: Each beta reduction sequence can be standardized. Theorem standardization: forall T T', {tm T} -> {betas T T'} -> {sred T T'}.