Fixed Point Semantics for Parallel Logic Programming Languages
Etsuya Shibayama · Institutional Repositories DataBase (IRDB) · 1987
A semantics description scheme is presented for parallel logic programming languages.This scheme consists of two parts: description of the semantics of unffication and that of goal reduction strategies.For the former, we define a semantic domain each of whose elements naturally represents a variable binding environment, and, for the latter, we employ the power domain technique.As application examples of this scheme, we describe the semantics of Guarded Horn Clauses (GHC) and Concurrent Prolog (CP). By Definition 2.5, $(\cup:\in$e'\in\{e\in$ $E|\cup t\in Ie;\subseteq e\}$ is satisfied and thus $e \supseteq\cap\{e\in E|\bigcup_{1\in I}e:\subseteq e\}=(\bigcup_{i\in I}e_{1})^{c}$ .Consequently, $( \bigcup_{i\in I}e_{i})^{c}$ is the least upper bound of $\{e_{i}\}_{i\in I}$ in E. $\square$The following lemmas and theorem suggest that, for each $t_{1},$ $\ldots,t_{n},$ $t_{1}^{t},$ $\ldots,t_{n}^{/}\in Termp\gamma$ , after completing a sequence of unifications: $t_{1}=t_{1}^{1},$ $t_{2}=t_{2},$ $\ldots,$ $t_{n}=t_{n}'$ successfully, the variable binding environment will be represented by $\{(t_{1},t_{1}^{t}), \ldots, (t_{n},t_{n}^{t})\}^{c}$ .Lemma 2.7 Let $e$ be $\{(t_{1},t_{1}'), \ldots, (t_{n}, t_{n}')\}^{c}$ .Suppose that $\langle t_{1}, \cdots , t_{n}\rangle$ and \ l a n g l e $t_{1}',$ $\cdots,t_{n}^{t}$ } are unifiable and that the most general unifier of them is $\theta=\{s_{1}/v_{1}, \ldots, s_{m}/v_{m}\}$ .It is satisfied that $\{(v_{1}, s_{1}), \ldots, (v_{m}, s_{m})\}\subseteq e$ .Proof: This lemma can be proven by induction on the total steps necessary to unify { $t_{1},$ $\cdots,t_{n}\rangle$ and { $t_{1}',$ $\cdots$ , $t_{n}'\rangle$ using the Robinson's unification algorithm.$\square$ Lemma 2.8 Let $r$ be a subset of $Term_{F,Y}\cross Term_{F,V}$ .$r^{c}=\{(t,t^{t})|\exists ns.t.t\Rightarrow^{nr}t'\}$ is satisfied, where the relation $\Rightarrow^{nr}$ is defined as follows: 1. $t\Rightarrow^{0r}t(t\in Term_{F,V})$ .2. $t\Rightarrow^{\prime 0}t'$ if $(t,t')\in r$ .