Dependent Nominal Type Theory

Prerequisites. Direct starred prerequisites: Chapter 62, Chapter 23. No later core chapter depends on this route.

The LF declaration $$\mathsf{lam}:(\mathsf{exp}\to \mathsf{exp})\to \mathsf{exp}$$ represents a binder without choosing a numerical index. It does not make the object-language question “are these names different?” available inside the signature. The obstruction is not binding itself. It is the absence of first-class names, freshness, and a typed operation for opening an abstraction.

This chapter freezes Cheney’s dependent nominal type theory, abbreviated $\mathsf{DNTT}$ [Che12]. Its ordinary fragment is LF; its new ingredients are name types, fresh-name context extensions, name-abstraction types, and concretion at a literal name. Its equality algorithm erases dependencies and uses a Kripke logical relation. No hereditary-substitution argument is substituted for that proof.

Atoms, support, and abstraction

Let $\mathbb{A}$ be a countably infinite set of atoms. A finite permutation $\pi$ is a bijection on $\mathbb{A}$ that moves only finitely many atoms. Transpositions $(ab)$ generate the finite permutations. A permutation action on a set $X$ satisfies $$\mathsf{id}\cdot x=x,({\pi }_2\circ {\pi }_1)\cdot x={\pi }_2\cdot ({\pi }_1\cdot x).$$ A finite set $S\subseteq \mathbb{A}$ supports $x\in X$ when every permutation fixing $S$ pointwise fixes $x$. A nominal set is a permutation set in which every element has finite support. Write $a\mathsf{fresh}x$ when $a$ is outside the least support of $x$.

Proof of Lemma 64.1 — Fresh atoms exist

Proof. The union $S=\bigcup _i\mathrm{supp}(x_i)$ is finite. Since $\mathbb{A}$ is infinite, choose $a\in \mathbb{A}\setminus S$. ◻

Name abstraction is not an ordered pair. On $\mathbb{A}\times X$, put $$(a,x)\sim (b,y)⟺\text{for some }c\mathsf{fresh}a,b,x,y,(ac)\cdot x=(bc)\cdot y.$$ The abstraction $⟨a⟩x$ is the equivalence class of $(a,x)$, and $[\mathbb{A}]X$ is the set of such classes. Different fresh choices of $c$ give the same relation: conjugating one fresh transposition to another uses a permutation that fixes the finite support of the remaining data. The same witness proves symmetry because equality is symmetric. For transitivity, choose one atom fresh for both given witnesses and the three pairs, then compose the two transposition equations. Thus $\sim$ is an equivariant equivalence relation [GP02]. For a fixed binder, abstraction is injective: if $⟨a⟩x=⟨a⟩y$, choose $c$ fresh for $a,x,y$. The defining equation gives $(ac)\cdot x=(ac)\cdot y$, and applying the same transposition gives $x=y$.

Proof of Lemma 64.2 — Support of abstraction

Proof. Let $S=\mathrm{supp}(x)\setminus \{a\}$. If $\pi$ fixes $S$, put $d=\pi a$. If $d=a$, then $\pi$ fixes all of $\mathrm{supp}(x)$. Otherwise $d\notin S$, and $\pi$ agrees on $\mathrm{supp}(x)$ with the transposition $(ad)$. In either case, the abstraction equation gives $⟨\pi a⟩(\pi \cdot x)=⟨a⟩x$, so $S$ supports the class. Conversely, if $b\ne a$ belongs to $\mathrm{supp}(x)$ but not to a support of the abstraction, choose $c$ fresh for that support, $a,b,x$. The transposition $(bc)$ would fix the class and $a$; fixed-binder injectivity would then make it fix $x$. This contradicts the fresh-transposition characterization of least support because $b\in \mathrm{supp}(x)$ and $c$ is fresh for $x$. The atom $a$ is removed by abstraction itself. ◻

For example, $⟨a⟩a=⟨b⟩b$: choose $c$ fresh for $a,b$, then $(ac)\cdot a=c=(bc)\cdot b$. But $⟨a⟩b\ne ⟨a⟩c$ for distinct $a,b,c$, since their supports are $\{b\}$ and $\{c\}$.

The dependent nominal signature

Fix disjoint countable sets of variables $x,y$, literal names $a,b$, object constants $c$, type constants $p$, and name-type constants $\alpha$. The exact syntactic classes are The binders $\mathsf{N}a:\alpha .B$ and $⟨a:\alpha ⟩M$ bind $a$. The expression $M@a$, called concretion, may use only a literal name as its right argument. Name-type constants cannot depend on terms.

A signature contains closed declarations $p:K$, $c:A$, and $\alpha :\mathsf{name}$. Contexts are ordered lists $$\mathrm{\Gamma }::=\cdot \mid \mathrm{\Gamma },x:A\mid \mathrm{\Gamma };\mathsf{fresh}a:\alpha .$$ The last extension asserts that $a$ is fresh for the whole prefix. Thus $\mathrm{\Gamma },x:A;\mathsf{fresh}a:\alpha$ embeds into $\mathrm{\Gamma };\mathsf{fresh}a:\alpha ,x:A$, but the reverse embedding need not hold: the latter context does not assert that $a$ is fresh for $A$.

The judgment $\mathrm{\Gamma }\mathsf{restrict}a:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime }$ removes $a$ and everything declared after it: $$\frac{\phantom{X}}{\mathrm{\Gamma };\mathsf{fresh}a:\alpha \mathsf{restrict}a:\alpha \Rightarrow \mathrm{\Gamma }}\mathrm{R}-\mathrm{Here}$$ $$\frac{\mathrm{\Gamma }\mathsf{restrict}a:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime }}{\mathrm{\Gamma };\mathsf{fresh}b:\beta \mathsf{restrict}a:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime };\mathsf{fresh}b:\beta }\mathrm{R}-\mathrm{Name}$$ $$\frac{\mathrm{\Gamma }\mathsf{restrict}a:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime }}{\mathrm{\Gamma },x:A\mathsf{restrict}a:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime }}\mathrm{R}-\mathrm{Var}.$$ The asymmetry matters: R-Name retains a later fresh name, whereas R-Var discards a later variable because its type may mention $a$.

The ordinary LF formation, variable, product, abstraction, application, and conversion rules are those of chapter 23. The nominal rules are the following; all judgments are relative to a well-formed signature. $$\frac{\alpha :\mathsf{name}\in \mathrm{\Sigma }}{\mathrm{\Gamma }⊢\alpha :\mathsf{type}}\mathrm{Name}-\mathrm{Type}$$ $$\frac{\begin{array}{c}\alpha :\mathsf{name}\in \mathrm{\Sigma }\\ \mathrm{\Gamma };\mathsf{fresh}a:\alpha ⊢B:\mathsf{type}\end{array}}{\mathrm{\Gamma }⊢\mathsf{N}a:\alpha .B:\mathsf{type}}\mathrm{New}-\mathrm{Type}$$ $$\frac{a:\alpha \in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢a:\alpha }\mathrm{Name}\frac{\mathrm{\Gamma };\mathsf{fresh}a:\alpha ⊢M:B}{\mathrm{\Gamma }⊢⟨a:\alpha ⟩M:\mathsf{N}a:\alpha .B}\mathrm{Name}-\mathrm{Abs}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }\mathsf{restrict}b:\alpha \Rightarrow {\mathrm{\Gamma }}^{\prime }\\ {\mathrm{\Gamma }}^{\prime }⊢M:\mathsf{N}a:\alpha .B\end{array}}{\mathrm{\Gamma }⊢M@b:B[b/a]}\mathrm{Concretion}.$$ The restriction premise prevents a term constructed with information declared after $b$ from being opened at $b$.

Proof of Lemma 64.3 — Restriction is deterministic

Proof. Induct on the first derivation and invert the second. A final R-Here forces the same last name declaration. A final R-Name or R-Var forces the same outer context constructor; the induction hypothesis identifies the prefixes. These are all rules. ◻

Substitution and the name beta–eta laws

A simultaneous substitution may assign objects to variables and literal names to names: $\theta ::=\cdot \mid \theta ,M/x\mid \theta ,b/a$. It is well formed, written $\mathrm{\Delta }⊢\theta :\mathrm{\Gamma }$, when it maps every declaration of $\mathrm{\Gamma }$ to legal data in $\mathrm{\Delta }$, and the name case respects restriction: $$\frac{\begin{array}{c}\mathrm{\Delta }\mathsf{restrict}b:\alpha \Rightarrow {\mathrm{\Delta }}^{\prime }\\ {\mathrm{\Delta }}^{\prime }⊢\theta :\mathrm{\Gamma }\end{array}}{\mathrm{\Delta }⊢(\theta ,b/a):\mathrm{\Gamma };\mathsf{fresh}a:\alpha }\mathrm{Sub}-\mathrm{Name}.$$ The operation $\theta -a$ deletes the image of $a$ and all later variable assignments. It mirrors context restriction.

Proof of Lemma 64.4 — Substitution restriction

Proof. Induct on the restriction derivation. The R-Here case inverts the final Sub-Name rule. The R-Name case applies the induction hypothesis and rebuilds Sub-Name; the R-Var case discards the corresponding object assignment. Restriction determinacy identifies the intermediate contexts. ◻

Proof of Theorem 64.5 — General substitution

Proof. Proceed by rule induction. The LF cases use ordinary capture-avoiding substitution. The name-formation and abstraction cases rename their bound atom fresh for $\theta$. For concretion, use lemma 64.4 to restrict $\mathrm{\Delta }$ at $\theta (b)$, then apply the induction hypothesis to the abstraction in that restricted context. Rule Concretion rebuilds the result. Declarations discarded by restriction cannot occur freely in its term or type, so $$M[\theta -b]=M[\theta ],B[\theta -b][\theta (b)/a]=B[b/a][\theta ].$$ This is the only new critical case. ◻

Definitional equality contains ordinary LF beta–eta equality and $$(⟨a:\alpha ⟩M)@b\equiv M[b/a]$$ when restriction at $b$ is defined. Its name-eta rule is $$\frac{\mathrm{\Gamma };\mathsf{fresh}a:\alpha ⊢M@a=N@a:B}{\mathrm{\Gamma }⊢M=N:\mathsf{N}a:\alpha .B}\mathrm{Name}-\mathrm{Eta}.$$ Beta is type preserving by the name-renaming instance of theorem 64.5; eta is type preserving because the fresh extension restricts back to $\mathrm{\Gamma }$.

Algorithmic beta–eta equivalence

Dependency is erased only for the equality algorithm: Erasure supplies a well-founded index for comparison; it does not assert that dependent types are simply typed. Write $\mathrm{\Delta }⊢M⟺N:\tau$ for extensional algorithmic equivalence and $\mathrm{\Delta }⊢M\leftrightarrow N:\tau$ for structural comparison of neutral heads. Both relations weak-head reduce before inspecting a head. The new clauses are $$\frac{a:\alpha \in \mathrm{\Delta }}{\mathrm{\Delta }⊢a\leftrightarrow a:\alpha }\mathrm{Alg}-\mathrm{Name}$$ $$\frac{\begin{array}{c}\mathrm{\Delta }\mathsf{restrict}a:\alpha \Rightarrow {\mathrm{\Delta }}^{\prime }\\ {\mathrm{\Delta }}^{\prime }⊢M\leftrightarrow N:[\alpha ]\tau \end{array}}{\mathrm{\Delta }⊢M@a\leftrightarrow N@a:\tau }\mathrm{Alg}-\mathrm{Conc}$$ $$\frac{\mathrm{\Delta };\mathsf{fresh}a:\alpha ⊢M@a⟺N@a:\tau }{\mathrm{\Delta }⊢M⟺N:[\alpha ]\tau }\mathrm{Alg}-\mathrm{New}-\mathrm{Ext}.$$ At a function type the extensional clause compares $Mx$ and $Nx$ at a fresh variable; at an atomic type it invokes structural comparison. Structural application compares heads structurally and arguments extensionally. Kind and type comparison use the same erasure, with congruence for $\mathrm{\Pi }$ and $\mathsf{N}$.

Proof of Theorem 64.6 — Soundness of algorithmic equivalence

Proof. Use simultaneous induction on the algorithmic and structural derivations. The function case reconstructs declarative function eta, and each LF neutral head reconstructs its matching congruence rule. Rule Alg-Name reconstructs name reflexivity. For Alg-Conc, typing inversion and soundness of erased restriction recover the same unique restricted context for both terms; the induction hypothesis gives equality there, and concretion congruence rebuilds the conclusion. Rule Alg-New-Ext uses declarative name eta. Subject reduction justifies the preliminary weak-head steps. These cases exhaust the nominal additions. ◻

Completeness requires the direction syntax induction cannot supply. A Kripke relation is defined by induction on erased types. At atomic types it is algorithmic equivalence. At arrows and name abstractions it is Logical substitutions relate pointwise, with the name clause mediated by restriction.

Proof of Lemma 64.7 — Fundamental logical-relation lemma

Proof. Induct on declarative equality. Lambda beta and eta use the arrow clause. In the name-beta case, logical substitution restriction yields a common context restricted at $\theta (b)=\rho (b)$; the induction hypothesis compares the bodies there, and closure under weak-head reduction relates the redex to its contractum. In the name-eta case, extend the substitutions by the same fresh name and invoke the abstraction clause. Concretion congruence again uses logical substitution restriction. The remaining cases are the LF clauses. ◻

Proof of Lemma 64.8 — Logical implies algorithmic

Proof. Induct on $\tau$. The atomic case is the definition. At an arrow, weaken by a fresh variable, apply the relation to that variable, use the induction hypothesis, and finish by algorithmic function extensionality. At $[\alpha ]\tau$, extend by a fresh name, apply the name-abstraction clause, use the induction hypothesis on the concretions, and finish with Alg-New-Ext. ◻

Proof of Theorem 64.9 — Completeness and decidability

Proof. Soundness is theorem 64.6. For completeness, use the identity logical substitution in lemma 64.7. Then apply lemma 64.8. Syntax directs the equality algorithm: weak-head reduction is invoked only on well-formed terms, and the logical relation proof supplies termination at the erased type. Restriction is a deterministic finite-context traversal. Bidirectional LF typing invokes the decidable equality algorithm at conversion points; the nominal constructors add only the displayed finite checks. Mutual induction yields a decision procedure. ◻

This is exactly the source’s beta–eta equality boundary. It is not a normalization theorem for a language with nominal recursion. Cheney’s earlier simply typed system has a separate strong-normalization proof; it does not silently strengthen this dependent calculus.

Canonical forms and adequacy

A canonical object is eta-long at its type and beta-normal: $$C::=\lambda x:A.C\mid ⟨a:\alpha ⟩C\mid H,H::=c\mid x\mid a\mid HC\mid H@a.$$ Typing, not this grammar alone, decides whether a neutral is saturated.

Proof of Theorem 64.10 — Canonicalization and conservativity

Proof. Existence runs the complete equality algorithm against the eta-expansion dictated by $A^{-}$. At $[\alpha ]\tau$, introduce a fresh name, canonicalize the concretion, and reabstract. Soundness follows from theorem 64.6; determinism follows by induction, using deterministic restriction for concretion. Hence two canonical forms are equal. For conservativity, a canonical LF judgment can contain no nominal head because its signature and result type contain none. Reading its derivation with the LF rules gives the result. ◻

Fix the signature Encode untyped lambda terms by

Proof of Theorem 64.11 — Adequacy of the nominal encoding

Proof. The forward map is structural; abstraction is independent of the chosen bound name by name-abstraction equality. For surjectivity, invert canonical forms at $\mathsf{exp}$. The only fully applied heads are $\mathsf{var}$, $\mathsf{app}$, and $\mathsf{lam}$. Their arguments recursively decode to a name, two terms, or a name abstraction. In the last case choose a fresh representative and decode its body. The same inversion proves injectivity; for two lambdas, open both at one fresh name and use the induction hypothesis. Renaming commutation is another structural induction. ◻

Add $\mathsf{neq}:\mathsf{exp}\to \mathsf{exp}\to \mathsf{type}$. Its constructor schemes are $${\mathsf{neq}}_{vv}:\mathsf{N}a:\mathsf{vr}.\mathsf{N}b:\mathsf{vr}.\mathsf{neq}(\mathsf{var}a)(\mathsf{var}b),$$ There are also constructors for each pair of unlike heads $\mathsf{var}/\mathsf{app}$, $\mathsf{var}/\mathsf{lam}$, and $\mathsf{app}/\mathsf{lam}$, in both orders. The two nested freshness binders in ${\mathsf{neq}}_{vv}$ force different literal names; the binder in ${\mathsf{neq}}_{\ell \ell }$ opens both bodies at one name [Che12].

Proof of Theorem 64.12 — Adequacy of explicit alpha-inequality

Proof. Forward, induct on the first unequal constructor position. Different variables use the two-fresh-name constructor; application and unlike-head cases use their corresponding constructors. For lambdas, rename both binders to one fresh atom and use the induction hypothesis on the bodies. Conversely, induct on the canonical proof term. Inversion identifies its inequality constructor. The variable constructor can be concreted only at distinct names; the application and unlike-head constructors carry exactly the required smaller inequalities. In the lambda case, concreting at one fresh name produces a smaller inequality proof for the opened bodies. ◻

Adding a name-case operator, fresh-name generation, or recursion over abstractions changes the canonical heads and requires new adequacy and normalization arguments.

Suggested first pass.

Begin with exercise 64.4; then implement exercise 64.6.

Exercise 64.4¶

★★☆ Encode $\lambda a.\lambda b.a$ twice using disjoint binder names. Open both outer abstractions at one fresh name, calculate the two beta steps, and derive algorithmic equality at $[\mathsf{vr}][\mathsf{vr}]\mathsf{exp}$. Mark the use of restriction. (One page.)

Referenced from 4 locations

• Dependent Nominal Type Theory
• Solutions for Chapters 64–66

Exercise 64.5¶

★★☆ The nominal-set function $[\mathbb{A}]\mathbb{A}\to \mathsf{Option}(\mathbb{A})$ returns $\mathsf{none}$ on $⟨a⟩a$ and $\mathsf{some}(b)$ on $⟨a⟩b$ for $a\ne b$. Explain why frozen DNTT cannot define it. Name an eliminator that would make it expressible and the two metatheorems then requiring new proofs.

Referenced from 3 locations

• Dependent Nominal Type Theory
• Solutions for Chapters 64–66

Exercise 64.6¶

★★★ Practical project.nominal-restriction-checker Implement in Agda or Kappa a finite checker for fresh-name contexts. It must calculate restriction, reject concretion when an abstraction depends on a later variable, accept alpha-renamed abstractions, and distinguish $⟨a⟩a$ from $⟨a⟩b$. Print retained and discarded declarations. State that the run checks a finite representation invariant, not DNTT decidability or adequacy.

Referenced from 5 locations

• Dependent Nominal Type Theory
• Object calculus checker and evaluator
• ch:dependent-nominal-type-theory: context restriction