Logical Frameworks, Encodings, and Adequacy

Proof. Prove the statement after $k$ enclosing binders simultaneously for every $k\ge 0$. The weakening renaming is then the $k$-fold lift $(+1{)}^{\uparrow k}$, and the substitution is ${\tau }^{\uparrow k}$. Induct on $s$. For a variable $i$, the two sides are $${\mathsf{rename}}_{(+1{)}^{\uparrow k}}({\tau }^{\uparrow k}(i))\text{and}((+1{)}^{\uparrow k}(i))[{\tau }^{\uparrow (k+1)}];$$ the zero and successor clauses of lifting make them identical. Application uses the two induction hypotheses. Under ${\lambda }_A$, the defining clauses lift both the weakening and the substitution once, so the body equation is the induction hypothesis at $k+1$. Taking $k=0$ gives the displayed law. ◻

Proof. The three equations are inductions on $t$. In the abstraction case, the defining equations give $$(\sigma ;\tau {)}^{\uparrow }={\sigma }^{\uparrow };{\tau }^{\uparrow },{\mathsf{id}}^{\uparrow }=\mathsf{id};$$ the identity equation is proved on variables by the zero and successor cases. For composition, the zero case is reflexive, while the successor case is For typing, induct on $\mathrm{\Gamma }{⊢}_{\mathsf{st}}t:A$. The variable case is the defining property of $\sigma$. Application uses both induction hypotheses. Abstraction uses ${\sigma }^{\uparrow }:(A,\mathrm{\Gamma })\to (A,\mathrm{\Delta })$; its zero branch is typed by Zero, and its successor branch is typed by weakening the corresponding component of $\sigma$. The object abstraction rule then gives the conclusion. ◻

Proof. Generalize opening from depth $0$ to an arbitrary depth $k$ and induct on $t$. At the free atom $x$, the right side opens the inserted $u$ and local closure gives $u^{[k\mapsto y]}=u$; a different free atom uses $y\ne x$. A bound index follows from the definition of opening. Application uses both induction hypotheses, and the abstraction case applies the body hypothesis at depth $k+1$. ◻

Proof. Induct on the typing derivation. Variables and application use the corresponding substitution clauses. In the abstraction case, let $L$ be the finite exclusion set in LN-Lam. Put $$L^{\prime }:=L\cup \mathrm{FV}(u)\cup \mathrm{dom}(\mathrm{\Gamma },\mathrm{\Delta })\cup \{x\}.$$ Let $y\notin L^{\prime }$ be arbitrary. The cofinite premise at this particular $y$ gives $\mathrm{\Gamma },x:A,\mathrm{\Delta },y:C{⊢}_{\mathsf{ln}}{t}_0^y:D$. The induction hypothesis therefore gives $$\mathrm{\Gamma },\mathrm{\Delta },y:C{⊢}_{\mathsf{ln}}(t_0^y)[u/x]:D.$$ Rule induction on the typing derivation of $u$ shows that $u$ is locally closed. Because $y\notin \mathrm{FV}(u)\cup \{x\}$, lemma 61.20 gives $$(t_0^y)[u/x]=(t_0[u/x]{)}^y.$$ Since $y$ was arbitrary outside $L^{\prime }$, rule LN-Lam closes the abstraction with exclusion set $L^{\prime }$. Free renaming is substitution by a variable; preservation is the statement proved above. ◻

Proof. The obstruction in the proof is that $\mathsf{Term}(V,-)$ has no general functorial action on maps of variable families: $V$ occurs to the left of an arrow in $\mathsf{abs}$. Substitution instead instantiates the polymorphic term at the nested family $\mathsf{Term}(V,-)$ and uses graph-relation free theorems to justify flattening, identity, and composition.

Suppose a polymorphic test selected different constructors for two related environment entries $v_0,v_1$. Relate them by $R_A$ and use equality on constructor tags as the result relation. Parametricity requires the two outputs to have related, hence equal, tags, a contradiction. The same argument applies beneath a binder because definition 61.22 quantifies over extensions $R^{\prime }$ that add the fresh pair of bound variables.

Renaming is precomposition: $${\mathsf{rename}}_{\rho }(p)(V)(\delta ):=p(V)({\rho }_V(\delta )).$$ Every component selected by $\rho$ has its declaration’s object type, so the result retains index $B$. Naturality of $\rho$ and parametricity of $p$ prove parametricity of the result.

For substitution, define the structural flattening function from $\mathsf{Term}(\mathsf{Term}(V,-),B)$ to $\mathsf{Term}(V,B)$. The abstraction clause injects the target bound variable before passing it to the source body; every recursive call is on a constructor subterm. Put $${\mathsf{Subst}}_{\theta }(p)(V)(\delta ):=\mathsf{flat}(p(\mathsf{Term}(V,-))({\theta }_V(\delta ))).$$ Every constructor in the definition carries its object type, so induction on the input proves that $\mathsf{flat}$ preserves the index $B$. Relational induction shows that flattening preserves related terms; together with parametricity of $p$ and $\theta$, this proves parametricity of the result.

The identity law uses the free theorem, not merely an induction on an arbitrary host function. Let ${\mathsf{mapVar}}_V:\mathsf{Env}(V,\mathrm{\Gamma })\to \mathsf{Env}(\mathsf{Term}(V,-),\mathrm{\Gamma })$ inject every environment component. Instantiate parametricity of $p$ with the graph of $\mathsf{var}$. It gives $$\mathsf{TermRel}(\mathrm{graph}(\mathsf{var}))(p(V)(\gamma ),p(\mathsf{Term}(V,-))({\mathsf{mapVar}}_V(\gamma ))).$$ Induction on that relational derivation proves that flattening its right-hand term returns its left-hand term; its abstraction case uses the extensional HOAS equality stated in the theorem. This is ${\mathsf{Subst}}_{\mathsf{id}}(p)(V)(\gamma )=p(V)(\gamma )$.

For composition, let $\theta :\mathrm{\Gamma }{\Rightarrow }_T\mathrm{\Delta }$ and $\varphi :\mathrm{\Delta }{\Rightarrow }_T\mathrm{\Xi }$. Define their composite componentwise by $$(\theta ;\varphi {)}_V(\xi ):=\mathsf{flatEnv}({\theta }_{\mathsf{Term}(V,-)}({\varphi }_V(\xi ))),$$ where $\mathsf{flatEnv}$ applies $\mathsf{flat}$ to every environment component. By the componentwise definition of $\mathsf{EnvRel}$, the graph of $\mathsf{flat}$ relates this nested environment to its $\mathsf{flatEnv}$ image. Naturality and parametricity of $\theta$ and $\varphi$ separately prove that the displayed composite is a natural, parametric substitution family. Instantiate parametricity of $p$ with that graph relation. It relates $$p(\mathsf{Term}(\mathsf{Term}(V,-),-))({\theta }_{\mathsf{Term}(V,-)}({\varphi }_V(\xi )))$$ to $$p(\mathsf{Term}(V,-))((\theta ;\varphi {)}_V(\xi )).$$ Induction on this $\mathsf{TermRel}(\mathrm{graph}(\mathsf{flat}))$ derivation proves that flattening the left twice equals flattening the right once; the Kripke-related abstraction case again uses extensional HOAS equality. Unfolding the two substitution definitions therefore gives the exact pointwise equation $${\mathsf{Subst}}_{\varphi }({\mathsf{Subst}}_{\theta }(p))(V)(\xi )={\mathsf{Subst}}_{\theta ;\varphi }(p)(V)(\xi ).$$ This argument uses no functorial action of $\mathsf{Term}$ on variable-family maps; the negative occurrence of the variable family in $\mathsf{abs}$ supplies no such general action. Renaming identity and composition are ordinary precomposition. Thus free-variable renaming uses $\rho$, while beta-substitution uses the environment substitution $\theta$; neither operation requires an ill-typed closed “variable injection.” ◻

Proof. Induct on $t$. Variable lookup has the family declared by $\sigma$. Application uses both induction hypotheses. Under an abstraction, extend $\sigma$ by the new variable and weaken its old components; this is exactly the lifted substitution ${\sigma }^{\uparrow }$ of lemma 61.19. The identity and composition equations follow by the same induction, with the abstraction case reduced to the corresponding lifted equations. Relative to the fixed ordered $\mathrm{\Gamma }$, erasure maps the $i$th contextual variable to index $i$; its inverse selects the chosen name of the $i$th declaration. Changing that naming changes the inverse only by simultaneous alpha-renaming. Induction on terms proves both inverse equations modulo alpha and the substitution square. ◻

Proof. The four preservation results are lemma 61.19, lemma 61.21, theorem 61.24, proposition 61.25. Each cited statement constructs substitution in its representation and proves the displayed typing implication of this section. ◻