Disjoint partitioning of lambda terms into normal and non-normal form

Executable Specification

[View normal.sig] [View normal.mod]
sig normal.

kind      tm                     type.

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

type      term                   tm -> o.
type      non_normal             tm -> o.
type      neutral, normal        tm -> o.

% From Dale Miller:
% It is easy to write code that determines if a given lambda-term (type
% tm) is in beta-normal form (using the fact that a term in normal form
% is of the form (lambda x1 ... lambda xn. h t1 ... tn) where t1, ...,
% tn are in beta-normal form and h is a variable (one of the x1, ...,
% xn, or a variable introduced before).  It is also possible to know
% that a term is not in beta-normal form since it contains a beta-redex
% (in abstract syntax, it would contain a subterm of the form (app (abs
% R) M).  An interesting theorem to try is the one that says
%   forall T : tm.  (normal T) or (non-normal T).
% This one should have a simple proof if the right induction invariant
% can be stated.

module normal.

term (app M N) :- term M, term N.
term (abs R) :- pi x\ term x => term (R x).

non_normal (app (abs R) M).
non_normal (app M N) :- non_normal M.
non_normal (app M N) :- non_normal N.
non_normal (abs R) :- pi x\ non_normal (R x).

normal (abs R) :- pi x\ neutral x => normal (R x).
normal M :- neutral M.
neutral (app M N) :- neutral M, normal N.


[View normal.thm]

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

%% The ctxs predicate encodes the relationship between the context
%% of the judgements (term T) and (normal T).

Specification "normal".

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

Define ctxs : olist -> olist -> prop by
  ctxs nil nil ;
  nabla x, ctxs (term x :: L) (neutral x :: K) := ctxs L K.

%% Lemmas about contexts

Theorem ctxs_member_term : forall L K E,
  ctxs L K -> member E L ->
  exists X, E = term X /\ member (neutral X) K /\ name X.

Theorem ctxs_var : forall E L K,
  ctxs L K -> member E K -> 
  exists X, E = neutral X /\ name X.

%% Partitioning is total

Theorem total_ext : forall T L K,
  ctxs L K -> {L |- term T} -> {K |- normal T} \/ {non_normal T}.

Theorem total : forall T,
  {term T} -> {normal T} \/ {non_normal T}.

%% Partitioning is disjoint

Theorem neutral_abs_absurd : forall L K R,
  ctxs L K -> {K |- neutral (abs R)} -> false.

Theorem disjoint_ext : forall L K T,
  ctxs L K -> {K |- normal T} -> {non_normal T} -> false.

Theorem disjoint : forall T,
  {normal T} -> {non_normal T} -> false.