View source for Assignement

{{MSC|68P05}} 

{{TEX|done}}

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 (Computer Science)|signature]] $\Sigma=(S,F)$ and a set $X$ of variables. These values $a_1,\ldots,a_n$ are elements of a [[Sigma-algebra (Computer Science)|$\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 <i>assignement</i> 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$ {{Cite|EM85}}.  The set of all assignements is typically designated as $B(A,X)$.  An assignement is also called <i>valuation</i>.

For an assignement $v\in B(A,X)$ and for a value $a\in s^A$ the <i>assignement changed at $x$ to $a$</i>, 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|term algebra]] $T(\Sigma,Y)$ with an $S$-sorted set $Y$ of variables as $\Sigma$-algebra $A$. In this case, assignements are called <i>substitutions</i> 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]$ {{Cite|ST99}}.

===References===

{|
|-
|valign="top"|{{Ref|EM85}}||valign="top"| H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 1, Springer 1985
|-
|valign="top"|{{Ref|EM90}}||valign="top"| H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 2, Springer 1990
|-
|valign="top"|{{Ref|M89}}||valign="top"| B. Möller: "Algorithmische Sprachen und Methodik des Programmierens I", lecture notes, Technical University Munich 1989
|-
|valign="top"|{{Ref|ST99}}||valign="top"| D. Sannella, A. Tarlecki, "Algebraic Preliminaries", in Egidio Astesiano, Hans-Joerg Kreowski, Bernd Krieg-Brueckner, "Algebraic Foundations of System Specification", Springer 1999
|-
|valign="top"|{{Ref|W90}}||valign="top"| M. Wirsing: "Algebraic Specification", in J. van Leeuwen: "Handbook of Theoretical Computer Science", Elsevier 1990
|-
|}