Substitution lemma

Type-preserving substitution is the property of a hypothetical judgment that if $\Gamma, x : A \vdash M(x) : B$ and $\Gamma \vdash N : A$, then $\Gamma \vdash 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.

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
%sort tp %.
%term tp/unit tp %.
%term tp/arrow %pi tp %-> tp %-> tp %.
%sort exp %.
%term exp/unit exp %.
%term exp/lam %pi tp %-> (%pi exp %-> exp) %-> exp %.
%term exp/app %pi exp %-> exp %-> exp %.
%% Typing judgement
%sort of {_ exp} {_ tp} %.
%term of/unit of exp/unit tp/unit %.
%term of/lam
  %pi (of (exp/lam T E) (tp/arrow T T'))
  %<- ({x exp} %pi (of x T) %-> (of (E x) T')) %.
%term of/app %pi (of (exp/app E1 E2) T') %<- (of E2 T) %<- (of E1 (tp/arrow T T')) %.

We can give a direct proof of substitution:

%sort subst {_ of E1 T} {_ {x exp} {dx of x T} of (E2 x) T'} {_ of (E2 E1) T'} %.
%mode subst %in %in %out %.
%term _ subst D1 D2 (D2 E1 D1) %.
%block of-block [T tp] {x exp} {dx of x T}%.
%worlds (of-block) (subst _ _ _) %.
%total {} (subst _ _ _) %.

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
%sort tp %.
%term tp/unit tp %.
%term tp/arrow %pi tp %-> tp %-> tp %.
%sort exp %.
%term exp/unit exp %.
%term exp/lam %pi tp %-> (%pi exp %-> exp) %-> exp %.
%term exp/app %pi exp %-> exp %-> exp %.
%% Typing judgements
%sort assm {_ exp} {_ tp} %.
%sort of {_ exp} {_ tp} %.
%term of/var %pi (of E T) %<- (assm E T) %.
%term of/unit of exp/unit tp/unit %.
%term of/lam
  %pi (of (exp/lam T E) (tp/arrow T T'))
  %<- ({x exp} %pi (assm x T) %-> (of (E x) T')) %.
%term of/app %pi (of (exp/app E1 E2) T') %<- (of E2 T) %<- (of E1 (tp/arrow T T')) %.

Now, we prove the substitution theorem:

%sort subst {_ of E1 T} {_ {x exp} {dx assm x T} of (E2 x) T'} {_ of (E2 E1) T'} %.
%mode subst %in %in %out %.
% case for substituting out the assumption
%term _ subst D1 ([x] [dx] of/var dx) D1 %.
% catch-all case for of/unit or instances of of/var for a different assumption
%term _ 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.

%term _
  %pi (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)) %.
%term _
  %pi (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 [T tp] {x exp} {dx assm x T}%.
%worlds (assm-block) (subst _ _ _) %.
%total (D1) (subst _ D1 _) %.

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.

TODO could be used to do substition in this case, but this technique is much simpler in practice.

%sort tp %.
%sort exp %.
%term tp/sing %pi exp %-> tp %.
%term tp/unit tp %.
%term tp/pi %pi tp %-> (%pi exp %-> tp) %-> tp %.
%term exp/unit exp %.
%term exp/lam %pi tp %-> (%pi exp %-> exp) %-> exp %.
%term exp/app %pi exp %-> exp %-> exp %.
%sort assm {_ exp} {_ tp} %.
%sort of {_ exp} {_ tp} %.
%term of/var %pi (of E T) %<- (assm E T) %.
%term of/unit of exp/unit tp/unit %.
%term of/lam
  %pi (of (exp/lam T E) (tp/pi T T'))
  %<- ({x exp} %pi (assm x T) %-> (of (E x) (T' x))) %.
%term of/app %pi (of (exp/app E1 E2) (T' E2)) %<- (of E2 T) %<- (of E1 (tp/pi T T')) %.
%term of/sing %pi (of E (tp/sing E)) %<- (of E tp/unit) %.
%block assm-block [T tp] {x exp} {dx assm x T}%.

The following metatheorem is actually true, but the naive attempt at proving it will fail.

%sort subst-wontwork {_ of E1 T} {_ {x exp} {dx assm x T} of (E2 x) (T' x)} {_ of (E2 E1) (T' E1)} %.
%mode subst-wontwork %in %in %out %.
% case for substituting out the assumption
%term _ subst-wontwork D1 ([x] [dx] of/var dx) D1 %.
% catch-all case for of/unit or instances of of/var for a different assumption
%term _ subst-wontwork D1 ([x] [dx] D2) D2 %.
%term _
  %pi (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') %.
%term _
  %pi (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 _).

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.

%sort subst* {_ of E1 T} {_ %pi (assm E1 T) %-> (of E3 T'')} {_ of E3 T''} %.
%mode subst* %in %in %out %.
% case for substituting out the assumption
%term _ subst* D1 ([dx] of/var dx) D1 %.
% catch-all case for of/unit or instances of of/var for a different assumption
%term _ subst* D1 ([dx] D2) D2 %.
%term _
  %pi (subst* D1 ([dx] of/app (D2 dx) (D3 dx)) (of/app D2' D3'))
  %<- (subst* D1 D2 D2')
  %<- (subst* D1 D3 D3') %.
%term _ %pi (subst* D1 ([dx] of/sing (D2 dx)) (of/sing D2')) %<- (subst* D1 D2 D2') %.
%term _
  %pi (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.

%sort subst {_ of E1 T} {_ {x exp} {dx assm x T} of (E2 x) (T' x)} {_ of (E2 E1) (T' E1)} %.
%mode subst %in %in %out %.
%term _
  %pi (subst (%the (of E1 T) D1) (%the ({x} {dx assm x T} of (E2 x) (T' x)) D2) D2')
  %<- (subst* D1 (D2 E1) D2') %.
%worlds (assm-block) (subst _ _ _) %.
%total {} (subst _ _ _) %.