Lawvere Theory

definition theorem example program

A Lawvere theory is an algebraic theory presented as a category. It is a small category $\mathcal{L}$ with finite products whose objects are the natural numbers $0,1,2,\dots$, with $n$ the $n$-fold product of $1$, together with an identity-on-objects, product-preserving functor from ${\mathbb{N}}^{\mathrm{op}}$ (finite sets and functions, opposite). A morphism $n\to m$ is an $m$-tuple of terms in $n$ variables, modulo the equations of the theory, and composition is substitution. A model of $\mathcal{L}$ in a category $\mathcal{C}$ with finite products is a product-preserving functor $M:\mathcal{L}\to \mathcal{C}$: it sends $1$ to a carrier $M(1)$, $n$ to $M(1{)}^n$, and each term to the function it denotes. Homomorphisms of models are natural transformations.

For the theory of monoids, $\mathcal{L}(n,1)$ is the set of words in $n$ letters; for commutative monoids it is ${\mathbb{N}}^n$, so $\mathcal{L}(n,m)$ is the set of $m\times n$ matrices over $\mathbb{N}$ and composition is matrix multiplication. A model in $\mathbf{Set}$ is exactly a commutative monoid.

Sources: Lawvere, Functorial Semantics of Algebraic Theories, PhD thesis, Columbia 1963 (reprinted in Reprints in Theory Appl. Categ. 5, 2004); Hyland & Power, The category theoretic understanding of universal algebra: Lawvere theories and monads, ENTCS 172 (2007); Adámek, Rosický & Vitale, Algebraic Theories (CUP 2011); Castellan, Clairambault & Dybjer arXiv:1904.00827 (notes) Definitions 5–7, Theorems 1–2 (contextual unityped cwfs ≃ cartesian operads ≃ Lawvere theories); Gambino & Kock arXiv:0906.4931 (notes) §1.24; Schultz et al. arXiv:1602.03501 (notes) Definition 3.1 (the multi-sorted version). See Functorial Semantics for Lawvere’s general programme.

Theories versus presentations

A presentation $(\Sigma ,E)$ — operation symbols with arities, and equations — is syntax; the Lawvere theory is what it presents: $\mathcal{L}(n,1)=T(\Sigma ,\{x_1,\dots ,x_n\})/{\equiv }_E$, terms modulo the Congruence generated by $E$. Different presentations of the same theory (groups with $\cdot {,}^{-1},e$, or with division alone) give isomorphic Lawvere theories, which is the point: the theory is presentation-independent, and a model is defined without choosing generators. Deciding whether two terms are equal in $\mathcal{L}$ is the word problem of the presentation — decidable by an E-Graph for ground equations, undecidable in general.

Lawvere theories and monads

Every Lawvere theory $\mathcal{L}$ determines a finitary monad $T$ on $\mathbf{Set}$: $T(X)$ is the free model on $X$ (terms over $X$ modulo the equations), and models of $\mathcal{L}$ are the Eilenberg–Moore algebras of $T$. Conversely $\mathcal{L}(n,m)={\mathrm{Kl}}_T(m,n)$ — the theory is (the opposite of) the Kleisli Category of the monad restricted to finite sets. This equivalence between finitary monads and Lawvere theories (Linton) is the basis of algebraic effects: an effect is presented by operations and equations (a theory), and the monad is derived.

The same idea, three more times

structure	a morphism is	models are
Lawvere theory	tuple of terms; composition by substitution	algebras in a cartesian category
contextual unityped cwf / cartesian operad	the same, read type-theoretically	— (Castellan et al., Theorems 1–2: the three are equivalent)
PROP (Prop)	a morphism $n\to m$ in a symmetric monoidal category, no copying/discarding built in	algebras in a monoidal category: linear theories
polynomial monad (Polynomial Functor)	trees of operations	algebras of the monad

Lawvere theories allow terms to copy and discard variables (because the category is cartesian); PROPs do not, which is why PROPs present linear and quantum theories and Lawvere theories present classical algebra. The multi-sorted version — objects are lists of sorts — is the type side of an Algebraic Database and the signature of a typed IR.

Sophia

A Sophia frontend is, at the level of signatures, a morphism of theories: it sends each operation of a source language to a term of the Core Calculus, and must respect equations. Machine primitives are operations of a multi-sorted theory whose sorts are i64, f64, … and whose equations differ per attribute (add.wrap is associative, add.nsw is not total). See Core Calculus and Cross-Language Semantic Hazards.

JuliaLean

Docs: plain Julia — Catlab has no dedicated API for this; related: Theories (Catlab) · GATlab standard library

using Random; Random.seed!(1)
# The Lawvere theory of commutative monoids: objects n ∈ ℕ, a morphism n → m is an m×n matrix over ℕ
# (row i = the term x₁^{a_i1} ⋯ x_n^{a_in}, written multiplicatively), composition = matrix product = substitution.
A = rand(0:2, 3, 2)          # 2 → 3: three terms in two variables
B = rand(0:2, 1, 3)          # 3 → 1: one term in three variables
B * A                        # 2 → 1: substitute the three terms of A into B
# A model is a product-preserving functor: a commutative monoid M, with n ↦ Mⁿ and a matrix acting on tuples.
additive(F) = x -> F * x                                   # model (ℤ, +, 0): row i ↦ Σ_j a_ij x_j
multiplicative(F) = x -> [prod(x .^ F[i, :]) for i in 1:size(F, 1)]   # model (ℝ>0, ·, 1): row i ↦ Π_j x_j^{a_ij}
x = [2, 5]; y = [2.0, 0.5]
additive(B * A)(x) == additive(B)(additive(A)(x))          # true: functoriality = associativity
multiplicative(B * A)(y) ≈ multiplicative(B)(multiplicative(A)(y))   # true: the same theory, another model
# identities and projections: the theory has finite products, πᵢ = rows of the identity matrix
π2 = [0 1]; additive(π2)(x) == [x[2]]                      # true

import Mathlib
-- The Lawvere theory of commutative monoids is the category of ℕ-matrices: composition (substitution)
-- is matrix multiplication, and its associativity is functoriality of every model.
example (A : Matrix (Fin 3) (Fin 2) ℕ) (B : Matrix (Fin 1) (Fin 3) ℕ) (C : Matrix (Fin 2) (Fin 4) ℕ) :
    B * (A * C) = (B * A) * C :=
  (Matrix.mul_assoc B A C).symm
 
-- the model (ℤ, +): a morphism acts on tuples by mulVec, and this is functorial
example (A : Matrix (Fin 3) (Fin 2) ℤ) (B : Matrix (Fin 1) (Fin 3) ℤ) (x : Fin 2 → ℤ) :
    (B * A).mulVec x = B.mulVec (A.mulVec x) :=
  (Matrix.mulVec_mulVec x B A).symm