Translation between higher-order and debruijn lambda terms

Executable Specification

[View debruijn.sig] [View debruijn.mod]
sig debruijn.

kind      nat         type.
type      z           nat.
type      s           nat -> nat.
type      add         nat -> nat -> nat -> o.

kind      hterm       type.
type      app         hterm -> hterm -> hterm.
type      lam         (hterm -> hterm) -> hterm.

kind      dterm       type.
type      dapp        dterm -> dterm -> dterm.
type      dlam        dterm -> dterm.
type      dvar        nat -> dterm.

type      ho2db       hterm -> nat -> dterm -> o.
type      depth       hterm -> nat -> o.

module debruijn.

add z C C.
add (s A) B (s C) :- add A B C.

% H here is the height (depth) of lambda abstractions
ho2db (app M N) H (dapp DM DN) :- ho2db M H DM, ho2db N H DN.
ho2db (lam R) H (dlam DR) :- pi x\ depth x H => ho2db (R x) (s H) DR.
ho2db X H (dvar DX) :- depth X HX, add HX DX H.

Reasoning

[View debruijn.thm]

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

%%
%% A similar result is shown for Twelf at
%%   http://twelf.plparty.org/wiki/Concrete_representation
%% They seem to need many contorsions which are unrelated to the
%% actual task of the translation. They also define both a forward
%% and backward translation, whereas we use a single translation and
%% prove it deterministic in both directions. Their key difficulty
%% is that they cannot use hypothetical assumptions like our (depth X N)
%% since regular worlds are not powerful enough to specify the
%% form of contexts which are created (e.g. they cannot show the
%% natural number N must be unique).

Specification "debruijn".

%% General property of member

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


%% Properties of addition

Define nat : nat -> prop by
  nat z ;
  nat (s X) := nat X.

Define le : nat -> nat -> prop by
  le X X ;
  le X (s Y) := le X Y.

Theorem le_dec : forall X Y,
  le (s X) Y -> le X Y.

Theorem le_absurd : forall X,
  nat X -> le (s X) X -> false.

Theorem add_le : forall A B C,
  {add A B C} -> le B C.

Theorem add_absurd : forall A C,
  nat C -> {add A (s C) C} -> false.

Theorem add_zero : forall A C,
  nat C -> {add A C C} -> A = z.

% add is deterministic in its first argument
Theorem add_det1 : forall A1 A2 B C,
  nat C -> {add A1 B C} -> {add A2 B C} -> A1 = A2.

% add is deterministic in its second argument
Theorem add_det2 : forall A B1 B2 C,
  {add A B1 C} -> {add A B2 C} -> B1 = B2.


%% Theorems specific to our translation

Define ctx : olist -> nat -> prop by
  ctx nil z ;
  nabla x, ctx (depth x H :: L) (s H) := ctx L H.

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

Theorem ctx_nat : forall L H,
  ctx L H -> nat H.

Theorem ctx_world : forall E L H,
  ctx L H -> member E L -> exists X HX, E = depth X HX /\ name X.

Theorem depth_name : forall L H X HX,
  ctx L H -> {L |- depth X HX} -> name X.

Theorem member_depth_det2 : forall L H X H1 H2,
  ctx L H -> member (depth X H1) L -> member (depth X H2) L -> H1 = H2.

Theorem depth_det2 : forall L H X H1 H2,
  ctx L H -> {L |- depth X H1} -> {L |- depth X H2} -> H1 = H2.

Theorem ctx_member_absurd : forall X H1 H2 L,
  ctx L H1 -> member (depth X H2) L -> le H1 H2 -> false.

Theorem member_depth_det1 : forall L H X1 X2 HX,
  ctx L H -> member (depth X1 HX) L -> member (depth X2 HX) L -> X1 = X2.

Theorem depth_det1 : forall L H X1 X2 HX,
  ctx L H -> {L |- depth X1 HX} -> {L |- depth X2 HX} -> X1 = X2.

Theorem add_ignores_ctx : forall L H A B C,
  ctx L H -> {L |- add A B C} -> {add A B C}.

%% ho2db is deterministic in its third argument
%% ie, higher-order --> debruijn is unique
Theorem ho2db_det3 : forall L M D1 D2 H,
  ctx L H -> {L |- ho2db M H D1} -> {L |- ho2db M H D2} -> D1 = D2.

Theorem ho2db_det3_simple : forall M D1 D2,
  {ho2db M z D1} -> {ho2db M z D2} -> D1 = D2.


%% ho2db is deterministic in its first argument
%% ie, debruijn --> higher-order is unique
%% proof is mostly the same as ho2db_det3 except with fewer cases
Theorem ho2db_det1 : forall L M1 M2 D H,
  ctx L H -> {L |- ho2db M1 H D} -> {L |- ho2db M2 H D} -> M1 = M2.

Theorem ho2db_det1_simple : forall M1 M2 D,
  {ho2db M1 z D} -> {ho2db M2 z D} -> M1 = M2.