Declarative Compilation for Constraint Logic Programming

Abstract

We present a new declarative compilation of logic programs with constraints into variable-free relational theories which are then executed by rewriting. This translation provides an algebraic formulation of the abstract syntax of logic programs. Management of logic variables, unification, and renaming apart is completely elided in favor of algebraic manipulation of variable-free relation expressions. We prove the translation is sound, and the rewriting system complete with respect to traditional SLD semantics.

1 Introduction

Logic programming is a paradigm based on proof search and directly programming with logical theories. This is done to achieve declarative transparency: guaranteeing that execution respects the mathematical meaning of the program. The power that such a paradigm offers comes at a cost for formal language research and implementation. Management of logic variables, unification, renaming variables apart and proof search are cumbersome to handle formally. Consequently, it is often the case that the formal definition of these aspects is left outside the semantics of programs, complicating reasoning about them and the introduction of new declarative features.

We address this problem here by proposing a new compilation framework – based on ideas of Tarski [21] and Freyd [9] – that encodes logic programming syntax into a variable-free algebraic formalism: relation algebra. Relation algebras are pure equational theories of structures containing the operations of composition, intersection and convolution. An important class of relation algebras is the so-called distributive relation algebras with quasi-projections, which also incorporate union and projections.

We present the translation of constraint logic programs to such algebras in 3 steps. First, for a CLP program $P$ with signature $\varSigma$, we define its associated relation algebra $\mathbf {QRA}_\varSigma$, which provides both the target object language for program translation and formal axiomatization of constraints and logic variables. Second, we introduce a constraint compilation procedure that maps constraints to variable-free relation terms in $\mathbf {QRA}_\varSigma$. Third, a program translation procedure compiles constraint logic programs to an equational theory over $\mathbf {QRA}_\varSigma$.

The key feature of the semantics and translation is its variable-free nature. Programs that contain logical variables are represented as ground terms in our setting, thus all reasoning and execution is reduced to algebraic equality, allowing the use of rewriting. The resulting system is sound and complete with respect to SLD resolution. Our compilation provides a solution to the following problems:

• Underspecification of abstract syntax and logic variable management in logic programs: solved by the the inclusion of metalogical operations directly into the compilation process.

• Interdependence of compilation and execution strategies: solved by making target code completely orthogonal to execution.

• Lack of transparency in compilation (for subsequent optimization and abstract interpretation): solved by making target code a low-level yet fully declarative translation of the original program.

Variable Elimination and Relation Composition. We illustrate the spirit of translation, and in particular the variable elimination procedure, by considering a simple case, namely the transitive closure of a graph:

In this carefully chosen example, the elimination of variables and the translation to binary relation symbols is immediate:

$$\begin{aligned} \mathbf {edge}= & {} (a,b) \cup (b,c) \cup (a,e) \cup (a,e)\cup (e,f) \\ \mathbf {connected}= & {} \mathbf {id}\cup \mathbf {edge};\mathbf {connected}\end{aligned}$$

The key feature of the resulting term is the composition $\mathbf {edge};\mathbf {connected}$. The logical variable $Z$ is eliminated by the composition of relations allowing the use of variable free object code. A query $\mathbf {connected}(a,X)$ is then modeled by the relation $\mathbf {connected}\cap (a,a)\mathbf 1$ where $\mathbf 1$ is the (maximal) universal relation. Computation can proceed by rewriting the query using a suitable orientation of the relation algebra equations and unfolding pertinent recursive definitions.

Handling actual arbitrary constraint logic programs is more involved. First, we use sequences and projection relations to handle predicates involving an arbitrary number of arguments and an unbounded number of logic variables; second, we formalize constraints in a relational way.

Projections and permutations algebraically encode all the operations of logical variables – disjunctive and conjunctive clauses are handled with the help of the standard relational operators $\cap$, $\cup$.

Constraint Logic Programming Conventions. We refer the reader to [16] for basic definitions of logic programming over Horn clauses, and [12] for background on the syntax and semantics of constraint logic programming. In this paper we fix a signature $\varSigma$, a set of terms ${\mathcal T}_\varSigma ({\mathcal X})$, and a subset $\mathcal{C}$ of all first-order formulas over $\varSigma$ closed under conjunction and existential quantification to be the set of constraint formulas as well as a $\varSigma$-structure $\mathcal {D}$, called the constraint domain. Constraint logic programs are sets of Horn clauses. We use vector notation extensively in the paper, to abbreviate Horn clauses with constraints $p\leftarrow q_1,\ldots ,q_n$, where $p$ is an atomic formula and $q_i$ may be an atomic formula or a constraint. For instance, in our vector notation, a clause is written $p({\varvec{t}}[{\varvec{x}}]) \leftarrow {\varvec{q}}({\varvec{u}}[{\varvec{x}},{\varvec{y}}])$, where the boldface symbols indicate vectors of variables ${\varvec{x}},{\varvec{y}}$, terms ${\varvec{t}},{\varvec{u}}$ (depending on variables ${\varvec{x}}$, etc...) and predicates ${\varvec{q}}$ (depending on terms ${\varvec{u}}$).

2 Relation Algebras and Signatures

In this section, we define $\mathbf {QRA}_\varSigma$, a relation algebra in the style of [9, 21] formalizing a CLP signature $\varSigma$ and a constraint domain $\mathcal {D}$. We define its language, its equational theory and semantics.

2.1 Relational Language and Theory

The relation language $\mathsf{R}_{\varSigma }$ is built from a set $\mathsf {R}_{\mathcal C}$ of relation constants for constant symbols a set $\mathsf {R}_{\mathcal F}$ of relation constants for function symbols from $\varSigma$, and a set of relation constants for primitive predicates $\mathsf {R}_\mathcal {CP}$, as well as a fixed set of relation constants and operators detailed below. Let us begin with $\mathsf {R}_{\mathcal C}$. Each constant symbol $a\in {\mathcal C}_\varSigma$ defines a constant symbol $(a,a)\in \mathsf {R}_{\mathcal C}$, each function symbol $f\in {\mathcal F}_\varSigma$ defines a constant symbol $\text{ R }_f$ in $\mathsf {R}_{\mathcal F}$. Each predicate symbol $r \in \mathcal {CP}_\varSigma$ defines a constant symbol $\text{ r }$ in $\mathsf {R}_\mathcal {CP}$. We write $\mathsf{R}_{\varSigma }$ for the full relation language:

$$\begin{aligned} \begin{array}{c} \mathsf {R}_{\mathcal C}= \{(a,a) \mid a \in {\mathcal C}_\varSigma \} \quad \mathsf {R}_{\mathcal F}~=~\{\text{ R }_f\mid f\in {\mathcal F}_\varSigma ,\} \quad \mathsf {R}_\mathcal {CP}~=~\{\text{ r } \mid r\in \mathcal {CP}_\varSigma \} \\ \begin{array}{lcl} \mathsf {R}_ atom &{}{:}{:}{=}&{} \mathsf {R}_{\mathcal C}\mid \mathsf {R}_{\mathcal F}\mid \mathsf {R}_\mathcal {CP}\mid id\mid di\mid \mathbf 1 \mid \mathbf 0 \mid hd \mid tl \\ \mathsf{R}_{\varSigma }&{}{:}{:}{=} &{} \mathsf {R}_ atom \mid {\mathsf{R}_{\varSigma }}^{\circ } \mid \mathsf{R}_{\varSigma }\cup \mathsf{R}_{\varSigma }\mid \mathsf{R}_{\varSigma }\cap \mathsf{R}_{\varSigma }\mid \mathsf{R}_{\varSigma }\mathsf{R}_{\varSigma }\end{array} \end{array} \end{aligned}$$

The constants $\mathbf 1, \mathbf 0, id , di$ respectively denote the universal relation (whose standard semantics is the set of all ordered pairs on a certain set), the empty relation, the identity (diagonal) relation, and identity’s complement. Juxtaposition $RR$ represents relation composition (often written R;R) and $R^{\circ }$ is the inverse of $R$. We write $hd$ and $tl$ for the head and tail relations. The projection of an n-tuple onto its $i$-th element is written $P_i$ and defined as $P_1 \, = \, hd, P_2 \, = \, tl;hd, \ldots , P_{n} \, = \, {tl}^{n-1};hd$.

Fig. 1.

$\mathbf {QRA}_\varSigma$

$\mathbf {QRA}_\varSigma$  (Fig. 1) is the standard theory of distributive relation algebras, plus Tarski’s quasiprojections [21], and equations axiomatizing the new relations of $\mathsf{R}_{\varSigma }$. Note that products and their projections are axiomatized in a relational, variable-free manner.

2.2 Semantics

Let $\varSigma$ be a constraint signature and $\mathcal {D}$ a $\varSigma$-structure. Write $t^\mathcal {D}$ for the interpretation of a term $t \in {\mathcal T}_\varSigma$. We define $\mathcal {D}^{\dagger }$ to be the union of $\mathcal {D}^0 = \{\langle {} \rangle \}$ (the empty sequence), $\mathcal {D}$ and $\mathcal {D}$-finite products, for example: $\mathcal {D}^2, \mathcal {D}^2 \times \mathcal {D}, \mathcal {D}\times \mathcal {D}^2,\ldots$ We write $\langle {a_1,\ldots ,a_n} \rangle$ for members of the n-fold product associating to the right, that is to say, $\langle {a_1,\langle {a_2,\ldots ,\langle {a_{n-1},a_n} \rangle \cdots } \rangle } \rangle$. Furthermore, we assume right-association of products when parentheses are absent. Note that the 1 element sequence does not exist in the domain, so we write $\langle {a} \rangle$ for $a$ as a convenience.

Let $\mathsf{R}_\mathcal {D}= \mathcal {D}^{\dagger }\times \mathcal {D}^{\dagger }$. We make the power set of $\mathsf{R}_\mathcal {D}$ into a model of the relation calculus by interpreting atomic relation terms in a certain canonical way, and the operators in their standard set-theoretic interpretation. We interpret $hd$ and $tl$ as projections in the model.

Definition 1

Given a structure $\mathcal {D}$ a relational $\mathcal {D}$-interpretation is a mapping $[\![ {\_} ]\!]^{\mathcal {D}^{\dag }}$ of relational terms into $\mathsf{R}_\mathcal {D}$ satisfying the identities in Fig. 2. The function $\alpha$ used in this table and elsewhere in this paper refers to the arity of its argument, whether a relation or function symbol from the underlying signature.

Fig. 2.

Standard interpretation of binary relations.

Theorem 1

Equational reasoning in $\mathbf {QRA}_\varSigma$ is sound for any interpretation:

$$\begin{aligned} \mathbf {QRA}_\varSigma \vdash R=S \Longrightarrow [\![ {R} ]\!]^{\mathcal {D}^{\dag }} = [\![ {S} ]\!]^{\mathcal {D}^{\dag }} \end{aligned}$$

3 Program Translation

We define constraint and program translation to relation terms. To this end, we define a function $\dot{K}$ from constraint formulas with – possibly free – logic variables to a variable-free relational term. $\dot{K}$ is the core of the variable elimination mechanism and will appear throughout the rest of the paper.

The reader should keep in mind that there are two kinds of predicate symbols in a constraint logic program: constraint predicates $r$ which are translated by the function $\dot{K}$ above to relation terms r, and defined or program predicates.

We translate defined predicates – and CLP programs – to equations where $\overline{{p}}$ will be drawn from a set of definitional variables standing for program predicate names $p$, and $R$ is a relation term. The set of definitional equations can be both seen as an executable specification, by understanding it in terms of the rewriting rules given in this paper; or as a declarative one, by unfolding the definitions and using the standard set-theoretic interpretation of binary relations.

3.1 Constraint Translation

We fix a canonical list $x_1,\ldots ,x_n$ of variables occurring in all terms, so as to translate them to variable-free relations in a systematic way. There is no loss of generality as later, we transform programs into this canonical form.

Definition 2

(Term Translation). Define a translation function $K : {\mathcal T}_\varSigma ({\mathcal X})\! \rightarrow \mathsf{R}_{\varSigma }$ from first-order terms to relation expressions as follows:

$$\begin{aligned} \begin{array}{lll} K(c)&{} =&{} (c,c)\mathbf 1 \\ K(x_i)&{} =&{} P_i^{\circ }\\ K(f(t_1,\ldots ,t_n)) &{} = &{} \text{ R }_f; \bigcap _{i\le n}\, P_i;K(t_i)\\ \end{array} \end{aligned}$$

This translation is extended to vectors of terms as follows $K(\langle {t_1,\ldots ,t_n} \rangle ) = \bigcap _{i\le n}\, P_i;K(t_i)$.

The semantics of the relational translation of a term is the set of all of the instances of that term, paired with the corresponding instances of its variables. For instance, the term $x_1 + s(s(x_2))$ is translated to the relation $\mathsf {+};(P_1;P_1^{\circ }\cap P_2;\mathsf {s};\mathsf {s};P_2^{\circ })$.

Lemma 1

Let $t[{\varvec{x}}]$ be a term of ${\mathcal T}_\varSigma ({\mathcal X})$ whose free variables are among those in the sequence ${\varvec{x}}=x_1,\ldots ,x_m$. Then, for any sequences ${\varvec{a}}= a_1,\ldots ,a_m \in \mathcal {D}^{\dagger }, {\varvec{u}}\in \mathcal {D}^{\dagger }$ and any $b\in \mathcal {D}$ we have

$$\begin{aligned} (b,{\varvec{a}}{\varvec{u}}) \in [\![ {K(t[{\varvec{x}}])} ]\!]^{\mathcal {D}^{\dag }} \iff b = t^{\mathcal {D}}[{\varvec{a}}/{\varvec{x}}] \end{aligned}$$

We will translate constraints over $m$ variables to partially coreflexive relations over the elements that satisfy them. A binary relation $R$ is coreflexive if it is contained in the identity relation, and it is $i$ -coreflexive if its $i$-th projection is contained in the identity relation: $P_i^{\circ };R;P_i \subseteq id$. Thus, for a variable $x_i$ free in a constraint, the translation will be $i$-coreflexive.

We now formally define two partial identity relation expressions $I_m$, $Q_i$ for the translation of existentially quantified formulas, in such a way that if a constraint $\varphi [{\varvec{x}}]$ over $m$ variables is translated to an $m$-coreflexive relation, the formula $\exists x_i.~\varphi [{\varvec{x}}]$ corresponds to a coreflexive relation in all the positions but the $i$-th one, as $x_i$ is no longer free. In this sense $Q_i$ may be seen as a hiding relation.

Definition 3

The partial identity relation expressions $I_m$, $Q_i$ for $m, i > 0$ are defined as:

$$\begin{aligned} I_m := \bigcap _{1\le i\le m} P_i(P_i)^{\circ }\qquad Q_i = I_{i-1} \cap J_{i+1} \qquad J_i = tl^i;(tl^{\circ })^i \end{aligned}$$

$I_m$ is the identity on sequences up to the first $m$ elements. $Q_i$ is the identity on all but the $i$-th element, with the $i$-th position relating arbitrary pairs of elements.

Definition 4

(Constraint Translation). The $\dot{K}: \mathcal {L}_\mathcal {D}\rightarrow \mathsf{R}_{\varSigma }$ translation function for constraint formulas is:

$$\begin{aligned} \begin{array}{lll} \dot{K}(p(t_1,\ldots ,t_n)) &{} = &{} (\bigcap _{i\le n}\, K(t_i)^{\circ };P_i^{\circ });\text{ p };(\bigcap _{i\le n}\, P_i;K(t_i))\\ \dot{K}(\varphi \wedge \theta ) &{} = &{} \dot{K}(\varphi )\cap \dot{K}(\theta ) \\ \dot{K}(\exists x_i.~\varphi ) &{} = &{} Q_i;\dot{K}(\varphi );Q_i \end{array} \end{aligned}$$

As an example, the translation of the constraint $\exists x_1, x_2. s(x_1) \le x_2$ is

$$ Q_1;Q_2;(P_1^{\circ };\mathsf {s}^{\circ };P_1 \cap P_2^{\circ };P_2);\mathsf {\le };(P_1;\mathsf {s};P_1^{\circ }\cap P_2;P_2^{\circ });Q_1;Q_2 $$

Lemma 2

Let $\varphi [{\varvec{x}}]$ be a constraint formula with free variables among ${\varvec{x}}=x_1,\ldots ,x_m$. Then, for any sequences ${\varvec{a}}= a_1,\ldots ,a_m$, ${\varvec{u}}$ and ${\varvec{u}}'$ of members of $\mathcal {D}$

$$ ({\varvec{a}}{\varvec{u}},{\varvec{a}}{\varvec{u}}') \in [\![ {\dot{K}(\varphi [{\varvec{x}}])} ]\!]^{\mathcal {D}^{\dag }} \iff \mathcal {D}\models \varphi [{\varvec{a}}/{\varvec{x}}] $$

3.2 Translation of Constraint Logic Programs

To motivate the technical definitions below, we illustrate the program translation procedure with an example. Assume a language with constant $0$, a unary function symbol $s$, constraint predicate $=$ and program predicate $add$. We can write the traditional Horn clause definition of Peano addition:

This program is first purified: the variables in the head of the clauses defining each predicate are chosen to be a sequence of fresh variables $x_1,x_2,x_3$, with all bindings stated as equations in the tail.

$$\begin{aligned} add(x_1,x_2,x_3)&\longleftarrow x_1 = 0, x_2 = x_3.\\ add(x_1,x_2,x_3)&\longleftarrow \exists x_4,x_5 x_1 = s(x_4), x_3 = s(x_5), add(x_4, x_2, x_5)) \end{aligned}$$

The clauses are combined into a single definition similar to the Clark completion of a program. We also use the variable permutation $\pi$ sending $x_1,x_2,x_3,x_4,x_5 \mapsto x_4,x_2,x_5,x_1,x_3$ to rewrite the occurrence of the predicate $add$ in the tail so that its arguments coincide with those in the head:

$$\begin{aligned} add(x_1,x_2,x_3)&\leftrightarrow ( x_1 = 0, x_2 = x_3)\\&\vee \exists x_4,x_5, x_1 = s(x_4), x_3 = s(x_5), w_\pi \,add(x_1, x_2, x_3). \end{aligned}$$

Now we apply relational translation $\dot{K}$ defined above to all relation equations, and eliminate the existential quantifier using the partial identity operator $I_3$ defined above. We represent the permutation $\pi$ using the relation expression $W_\pi$ that simulates its behavior in a variable-free manner and replace the predicate $add$ with a corresponding relation variable $\overline{add}$. (A formal definition of $W_\pi$ and its connection with function $w_\pi$ is given below, see Definition 7 and Lemma 4.)

Now we give a description of the general translation procedure. We first process programs to their complete database form as defined in [6], which given the executable nature of our semantics reflects the choice to work within the minimal semantics. The main difference in our processing of a program $P$ to its completed form $P'$ is that a strict policy on variable naming is enforced, so that the resulting completed form is suitable for translation to relational terms.

Definition 5

(General Purified Form for Clauses). For a clause $p({\varvec{t}}[{\varvec{y}}]) \leftarrow {\varvec{q}}({\varvec{v}}[{\varvec{y}}])$, let $h = \alpha (p)$, $y = |{{\varvec{y}}}|$, $v = |{{\varvec{v}}}|$, and $m = h + y + v$. Assume vectors:

$$\begin{aligned} \begin{array}{llllrll@{}l@{}l} {\varvec{x}}&{}=&{} {\varvec{x}}_h{\varvec{x}}_t &{}=&{} {\varvec{x}}_h {\varvec{x}}_y {\varvec{x}}_v &{}=&{} {x}_1,\ldots ,{x}_{h}, &{} {x}_{h +1},\ldots ,{x}_{h+y},&{} {x}_{h+y+1},\ldots ,{x}_{m}\\ {\varvec{x}}_h &{}&{} &{}&{} &{}=&{} {x}_1,\ldots ,{x}_{h} &{} &{} \\ {\varvec{x}}_t &{}&{} &{}=&{} {\varvec{x}}_y {\varvec{x}}_v &{}=&{} &{} {x}_{h +1},\ldots ,{x}_{h+y},&{} {x}_{h+y+1},\ldots ,{x}_{m}\\ {\varvec{x}}_y &{}&{} &{}&{} &{}=&{} &{} {x}_{h +1},\ldots ,{x}_{h+y}&{} \\ {\varvec{x}}_v &{}&{} &{}&{} &{}=&{} &{} &{} {x}_{h+y+1},\ldots ,{x}_{m}\\ \end{array} \end{aligned}$$

the clause’s GPF form is:

$$\begin{aligned} p({\varvec{x}}_h) \leftarrow \exists ^{{h}\uparrow }. (({\varvec{x}}_h = {\varvec{t}}[{\varvec{x}}_y] \wedge {\varvec{x}}_v = {\varvec{v}}[{\varvec{x}}_y]), {\varvec{q}}({\varvec{x}}_v)) \end{aligned}$$

$\exists ^{{n}\uparrow }$ denotes existential closure with respect to all variables whose index is greater than $n$. ${\varvec{x}}_h$ and ${\varvec{x}}_t$ stand for head and tail variables. A program is in GPF form iff every one of its clauses is. After the GPF step, we perform Clark’s completion.

Definition 6

(Completion of a Predicate). We define Clark’s completed form for a predicate $p$ with clauses $cl_1,\ldots ,cl_n$ in GPF form:

The above definition easily extends to programs. Completed forms are translated to relations by using $\dot{K}$ for the constraints, mapping conjunction to $\cap$ and $\vee$ to $\cup$. Existential quantification, recursive definitions and parameter passing are handled in a special way which we proceed to detail next.

Existential Quantification: Binding Local Variables. Variables local to the tail of a clause are existentially quantified. For technical reasons — simpler rewrite rules — we use the partial identity relation $I_n$, rather than the $Q_n$ relation defined in the previous sections. $I_n$ acts as an existential quantifier for all variables of index greater than a given number.

Lemma 3

Let ${\varvec{a}}= {a}_1,\ldots ,{a}_n \in \mathcal {D}$, ${\varvec{x}}= {x}_1,\ldots ,{x}_n$, let $\varphi$ be a constraint over $m$ free variables, with $m > n$, ${\varvec{y}}$ a vector of length $k$ such that $n + k = m$, and ${\varvec{u}}, {\varvec{v}}\in \mathcal {D}^\dag$, then:

$$\begin{aligned} ({\varvec{a}}{\varvec{u}}, {\varvec{a}}{\varvec{v}}) \in [\![ {I_n;\dot{K}(\varphi [{\varvec{x}}{\varvec{y}}]);I_n} ]\!]^{\mathcal {D}^{\dag }} \iff \mathcal {D}\models (\exists ^{{n}\uparrow }. \varphi [{\varvec{x}}{\varvec{y}}])[{\varvec{a}}/{\varvec{x}}] \end{aligned}$$

Recursive Predicate Definitions. We shall handle recursive predicate definitions by extending the relational language with a set of definitional symbols $\overline{{p}}, \overline{{q}}, \overline{{r}}, \ldots$ for predicates. Then, a recursive predicate $\overline{{p}}$ is translated to a definitional equation spelled out in Definition 8 where the notation $R({\overline{{p}}}_1,\ldots ,{\overline{{p}}}_n)$ indicates that relation $R$ resulting from the translation may depend on predicate symbols ${\overline{{p}}}_1,\ldots ,{\overline{{p}}}_n$. Note that $R$ is monotone in ${\overline{{p}}}_1,\ldots ,{\overline{{p}}}_n$. Consequently, using a straightforward fixed point construction we can extend the interpretation $[\![ {\_} ]\!]^{\mathcal {D}^{\dag }}$ to satisfy $[\![ {\overline{{p}}} ]\!]^{\mathcal {D}^{\dag }} = [\![ {R({\overline{{p}}}_1,\ldots ,{\overline{{p}}}_n)} ]\!]^{\mathcal {D}^{\dag }}$, thus preserving soundness when we adjoin the definitional equations to $\mathbf {QRA}_\varSigma$. The details are given in Subsect. 3.3, below.

Parameter Passing. The information about the order of parameters in each pure atomic formula $p(x_{i_1},\ldots ,x_{i_r})$ is captured using permutations. Given a permutation $\pi : \{1..n\} \rightarrow \{1..n\}$, the function $w_\pi$ on formulas and terms is defined in the standard way by its action over variables. We write $W_\pi$ for the corresponding relation:

Definition 7

(Switching Relations). Let $\pi : \{1..n\} \rightarrow \{1..n\}$ be a permutation. The switching relation expression $W_\pi$, associated to $\pi$ is:

$$\begin{aligned} W_\pi = \bigcap _{j=1}^{n}\, P_{\pi (j)}(P_j)^{\circ }. \end{aligned}$$

Lemma 4

Fix a permutation $\pi$ and its corresponding $w_\pi$ and $W_\pi$. Then:

$$\begin{aligned}{}[\![ {\dot{K}(w_\pi (p({x}_1,\ldots ,{x}_n)))} ]\!] = [\![ {W_\pi \dot{K}(p) W_\pi ^{\circ }} ]\!] \end{aligned}$$

The Translation Function. Now we may define the translation for defined predicates.

Definition 8

(Relational Translation of Predicates). Let $h, p({\varvec{x}}_h)$ be as in Definition 5. The translation function $Tr$ from completed predicates to relational equations is defined by:

where ${\varvec{x}}_i$ is the original sequence of variables in $p_i$ in the Clark completion of the program, and $\pi$ a permutation that transforms the ordered sequence of length $\alpha (p)$ starting at $x_1$ to ${\varvec{x}}_i$.

We will sometimes write $I_n(R)$ for $I_nRI_n$ and $W_\pi (R)$ for $W_\pi RW^\circ _{i}$.

Example 1

Figure 3 shows a fragment of a constraint logic program to represent a family relations database [20].

Fig. 3.

Biblical family relations in prolog.

Consider the translation of the program predicates mother, parent, sibling and brother. We write the program in general purified form:

$$\begin{aligned} mother (x_1,x_2)\iff & {} (x_1 = sarah ) \wedge (x_2 = isaac ) \\ parent (x_1,x_2)\iff & {} father (x_1,x_2) \vee mother (x_1,x_2) \\ sibling (x_1,x_2)\iff & {} \exists x_3.~ x_1 \ne x_2 \wedge parent (x_3,x_1) \wedge parent (x_3,x_2)\\ brother (x_1,x_2)\iff & {} male (x_1) \wedge sibling (x_1,x_2) \end{aligned}$$

Letting $\sigma _1$ and $\sigma _2$ be the permutations $\langle {1,2,3} \rangle \longrightarrow \langle {2,3,1} \rangle$ and $\langle {1,2,3} \rangle \longrightarrow \langle {3,2,1} \rangle$ respectively we obtain

$$\begin{aligned} \overline{ mother }= & {} \dot{K}(x_1 = sarah ) \cap \dot{K}(x_2 = isaac )\\ \overline{ parent }= & {} \overline{ father } \cup \overline{ mother }\\ \overline{ sibling }= & {} \dot{K}(x_1 \ne x_2) \cap I_2[W_{\sigma _1} \overline{ parent } W_{\sigma _1}^o \cap W_{\sigma _2} \overline{ parent } W_{\sigma _2}^o]I_2\\ \overline{ brother }= & {} \overline{ male } \cap \overline{ sibling } \end{aligned}$$

The query $brother (X,milcah)$ leads to the rewriting of the term $\dot{K}(x_2 = milcah ) \cap \overline{ brother }$ to $\dot{K}(x_2 = milcah ) \cap \dot{K}(x_1 = lot)$.

3.3 The Least Relational Interpretation Satisfying Definitional Equations

Let $P$ be a program and $\overline{{p}}_1,\ldots ,\overline{{p}}_n$ be a sequence of relation variables, one for each predicate symbol $p_i$ in the language of $P$. We define the extended relation calculus $\mathsf{R}_{\varSigma }(\overline{{p}}_1,\ldots ,\overline{{p}}_n)$ to be the set of terms generated by $\overline{{p}}_1,\ldots ,\overline{{p}}_n$ and the terms of $\mathsf{R}_{\varSigma }$. More formally

$$ \begin{array}{lcl} \mathsf {R}_ atom &{}{:}{:}{=}&{} \overline{{p}}_1\mid \cdots \ \mid \overline{{p}}_n\mid \mathsf {R}_{\mathcal C}\mid \mathsf {R}_{\mathcal F}\mid \mathsf {R}_\mathcal {CP}\mid id\mid di\mid \mathbf 1 \mid \mathbf 0 \mid hd \mid tl \\ \mathsf{R}_{\varSigma }(\overline{{p}}_1,\ldots ,\overline{{p}}_n)&{} {:}{:}{=} &{} \mathsf {R}_ atom \mid {\mathsf{R}_{\varSigma }}^{\circ } \mid \mathsf{R}_{\varSigma }\cup \mathsf{R}_{\varSigma }\mid \mathsf{R}_{\varSigma }\cap \mathsf{R}_{\varSigma }\mid \mathsf{R}_{\varSigma }\mathsf{R}_{\varSigma }\end{array} $$

Observe that the relational translation of Definition 8 maps programs to sets of definitional equations over $\mathsf{R}_{\varSigma }(\overline{{p}}_1,\ldots ,\overline{{p}}_n)$. Let $\mathcal{F}$ be the set of all $n$ such definitional equations.

Given a structure $\mathcal{D}$ we now lift the definition of $\mathcal{D}$ -interpretation given in Definition 1 to the extended relation calculus. An extended interpretation $[\![ {~} ]\!] :\mathsf{R}_{\varSigma }(\overline{{p}}_1,\ldots ,\overline{{p}}_n)\longrightarrow \mathsf {R}_\mathcal{D}$ is a function satisfying the identities in Fig. 2 as well as mapping each relation variable $\overline{{p}}_i$ to an arbitrary member $[\![ {\overline{{p}}_i} ]\!]$ of $\mathsf {R}_\mathcal{D}$. Given a structure $\mathcal{D}$ for the language of a program, its action is completely determined by its values at the $\overline{{p}}_i$. Note that the set $\mathcal{I}$ of all such interpretations forms a CPO, a complete partial order with a least element, under pointwise operations. That is to say, any directed set $\{[\![ {\ } ]\!]_d: d\in \varLambda \}$ of interpretations has a supremum $\bigvee _{d\in \varLambda }[\![ {\ } ]\!]_d$ given by $T\mapsto \bigcup _{d\in \varLambda } [\![ {T} ]\!]_d$. The directedness assumption is necessary. For example, to show that a pointwise supremum of interpretations $\bigvee _{d\in \varLambda } [\![ {\ } ]\!]_d$ preserves composition (one of the 13 identities of Fig. 2), we must show that for any relation terms $R$ and $S$ we have $\bigcup _{d\in \varLambda } [\![ {RS} ]\!]_d = \bigcup _{d\in \varLambda } [\![ {R} ]\!]_d ; \bigcup _{d\in \varLambda } [\![ {S} ]\!]_d$. However the right hand side of this identity is equal to $\bigcup _{d,e\in \varLambda \times \varLambda } [\![ {R} ]\!]_d;[\![ {S} ]\!]_e$. But since the family of interpretations is directed, for every pair $d,e$ of indices in $\varLambda$ there is an $m\in \varLambda$ with $[\![ {\ } ]\!]_d, [\![ {\ } ]\!]_e\le [\![ {\ } ]\!]_m$, hence $\bigcup _{d,e\in \varLambda \times \varLambda } [\![ {R} ]\!]_d;[\![ {S} ]\!]_e \le \bigcup _{m\in \varLambda } [\![ {R} ]\!]_m [\![ {S} ]\!]_m$. The reverse inequality is immediate and we obtain $\bigcup _{d\in \varLambda } [\![ {R} ]\!]_d ; \bigcup _{d\in \varLambda } [\![ {S} ]\!]_d = \bigcup _{d\in \varLambda } [\![ {RS} ]\!]_d$.

The least element of the collection $\mathcal{I}$ is the interpretation $[\![ {\ } ]\!]_0$ given by $[\![ {\overline{p_i}} ]\!]_0 = \emptyset$ for all $i$ $(1\le i\le n)$.

In the remainder of this section, the word interpretation will refer to an extended $\mathcal{D}$-interpretation.

Lemma 5

Let $[\![ {\ } ]\!]$ and $[\![ {\ } ]\!]'$ be interpretations. If for all $i$ $[\![ {\overline{{p}}_i} ]\!]\subseteq [\![ {\overline{{p}}_i} ]\!]'$ then $[\![ {\ } ]\!]\le [\![ {\ } ]\!]'$.

Proof

By induction on the structure of extended relations. For all relational constants $c$ we have $[\![ {c} ]\!] = [\![ {c} ]\!]'$ We will consider one of the inductive cases, namely that of composition. Suppose $[\![ {R} ]\!]\subseteq [\![ {R} ]\!]'$ and $[\![ {S} ]\!]\subseteq [\![ {S} ]\!]'$. Then we must show that $[\![ {RS} ]\!]\subseteq [\![ {RS} ]\!]'$. But this follows immediately by a set-theoretic argument, since $(x,u)\in [\![ {R} ]\!]$ and $(u,y)\in [\![ {S} ]\!]$ imply, by inductive hypothesis, that $(x,u)\in [\![ {R} ]\!]'$ and $(u,y)\in [\![ {S} ]\!]'$. It can also be proved using the axioms of $\mathbf {QRA}_\varSigma$ by showing that $A\cup A' = A'$ and $B\cup B'=B'$ imply $AB\cup A'B'=A'B'$. We leave the remaining cases to the reader.

We will now define a operator $\varPhi _\mathcal{F}$ from interpretations to interpretations, show it continuous and define the interpretation generated by $\mathcal{F}$ as its least fixed point. This interpretation will be the least extension of a given relational $\mathcal{D}$-interpretation satisfying the equations in $\mathcal{F}$.

Definition 9

Let $P$ be a program, with predicate symbols $\{p_1,\ldots ,p_n\}$. Fix a structure $\mathcal{D}$ for the language of $P$. Let $\mathcal{F}$ be the set of definitional equations produced by the translation $Tr$ of $P$ of Definition 8. Let $\mathcal{I}$ be the set of extended $\mathcal{D}$-interpretations, with poset structure induced pointwise. Then we define the operator $\varPhi _\mathcal{F}:\mathcal{I}\longrightarrow \mathcal{I}$ as follows

$$ \varPhi _\mathcal{F}([\![ {\ } ]\!])(\overline{{p}}_i) = [\![ {R_i(\overline{{p}}_1,\ldots ,\overline{{p}}_n)} ]\!]. $$

Theorem 2

$\varPhi _\mathcal{F}$ is a continuous operator, that is to say it preserves suprema of directed sets.

Proof

Let $\{[\![ {\ } ]\!]_d:d\in \varLambda \}$ be a directed set of interpretations. By Lemma 5 it suffices to show that for all $p_i$

$$ \varPhi _\mathcal{F}(\bigvee _{d\in \varLambda }{[\![ {\ } ]\!]_d}) (\overline{{p}}_i) = (\bigvee _{d\in \varLambda }\varPhi _\mathcal{F}({[\![ {\ } ]\!]_d}))(\overline{{p}}_i). $$

Let $[\![ {\ } ]\!]^* = \bigvee _{d\in \varLambda }{[\![ {\ } ]\!]_d}$. Then $\varPhi _\mathcal{F}(\bigvee _{d\in \varLambda }{[\![ {\ } ]\!]_d}) (\overline{{p}}_i) = [\![ {R_i(\overline{{p}}_1,\ldots ,\overline{{p}}_n)} ]\!]^*$, which in turn is the union $\bigcup _{d\in \varLambda } [\![ {R_i(\overline{{p}}_1,\ldots ,\overline{{p}}_n)} ]\!]_d$. But this is equal to $\bigcup _{d\in \varLambda }\varPhi _\mathcal{F}({[\![ {\ } ]\!]_d})(\overline{{p}}_i)$. Therefore $\varPhi _\mathcal{F}(\bigvee _{d\in \varLambda }{[\![ {\ } ]\!]_d}) = \bigvee _{d\in \varLambda }\varPhi _\mathcal{F}({[\![ {\ } ]\!]_d})$.

By Kleene’s fixed point theorem $\varPhi _\mathcal{F}$ has a least fixed point ${[\![ {\ } ]\!]}^{\dagger }$ in $\mathcal{I}$. This fixed point is, in fact, the union of all $\varPhi _\mathcal{F}^{(n)}([\![ {\ } ]\!]_0), (n\in {\mathbb {N}})$. By virtue of its being fixed by $\varPhi _\mathcal{F}$ we have ${[\![ {\overline{{p}}_i } ]\!]}^{\dagger } = {[\![ {R_i(\overline{{p}}_1,\ldots ,\overline{{p}}_n) } ]\!]}^{\dagger }$. That is to say, all equations in $\mathcal{F}$ are true in ${[\![ {\ } ]\!]}^{\dagger }$, which is the least interpretation with this property under the pointwise order.

4 A Rewriting System for Resolution

In this section, we develop a rewriting system for proof search based on the equational theory $\mathbf {QRA}_\varSigma$, which will be proven equivalent to the traditional operational semantics for CLP. In Sect. 5 we will show that answers obtained by resolution correspond to answers yielded by our rewriting system and conversely.

The use of ground terms permits the use of rewriting, overcoming the practical and theoretical difficulties that the existence of logic variables causes in equational reasoning. Additionally, we may speak of executable semantics: we use the same function to compile and interpret CLP programs in the relational denotation.

For practical reasons, we don’t rewrite over the full relational language, but we will use a more compact representation of the relations resulting from the translation.¹

Formally, the signature of our rewriting system is given by the following term-forming operations over the sort $\mathcal {T}_R$: $\mathsf {I} : (\mathbb {N} \times \mathcal {T}_R) \rightarrow \mathcal {T}_R,\ \mathsf {W}:(\mathsf {Perm} \times \mathcal {T}_R) \rightarrow \mathcal {T}_R,\ \mathsf {K}:\mathcal {L}_\mathcal {D}\rightarrow \mathcal {T}_R,\ \cup : ({\mathcal {T}_R} \times {\mathcal {T}_R}) \rightarrow \mathcal {T}_R$ and $\cap : ({\mathcal {T}_R} \times {\mathcal {T}_R}) \rightarrow \mathcal {T}_R$. Thus, for instance, the relation $I_n;R;I_n$ is formally represented in the rewriting system as $\mathsf {I}(n,\mathsf{R})$, provided $\mathsf{R}$ can be represented in it. In practice we make use of the conventional relational notation $I_n,W_\pi$ when no confusion can arise.

4.1 Meta-Reductions

We formalize the interface between the rewrite system and the constraint solver as meta-reductions (Fig. 4). Every meta-reduction uses the constraint solver in a black-box manner to perform constraint manipulation and satisfiability checking.

Fig. 4.

Constraint meta-reductions

Lemma 6

All meta-reductions are sound: if $m_i:l\mathop {\longmapsto }\limits ^{_{P}}r$ then $[\![ {l} ]\!]^{\mathcal {D}^{\dag }}=[\![ {r} ]\!]^{\mathcal {D}^{\dag }}$.

4.2 A Rewriting System for SLD Resolution

We present a rewriting system for proof search in Fig. 5. We prove local confluence. Later we will prove that a query rewrites to a term in the canonical form $\dot{K}(\psi _{})\cup R$ iff the leftmost branch of the associated SLD-tree of the program is finite.

Fig. 5.

Rewriting system for $SLD$.

Lemma 7

$\mathop {\longmapsto }\limits ^{_{P}}$ is sound: if $p_i:l\mathop {\longmapsto }\limits ^{_{P}}r$ then $[\![ {l} ]\!]^{\mathcal {D}^{\dag }}=[\![ {r} ]\!]^{\mathcal {D}^{\dag }}$.

Lemma 8

If we give higher priority to $p_7$ over $p_8$, $\mathop {\longmapsto }\limits ^{_{P}}$ is locally confluent.

A left outermost strategy gives priority to $p_7$ over $p_8$.

5 Operational Equivalence

We prove that our rewriting system over relational terms simulates “traditional” SLD proof search specified as a transition-based operational semantics (i.e. [7, 12]). For reasons of space, we give a high-level overview of the proof. The full details can be found in the online technical report.

Recall a resolvent is a sequence of atoms or constraints ${\varvec{p}}$. We write $\Box$ for the empty resolvent. We assume given a constraint domain $\mathcal {D}$ and its satisfaction relation $\mathcal {D}\models \varphi$. A program state is an ordered pair $\langle {{{\varvec{p}}}\,\vert \,{\varphi }} \rangle$ where ${\varvec{p}}$ is a resolvent and $\varphi$ is a constraint (called the constraint store). The notation $cl: p({\varvec{u}}[{\varvec{y}}]) \leftarrow {\varvec{q}}({\varvec{v}}[{\varvec{z}}])$ indicates that $p({\varvec{u}}[{\varvec{y}}]) \leftarrow {\varvec{q}}({\varvec{v}}[{\varvec{z}}])$ is a program clause with label $cl$. Then, the standard operational semantics for SLD resolution can be defined as the following transition system over program states:

Definition 10

(Standard SLD Semantics).

$$\begin{aligned} \begin{array}{lcl} \langle {{\varphi ,{\varvec{p}}}\,\vert \,{\psi }} \rangle &{}\xrightarrow {cs}_l &{} \langle {{{\varvec{p}}}\,\vert \,{\psi \wedge \varphi }} \rangle \text {iff}~\mathcal {D}\models \psi \wedge \varphi \\ \langle {{p({\varvec{t}}[{\varvec{x}}]),{\varvec{p}}}\,\vert \,{\varphi }} \rangle &{} \xrightarrow {res_{cl}}_l &{} \langle {{{\varvec{q}}({\varvec{v}}[\sigma ({\varvec{z}})]),{\varvec{p}}}\,\vert \,{\varphi \wedge ({\varvec{u}}[\sigma ({\varvec{y}})] = {\varvec{t}}[{\varvec{x}}])}} \rangle \\ &{} \text {where:} &{} \begin{array}{l} cl: p({\varvec{u}}[{\varvec{y}}]) \leftarrow {\varvec{q}}({\varvec{v}}[{\varvec{z}}]) \\ \mathcal {D}\models \varphi \wedge ({\varvec{u}}[\sigma ({\varvec{y}})] = {\varvec{t}}[{\varvec{x}}]) \\ \sigma \text { a renaming apart for }{\varvec{y}}, {\varvec{z}}, {\varvec{x}}\end{array} \end{array} \end{aligned}$$

Taking the previous system as a reference, the proof proceeds in two steps: we first define a new transition system that internalizes renaming apart and proof search, and we prove it equivalent to the standard one.

Second, we show a simulation relation between the fully internalized transition system and a transition system defined over relations, which is implemented by the rewriting system of Sect. 4.

With these two equivalences in place, the main theorem is:

Theorem 3

The rewriting system of Fig. 5 implements the transition system of Definition 10. Formally, for every transition $(r_1, r_2) \in (\xrightarrow {}_l)^*$,

$$ \exists n. (Tr(r_1), Tr(r_2)) \in (\mathop {\longmapsto }\limits ^{_{P}})^n $$

and

$$ \forall r_3. (Tr(r_1), r_3) \in (\mathop {\longmapsto }\limits ^{_{P}})^n \Rightarrow Tr(r_2) = r_3 $$

Thus, given a program $P$, relational rewriting of translation will return an answer constraint $K(\varphi )$ iff SLD resolution from $P$ reaches a program state $\langle {{\Box }\,\vert \,{\varphi '}} \rangle$, with $\varphi \iff \varphi '$.

In the next section, we briefly describe the main intermediate system used in the proof.

5.1 The Resolution Transition System

The crucial part of the SLD-simulation proof is the definition of a new extended transition system over program states that will internalize both renaming apart and the proof-search tree. It is an intermediate system between relation rewriting and traditional proof search.

The first step towards the new system is the definition of an extended notion of state. In the standard system of Definition 10, a state is a resolvent plus a constraint store. Our extended notion of state includes:

• A notion of scope, which is captured by a natural number which can be understood as the number of global variables of the state.

• A notion of substate, which includes information about parameter passing in the form of a permutation.

• A notion of clause selection, and

• a notion of failure and parallel state, which represents failures in the search tree and alternatives.

Such states are enough to capture all the meta-theory of constraint logic programming except recursion, which operates meta-logically by replacing predicate symbols by their definitions. Formally:

Definition 11

The set $\mathcal {PS}$ of resolution states is inductively defined as:

• $\langle fail \rangle$.

• $\langle {\varvec{p}}|\varphi \rangle _n$, where $p_i \equiv P_i({\varvec{x}}_i)$ is an atom, or a constraint $p_i \equiv \psi$, ${\varvec{x}}_i$ a vector of variables, $\varphi$ a constraint store and $n$ a natural number.

• $\langle ^{\pi }{ PS },{\varvec{p}}|\varphi \rangle _n$, where $PS$ is a resolution state, and $\pi$ a permutation.

• ${\langle ^{\pi }{\blacktriangleright }{PS},{\varvec{p}}|{\varphi }\rangle }_n$, the “select state”. It represents the state just before selecting a clause to proceed with proof search.

• The bar is parallel composition, capturing choice in the proof search tree.

The resolution transition system $\rightarrow _P \subseteq (\mathcal {PS} \times \mathcal {PS})$ is shown in Fig. 6. The two first transitions deal with the case where a constraint is first in the resolvent, failing or adding it to the constraint store in case it is satisfiable.

Fig. 6.

Resolution transition system

When the head of the resolvent is a defined predicate, the call transition will replace it by its definition, properly encapsulated by a select state equipped with the permutation capturing argument order.

The select transition performs two tasks: first, it modifies the current constraint store adding the appropriate permutation and scoping ($n,\pi$); second, it selects the first clause for proof search.

The return transitions will either propagate failure or undo the permutation and scoping performed at call time.

sub, backtrack, and seq are structural transitions with a straightforward interpretation from a proof search perspective.

Then, we have the following lemma:

Lemma 9

For all queries $\langle {\varvec{p}}|\varphi \rangle _n$, the first successful $\xrightarrow {}_l$ derivation using a SLD strategy uniquely corresponds to a $\xrightarrow {}_p$ derivation:

for some resolution state PS.

Corollary 1

The transition systems of Definition 10 and Fig. 6 are answer-equivalent: for any query they return the same answer constraint.

With this lemma in place, the proof of Theorem 3 is completed by showing a simulation between the resolution system and a transition system induced by relation rewriting.

6 Related and Future Work

Previous Work: The paper is the continuation of previous work in [4, 10, 15] considerably extended to include constraint logic programming, which requires a different translation procedure and a different rewriting system.

In particular, the presence of constraints in this paper permits a different translation of the Clark completion of a program and plays a crucial role in the proof of completeness, which was missing in earlier work. The operational semantics is also new.

Related Work: A number of solutions have been proposed to the syntactic specification problem. There is an extensive literature treating abstract syntax of logic programming (and other programming paradigms) using encodings in higher-order logic and the lambda calculus [18], which has been very successful in formalizing the treatment of substitution, unification and renaming of variables, although it provides no special framework for the management and progressive instantiation of logic variables, and no treatment of constraints. Our approach is essentially orthogonal to this, since it relies on the complete elimination of variables, substitution, renaming and, in particular, existentially quantified variables. Our reduction of management of logic variables to variable free rewriting is new, and provides a complete solution to their formal treatment.

An interesting approach to syntax specification is the use of nominal logic [5, 22] in logic programming, another, the formalization of logic programming in categorical logic [1, 2, 8, 13, 19] which provides a mathematical framework for the treatment of variables, as well as for derivations [14]. None of the cited work gives a solution that simultaneously includes logic variables, constraints and proof search strategies however.

Bellia and Occhiuto [3] have defined a new calculus, the C-expression calculus, to eliminate variables in logic programming. We believe our translation into the well-understood and scalable formalism of relations is more applicable to extensions of logic programming. Furthermore the authors do not consider constraints.

Future Work: A complementary approach to this work is the use of category theory, in particular the Freyd’s theory of tabular allegories [9] which extends the relation calculus to an abstract category of relations providing native facilities for generation of fresh variables and a categorical treatment of monads. A first attempt in this direction has been published by the authors in [11]. It would be interesting to extend the translation to hereditarily Harrop or higher order logic [17] by using a stronger relational formalism, such as Division and Power Allegories. Also, the framework would yield important benefits if it was extended to include relation and set constraints explicitly.

7 Conclusion

We have developed a declarative relational framework for the compilation of Constraint Logic programming that eliminates logic variables and gives an algebraic treatment of program syntax. We have proved operational equivalence to the classical approach. Our framework has several significant advantages.

Programs can be analyzed, transformed and optimized entirely within this framework. Execution is carried out by rewriting over relational terms. In these two ways, specification and implementation are brought much closer together than in the traditional logic programming formalism.