4.3. Term algebras

Synonymous terms

Terms in different drafts D, E with the same variables, can be so compared by interpreting ≃ in their coproduct D ⊔_V E. Equivalently, for any morphisms f∈Mor_L,V(D,F), g∈Mor_L,V(E,F) to a functional draft F,

∀x∈D, ∀y∈E, x ≃ y ⇔ f(x) = g(y).

∀h∈Mor_L,V(D,E), ∀x,y∈D, h(x) ≃ x ∧ (x ≃ y ⇔ h(x) ≃ h(y))

Term algebras

1. An algebraic L-draft D where V_D = V;
2. An injective L-algebra D generated by V where V ∩ Im φ_D = ∅ (thus D\Im φ_D = V);
3. A final L-draft in the sense of variables-preserving morphisms Mor_L,V ;
4. An L-algebra with basis V in the category of L-algebras.

Proof of equivalence. Already 1. ⇔ 2. ⇒ (3. ∧ 4.).
Proof of 3. ⇒ 1. : any final L-draft D is

• Functional : ∃f∈Mor_L,V(⤓D, D), f ⚬ ≃⃗_D ∈ Mor_L,V(D, D) ∴ f ⚬ ≃⃗_D = Id_D ∴ Inj ≃⃗_D
• Serial : Mor_L,V(D∪(^LD\Dom D), D) ≠∅
• V_D = V because V is a draft.

• minimal : ∃f∈Mor_L(E, Min_LE), f ∈ End_L(E) = {Id_E} ∴ Min_LE = E
• injective : (F = ^LE ∧ φ_F = ^Lφ_E) ⇒ φ_E ⚬ ^Lφ_E = φ_E ⚬ φ_F ⇔ φ_E∈Mor_L(F,E)
  ∴ ∃f∈ Mor_L(E,F), φ_E⚬f ∈ End_L E = {Id_E} ∴ f⚬φ_E = φ_F⚬^Lf = ^L(φ_E⚬f) = Id_F.∎

Term algebras in injective algebras

For any f∈Mor_L(K,E) from a ground draft K to an injective system E, the system Im f is both injective and minimal, i.e. a ground draft. As with any morphism, if K is serial then Im f is serial; if E is functional then Im f is functional. Thus, if K is a ground term algebra and E is an injective partial algebra then Im f is a ground term algebra, and thus f is injective (by essential uniqueness of initial or final objects).

• If K is a serial minimal system and E is an injective partial algebra then Im f is a ground term algebra;
• If K is a functional ground draft and E is injective then f is injective (because ∼_f ⊂ f_⋆(≃_{Im f}) = ≃_K = 𝛿_K).

Particular languages

Trajectories by transformation sets

∀x∈E, 〈{x}〉_L = {f(x)|f∈〈L〉_{Id,⚬}}
∀X⊂E, 〈X〉_L = ⋃_{f∈〈L〉{Id,⚬}} f[X] = ⋃_x∈X 〈{x}〉_L

Id_E ∈ M ∴ X⊂K
∀g∈L, ∀y∈K, ∃(f,x)∈M×X, y = f(x) ∧ g⚬f ∈ M ∴ g(y) = g⚬f(x) ∈ K
K ∈ Sub_L E

L ⊂ {f∈E^E| A ∈ Sub_{f}E} = End_{A}E ∈ Sub_{Id,⚬}E^E
M ⊂ End_{A}E
∀f∈M, X ⊂ A ∈ Sub_{f}E ∴ f[X] ⊂ A. ∎

Free monoids

Any unary term L-algebra M (if it exists) is an egg in the category of L-algebras, thus (as seen in 3.11) a monoid acting on all L-algebras with Mor_L ⊂ Mor_M.

If L is a language of function symbols and M is a unary term L-algebra then L is a basis of M in the category of monoids.
Proof:

Let us confuse every s∈L with its copy s_M(e) ∈ M.
By the representation theorem, any monoid N is isomorphic to a transformation monoid N ⊂ X^X (by taking X = N and reading composition as left action).
Any u∈N^L makes X an L-algebra, thus defines an action f ∈ Mor_{e,•}(M,X^X) ∧ f_|L = u.
Such an f is unique because L is a generating subset of the monoid M identified as a submonoid of the transformation monoid M^M:
〈L〉_{e,•} = {s•e | s∈〈L〉_{e,•}} = {g(e) | g∈〈{s_M|s∈L}〉_{Id,⚬}} = 〈{e}〉_L = M.
Finally Im f = f[〈L〉_{e,•}] ⊂ 〈Im u〉_{Id,⚬} ⊂ N.∎

Any L-algebra structure on any set E is uniquely extensible as an M-set structure. Thus Mor_M ⊂ Mor_L, and (M, e) is an egg in the category with M-morphisms on the class of L-algebras. Thus
∀x∈E, h_x ∈ Mor_M(M,X) ⊂ Mor_L(M,X) ∧ h_x(e) = x.
To conclude that (M, e) is also an egg in the category of L-algebras, we deduce uniqueness from
〈{e}〉_L = 〈L〉_{Id,•} = M. ∎

This view of free monoids as unary term algebras on languages of function symbols, can then be re-expressed saying they are made of all finite strings (i.e. tuples) of symbols from a given set, with concatenation in the role of composition. This can be easily understood after the definition of ℕ in 4.4, which is a particular case involved in the general construction.
The unique variables-preserving morphism from any {e,•}-draft to the free monoid with basis its set of variables, is the function of "syntactic simplification" which removes the occurrences of e and "removes all parenthesis", according respectively to the axioms of identity and associativity which define the category of monoids. Such morphisms from {e,•}-term algebras are surjective.

(Old French text)