Logical frameworks and representations of binding

Chapter 61: LF, canonical heads, and adequacy

LF signatures distinguish family declarations $a:K$ from object declarations $c:A$. In addition to the inherited dependent-product, abstraction, application, structural, and beta–eta conversion rules, the framework-specific rules are $$\frac{\phantom{X}}{\cdot {⊢}_{\mathrm{\Sigma }}\mathsf{type}\mathsf{kind}}\mathrm{Type}\frac{a:K\in \mathrm{\Sigma }}{\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}a:K}\mathrm{Fam}\frac{c:A\in \mathrm{\Sigma }}{\mathrm{\Gamma }{⊢}_{\mathrm{\Sigma }}c:A}\mathrm{Con}.$$ Products in families and kinds bind only object variables. A canonical object at a product family is an annotated lambda; at an atomic family it is a variable or object constant fully applied to canonical arguments. The implicational object logic has exactly $$\frac{u:P\in \mathrm{\Delta }}{\mathrm{\Delta }{⊢}_{\supset }u:P}\mathrm{Sup}-\mathrm{Assm}\frac{\begin{array}{c}\mathrm{\Delta },u:P{⊢}_{\supset }D:Q\\ u\notin \mathrm{dom}(\mathrm{\Delta })\end{array}}{\mathrm{\Delta }{⊢}_{\supset }\mathsf{supI}(u.D):P\supset Q}\mathrm{Sup}-\mathrm{I}$$ $$\frac{\begin{array}{c}\mathrm{\Delta }{⊢}_{\supset }D:P\supset Q\\ \mathrm{\Delta }{⊢}_{\supset }E:P\end{array}}{\mathrm{\Delta }{⊢}_{\supset }\mathsf{supE}(D,E):Q}\mathrm{Sup}-\mathrm{E}.$$ The STLC object judgment used for the binding-rich encoding has the ordinary variable, annotated-lambda, and application rules. Its LF signature declares $\mathsf{tm}:\mathsf{tp}\to \mathsf{type}$, with fully applied heads $\mathsf{lam}:(\mathsf{tm}A\to \mathsf{tm}B)\to \mathsf{tm}(\mathsf{arr}AB)$ and $\mathsf{app}:\mathsf{tm}(\mathsf{arr}AB)\to \mathsf{tm}A\to \mathsf{tm}B$, including their implicit $A,B:\mathsf{tp}$ products.

For the de Bruijn comparison, contexts list their newest declaration first. Membership is generated by

$0:A\in (A,\mathrm{\Gamma })$

$i:A\in \mathrm{\Gamma }$

$i+1:A\in (B,\mathrm{\Gamma })$

For the locally nameless comparison, the cofinite binder rule is

$L{\subseteq }_{\mathrm{fin}}\mathbb{A}$$\mathrm{\forall }x\notin L.\mathrm{\Gamma },x:A{⊢}_{\mathsf{ln}}{t}^x:B$

$\mathrm{\Gamma }{⊢}_{\mathsf{ln}}{\lambda }_{A}t:A\to B$

Chapter 62: nominal support, binding, and substitution

A finite set $S$ supports $x$ exactly when $$(\mathrm{\forall }\pi )((\mathrm{\forall }a\in S.\pi (a)=a)⟹\pi \cdot x=x),a\mathrm{\#}x⟺a\notin \mathrm{supp}(x).$$ Name abstraction is the least equivalence generated by $$(a,x)\sim (b,(ab)\cdot x)\text{when }b\mathrm{\#}x,\pi \cdot [a]x=[\pi (a)](\pi \cdot x).$$ Its support equation is $$\mathrm{supp}([a]x)=\mathrm{supp}(x)\setminus \{a\}.$$ The complete nominal STLC sheet is

$a:A\in \mathrm{\Gamma }$

$\mathrm{\Gamma }{⊢}_{\mathsf{nom}}\mathsf{var}(a):A$

$\mathrm{\Gamma }{⊢}_{\mathsf{nom}}t:A\to B$$\mathrm{\Gamma }{⊢}_{\mathsf{nom}}u:A$

$\mathrm{\Gamma }{⊢}_{\mathsf{nom}}\mathsf{app}(t,u):B$

$\mathrm{\Gamma },a:A{⊢}_{\mathsf{nom}}t:B$$a\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Gamma }{⊢}_{\mathsf{nom}}{\mathsf{lam}}_A([a]t):A\to B$

Capture-avoiding substitution at a binder first chooses a representative $[b]t=[c]t^{\prime }$ with $c\mathrm{\#}(a,u)$, then uses $${\mathsf{lam}}_A([b]t)[u/a]={\mathsf{lam}}_A([c](t^{\prime }[u/a])).$$ The fresh-representative lemma makes the clause total, and abstraction comparison plus equivariance makes it independent of $c$. For a simultaneous typed substitution $\sigma :\mathrm{\Gamma }\to \mathrm{\Delta }$, define $operatornamesupp(\sigma )$ as the union of its component supports. At a binder fresh for both contexts and this support, the complete clause is $${\mathsf{lam}}_A([b]t)[\sigma ]={\mathsf{lam}}_A([b](t[{\sigma }^{+b}])),{\sigma }^{+b}(b)=\mathsf{var}(b),$$ with ${\sigma }^{+b}$ equal to $\sigma$ on every old atom.

Chapter 63: contextual objects and hereditary substitution

The simply typed modal rules, with all premises, are $$\frac{\mathrm{\Delta };\mathrm{\Psi }⊢M:A}{\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{box}(\mathrm{\Psi }.M):[\mathrm{\Psi }⊢A]}\mathrm{Ctx}-\mathrm{I}$$ $$\frac{\begin{array}{c}\mathrm{\Delta };\mathrm{\Gamma }⊢M:[\mathrm{\Psi }⊢A]\\ \mathrm{\Delta },u::A[\mathrm{\Psi }];\mathrm{\Gamma }⊢N:C\end{array}}{\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{letbox}(M,u.N):C}\mathrm{Ctx}-\mathrm{E}$$ $$\frac{\begin{array}{c}u::A[\mathrm{\Psi }]\in \mathrm{\Delta }\\ \mathrm{\Delta };\mathrm{\Gamma }⊢\sigma :\mathrm{\Psi }\end{array}}{\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{clo}(u,\sigma ):A}\mathrm{Meta}.$$ The dependent canonical extension adds $$\frac{\begin{array}{c}⊢\mathrm{\Delta }\mathsf{mctx}\\ \mathrm{\Delta }⊢\mathrm{\Psi }\mathsf{ctx}\\ \mathrm{\Delta };\mathrm{\Psi }⊢A\Leftarrow \mathsf{type}\end{array}}{⊢\mathrm{\Delta },u::A[\mathrm{\Psi }]\mathsf{mctx}}\mathrm{MCtx}$$ $$\frac{\begin{array}{c}\mathrm{\Delta }⊢\mathrm{\Psi }\mathsf{ctx}\\ \mathrm{\Delta };\mathrm{\Psi }⊢A\Leftarrow \mathsf{type}\\ \mathrm{\Delta },u::A[\mathrm{\Psi }];\mathrm{\Gamma }⊢B\Leftarrow \mathsf{type}\end{array}}{\mathrm{\Delta };\mathrm{\Gamma }⊢\prod _{u::A[\mathrm{\Psi }]}B\Leftarrow \mathsf{type}}\mathrm{MPi}$$ $$\frac{\mathrm{\Delta },u::A[\mathrm{\Psi }];\mathrm{\Gamma }⊢M\Leftarrow B}{\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{mlam}(u.M)\Leftarrow \prod _{u::A[\mathrm{\Psi }]}B}\mathrm{MLam}$$ $$\frac{\begin{array}{c}\mathrm{\Delta };\mathrm{\Gamma }⊢R\Rightarrow \prod _{u::A[\mathrm{\Psi }]}B\\ \mathrm{\Delta };\mathrm{\Psi }⊢N\Leftarrow A\end{array}}{\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{mapp}(R,\hat{\mathrm{\Psi }}.N)\Rightarrow (B[\hat{\mathrm{\Psi }}.N/u]{)}_{A[\mathrm{\Psi }]}^a}\mathrm{MApp}.$$ Closure and explicit-substitution formation are $$\frac{\mathrm{\Delta },u::A[\mathrm{\Psi }],{\mathrm{\Delta }}^{\prime };\mathrm{\Gamma }⊢\sigma \Leftarrow \mathrm{\Psi }}{\mathrm{\Delta },u::A[\mathrm{\Psi }],{\mathrm{\Delta }}^{\prime };\mathrm{\Gamma }⊢\mathsf{clo}(u,\sigma )\Rightarrow (A[\sigma ]{)}_{\mathrm{\Psi }}^a}\mathrm{MVar}$$ $$\frac{\phantom{X}}{\mathrm{\Delta };\mathrm{\Gamma }⊢\cdot \Leftarrow \cdot }\mathrm{SNil}\frac{\begin{array}{c}\mathrm{\Delta };\mathrm{\Gamma }⊢\sigma \Leftarrow \mathrm{\Psi }\\ \mathrm{\Delta };\mathrm{\Gamma }⊢M\Leftarrow (A[\sigma ]{)}_{\mathrm{\Psi }}^a\end{array}}{\mathrm{\Delta };\mathrm{\Gamma }⊢\sigma ,M/x\Leftarrow \mathrm{\Psi },x:A}\mathrm{SNorm}$$ $$\frac{\begin{array}{c}\mathrm{\Delta };\mathrm{\Gamma }⊢\sigma \Leftarrow \mathrm{\Psi }\\ \mathrm{\Delta };\mathrm{\Gamma }⊢R\Rightarrow A^{\prime }\\ A^{\prime }=(A[\sigma ]{)}_{\mathrm{\Psi }}^a\end{array}}{\mathrm{\Delta };\mathrm{\Gamma }⊢\sigma ,R//x\Leftarrow \mathrm{\Psi },x:A}\mathrm{SAtom}.$$ The hereditary operation is partial on raw syntax. Preservation therefore requires the existence and well-formedness premises printed in theorem 63.6; they are part of the theorem, not implicit side conditions.