ch:logical-frameworks: ch:logical-frameworks

The eta-long form is $$\lambda (x:A).\lambda (y:B).fxy.$$ Here $B$ and $C$ are read in the context extended by $x:A$. For canonical $M:A$ and $N:B[M/x]$, the two contractions, with the dependent annotation made visible, are The final type is $C[M/x][N/y]$.

For the specialized redex, the unreduced proof has representation $$\mathsf{supE}⌜P⌝⌜P⌝(\mathsf{supI}⌜P⌝⌜P⌝(\lambda (u:\mathsf{ded}⌜P⌝).u))e.$$ It is LF beta-normal because its head is the constant $\mathsf{supE}$; LF has no rewrite rule relating $\mathsf{supE}$ and $\mathsf{supI}$. The reduct is represented by the assumption $e$. These two canonical LF objects are not beta-eta equal: their heads are respectively $\mathsf{supE}$ and the context variable $e$. In general, compositionality gives $⌜D[E/u]⌝{=}_{\beta \eta }⌜D⌝[⌜E⌝/u]$; its right side is the beta-result of applying the represented hypothetical body to $⌜E⌝$. That calculation proves compositionality of substitution, not completeness; completeness still requires canonical-head inversion.

For canonical $M:\mathsf{tm}⌜A⌝$, the extension creates the canonical atomic object $$\mathsf{inspect}⌜A⌝M:\mathsf{tm}⌜A⌝.$$ It is fully applied and its LF type is sound, but its head is neither a represented variable nor $\mathsf{lam}$ nor $\mathsf{app}$. The inverse in the adequacy proof has no object constructor to return, so the encoding is not surjective onto canonical LF inhabitants.

With newest de Bruijn declarations at the left, the redex is $({\lambda }_A{\lambda }_{B}1)u$. The outer substitution maps $0$ to $u$. Its lift under the $B$-binder maps $0$ to $0$ and $i+1$ to the weakening of the old component; therefore $$({\lambda }_A{\lambda }_{B}1)u{⟶}_{\mathrm{beta}}{\lambda }_B(1[{\sigma }^{\uparrow }])={\lambda }_B({\mathsf{rename}}_{(+1)}u).$$

Locally nameless syntax gives $({\lambda }_A{\lambda }_B\underset{―}{1})u$. Choose $z\notin \mathrm{FV}(u)$. Opening the outer binder under the inner one leaves the inner index $\underset{―}{0}$ fixed and inserts the free term $u$; closing again gives ${\lambda }_{B}u$. Translation under the new binder weakens the free context, yielding the displayed de Bruijn result.

In open PHOAS, let $U:\mathsf{PTerm}(\mathrm{\Gamma },A)$ represent $u$ and evaluate the redex at $V$ and $\gamma :\mathsf{Env}(V,\mathrm{\Gamma })$. The substitution environment maps the outer binder to $U(V)(\gamma )$. Flattening returns $\mathsf{abs}(y.U(V)(\gamma ))$. For related environments $\gamma ,\delta$, parametricity of $U$ relates $U(V)(\gamma )$ and $U(W)(\delta )$; beneath the second binder, extend that relation by the fresh pair $(y_V,y_W)$. The relation-extension clause prevents the body from inspecting $y$ and choosing a different result.

For contextual syntax, let $\sigma :[\mathrm{\Gamma }⊢x:A]$ map $x$ to $u:[\mathrm{\Gamma }⊢A]$. Under $y:B$, its lift is ${\sigma }^{\uparrow }=(y\mapsto y,x\mapsto \mathsf{weak}(u))$. Hence the body $x$ becomes $\mathsf{weak}(u)$ and the result is $[\mathrm{\Gamma }⊢{\lambda }_B\mathsf{weak}(u):B\to A]$. Erasure of all four results is ${\lambda }_B({\mathsf{rename}}_{(+1)}u)$.

Take $$M=\mathsf{supI}⌜P\supset Q⌝⌜P\supset Q⌝(\lambda (h:\mathsf{ded}⌜P\supset Q⌝).h).$$ Canonical-head inversion first selects $\mathsf{supI}$ and decodes its two proposition arguments as $P\supset Q$. Eta-long inversion exposes the LF lambda, extends the represented context by $h:P\supset Q$, and decodes its body $h$ by the assumption case. The result is $\mathsf{supI}(h.h):(P\supset Q)\supset (P\supset Q)$. Re-encoding applies the same constructor and returns the displayed LF lambda; only its bound name may differ, so the result is alpha-equivalent to $M$.

The new $k$ is a closed canonical atomic LF object of family $\mathsf{tm}(\mathsf{arr}\mathsf{i}\mathsf{i})$. Checking and canonicalization stop successfully at that declared head, but the inverse has only variable, $\mathsf{lam}$, and $\mathsf{app}$ cases. The weakest object extension adds one constant constructor $\kappa :\iota \to \iota$ with typing axiom $\cdot {⊢}_{\mathsf{st}}\kappa :\iota \to \iota$ and sets $⌜\kappa ⌝=k$. The new head case decodes $k$ to $\kappa$; its inverse equation is definitional. No other adequacy case changes.

Let the target context contain one free variable $q:C$, and substitute the de Bruijn variable $0:C$ for the outer free variable of ${\lambda }_A{\lambda }_{B}2$. Without lifting under either binder, the result is ${\lambda }_A{\lambda }_{B}0$; index $0$ denotes the $B$-bound variable, so the free $C$-variable was captured. Two lifts give ${\lambda }_A{\lambda }_{B}2$, which denotes $q$ and has the required type.

For locally nameless syntax, take the body ${\lambda }_{B}p$ and substitute the free atom $y$ for $p$. If the cofinite proof opens the binder at the same atom $y$, opening and free substitution collide. Enlarging the exclusion set by $\{p,y\}$ chooses an atom $z\ne p,y$ and gives ${\lambda }_{B}y$ with $y$ free.

For PHOAS, omit relation extension beneath $\mathsf{abs}$ and use a body that tests its host argument, returning a variable at one related input and an abstraction at the other. The two outputs have different heads and therefore violate $\mathsf{TermRel}(R^{\prime })$. Quantifying over every extension $R^{\prime }$ that contains the bound pair forces equal heads and restores the abstraction case.

For contextual syntax, package the closed identity once as $[\cdot ⊢A\to A]$ and once as $[x:B⊢A\to A]$. Erasing the domain would admit the second package where the first is required. Retaining the exact domain rejects that substitution; weakening first gives a contextual substitution from the larger domain and restores the typing judgment. These four repairs yield the two-binder results computed in exercise 61.4.