Term evaluation

Remarks

The recursion is well defined because every term has a unique reading. The value depends only on the values of $\alpha$ at the variables that occur in $t$. If these variables are among $x_1, \ldots, x_n$ and $\alpha(x_i) = a_i$, one writes $t^A(a_1, \ldots, a_n)$.

Example: in the ring $(\Z, +, \cdot, 0, 1)$, let $t = x \cdot (y + 1)$ and $\alpha(x) = 3$, $\alpha(y) = 4$. Clause 1 gives $x \mapsto 3$ and $y \mapsto 4$, clause 2 gives $1 \mapsto 1$, and clause 3 twice gives $y + 1 \mapsto 5$ and $t \mapsto 15$.

Non-example: computing $x \cdot (y + 1)$ at the same assignment as $3 \cdot 4 + 1 = 13$ is not term evaluation. The outermost symbol of $t$ is $\cdot$ applied to $x$ and $y + 1$, so clause 3 requires the product of the values $3$ and $5$.

Homomorphisms commute with evaluation: if $h \colon A \to B$ is a homomorphism, then $h(t^A[\alpha]) = t^B[h \circ \alpha]$. In Mathlib term evaluation is FirstOrder.Language.Term.realize.