The free many-sorted algebra $\mathbf{T}_\Sigma(X)$

Definition

MSKleene_Term

by Cosme · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

formal-languagesmany-sorted-algebratree-automatauniversal-algebra

The free $\Sigma$ -algebra $\mathbf{T}_\Sigma(X)$ on an $S$ -sorted set of variables $X$ (Definitions 3.1, 3.2), represented by the mutual inductive Term / TermVec: a term is a variable var x or an operation symbol applied to a vector of subterms of the matching arity, app σ ts (a constant is app σ .nil).

The file provides the algebra structure freeAlgebra (carrier Term sig X, operations app), the insertion of generators eta ( $\eta^X$ ), the evaluation Term.eval of a term in an arbitrary $\Sigma$ -algebra A under an assignment ρ : X → A, and the induced homomorphism evalHom with evalHom_eta : evalHom A ρ ∘ η^X = ρ. This is the existence half of the universal property of $\mathbf{T}_\Sigma(X)$ (Proposition 3.5).

Formalization Note TermVec sig X w is a heterogeneous list holding one subterm of sort w[i] per argument position; ofArgs / toArgs convert between it and the nested-product Args.

Definition code

/-
The free many-sorted `Σ`-algebra `T_Σ(X)` (Definitions 3.1, 3.2) as an
inductive family of terms, together with:
  * its `Algebra` structure (`freeAlgebra`);
  * the insertion of generators `η^X`;
  * evaluation of a term into any `Σ`-algebra under an assignment, and the
    induced homomorphism (the existence half of the universal property, Prop. 3.5).

Terms are represented by the mutual inductive `Term` / `TermVec`, the standard
encoding of many-sorted terms: `TermVec sig X w` is a heterogeneous list holding
one subterm of sort `w[i]` per argument position.
-/
import Definitions.Def_MSKleene_Core

namespace MSKleene

universe u

variable {S : Type u}

-- Many-sorted terms over signature `sig` with variables in `X`:
-- `var` injects a variable; `app` applies an operation symbol to a vector of
-- subterms of the matching arity (a constant is `app σ .nil`).
-- `TermVec sig X w` is a heterogeneous list holding one subterm of sort `w[i]`
-- per argument position.
mutual
inductive Term (sig : Signature S) (X : SSet S) : S → Type u where
  | var {s : S} : X s → Term sig X s
  | app {w : List S} {s : S} : sig w s → TermVec sig X w → Term sig X s
inductive TermVec (sig : Signature S) (X : SSet S) : List S → Type u where
  | nil : TermVec sig X []
  | cons {s : S} {w : List S} : Term sig X s → TermVec sig X w → TermVec sig X (s :: w)
end

/-- Convert an `Args` tuple of terms into a `TermVec`. -/
def TermVec.ofArgs {sig : Signature S} {X : SSet S} :
    {w : List S} → Args (Term sig X) w → TermVec sig X w
  | [], _ => .nil
  | _ :: _, (t, rest) => .cons t (TermVec.ofArgs rest)

/-- Convert a `TermVec` back into an `Args` tuple of terms. -/
def TermVec.toArgs {sig : Signature S} {X : SSet S} :
    {w : List S} → TermVec sig X w → Args (Term sig X) w
  | [], _ => PUnit.unit
  | _ :: _, .cons t rest => (t, TermVec.toArgs rest)

/-- The free `Σ`-algebra `T_Σ(X)`: carrier `Term sig X`, operations `app`
(Definition 3.2). -/
def freeAlgebra (sig : Signature S) (X : SSet S) : Algebra sig where
  carrier := Term sig X
  op := fun σ args => Term.app σ (TermVec.ofArgs args)

/-- Insertion of the generators, `η^X : X → T_Σ(X)` (Proposition 3.5). -/
def eta (sig : Signature S) (X : SSet S) : SMap X (freeAlgebra sig X).carrier :=
  fun _ x => Term.var x

-- Evaluate a term in the algebra `A` under the assignment `ρ : X → A`.
-- Together with `evalArgs` this is the unique-extension map of Proposition 3.5.
mutual
def Term.eval {sig : Signature S} {X : SSet S} (A : Algebra sig)
    (ρ : SMap X A.carrier) : {s : S} → Term sig X s → A.carrier s
  | _, .var x => ρ _ x
  | _, .app σ ts => A.op σ (TermVec.evalArgs A ρ ts)
def TermVec.evalArgs {sig : Signature S} {X : SSet S} (A : Algebra sig)
    (ρ : SMap X A.carrier) : {w : List S} → TermVec sig X w → Args A.carrier w
  | [], _ => PUnit.unit
  | _ :: _, .cons t ts => (Term.eval A ρ t, TermVec.evalArgs A ρ ts)
end

theorem TermVec.evalArgs_ofArgs {sig : Signature S} {X : SSet S} (A : Algebra sig)
    (ρ : SMap X A.carrier) :
    ∀ {w : List S} (args : Args (Term sig X) w),
      TermVec.evalArgs A ρ (TermVec.ofArgs args)
        = Args.map (fun s (t : Term sig X s) => Term.eval A ρ t) args
  | [], _ => rfl
  | _ :: _, (t, rest) => congrArg (Prod.mk (Term.eval A ρ t))
      (TermVec.evalArgs_ofArgs A ρ rest)

/-- The homomorphism `ρ^♯ : T_Σ(X) → A` induced by an assignment `ρ`
(the existence half of Proposition 3.5). -/
def evalHom {sig : Signature S} {X : SSet S} (A : Algebra sig)
    (ρ : SMap X A.carrier) : Hom (freeAlgebra sig X) A where
  toFun := fun _ t => Term.eval A ρ t
  map_op := by
    intro w s σ args
    show Term.eval A ρ (Term.app σ (TermVec.ofArgs args)) = _
    show A.op σ (TermVec.evalArgs A ρ (TermVec.ofArgs args)) = _
    exact congrArg (A.op σ) (TermVec.evalArgs_ofArgs A ρ args)

/-- `ρ^♯ ∘ η^X = ρ`: the induced homomorphism restricts to `ρ` on generators. -/
theorem evalHom_eta {sig : Signature S} {X : SSet S} (A : Algebra sig)
    (ρ : SMap X A.carrier) (s : S) (x : X s) :
    (evalHom A ρ).toFun s (eta sig X s x) = ρ s x := rfl

end MSKleene

Source

Gong, Ruiz Mora, Sanmartín Vich, Cosme Llópez, "A Kleene theorem for free many-sorted algebras", 2026, https://arxiv.org/abs/1808.08217 (predecessor CVCL20)

Read-back

What the Lean code literally says, in plain math · claude-sonnet-5

`Term` and `TermVec` (mutually inductive families)

Throughout, $S$ is an implicit type of sorts. Fixed as explicit parameters are a signature $sig$ over $S$ — a rule assigning to each pair consisting of a word $w \in \mathrm{List}\,S$ and a sort $s \in S$ a type $sig\,w\,s$ , thought of as the operation symbols of argument profile $w$ and result sort $s$ — and a sort-indexed family of variable types $X$ , assigning to each sort $s$ a type $X_s$ . The declaration introduces, simultaneously, two inductive families valued in $\mathrm{Type}$ :

$\mathrm{Term}\,sig\,X : S \to \mathrm{Type}$ , where $\mathrm{Term}\,sig\,X\,s$ is meant to be the terms of sort $s$ ;
$\mathrm{TermVec}\,sig\,X : \mathrm{List}\,S \to \mathrm{Type}$ , where $\mathrm{TermVec}\,sig\,X\,w$ is meant to be the finite sequences of terms whose sorts are exactly the entries of $w$ , in order.

$\mathrm{Term}$ has two constructors. The constructor $\mathrm{var}$ takes an implicit sort $s$ and an element $x : X_s$ and returns $\mathrm{var}\,x : \mathrm{Term}\,sig\,X\,s$ . The constructor $\mathrm{app}$ takes an implicit word $w$ , an implicit sort $s$ , an operation symbol $\sigma : sig\,w\,s$ , and a term-vector $ts : \mathrm{TermVec}\,sig\,X\,w$ , and returns $\mathrm{app}\,\sigma\,ts : \mathrm{Term}\,sig\,X\,s$ . $\mathrm{TermVec}$ has two constructors: $\mathrm{nil} : \mathrm{TermVec}\,sig\,X\,[\,]$ , and $\mathrm{cons}$ , which takes an implicit sort $s$ , an implicit word $w$ , a term $t : \mathrm{Term}\,sig\,X\,s$ and a vector $ts : \mathrm{TermVec}\,sig\,X\,w$ , and returns $\mathrm{cons}\,t\,ts : \mathrm{TermVec}\,sig\,X\,(s :: w)$ , where $s :: w$ is the list with head $s$ and tail $w$ . Being inductive, $\mathrm{Term}\,sig\,X$ and $\mathrm{TermVec}\,sig\,X$ are the least families closed under these constructors: every element is built from finitely many applications of $\mathrm{var}$ , $\mathrm{app}$ , $\mathrm{nil}$ , $\mathrm{cons}$ . Nullary operation symbols $\sigma : sig\,[\,]\,s$ give constant terms $\mathrm{app}\,\sigma\,\mathrm{nil}$ . No finiteness or decidability hypothesis is imposed on $S$ , $sig$ , or $X$ ; if some $X_s$ is empty there are simply no $\mathrm{var}$ -terms of that sort.

`TermVec.ofArgs`

For implicit $sig$ , implicit $X$ , and implicit word $w$ , this defines a function

\mathrm{ofArgs} : \mathrm{Args}\,(\mathrm{Term}\,sig\,X)\,w \longrightarrow \mathrm{TermVec}\,sig\,X\,w .

Here $\mathrm{Args}\,B\,w$ is the iterated product type defined by recursion on $w$ : $\mathrm{Args}\,B\,[\,]$ is the one-element type $\mathrm{PUnit}$ , and $\mathrm{Args}\,B\,(s :: w) = B_s \times \mathrm{Args}\,B\,w$ ; so $\mathrm{Args}\,(\mathrm{Term}\,sig\,X)\,w$ is a tuple holding one term for each sort listed in $w$ (plus a trailing unit). The function is defined by recursion on $w$ : on the empty word, the unique input is sent to $\mathrm{nil}$ ; on $s :: w$ , an input which is a pair $(t, \mathit{rest})$ with $t : \mathrm{Term}\,sig\,X\,s$ and $\mathit{rest} : \mathrm{Args}\,(\mathrm{Term}\,sig\,X)\,w$ is sent to $\mathrm{cons}\,t\,(\mathrm{ofArgs}\,\mathit{rest})$ .

`TermVec.toArgs`

For implicit $sig$ , $X$ , and $w$ , this defines the reverse conversion

\mathrm{toArgs} : \mathrm{TermVec}\,sig\,X\,w \longrightarrow \mathrm{Args}\,(\mathrm{Term}\,sig\,X)\,w ,

by recursion on $w$ : on the empty word it returns the unique element of $\mathrm{PUnit}$ ; on $s :: w$ it matches an input of the form $\mathrm{cons}\,t\,\mathit{rest}$ and returns the pair $(t,\ \mathrm{toArgs}\,\mathit{rest})$ .

`freeAlgebra`

Given explicit parameters $sig$ and $X$ , this produces an element of $\mathrm{Algebra}\,sig$ . An $\mathrm{Algebra}\,sig$ is a structure consisting of a carrier family $|A| : S \to \mathrm{Type}$ together with an operation map that, for implicit $w$ and $s$ , takes an operation symbol $\sigma : sig\,w\,s$ and a tuple $\mathrm{Args}\,|A|\,w$ and returns an element of $|A|_s$ . For $\mathrm{freeAlgebra}\,sig\,X$ the carrier family is $\mathrm{Term}\,sig\,X$ itself, and the operation map sends $\sigma : sig\,w\,s$ and $args : \mathrm{Args}\,(\mathrm{Term}\,sig\,X)\,w$ to the term $\mathrm{app}\,\sigma\,(\mathrm{ofArgs}\,args) : \mathrm{Term}\,sig\,X\,s$ .

`eta`

Given explicit parameters $sig$ and $X$ , this produces an element of $\mathrm{SMap}\,X\,\big(|\mathrm{freeAlgebra}\,sig\,X|\big)$ , that is, a family of functions $\eta_s : X_s \to \mathrm{Term}\,sig\,X\,s$ (one for each sort $s$ ). The function ignores its sort argument in the sense that at every sort it is given by $x \mapsto \mathrm{var}\,x$ .

`Term.eval` and `TermVec.evalArgs` (mutually recursive)

Fix implicit $sig$ and $X$ , an explicit algebra $A : \mathrm{Algebra}\,sig$ , and an explicit assignment $\rho : \mathrm{SMap}\,X\,|A|$ , i.e. a family of functions $\rho_s : X_s \to |A|_s$ . This mutually defines two total functions.

$\mathrm{Term.eval}\,A\,\rho$ takes an implicit sort $s$ and a term of $\mathrm{Term}\,sig\,X\,s$ and returns an element of $|A|_s$ , by structural recursion:

\mathrm{eval}\,(\mathrm{var}\,x) = \rho_s\,x, \qquad \mathrm{eval}\,(\mathrm{app}\,\sigma\,ts) = A.\mathrm{op}\,\sigma\,\big(\mathrm{evalArgs}\,A\,\rho\,ts\big).

$\mathrm{TermVec.evalArgs}\,A\,\rho$ takes an implicit word $w$ and a vector of $\mathrm{TermVec}\,sig\,X\,w$ and returns an element of $\mathrm{Args}\,|A|\,w$ , by recursion on $w$ : the empty vector is sent to the unique element of $\mathrm{PUnit}$ ; a vector $\mathrm{cons}\,t\,ts$ is sent to the pair $\big(\mathrm{Term.eval}\,A\,\rho\,t,\ \mathrm{TermVec.evalArgs}\,A\,\rho\,ts\big)$ .

`TermVec.evalArgs_ofArgs`

For all implicit $sig$ and $X$ , every algebra $A : \mathrm{Algebra}\,sig$ , every assignment $\rho : \mathrm{SMap}\,X\,|A|$ , every implicit word $w : \mathrm{List}\,S$ , and every tuple $args : \mathrm{Args}\,(\mathrm{Term}\,sig\,X)\,w$ , the following equality of elements of $\mathrm{Args}\,|A|\,w$ holds:

\mathrm{TermVec.evalArgs}\,A\,\rho\,\big(\mathrm{TermVec.ofArgs}\,args\big) \;=\; \mathrm{Args.map}\,\big(\lambda\,s\ \lambda\,t.\ \mathrm{Term.eval}\,A\,\rho\,t\big)\,args ,

where $\mathrm{Args.map}\,f$ applies the sort-indexed function $f$ componentwise to every entry of a tuple. In words: converting $args$ into a term-vector and then evaluating that vector yields the same tuple as evaluating each component term of $args$ individually.

`evalHom`

For implicit $sig$ and $X$ , an explicit algebra $A : \mathrm{Algebra}\,sig$ and an explicit assignment $\rho : \mathrm{SMap}\,X\,|A|$ , this produces an element of $\mathrm{Hom}\,(\mathrm{freeAlgebra}\,sig\,X)\,A$ . A $\mathrm{Hom}\,B\,C$ is a structure bundling a sorted map $\mathrm{toFun} : \mathrm{SMap}\,|B|\,|C|$ together with a proof that it commutes with every operation. For $\mathrm{evalHom}\,A\,\rho$ , the map $\mathrm{toFun}$ is, at every sort, $t \mapsto \mathrm{Term.eval}\,A\,\rho\,t$ , and the bundled proof asserts that for all implicit $w$ , $s$ , every operation symbol $\sigma : sig\,w\,s$ and every $args : \mathrm{Args}\,(\mathrm{Term}\,sig\,X)\,w$ ,

\mathrm{Term.eval}\,A\,\rho\,\big(\mathrm{app}\,\sigma\,(\mathrm{ofArgs}\,args)\big) \;=\; A.\mathrm{op}\,\sigma\,\big(\mathrm{Args.map}\,(\lambda\,s\ \lambda\,t.\ \mathrm{Term.eval}\,A\,\rho\,t)\,args\big),

i.e. that applying the evaluation map to the free algebra's interpretation of $\sigma$ agrees with $A$ 's interpretation of $\sigma$ applied to the pointwise-evaluated arguments.

`evalHom_eta`

For all implicit $sig$ and $X$ , every algebra $A : \mathrm{Algebra}\,sig$ , every assignment $\rho : \mathrm{SMap}\,X\,|A|$ , every sort $s : S$ , and every variable $x : X_s$ , the following holds:

(\mathrm{evalHom}\,A\,\rho).\mathrm{toFun}\,s\,\big(\mathrm{eta}\,sig\,X\,s\,x\big) \;=\; \rho\,s\,x .

Unfolding the definitions, $\mathrm{eta}\,sig\,X\,s\,x$ is $\mathrm{var}\,x$ and the underlying map of $\mathrm{evalHom}\,A\,\rho$ is $\mathrm{Term.eval}\,A\,\rho$ , so this states $\mathrm{Term.eval}\,A\,\rho\,(\mathrm{var}\,x) = \rho_s\,x$ . It is asserted to hold by reflexivity, i.e. definitionally.

Human review

Endorsed by Shuze Chen · Sep 9, 2026
Endorsed by Cosme · Sep 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The free many-sorted algebra TΣ(X)\mathbf{T}_\Sigma(X)TΣ​(X)

Term and TermVec (mutually inductive families)

TermVec.ofArgs

TermVec.toArgs

freeAlgebra

eta

Term.eval and TermVec.evalArgs (mutually recursive)

TermVec.evalArgs_ofArgs

evalHom

evalHom_eta