Tait's logical relations argument for weak normalization of STLC

Executable Specification

[View stlc-weak-norm.sig] [View stlc-weak-norm.mod]
sig stlc-weak-norm.

kind    tm, ty         type.

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

type    top            ty.
type    arrow          ty -> ty -> ty.

type    value          tm -> o.
type    of             tm -> ty -> o.
type    step, steps    tm -> tm -> o.

module stlc-weak-norm.

value (abs A R).

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

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

steps M M.
steps M N :- step M P, steps P N.

Reasoning

[View stlc-weak-norm.thm]

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

%%
%% This is based on the presentation in Types and Programming
%% Languages by Pierce.

Specification "stlc-weak-norm".
Close tm, ty.

%% Conventions:
%% Types: A, B, C
%% Terms: M, N, P, R
%% Values (Terms): V
%% Contexts: L

Define halts : tm -> prop by
  halts M := exists V, {steps M V} /\ {value V}.

%% Reduce is the logical relation used to prove normalization.
%%
%% This definition uses itself recursively in a negative context (the
%% left side of an implication). In order to guarantee consistency of
%% the system we must ensure this definition is stratified. Note the
%% second argument to reduce is strictly smaller in the (negative)
%% recursive occurrence, thus the definition is indeed stratified.

Define reduce : tm -> ty -> prop by
  reduce M top := {of M top} /\ halts M ;
  reduce M (arrow A B) := {of M (arrow A B)} /\
                          halts M /\
                          (forall N, reduce N A -> reduce (app M N) B).

Theorem reduce_halts : forall A M, reduce M A -> halts M.

Theorem reduce_of : forall A M, reduce M A -> {of M A}.


%% Properties of evaluation

Theorem absurd_step_value : forall V M,
  {step V M} -> {value V} -> false.

Theorem step_det : forall M N P,
  {step M N} -> {step M P} -> N = P.

Theorem step_follows_steps : forall M N V,
  {step M N} -> {steps M V} -> {value V} -> {steps N V}.

% steps is defined by left recursion on step, so this lemma tells us
% that it acts right recursively as well
Theorem steps_right : forall M N R,
  {steps M N} -> {step N R} -> {steps M R}.

Theorem steps_app_value : forall M N R,
  {value M} -> {steps N R} -> {steps (app M N) (app M R)}.

Theorem halt_step_forward : forall M N,
  halts M -> {step M N} -> halts N.

Theorem halt_step_backward : forall M N,
  halts N -> {step M N} -> halts M.

Theorem of_step_forward : forall M N A,
  {of M A} -> {step M N} -> {of N A}.

Theorem reduce_step_forward : forall M N A,
  reduce M A -> {step M N} -> reduce N A.

Theorem reduce_steps_forward : forall M N A,
  reduce M A -> {steps M N} -> reduce N A.

Theorem reduce_step_backward : forall M N A,
  reduce N A -> {step M N} -> {of M A} -> reduce M A.

Theorem reduce_steps_backward : forall M N A,
  reduce N A -> {steps M N} -> {of M A} -> reduce M A.


%% Properties about nominal constants, e.g. where they can and cannot occur.
%% Also properties about the contexts of judgments.

Define ctx : olist -> prop by
  ctx nil ;
  nabla x, ctx (of x A :: L) := ctx L.

% A term is closed if it can be typed in the empty context
Define closed : tm -> prop by
  closed M := exists A, {of M A}.

Define name : tm -> prop by
  nabla x, name x.

Theorem ctx_member :
  forall L E,
  ctx L -> member E L ->
  exists X A, E = of X A /\ name X.

Theorem member_prune : forall L E, nabla (x:tm),
  member (E x) L -> exists F, E = y\F.

% A term cannot contain a nominal variable which does not appear in
% its typing context L.
Theorem prune_of : forall L R A, nabla (x:tm),
  ctx L -> {L |- of (R x) A} -> exists M, R = y\M.

% Closed terms cannot contain any nominal constants
Theorem prune_closed : forall R, nabla (x:tm),
  closed (R x) -> exists M, R = y\M.

Theorem reduce_closed : forall M A, reduce M A -> closed M.

Theorem prune_reduce : forall R A, nabla (x:tm),
  reduce (R x) A -> exists M, R = y\M.


%% Now we need to state the generalize theorem. This will require reasoning
%% about all possible closed instantiations of an open term.

% Suppose that {L |- of M A} is true. Then M is an open term with nominal
% constants that are listed in L. The judgment "subst L M N" holds for all
% instantiations N of the nominal constants in M with values that satisfy
% the reduce relation for their respective types. The key to defining this
% judgment is the use of nabla in the head of a definition which extracts
% a nominal constant from L and M. The definition of subst then substitutes
% for this nominal constant and continues processing the list L.
Define subst : olist -> tm -> tm -> prop by
  subst nil M M ;
  nabla x, subst (of x A :: L) (R x) M :=
    exists V, reduce V A /\ {value V} /\ subst L (R V) M.

% Subst on a closed term has no effect
Theorem closed_subst : forall L M N,
  closed M -> subst L M N -> M = N.

Theorem subst_var : forall L M N A,
  ctx L -> member (of M A) L -> subst L M N -> reduce N A.

Theorem subst_app : forall L M N R,
  ctx L -> subst L (app M N) R ->
    exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR.

Theorem subst_abs : forall L M R A,
  ctx L -> subst L (abs A M) R ->
      exists MR, R = abs A MR /\
        (forall V, reduce V A -> {value V} ->
                     nabla x, subst (of x A :: L) (M x) (MR V)).

Theorem subst_preserves_ty : forall L M N A,
  ctx L -> subst L M N -> {L |- of M A} -> {of N A}.

Theorem weak_norm_ext : forall L M R A,
  ctx L -> {L |- of M A} -> subst L M R -> reduce R A.

Theorem weak_norm : forall M A, {of M A} -> halts M.