Assignement

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

An assignement is used for assigning specific values $a_1,\ldots,a_n$ to the free variables $X_1,\ldots,X_n\in V(t)$ of a term $t\in T(\Sigma,X)$ belonging to a signature $\Sigma=(S,F)$ and a set $X$ of variables. These values $a_1,\ldots,a_n$ are elements of a $\Sigma$-algebra $A$, whereby the sorts of $a_i$ and $X_i$ coincide in each case (i.e. $a_i\in s^A_i$ for $X_i\in X_{s_i}$ with $s_i\in S$). In this way, variables contained in the term $t$ can be eliminated and the overall 'value' of $t$ concretized. Formally, an assignement is a mapping $v\colon X\longrightarrow \bigcup_{s\in S} s^A$ with $v(x)\in s^A$ for $x\in X_s$, $s\in S$ [EM85]. The set of all assignements is typically designated as $B(A,X)$. An assignement is also called valuation.

For an assignement $v\in B(A,X)$ and for a value $a\in s^A$ the assignement changed at $x$ to $a$, designated as $v[x\leftarrow a]$, is defined as $$v[x\leftarrow a](y) := \begin{cases} a & \mathrm{ if~} y=x\\ v(y) & \mathrm{ otherwise } \end{cases}$$

It is possible, of course, to use specifically a term algebra $T(\Sigma,Y)$ with an $S$-sorted set $Y$ of variables as $\Sigma$-algebra $A$. In this case, assignements are called substitutions of terms in $T(\Sigma,Y)$ for variables. The value of a term $t\in T(\Sigma,X)$ under a substitution $B(T(\Sigma,Y),X)\ni v \colon X \longrightarrow T(\Sigma,Y)$, written $t[v]$, is just the result of substituting $v(x)$ for all occurences of $x$ in $t$ in the usual sense. For a simple substitution $$v(y) := \begin{cases} u & \mathrm{ if~} y=x\\ y & \mathrm{ otherwise } \end{cases}$$ replacing $x$ by $u\in T(\Sigma,Y)$ in $t\in T(\Sigma,X)$ one often writes $t[x \leftarrow u]$ instead of $t[v]$ [ST99].

References[edit]