Hereditary substitution for the STLC (part 2)

From The Twelf Project
Jump to: navigation, search

This is part 2 of the case study Hereditary substitution for the STLC.


External language: syntax and judgements

Syntax

The external language syntax is a copy of the internal language, where we additionally include canonincal terms M into atomic terms R. To preserve the modes of the typing judgements, these canonical terms are annotated with the type that they should be checked against.

el_rtm : type.
el_mtm : type.

el_app : el_rtm -> el_mtm -> el_rtm.
el_c : el_rtm.
el_fst : el_rtm -> el_rtm.
el_snd : el_rtm -> el_rtm.
el_annot : el_mtm -> tp -> el_rtm.

el_asm : el_rtm -> el_mtm.
el_lam : (el_rtm -> el_mtm) -> el_mtm.
el_pair : el_mtm -> el_mtm -> el_mtm.

%block el_rtm_block : block {x : el_rtm}.

Modulo the placement of type annotations, this grammar lets you write any term that you can write without the syntactic stratification.

Typing judgements

The typing judgements for the external language extand the judgements for canonical forms with a rule synth_annot for synthesizing the type of an annotated term. Additionally, the rules do not force terms to be η-long.

synth : el_rtm -> tp -> type.
%mode synth +X1 -X2.
check : el_mtm -> tp -> type.
%mode check +X1 +X2.

% synthesize

synth_c : synth el_c b.

synth_app : synth (el_app R1 M2) A
             <- synth R1 (arrow A2 A)
             <- check M2 A2.

synth_fst : synth (el_fst R) A1
             <- synth R (prod A1 A2).

synth_snd : synth (el_snd R) A2
             <- synth R (prod A1 A2).

%% admit non-canonical forms with an annotation
synth_annot : synth (el_annot M A) A
               <- check M A.

%% check

%% in the EL anything that synths also checks, no matter the type
check_asm : check (el_asm R) A
             <- synth R A.

check_lam : check (el_lam M) (arrow A2 A)
             <- ({x : el_rtm} (synth x A2) -> check (M x) A).

check_pair : check (el_pair M1 M2) (prod A1 A2)
              <- check M1 A1
              <- check M2 A2.

%block synth_block : some {A:tp} block {x : el_rtm} {dx : synth x A}.
%worlds (synth_block) (synth _ _) (check _ _).

It is possible to show that any well-typed term in a standard presentation of the λ-calculus can be translated into a term in this syntax that is well-typed by these rules. However, we have not formulated this step here, choosing instead to take these rules as the definition of the external language.

Elaboration

We now define elaboration. We define three mutually recursive elaboration judgements, one for checked terms, and two for synthesizing terms. The two judgements for synthesizing terms differ in whether the elaboration of the synthesizing term is an atomic term or a canonical term.

elab_m : el_mtm -> mtm -> tp -> type.
%mode elab_m +X1 -X2 +X3.

elab_r_to_r : el_rtm -> rtm -> tp -> type.
%mode elab_r_to_r +X1 -X2 -X3.

elab_r_to_m : el_rtm -> mtm -> tp -> type.
%mode elab_r_to_m +X1 -X2 -X3.

% M

elab_m_asm_r2r : elab_m (el_asm ER) M A
                  <- elab_r_to_r ER R A
                  <- expand A R M.

elab_m_asm_r2m : elab_m (el_asm ER) M A
                  <- elab_r_to_m ER M A.

elab_m_lam : elab_m (el_lam EM) (lam M) (arrow A2 A)
              <- ({el_x : el_rtm} {x : rtm} 
                    (elab_r_to_r el_x x A2) 
                    -> elab_m (EM el_x) (M x) A).

elab_m_pair : elab_m (el_pair EM1 EM2) (pair M1 M2) (prod A1 A2)
               <- elab_m EM1 M1 A1
               <- elab_m EM2 M2 A2.

% R to R

elab_r_to_r_c : elab_r_to_r el_c c b.

elab_r_to_r_app : elab_r_to_r (el_app ER1 EM2) (app R1 M2) A
                   <- elab_r_to_r ER1 R1 (arrow A2 A)
                   <- elab_m EM2 M2 A2.

elab_r_to_r_fst : elab_r_to_r (el_fst ER) (fst R) A1
                   <- elab_r_to_r ER R (prod A1 A2).

elab_r_to_r_snd : elab_r_to_r (el_snd ER) (snd R) A2
                   <- elab_r_to_r ER R (prod A1 A2).

% R root

elab_r_to_m_annot : elab_r_to_m (el_annot EM A) M A
                     <- elab_m EM M A.

elab_r_to_m_app : elab_r_to_m (el_app ER1 EM2) M' A
                   <- elab_r_to_m ER1 (lam M) (arrow A2 A)
                   <- elab_m EM2 M2 A2
                   <- hsubst_m M2 A2 M M'.

elab_r_to_m_fst : elab_r_to_m (el_fst ER) M1 A1
                   <- elab_r_to_m ER (pair M1 M2) (prod A1 A2).

elab_r_to_m_snd : elab_r_to_m (el_snd ER) M2 A2
                   <- elab_r_to_m ER (pair M1 M2) (prod A1 A2).

%block elab_block : some {A:tp}
                     block 
                     {el_x : el_rtm} 
                     {x : rtm} 
                     {dex : elab_r_to_r el_x x A}.

The inductive structure of the elaboration judgements is similar to the structure of hereditary substitution. Elaboration uses hereditary substitution in the key rule elab_r_to_m_app to compute the canonical result of a function application. Elaboration also uses expansion to expand atomic terms into canonical ones.

External Language: Metatheory

Static Correctness of Elaboration

First, we prove that the elaboration of a well-typed term is well-typed.

elab_m_reg : elab_m EM M A
	      -> check EM A
	      -> canon M A
	      -> type.
%mode elab_m_reg +X1 -X2 -X3.

elab_r2r_reg : elab_r_to_r ER R A
 		-> synth ER A
 		-> atom R A
 		-> type.
%mode elab_r2r_reg +X1 -X2 -X3.

elab_r2m_reg : elab_r_to_m ER M A
		-> synth ER A
		-> canon M A
		-> type.
%mode elab_r2m_reg +X1 -X2 -X3.

%% M to M

- : elab_m_reg
     (elab_m_asm_r2r Dex Del)
     (check_asm DsynER)
     DcanM
     <- elab_r2r_reg Del DsynER DaR
     <- expand_exists _ DaR Dex-2 DcanM-2
     <- expand_unique Dex-2 Dex Did
     <- canon_respects_id Did id/tp_refl DcanM-2 DcanM.

- : elab_m_reg
     (elab_m_asm_r2m Del)
     (check_asm DsynER)
     DcanM
     <- elab_r2m_reg Del DsynER DcanM.

- : elab_m_reg
     (elab_m_lam Del)
     (check_lam Dcheck)
     (canon_lam Dcanon)
     <- ({el_x : el_rtm} 
	   {delx : synth el_x A}
	   {x : rtm}
	   {dx : atom x A}
	   {delabx : elab_r_to_r el_x x A}
	   {_ : elab_r2r_reg delabx delx dx}
	   elab_m_reg (Del el_x x delabx) (Dcheck el_x delx) (Dcanon x dx)).

- : elab_m_reg
     (elab_m_pair De2 De1)
     (check_pair Dcheck2 Dcheck1)
     (canon_pair Dcanon2 Dcanon1)
     <- elab_m_reg De2 Dcheck2 Dcanon2 
     <- elab_m_reg De1 Dcheck1 Dcanon1.

%% R to R

- : elab_r2r_reg
     elab_r_to_r_c 
     synth_c
     atom_c.

- : elab_r2r_reg
     (elab_r_to_r_app De2 De1)
     (synth_app Dcheck2 Dsynth1)
     (atom_app Dcanon2 Datom1)
     <- elab_m_reg De2 Dcheck2 Dcanon2 
     <- elab_r2r_reg De1 Dsynth1 Datom1.

- : elab_r2r_reg
     (elab_r_to_r_fst De1)
     (synth_fst Dsynth1)
     (atom_fst Datom1)
     <- elab_r2r_reg De1 Dsynth1 Datom1.

- : elab_r2r_reg
     (elab_r_to_r_snd De1)
     (synth_snd Dsynth1)
     (atom_snd Datom1)
     <- elab_r2r_reg De1 Dsynth1 Datom1.

%% R to M

- : elab_r2m_reg
     (elab_r_to_m_annot De)
     (synth_annot DcheckM)
     DcanonM
     <- elab_m_reg De DcheckM DcanonM.
     
- : elab_r2m_reg
     (elab_r_to_m_app DsubstM2 DeM2 DeR1)
     (synth_app DcheckM2 DsynthR1)
     DcanonM'
     <- elab_r2m_reg DeR1 DsynthR1 (canon_lam DcanonM)
     <- elab_m_reg DeM2 DcheckM2 DcanonM2
     <- hsubst_m_exists _ DcanonM DcanonM2 DsubstM2-2 DcanonM'-2
     <- hsubst_m_unique DsubstM2-2 DsubstM2 Did
     <- canon_respects_id Did id/tp_refl DcanonM'-2 DcanonM'.

- : elab_r2m_reg
     (elab_r_to_m_fst DeR)
     (synth_fst DsynthR)
     DcM1
     <- elab_r2m_reg DeR DsynthR (canon_pair DcM2 DcM1).

- : elab_r2m_reg
     (elab_r_to_m_snd DeR)
     (synth_snd DsynthR)
     DcM2
     <- elab_r2m_reg DeR DsynthR (canon_pair DcM2 DcM1).


%% because world subsumption doesn't do exchange,
%% you can't get this block to match both
%% atom_block/synth_block and elab_block.
%%
%% this order matches atom_block/synth_block but not elab_block.
%block elab_reg_block : some {A:tp}
                         block 
                         {el_x : el_rtm} 
                         {delx : synth el_x A}
                         {x : rtm}
                         {dx : atom x A}
                         {delabx : elab_r_to_r el_x x A}
                         {_ : elab_r2r_reg delabx delx dx}.


%worlds (elab_reg_block) 
(elab_m_reg _ _ _)
(elab_r2r_reg _ _ _)
(elab_r2m_reg _ _ _).

%total (D1 D2 D3)
(elab_m_reg D1 _ _)
(elab_r2r_reg D2 _ _)
(elab_r2m_reg D3 _ _).

The proof is a straightforward induction, using hsubst_m_exists and expand_exists. Because these two lemmas output a hereditary substitution or expansion, along with the typing derivation for the result of the operation, we use uniqueness here to show well-typedness of the outputs of the hereditary substitution and expansion derivations given by elaboration. In retrospect, we should have factored this reasoning into separate lemmas that are like hsubst_m_exists and expand_exists but take the the hereditary substitution or expansion as an input.

Existence of elaboration

We require one addtional respects lemma.

elab_r2m_respects_id :  id/mtm M M'
			-> id/tp A A'
			-> elab_r_to_m R M A
			-> elab_r_to_m R M' A'
			-> type.
%mode elab_r2m_respects_id +X1 +X2 +X3 -X4.

- : elab_r2m_respects_id _ _ D D.

%worlds (elab_block | elab_reg_block) (elab_r2m_respects_id _ _ _ _).  %% bar in other block
%total {} (elab_r2m_respects_id _ _ _ _).
%reduces D1 = D2 (elab_r2m_respects_id _ _ D2 D1).

The worlds of this lemma require a little explanation. elab_reg_block should equal elab_block for this type family. However, world subsumption does not notice this relationship because doing so would require permutation. Consequently, we prove the theorem for both blocks directly.

Next, we prove that all well-typed terms elaborate. Analogously to hereditary substitution, the theorem for synthesizing terms computes a sum of the two ways it could elaborate:

elab_r_exists_sum : el_rtm -> tp -> type.
elab_r_exists_sum_r2r : elab_r_exists_sum ER A
                         <- elab_r_to_r ER R A.
elab_r_exists_sum_r2m : elab_r_exists_sum ER A
                         <- elab_r_to_m ER M A.

We begin with some output factoring and canonical forms lemmas:

elab_m_exists_asm : elab_r_exists_sum ER A
		     -> elab_m (el_asm ER) M' A
		     -> type.
%mode elab_m_exists_asm +X1 -X2.

- : elab_m_exists_asm 
     (elab_r_exists_sum_r2m DeR)
     (elab_m_asm_r2m DeR).

- : elab_m_exists_asm 
     (elab_r_exists_sum_r2r DeR)
     (elab_m_asm_r2r Dex DeR)
     <- elab_r2r_reg DeR _ DaR
     <- expand_exists _ DaR Dex _.

%worlds (elab_reg_block) (elab_m_exists_asm _ _).
%total {} (elab_m_exists_asm _ _).


canon_prod_is_pair : canon M (prod A1 A2)
		      -> id/mtm M (pair M1 M2)
		      -> type.
%mode canon_prod_is_pair +X1 -X2.

- : canon_prod_is_pair _ id/mtm_refl.

%worlds (elab_reg_block) (canon_prod_is_pair _ _).
%total {} (canon_prod_is_pair _ _).

elab_r_exists_fst : elab_r_exists_sum R (prod A1 A2)
		     -> elab_r_exists_sum (el_fst R) A1
		     -> type.
%mode elab_r_exists_fst +X1 -X2.

- : elab_r_exists_fst
     (elab_r_exists_sum_r2r DeR)
     (elab_r_exists_sum_r2r (elab_r_to_r_fst DeR)).

- : elab_r_exists_fst
     (elab_r_exists_sum_r2m DeR)
     (elab_r_exists_sum_r2m (elab_r_to_m_fst DeR-2))
     <- elab_r2m_reg DeR _ DcM
     <- canon_prod_is_pair DcM Did
     <- elab_r2m_respects_id Did id/tp_refl DeR DeR-2.
     
%worlds (elab_reg_block) (elab_r_exists_fst _ _).
%total {} (elab_r_exists_fst _ _).

elab_r_exists_snd : elab_r_exists_sum R (prod A1 A2)
		     -> elab_r_exists_sum (el_snd R) A2
		     -> type.
%mode elab_r_exists_snd +X1 -X2.

- : elab_r_exists_snd
     (elab_r_exists_sum_r2r DeR)
     (elab_r_exists_sum_r2r (elab_r_to_r_snd DeR)).

- : elab_r_exists_snd
     (elab_r_exists_sum_r2m DeR)
     (elab_r_exists_sum_r2m (elab_r_to_m_snd DeR-2))
     <- elab_r2m_reg DeR _ DcM
     <- canon_prod_is_pair DcM Did
     <- elab_r2m_respects_id Did id/tp_refl DeR DeR-2.
     
%worlds (elab_reg_block) (elab_r_exists_snd _ _).
%total {} (elab_r_exists_snd _ _).


canon_arrow_is_lam : canon M (arrow A2 A)
		      -> id/mtm M (lam M')
		      -> type.
%mode canon_arrow_is_lam +X1 -X2.

- : canon_arrow_is_lam _ id/mtm_refl.

%worlds (elab_reg_block) (canon_arrow_is_lam _ _).
%total {} (canon_arrow_is_lam _ _).

elab_r_exists_app : elab_r_exists_sum ER1 (arrow A2 A)
		     -> elab_m EM2 M2 A2
		     -> elab_r_exists_sum (el_app ER1 EM2) A
		     -> type.
%mode elab_r_exists_app +X1 +X2 -X3.

- : elab_r_exists_app
     (elab_r_exists_sum_r2r DeR1)
     DeM2
     (elab_r_exists_sum_r2r (elab_r_to_r_app DeM2 DeR1)).

- : elab_r_exists_app
     (elab_r_exists_sum_r2m DeR1)
     DeM2
     (elab_r_exists_sum_r2m (elab_r_to_m_app Ds DeM2 DeR1-2))
     <- elab_r2m_reg DeR1 _ DcM1
     <- elab_m_reg DeM2 _ DcM2
     <- canon_arrow_is_lam DcM1 Did
     <- canon_respects_id Did id/tp_refl DcM1 (canon_lam DcBody)
     <- elab_r2m_respects_id Did id/tp_refl DeR1 DeR1-2
     <- hsubst_m_exists _ DcBody DcM2 Ds _.

%worlds (elab_reg_block) (elab_r_exists_app _ _ _).
%total {} (elab_r_exists_app _ _ _).

Finally, we prove the main results:

elab_m_exists : check EM A
		 -> elab_m EM M A
		 -> type.
%mode elab_m_exists +X1 -X2.

elab_r_exists : synth ER A
 		 -> elab_r_exists_sum ER A
 		 -> type.
%mode elab_r_exists +X1 -X2.

%% M

- : elab_m_exists
     (check_asm Dsyn)
     DeRes
     <- elab_r_exists Dsyn Dsum
     <- elab_m_exists_asm Dsum DeRes.

- : elab_m_exists 
     (check_lam DcM)
     (elab_m_lam DelabM)
     <- ({el_x : el_rtm} 
	   {delx : synth el_x A}
	   {x : rtm}
	   {dx : atom x A}
	   {delabx : elab_r_to_r el_x x A}
	   {_ : elab_r2r_reg delabx delx dx}
	   {_ : elab_r_exists delx (elab_r_exists_sum_r2r delabx)}
	   elab_m_exists (DcM el_x delx) (DelabM el_x x delabx)).
	
- : elab_m_exists 
     (check_pair Dc2 Dc1)
     (elab_m_pair De2 De1)
     <- elab_m_exists Dc1 De1 
     <- elab_m_exists Dc2 De2.

%% R 

- : elab_r_exists
     synth_c 
     (elab_r_exists_sum_r2r elab_r_to_r_c).

- : elab_r_exists 
     (synth_app DchM DsynR)
     DsumApp
     <- elab_r_exists DsynR DsumR
     <- elab_m_exists DchM DeM
     <- elab_r_exists_app DsumR DeM DsumApp.


- : elab_r_exists
     (synth_fst Dsyn)
     Dsum'
     <- elab_r_exists Dsyn Dsum
     <- elab_r_exists_fst Dsum Dsum'.

- : elab_r_exists
     (synth_snd Dsyn)
     Dsum'
     <- elab_r_exists Dsyn Dsum
     <- elab_r_exists_snd Dsum Dsum'.

- : elab_r_exists
     (synth_annot DcM)
     (elab_r_exists_sum_r2m (elab_r_to_m_annot DeM))
     <- elab_m_exists DcM DeM.
     
% maintains all the invariants from elab_reg_block because the above lemmas use call regularity
%block elab_exists_block : some {A:tp}
                            block 
                            {el_x : el_rtm} 
                            {delx : synth el_x A}
                            {x : rtm}
                            {dx : atom x A}
                            {delabx : elab_r_to_r el_x x A}
                            {_ : elab_r2r_reg delabx delx dx}
                            {_ : elab_r_exists delx (elab_r_exists_sum_r2r delabx)}.
%worlds (elab_exists_block) 
(elab_m_exists _ _)
(elab_r_exists _ _).

%total (D1 D2) 
(elab_m_exists D1 _)
(elab_r_exists D2 _).

All Twelf code for this tutorial. See Twelf's output.


Read more Twelf case studies and other Twelf documentation.