Properties of PCF

Executable Specification

[View pcf.sig] [View pcf.mod]
sig pcf.

kind    tm, ty                   type.

type    zero, tt, ff             tm.
type    succ, pred, is_zero      tm -> tm.
type    if                       tm -> tm -> tm -> tm.
type    abs, rec                 ty -> (tm -> tm) -> tm.
type    app                      tm -> tm -> tm.

type    num, bool                ty.
type    arr                      ty -> ty -> ty.

type    eval                     tm -> tm -> o.
type    of                       tm -> ty -> o.

module pcf.

eval zero zero.
eval tt tt.
eval ff ff.
eval (succ M) (succ V) :- eval M V.
eval (pred M) zero :- eval M zero.
eval (pred M) V :- eval M (succ V).
eval (is_zero M) tt :- eval M zero.
eval (is_zero M) ff :- eval M (succ V).
eval (if M N1 N2) V :- eval M tt, eval N1 V.
eval (if M N1 N2) V :- eval M ff, eval N2 V.
eval (abs T R) (abs T R).
eval (app M N) V :- eval M (abs T R), eval (R N) V.
eval (rec T R) V :- eval (R (rec T R)) V.

of zero num.
of tt bool.
of ff bool.
of (succ M) num :- of M num.
of (pred M) num :- of M num.
of (is_zero M) bool :- of M num.
of (if M N1 N2) T :- of M bool, of N1 T, of N2 T.
of (abs T R) (arr T U) :- pi n\ (of n T => of (R n) U).
of (app M N) T :- of M (arr U T), of N U.
of (rec T R) T :- pi n\ (of n T => of (R n) T).

Reasoning

[View pcf.thm]

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

Specification "pcf".

%% Subject reduction

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


%% Type uniqueness

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

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

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

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

Theorem ctx_uniq : forall L E T1 T2,
  ctx L -> member (of E T1) L -> member (of E T2) L -> T1 = T2.

% Some basic automation with regards to ctx_member would be great here

Theorem type_uniq : forall L E T1 T2,
  ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2.

Query
  Add = (rec (arr num (arr num num))
             (add\ abs num x\ abs num y\
                     if (is_zero x) y (succ (app (app add (pred x)) y))))
    /\
  Two = succ (succ zero) /\
  Three = succ (succ (succ zero)) /\
  {eval (app (app Add Two) Three) V}.