Notes on Universal Algebra
This note is about universal algebra based on Chapter 3 of John Mitchell’s book Foundations for Programming Languages.
1 Algebras, Signatures, and Terms
An algebra consist one or more sets (carriers), a collection of distinguished elements, and a collection of first-order (algebraic) functions over the carriers of the algebra.
Example: \langle \N, 0, 1, +, * \rangle is an algebra over natural numbers.
1.1 Syntax of Algebraic Terms
Definition (Signature): A signature \Sigma = \langle S, F \rangle consists of
A set S that contains sorts (basic type symbols),
A collection F of pairs \langle f, s_1 \times \dots \times s_k \to s \rangle, where s_1 \dots s_k, s \in S and f is distinct.
A symbol f : s is called a constant symbol.
Example: A signature for the aforementioned algebra over natural number is \Sigma_{\mathcal{N}} = \langle \{ \mathit{nat} \}, F \rangle, where F contains 0, 1: \mathit{nat} and +, *: \mathit{nat} \times \mathit{nat} \to \mathit{nat}.
Definition (Sort Assignment): A sort assignment is a finite set of \langle var \rangle : \langle sort \rangle pairs \Gamma = \{ x_1 : s_1, \dots, x_k : s_k \}.
Definition (Set of Algebraic Terms): Given a signature \Sigma and sort assignment \Gamma, we define the set \mathit{Term}^{s}(\Sigma, \Gamma) of algebraic terms of sort s over \Sigma and \Gamma:
\dfrac{ x : s \in \Gamma }{ x \in \mathit{Term}^{s}(\Sigma, \Gamma) } \dfrac{ \begin{array}{c} f : s_1 \times \dots \times s_k \to s \\ M_i \in \mathit{Term}^{s_i}(\Sigma, \Gamma) \text{ for } i = 1, \dots, k \end{array} }{ f M_1 \dots M_2 \in \mathit{Term}^{s}(\Sigma, \Gamma) }
A substitution [N/x]M replaces all occurrences of x with N in M.
Lemma: If M \in \mathit{Term}^{s}(\Sigma, \Gamma, x : s{}’), and N \in \mathit{Term}^{s{}’}(\Sigma, \Gamma), then [N/x]M \in \mathit{Term}^{s}(\Sigma, \Gamma).
1.2 Interpretation of Algebraic Terms
Algebras are mathematical structures that provide meaning (denotation semantics) for algebraic terms.
Definition (Algebra): If \Sigma is a signature, then a \Sigma-algebra \mathcal{A} consists of
\{ A^s \}_{s \in S}, that is, one carrier A^{s} for each sort symbol s \in S,
an interpretation map \mathcal{I} assigning a function \mathcal{I}(f): A^{s_1} \times \dots A^{s_k} \to A^{s} to each proper function symbol f : s_1 \times \dots s_k \to s \in F and an element \mathcal{I}(f) : A^{s} to each constant symbol f : s \in F. \mathcal{I}(f) is also written as f^{\mathcal{A}}.
If \Sigma has only one sort, then \Sigma-algebra is single-sorted, otherwise it is many-sorted or multi-sorted.
Definition (Environment): An environment \eta : \mathcal{V} \to \cup_s A^s for algebra \mathcal{A} is a mapping from variables to elements of the carriers of \mathcal{A}.
We say an enviornment \eta satisfies \Gamma if \forall x : s \in \Gamma, \eta(x) \in A^s.
Definition (Meaning of Syntactic Terms): Given an environment \eta for \mathcal{A} that satisfies \Gamma, we define the meaning \mathcal{A}⟦M⟧\eta for term M \in \mathit{Term}^{s}(\Sigma, \Gamma):
\mathcal{A}⟦x⟧\eta = \eta(x)
\mathcal{A}⟦f ~ M_1 \dots M_k⟧\eta = f^{\mathcal{A}}( \mathcal{A}⟦M_1⟧\eta \dots \mathcal{A}⟦M_k⟧\eta )
Some properties informally: (1) the meaning of a term M \in \mathit{Term}^{s}(\Sigma, \Gamma) is an element of the appropriate carrier A^s. (2) If two environments \eta_1 and \eta_2 are equal for all variables, then the meanings ⟦M⟧\eta_1 and ⟦M⟧\eta_2 are equal.
1.3 Substitution Lemma
Informally, the lemma states that substituing a term N for a variable x in term M has the same effect on the meaning of M as changing the environment so that the value of x is the value of N.
Lemma (Substitution): Let M \in \mathit{Term}^{s}(\Sigma, (\Gamma, x : s{}’)) and N \in \mathit{Term}^{s{}’}(\Sigma, \Gamma), so that [N/x]M \in \mathit{Term}^{s}(\Sigma, \Gamma). Then for any environment \eta, we have ⟦ [N/x]M ⟧\eta = ⟦M⟧(\eta[x \mapsto ⟦N⟧\eta]).