The λ-calculus as a nominal set

The λ-calculus with terms defined nominally from the start, over the Atom / FinPerm / NomSet framework. Raw terms carry the FinPerm action and form a NomSet; quotienting by α-equivalence yields Tm, the genuine nominal term type. Changing the bound name of lam to any fresh atom leaves the term equal (Tm.lam_rename) — an equality of terms, not a separate α-relation.

Main definitions

• Raw, atoms, fv — raw terms, their atoms, and free variables.
• AEq — α-equivalence as a generated congruence (refl/symm/trans are constructors, so it is an equivalence relation by construction).
• Tm := Raw / AEq — nominal λ-terms; Tm.var / Tm.app / Tm.lam.

Main results

• instance : NomSet Raw — raw terms as a nominal set (support = all atoms).
• instance : NomSet Tm — nominal λ-terms as a nominal set (support = fv), whose support-minimality is aeq_of_fixes_fv.
• Tm.lam_rename — α-correctness of the binder.

References

• A. M. Pitts, Nominal Sets: Names and Symmetry in Computer Science, CUP 2013.

Raw λ-terms and the permutation action

inductive CatCrypt.Nominal.Lambda.Raw : Type

Raw (pre-α) λ-terms over atoms.

• var : Atom → Raw
• app : Raw → Raw → Raw
• lam : Atom → Raw → Raw

@[instance_reducible]

instance CatCrypt.Nominal.Lambda.instDecidableEqRaw : DecidableEq Raw

Equations

• CatCrypt.Nominal.Lambda.instDecidableEqRaw = CatCrypt.Nominal.Lambda.instDecidableEqRaw.decEq

def CatCrypt.Nominal.Lambda.instDecidableEqRaw.decEq (x✝ x✝¹ : Raw) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.Nominal.Lambda.instDecidableEqRaw.decEq (CatCrypt.Nominal.Lambda.Raw.var a) (CatCrypt.Nominal.Lambda.Raw.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• CatCrypt.Nominal.Lambda.instDecidableEqRaw.decEq (CatCrypt.Nominal.Lambda.Raw.var a) (a_1.app a_2) = isFalse ⋯
• CatCrypt.Nominal.Lambda.instDecidableEqRaw.decEq (CatCrypt.Nominal.Lambda.Raw.var a) (CatCrypt.Nominal.Lambda.Raw.lam a_1 a_2) = isFalse ⋯
• CatCrypt.Nominal.Lambda.instDecidableEqRaw.decEq (a.app a_1) (CatCrypt.Nominal.Lambda.Raw.var a_2) = isFalse ⋯
• CatCrypt.Nominal.Lambda.instDecidableEqRaw.decEq (a.app a_1) (CatCrypt.Nominal.Lambda.Raw.lam a_2 a_3) = isFalse ⋯
• CatCrypt.Nominal.Lambda.instDecidableEqRaw.decEq (CatCrypt.Nominal.Lambda.Raw.lam a a_1) (CatCrypt.Nominal.Lambda.Raw.var a_2) = isFalse ⋯
• CatCrypt.Nominal.Lambda.instDecidableEqRaw.decEq (CatCrypt.Nominal.Lambda.Raw.lam a a_1) (a_2.app a_3) = isFalse ⋯

def CatCrypt.Nominal.Lambda.rawAct (π : FinPerm) : Raw → Raw

The FinPerm action on raw terms: rename every atom (free and bound).

Equations

• CatCrypt.Nominal.Lambda.rawAct π (CatCrypt.Nominal.Lambda.Raw.var a) = CatCrypt.Nominal.Lambda.Raw.var (π.apply a)
• CatCrypt.Nominal.Lambda.rawAct π (s.app t) = (CatCrypt.Nominal.Lambda.rawAct π s).app (CatCrypt.Nominal.Lambda.rawAct π t)
• CatCrypt.Nominal.Lambda.rawAct π (CatCrypt.Nominal.Lambda.Raw.lam a t) = CatCrypt.Nominal.Lambda.Raw.lam (π.apply a) (CatCrypt.Nominal.Lambda.rawAct π t)

theorem CatCrypt.Nominal.Lambda.rawAct_one (t : Raw) : rawAct 1 t = t

theorem CatCrypt.Nominal.Lambda.rawAct_mul (π₁ π₂ : FinPerm) (t : Raw) : rawAct (π₁ * π₂) t = rawAct π₁ (rawAct π₂ t)

@[instance_reducible]

instance CatCrypt.Nominal.Lambda.instMulActionFinPermRaw : MulAction FinPerm Raw

Equations

• CatCrypt.Nominal.Lambda.instMulActionFinPermRaw = { smul := CatCrypt.Nominal.Lambda.rawAct, mul_smul := CatCrypt.Nominal.Lambda.rawAct_mul, one_smul := CatCrypt.Nominal.Lambda.rawAct_one }

@[simp]

theorem CatCrypt.Nominal.Lambda.smul_var (π : FinPerm) (a : Atom) : π • Raw.var a = Raw.var (π.apply a)

@[simp]

theorem CatCrypt.Nominal.Lambda.smul_app (π : FinPerm) (s t : Raw) : π • s.app t = (π • s).app (π • t)

@[simp]

theorem CatCrypt.Nominal.Lambda.smul_lam (π : FinPerm) (a : Atom) (t : Raw) : π • Raw.lam a t = Raw.lam (π.apply a) (π • t)

Atoms of a term and the NomSet structure

def CatCrypt.Nominal.Lambda.atoms : Raw → Finset Atom

Every atom occurring in a term (free or bound) — the support of the raw term (raw terms are not yet α-quotiented, so bound names count).

Equations

• CatCrypt.Nominal.Lambda.atoms (CatCrypt.Nominal.Lambda.Raw.var a) = {a}
• CatCrypt.Nominal.Lambda.atoms (s.app t) = CatCrypt.Nominal.Lambda.atoms s ∪ CatCrypt.Nominal.Lambda.atoms t
• CatCrypt.Nominal.Lambda.atoms (CatCrypt.Nominal.Lambda.Raw.lam a t) = insert a (CatCrypt.Nominal.Lambda.atoms t)

@[simp]

theorem CatCrypt.Nominal.Lambda.atoms_var (a : Atom) : atoms (Raw.var a) = {a}

@[simp]

theorem CatCrypt.Nominal.Lambda.atoms_app (s t : Raw) : atoms (s.app t) = atoms s ∪ atoms t

@[simp]

theorem CatCrypt.Nominal.Lambda.atoms_lam (a : Atom) (t : Raw) : atoms (Raw.lam a t) = insert a (atoms t)

theorem CatCrypt.Nominal.Lambda.atoms_smul (π : FinPerm) (t : Raw) : atoms (π • t) = Finset.image (fun (x : Atom) => π.apply x) (atoms t)

theorem CatCrypt.Nominal.Lambda.smul_eq_of_atoms_fixed {π : FinPerm} {t : Raw} (h : ∀ a ∈ atoms t, π.apply a = a) : π • t = t

If a permutation fixes every atom of t, it fixes t.

@[instance_reducible]

instance CatCrypt.Nominal.Lambda.instNomSetRaw : NomSet Raw

Equations

• CatCrypt.Nominal.Lambda.instNomSetRaw = { toMulAction := CatCrypt.Nominal.Lambda.instMulActionFinPermRaw, supp := CatCrypt.Nominal.Lambda.atoms, supp_supports := ⋯, supp_equivariant := ⋯ }

@[simp]

theorem CatCrypt.Nominal.Lambda.supp_raw (t : Raw) : NomSet.supp t = atoms t

Free variables

def CatCrypt.Nominal.Lambda.fv : Raw → Finset Atom

The free variables of a term (lam binds).

Equations

• CatCrypt.Nominal.Lambda.fv (CatCrypt.Nominal.Lambda.Raw.var a) = {a}
• CatCrypt.Nominal.Lambda.fv (s.app t) = CatCrypt.Nominal.Lambda.fv s ∪ CatCrypt.Nominal.Lambda.fv t
• CatCrypt.Nominal.Lambda.fv (CatCrypt.Nominal.Lambda.Raw.lam a t) = CatCrypt.Nominal.Lambda.fv t \ {a}

@[simp]

theorem CatCrypt.Nominal.Lambda.fv_var (a : Atom) : fv (Raw.var a) = {a}

@[simp]

theorem CatCrypt.Nominal.Lambda.fv_app (s t : Raw) : fv (s.app t) = fv s ∪ fv t

@[simp]

theorem CatCrypt.Nominal.Lambda.fv_lam (a : Atom) (t : Raw) : fv (Raw.lam a t) = fv t \ {a}

theorem CatCrypt.Nominal.Lambda.fv_subset_atoms (t : Raw) : fv t ⊆ atoms t

theorem CatCrypt.Nominal.Lambda.fv_smul (π : FinPerm) (t : Raw) : fv (π • t) = Finset.image (fun (x : Atom) => π.apply x) (fv t)

α-equivalence (generated congruence) and the quotient

AEq is the least congruence identifying lam a t with lam b (swap a b • t) for a fresh b. Taking refl/symm/trans as constructors makes it an equivalence relation by construction — no hand proof of α-transitivity.

inductive CatCrypt.Nominal.Lambda.AEq : Raw → Raw → Prop

α-equivalence of raw terms.

• rfl (t : Raw) : AEq t t
• symm {s t : Raw} : AEq s t → AEq t s
• trans {s t u : Raw} : AEq s t → AEq t u → AEq s u
• app {s s' t t' : Raw} : AEq s s' → AEq t t' → AEq (s.app t) (s'.app t')
• lam {a : Atom} {s t : Raw} : AEq s t → AEq (Raw.lam a s) (Raw.lam a t)
• rename (a b : Atom) (t : Raw) (h : b ∉ atoms t) : AEq (Raw.lam a t) (Raw.lam b (FinPerm.swap a b • t))

theorem CatCrypt.Nominal.Lambda.AEq.equivalence : Equivalence AEq

theorem CatCrypt.Nominal.Lambda.aeq_smul (π : FinPerm) {s t : Raw} (h : AEq s t) : AEq (π • s) (π • t)

α-equivalence is equivariant.

theorem CatCrypt.Nominal.Lambda.aeq_fv {s t : Raw} (h : AEq s t) : fv s = fv t

α-equivalent terms have the same free variables.

The nominal term type Tm := Raw / α

def CatCrypt.Nominal.Lambda.aeqSetoid : Setoid Raw

The α-equivalence setoid.

Equations

• CatCrypt.Nominal.Lambda.aeqSetoid = { r := CatCrypt.Nominal.Lambda.AEq, iseqv := CatCrypt.Nominal.Lambda.AEq.equivalence }

def CatCrypt.Nominal.Lambda.Tm : Type

Nominal λ-terms: raw terms up to α-equivalence.

Equations

• CatCrypt.Nominal.Lambda.Tm = Quotient CatCrypt.Nominal.Lambda.aeqSetoid

def CatCrypt.Nominal.Lambda.Tm.mk (t : Raw) : Tm

The class of a raw term.

Equations

• CatCrypt.Nominal.Lambda.Tm.mk t = ⟦t⟧

theorem CatCrypt.Nominal.Lambda.Tm.mk_eq {s t : Raw} (h : AEq s t) : mk s = mk t

theorem CatCrypt.Nominal.Lambda.Tm.ind {motive : Tm → Prop} (h : ∀ (t : Raw), motive (mk t)) (q : Tm) : motive q

@[instance_reducible]

instance CatCrypt.Nominal.Lambda.instMulActionFinPermTm : MulAction FinPerm Tm

The permutation action descends to the quotient.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CatCrypt.Nominal.Lambda.Tm.smul_mk (π : FinPerm) (t : Raw) : π • mk t = mk (π • t)

def CatCrypt.Nominal.Lambda.Tm.freeVars : Tm → Finset Atom

Free variables, descended to the quotient (α-invariant).

Equations

• CatCrypt.Nominal.Lambda.Tm.freeVars = Quotient.lift CatCrypt.Nominal.Lambda.fv ⋯

@[simp]

theorem CatCrypt.Nominal.Lambda.Tm.freeVars_mk (t : Raw) : (mk t).freeVars = fv t

Constructors on Tm, and α-correctness of lam

def CatCrypt.Nominal.Lambda.Tm.var (a : Atom) : Tm

Variable.

Equations

• CatCrypt.Nominal.Lambda.Tm.var a = CatCrypt.Nominal.Lambda.Tm.mk (CatCrypt.Nominal.Lambda.Raw.var a)

def CatCrypt.Nominal.Lambda.Tm.app : Tm → Tm → Tm

Application.

Equations

• CatCrypt.Nominal.Lambda.Tm.app = Quotient.lift₂ (fun (s t : CatCrypt.Nominal.Lambda.Raw) => CatCrypt.Nominal.Lambda.Tm.mk (s.app t)) CatCrypt.Nominal.Lambda.Tm.app._proof_1

def CatCrypt.Nominal.Lambda.Tm.lam (a : Atom) : Tm → Tm

Abstraction (binding).

Equations

• CatCrypt.Nominal.Lambda.Tm.lam a = Quotient.lift (fun (t : CatCrypt.Nominal.Lambda.Raw) => CatCrypt.Nominal.Lambda.Tm.mk (CatCrypt.Nominal.Lambda.Raw.lam a t)) ⋯

@[simp]

theorem CatCrypt.Nominal.Lambda.Tm.lam_mk (a : Atom) (t : Raw) : lam a (mk t) = mk (Raw.lam a t)

theorem CatCrypt.Nominal.Lambda.Tm.lam_rename (a b : Atom) (t : Raw) (h : b ∉ atoms t) : lam a (mk t) = lam b (mk (FinPerm.swap a b • t))

α-correctness of lam: lam a t = lam b (swap a b • t) for fresh b, an equality of terms — the defining property of a nominal binder.

Support minimality: Tm is a nominal set with supp = fv

The nontrivial half: a permutation fixing the free variables of a term acts α-trivially on it.

theorem CatCrypt.Nominal.Lambda.aeq_of_fixes_fv {t : Raw} {π : FinPerm} : (∀ a ∈ fv t, π.apply a = a) → AEq (π • t) t

A permutation fixing every free variable of t fixes t up to α.

@[instance_reducible]

noncomputable instance CatCrypt.Nominal.Lambda.instNomSetTm : NomSet Tm

Tm is a nominal set over Atom/FinPerm, with support the free variables.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CatCrypt.Nominal.Lambda.Tm.supp_mk (t : Raw) : NomSet.supp (mk t) = fv t