Chapter 62Optional

Nominal Syntax, Support, and Binding

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

The raw substitution clause $(λ (b : A) . t) [u / a] \overset{?}{=} λ (b : A) . t [u / a]$ fails when $b$ occurs free in $u$ . For example, it sends $(λ (b : A) . a) [b / a]$ to $λ (b : A) . b$ and captures the free $b$ . Renaming the binder first to an atom $c \notin {a, b}$ gives $λ (c : A) . b$ . Nominal syntax must make this choice independent of $c$ while retaining atoms as data.

Atoms and name abstraction

HOAS makes alpha-renaming an LF conversion, but it does not provide an object-level atom that a program may compare or choose fresh. Nominal syntax keeps atoms as data while quotienting the choice of a bound atom.

Definition 62.1 — Atoms and finite permutations ¶

Let $A$ be a countably infinite set of atoms, which are names that may be permuted. A finite permutation $π : A \to A$ is a bijection that moves only finitely many atoms. Composition and inverse make these permutations a group. The transposition $(a b)$ exchanges $a$ and $b$ and fixes every other atom.

Referenced from 4 locations

Definition 62.2 — Support, freshness, and equivariance ¶

Let the group of finite permutations of $A$ act on a set $X$ . A finite set $S \subseteq A$ supports $x \in X$ when every permutation that fixes each atom of $S$ also fixes $x$ . A set in which every element has finite support is a nominal set. The least finite support of $x$ is written $supp (x)$ . Write $a # x$ , read $a$ is fresh for $x$ , if and only if $a \notin supp (x)$ .

A map $f : X \to Y$ of nominal sets is equivariant if and only if $f (π \cdot x) = π \cdot f (x)$ for every finite permutation $π$ . A predicate is equivariant when its truth value is invariant under the simultaneous permutation of all nominal parameters.

Referenced from 4 locations

Proposition 62.3 — Least finite support ¶

Every finitely supported element has a unique least finite support. If $S$ supports $x$ , then $supp (x) \subseteq S$ . In particular, $a # x$ if and only if some finite support of $x$ omits $a$ . Moreover, if $c # x$ and $b \neq c$ , then $b \in supp (x) ⟺ (b c) \cdot x \neq x .$

Referenced from 4 locations

Proof of Proposition 62.3 — Least finite support

Proof. Gabbay and Pitts prove the claim for the finite-permutation action of definition 62.1 [GP02]. They construct the least support from the transpositions that move $x$ and prove that it is contained in every finite support; this construction also gives the displayed transposition criterion. The freshness equivalence is the definition in terms of that least support. ◻

For atoms, $π \cdot a : = π (a)$ and ${a}$ supports $a$ . For pairs and syntax trees, permutations act componentwise, so the union of component supports is a support. The support condition is stronger than saying that one particular transposition fixes $x$ : it quantifies over every permutation that fixes the chosen finite set.

Definition 62.4 — Name abstraction ¶

For a nominal set $X$ , a name abstraction $[a] x$ is the equivalence class of $(a, x) \in A \times X$ under the least equivalence relation containing $(a, x) \sim (b, (a b) \cdot x) whenever b # x .$ The permutation action is $π \cdot [a] x : = [π (a)] (π \cdot x)$ .

Referenced from 7 locations

The freshness premise is necessary. Without $b # x$ , renaming a binder to a name already used freely in $x$ would identify $λ a . b$ with $λ b . a$ .

Lemma 62.5 — Fresh comparison of abstractions ¶

Let $X$ be a nominal set, let $a, b, d \in A$ , and let $x, y \in X$ . If $d # (a, x, b, y)$ , then $[a] x = [b] y ⟺ (a d) \cdot x = (b d) \cdot y .$

Referenced from 3 locations

Nominal Syntax, Support, and Binding

Proof of Lemma 62.5 — Fresh comparison of abstractions

Proof. First observe that the comparison atom is immaterial. If both $d$ and $e$ are fresh for $(a, x, b, y)$ , then applying $(d e)$ to $(a d) \cdot x = (b d) \cdot y$ gives $(a e) \cdot x = (b e) \cdot y$ : the two permutation composites agree on supports of $x$ and $y$ . Applying $(d e)$ again proves the converse.

For the forward direction, represent equality in the least equivalence of definition 62.4 by a finite chain and choose an auxiliary $e$ fresh for every body and binder in that chain. It suffices to check one generating step $(a, x) \sim (b, (a b) \cdot x), b # x .$ On a support of $x$ , both $(a e)$ and the composite $(b e) (a b)$ send $a$ to $e$ and fix every other supported atom, because $b, e # x$ . Hence their actions on $x$ agree. Equality is preserved by reversing or composing chain steps, which proves the implication. The first observation replaces the auxiliary $e$ by the $d$ in the statement.

Conversely, freshness gives the two generating equalities $[a] x = [d] ((a d) \cdot x), [b] y = [d] ((b d) \cdot y) .$ If the displayed bodies are equal, transitivity proves $[a] x = [b] y$ . ◻

Proposition 62.6 — Support of name abstraction ¶

For every atom $a$ and finitely supported element $x$ , $supp ([a] x) = supp (x) ∖ {a} .$

Referenced from 3 locations

Nominal Syntax, Support, and Binding

Proof of Proposition 62.6 — Support of name abstraction

Proof. This is the support calculation for the abstraction set in Gabbay and Pitts’s construction [GP02]. For the forward inclusion, a permutation fixing $supp (x) ∖ {a}$ may change $a$ , but name abstraction identifies the correspondingly renamed representative. For the reverse inclusion, let $b \neq a$ lie in $supp (x)$ and choose an atom $c$ fresh for $x$ , $a$ , and $b$ . The transposition criterion of proposition 62.3 gives $(b c) \cdot x \neq x$ . If $(b c)$ fixed $[a] x$ , apply lemma 62.5 with a comparison atom fresh for both bodies; because $(b c)$ fixes $a$ , the resulting body equality would imply $(b c) \cdot x = x$ , a contradiction. Hence every support of $[a] x$ contains $b$ . Leastness gives the reverse inclusion. ◻

Lemma 62.7 — Fresh representative ¶

Let $[a] x$ be a name abstraction and let $C \subseteq A$ be finite. There are $b \notin C$ and $y \in X$ such that $[a] x = [b] y$ . More generally, if $z$ is a finite tuple of external nominal parameters and $C$ contains a support of $z$ , then $b$ may be chosen with $b # z$ .

Referenced from 7 locations

Nominal Syntax, Support, and Binding

Proof of Lemma 62.7 — Fresh representative

Proof. Choose $b \notin C \cup S_{x} \cup S_{z},$ where $S_{x}$ supports $x$ and $S_{z}$ supports the external tuple $z$ ; omit $S_{z}$ in the first claim. Such a $b$ exists because $A$ is infinite. Put $y : = (a b) \cdot x$ . Since $b # x$ , definition 62.4 gives $[a] x = [b] y$ . The set $S_{z}$ witnesses $b # z$ . ◻

Definition 62.8 — Nominal STLC syntax ¶

For the types of definition 61.11, nominal terms are generated by $t ::= var (a) ∣ app (t, u) ∣ {lam}_{A} ([a] t) .$ Permutations act on variables, applications componentwise, and abstractions as in definition 62.4. The quotient built into $[a] t$ is the alpha-equivalence of nominal abstractions.

The typing judgment is generated by $\frac{a : A \in Γ}{Γ ⊢_{nom} var (a) : A} Nom - Var$ $\frac{\begin{matrix} Γ ⊢_{nom} t : A \to B \\ Γ ⊢_{nom} u : A \end{matrix}}{Γ ⊢_{nom} app (t, u) : B} Nom - App$ $\frac{\begin{matrix} Γ, a : A ⊢_{nom} t : B \\ a \notin dom (Γ) \end{matrix}}{Γ ⊢_{nom} {lam}_{A} ([a] t) : A \to B} Nom - Lam .$ Contexts are finite lists of distinctly named atoms. The abstraction rule may use any representative fresh for the context; the fresh-comparison lemma and equivariance below show that its conclusion is independent of that choice.

Referenced from 2 locations

Nominal Syntax, Support, and Binding

Lemma 62.9 — Typing equivariance ¶

For every finite permutation $π$ , $Γ ⊢_{nom} t : A$ if and only if $π \cdot Γ ⊢_{nom} π \cdot t : A$ . Here permutation of a context acts only on its atom labels.

Referenced from 3 locations

Nominal Syntax, Support, and Binding

Proof of Lemma 62.9 — Typing equivariance

Proof. The typing claim is rule induction. A variable declaration $a : A \in Γ$ maps to $π (a) : A \in π \cdot Γ$ ; application is componentwise. An abstraction premise under $Γ, a : A$ maps by the induction hypothesis to a premise under $π \cdot Γ, π (a) : A$ . Bijection of $π$ preserves the freshness side condition, so Nom-Lam reconstructs the permuted abstraction. Applying $π^{- 1}$ proves the reverse implication. ◻

Theorem 62.10 — Freshness induction ¶

Let $P$ be a predicate on nominal terms such that $P (π \cdot t) ⟺ P (t)$ for every finite permutation $π$ and nominal term $t$ . Let $C \subseteq A$ be finite. To prove $P (t)$ for every nominal term, it suffices to prove:

$P (var (a))$ for every atom $a$ ;
for all nominal terms $t, u$ , $P (t)$ and $P (u)$ imply $P (app (t, u))$ ;
for every object type $A$ , atom $a$ , and nominal term $t$ , if $a \notin C$ and $P (t)$ , then $P ({lam}_{A} ([a] t))$ .

Referenced from 2 locations

Nominal Syntax, Support, and Binding

Proof of Theorem 62.10 — Freshness induction

Proof. Induct on the quotient syntax. Variable and application use the first two clauses. For an abstraction $[b] u$ , use lemma 62.7 to choose $[b] u = [a] t$ with $a \notin C, t = (b a) \cdot u .$ The induction hypothesis gives $P (u)$ ; the displayed equivalence for the transposition $(b a)$ gives $P (t)$ . The third clause gives $P ({lam}_{A} ([a] t))$ , which is the required property because $[a] t = [b] u$ . ◻

Theorem 62.11 — Freshness recursion ¶

Let $X$ be a nominal set and let $z$ be a finite tuple of external nominal parameters. Suppose the following data are equivariant jointly in $z$ and their displayed arguments: $\begin{aligned} V_{z} (a) & \in X, \\ A_{z} (r_{1}, r_{2}) & \in X, \\ L_{A, z} (a, t, r) & \in X (a # z) . \end{aligned}$ Assume the binder data satisfy the fresh-renaming equation $L_{A, z} (a, t, r) = L_{A, z} (b, (a b) \cdot t, (a b) \cdot r)$ whenever $a # z$ , $b # z$ , and $b # (t, r)$ . Then there is a unique function $F_{z}$ from nominal terms to $X$ , equivariant jointly in $z$ and its term argument, such that $\begin{aligned} F_{z} (var (a)) & = V_{z} (a), \\ F_{z} (app (t, u)) & = A_{z} (F_{z} (t), F_{z} (u)), \\ F_{z} ({lam}_{A} ([a] t)) & = L_{A, z} (a, t, F_{z} (t)) (a # z) . \end{aligned}$ The final equation may use any representative whose binder is fresh for $z$ .

Referenced from 4 locations

Nominal Syntax, Support, and Binding

Proof of Theorem 62.11 — Freshness recursion

Proof. For an abstraction, lemma 62.7 chooses a representative $[a] t$ with $a # z$ . Recurse on $t$ and apply $L_{A, z}$ . If $[b] u$ is another representative with $b # z$ , choose $d # (z, a, t, b, u, F_{z} (t), F_{z} (u))$ . The fresh-comparison equation transports both representatives to binder $d$ ; equivariance of the recursive calls and the fresh-renaming hypothesis for $L$ make the two results equal. Thus the definition is independent of representatives.

Structural induction proves joint equivariance for variables and applications. In the abstraction case, choose a binder fresh for both $z$ and its permuted image and use equivariance of $L$ . Freshness induction proves uniqueness: choose the abstraction representative fresh for $z$ and apply the third defining equation after the induction hypothesis for its body. ◻

Definition 62.12 — Nominal substitution ¶

Apply theorem 62.11 with external parameters $(a, u)$ and codomain the nominal terms. The variable and application data are the first three clauses below, and $L_{A, (a, u)} (b, t, r) : = {lam}_{A} ([b] r)$ . Name abstraction gives the required fresh-renaming equation. The resulting capture-avoiding substitution is $\begin{array}{rcl} var (a) [u / a] & : = & u, \\ var (b) [u / a] & : = & var (b) (b \neq a), \\ app (t_{1}, t_{2}) [u / a] & : = & app (t_{1} [u / a], t_{2} [u / a]), \\ {lam}_{A} ([b] t) [u / a] & : = & {lam}_{A} ([b] (t [u / a])), \end{array}$ where the final clause first chooses a representative satisfying $b # (a, u)$ by lemma 62.7. If $b = a$ , choose a different representative before applying the clause.

Referenced from 4 locations

Nominal Syntax, Support, and Binding

Lemma 62.13 — Nominal substitution and typing ¶

The operation in definition 62.12 is independent of the chosen fresh representative and satisfies $π \cdot (t [u / a]) = (π \cdot t) [(π \cdot u) / π (a)] .$ If $Γ, a : A, Δ ⊢_{nom} t : B and Γ ⊢_{nom} u : A,$ then $Γ, Δ ⊢_{nom} t [u / a] : B$ .

Referenced from 3 locations

Nominal Syntax, Support, and Binding

Proof of Lemma 62.13 — Nominal substitution and typing

Proof. Theorem 62.11 gives independence of the representative. Its joint equivariance equation, instantiated at the parameter tuple $(a, u)$ , is exactly $π \cdot (t [u / a]) = (π \cdot t) [(π \cdot u) / π (a)] .$

For typing, perform rule induction on the given typing derivation, generalized over the context split and substituting derivation. Variables and application use the defining clauses and induction hypotheses. In an abstraction case, choose a finite support $S_{u}$ of $u$ and use lemma 62.7 to select a representative with $b \notin dom (Γ, a : A, Δ) \cup S_{u}$ . Typing equivariance transports the original abstraction premise to that representative, because the required transposition fixes the external context. The transported premise is $Γ, a : A, Δ, b : C_{0} ⊢_{nom} t_{0} : D .$ The induction hypothesis gives $Γ, Δ, b : C_{0} ⊢_{nom} t_{0} [u / a] : D$ ; the abstraction rule closes the result. The fresh choice prevents capture. ◻

Theorem 62.14 — Nominal adequacy for STLC ¶

Let $Γ$ be an STLC context with pairwise distinct atom labels. Define the untyped carriers $\begin{aligned} Named (Γ) & : = {t ∣ FV (t) \subseteq dom (Γ)} / =_{α}, \\ Nom (Γ) & : = {n ∣ b # n for every b \in A ∖ dom (Γ)} . \end{aligned}$ Encoding and decoding are inverse bijections $Named (Γ) ⟷ Nom (Γ)$ that commute with renaming and capture-avoiding substitution. For every object type $A$ , they also satisfy the separate typing equivalence $Γ ⊢_{st} t : A ⟺ Γ ⊢_{nom} encode (t) : A .$

Referenced from 2 locations

Nominal Syntax, Support, and Binding

Proof of Theorem 62.14 — Nominal adequacy for STLC

Proof. Decode $var (a)$ and $app$ componentwise. Decode ${lam}_{A} ([a] t)$ by choosing any representative and returning $λ (a : A) . decode (t)$ . Name abstraction makes this independent of the representative modulo object alpha-equivalence. Encode variables and applications componentwise and encode $λ (a : A) . t$ as ${lam}_{A} ([a] encode (t))$ .

Structural induction gives both inverse equations; the abstraction equation uses exactly the alpha quotient in definition 62.4. Equivariance gives the renaming equation, and induction using the fresh representative in the abstraction case gives the substitution equation. Typing preservation and reflection are rule inductions because the nominal and named rules have the same premises after choosing a representative. ◻

Proposition 62.15 — Nominal and de Bruijn comparison ¶

Given an ordered nominal context $a_{0} : A_{0}, \dots, a_{n - 1} : A_{n - 1}$ , replacing $a_{i}$ by its context position defines a translation to typed de Bruijn syntax. It is invariant under simultaneous permutation of the context and term, and it commutes with typed substitution.

Referenced from 3 locations

Nominal Syntax, Support, and Binding

Proof of Proposition 62.15 — Nominal and de Bruijn comparison

Proof. Translate variables by lookup, application componentwise, and abstraction by choosing a representative whose binder is outside the context and extending the context at the left. Lemma 62.7 supplies the choice. Simultaneously permuting context and term preserves every lookup position, so induction on terms proves invariance. The same induction proves the substitution square; under a binder it is the lifted-substitution equation of lemma 61.19. ◻

Remark 62.16 — Fresh atoms require a larger signature ¶

To state fresh-atom generation as an LF relation, a signature needs an atom family and a judgment family relating an input term to a fresh result atom. The signature $Σ_{st}$ declares neither: it contains only object types, intrinsically typed terms, application, and abstraction. Hence no LF judgment over this signature can even state that an output atom is fresh for an input. Adding an atom family, atom equality, and a freshness relation defines a different framework signature and requires a new adequacy proof.

Referenced from 2 locations

Nominal Syntax, Support, and Binding

Exercise 62.1 ¶

★★☆ Compute ${lam}_{B} ([b] var (a)) [var (b) / a]$ . Choose an atom $c$ with $c \notin {a, b}$ , display the transposition used to change representatives, and show that the result decodes to an alpha-variant of $λ (c : B) . b$ , not $λ (b : B) . b$ . (Half a page.)

Referenced from 3 locations

The substitution support bound

The substitution theorem preserves typing, but it also controls which atoms may remain free. The bound is stated using least support, so it is independent of the particular fresh representative selected under a binder.

Lemma 62.17 — Support of nominal substitution ¶

For nominal terms $t, u$ and an atom $a$ , $supp (t [u / a]) \subseteq (supp (t) ∖ {a}) \cup supp (u) .$

Referenced from 3 locations

Nominal Syntax, Support, and Binding

Proof of Lemma 62.17 — Support of nominal substitution

Proof. Use freshness induction with the finite set $C = {a} \cup supp (u)$ . The variable case is the defining split of substitution. Application uses the two induction hypotheses and the fact that the support of a pair is the union of its component supports.

For an abstraction, choose $b \notin C$ and a representative ${lam}_{A} ([b] t_{0})$ . The defining substitution clause gives ${lam}_{A} ([b] (t_{0} [u / a]))$ . By the induction hypothesis, $supp (t_{0} [u / a]) \subseteq (supp (t_{0}) ∖ {a}) \cup supp (u) .$ Name abstraction removes the bound atom $b$ from support. Since $b \notin {a} \cup supp (u)$ , removing $b$ from the right-hand side yields exactly the required bound for the abstraction by proposition 62.6. ◻

Exercise 62.2 ¶

★☆☆ Let $t = {lam}_{A} ([a] app (var (a), var (b))) .$ Compute $supp (t)$ and the support of $(a c) \cdot t$ for pairwise distinct atoms $a, b, c$ . Then exhibit one permutation fixing the empty set but changing $t$ . (Six lines.)

Referenced from 3 locations

One obligation across four representations

The comparison in theorem 61.26 fixes one STLC renaming and substitution obligation. Nominal syntax satisfies that obligation by lemma 62.9, lemma 62.13; it does not inherit the proof invariant of any of the other representations. The binder case is the point of separation: $\begin{array}{cl} representation & binder operation \\ de Bruijn & lift the substitution and weaken old components \\ locally nameless & open outside a finite exclusion set \\ PHOAS & extend the relation family by the bound pair \\ nominal & choose a representative fresh for the substitution data . \end{array}$ Each row proves the same typing implication. No row provides the side condition named in another row.

Definition 62.18 — Typed simultaneous nominal substitution ¶

A typed substitution $σ : Γ \to Δ$ assigns to each declaration $a : A \in Γ$ a nominal term satisfying $Δ ⊢_{nom} σ (a) : A$ . Its finite support is $supp (σ) : = ⋃_{a \in dom (Γ)} supp (σ (a)) .$ The simultaneous action on variables and applications is componentwise. At an abstraction, choose a representative ${lam}_{A} ([b] t_{0})$ with $b \notin dom (Γ) \cup dom (Δ) \cup supp (σ)$ and put ${lam}_{A} ([b] t_{0}) [σ] : = {lam}_{A} ([b] (t_{0} [σ^{+ b}])) .$ Here $σ^{+ b} : Γ, b : A \to Δ, b : A$ maps $b$ to $var (b)$ and maps every old atom $a$ to $σ (a)$ . Freshness recursion makes the action independent of the chosen representative; rule induction gives $Γ ⊢_{nom} t : C ⟹ Δ ⊢_{nom} t [σ] : C .$ The one-variable operation of definition 62.12 is the instance that is the identity away from its target.

Referenced from 2 locations

Nominal Syntax, Support, and Binding

Proposition 62.19 — Nominal substitution square ¶

Let $Γ$ be an ordered nominal context, let $σ : Γ \to Δ$ be a typed nominal substitution, and let ${db}_{Γ}$ be the translation of proposition 62.15. If $Γ ⊢_{nom} t : C$ , then ${db}_{Δ} (t [σ]) = {db}_{Γ} (t) [db (σ)] .$ Here $db (σ)$ maps the de Bruijn position of each $a$ in $Γ$ to ${db}_{Δ} (σ (a))$ . Changing every atom label by one simultaneous permutation changes neither side.

Referenced from 2 locations

Nominal Syntax, Support, and Binding

Proof of Proposition 62.19 — Nominal substitution square

Proof. Induct on $t$ . Variables are lookup in $σ$ and applications use the two induction hypotheses. For an abstraction, choose a representative $[a] t_{0}$ with $a \notin dom (Γ) \cup dom (Δ) \cup supp (σ) .$ The nominal substitution enters $t_{0}$ with the fresh representative. The de Bruijn translation extends both ordered contexts by their newest declaration and therefore uses the lifted substitution $db (σ)^{↑}$ . The body equation is the induction hypothesis under those extensions; lemma 61.19 identifies the lifted right-hand side. If another fresh representative is selected, typing equivariance transports the nominal premise while simultaneous permutation preserves every de Bruijn lookup position. Hence the equation is independent of the representative. ◻

Remark 62.20 — The boundary of the comparison ¶

The square compares one typed STLC substitution. It proves no equivalence between nominal support and locally nameless local closure, and no parametricity theorem for PHOAS. Nominal unification and dependent nominal typing require calculi and metatheorems beyond this chapter.

Referenced from 2 locations

Nominal Syntax, Support, and Binding

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 62.3, then complete exercise 62.6.

Exercise 62.3 ¶

★☆☆ For pairwise distinct $a, b, c$ , compute least supports of $var (a)$ , $app (var (a), var (b))$ , and ${lam}_{A} ([a] app (var (a), var (b)))$ . For each atom in a computed support, give a transposition that fixes the other computed atoms but changes the term. (Half a page.)

Referenced from 4 locations

Exercise 62.4 ¶

★★☆ Prove that the inclusion in lemma 62.17 can be strict. Give one example because $a$ does not occur in $t$ , and one because an occurrence of $a$ lies under a binder. Compute both sides of the inclusion in each example.

Referenced from 3 locations

Exercise 62.5 ¶

★★★ Let $Γ = (p : C)$ , let $Δ = \cdot$ , let $u$ be a closed term of type $C$ , and define $σ : Γ \to Δ$ by $σ (p) = u$ . For $t = λ (a : A) . λ (b : B) . p$ , prove the nominal–de Bruijn substitution square. Name the representative chosen fresh for $u$ , the two lifted de Bruijn substitutions, and the equivariance equation used after changing the outer representative. (Two pages.)

Referenced from 3 locations

Exercise 62.6 ¶

★★★ Practical project.nominal-substitution-checker Implement in Agda or Kappa finite permutations, finite-support probes, and capture-avoiding substitution for the untyped nominal lambda fragment. Reserve every atom occurring in the body or substitution argument before choosing a replacement binder. Check that the support of $λ a . a b$ is ${b}$ , that transposing $b$ and $d$ transports that support to ${d}$ , that $(λ b . a) [b / a]$ becomes the fresh representative $λ c . b$ , and that substitution stops beneath a binder equal to its target. A version that descends beneath that shadowing binder must fail the fourth oracle.

Referenced from 6 locations

Sources. Finite support and its least-support property are Definition 3.3 and Proposition 3.4 of Gabbay and Pitts [GP02]. Their abstraction-set construction and local-freshness eliminator appear on pp. 15–16; structural iteration, recursion, and induction are Theorem 6.5, Corollary 6.7, and Theorem 6.8 on pp. 17–18; capture-avoiding substitution is Example 6.9 on p. 18. Pitts motivates equivariant predicates and swapping on pp. 2–3; those nominal-logic axioms do not strengthen the nominal-set theorem boundary [Pit03].