Substitution lemma
Type-preserving substitution is the property of a hypothetical judgment that if Γ, x : A ⊦ M(x) : B and Γ ⊦ N : A, then Γ, ⊦ M(N) : B. In other words, if we have a well-typed term M(x) that depends on a hypothesis x of type A, and we have a well-typed term N : A, then we can substitute N for the variable x within M to produce a well-typed term that does not depend on x.
Depending on how the type system of an object language is encoded, there are a number of different techniques for proving a substitution lemma for the language.
Contents
Substitution via application in LF
When an object language is encoded using higher-order representations of hypothetical judgements, substitution comes for free: object-language variables and typing assumptions are represented by LF lambdas, so substitution follows from LF application.
Consider the following encoding of a simply typed λ-calculus:
%% Syntax
tp : type.
tp/unit : tp.
tp/arrow : tp -> tp -> tp.
exp : type.
exp/unit : exp.
exp/lam : tp -> (exp -> exp) -> exp.
exp/app : exp -> exp -> exp.
%% Typing judgement
of : exp -> tp -> type.
of/unit : of exp/unit tp/unit.
of/lam : of (exp/lam T E) (tp/arrow T T')
<- ({x:exp} of x T
-> of (E x) T').
of/app : of (exp/app E1 E2) T'
<- of E2 T
<- of E1 (tp/arrow T T').
We can give a direct proof of substitution:
subst : of E1 T
-> ({x:exp}{dx:of x T} of (E2 x) T')
-> of (E2 E1) T'
-> type.
%mode subst +D1 +D2 -D3.
- : subst D1 D2 (D2 E1 D1).
%block of-block : some {T:tp} block {x:exp}{dx:of x T}.
%worlds (of-block) (subst _ _ _).
%total {} (subst _ _ _).See Twelf's output
The typing derivation for the substitution is created by applying the LF function D2, which represents the hypothetical typing derivation, to the LF term D1, which represents the typing derivation for the substituted term.
Although we proved substitution as a metatheorem subst here, in practice it is unnecessary to state substitution as a lemma. The substitution can be performed via application whenever it is necessary.
Substitution lemmas with a "var" rule
In the above language, there was no explicit typing rule in the system for typing variables. Instead, typing derivations for variables were put directly into the LF context. However, for some languages it is necessary to use separate judgments for assumptions about variables and for typing derivations. This is common for languages with references and stores which require a lemma that shows it is admissible to weaken typing derivations with respect to the store.
In the following example, the assm judgment is used in conjunction with the oftp/var rule to give of typing derivations for variables. A derivation of {x:exp} assm x T -> of (E2 x) T' and a derivation of of E1 T cannot be used to show of (E2 E1) T' via application in LF. This is because a hypothetical judgment expecting an assm derivation cannot be applied to an of derivation. That is, the LF representation does not directly tell us that substitution holds, as the assumption is of a different type.
However, in this case, the desired substitution principle can be proved via an induction over the structure of the hypothetical judgment. The key to making the following proof work is the fact that exchange is admissible for this language via its encoding in LF. In general, exchange is admissible whenever assumptions about variables cannot depend on assumptions earlier in the context.
Here is an encoding that uses a different judgement for assumptions:
%% Syntax
tp : type.
tp/unit : tp.
tp/arrow : tp -> tp -> tp.
exp : type.
exp/unit : exp.
exp/lam : tp -> (exp -> exp) -> exp.
exp/app : exp -> exp -> exp.
%% Typing judgements
assm : exp -> tp -> type.
of : exp -> tp -> type.
of/var : of E T
<- assm E T.
of/unit : of exp/unit tp/unit.
of/lam : of (exp/lam T E) (tp/arrow T T')
<- ({x:exp} assm x T
-> of (E x) T').
of/app : of (exp/app E1 E2) T'
<- of E2 T
<- of E1 (tp/arrow T T').
Now, we prove the substitution theorem:
subst : of E1 T
-> ({x:exp}{dx:assm x T} of (E2 x) T')
-> of (E2 E1) T'
-> type.
%mode subst +D1 +D2 -D3.
% case for substituting out the assumption
- : subst D1 ([x][dx] of/var dx) D1.
% catch-all case for of/unit or instances of of/var for a different assumption
- : subst D1 ([x][dx] D2) D2.
The following case is the key for the proof of this metatheorem. It works because the language admits the property of exchange.
In the following case, D2 has the type
{x:exp}{dx:of x T}{y:exp}{dy:of y T'} of (E' x y) T''
The principle of exchange can be applied to produce a derivation of
{y:exp}{dy:of y T'}{x:exp}{dx:of x T} of (E' x y) T''
On the inductive call to subst, the assumptions
{y:exp}{dy:of y T'}
are pushed into the LF context, so that a derivation of type
{x:exp}{dx:of x T} of (E' x y) T''
can be given as the second argument to the inductive call.
- : subst D1 ([x][dx] of/lam ([y][dy] D2 x dx y dy)) (of/lam D2')
<- ({y}{dy} subst D1 ([x][dx] D2 x dx y dy) (D2' y dy)).
- : subst D1 ([x][dx] of/app (D2 x dx) (D3 x dx)) (of/app D2' D3')
<- subst D1 D2 D2'
<- subst D1 D3 D3'.
%block assm-block : some {T:tp} block {x:exp}{dx:assm x T}.
%worlds (assm-block) (subst _ _ _).
%total (D1) (subst _ D1 _).See Twelf's output
Substitution lemmas with dependent types [Advanced topic]
The preceding technique for showing substitution lemmas works fine for systems without dependent types. However, it would not work for a system with dependent types, because its typing assumptions could not admit exchange, in general. A recent discovery is that a similarly general technique is available for languages with dependent types and a var rule, despite the apparent absence of an exchange property. Of course, if the system has the same judgment for assumptions and typing derivations, then substitution can be performed via application in LF.
The following example studies a very simple singleton calculus with the dependent Π type for functions. The presence of dependent types means typing assumptions about expressions can depend on expression variables introduced in earlier assumptions.
Explicit contexts could be used to do substition in this case, but this technique is much simpler in practice.
tp : type.
exp : type.
tp/sing : exp -> tp.
tp/unit : tp.
tp/pi : tp -> (exp -> tp) -> tp.
exp/unit : exp.
exp/lam : tp -> (exp -> exp) -> exp.
exp/app : exp -> exp -> exp.
assm : exp -> tp -> type.
of : exp -> tp -> type.
of/var : of E T
<- assm E T.
of/unit : of exp/unit tp/unit.
of/lam : of (exp/lam T E) (tp/pi T T')
<- ({x:exp} assm x T
-> of (E x) (T' x)).
of/app : of (exp/app E1 E2) (T' E2)
<- of E2 T
<- of E1 (tp/pi T T').
of/sing : of E (tp/sing E)
<- of E tp/unit.
%block assm-block : some {T:tp} block {x:exp}{dx:assm x T}.
The following metatheorem is actually true, but the naive attempt at proving it will fail.
subst-wontwork : of E1 T
-> ({x:exp}{dx:assm x T} of (E2 x) (T' x))
-> of (E2 E1) (T' E1)
-> type.
%mode subst-wontwork +D1 +D2 -D3.
% case for substituting out the assumption
- : subst-wontwork D1 ([x][dx] of/var dx) D1.
% catch-all case for of/unit or instances of of/var for a different assumption
- : subst-wontwork D1 ([x][dx] D2) D2.
- : subst-wontwork D1 ([x][dx] of/app (D2 x dx) (D3 x dx)) (of/app D2' D3')
<- subst-wontwork D1 D2 D2'
<- subst-wontwork D1 D3 D3'.
- : subst-wontwork D1 ([x][dx] of/sing (D2 x dx)) (of/sing D2')
<- subst-wontwork D1 D2 D2'.
The proof fails because this case is not general enough to cover all lambdas. Specifically, this case only applies if the type assigned to the variable y does not depend on the variable x.
- : subst-wontwork D1 ([x][dx] of/lam ([y][dy:assm y T'] D2 x dx y dy)) (of/lam D2')
<- ({y}{dy} subst-wontwork D1 ([x][dx] D2 x dx y dy) (D2' y dy)).
%worlds (assm-block) (subst-wontwork _ _ _).
%total (D1) (subst-wontwork _ D1 _).Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)- : {T':tp} {X1:exp} {X2:tp} {X3:exp -> exp -> exp} {X4:exp -> exp -> tp} {D1:of X1 X2} {D2:{x:exp} assm x X2 -> ({x1:exp} assm x1 T' -> of (X3 x x1) (X4 x x1))} {D2':{x:exp} assm x T' -> of (X3 X1 x) (X4 X1 x)} ({y:exp} {dy:assm y T'} subst-wontwork D1 ([x:exp] [dx:assm x X2] D2 x dx y dy) (D2' y dy)) -> subst-wontwork D1 ([x:exp] [dx:assm x X2] of/lam ([y:exp] [dy:assm y T'] D2 x dx y dy)) (of/lam ([x:exp] [x1:assm x T'] D2' x x1)). %worlds (assm-block) (subst-wontwork _ _ _). Error: Coverage error --- missing cases: {X1:exp} {X2:tp} {X3:exp -> tp} {X4:exp -> exp -> exp} {X5:exp -> exp -> tp} {X6:of X1 X2} {X7:{x:exp} assm x X2 -> ({x1:exp} assm x1 (X3 x) -> of (X4 x x1) (X5 x x1))} {X8:of (exp/lam (X3 X1) ([x:exp] X4 X1 x)) (tp/pi (X3 X1) ([x:exp] X5 X1 x))} |- subst-wontwork X6 ([x:exp] [dx:assm x X2] of/lam ([x2:exp] [x1:assm x2 (X3 x)] X7 x dx x2 x1)) X8.
%% ABORT %%
In the blocker case for the above proof attempt, the problem was that new assumptions could depend on the x. However, E1 is going to be substituted in for x anyway. If it is substituted in first, then these dependencies disappear. What remains is to show that we can swap in a derivation for of E1 T into a derivation of (assm E1 T -> of (E2 E1) (T' E1)).
In the statement of the following metatheorem, (E2 E1) and (T' E1) are generalized by the schematic variables E3 and T, respectively.
subst* : of E1 T
-> (assm E1 T -> of E3 T'')
-> of E3 T''
-> type.
%mode subst* +D1 +D2 -D3.
% case for substituting out the assumption
- : subst* D1 ([dx] of/var dx) D1.
% catch-all case for of/unit or instances of of/var for a different assumption
- : subst* D1 ([dx] D2) D2.
- : subst* D1 ([dx] of/app (D2 dx) (D3 dx)) (of/app D2' D3')
<- subst* D1 D2 D2'
<- subst* D1 D3 D3'.
- : subst* D1 ([dx] of/sing (D2 dx)) (of/sing D2')
<- subst* D1 D2 D2'.
- : subst* D1 ([dx] of/lam ([y][dy] D2 dx y dy)) (of/lam D2')
<- ({y}{dy} subst* D1 ([dx] D2 dx y dy) (D2' y dy)).
%worlds (assm-block) (subst* _ _ _).
%total (D1) (subst* _ D1 _).
Having proved the preceding lemma, the general substitution principle can be proven by first substituting E1 in for x, and then applying subst* to eliminate the dependency on assm E1 T.
subst : of E1 T
-> ({x:exp}{dx:assm x T} of (E2 x) (T' x))
-> of (E2 E1) (T' E1)
-> type.
%mode subst +D1 +D2 -D3.
- : subst (D1 : of E1 T) (D2 : {x} {dx:assm x T} of (E2 x) (T' x)) D2'
<- subst* D1 (D2 E1) D2'.
%worlds (assm-block) (subst _ _ _).
%total {} (subst _ _ _).See Twelf's output
Remarks about adequacy
The reader may have concerns as to whether this proof technique affects adequacy for the object language. Although the second input to the subst* is not an adequate encoding of a typing derivation that makes a proper extension to the LF context (because it is missing an {x:exp} argument), the result is a valid typing derivation in the object logic. subst* is a correct lemma about LF terms of a particular form. Doing a proof of subst using subst* does not "break" the object language in any way, because 1) the deviations from adequate encodings occured only in intermediate stages of the proof and 2) the proof produces results that are adequate encodings of the object language.
Comparison to the POPLMark 1a narrowing proof
This technique is similar to how the narrowing lemma was proven for POPLMark challenge 1a. However, because we are proving a substitution lemma instead of narrowing the type of a variable, we have an actual term to substitute in for the variable. Because the variable can be substituted away and does not have to be put into the LF context, this proof does not need to deal with any special worlds.
Read more Twelf tutorials and other Twelf documentation.
