View source for Interpretation (Formalized Language)

{{MSC|68P05}} 

{{TEX|done}}

Interpretations establish a relationship between [[Syntax|syntax]] and [[Semantics|semantics]]. The syntax is represented by the [[Term (Formalized Language)|terms]] $T(\Sigma,X)$ constructable by the symbols given by the [[Signature (Computer Science)|signature]] $\Sigma=(S,F)$ and a set $X$ of variables, whereas the semantics is defined by a [[Sigma-algebra (Computer Science)|$\Sigma$-algebra $A$]]. An interpretation $v^\ast \colon T(\Sigma,X) \longrightarrow A$ always relies on an [[Assignement|assignement]] $B(A,X)\ni v\colon X\longrightarrow A$, which is extended from variables $X$ to terms $T(\Sigma,X)$. 

===Definition of Interpretations===

Let a signature $\Sigma=(S,F)$, a set $X$ of variables, and a $\Sigma$-algebra $A$ be given.  For an assignement $v\in B(A,X)$ written as $v\colon X \rightarrow \bigcup_{s\in S} s^A$ it exists a unique $\Sigma$-algebra-morphism $v^\ast\colon T(\Sigma,X) \longrightarrow \bigcup_{s\in S} s^A$, which extends $v$, i.e. which fulfills $v^\ast_s (x) = v_s(x)$ for all $s \in S$, $x \in X$ {{Cite|ST99}} {{Cite|W90}}. This extension is called an <i>interpretation with respect to the assignement $v$</i> and written as $t[v]$ for a term $t\in T(\Sigma,X)$. Sometimes it is also called <i>extended assignement</i>. Ground terms $t\in T(\Sigma)$, i.e. terms which do not contain any variable $x\in X$, have an interpretation independent from $v$.

Whereas an assignement makes only a concretion of the variables in the set $X$, an interpretations concretizes a whole term $t\in T(\Sigma,X)$ containing variables. It relates terms --- having a syntactical origin --- and $\Sigma$-algebras, which provides a semantics in the final.

An inductive definition of an interpretation $t[v]$ is given in {{Cite|EM85}}:
* For $x\in X_s$, it holds $x[v] := v(x)$
* For $f\in F$ with ar$(f)=0$, it holds $f[v]:= f^A$
* For $f\in F$ with type$(f)= s_1\times\cdots\times s_n \longrightarrow s$ and for $t_i\in T_{s_i}(\Sigma,X)$, it holds $f(t_1,\ldots,t_n)[v]:= f^A(t_1[v],\ldots,t_n[v])$

===Interpretations and Morphisms===

The special properties of interpretations enable the statement of some compatibility theorems. These theorems describe the relationship between several interpretation mappings as well as between interpretaions and $\Sigma$-algebra-morphisms. Here, at first two theorems concerning general $\Sigma$-algebras are given. Afterwards, the special situation for [[Term-generated Sigma-algebra|term-generated $\Sigma$-algebras]] is discussed.

Let $Y$ be another set of variables with $X\cap Y=\emptyset$.  Furthermore, let
* $B(A,X)\ni v_x\colon X\longrightarrow A$
* $B(A,Y)\ni v_y\colon Y\longrightarrow A$
* $B(T(\Sigma,Y),X)\ni v\colon X\longrightarrow T(\Sigma,Y)$
be assignements. Then $v_x=v_y^\ast\circ v$ implies $v_x^\ast= v_y^\ast\circ v^\ast$ {{Cite|EM85}}.  Now, let $B$ be another $\Sigma$-algebra. Furthermore, let the following mappings be given:
* A $\Sigma$-algebra-morphism $f\colon A\longrightarrow B$
* An assignement $B(A,X)\ni v_A\colon X\longrightarrow A$
* An assignement $B(B,X)\ni v_B\colon X\longrightarrow B$
Then $v_B= f\circ v_A$ implies $v_B^\ast= f\circ v_A^\ast$ {{Cite|EM85}}.

In the special case of term-generated $\Sigma$-algebras $A,B\in \mathrm{Gen}(\Sigma)$, some stronger statements can be made {{Cite|W90}}.  First of all, a morphisms between $A$ and $B$ is uniquely determined by the corresponding assignements of variables. As an immediate consequence, it exists at most one $\Sigma$-algebra-morphism $f$ between two $\Sigma$-algebras $A$ and $B$. If it exists a $\Sigma$-algebra-morphism $f'\colon A\longrightarrow B$ and a $\Sigma$-algebra-morphism $f''\colon B\longrightarrow A$, then it holds $A\cong B$. 

===Special Topics===

;Substitution Theorem
:For terms $t,w\in T(\Sigma,X)$, varianles $x\in X$, and assignements $v\in B(A,X)$ it holds $t[x\leftarrow w][v] = t[v[x\leftarrow w[v]]]$ {{Cite|M89}}.
;Coincidence Theorem
:Let $t\in T(\Sigma,X)$ be a term.  If for assignement $v_1,v_2\in B(A,X)$ it holds $\forall x\in V(t) \colon v_1(x)=v_2(x)$, then it also holds $t[v_1]=t[v_2]$. 
;Interpretations and Reduct
:Let a signature morphism $\sigma\colon \Sigma \longrightarrow \Sigma'$ be given. Let $X$ be an $S$-sorted set of variables such that $X_s$ and $X_{s'}$ are disjoint for $s \neq s'$, $s,s' \in S$, and $X' =  (\bigcup\limits_{\sigma(s)=s'} X_s)_{s'\in S'}$.  Let $A'$ be a $\Sigma'$-algebra and $v' \colon X' \longrightarrow A'$ be an assignement. Define $v \colon X \longrightarrow  A' |_\sigma$ by $v_s(x) = (v')_{\sigma(s)}(x)$ for $s\in S$ and $x \in X$. Then for any $\Sigma$-term $t \in T(\Sigma,X)$, $v^\ast(t) = (v')^\ast(\sigma(t))$. In particular, if $t$ is a ground term, then $t^{A' |_\sigma} = \sigma(t)^{A'}$ {{Cite|ST99}}.
;Relationship between Evaluations, Assignements and Interpretations
:Let $v\in B(A,X)$ be an interpretation $v\colon T(\Sigma,X) \longrightarrow A$.  Then the diagram
[[File:Diagram_interpretation.png|500px|]]
:commutes, if $\bar a \circ i_a = e$ and $\bar a \circ i_v = a$ {{Cite|EM85}}.

===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
|-
|}