Namespaces
Variants
Actions

Interpretation (Formalized Language)

From Encyclopedia of Mathematics
Revision as of 21:29, 24 March 2013 by Boris Tsirelson (talk | contribs) (→‎Definition of Interpretations: a bit nicer)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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

Interpretations establish a relationship between syntax and semantics. The syntax is represented by the terms $T(\Sigma,X)$ constructable by the symbols given by the signature $\Sigma=(S,F)$ and a set $X$ of variables, whereas the semantics is defined by a $\Sigma$-algebra $A$. An interpretation $v^\ast \colon T(\Sigma,X) \longrightarrow A$ always relies on an 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$ [ST99] [W90]. This extension is called an interpretation with respect to the assignement $v$ and written as $t[v]$ for a term $t\in T(\Sigma,X)$. Sometimes it is also called extended assignement. 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 [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$-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$ [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$ [EM85].

In the special case of term-generated $\Sigma$-algebras $A,B\in \mathrm{Gen}(\Sigma)$, some stronger statements can be made [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)$, variables $x\in X$, and assignements $v\in B(A,X)$ it holds $t[x\leftarrow w][v] = t[v[x\leftarrow w[v]]]$ [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'}$ [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

Diagram interpretation.png

commutes, if $\bar a \circ i_a = e$ and $\bar a \circ i_v = a$ [EM85].

References

[EM85] H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 1, Springer 1985
[EM90] H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 2, Springer 1990
[M89] B. Möller: "Algorithmische Sprachen und Methodik des Programmierens I", lecture notes, Technical University Munich 1989
[ST99] D. Sannella, A. Tarlecki, "Algebraic Preliminaries", in Egidio Astesiano, Hans-Joerg Kreowski, Bernd Krieg-Brueckner, "Algebraic Foundations of System Specification", Springer 1999
[W90] M. Wirsing: "Algebraic Specification", in J. van Leeuwen: "Handbook of Theoretical Computer Science", Elsevier 1990
How to Cite This Entry:
Interpretation (Formalized Language). Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Interpretation_(Formalized_Language)&oldid=29556