Evaluation

2020 Mathematics Subject Classification: Primary: 68P05 [MSN][ZBL]

An interpretation $v^{\ast }:T(\mathrm{\Sigma },\mathrm{\varnothing })⟶A$ only defined on the ground terms $t\in T(\mathrm{\Sigma })$ of a signature $\mathrm{\Sigma }$ is called an evaluation. Since interpretations are $\mathrm{\Sigma }$-algebra-morphisms, evaluations are $\mathrm{\Sigma }$-algebra-morphisms as well. Furthermore, evaluations are uniquely determined, i.e. there exists exactly one mapping $e:T(\mathrm{\Sigma })⟶A$. This specific property has remarkable consequences. Consider for example a $\mathrm{\Sigma }$-algebra-morphism $f:A⟶B$ between $\mathrm{\Sigma }$-algebras $A$ and $B$. Then the equality $e_A=f\circ e_B$ holds for evaluations $e_A$ and $e_B$. In effect, each assignement can be extended to a functor between the term algebra $T(\mathrm{\Sigma })$ and $A$.

For reasons of simplicity, the application of the (uniquely determined) evaluation $e:T(\mathrm{\Sigma })⟶A$ to a term $t\in T(\mathrm{\Sigma })$ is often designated as $t^A:=e(t)$.

References[edit]