1:
2: \documentclass{article}
3:
4: %%%%% Dimensioni
5: \newcommand{\delt}{1.2}
6: \setlength{\textwidth}{\delt\textwidth}
7: \setlength{\textheight}{\delt\textheight}
8: \setlength{\topmargin}{-\delt cm}
9: \setlength{\oddsidemargin}{0.5 cm}
10: \setlength{\evensidemargin}{\oddsidemargin}
11: \newcommand{\scala}{1.2}
12: %%%%%%
13:
14: \usepackage{amsfonts,latexsym,upref}
15: %%% Macro per rappresentante canonico
16: \newcommand{\rappr}[1]{
17: \raisebox{-0.5 ex}[0 ex][0 ex]
18: {\begin{picture}(10,10)(0,0)
19: \put(5,5){\circle{10}}
20: \put(3,2.5){${#1}$}
21: \end{picture}}}
22: \newcommand{\rapprmedio}[1]{
23: \raisebox{-0.5 ex}[0 ex][0 ex]
24: {\begin{picture}(14,10)(0,0)
25: \put(7,5){\oval(14,10)}
26: \put(3,2.5){${#1}$}
27: \end{picture}}}
28: \newcommand{\rapprmediocre}[1]{
29: \raisebox{-0.5 ex}[0 ex][0 ex]
30: {\begin{picture}(22,10)(0,0)
31: \put(11,5){\oval(22,10)}
32: \put(3,2.5){${#1}$}
33: \end{picture}}}
34: \newcommand{\rapprlungo}[1]{
35: \raisebox{-0.5 ex}[0 ex][0 ex]
36: {\begin{picture}(70,10)(0,0)
37: \put(35,5){\oval(70,10)}
38: \put(3,2.5){${#1}$}
39: \end{picture}}}
40:
41: %%% Macro per nomi teorie %%%%%%%%%%%%%
42: \newcommand{\lst}{{\it List}}
43: \newcommand{\bag}{{\it MSet}}
44: \newcommand{\bagi}{{\it MSet}^i}
45: \newcommand{\clist}{{\it CList}}
46: \newcommand{\set}{{\it Set}}
47: %%%%%%%%%%%%%
48: %%%\newcommand{\HF}{\mathbb{HF}}
49: \newcommand{\Th}{\mathbb{T}}
50: \newcommand{\T}{{\cal T}}
51: \newcommand{\size}{\mathit{size}}
52: \newcommand{\false}{{\tt false}}
53: \newcommand{\true}{{\tt true}}
54: \newcommand{\nil}{{\tt nil}}
55: \newcommand{\e}{\emptyset}
56: %%%%%%%%%%
57: \newcommand{\mo}{\{ \hspace*{-0.55ex} [\,}
58: \newcommand{\mc}{\,] \hspace*{-0.55ex} \}}
59: \newcommand{\clo}{[ \hspace*{-0.35ex} [\,}
60: \newcommand{\clc}{\,] \hspace*{-0.35ex} ]}
61: %%%%%%%%%%
62: \newcommand{\lf}{[\, \cdot \,|\,\cdot \,]}
63: \newcommand{\lcf}{\clo\,\cdot\,|\,\cdot\,\clc}
64: \newcommand{\sef}{\{ \,\cdot\,|\,\cdot\,\}}
65: \newcommand{\mf}{\mo\,\cdot\,|\,\cdot\,\mc}
66: \newcommand{\cons}{{\tt cons_\Th}(\,\cdot\,,\,\cdot\,)}
67: \newcommand{\w}{{\tt with}}
68: %%%%%%%%%%
69: \newcommand{\nat}{\mathbb{N}}
70: \newcommand{\dentro}{\phantom{a}}
71: \newcommand{\kernel}{{\sf ker}}
72: \newcommand{\fail}{\tt fail}
73: \newcommand{\vars}{FV}
74: \newcommand{\multi}{\mo\cdot\,|\,\cdot\mc}
75: %\newcommand{\ucap}
76: % {{\cap}\hspace*{-1.38ex}{\mbox{\tiny +}\,}}
77: %\newcommand{\usetminus}{\setminus_{+}}
78: %\newcommand{\integer}{{\sf Z \hspace*{-1 ex} Z}}
79: %%%%%%%%%%%%%%%%%
80: \newcommand{\Base}{\noindent\mbox{\sc Basis.}~}
81: \newcommand{\Step}{\noindent\mbox{\sc Step.}~}
82: \newtheorem{theorem}{Theorem}[section]
83: \newtheorem{definition}[theorem]{Definition}
84: \newtheorem{lemma}[theorem]{Lemma}
85: \newtheorem{proposition}[theorem]{Proposition}
86: \newtheorem{corollary}[theorem]{Corollary}
87: \newtheorem{remark}[theorem]{Remark}
88: \newtheorem{example}[theorem]{Example}
89: %\newenvironment{proof}{\emph{Proof.~}~}
90: %{\hfill$\Box$\par \medskip \par}
91: \newcommand{\qed}{\hfill$\Box$\par\medskip\par}
92: \newenvironment{proof}
93: {\emph{Proof.~}~\baselineskip 8pt \small}
94: {\hfill$\Box$\par\medskip\par \baselineskip 12pt
95: \normalsize}
96: %%%%%%%%%%%%%%%%
97: \title{A uniform approach to constraint-solving for
98: lists, multisets, compact lists, and sets}
99: \author{{\sc Agostino Dovier}$^*$
100: \and {\sc Carla Piazza}\thanks{
101: Dip. di Matematica e Informatica,
102: Universit\`a di Udine.
103: Via delle Scienze 206,
104: 33100 Udine (Italy).
105: {\sf dovier$|$piazza@dimi.uniud.it}}
106: \and {\sc Gianfranco Rossi}\thanks{
107: Dip. di Matematica,
108: Universit\`a di Parma.
109: Via M. D'Azeglio 85/A,
110: 43100 Parma (Italy).
111: {{\sf gianfranco.rossi@unipr.it}}}
112: }
113:
114: \begin{document}
115:
116: \maketitle
117:
118: \vspace*{-4ex}
119:
120: \begin{abstract}
121: Lists, multisets, and sets are well-known data structures whose
122: usefulness is widely recognized in various areas of Computer
123: Science. These data structures have been analyzed from an
124: axiomatic point of view with a parametric approach
125: in~\cite{DPR98-fuin} where the relevant {unification algorithms}
126: have been developed. In this paper we extend
127: these results considering more general constraints including not
128: only equality but also membership constraints as well as their
129: negative counterparts.
130: \end{abstract}
131:
132: \begin{center}
133: {\small {\bf Keywords:} Membership and Equality Constraints, Lists,
134: Multisets, Compact Lists, Sets.}
135: \end{center}
136:
137: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
138: \section{Introduction}
139: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
140:
141: Programming and specification languages usually allow the user to
142: represent various forms of aggregates of data objects,
143: characterized by the way elements are organized and accessed. In
144: this paper we consider four different kinds of aggregates: lists,
145: multisets, compact lists, and sets. The basic difference between
146: them lies in the order and/or repetitions of their data objects.
147:
148: Importance of these forms of aggregates is widely recognized in
149: various areas of Computer Science. Lists are the classical example
150: used to introduce dynamic data structures in imperative
151: programming languages. They are the fundamental data structure in
152: functional and logic languages. Sets are the main data structure
153: used in specification languages (e.g., in Z~\cite{PST96}) and in
154: high-level declarative programming
155: languages~\cite{BNST91,JLP1,Ger97,HL94}; but also imperative
156: programming languages may take advantage from the set data
157: abstraction (e.g., SETL~\cite{SDDS86}). Multisets, often called
158: \emph{bags} in the literature, emerge as the most natural data
159: structure in several interesting
160: applications~\cite{BM93,GM96,TZO98}. A compact list is a list in
161: which contiguous occurrences of the same element are immaterial;
162: some possible application examples are suggested
163: in~\cite{DPR98-fuin}.
164:
165: \par\smallskip\par
166: \begin{minipage}[b]{0.4\textwidth}
167: %\begin{figure}[htb]
168: %%\renewcommand{\arraystretch}{\scala}
169: $$\begin{array}{crclc}
170: %\hline
171: &&\mbox{Sets}&&\\
172: &\nearrow&&\nwarrow&\\
173: &\mbox{Multisets}&&\mbox{Compact lists}&\\
174: &\nwarrow &&\nearrow&\\
175: &&\mbox{Lists}&&\\
176: %\hline
177: \end{array}$$
178: %\vspace{-5pt}\caption
179: \vspace{5pt}
180: \centerline{\label{lattice}The lattice of the four
181: aggregates}
182: %\vspace{5pt}
183: %\end{figure}
184: \end{minipage}
185: \phantom{aaa}
186: \begin{minipage}[b]{0.5\textwidth}
187: Lists, multisets, compact lists, and sets have been analyzed from
188: an axiomatic point of view and studied in the context of
189: (Constraint) Logic Programming (CLP)
190: languages~\cite{DPR98-fuin}---see figure on the left
191: %%%Figure~\ref{lattice}
192: for a lattice induced by their axiomatizations. In this context,
193: these aggregates are conveniently represented as terms, using
194: different constructors.
195: \end{minipage}
196: \par\smallskip\par
197:
198:
199: The theories studied deal with aggregate constructor symbols as
200: well as with an arbitrary number of free constant and function
201: symbols. \cite{DPR98-fuin} focuses on \emph{equality} between
202: terms in each of the four theories. This amounts to solve the
203: unification problems in the equational theories describing the
204: properties of the four considered aggregates. Unification
205: algorithms for all of them are provided in~\cite{DPR98-fuin};
206: NP-unification algorithms for sets and multisets are also
207: presented in~\cite{ADR99,DV99}. In Section~\ref{teorie} and
208: \ref{sec.unif} we recall the main results of~\cite{DPR98-fuin}.
209:
210:
211: In this paper we extend the results of~\cite{DPR98-fuin} to the
212: case of more general \emph{constraints}. The constraints we
213: consider are conjunctions of literals based on both equality and
214: membership predicate symbols. For the case of sets, the problem
215: is studied in~\cite{DPPR00,DR93}. In Section~\ref{privileged} we
216: define the notion of constraints and we identify the privileged
217: models for the axiomatic theories used to describe the
218: considered aggregates. We show that satisfiability of constraints
219: in those models is equivalent to satisfiability in any model. We
220: then define the notion of solved form for constraints, and we
221: prove that solved form constraints are satisfiable over the
222: proposed privileged models. In Section~\ref{constraint-rewriting}
223: we describe, for each kind of aggregate, the constraint rewriting
224: procedures used to eliminate all atomic constraints not in solved
225: form. We use these procedures in Section~\ref{constraint-solving}
226: to solve the general satisfiability problem for the considered
227: constraints. Some conclusions are drawn in
228: Section~\ref{conclusions}. Throughout the paper the word
229: \emph{aggregate} is used for denoting generically one of the four
230: considered aggregates, namely lists, multisets, compact lists,
231: and sets.
232:
233:
234:
235: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
236: \section{Preliminary Notions}
237: \label{preliminari}
238: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
239:
240: Basic knowledge of first-order logic
241: (e.g.,~\cite{CK73,End73}) is assumed; in this section we recall
242: some notions and we fix some notations that we will use throughout
243: the paper.
244:
245: \medskip
246:
247: A first-order language ${\cal L} = \langle
248: \Sigma, {\cal V}\rangle$ is defined by a \emph{signature} $\Sigma
249: = \langle {\cal F}, \Pi \rangle$ composed by a set ${\cal F}$ of
250: constant and function symbols, by a set $\Pi$ of predicate
251: symbols, and by a denumerable set $\cal V$ of variables. A
252: \emph{(first-order) theory} $\T$ on a language $\cal L$ is a set
253: of closed first-order formulas of $\cal L$ such that each closed
254: formula of $\cal L$ which can be deduced from $\T$ is in $\T$\/. A
255: \emph{(first-order) set of axioms} $\Theta$ on $\cal L$ is a set of
256: closed first-order formulas of $\cal L$\/. A set of axioms $\Theta$ is
257: said to be an \emph{axiomatization} of $\T$ if $\T$ is the
258: smallest theory such that $\Theta\subseteq \T$\/. Sometimes we use
259: the term \emph{theory} also to refer to an axiomatization of the
260: theory. When $\Theta = \{\varphi_1,\dots,\varphi_n\}$,
261: and $A_1,\dots,A_n$ are the names of the formulas
262: $\varphi_1,\dots,\varphi_n$, we refer to that theory simply
263: as: $A_1\cdots A_n$.
264:
265: \medskip
266:
267: Capital letters $X,Y,Z$\/, etc.\ are used to represent variables,
268: $f$\/, $g$\/, etc. to represent constant and function symbols, and $p$\/,
269: $q$\/, etc. to represent predicate symbols. We also use $\bar X$
270: to denote a (possibly empty) sequence of variables. $T({\cal
271: F},{\cal V})$ ($T({\cal F})$) denotes the set of first-order terms
272: (resp., ground terms) built from $\cal F$ and ${\cal V}$ (resp.,
273: $\cal F$). The function $\size:T({\cal F},{\cal V})\longrightarrow
274: \nat$ returns the number of occurrences of constant and function
275: symbols in a term. Given a term $t$, with $\vars(t)$ we denote
276: the set of all variables
277: which occur in the term $t$.
278: Given a sequence of terms $t_1,\ldots,t_n$\/,
279: $\vars(t_1,\ldots,t_n)$ is the set $\bigcup_{i=1}^n \vars(t_i)$.
280: When the context
281: is clear, we use $\bar t$ to denote a sequence $t_1,\ldots,t_n$ of
282: terms. If $\varphi$ is a first-order formula, $\vars(\varphi)$
283: denotes the set of free variables in $\varphi$\/. $\exists
284: \varphi$ ($\forall \varphi$) is used to denote the existential
285: (universal) closure of the formula $\varphi$\/, namely $\exists
286: X_1 \cdots \exists X_n\, \varphi$ ($\forall X_1 \cdots \forall X_n
287: \, \varphi$\/), where $\{ X_1 ,\dots ,X_n \} = \vars(\varphi)$\/.
288: An \emph{equational axiom} is a formula of the form $\forall
289: X_1\cdots\forall X_n (\ell = r)$ where $\vars(\ell=r) =
290: \{X_1,\dots,X_n\}$. An \emph{equational theory} is an
291: axiomatization whose axioms are equational axioms.
292:
293: \medskip
294:
295: Given a first-order theory ${\cal L} = \langle \Sigma, {\cal
296: V}\rangle$, a $\Sigma$-\emph{structure} is a pair $\mathcal{A} =
297: \langle A, I \rangle$ where $A$ is a non-empty set (the domain)
298: and $I$ is the interpretation function of all constant, function,
299: and predicate symbols of $\Sigma$ on $A$. A \emph{valuation}
300: $\sigma$ is a function from a subset of the set of variables
301: ${\cal V}$ to $A$. $\sigma$ and $I$ determine uniquely a function
302: $\sigma^{I}$ from the set of first-order terms over $\cal L$ to
303: $A$ and a function from the set of formulas over $\cal L$ to the
304: set $\{\false,\true\}$. When the $\Sigma$-structure is fixed,
305: $\sigma^I$ depends only by $\sigma$. Thus, with abuse of notation,
306: $\sigma^I$ is simply written as $\sigma$. Given a
307: $\Sigma$-structure $\cal A$, a valuation $\sigma$ is said a
308: \emph{successful valuation} of $\varphi$ if ${\sigma}(\varphi) =
309: \true$. This fact is also denoted by: ${\mathcal A}\models
310: \sigma^{I}(\varphi)$. A formula $\varphi$ is \emph{satisfiable}
311: in $\mathcal{A}$ if there is a valuation
312: $\sigma:\vars(\varphi)\longrightarrow A$ such that $\mathcal{A}
313: \models \sigma(\varphi)$. In this case we say that ${\mathcal
314: A}\models \exists\varphi$. We say that ${\mathcal A}\models
315: \varphi$ if for every valuation $\sigma$ from $\vars(\varphi)
316: \longrightarrow A$ it holds that $\mathcal{A} \models
317: \sigma(\varphi)$. A formula $\varphi$ is \emph{satisfiable} in
318: $\mathcal{A}$ if there is a valuation
319: $\sigma:\vars(\varphi)\longrightarrow A$ such that $\mathcal{A}
320: \models \sigma(\varphi)$. In this case we say that ${\mathcal
321: A}\models \exists\varphi$. We remind that a formula is
322: satisfiable in a $\Sigma$-structure $\mathcal{A}$ if and only if
323: its existential closure is satisfiable in $\mathcal{A}$. Two
324: formulas $C_1$ and $C_2$ are \emph{equi-satisfiable} in
325: $\mathcal{A}$ if: $C_1$ is satisfiable in $\mathcal{A}$ if and
326: only if $C_2$ is satisfiable in $\mathcal{A}$. A structure $\cal
327: A$ is a \emph{model} of a theory $\cal T$ if $\mathcal{A} \models
328: \varphi$ for all $\varphi$ in $\cal T$. We say that ${\cal T}
329: \models \varphi$ if ${\cal A} \models \varphi$ for all models
330: $\cal A$ of $\cal T$.
331:
332:
333:
334:
335: \section{The Theories} \label{teorie}
336:
337: For each aggregate considered, we assume that
338: $\Pi$ is $\{ = , \in\}$ and ${\cal F}$ contains the constant
339: symbol $\nil$\/ and exactly one among the binary function symbols:
340: $$\begin{array}{clccl}
341: {\lf} & \mbox{for lists,} & \phantom{aaaa} &
342: \mf & \mbox{for multisets,}\\
343: \lcf & \mbox{for compact lists,}&&
344: \sef & \mbox{for sets,}
345: \end{array}$$
346: Moreover, each signature can contain an arbitrary number of other
347: constant and function symbols.
348: The four function symbols above are referred as the \emph{aggregate
349: constructors}. The empty list, multiset, compact list, and set are
350: all denoted by the constant symbol $\nil$\/. We use simple
351: syntactic notations for terms built using these symbols. In
352: particular, the list
353: $[\,s_1\,|\,[\,s_2\,|\,\cdots\,[\,s_n\,|\,t\,] \cdots ]]$ will be
354: denoted by $[s_1,\dots,s_n\,|\,t]$ or simply by $[s_1,\dots,s_n]$
355: when $t$ is $\nil$\/. The same conventions will be exploited also
356: for the other aggregates.
357:
358:
359: \subsection{Lists}\label{hybrid.lists}
360:
361: The language ${\cal L}_\lst$ is defined as $\langle
362: \Sigma_\lst,{\cal V}\rangle$, where $\Sigma_\lst=\langle {\cal
363: F}_\lst,\Pi\rangle$, $\lf$ and $\nil$ are in ${\cal F}_\lst$, and
364: $\Pi=\{=,\in\}$\/. We recall that ${\cal
365: F}_\lst$ can contain other constant and function symbols.
366: The first-order theory \lst\ for lists is shown
367: in the figure below.
368: %\begin{figure}[htb]
369: $${\renewcommand{\arraystretch}{\scala}
370: \begin{array}{|crcl|}
371: \hline
372: (K) & \forall x\,y_1\cdots y_n & (x \not\in
373: f(y_1,\dots,y_n)\,) & f \in {\cal F}_\lst, f \mbox{ is not }
374: [\,\cdot\,|\,\cdot\,]\\
375: (W) & \forall y \,v \, x \, & (x \in [\,y\,|\,v\,]
376: \leftrightarrow x \in v \vee x = y) & \\
377: (F_1) & \forall x_1\cdots x_n y_1 \cdots y_n
378: & \left(\begin{array}{c}
379: f(x_1,\dots,x_n) = f(y_1,\dots,y_n)\\
380: \rightarrow
381: x_1 = y_1 \wedge \cdots \wedge x_n = y_n
382: \end{array}\right)
383: & f \in {\cal F}_\lst \\
384: (F_2) & \forall x_1\cdots x_m y_1 \cdots y_n
385: & f(x_1,\dots,x_m) \not= g(y_1,\dots,y_m)
386: & f,g\in{\cal F}_\lst, f \mbox{ is not } g\\
387: (F_3) & \forall x &
388: (x \not= t[x]) &\\
389: & \multicolumn{3}{l|}{\mbox{\em where $t[x]$ denotes
390: a term $t$, having $x$ as proper subterm}}\\
391: \hline
392: \end{array}}$$
393: %%\end{figure}
394:
395: The three axiom schemata $(F_{1}),(F_{2})$\/, and $(F_{3})$
396: (called freeness axioms, or
397: Clark's equality axioms---see~\cite{Cla78}) have been
398: originally introduced by Mal'cev in~\cite{Mal71}.
399: Observe that $(F_1)$ holds for
400: $[\,\cdot\,|\,\cdot\,]$ as a particular case.
401: $(F_3)$ states that there is no term
402: which is also a subterm of itself.
403: Note that $(K)$ implies that $\forall x \, ( x \notin \nil)$\/.
404:
405: \subsection{Multisets}\label{sub.bags}
406:
407: The language ${\cal L}_\bag$ is defined as $\langle
408: \Sigma_\bag,{\cal V}\rangle$, where $\Sigma_\bag=\langle {\cal
409: F}_\bag,\Pi\rangle$, $\mf$ and $\nil$ are in ${\cal F}_\bag$, and
410: $\Pi=\{=,\in\}$\/. A theory of multisets---called \bag---can be
411: simply obtained from the theory of lists shown above. The
412: constructor $[\,\cdot\,|\,\cdot\,]$ is replaced by the constructor
413: $\mo\,\cdot\,|\,\cdot\,\mc$ in axiom schema $(K)$ and axiom $(W)$.
414: The behavior of this new symbol is regulated by the following
415: equational axiom
416: $$\renewcommand{\arraystretch}{\scala}
417: \begin{array}{|cclr|}
418: \hline
419: (E_p^m) & \dentro &
420: \forall x y z \,\,\, \mo x,y\,|\,z\mc = \mo y,x\,|\,z\mc &
421: (\emph{permutativity})\\
422: \hline
423: \end{array}$$
424: which, intuitively, states that the order of elements in a
425: multiset is immaterial. Axiom schema $(F_1)$ does not hold for
426: multisets, when $f$ is $\mo\,\cdot\,|\,\cdot\,\mc$\/. It is
427: replaced by axiom schemata $(F_1^{m})$:
428: $$\renewcommand{\arraystretch}{\scala}
429: \begin{array}{|clrl|}
430: \hline
431: (F_1^m) & \dentro & \forall x_1\cdots x_n y_1 \cdots y_n
432: & \left(\begin{array}{c}
433: f(x_1,\dots,x_n) = f(y_1,\dots,y_n)\\
434: \rightarrow
435: x_1 = y_1 \wedge \cdots \wedge x_n = y_n
436: \end{array}\right)\\
437: & \multicolumn{3}{l|}{\mbox{\em for any $f \in {\cal F}_\bag$,
438: $f$ distinct from $\mo\,\cdot\,|\,\cdot\,\mc$\/}}\\
439: \hline
440: \end{array}$$
441: In the theory $KWE_p^mF_1^mF_2F_3$\/, however, we lack in a general
442: criterion for establishing equality and disequality between
443: multisets. To obtain it, the following \emph{multiset
444: extensio\-na\-li\-ty\/} property is introduced: \emph{Two
445: multisets are equal if and only if they have the same number of
446: occurrences of each element, regardless of their order.} The axiom
447: proposed in~\cite{DPR98-fuin} to force this property is the
448: following:
449: $$
450: \renewcommand{\arraystretch}{\scala}
451: \begin{array}{|cll|}
452: \hline
453: (E^m_k) &\dentro &
454: \forall y_1 y_2 v_1 v_2\,
455: \left(\begin{array}{l}
456: \mo y_1\,|\,v_1 \mc = \mo y_2\,|\,v_2 \mc \:\:
457: \leftrightarrow \\
458: \phantom{aaaaaaaa}
459: (y_1 = y_2 \wedge v_1 = v_2) \vee\\
460: \phantom{aaaaaaaa}
461: \exists z\,(v_1 = \mo y_2\,|\,z \mc \wedge
462: v_2 = \mo y_1\,|\,z \mc )
463: \end{array}\right)\\
464: \hline
465: \end{array}$$
466: $(E^m_k)$ implies $(E^m_p)$\/.
467: Axiom schema $(F^m_3)$ is also introduced:
468: $$
469: \renewcommand{\arraystretch}{\scala}
470: \begin{array}{|cll|}
471: \hline
472: (F_3^m) &
473: \forall x_1\cdots x_m y_1 \cdots y_n x\, &
474: \left( \begin{array}{l}
475: \mo x_1,\dots,x_m \,|\, x \mc =
476: \mo y_1,\dots,y_n\,|\,x \mc \\
477: \rightarrow \mo x_1,\dots,x_m \mc =
478: \mo y_1,\dots,y_n \mc
479: \end{array} \right) \\
480: \hline
481: \end{array}$$
482:
483:
484: Axiom schema $(F_3^m)$ reinforces the acyclicity condition
485: imposed by standard axiom schema $(F_3)$. As a matter of fact, $X
486: \neq \mo a , b , b \,|\, X\mc$ follows from $(F_3)$. Axiom schema
487: $(F_3^m)$ states that, since $\mo a , a , b \mc \neq \mo a , b ,b
488: \mc$, then $\mo a , a , b\,|\,X \mc \neq \mo a , b ,b \,|\,X
489: \mc$. This property is not a consequence of the the remaining
490: part of the theory.
491:
492: \subsection{Compact Lists}\label{compact}
493:
494: The language ${\cal L}_\clist$ is defined as ${\cal
495: L}_\clist=\langle \Sigma_\clist,{\cal V}\rangle$, where
496: $\Sigma_\clist=\langle {\cal F}_\clist,\Pi\rangle$, $\lcf$ and
497: $\nil$ are in ${\cal F}_\clist$, and $\Pi=\{=,\in\}$\/. Similarly
498: to multisets, the theory of \emph{compact lists}---called
499: \clist---is obtained from the theory of lists with only a few
500: changes. The list constructor symbol is replaced by the binary
501: compact list constructor $\clo\,\cdot\,|\,\cdot\,\clc$ in $(K)$
502: and $(W)$. The behavior of this symbol is regulated by the
503: equational axiom
504: $$\renewcommand{\arraystretch}{\scala}
505: \begin{array}{|cclr|}
506: \hline
507: (E_a^c) & \dentro &
508: \forall x y \,\,\, \clo x,x\,|\,y\clc = \clo x\,|\,y\clc &
509: (\emph{absorption}) \\
510: \hline
511: \end{array}$$
512: which, intuitively, states that contiguous duplicates in a
513: compact list are immaterial.
514: As for multisets, we introduce a general criterion for establishing
515: both equality and disequality between compact lists.
516: This is obtained by introducing the following axiom:
517: $$\renewcommand{\arraystretch}{\scala}
518: \begin{array}{|clll|}
519: \hline
520: (E^c_k) &\dentro &
521: \forall y_1 y_2 v_1 v_2 &
522: \left(\begin{array}{l}
523: \clo y_1\,|\,v_1 \clc = \clo y_2\,|\,v_2 \clc \:\:
524: \leftrightarrow \\
525: \phantom{aaaaaaaa}
526: (y_1 = y_2 \wedge v_1 = v_2) \vee\\
527: \phantom{aaaaaaaa}
528: (y_1 = y_2 \wedge v_1 = \clo y_2\,|\,v_2 \clc) \vee\\
529: \phantom{aaaaaaaa}
530: (y_1 = y_2 \wedge \clo y_1\,|\,v_1 \clc = v_2) \\
531: \end{array}\right) \\
532: \hline
533: \end{array}$$
534: $(E^c_a)$ is implied by $(E^c_k)$.
535: Axiom schema $(F_1)$ is replaced by axiom schema $(F_1^c)$:
536: $$\renewcommand{\arraystretch}{\scala}
537: \begin{array}{|clrl|}
538: \hline
539: (F_1^c) & \dentro & \forall x_1\cdots x_n y_1 \cdots y_n
540: & \left(\begin{array}{c}
541: f(x_1,\dots,x_n) = f(y_1,\dots,y_n)\\
542: \rightarrow
543: x_1 = y_1 \wedge \cdots \wedge x_n = y_n
544: \end{array}\right)\\
545: & \multicolumn{3}{l|}{\mbox{\em for any $f \in {\cal F}_\clist$,
546: $f$ distinct from $\clo\,\cdot\,|\,\cdot\,\clc$\/}}\\
547: \hline
548: \end{array}$$
549: The freeness axiom $(F_3)$ needs to be
550: suitably modified. The introduction of $(F_3)$ is motivated by
551: the requirement of finding solutions to equality constraints
552: over $\Sigma$-structures with the domain built based on
553: Herbrand Universe, where each term is
554: modeled by a finite tree. As opposed to lists and multisets, an
555: equation such as
556: $X = \clo \nil\,|\, X\clc$ admits a solution in these structures.
557: Precisely, a solution that binds $X$ to the term
558: $\clo \nil\,|\,t \clc$, where $t$ is any term.
559: Therefore, as explained in~\cite{DPR98-fuin},
560: axiom schema $(F_3)$ should be weakened and, thus, replaced by:
561: $$
562: \renewcommand{\arraystretch}{\scala}
563: \begin{array}{|ccll|}
564: \hline
565: (F_3^c) & \dentro & \forall x & (x \neq t[x])\\
566: & \multicolumn{3}{l|}{\mbox{\em unless: $t$ is of the form
567: $\clo t_1,\dots,t_n\,|\,x \clc$\/, with $n > 0$,}}\\
568: & \multicolumn{3}{l|}{\mbox{\em $x \notin \vars(t_1,\dots,t_n)$\/, and $t_1= \cdots = t_n$}}\\
569: \hline
570: \end{array}$$
571:
572: \subsection{Sets}\label{Sets}
573:
574: The language ${\cal L}_\set$ is defined as
575: ${\cal L}_\set=\langle \Sigma_\set,{\cal V}\rangle$, where
576: $\Sigma_\set=\langle {\cal
577: F}_\set,\Pi\rangle$,
578: $\sef$
579: and $\nil$
580: are in ${\cal F}_\set$, and
581: $\Pi=\{=,\in\}$\/.
582: The last theory we consider is the simple theory of sets \set.
583: Sets have both the \emph{permutativity\/} and the
584: \emph{absorption properties\/}
585: which, in the case of $\sef$\/,
586: can be rewritten as follows:
587: $$\renewcommand{\arraystretch}{\scala}
588: \begin{array}{|ccrcl|}
589: \hline
590: (E_p^s) & \dentro &
591: \forall x y z \,\,\, \{ x,y\,|\,z\} & = & \{ y,x\,|\,z\}
592: \\
593: (E_a^s) & \dentro &
594: \forall x y \,\,\, \{ x,x\,|\,y\} & = & \{ x\,|\,y\}\\
595: \hline
596: \end{array}$$
597: A criterion for testing equality (and disequality)
598: between sets is obtained by merging
599: the multiset equality axiom $(E^m_k)$ and the compact
600: list equality axiom $(E^c_k)$\/:
601: $$\renewcommand{\arraystretch}{\scala}
602: \begin{array}{|clll|}
603: \hline
604: (E^s_k) &\dentro &
605: \forall y_1 y_2 v_1 v_2 &
606: { \left(\begin{array}{l}
607: \{ y_1\,|\,v_1 \} = \{ y_2\,|\,v_2 \} \:\:
608: \leftrightarrow \\
609: \phantom{aaaaaaaa}
610: (y_1 = y_2 \wedge v_1 = v_2) \vee\\
611: \phantom{aaaaaaaa}
612: (y_1 = y_2 \wedge v_1 = \{ y_2\,|\,v_2 \}) \vee\\
613: \phantom{aaaaaaaa}
614: (y_1 = y_2 \wedge \{ y_1\,|\,v_1 \} = v_2) \vee\\
615: \phantom{aaaaa}\exists k \:( v_1 = \{y_2\,|\,k\} \wedge
616: v_2 = \{y_1 \,|\, k \} )
617: \end{array}\right) }\\
618: \hline
619: \end{array}
620: $$
621: According to $(E^s_k)$ duplicates and ordering of elements in
622: sets are immaterial. Thus, $(E^s_k)$ implies the equational axioms
623: $(E^s_p)$ and $(E^s_a)$\/. In~\cite{DPR98-fuin} it is also proved
624: that they are equivalent when domains are made by terms. The
625: theory \set\ also contains axioms $(K)$\/, $(W)$ with
626: $[\,\cdot\,|\,\cdot\,]$ replaced by $\sef$\/, and axiom schemata
627: $(F_2)$ Axiom schema $(F_1)$ is replaced by:
628: $$\renewcommand{\arraystretch}{\scala}
629: \begin{array}{|clrl|}
630: \hline
631: (F_1^s) & \dentro & \forall x_1\cdots x_n y_1 \cdots y_n
632: & \left(\begin{array}{c}
633: f(x_1,\dots,x_n) = f(y_1,\dots,y_n)\\
634: \rightarrow
635: x_1 = y_1 \wedge \cdots \wedge x_n = y_n
636: \end{array}\right)\\
637: & \multicolumn{3}{l|}{\mbox{\em for any $f \in {\cal F}_\set$,
638: $f$ distinct from $\{\,\cdot\,|\,\cdot\,\}$\/}}\\
639: \hline
640: \end{array}$$
641: The modification of axiom schema $(F_3)$ for sets, instead,
642: simplifies the one used for compact lists:
643: $$
644: \renewcommand{\arraystretch}{\scala}
645: \begin{array}{|ccll|}
646: \hline
647: (F_3^s) & \dentro & \forall x & (x \not= t[x])\\
648: & \multicolumn{3}{l|}{\mbox{\em unless: $t$ is of the form
649: $\{ t_1,\dots,t_n\,|\,x \}$ and
650: $x \in \vars(t_1,\dots,t_n)$}}\\
651: \hline
652: \end{array}$$
653:
654: \subsection{Equational theories}\label{Sunto}
655:
656: As we have seen in this section, each aggregate constructor is
657: precisely characterized by zero, one or 2 equational axioms. We
658: define the four corresponding \emph{equational theories} as
659: follows:
660: \begin{center}
661: \begin{tabular}{|rl|}
662: \hline
663: $E_\lst$ & the empty theory for \lst,\\
664: $E_\bag$ & consisting of the \emph{Permutativity}
665: axiom $(E^m_p)$ for \bag, \\
666: $E_\clist$ & consisting of the \emph{Absorption}
667: axiom $(E^c_a)$ for \clist,\\
668: $E_\set$ & consisting of both the
669: \emph{Permutativity} $(E^s_p)$ and
670: \emph{Absorption} $(E^s_a)$ axioms for \set.\\
671: \hline
672: \end{tabular}
673: \end{center}
674: Relationships between these equational theories,
675: $\Sigma$-structures, and the proposed first-order theories for
676: aggregates are explained in the next section.
677: Figure~\ref{sommario} summarizes the axiomatizations of the four
678: theories.
679:
680:
681: \begin{figure}[t]
682: \begin{center}
683: {\small
684: %\renewcommand{\arraystretch}{\scala}
685: \begin{tabular}{c|c|c|c|c|c|c||c|c|c}
686: Name & empty & with & \multicolumn{2}{|c|}{Equality} &
687: Herbrand & Acycl. & Perm. & Abs. & Equational Name \\
688: \hline
689: \lst & $(K)$ & $(W)$ & \multicolumn{2}{|c|}{$(F_1)$} &
690: $(F_2)$ & $(F_3)$ & & & $E_\lst$ \\
691: \hline
692: \bag & $(K)$ & $(W)$ & $(E^m_k)$ & $(F^m_1)$ &
693: $(F_2)$ & $(F_3)$ & $(E^m_p)$ & & $E_\bag$\\
694: \hline
695: \clist & $(K)$ & $(W)$ & $(E^c_k)$ & $(F^c_1)$ &
696: $(F_2)$ & $(F^c_3)$ & & $(E^c_a)$ & $E_\clist$\\
697: \hline
698: \set & $(K)$ & $(W)$ & $(E^s_k)$ & $(F^s_1)$ &
699: $(F_2)$ & $(F^s_3)$ & $(E^s_p)$ & $(E^s_a)$ & $E_\set$\\
700: \hline
701: \end{tabular}}
702: \end{center}
703: \caption{\label{sommario}Axioms for the four theories}
704: \end{figure}
705:
706: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
707: \section{Constraints, Privileged Models, and Solved Form}
708: \label{privileged}
709: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
710:
711: In this section we introduce the privileged models for the
712: four theories introduced in the previous section. These models
713: are used to testing satisfiability of the particular kind of
714: formulas we are concerned with, namely, \emph{constraints}. We
715: then show that the models and the theories defined in the
716: previous section \emph{correspond} on the class of constraints
717: considered. Moreover, we give a general notion of \emph{solved
718: form} for constraints, and we prove that a solved form constraint
719: is satisfiable in the corresponding privileged model.
720:
721: \begin{definition}[Constraints] \label{constraintdef}
722: Let $\Th$ be either $\lst$ or $\bag$ or $\clist$ or $\set$\/. A
723: \emph{$\Th$-constraint} $C_\Th$ is a conjunction of atomic ${\cal
724: L}_\Th$-formulas or negation of atomic ${\cal L}_\Th$-formulas of
725: the form $s \mathbin{\pi} t$,
726: where $\mathbin{\pi}\in \Pi$\/,
727: and $s,t \in T({\cal F}_{\Th},{\cal V})$.
728: \end{definition}
729:
730:
731: Throughout the paper we will use the following terminology to
732: refer to particular kinds of constraints: \emph{equality} (resp.,
733: \emph{disequality}) \emph{constraints} are conjunctions of atomic
734: formulas of the form $s = t$ (resp., $s \neq t$).
735: \emph{Membership} (resp., \emph{not-membership}) constraints are
736: conjunctions of membership atoms (resp., membership negative
737: literals), i.e. formulas of the kind $s \in t$ (resp., $s\not\in
738: t$).
739:
740:
741: \subsection{Privileged Models}\label{privistru}
742:
743: As discussed in Section~\ref{Sunto}, each aggregate constructor
744: is precisely characterized by an equational theory, that we have
745: named $E_\lst$, $E_\bag$, $E_\clist$, and $E_\set$. Using the
746: appropriate equational theory we can define a privileged model
747: for the first-order theory $\lst$, $\bag$, $\clist$, and $\set$
748: for each aggregate. Each model is obtained as a partition of the
749: Herbrand Universe.
750:
751: \begin{definition}\label{defstruttura}
752: Let $\Th$ be $\lst$ (resp., $\bag$, $\clist$, or $\set$\/). A
753: \emph{privileged $\Sigma$-structure for $\Th$} is defined
754: as follows.
755: \begin{enumerate}
756: \item The \emph{domain} of the $\Sigma$-structure is the quotient
757: $T({\cal F}_\Th)/\equiv_\Th$ of the Herbrand Universe
758: $T({\cal F}_\Th)$
759: over the smallest congruence relation $\equiv_\Th$ induced
760: by the equational theory $ E_\Th$ on $T({\cal F}_\Th)$\/.
761: \item The interpretation of a term $t$ is its equivalence
762: class w.r.t.\ $\equiv_\Th$, denoted by $\rappr{t}$\/.
763:
764: \item $=$ is interpreted as the identity on the
765: domain $T({\cal F}_\Th)/\equiv_\Th$\/.
766:
767: \item The interpretation of membership is:
768: $ \rappr{t} \in \rappr{s} $ is \true\ if and only if there
769: is a term in $\rappr{s}$ of the form
770: $[ t_1,\dots,t_n , t\,|\,r ]$
771: (resp., $\mo t_1,\dots,t_n , t\,|\,r \mc$\/,
772: $\clo t_1,\dots,t_n , t\,|\,r \clc$\/,
773: or $ \{ t_1,\dots,t_n , t\,|\,r \}$\/)
774: for some terms $t_1,\dots,t_n,r$\/.
775: \end{enumerate}
776: \end{definition}
777:
778: It is easy to prove that the above defined $\Sigma$-structures
779: are in fact models of the corresponding theories.
780: In Lemma~\ref{versofacile} we prove this property for multisets.
781: >From now on, we will call the privileged $\Sigma$-structures above
782: defined \emph{privileged models} for $\lst$, $\bag$, $\clist$, and
783: $\set$. We refer to them as
784: $\cal LIST$, $\cal MSET$, $\cal CLIST$, and $\cal SET$\/,
785: respectively.
786:
787:
788: \begin{remark}\label{member set}
789: When $\rappr{s}$ is the class of a multiset (resp., a set),
790: since the permutativity property holds, the requirement for $
791: \rappr{t} \in \rappr{s} $ to be \true\ can be simplified to: $\mo
792: t\,|\,r \mc$ (resp., $ \{ t\,|\,r \}$) is in $ \rappr{s}$.
793: \end{remark}
794:
795: The following notion from~\cite{JM94}
796: is crucial for characterizing the above
797: privileged models.
798:
799: \begin{definition}%%[Correspondence]
800: Given a first-order language ${\cal L} = \langle \Sigma,
801: {\cal V} \rangle$,
802: a set of first-order formulas $\cal C$ on $\cal L$,
803: a theory $\T$ on $\cal L$, and a
804: $\Sigma$-structure ${\cal A}$\/,
805: $\T$ and $\cal A$ \emph{correspond} on the
806: set $\cal C$ if, for each $\varphi \in \cal C$\/, we have that $\T
807: \models \exists \varphi$ if and only if ${\cal A} \models
808: \exists \varphi$\/.
809: \end{definition}
810:
811: This property means that if $\varphi$ is an element of $\cal C$
812: and $\varphi$ is satisfiable in $\cal A$, then it is satisfiable
813: in all the models of $\T$\/. We prove the correspondence property
814: for our theories and the privileged models, when the class $\cal
815: C$ is the class of constraints defined in Definition
816: \ref{constraintdef}. We show below the proof of this result in the
817: case of the model $\cal MSET$ and the theory \bag. The other
818: cases are similar. In the proof we use some basic results which
819: can be found in the Appendix~\ref{modellistiche}
820: (Lemmas~\ref{logica}--\ref{versodifficile}).
821:
822: \begin{theorem}\label{corrispondenza}
823: The model $\cal MSET$ (resp., $\cal LIST$, $\cal CLIST$, $\cal
824: SET$\/) and the theory \bag\ (resp., \lst, \clist, and \set)
825: correspond on the class of \bag- (resp., \lst-, \clist-, and
826: \set-)constraints.
827: \end{theorem}
828: \begin{proof}
829: {F}rom Lemma~\ref{versofacile} it follows that
830: ${\cal MSET}$ is a model of \bag, namely that
831: if $C$ is a
832: first-order formula and $\bag\models C$\/, then ${\cal
833: MSET}\models C$\/.
834:
835: On the other hand, if $\exists C$ is a formula with only
836: existential quantifiers, then ${\cal MSET}\models \exists C$
837: if and only if there exists $\sigma$ such that ${\cal MSET}\models
838: \sigma(C)$\/.
839: Assume that ${\cal M}\models \sigma(C)$. From Lemmas~\ref{logica}
840: and~\ref{versodifficile}, we have that ${\cal M}\models
841: \exists C$ for all models ${\cal M}$ of \bag. This implies that
842: $\bag \models \exists C$\/.
843: \end{proof}
844:
845:
846: \subsection{Solved Form}
847:
848: Solved form constraints play a fundamental r\^ole in establishing
849: satisfiability of constraints in the corresponding privileged
850: model. The solved form is obtained by defining first a weaker
851: form, called the pre-solved form, and then by adding to this form
852: two further conditions.
853:
854: \begin{definition}%%[Pre-Solved Form]
855: \label{pre-solvedform}
856: A constraint $C = c_1 \wedge \cdots \wedge c_n$ is in
857: \emph{pre-solved form} if for $i \in \{1,\dots,n\}$, $c_i$ is in
858: \emph{pre-solved form in $C$}, i.e.\ in one of the following forms:
859: \begin{itemize}
860: \item $X = t$ and $X$ does not occur elsewhere in $C$
861: \item $t \in X$ and $X$ does not occur in $t$
862: \item $X \neq t$ and $X$ does not occur in $t$
863: \item $t \notin X$ and $X$ does not occur in $t$\/.
864: \end{itemize}
865: \end{definition}
866: %The asymmetry in the definition in the case of equality
867: %constraints is justified by the fact that, once we know
868: %the value of a variable $X$\/,
869: %we can safely remove it from the system.
870:
871: A constraint in pre-solved form is not guaranteed to be
872: satisfiable in the corresponding privileged model. For example, the
873: constraint $X \in Y \wedge Y \in X$ is in pre-solved form but it
874: is unsatisfiable in each of the privileged models $\cal LIST, MSET, CLIST$\/, and
875: $\cal SET$. The first condition we introduce below takes care of
876: this situation.
877:
878: \begin{definition}[Acyclicity Condition] Let $C$ be a pre-solved
879: form constraint and $C^{\in}$ be the part of $C$ containing only
880: membership constraints. Let ${\cal G}^{\in}_{C}$ be the directed
881: graph obtained as follows:
882: \begin{description}
883: \item[\emph{Nodes}.] Associate a distinct node to
884: each variable $X$ in $C^{\in}$\/.
885: \item[\emph{Edges}.] If $t \in X$ is in $C^{\in}$\/,
886: $\nu_1,\dots,\nu_n$ are the nodes
887: associated with the variables in $t$\/, and
888: $\mu$ is the node associated with the variable
889: $X$\/, then add the edges
890: $\langle \nu_1,\mu\rangle,\dots,\langle\nu_n,\mu\rangle$\/.
891: \end{description}
892: We say that a pre-solved form constraint $C$ is \emph{acyclic} if
893: ${\cal G}_{C}^{\in}$ is acyclic.
894: \end{definition}
895:
896: The acyclicity condition is not sufficient for satisfiability.
897: Consider the constraint $\{ A,B \} \in X \wedge \{ B,A \} \notin
898: X$. It is in pre-solved form and acyclic but unsatisfiable in all
899: the considered privileged models. Conversely, the constraint $\{
900: A \} \in X \wedge \{ a \} \notin X$ is satisfiable in $\cal SET$
901: (e.g., $A = b, X = \{\{b\}\}$). We observe that whenever there
902: are two constraints $t \in X$ and $t' \not\in X$ in $C$ such that
903: $t$ and $t'$ are equivalent terms in the equational theory
904: $E_\Th$, the constraint $C$ is unsatisfiable.
905:
906: This analysis, however, does not cover all the possible cases in
907: which an acyclic constraint in pre-solved form is unsatisfiable,
908: as it ensues from the following example:
909: $$a\in X\wedge X\in Y\wedge \{a\,|\,X\}\not\in Y.$$
910: Observe that there are no pairs of terms $t,t'$ of the form
911: singled out above. Nevertheless, since the satisfiability of $a
912: \in X$ is equivalent in \set\ to that of $X = \{a\,|\,N\}$ ($N$ is
913: a new variable), we have that the constraint is equi-satisfiable
914: to:
915: $$X = \{a\,|\,N\} \wedge \{a\,|\,N\} \in Y\wedge
916: \{a,a\,|\,N\}\not\in Y.$$
917: Now, $\{a\,|\,N\}$ and
918: $\{a,a\,|\,N\}$ are equivalent terms in $E_\set$, and thus the
919: constraint is unsatisfiable.
920:
921: \medskip
922:
923: To formally define the second condition for solved form
924: constraints, taking into account all the possible cases informally
925: described above, we introduce the following definitions.
926:
927: \begin{definition}%%[Stabilizing Substitutions - Closure]
928: Let $\theta\equiv[X_1/t_1,\dots,X_n/t_n]$ be a substitution and
929: $m\in\nat$. We recursively define the substitution
930: $\theta^m$ as:
931: $$\left\{\begin{array}{rcll}\theta^1 & = & \theta\\
932: \theta^{m+1} & = &[X_1/\theta^m(t_1),\dots, X_n/\theta^m(t_n)] & m>0
933: \end{array}\right.$$
934: If there exists $m>0$ such that $\theta^{m+1}\equiv \theta^{m}$
935: we say that $\theta$ is \emph{stabilizing}. Given a stabilizing
936: substitution $\theta$, the \emph{closure} $\theta^*$ of $\theta$
937: is the substitution $\theta^m$ such that $\forall k>m$ we have that
938: $\theta^{k}\equiv\theta^m$\/.
939: \end{definition}
940:
941: \begin{definition}%%[Member Substitution]
942: \label{subC}
943: Let $C$ be a constraint in pre-solved form over the language
944: ${\cal L}_{\lst}$ (${\cal L}_\bag, {\cal L}_\clist, {\cal
945: L}_\set$\/) and let
946: $t_1^1\in X_1,\dots,t_1^{k_1}\in X_1,\dots,
947: t_q^1\in X_q,\dots,t_q^{k_q}\in X_q$
948: be all membership atoms of $C$\/. We define the \emph{member
949: substitution} $\sigma_C$ as follows:
950: $$\sigma_C\equiv[X_1/[F_1,t_1^1,\dots, t_1^{k_1}\,|\,M_1],\dots,
951: X_q/[F_q,t_q^{1},\dots,t_q^{k_q}\,|\,M_q] ]$$ (respectively,
952: $\sigma_C \equiv [ X_1/\mo F_1, t_1^1,\dots,
953: t_1^{k_1}\,|\,M_1\mc,\dots
954: %X_q/\mo F_q,t_q^{1},\dots,
955: %t_q^{k_q}\,|\,M_q\mc
956: ],$
957: %or
958: %\phantom{(resp., }
959: $\sigma_C\equiv [ X_1/ \clo
960: F_1,t_1^1,\dots,t_1^{k_1}\,|\,M_1\clc,\dots
961: %X_q/\clo F_q,t_q^{1},\dots,t_q^{k_q}\,|\,M_q\clc
962: ],$\\
963: %or
964: %%\phantom{(resp., }
965: $\sigma_C\equiv [ X_1/\{ F_1, t_1^1,\dots,
966: t_1^{k_1}\,|\,M_1\},\dots
967: %X_q/\{F_q,t_q^{1},\dots,t_q^{k_q}\,|\,M_q\}
968: ])$
969: where $F_i$ and $M_i$ are new variables not occurring in $C$\/.
970: \end{definition}
971:
972: The member substitution $\sigma_C$ forces all the terms
973: $t_i^j$'s to be member of the aggregate represented by $X_i$.
974: The variable $F_i$ in $X_i$ is
975: necessary in the case of compact lists. As a matter of fact, in
976: every valuation $\sigma$ satisfying the constraint:
977: $$Y\in X_1\wedge \clo Y\,|\,X_1\clc\in X_2\wedge X_1\not\in X_2$$
978: it must be $\sigma(X_1)\neq\sigma(\clo Y\,|\,X_1\clc)$. Thus, in
979: $\sigma_C$ we give the possibility to the first element of
980: $\sigma(X_1)$ to be different from $\sigma(Y)$. We show in the
981: Appendix~\ref{modellistiche} that if $C$ is a constraint in
982: pre-solved form and acyclic, then $\sigma_C$ is stabilizing
983: (Lemma~\ref{convergente}).
984:
985: We are now ready to state the second condition for the solved
986: form.
987:
988: \begin{definition}[Membership Consistency Condition]
989: Let $E_\Th$ be one of the four equational theories for aggregates.
990: A constraint $C$ in pre-solved
991: form and acyclic is \emph{membership consistent} if for each pair
992: of literals of the form $t\not\in X, t'\in X$ in $C$ we have that:
993: $$E_\Th\not\models \forall (\sigma_C^*(t)=\sigma_C^*(t')).$$
994: \end{definition}
995:
996: The definition of solved form, therefore, can be given simply as
997: follows:
998:
999: \begin{definition}[Solved Form]\label{solvedform}
1000: A constraint $C$ in pre-solved form is said to be in \emph{solved
1001: form} if it satisfies the membership consistent condition.
1002: \end{definition}
1003:
1004: Observe that the membership consistency condition implies the
1005: acyclicity condition. It is a semantic requirement of equivalence
1006: of two terms under a given equational theory. However, this test
1007: can be automatized in the following way. As well-known from
1008: unification theory (see, e.g.,~\cite{BN98,Sie90}), given an
1009: equational theory $E$, knowing whether two terms are equivalent
1010: modulo $\equiv_E$ is the same as verifying whether the two terms
1011: $t$ and $t'$ are $E$-unifiable with empty m.g.u. ($\varepsilon$).
1012: Thus, the test is connected with the availability of a
1013: unification algorithm for the theory $ E_\Th$\/.
1014: In~\cite{DPR98-fuin} it is proved that the four equational
1015: theories we are dealing with are finitary (i.e., they admit a
1016: finite set of mgu's that covers all possible unifiers) and,
1017: moreover, the unification algorithms for the four theories are
1018: presented. This give us a decision procedure for the above test.
1019:
1020: As an example, let $C$ be the pre-solved form and acyclic
1021: \set-constraint:
1022: $a\in Y\wedge Y\in X\wedge X\in Z\wedge \{\{a\,|\,Y\}\,|\,X\}
1023: \not\in Z$.
1024: It holds that:
1025: $$\begin{array}{rcl}
1026: \sigma_C & = & [Y/\{F_Y,a\,|\,M_Y\}, X/\{F_X,Y\,|\,M_X\},
1027: Z/\{F_Z,X\,|\,M_Z\}]\,,\\
1028: \sigma_C^* & = &[Y/\{F_Y,a\,|\,M_Y\},
1029: X/\{F_X,\{F_Y,a\,|\,M_Y\}\,|\,M_X\},\\
1030: && \,\,
1031: Z/\{F_Z,\{F_X,\{F_Y,a\,|\,M_Y\}\,|\,M_X\}\,|\,M_Z\}] \\
1032: \sigma_C^*(X) &=& \{F_X,\{F_Y,a\,|\,M_Y\}\,|\, M_X\} \\
1033: \sigma_C^*(\{\{a\,|\,Y\}\,|\,X\}) &=&
1034: \{\{a,F_Y,a\,|\,M_Y\},F_X,\{F_Y,a\,|\,M_Y\}\,|\,M_X\}
1035: \end{array}$$
1036: The
1037: constraint is not in solved form since $E_\set\models
1038: \forall(\sigma_C^*(X)= \sigma_C^*(\{\{a\,|\,Y\}\,|\,X\}))$\/.
1039:
1040:
1041: \medskip
1042:
1043: We prove now that solved form constraints are satisfiable in the
1044: corresponding privileged models.
1045: We prove the property for \set-constraints.
1046: The proof is similar for the other cases.
1047:
1048: \begin{theorem}[Satisfiability of the Solved Form]\label{all solved}
1049: Let $C$ be a constraint in solved form over the language ${\cal
1050: L}_\set$ (resp., ${\cal L}_\lst$, ${\cal L}_\bag$, ${\cal
1051: L}_\clist$). Then ${\cal SET}\models \exists C$\/ (resp., $\cal
1052: LIST$, $\cal MSET$, and $\cal CLIST$).
1053: \end{theorem}
1054: \begin{proof}
1055: We split $C$ into the four parts: $C^=$, $C^{\in}$, $C^{\notin}$,
1056: and $C^{\neq}$, containing $=,\in, \notin$\/, and $ \neq$
1057: literals, respectively. For all pairs of literals $p \in V,r
1058: \notin V$ in $C$ let $NEQ_{pr}$ be an auxiliary variable, that
1059: will be used as a `constraint store', initialized to the empty
1060: set $\e$\/. We will use the two auxiliary functions {\it rank}
1061: and {\it find}. The {\it rank}\/ of a well-founded set is
1062: basically the maximum nesting of braces needed to write it.
1063: Precisely:
1064: $$ {\it rank}(s) = \left\{
1065: \begin{array}{ll}
1066: 0 & \mbox{if $s$ is not of the form $\{u\,|\,v\}$}\\
1067: \max\{1 + {\it rank}(u), {\it rank}(v)\} &
1068: \mbox{if $s$ is $\{u\,|\,v\}$\/}
1069: \end{array}
1070: \right.$$
1071: ${\it find}(X,t)$ is a function that produces for each
1072: pair $(X,t)$ a set of integer numbers indicating the `depth' of
1073: the occurrences of the variable $X$ in $t$\/. It can be defined
1074: as:
1075: $$ {\it find}(X,t) = \left\{
1076: \begin{array}{ll}
1077: \emptyset & \mbox{if $t$ is a constant term}\\
1078: \{0\} & \mbox{if $t$ is a variable $X$}\\
1079: {\{1 + n : n \in {\it find}(X,y)\}} &
1080: \mbox{if $t$ is $\{y\,|\,f(t_1,\dots,t_m)\}$,
1081: $f$ is not $\sef$} \\
1082: {\{1 + n : n \in {\it find}(X,t_1) \cup \cdots\cup
1083: {\it find}(X,t_m) \}} &
1084: \mbox{if $t$ is $f(t_1,\dots,t_m)$, $f$ is not $\sef$} \\
1085: {\{1 + n : n \in {\it find}(X,y)\}\:
1086: \cup{\it find}(X,s)} &
1087: \mbox{if $t$ is $\{y\,|\,s\}$\/, $s \neq \nil$}\\
1088: \end{array}
1089: \right.$$
1090: We build a successful valuation $\gamma$ of $C$, in
1091: various steps.
1092:
1093: \begin{description}
1094: \item[$C^{=}$] is of the form $ X_1 = t_1 \wedge \cdots
1095: \wedge X_m = t_m$.
1096: %where for all $i\in\{1,\dots ,m\}$\/,
1097: %$X_i$ occurs uniquely in $X_i=t_i$ and $X_i\not\in \vars(t_i)$\/.
1098: We define the mapping:
1099: $\theta_1 = [X_1 / t_1,\dots,X_m / t_m].$
1100:
1101: \item[$C^{\in}$] is of the form $p_{1}^{1}\in V_{1}\wedge\cdots\wedge
1102: p_{1}^{v1}\in V_{1}\wedge\cdots\wedge p^{vq}_{q}\in V_{q}$\/.
1103: Consider the member substitution
1104: $$\sigma_C = [V_{1} /
1105: \{F_{1},p_{1}^{1},\dots,p_{1}^{v1}\,|\, M_{1}\},\dots, V_{q} /
1106: \{F_q,p_{q}^{1},\dots,p_{q}^{vq}\,|\, M_{q}\}].$$ Since, by
1107: hypothesis, $C$ is acyclic, then $\sigma_C^*$ can be computed
1108: (see Lemma~\ref{convergente}).
1109:
1110: For each pair of literals $p \in V$, $r \notin V$ of $C$ consider the
1111: equality constraints in solved form $D_{1},\dots,D_{k}$ that are the
1112: solutions to the unification problem
1113: $\sigma_C^*(p)=\sigma_C^*(r)$
1114: (since $C$ is in solved form they are all different from the
1115: empty substitution).
1116: By the results concerning unification (cf.~\cite{DPR98-fuin})
1117: we have that
1118: $$ \sigma_C^*(p)=\sigma_C^*(r) \leftrightarrow
1119: \bigvee_{j=1}^{k}(\exists \bar N (D_{j})),$$
1120: where $\bar N$ are new variables, and each $D_{j}$ is a
1121: conjunction of equations which contains at least one atom of the
1122: form $A=\{a_{1},\dots,a_{h}\,|\,B\}$ with $A\in
1123: FV(\sigma_C^*(p))\cup FV(\sigma_C^*(r))$ and $FV(a_{i})\subseteq
1124: FV(\sigma_C^*(p))\cup FV(\sigma_C^*(r))$\/, or one atom of the
1125: form $A=B$ with $A,B\in FV(\sigma_C^*(p))\cup FV(\sigma_C^*(r))$\/.
1126:
1127: Since we want to satisfy $\sigma_C^*(r)\notin \sigma_C^*(V)$ we
1128: are interested in satisfying
1129: $\sigma_C^*(r)\neq \sigma_C^*(p)$, which is in turn equivalent to:
1130: $$\bigwedge_{j=1}^{k}(\forall N\neg D_{j}).$$
1131: For doing that, for each $D_{j}$ we choose an atom of the form
1132: $A=\{a_{1},\dots,a_{h}\,|\,B\}$ or $A=B$ and we store it in the
1133: variable $NEQ_{pr}$\/. Points (5) and (6) below will take care of
1134: this constraint store.
1135:
1136: \item[$C^{\notin}$] is of the form $r_1 \notin Y_1 \wedge \cdots
1137: \wedge r_n \notin Y_n$ (\/$Y_i$ does not occur in $r_i$\/)
1138: and
1139: $C^{\neq}$ is of the form $Z_1 \neq s_1 \wedge\cdots\wedge Z_o
1140: \neq s_o$ (\/$Z_i$ does not occur in $s_i$\/).
1141: Let $W_1,\dots,W_h$ be the variables occurring in $C$ other than
1142: $X_1,\dots,X_m,V_{1},\dots,
1143: V_{q},Y_1,\dots,Y_n,Z_1,\dots,Z_o$\/.
1144:
1145: Let $\bar{s} = \max\{ {\it rank}(t): \mbox{ $t$ occurs in
1146: $\sigma_C^*(\theta_1(C))$}\}+1+h$\/.
1147:
1148: Let $R_1,\dots,R_j$ be the variables occurring in
1149: $\sigma_C^*(\theta_1(C^{\notin}\wedge C^{\neq}))$ (actually, the
1150: variables $\bar F, \bar M$\/, and some of the $\bar Y$ and $\bar
1151: Z$\/) and $n_1,\dots,n_j$ be auxiliary variables ranging over
1152: $\nat$\/.
1153:
1154: We build an integer disequation system $S$ in the following way:
1155:
1156: \begin{enumerate}
1157:
1158: \item $S = \{n_i > \bar{s}: \forall i \in \{1,\dots,j\}\} \cup
1159: \{n_{i_1} \neq n_{i_2}: \forall i_1,i_2 \in\{1,\ldots,j\},
1160: i_1 \neq i_2 \}$.
1161:
1162: \item For each literal $R_{i_1} \neq t$
1163: in $\sigma_C^*(C^{\neq })$
1164: $$S = S \cup \{ n_{i_1} \neq n_{i_2} + c: \forall i_2 \neq
1165: i_1, \forall c \in {\it find}(R_{i_2},t)\}$$
1166:
1167: \item For each literal
1168: $\{R_{i_1},p_{j}^{1},\dots,p_{j}^{vj}\,|\,R_{h}\}\neq t$ in
1169: $\sigma_C^*(C^{\neq })$
1170: $$S = S \cup \{ n_{i_1} \neq n_{i_2} + c-1: \forall i_2 \neq
1171: i_1, \forall c \in {\it find}(R_{i_2},t)\}$$
1172:
1173:
1174: \item For each literal
1175: $t \notin R_{i_1}$ in $\sigma_C^*(C^{\notin})$ $$ S = S \cup
1176: \{n_{i_1} \neq n_{i_2} + c +1: \forall i_2 \neq i_1, \forall c
1177: \in {\it find}(R_{i_2},t)\}$$
1178:
1179: \item For each literal
1180: $t\notin \{R_h,p_{j}^{1},\dots,p_{j}^{vj}\,|\,R_{i_{1}}\}$\/,
1181: for each
1182: $k\leq vj$, for all $R_{i_{2}}=\{a_{1},\dots, a_{h}\,|\,B\}$
1183: in
1184: $NEQ_{p_{j}^{k}t}$
1185: $$S = S\cup \{n_{i_2} \neq n_{i_3} + c + 1: \forall
1186: i_3 \neq
1187: i_2, \forall c \in {\it find}(R_{i_3},a_{1})\}$$
1188:
1189: \item For each literal
1190: $t\notin \{R_h,p_{j}^{1},\dots,p_{j}^{vj}\,|\,R_{i_{1}}\}$\/,
1191: for each
1192: $k\leq vj$, for all $R_{i_{2}}=R_{i_{3}}$ in
1193: $NEQ_{p_{j}^{k}t}$
1194: $$S = S\cup \{n_{i_2} \neq n_{i_3}\}$$
1195:
1196: \item For each literal
1197: $t\notin \{R_{i_1},p_{j}^{1},\dots,p_{j}^{vj}\,|\,R_{h}\}$\/,
1198: $$S = S\cup \{n_{i_1} \neq n_{i_2}+c: \forall i_2\neq i_1,
1199: \forall c\in {\it find}(R_{i_2},t)\}$$
1200:
1201: \item For each literal
1202: $t\notin \{R_h,p_{j}^{1},\dots,p_{j}^{vj}\,|\,R_{i_{1}}\}$\/,
1203: $$S = S\cup \{n_{i_1} \neq n_{i_2} + c + 1: \forall
1204: i_2 \neq
1205: i_1, \forall c \in {\it find}(R_{i_2},t)\}$$
1206:
1207: \end{enumerate}
1208: \end{description}
1209:
1210: An integer disequation is \emph{safe} if, after expression
1211: evaluation, it is not of the form $u \neq u$\/. A safe disequation
1212: has always an infinite number of solutions. A finite set of safe
1213: disequations has always an infinite number of solutions. We show
1214: that all disequations of $S$ are safe. The disequations generated
1215: at point $(1)$ are safe by definition; those introduced in points
1216: $(2),(4),(5),(6),(7),$ and $(8)$ are safe since $c$ is always a
1217: positive number. We prove that the disequations generated at point
1218: $(3)$ are safe. If in $C$ there was a situation of the form
1219: $p_1\in Y\wedge\dots\wedge p_m\in Y\wedge Y\neq t$ from which we
1220: have obtained
1221: $\{F_Y,\sigma_C^*(p_1),\dots,\sigma_C^*(p_m)\,|\,M_Y\}\neq
1222: \sigma_C^*(t)$, then we had, from the definition of solved form,
1223: that $Y$ does not occur in $t$, hence $F_Y$ does not occur at
1224: depth $1$ in $\sigma_C^*(t)$, hence we do not obtain a disequation
1225: of the form $n_{F_Y}\neq n_{F_Y}+1-1$.
1226:
1227: {F}rom the safeness property, it is possible to find an integer
1228: solution to the system $S$ by choosing arbitrarily large values
1229: satisfying the constraints. Let $\{n_1 = \bar{n}_1,\dots, n_j =
1230: \bar{n}_j\}$ be a solution and define $$\theta_2 = [R_i / \{ \nil
1231: \}^ {\bar{n}_i}: \forall i \in \{1,\dots, j\}] \,.$$ where $ \{
1232: \nil \}^ {\bar{n}}$ denotes the term
1233: $\underbrace{\{\cdots\{}_{\bar{n}} \nil \}\cdots\}$ (similarly
1234: for the other theories employed).
1235:
1236: Let $\gamma = \theta_1 \sigma_C^*\theta_2$ (where $s \mu\nu$
1237: stands for $(s\mu)\nu$) and observe that $C\gamma$ is a
1238: conjunction of ground literals. We show that $KE^s_kF^s_1F_2F^3_s
1239: \models C\gamma$. We analyze each literal of $C$\/.
1240:
1241: \begin{description}
1242:
1243: \item [$X = t:$] $\theta_1(X)$ coincides syntactically with
1244: $\theta_1(t)=t$\/. Hence, a literal of this form is true
1245: in any model of equality.
1246:
1247: \item [$t \in X:$]
1248: $\theta_2(\sigma_C^*(X))=\{\dots,\theta_2(\sigma_{C}^*(t)),
1249: \dots\}$\/,
1250: so the atom is satisfied.
1251:
1252: \item [$Z\neq u:$] two cases are possible:
1253: \begin{enumerate}
1254: \item if there are no atoms of the form $t\in Z$ in $C$\/,
1255: then the conditions in $S$ and over $\bar{s}$ ensure
1256: that ${\it rank}(\gamma(Z))\neq {\it rank}(\gamma(u))$\/;
1257: \item if there is at least one atom of the form $t\in Z$ in $C$\/,
1258: then $\sigma_C^*(Z)=\{F, t_{1},\dots,t_{k}\,|\,M\}$\/,
1259: the conditions in $S$ and over $\bar{s}$ ensure
1260: that ${\it rank}(\gamma(F))\neq {\it rank}(\gamma(u))-1$,
1261: hence $\gamma(F)$ is
1262: not an element of $\gamma(u)$.
1263: \end{enumerate}
1264:
1265: \item [$r \notin Y:$] two cases are possible:
1266: \begin{enumerate}
1267: \item no atoms of the form $t\in Y$ occur in $C$\/:
1268: if $r$ is ground, then it can not be an element of $Y$
1269: since $\gamma(Y)=\{\nil\}^{i}$, with $i\geq \bar{s}$\/; if $r$
1270: is not ground, then the conditions in $S$ ensure that ${\it
1271: rank}(\gamma(Y))\neq {\it rank}(\gamma(r))+1$\/;
1272: \item at least one atom of the form $t\in Y$ occurs in $C$\/, hence
1273: $\sigma_{C}^*(Y)=\{F,t_{1},\dots,t_{k}\,|\,M\}$\/: if $r$
1274: is ground the result is trivial; if $r$ is not ground then the
1275: conditions in $S$ ensure that
1276: ${\it rank}(\gamma(t_j))\neq {\it rank}(\gamma(r))$ for
1277: all $j\leq k$,
1278: ${\it rank}(\gamma(F))\neq {\it rank}(\gamma(r))$,
1279: and
1280: ${\it rank}(\gamma(M))\neq {\it rank}(\gamma(r))+1$\/.
1281: \end{enumerate}
1282: \end{description}
1283: \end{proof}
1284:
1285: %\subsection{Refining the Solved Form}\label{refining}
1286: \begin{remark}\label{refining}
1287: The task of testing whether a pre-solved form constraint $C$ is in
1288: solved form could be avoided in the cases of multisets
1289: and sets, where all membership atoms can be removed. As a
1290: matter of fact, in the privileged models considered for sets and
1291: multisets it holds that:
1292: $$s \in t \leftrightarrow \exists N(t = \{s\,|\,N\}).$$
1293: We can therefore replace each membership atom $s \in t$ with an
1294: equi-satisfiable equality atom $t = \{s\,|\,N\}$ with $N$ a new
1295: variable. This implies that the additional conditions on the
1296: pre-solved form are not required at all, since membership atoms can
1297: be removed.
1298: %%The above rewriting cannot be done for lists and compact lists.
1299: %%This is basically due to the fact that if $t$ is a (compact) list
1300: %%in order to rewrite the constraint $s\in t$ using our constructors
1301: %%we need to know exactly how many elements there are in $t$ before
1302: %%the first occurrence of $s$.
1303: \end{remark}
1304:
1305:
1306: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1307: \section{Constraint Rewriting Procedures}
1308: \label{constraint-rewriting}
1309: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1310:
1311: In this section we describe the procedures that can be used to
1312: rewrite a given constraint $C$ into a equi-satisfiable disjunction
1313: of constraints in pre-solved form.
1314: All the procedures have the same overall structure
1315: shown in Figure~\ref{main loop}: they take a constraint $C$\/ as
1316: their input and repeatedly select an conjunct $c$ in $C$
1317: not in pre-solved form (if any) and apply one of the rewriting
1318: rules to it. The procedure stops when the constraint $C$ is
1319: in pre-solved or \false\ is a conjunct of the constraint.
1320: The procedure is non-deterministic. Some rewriting rules
1321: have two or more possible non-deterministic choices.
1322: Each non deterministic computation returns a constraint of the form
1323: above. However there is globally a finite set
1324: $C_1,\dots,C_k$ of constraints non-deterministically
1325: returned.
1326: The input constraint $C$ and
1327: the disjunction
1328: $C_1 \vee \cdots \vee C_k$ are equi-satisfiable.
1329:
1330: \begin{figure}[htb]
1331: {\small
1332: $$%%\renewcommand{\arraystretch}{\scala}
1333: \begin{array}{||c|rcl||}
1334: \multicolumn{4}{l}{\mbox{\sf \emph{Let $\Th$ be one of the
1335: theories \lst, \bag, \clist, \set, $\pi$ a symbol in
1336: \{$=$,$\neq$,$\in$,$\not\in$\}, and $C$ a $\Th$-constraint}}}\\
1337: \multicolumn{4}{l}{\vspace{-5pt}}\\
1338: \hline\hline \multicolumn{4}{||l||} {\phantom{aaa}\mbox{\sf while
1339: $C$ contains
1340: an atomic constraint $c$ of the form $\ell \pi r$ not in pre-solved
1341: form and $c \neq \false$ do}}\\
1342: \multicolumn{4}{||l||}
1343: {\phantom{aaaaaa}\mbox{\sf select $c$\/;}}\\
1344: \multicolumn{4}{||l||}
1345: {\phantom{aaaaaa}\mbox{\sf if $c$ = \false\ then return \false}}\\
1346: \multicolumn{4}{||l||}
1347: {\phantom{aaaaaa}\mbox{\sf else if $c$ = \true\ then erase $c$}}\\
1348: \multicolumn{4}{||l||}
1349: {\phantom{aaaaaa}\mbox{\sf else apply to $c$ any
1350: rewriting rule for $\Th$-constraints of the form $\cdot \pi \cdot$\/;} }\\
1351: \multicolumn{4}{||l||}
1352: {\phantom{aaa}\mbox{\sf return $C$}}\\
1353: \hline\hline
1354: \end{array} $$}
1355: \vspace{-5pt}\caption{\label{main loop}Main loop of constraint
1356: rewriting procedures}
1357: \end{figure}
1358:
1359:
1360: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1361: \subsection{Equality Constraints} \label{sec.unif}
1362: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1363:
1364: Unification algorithms for verifying the satisfiability and
1365: producing the solutions of equality constraints in the four
1366: aggregate's theories have been proposed
1367: in~\cite{DPR98-fuin}. The
1368: unification algorithms proposed in~\cite{DPR98-fuin}
1369: fall in the general schema of Figure~\ref{main loop}.
1370: Some determinism in the statement {\sf select $c$} is
1371: added to ensure termination.
1372: They are called:
1373: \begin{center}\begin{tabular}{lcl}
1374: {\sf Unify\_lists} for lists & \phantom{aaaa}&
1375: {\sf Unify\_msets} ({\sf Unify\_bags} in~\cite{DPR98-fuin})
1376: for multisets\\
1377: {\sf Unify\_clists} for compact lists &&
1378: {\sf Unify\_sets} for sets
1379: \end{tabular}\end{center}
1380: and they are used unaltered in the four global constraint
1381: solvers that we propose in this paper.
1382:
1383: The output of the algorithms is either $\false$\/, when the
1384: constraint is unsatisfiable, or a collection of solved form
1385: constraints (Def.~\ref{solvedform}) composed only by equality
1386: atoms. In Figure \ref{algobags.a} we have reported the rewriting
1387: rules for the multisets unification used in algorithm
1388: {\sf Unify\_msets}.
1389:
1390: \begin{figure}[htb]
1391: \small
1392: $$\begin{array}{||c|rcl||}
1393: \hline\hline
1394: \multicolumn{4}{||l||}{\mbox{\sf \emph{Rules for {\sf Unify\_msets}}}}\\
1395: \hline
1396: (1) &
1397: X = X \phantom{iii} &
1398: \mapsto & \true \\
1399: \hline
1400: (2) &
1401: \left.\begin{array}{r }
1402: t = X \\
1403: \mbox{\small $t$ is not a variable}
1404: \end{array}\right\} &
1405: \mapsto & X = t \\
1406: \hline
1407: (3) &
1408: \left.\begin{array}{r}
1409: X = t \\
1410: \mbox{\small $X$ does not occur in $t$, $X$ occurs in $C$}
1411: \end{array}\right\} &
1412: \mapsto & \\
1413: & \multicolumn{3}{r||}{X = t \mbox{ {\small and apply the
1414: substitution $X/t$ to $C$}}}\\
1415: \hline
1416: (4) &
1417: \left.\begin{array}{r}
1418: X = t \\
1419: \mbox{\small $X$ is not $t$ and $X$ occurs in $t$}
1420: \end{array}\right\} &
1421: \mapsto & \false \\
1422: \hline
1423: (5) &
1424: \left.\begin{array}{r}
1425: f(s_1,\dots,s_m) =
1426: g(t_1,\dots,t_n) \\
1427: f \mbox{ is not } g
1428: \end{array}\right\} &
1429: \mapsto & \false \\
1430: \hline
1431: (6) &
1432: \left.\begin{array}{r}
1433: f(s_1,\dots,s_m) =
1434: f(t_1,\dots,t_m) \\
1435: m \geq 0, f \mbox{ is not } \mf
1436: \end{array}\right\} &
1437: \mapsto & \\
1438: & \multicolumn{3}{r||}{s_1 = t_1 \wedge \dots
1439: \wedge s_m = t_m} \\
1440: \hline
1441: (7) &\left.
1442: \begin{array}{r}
1443: \mo t\,|\,s\mc = \mo t'\,|\,s'\mc \\
1444: \mbox{\small ${\sf tail}(s)$ and ${\sf tail}(s')$
1445: are not the same variable}
1446: \end{array}
1447: \right\} & \mapsto &\\
1448: & \multicolumn{3}{r||}{
1449: \begin{array}{cl}
1450: (i) & (t = t' \wedge s = s') \vee\\
1451: (ii) & (s = \mo t'\,|\,N\mc \wedge
1452: \mo t\,|\,N \mc = s')
1453: \end{array}} \\
1454: \hline
1455: (8) &\left.
1456: \begin{array}{r}
1457: \mo t\,|\,s\mc = \mo t'\,|\,s'\mc \\
1458: \mbox{\small ${\sf tail}(s)$ and ${\sf tail}(s')$
1459: are the same variable}
1460: \end{array}
1461: \right\} & \mapsto & \\
1462: & \multicolumn{3}{r||}{
1463: {\sf untail}(\mo t\,|\,s\mc) =
1464: {\sf untail}(\mo t'\,|\,s'\mc )}\\
1465: \hline\hline
1466: \end{array}$$
1467: \caption{\label{algobags.a}Rewriting rules for the Unification
1468: algorithm for multisets}
1469: \end{figure}
1470:
1471: \label{untail}
1472: The algorithm uses the auxiliary
1473: functions ${\sf tail}$ and ${\sf untail}$ defined
1474: as follows:
1475: $$\begin{array}{lcll}
1476: {\sf tail}(f(t_1,\dots,t_n)) & = & f(t_1,\dots,t_n) &
1477: \mbox{$f$ is not $\mf$, $n\geq 0$}\\
1478: {\sf tail}(X) & = & X & \mbox{$X$ is a variable}\\
1479: {\sf tail}(\mo t\,|\, s \mc) & = &
1480: {\sf tail}( s )\\
1481: {\sf untail}(X) & = & \nil& \mbox{$X$ is a variable}\\
1482: {\sf untail}(\mo t\,|\, s \mc) & = &
1483: \mo t\,|\, {\sf untail}( s ) \mc
1484: \end{array}$$
1485:
1486:
1487: \subsection{Membership and not-Membership Constraints}
1488:
1489: The rewriting rules for membership and not-membership constraints
1490: are justified by axioms $(K)$ and $(W)$ that hold in all the four
1491: theories. Therefore, in Figure~\ref{innonin} we give a single
1492: definition of these rules. They are used within the main loop in
1493: Figure~\ref{main loop} to define the rewriting procedures for
1494: membership and not-membership constraints over the considered
1495: aggregate. When useful, we will refer to these procedures with the
1496: generic names {\sf in-$\Th$} and {\sf nin-$\Th$}, where $\Th$ is
1497: any of the aggregate theories.
1498:
1499: %%%%%%%%%%%%%%%%%% general in and nin %%%%%%%%%%%%%%%%%%%
1500: \begin{figure}[htb]
1501: {\small
1502: %%\renewcommand{\arraystretch}{\scala}
1503: $$\begin{array}{||c|rcll||}
1504: \multicolumn{5}{l}{\mbox{\sf \emph{Let $\cons$ be the aggregate
1505: constructor for the theory $\Th$}}}\\
1506: \hline\hline
1507: \multicolumn{5}{||l||}{\mbox{\sf \emph{Rules for {\bf in-$\Th$}}}}\\
1508: \hline
1509: (1) & \left.\begin{array}{r}
1510: r \in f(t_1,\dots,t_n)\\
1511: f \mbox{ is not } \cons
1512: \end{array}\right\} & \mapsto & {\false} & \\
1513: \hline
1514: (2) & \left.\begin{array}{r} r \in {\tt cons_\Th}(t,s)
1515: \end{array}\right\} & \mapsto & r = t \:\vee & (a) \\
1516: &&& r \in s & (b)\\
1517: \hline
1518: (3) & \left.\begin{array}{r}
1519: r \in X \\
1520: X \in \vars(r)
1521: \end{array}\right\} & \mapsto & {\false} & \\
1522: \hline\hline
1523: \end{array}$$
1524:
1525: $$\begin{array}{||c|rcl||}
1526: \hline\hline
1527: \multicolumn{4}{||l||}{\mbox{\sf \emph{Rules for {\bf nin-$\Th$}}}}\\
1528: \hline
1529: (1) & \left.\begin{array}{r}
1530: r \notin f(t_1,\dots,t_n)\\
1531: f \mbox{ is not } \cons
1532: \end{array}\right\} & \mapsto & {\true} \\
1533: \hline
1534: (2) & \left.\begin{array}{r}
1535: r \notin {\tt cons_\Th}(t,s)
1536: \end{array}\right\} & \mapsto &
1537: r \neq t \wedge r \notin s \\
1538: \hline
1539: (3) & \left.\begin{array}{r}
1540: r \notin X \\
1541: X \in \vars(r)
1542: \end{array}\right\} & \mapsto & {\true} \\
1543: \hline \hline
1544: \end{array}$$}
1545:
1546: \vspace{-5pt}\caption{\label{innonin}Parametric rewriting rules
1547: for membership and not-membership constraints}\vspace{+10pt}
1548: \end{figure}
1549:
1550: \begin{lemma}\label{tuttimember}
1551: Let $\Th$ be one of the theories \lst, \bag, \clist, \set, and
1552: ${\cal A}_{\Th}$ the privileged model for the theory $\Th$\/.
1553: Let $C$ be a $\Th$-constraint, $C_1,\dots,C_k$ be the constraints
1554: non-deterministically returned by {\sf
1555: nin-{$\Th$}(in-{$\Th$}$(C)$))}\/, and $\bar N_i = \vars(C_i)
1556: \setminus \vars(C)$\/. Then ${\cal A}_{\Th} \models \forall
1557: \left(C \leftrightarrow \bigvee_{i=1}^{k} \exists \bar N_i C_i
1558: \right)$\/.
1559: \end{lemma}
1560: \begin{proof}
1561: We prove correctness and completeness for lists, thus with respect
1562: to the model $\cal LIST$\/. Soundness and completeness for the
1563: other aggregates are proved in the very same way. Soundness and
1564: completeness is proved for each rewriting rule separately since
1565: the rules are mutually exclusive. When possible, we simply point
1566: out the axioms of the corresponding theory \lst\ involved in the
1567: proof (note that $\cal LIST$ is a model of those axioms):
1568: \begin{description}
1569: \item[\mbox{{\sf in-List}, {\rm rule} $(1)$}\/.] $r \in
1570: f(t_1,\dots,t_n)$\/, with $f$ different from $[ \cdot \,|\, \cdot ]$ is
1571: equivalent to {\true}\ by axiom $(K)$\/.
1572: \item[\mbox{{\sf in-List}, {\rm rule} $(2)$}\/.] This is
1573: exactly axiom $(W)$\/.
1574: \item[\mbox{{\sf in-List}, {\rm rule} $(3)$}\/.]
1575: Assume that there is a valuation
1576: $\sigma$ such that ${\cal LIST} \models \sigma(r \in X)$\/.
1577: This means that $\sigma(X)$ contains a term of the form:
1578: $[ s_1 , \dots, s_n , r'
1579: \,|\, t]$ for some terms $s_1,\dots,s_n,t$\/,
1580: and some term $r'$ in $\sigma(r)$. Axiom $(F_3)$
1581: ensures that $X$ can not be a subterm of $r$\/.
1582: \item[\mbox{{\sf nin-List}, {\rm rules} $(1)$\/, $(2)$\/, $(3)$}\/.]
1583: Same proofs as for the corresponding {\sf in-List} rules, using
1584: the same axioms.
1585: \end{description}
1586: \end{proof}
1587:
1588: In the above lemma it holds that the lists of variables
1589: $\bar N_i$ are all empty.
1590: However, for the sake of uniformity with respect to the
1591: other similar correctness results, we have made them explicit.
1592: Let us observe that the rewriting rules for procedure {\sf
1593: in-MSet} and {\sf in-Set} could safely be extended by the rule:
1594: {\small
1595: $$\renewcommand{\arraystretch}{\scala}
1596: \begin{array}{||c|rcl||}
1597: \hline\hline (4) & \phantom{aaa} \left.\begin{array}{r}
1598: r \in X \\
1599: X \not\in \vars(r)
1600: \end{array}\right\} & \mapsto &
1601: X = \mo r \,|\, N \mc \phantom{aaa}(X = \{ r \,|\, N \}) \\
1602: \hline\hline
1603: \end{array}$$
1604: }
1605:
1606: \noindent where $N$ is a new variable (see also
1607: Remark~\ref{refining}). In this way, we are sure to completely
1608: remove membership atoms from the constraints and that the
1609: pre-solved form constraints obtained are in solved form.
1610:
1611:
1612: \subsection{Disequality constraints}
1613:
1614: Rewriting rules for disequality constraints consist of a part
1615: which is the same for the four theories (although parametric with
1616: respect to the considered theory), and a part which is specific
1617: for each one of the four theories. Rules of the common part are
1618: shown in Figure~\ref{algo-neq-general}, while specific rules are
1619: described in the next subsections.
1620:
1621: %%%%%%%%%%%%%%%%%%%% general neq %%%%%%%%%%%%%%%%%%%%%
1622: \begin{figure}[htb]
1623: {\small
1624: %%\renewcommand{\arraystretch}{\scala}
1625: $$\begin{array}{||c|rcl||}
1626: \multicolumn{4}{l}{\mbox{\sf \emph{Let $\cons$ be the aggregate
1627: constructor for the theory $\Th$}}}\\
1628: \multicolumn{4}{l}{\vspace{-5pt}}\\
1629: \hline \hline
1630: \multicolumn{4}{||l||}{\mbox{\sf \emph{Rules for {\bf neq-$\Th$}}}}\\
1631: \hline
1632: (1) & \left.\begin{array}{r}
1633: d \neq d \\
1634: d \mbox{ is a constant}
1635: \end{array}\right\}
1636: & \mapsto & {\false} \\
1637: \hline
1638: (2) & \left.\begin{array}{r}
1639: f(s_1,\dots,s_m) \neq g(t_1,\dots,t_n) \\
1640: f \mbox{ is not } g
1641: \end{array}\right\} &
1642: \mapsto & {\true} \\
1643: \hline
1644: (3) & \left.\begin{array}{r}
1645: t \neq X \\
1646: \mbox{$t$ is not a variable}
1647: \end{array}\right\} & \mapsto & X \neq t \\
1648: \hline
1649: (4) & \left.\begin{array}{r}
1650: X \neq X \\
1651: X \mbox{ is a variable}
1652: \end{array}\right\}
1653: & \mapsto & {\false} \\
1654: \hline
1655: (5) & \left.\begin{array}{r}
1656: f(s_{1},\dots,s_n)
1657: \neq
1658: f(t_{1},\dots,t_n) \\
1659: n > 0, f \mbox{ is not } \cons
1660: \end{array}\right\} & \mapsto &
1661: \begin{array}[t]{lc}
1662: s_{1} \neq t_{1} \vee & (1)\\
1663: \vdots & \vdots\\
1664: s_{n} \neq t_{n} & (n)
1665: \end{array} \\
1666: \hline\hline
1667: \end{array} $$}
1668: \vspace{-5pt}\caption{\label{algo-neq-general}General rewriting
1669: rules for disequality constraints} \vspace{+10pt}
1670: \end{figure}
1671:
1672:
1673: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1674: \subsubsection{Lists}
1675:
1676: Specific rules for the theory \lst\ are presented in Figure
1677: \ref{algo-neq-list}. These rules are inserted in the general
1678: schema of Figure~\ref{main loop} to generate the procedure
1679: \mbox{\sf neq-List}.
1680:
1681: %%%%%%%%%%%%%%%%%%%% neq for lists %%%%%%%%%%%%%%%%%%%%%
1682: \begin{figure}[htb]
1683: {\small
1684: %%\renewcommand{\arraystretch}{\scala}
1685: $$\begin{array}{||c|rcl||}
1686: \hline\hline
1687: \multicolumn{4}{||l||}{\mbox{\sf \emph{Rules for {\bf neq-List}}}}\\
1688: %\multicolumn{4}{||l||} {\phantom{aaa}\mbox{\sf while there is a
1689: %$\neq$-constraint
1690: %$c$ in $C$ not in pre-solved form and $C \neq \false$ do}}\\
1691: %\multicolumn{4}{||l||}
1692: %{\phantom{aaaaaa}\mbox{\sf case $c$ of}}\\
1693: \hline
1694: %\multicolumn{4}{||l||}
1695: $(1)$-$(5)$ & {\mbox{\sf see Figure~\ref{algo-neq-general}}} & &\\
1696: \hline
1697: (6) & \left.\begin{array}{r}
1698: [ s_{1}\,|\, s_2 ]
1699: \neq
1700: [ t_{1}\,|\,t_2 ]
1701: \end{array}\right\} & \mapsto &
1702: \begin{array}[t]{lc}
1703: s_{1} \neq t_{1} \vee & (i)\\
1704: s_{2} \neq t_{2} & (ii)
1705: \end{array} \\
1706: \hline
1707: (7) & \left.\begin{array}{r}
1708: X \neq f(t_{1},\dots,t_n) \\
1709: X \in \vars(t_{1},\dots,t_n)
1710: \end{array}\right\}
1711: & \mapsto & {\true} \\
1712: \hline\hline
1713: \end{array} $$}
1714: \vspace{-5pt}\caption{\label{algo-neq-list}Rewriting rules for
1715: disequality constraints over lists} \vspace{+10pt}
1716: \end{figure}
1717:
1718: \begin{lemma}\label{corrlist}
1719: Let $C$ be a \lst-constraint, $C_1,\dots,C_k$ be the constraints
1720: non-deterministically returned by {\sf neq-List}$(C)$\/, and $\bar
1721: N_i = \vars(C_i) \setminus \vars(C)$\/. Then $\mbox{\lst} \models
1722: \forall \left(C \leftrightarrow \bigvee_{i=1}^{k} \exists \bar
1723: N_i C_i \right)$\/.
1724: \end{lemma}
1725: \begin{proof}
1726: Soundness and completeness of the rewriting rules (and, hence, of
1727: the whole rewriting procedure {\sf neq-List}) are immediate
1728: consequence of standard equality axioms and axiom schemata
1729: $(F_1),(F_2),$ and $(F_3)$\/.
1730: \end{proof}
1731:
1732:
1733: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1734: \subsubsection{Multisets}
1735:
1736: Disequality constraints over multisets are simplified using the
1737: rewriting rules presented in Figure~\ref{neq-bag-fig}. They make
1738: use of functions ${\sf tail}$ and ${\sf untail}$ defined in
1739: Section~\ref{untail}. Using these rules within the generic
1740: rewriting scheme of Figure~\ref{main loop} we get the rewriting
1741: procedure for disequality constraints over multisets, called {\sf
1742: neq-MSet}.
1743: \begin{figure}[htb]
1744: {\small
1745: %%\renewcommand{\arraystretch}{\scala}
1746: $$\begin{array}{||c|rcl||}
1747: \hline\hline
1748: \multicolumn{4}{||l||}{\mbox{\sf \emph{Rules for {\bf neq-MSet}}}}\\
1749: \hline
1750: $(1)$-$(5)$ & {\mbox{\sf see Figure~\ref{algo-neq-general}}} & &\\
1751: \hline
1752: (6.1) & \left.\begin{array} {r}
1753: \mo t_1 \,|\, s_1\mc \neq \mo t_2 \,|\, s_2 \mc\\
1754: \mbox{${\sf tail}(s_1)$ and ${\sf tail}(s_2)$}\\
1755: \mbox{are the same variable}
1756: \end{array}\right\} & \mapsto &
1757: {\sf untail}(\mo t_1 \,|\, s_1 \mc) \neq
1758: {\sf untail}(\mo t_2 \,|\, s_2 \mc)\\
1759: \hline
1760: (6.2) & \left. \begin{array} {r}
1761: \mo t_1 \,|\, s_1 \mc \neq \mo t_2 \,|\, s_2 \mc\\
1762: \mbox{${\sf tail}(s_1)$ and ${\sf tail}(s_2)$}\\
1763: \mbox{are not the same variable}
1764: \end{array} \right\} & \mapsto &
1765: \begin{array}[t]{lc}
1766: (t_1 \neq t_2 \wedge t_1 \notin s_2) \vee & (a)\\
1767: (\mo t_2 \,|\, s_2 \mc = \mo t_1 \,|\, N \mc
1768: \wedge s_1 \neq N ) & (b)
1769: \end{array}\\
1770: \hline
1771: (7) & \left.\begin{array}{r}
1772: X \neq f(t_{1},\dots,t_n) \\
1773: X \in \vars(t_{1},\dots,t_n)
1774: \end{array}\right\}
1775: & \mapsto & {\true} \\
1776: \hline\hline
1777: \end{array}$$}
1778: \vspace{-5pt}\caption{\label{neq-bag-fig} Rewriting rules for
1779: disequality constraints over multisets}\vspace{+10pt}
1780: \end{figure}
1781:
1782: Some words are needed for explaining the rules related to the
1783: management of disequalities between multisets; in particular rule
1784: $(6.2)$ of Figure~\ref{neq-bag-fig}. If we use directly axiom
1785: $(E^m_k)$\/, we have that:
1786: $$\begin{array}{rcl}
1787: \mo t_1 \,|\, s_1 \mc \neq \mo t_2 \,|\, s_2 \mc &
1788: \leftrightarrow & (t_1 \neq t_2 \vee s_1 \neq s_2) \wedge\\
1789: && \forall N\,(s_2 \neq \mo t_2 \,|\, N \mc \vee
1790: s_1 \neq \mo t_1 \,|\, N \mc)
1791: \end{array}$$
1792: This way, an universal quantification is introduced: this is
1793: no longer a constraint according to Definition~\ref{constraintdef}.
1794:
1795: Alternatively, we could use the intuitive notion of
1796: multi-membership: $x \in^i y$ if $x$ belongs at least $i$ times to the
1797: multiset $y$\/. This way, one can provide an alternative version
1798: of equality and disequality between multisets. In particular, we
1799: have:
1800: $$\begin{array}{rcl}
1801: \mo t_1 \,|\, s_1 \mc \neq \mo t_2 \,|\, s_2 \mc &
1802: \leftrightarrow & \exists X \exists n \,( n \in \nat
1803: \,\wedge \\
1804: && \phantom{aaaaaa}
1805: (X \in^n \mo t_1 \,|\, s_1 \mc \wedge
1806: X \notin^n \mo t_2 \,|\, s_2 \mc) \vee\\
1807: && \phantom{aaaaaa}
1808: (X \in^n \mo t_2 \,|\, s_2 \mc \wedge
1809: X \notin^n \mo t_1 \,|\, s_1 \mc\mo t_2 \,|\, s_2 \mc))
1810: \end{array}$$
1811: In this case, however, we have a quantification on natural
1812: numbers: we are outside the language we are studying.
1813: The rewriting rule $(6.2)$ adopted in Figure~\ref{neq-bag-fig}
1814: avoids these difficulties introducing only existential
1815: quantification. Its correctness and completeness are proved in
1816: the following lemma.
1817:
1818:
1819: \begin{lemma}\label{corrbag}
1820: Let $C$ be a \bag-constraint, $C_1,\dots,C_k$ be the constraints
1821: non-deterministically returned by {\sf neq-MSet}$(C)$\/, and $\bar
1822: N_i = \vars(C_i) \setminus \vars(C)$\/. Then ${\cal MSET} \models
1823: \forall \left(C \leftrightarrow \bigvee_{i=1}^{k} \exists \bar
1824: N_i C_i \right)$\/.
1825: \end{lemma}
1826: \begin{proof}
1827: {F}rom Lemma~\ref{corrlist} we know that the result holds for
1828: rules $(1)$--$(5)$ and $(7)$ for the model $\cal LIST$\/. Since
1829: permutativity has not been used for that result, and axiom $(F_3)$
1830: holds for both the theories, the same holds for the model $\cal
1831: MSET$\/. We need to prove correctness and completeness of
1832: rewriting rules $(6.1)$ and $(6.2)$\/.
1833: \begin{description}
1834: \item[$(6.1)$] It is immediately justified by axiom schema $(F_3^m)$.
1835:
1836: \item[$(6.2)$] The constraint
1837: $\mo t_1\,|\,s_1 \mc \neq \mo t_2\,|\,s_2 \mc$
1838: is equivalent to:
1839: \begin{eqnarray}
1840: && t_1 \notin \mo t_2\,|\,s_2 \mc \wedge \mo t_1\,|\,s_1
1841: \mc
1842: \neq \mo t_2\,|\,s_2 \mc
1843: \, \vee\label{formulaa} \\
1844: && t_1 \in \mo t_2\,|\,s_2 \mc \wedge \mo t_1\,|\,s_1 \mc
1845: \neq \mo t_2\,|\,s_2 \mc
1846: \label{formulab}
1847: \end{eqnarray}
1848: Since we are looking for successful valuations over $\cal MSET$
1849: that deal with multisets of finite elements, axiom $(E^m_k)$
1850: ensures that $t_1 \notin \mo t_2\,|\,s_2 \mc $ implies
1851: $\mo t_1\,|\,s_1 \mc \neq \mo t_2\,|\,s_2 \mc$\/.
1852: Thus, formula (\ref{formulaa}) is equivalent to
1853: $t_1 \in \mo t_2\,|\,s_2 \mc $ which, in turn, is equivalent
1854: by $(W)$ to the disjunct $(a)$ of the rewriting rule.
1855:
1856: Consider now formula (\ref{formulab}).
1857: It is easy to see that
1858: \begin{eqnarray}\label{formulac}
1859: {\cal MSET} \models \forall (t_1 \in \mo t_2\,|\,s_2 \mc
1860: \leftrightarrow \exists M \, (
1861: \mo t_1 \,|\, M \mc =
1862: \mo t_2\,|\,s_2 \mc))
1863: \end{eqnarray}
1864: Thus, (\ref{formulab}) is equivalent
1865: to
1866: \begin{eqnarray}\label{formulad}
1867: \exists M \, (
1868: \mo t_1 \,|\, M \mc =
1869: \mo t_2\,|\,s_2 \mc
1870: \wedge \mo t_1\,|\,s_1 \mc \neq \mo
1871: t_2\,|\,s_2 \mc )
1872: \end{eqnarray}
1873: It remains to prove that (\ref{formulad}) is equivalent to
1874: the disjunct $(b)$\/, namely:
1875: \begin{eqnarray}\label{formulas}
1876: \exists N\, ( s_1 \neq N \wedge
1877: \mo t_2 \,|\, s_2 \mc = \mo t_1 \,|\, N \mc )
1878: \end{eqnarray}
1879:
1880: \begin{description}
1881: \item[\rm $(\ref{formulad}) \rightarrow (\ref{formulas})$]
1882: Assume there is $M$ so as to satisfy $(\ref{formulad})$\/.
1883: $M = s_1$ will immediately lead to a contradiction.
1884: Thus, $ (\ref{formulas})$ is satisfied by $N = M$\/.
1885:
1886: \item[\rm $(\ref{formulas}) \rightarrow (\ref{formulad})$]
1887: Assume there is $N$ so as to satisfy $(\ref{formulas})$\/.
1888: It follows immediately from the fact, true for finite multisets,
1889: that $s_1 \neq N$ implies $\mo t_1 \,|\, s_1 \mc \neq \mo t_1
1890: \,|\, N \mc$\/. Thus, choose $M = N$\/.
1891:
1892: \end{description}\end{description}
1893: \end{proof}
1894:
1895:
1896: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1897: \subsubsection{Compact Lists}
1898:
1899: The rewriting rules for disequality constraints over compact lists
1900: are shown in Figure~\ref{neq-clist-fig}.
1901: These rules can be immediately exploited in conjunction with the
1902: generic scheme of Figure~\ref{main loop} to obtain a rewriting
1903: procedure for disequality constraints over multisets--called {\sf
1904: neq-CList}. Soundness and completeness of {\sf neq-CList} are
1905: stated by the following lemma.
1906:
1907: \begin{figure}[htb]
1908: {\small
1909: %%\renewcommand{\arraystretch}{\scala}
1910: $$\begin{array}{||c|rcl||}
1911: \hline\hline
1912: \multicolumn{4}{||l||}{\mbox{\sf \emph{Rules for {\bf neq-CList}}}}\\
1913: \hline
1914: $(1)$-$(5)$ & {\mbox{\sf see Figure~\ref{algo-neq-general}}} & &\\
1915: \hline
1916: (6) & \left.\begin{array}[t]{r}
1917: \clo t_1 \,|\, s_1 \clc \neq \clo t_2 \,|\, s_2 \clc
1918: \end{array}\right\}
1919: & \mapsto & \\
1920: & \multicolumn{3}{|r||}{
1921: \begin{array}[t]{lc}
1922: t_1 \neq t_2 \vee & (a)\\
1923: s_1 \neq s_2 \wedge
1924: \clo t_1\,|\,s_1 \clc \neq s_2 \wedge
1925: s_1 \neq \clo t_2 \,|\, s_2 \clc & (b)
1926: \end{array}} \\
1927: \hline
1928: (7.1) & \left.
1929: \begin{array}{r}
1930: X \neq f(t_1,\dots,t_n) \\
1931: X \in \vars(t_1,\dots,t_n), f \mbox{ is not } \lcf\\
1932: \end{array}\right\}
1933: & \mapsto & {\true} \\
1934: \hline
1935: (7.2) & \left.\begin{array}{r}
1936: X \neq \clo t_1,\dots,t_n \,|\,X\clc \\
1937: X \in \vars(t_1,\dots,t_n)
1938: \end{array}\right\}
1939: & \mapsto & {\true} \\
1940: \hline
1941: (7.3) & \left.\begin{array}{r}
1942: X \neq \clo t_1,\dots,t_n \,|\,X\clc \\
1943: X \notin \vars(t_1,\dots,t_n)
1944: \end{array}\right\}
1945: & \mapsto &
1946: \begin{array}[t]{lc}
1947: t_1 \neq t_2 \vee & (a.1)\\
1948: \vdots & \vdots \\
1949: t_1 \neq t_n \vee & (a.n)\\
1950: X = \nil\; \vee & (b) \\
1951: X = \clo N_1 \,|\, N_2 \clc \wedge N_1 \neq t_1 & (c)
1952: \end{array}\\
1953: \hline\hline
1954: \end{array}$$}
1955: \vspace{-5pt}\caption{\label{neq-clist-fig} Rewriting rules for
1956: disequality constraints over compact lists}\vspace{+10pt}
1957: \end{figure}
1958:
1959:
1960: \begin{lemma}\label{corrclists}
1961: Let $C$ be a \clist-constraint, $C_1,\dots,C_k$ be the constraints
1962: non-deterministically returned by {\sf neq-CList}$(C)$\/, and
1963: $\bar N_i = \vars(C_i) \setminus \vars(C)$\/. Then ${\cal CLIST}
1964: \models \forall \left(C \leftrightarrow \bigvee_{i=1}^{k}
1965: \exists \bar N_i C_i \right)$\/.
1966: \end{lemma}
1967: \begin{proof}
1968: For rules $(1)$--$(5)$ the result follows immediately from those for lists.
1969: Rules $(7.1)$--$(7.3)$ follows from axiom $(F^c_3)$.
1970: Rule $(6)$ is exactly axiom $(E^c_k)$\/.
1971: \end{proof}
1972:
1973: Observe that, differently from multisets, the rewriting rule for
1974: disequality between compact lists follows immediately from axiom
1975: $(E^c_k)$\/. As a matter of fact, this axiom does not introduce
1976: any new variable.
1977:
1978: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1979: \subsubsection{Sets}
1980:
1981: Disequality constraints over sets are dealt with by the rewriting
1982: rules shown in Figure~\ref{neqsetfig}, and they constitute the
1983: procedure {\sf neq-Set}.
1984:
1985: \begin{figure}[htb]
1986: {\small
1987: %%\renewcommand{\arraystretch}{\scala}
1988: $$\begin{array}{||c|rcl||}
1989: \hline\hline
1990: \multicolumn{4}{||l||}{\mbox{\sf \emph{Rules for {\bf neq-Set}}}}\\
1991: \hline
1992: $(1)$-$(5)$ & {\mbox{\sf see Figure~\ref{algo-neq-general}}} & &\\
1993: \hline (6) & \left.\begin{array}[t]{r}
1994: \{ t_1 \,|\, s_1 \} \neq \{ t_2 \,|\, s_2 \}
1995: \end{array} \right\}
1996: & \mapsto & \\
1997: & \multicolumn{3}{|r||}{
1998: \begin{array}[t]{lc}
1999: Z \in \{ t_1 \,|\, s_1 \} \wedge
2000: Z \notin \{ t_2 \,|\, s_2 \} \vee & (a)\\
2001: Z \in \{ t_2 \,|\, s_2 \} \wedge
2002: Z \notin \{ t_1 \,|\, s_1 \} & (b)
2003: \end{array}} \\
2004: \hline
2005: (7.1) & \left.
2006: \begin{array}{r}
2007: X \neq f(t_1,\dots,t_n) \\
2008: X \in \vars(t_1,\dots,t_n), f \mbox{ is not } \sef\\
2009: \end{array}\right\}
2010: & \mapsto & {\true} \\
2011: \hline
2012: (7.2) & \left.
2013: \begin{array}{r}
2014: X \neq \{ t_1,\dots,t_n \,|\,X\} \\
2015: X \in \vars(t_1,\dots,t_n)
2016: \end{array}\right\}
2017: & \mapsto & {\true} \\
2018: \hline
2019: (7.3) & \left.\begin{array}{r}
2020: X \neq \{ t_1,\dots,t_n \,|\,X\} \\
2021: X \notin \vars(t_1,\dots,t_n)
2022: \end{array}\right\}
2023: & \mapsto &
2024: \begin{array}[t]{lc}
2025: t_1 \notin X \vee & (i)\\
2026: \vdots & \vdots \\
2027: t_n \notin X & (n)
2028: \end{array}\\
2029: \hline\hline
2030: \end{array}$$}
2031: \vspace{-5pt}\caption{\label{neqsetfig}Rewriting rules for
2032: disequality constraints over sets}\vspace{+10pt}
2033: \end{figure}
2034:
2035: Some remarks are needed regarding rule $(6)$\/. As for multisets,
2036: axiom $(E^s_k)$ introduces an existentially quantified variable to
2037: state equality. Thus, its direct application for stating
2038: disequality requires universally quantified constraints that go
2039: outside the language. On the other hand, the rewriting rule
2040: $(6.2)$ used for multisets can not be used in this context. In
2041: fact, the property that $s_1 \neq N$ implies $\mo t_1 \,|\, s_1
2042: \mc \neq \mo t_1 \,|\, N \mc$\/, that holds for finite multisets,
2043: does not hold for sets. For instance, $\{ a\} \neq \{a,b\}$ but
2044: $\{ b , a \} = \{ b,a,b\}$\/. Thus, this rewriting rule would be
2045: not correct for sets.
2046:
2047: A rewriting rule for disequality constraints over sets can be
2048: obtained by taking the negation of the standard extensionality
2049: axiom
2050: $$
2051: \renewcommand{\arraystretch}{\scala}
2052: \begin{array}{|crcl|}
2053: \hline
2054: (E_k) & x = y & \leftrightarrow &
2055: \forall z \, (z \in x \leftrightarrow z \in y) \\
2056: \hline
2057: \end{array}$$
2058:
2059:
2060:
2061: \begin{lemma}\label{corrset}
2062: Let $C$ be a \set-constraint, $C_1,\dots,C_k$ be the constraints
2063: non-determini\-stically returned by {\sf neq-Set}$(C)$\/, and
2064: $\bar N_i = \vars(C_i) \setminus \vars(C)$\/. Then ${\cal SET}
2065: \models \forall \left(C \leftarrow \bigvee_{i=1}^{k} \exists
2066: \bar N_i C_i \right)$\/.
2067: \end{lemma}
2068: \begin{proof}
2069: For rules $(1)$--$(5)$ the result follows from those for lists.
2070: Rules $(7.1)$ and $(7.2)$ are exactly axiom $(F^s_3)$\/.
2071: Rule $(6)$ is axiom $(E_k)$\/, implied by $(E^s_k)$ on
2072: $\cal SET$.
2073: \end{proof}
2074:
2075: \begin{remark}
2076: %\subsection{Discussion}
2077:
2078: In our theories an aggregate can be built by starting from any
2079: ground uninterpreted Herbrand term---called the
2080: \emph{kernel}---and then adding to this term the elements
2081: that compose the aggregate. Thus, two aggregates can contain the
2082: same elements but nevertheless they can be different because of
2083: their different kernels. For example, the two terms $\{a\,|\,b\}
2084: \mbox{ and } \{a\,|\,c\}$ denote two different sets containing
2085: the same elements ($a$) but based on different kernels ($b$ and
2086: $c$, respectively).
2087:
2088: Rewriting rules for disequality constraints over aggregates other
2089: than sets are formulated in such a way to take care of the
2090: (possibly different) kernels in the two aggregates without having
2091: to explicitly resort to kernels. Conversely, the rewriting rule
2092: for disequality constraints over sets (rule (6)) is not able to
2093: ``force'' disequality between two sets when they have the same
2094: elements but different kernels. This the reason why the
2095: $(\rightarrow)$ direction of Lemma \ref{corrset} does not hold.
2096:
2097: A possible completion of the above procedures to take care of this
2098: case is presented in~\cite{DR93}; for doing that some technical
2099: complications are introduced. Basically, a new constraint
2100: ($\ker$) is introduced and the rewriting rule (6) is endowed with
2101: a third non-deterministic case: $\ker(s_1) \neq \ker(s_2)$. The
2102: advantage of this solution is completeness (the $(\rightarrow)$
2103: direction of Lemma~\ref{corrset}). However, for the sake of
2104: simplicity, we do not add here the details on the modifications of
2105: the rewriting rules for dealing with $\ker$ that are instead
2106: presented in~\cite{DR93}.
2107: \end{remark}
2108:
2109:
2110: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2111: \section{Constraint solving}\label{constraint-solving}
2112: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2113:
2114: In this section we address the problem of establishing if a
2115: constraint $C$ is satisfiable or not in the corresponding privileged
2116: model. The correspondence result (Theorem \ref{corrispondenza})
2117: ensures that the property is inherited by any model.
2118:
2119: Constraint satisfiability for the theory $\Th$ is checked by the
2120: non-deterministic rewriting procedure ${\sf SAT}_{\Th}$\/ shown in
2121: Figure~\ref{figuraSAT}. Its definition is completely parametric
2122: with respect to the theory involved. ${\sf SAT}_{\Th}$ uses
2123: iteratively the various rewriting procedures presented in the
2124: previous section, until a fixed-point is reached---i.e., any new
2125: rewritings do not further simplify the constraint. This happens
2126: exactly when the constraint is in pre-solved form or it is
2127: \false. The two conditions that guarantee that a constraint in
2128: pre-solved form is in solved form are tested by function ${\sf
2129: is\_solved}_{\Th}$ shown in Figure~\ref{acyclic-proc}.
2130:
2131: By Theorem~\ref{all solved} a constraint in solved form is
2132: guaranteed to be satisfiable in the corresponding model.
2133: Moreover, it will be proved (see Theorem~\ref{bagscorrect}) that
2134: the disjunction of solved form constraints returned by ${\sf
2135: SAT}_{\Th}$ is equi-satisfiable in that model to the original
2136: constraint $C$\/. Therefore, ${\sf SAT}_{\Th}$ can be used as a
2137: test procedure to check satisfiability of $C$: if it is able to
2138: reduce $C$ to at least one solved form constraint $C'$ then $C$ is
2139: satisfiable; otherwise, $C$ is unsatisfiable. Moreover, the
2140: generated constraint in solved form can be immediately exploited
2141: to compute all possible solutions for $C$\/.
2142:
2143: \begin{figure}[htb]
2144: {\small
2145: %%\renewcommand{\arraystretch}{\scala}
2146: $$\begin{array}{||rcl||}
2147: \hline\hline
2148: \multicolumn{3}{||l||}
2149: {\mbox{\sf function {\sf SAT}$_{\Th}$}(C)}\\
2150: \multicolumn{3}{||l||}
2151: {\phantom{aaa}{\sf repeat}}\\
2152: & & \phantom{aaa} C' := C;\\
2153: & & \phantom{aaa} C := \mbox{\sf Unify\_{$\Th$s}}(
2154: \mbox{\sf neq-$\Th$}(
2155: \mbox{\sf nin-$\Th$}(
2156: \mbox{\sf in-$\Th$}(C))))\\
2157: \multicolumn{3}{||l||}{\phantom{aaa} {\sf until}\;C = C';}\\
2158: \multicolumn{3}{||l||}{\phantom{aaa} \mbox{\sf return(
2159: is\_solved}_{\Th}(C)).}\\
2160: \hline\hline
2161: \end{array}$$}
2162: \vspace{-5pt}\caption{\label{figuraSAT}The satisfiability
2163: procedure, parametric with respect to $\Th$}\vspace{+10pt}
2164: \end{figure}
2165:
2166: \begin{figure}
2167: {\small
2168: %%\renewcommand{\arraystretch}{\scala}
2169: $$\begin{array}{||l||}
2170: \hline\hline
2171: \mbox{\sf function is\_solved$_{\Th}$}(C)\\
2172: \phantom{aaa}\mbox{\sf build the directed graph ${\cal
2173: G}_{C}^{\in}$};\\
2174: \phantom{aaa}\mbox{\sf if ${\cal G}_{C}^{\in}$ has a
2175: cycle}\\
2176: \phantom{aaaaaa}\mbox{\sf then return \false}\\
2177: \phantom{aaaaaa}\mbox{\sf else}\\
2178: \phantom{aaaaaaaaa}\mbox{compute $\sigma_C^*$}\\
2179: \phantom{aaaaaaaaa}\mbox{\sf if there is a pair $t \in X , t'
2180: \notin X$
2181: in $C$ s.t. $\Th \models \forall (\sigma_C^*(t) = \sigma_C^*(t'))$}\\
2182: \phantom{aaaaaaaaaaaa}\mbox{\sf then return \false}\\
2183: \phantom{aaaaaaaaaaaa}\mbox{\sf else return $C$\/.}\\
2184: \hline\hline
2185: \end{array}$$}
2186: \vspace{-5pt}\caption{\label{acyclic-proc}Final check for solved
2187: form constraints}\vspace{+10pt}
2188: \end{figure}
2189:
2190: The rest of this section is devoted to prove the crucial result of
2191: termination for procedure ${\sf SAT}_{\Th}(C)$ and, then, to prove
2192: its soundness and completeness.
2193:
2194: \begin{theorem}[Termination]
2195: \label{termina-lists} \label{termina-bags} \label{termina-clist}
2196: \label{termina-set}
2197:
2198: Let $\Th$ be one of the theories \lst, \bag, \clist, \set, and $C$
2199: be a $\Th$-constraint. Each non-determi\-nistic execution of $ {\sf
2200: SAT}_{\Th}(C) $\/ terminates in a finite number of steps.
2201: Moreover, the constraint returned is either $\false$ or a solved
2202: form constraint.
2203: \end{theorem}
2204: \begin{proof}
2205: We give the proof for the case of \bag. The other proofs are in
2206: Appendix~\ref{termination}.
2207:
2208: It is immediate to see, by the definition of the procedures, that
2209: if $C$ is different from $\false$ and not in pre-solved form,
2210: then some rewriting rule can be applied. The function ${\sf
2211: is\_solved_{\bag}}$, whose termination follows from termination
2212: of {\sf Unify\_msets}~\cite{DPR98-fuin}, needed for the solved
2213: form test $\Th \models\forall (\sigma_C^*(t) =
2214: \sigma_C^*(t'))$\/, produces by definition solved form
2215: constraints or \false.
2216:
2217: We prove that the {\sf repeat} cycle can not loop forever. For
2218: doing that, we define a complexity measure for constraints. Let us
2219: assume that constraints of the form $X=t$\/, with $X$ neither in
2220: $t$ nor elsewhere in $C$\/, are removed from $C$\/. Similarly, we
2221: assume that $\true$ constraints are not counted in the complexity
2222: measure. These two assumptions are safe since those constraints
2223: do not fire any new rule application. The complexity measure that
2224: we associate with a constraint is the following triple:
2225: $$\begin{array}{rclll} compl(C) & = & \langle &
2226: \alpha(C) = \mbox{\# vars in $C$},\\ &&& \beta(C) = \mo \size(s) +
2227: \size(t) : s \mathbin{op} t \in C \mc , \\ &&& \gamma(C) =
2228: \sum_{s\:\mathbin{op}\:t \in C} \size(s) &\rangle
2229: \end{array}$$
2230:
2231: The first and third element of the tuple are non-negative
2232: integers. The second is a multiset of non-negative integers.
2233: They are well-ordered~\cite{DM79} by the ordering obtained as
2234: the transitive closure of the rule:
2235: $$\mo s_1,\dots,s_{i-1},t_1,\dots,t_n,s_{i+1},\dots,s_m\mc
2236: \prec
2237: \mo s_1,\dots, s_m\mc \,,$$
2238: for $i \in \{1,\dots,m \}$\/, $n \geq 0$\/,
2239: $t_{1} < s_{i},\dots,t_{n}< s_{i}$\/.
2240: The ordering on triples
2241: is the (well-founded) lexicographical ordering.
2242:
2243: We will prove that given a constraint $C$, in a finite number of
2244: non-failing successive rule applications, a constraint $C'$ with
2245: lower complexity is reached. We show, by case analysis, this
2246: property. Most rule applications decreases the complexity in one
2247: step. When this does not happen, we enter in more detail.
2248:
2249: \begin{description}
2250: \item[{\sf Unify\_msets}$(1)$] $\alpha$ does not increase,
2251: $\beta$ decreases.
2252: \item[{\sf Unify\_msets}$(2)$] $\alpha$ and $\beta$ do not increase.
2253: $\gamma$ decreases, since $\size(X) = 0$ and $\size(t) > 0$\/.
2254: \item[{\sf Unify\_msets}$(3)$] $\alpha$ decreases by 1.
2255: \item[{\sf Unify\_msets}$(6)$] $\alpha$ does not increase.
2256: $\beta$ decreases, since
2257: an equation of size $1 + \sum_{i=1}^m \size(s_i) +
2258: \size(t_i)$
2259: is replaced by $m$ smaller equations of size $\size(s_i) +
2260: \size(t_i)$\/.
2261: \item[{\sf Unify\_msets}$(7)$] In this case the complexity may
2262: remain unchanged at the first step. However, the unification
2263: algorithm adopts a selection strategy that ensures that after a
2264: finite number of steps, we either reach a situation such that
2265: $\alpha$ decreases or a situation where $\alpha$ is unchanged and
2266: $\beta$ decreases (see~\cite{DPR98-fuin} for details).
2267: \item[{\sf Unify\_msets}$(8)$] After one rule application, we
2268: are in the case $(7)$ with both the tails of the multisets non
2269: variables. After a finite number of steps, we enter the situation
2270: where $\alpha$ is unchanged and $\beta$ decreases.
2271: %%%%%%%%%%%
2272: \item[{\sf in-MSet}$(2)$]
2273: $\alpha$ does not increase. $\beta$ decreases, since
2274: a constraint of size $1 + \size(r) + \size(s) + \size(t)$
2275: is non-deterministically replaced by one of smaller size
2276: $\size(r) + \size(s)$ or $\size(r) + \size(t)$\/.
2277:
2278: \item[{\sf nin-MSet}$(1),(3)$]
2279: Trivially, $\alpha$ does not increase and $\beta$ decreases.
2280:
2281: \item[{\sf nin-MSet}$(2)$]
2282: $\alpha$ does not increase. $\beta$ decreases, since
2283: a constraint of size $1 + \size(r) + \size(s) + \size(t)$
2284: is non-deterministically replaced by two of smaller size
2285: $\size(r) + \size(s)$ and $\size(r) + \size(t)$\/.
2286: %%%%%%%%%%%%%%
2287: \item[{\sf neq-MSet}$(2),(7)$]
2288: Trivially, $\alpha$ does not increase and $\beta$ decreases.
2289: \item[{\sf neq-MSet}$(3)$]
2290: $\alpha$ and $\beta$ do not increase.
2291: $\gamma$ decreases, since $\size(X) = 0$ and $\size(t) > 0$.
2292: \item[{\sf neq-MSet}$(5)$]
2293: $\alpha$ does not increase. $\beta$ decreases, since
2294: a constraint of size $1 + \sum_{i=1}^m \size(s_i) +
2295: \size(t_i)$
2296: is non-deterministically replaced by one of size
2297: $\size(s_i) + \size(t_i)$\/.
2298: \item[{\sf neq-MSet}$(6.2)$] A unique application of
2299: this rule may not decrease the constraint complexity.
2300: Thus, we enter in some detail. The rule
2301: removes
2302: $\mo t_1 \,|\, s_1 \mc \neq \mo t_2 \,|\, s_2 \mc$
2303: and introduces
2304: \begin{eqnarray}
2305: &&\mo t_2 \,|\, s_2 \mc = \mo t_1 \,|\, N \mc \wedge
2306: \label{stella}\\
2307: &&s_1 \neq N \label{duestelle}
2308: \end{eqnarray}
2309: Consider now the two cases:
2310: \begin{enumerate}
2311: \item $\mo t_2 \,|\, s_2 \mc$ is $\mo r_{1},\dots,r_{n}\mc$
2312: \item $\mo t_2 \,|\, s_2 \mc$ is $\mo
2313: r_{1},\dots,r_{n}\,|\,A\mc$\/, for
2314: some variable $A$ distinct from $N$ that has just been
2315: introduced.
2316: \end{enumerate}
2317: In the first case the successive execution of {\sf Unify\_{bags}}
2318: replaces equation (\ref{stella}) by:
2319: $$t_{1} = r_{i}, N = \mo
2320: r_{1},\dots,r_{i-1},r_{i+1},\dots,r_{n} \mc$$
2321: for some $i = 1,\dots,n$\/.
2322: We have that
2323: $$size(t_{1}) + \size(r_{i}) <
2324: \size(\mo t_1 \,|\, s_1 \mc) + \size(\mo t_2 \,|\, s_2
2325: \mc).$$ The equation $ N = \mo
2326: r_{1},\dots,r_{i-1},r_{i+1},\dots,r_{n}\mc$ is eliminated by
2327: applying the substitution for $N$\/. $N$ occurs only in the
2328: constraint $s_{1} \neq N$\/, that becomes $s_{1} \neq \mo
2329: r_{1},\dots,r_{i-1},r_{i+1},\dots,r_{n}\mc$\/. Again, its $size$
2330: is strictly smaller than that of the original disequality
2331: constraint. Thus, after some further steps, $\alpha$ remains
2332: unchanged while $\beta$ decreases.
2333: Strictly speaking, some other
2334: actions may occur during that sequence of actions. However, if no
2335: other rule $(6.2)$ is executed, then all rules decrease the
2336: complexity tuples. Conversely, if other rules of this form are
2337: executed, then we need to wait for all the substitutions of this
2338: form to be applied. But they are all independent processes.
2339:
2340: The second case is similar, but in this case a substitution
2341: also for $A$ is computed, ensuring that $\alpha$ decreases.
2342:
2343: \item[{\sf neq-MSet}$(6.1)$] After one step, we are in
2344: the above situation $(6.2)$.
2345: \end{description}
2346: \end{proof}
2347: The soundness and completeness result of the global constraint
2348: solving procedure for \lst, \bag, and \clist\ follows from the
2349: lemmas in the previous section and two lemmas in the
2350: Appendix~\ref{modellistiche}.
2351:
2352:
2353:
2354: \begin{theorem}[Soundness - Completeness]
2355: \label{listcorrect} \label{bagscorrect} \label{clistcorrect}
2356: \label{setcorrect} Let $\Th$ be one of the theories \lst, \bag,
2357: \clist, and \set, $C$ be a $\Th$-constraint, and $C_1,\dots,C_k$
2358: be the solved form constraints non-determi\-nistically returned by
2359: ${\sf SAT}_{\Th}(C)$\/, and $\bar N_i$ be $\vars(C_i) \setminus
2360: \vars(C)$\/. Then ${\cal A}_{\Th} \models \forall \left(C
2361: \leftrightarrow \bigvee_{i=1}^{k} \exists \bar N_i C_i \right)$\/,
2362: where ${\cal A}_{\Th}$ is the model which corresponds with $\Th$.
2363: \end{theorem}
2364: \begin{proof}
2365: Theorem~\ref{termina-lists} ensures the termination of each
2366: non-deterministic branch. At each branch point, the number of
2367: non-deterministic choices is finite. Thus, $C_1,\dots,C_k$ can be
2368: effectively computed. Soundness and completeness follow from the
2369: results proved individually for the procedures involved:
2370: Lemma~\ref{tuttimember} for {\sf in}-$\Th$ and {\sf nin}-$\Th$\/;
2371: Lemma~\ref{corrlist}, Lemma~\ref{corrbag},
2372: Lemma~\ref{corrclists}, and Lemma~\ref{corrset} for {\sf
2373: neq-MSet}, {\sf neq-List}, {\sf neq-CList}, and {\sf neq-Set},
2374: respectively; Lemma~\ref{uffa} for ${\sf is\_solved_\Th(C)}$;
2375: \cite{DPR98-fuin} for unification.
2376: \end{proof}
2377:
2378: \begin{corollary}[Decidability]\label{decidlist}
2379: Given a $\Th$-constraint $C$\/, it is decidable whether ${\cal A}
2380: \models \exists\, C$\/, where ${\cal A}$ is one of the
2381: privileged models $\cal LIST$\/, $\cal MSET$\/, $\cal CLIST$\/, $\cal
2382: SET$\/.
2383: \end{corollary}
2384: \begin{proof}
2385: {F}rom Theorem~\ref{listcorrect} we know that $C$ is
2386: equi-satisfiable to $C_1 \vee \cdots \vee C_k$\/. If all the $C_i$
2387: are $\false$\/, then $C$ is unsatisfiable in $\cal LIST$ ($\cal
2388: MSET$\/, $\cal CLIST$\/, $\cal SET$). Otherwise, it is
2389: satisfiable, since solved form constraints are satisfiable
2390: (Theorem~\ref{all solved}).
2391: \end{proof}
2392:
2393: \subsection{Complexity Issues}
2394:
2395: Complexity of the four unification problems is studied
2396: in~\cite{DPR98-fuin}: the decision problem for unification
2397: is proved to be solvable in linear time for lists, and
2398: it is NP-complete for the other cases.
2399:
2400: In the case of lists, if the constraint is a conjunction of
2401: equality and disequality constraints, then the satisfiability
2402: problem for a constraint $C$ is solvable in $O(n^{2})$ where $n =
2403: |C|$~\cite{BN98,CB83}. Instead, the satisfiability problem for
2404: conjunctions of membership and disequality constraints over lists
2405: %%(and, thus, the satisfiability problem for \lst-constraints)
2406: is NP-hard. As a matter of fact, let us consider the following
2407: instance of 3-SAT:
2408: $$(X_1 \vee X_2 \vee \neg X_3) \wedge
2409: (\neg X_1 \vee X_2 \vee X_3) \wedge
2410: (X_1 \vee \neg X_2 \vee X_3)\;.$$
2411: The above instance of
2412: 3-SAT can be re-written as the following
2413: constraint problem:
2414: $$\begin{array}[t]{ccccc}
2415: X_1 \in [\underline{0}, \underline{1}] & \wedge &
2416: Y_1 \in [\underline{0}, \underline{1}] & \wedge & \\
2417: {[X_1,Y_1]} \neq [ \underline{0}, \underline{0}] & \wedge &
2418: [X_1,Y_1] \neq [ \underline{1}, \underline{1}] & \wedge &\\
2419: X_2 \in [\underline{0}, \underline{1}] & \wedge &
2420: Y_2 \in [\underline{0}, \underline{1}] & \wedge & \\
2421: {[X_2,Y_2]} \neq [ \underline{0}, \underline{0}] & \wedge &
2422: [X_2,Y_2] \neq [ \underline{1}, \underline{1}] & \wedge &\\
2423: X_3 \in [\underline{0}, \underline{1}] & \wedge &
2424: Y_3 \in [\underline{0}, \underline{1}] & \wedge & \\
2425: {[X_3,Y_3]} \neq [ \underline{0}, \underline{0}] & \wedge &
2426: [X_3,Y_3] \neq [ \underline{1}, \underline{1}] & \wedge &\\
2427: {[ X_1,X_2,Y_3]} \neq [ \underline{0}, \underline{0},
2428: \underline{0}] & \wedge &
2429: [ Y_1,X_2,X_3] \neq [ \underline{0}, \underline{0},
2430: \underline{0}] & \wedge &
2431: [ X_1, Y_2, X_3 ] \neq [ \underline{0}, \underline{0},
2432: \underline{0}]
2433: \end{array} $$
2434: where $\underline{0}$ and $\underline{1}$ can be represented by
2435: $\nil$ and $[\nil]$\/, respectively, and $Y_i$ takes the place of
2436: $\neg X_i$ and vice versa. It is immediate to prove that any
2437: substitution satisfying the constraint problem is also a solution
2438: for the above formula, provided $\underline{0}$ is interpreted as
2439: {\false} and $\underline{1}$ is interpreted as {\true}, and vice
2440: versa.
2441:
2442: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2443: \section{Conclusions}\label{conclusions}
2444: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2445:
2446: In this paper we have extended the results of~\cite{DPR98-fuin}
2447: studying the constraint solving problem for four different
2448: theories: the theories of lists, multisets, compact
2449: lists, and sets. The analyzed constraints are conjunctions of
2450: literals based on equality and membership predicate symbols. We
2451: have identified the privileged models for these theories by
2452: showing that they correspond with the theories on the class of
2453: considered constraints. We have developed a notion of solved form
2454: (proved to be satisfiable) and presented the rewriting algorithms
2455: which allow this notion to be used to decide the satisfiability
2456: problems in the four contexts.
2457:
2458: In particular, we have shown how constraint solving can be
2459: developed parametrically for these theories and we have pointed
2460: out the differences and similarities between the four kinds of
2461: aggregates.
2462:
2463: As further work it could be interesting to study the properties of
2464: the four aggregates in presence of
2465: append-like operators (\emph{append} for lists, $\cup$ for sets,
2466: $\uplus$ for multisets). These
2467: operators can not be defined without using universal quantifiers
2468: (or recursion) with the languages analyzed in this
2469: paper~\cite{DPP00-nancy}.
2470:
2471: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2472: \baselineskip 10pt \small
2473:
2474: \subsection*{Acknowledgments}
2475: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2476:
2477: The authors wish to thank Alberto Policriti, Ashish Tiwari, and
2478: Silvia Monica for useful discussions on the topics of this paper.
2479: The anonymous referee greatly helped us in improving the
2480: presentation of the paper. This work is partially supported by
2481: MIUR project \emph{Ragionamento su aggregati e numeri a supporto
2482: della programmazione e relative verifiche}.\vspace*{-2ex}
2483:
2484: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2485: % \bibliographystyle{plain}
2486: % \bibliography{fundamenta2}
2487: \begin{thebibliography}{10}
2488: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2489:
2490: \bibitem{ADR99}
2491: D.~Aliffi, A.~Dovier, and G.~Rossi.
2492: \newblock From {S}et to {H}yperset {U}nification.
2493: \newblock {\em Journal of Functional and Logic Programming},
2494: 1999(10):1--48. The MIT Press, September 1999.
2495:
2496: \bibitem{BN98}
2497: F. Baader and T. Nipkow.
2498: \newblock {\em Term Rewriting and All That}.
2499: \newblock Cambridge University Press, Cambridge, 1998
2500:
2501: \bibitem{BM93}
2502: J.~Banatre and D. Le Metayer.
2503: \newblock Programming by Multiset Transformation.
2504: \newblock \emph{Communications of the ACM},
2505: 36(1):98--111. January 1993.
2506:
2507: %\bibitem{BB98}
2508: %G. Berry and G. Boudol.
2509: %\newblock The Chemical Abstract Machine.
2510: %\newblock \emph{Theoretical Computer Science}, vol. 96 (1992) 217-248.
2511:
2512: \bibitem{BNST91}
2513: C. Beeri, S. Naqvi, O. Shmueli, and S. Tsur.
2514: \newblock {S}et {C}onstructors in a {L}ogic {D}atabase {L}anguage.
2515: \newblock {\em Journal of Logic Programming 10}, 3 (1991), 181--232.
2516:
2517: %\bibitem{COP90}
2518: %D.~Cantone, E.~G. Omodeo, and A.~Policriti.
2519: %\newblock The Automation of Syllogistic. II. Optimization
2520: %and Complexity Issues.
2521: %\newblock {\em Journal of Automated Reasoning}, 6:173--187,
2522: %1990.
2523:
2524: \bibitem{CK73}
2525: C.~C. Chang and H.~J. Keisler.
2526: \newblock {\em Model {T}heory}.
2527: \newblock {S}tudies in {L}ogic. North Holland, 1973.
2528:
2529: \bibitem{Cla78}
2530: K.~L. Clark.
2531: \newblock Negation as {F}ailure.
2532: \newblock In H.~Gallaire and J.~Minker, editors, {\em Logic
2533: and Databases},
2534: pages 293--321. Plenum Press, 1978.
2535:
2536: \bibitem{CB83}
2537: J. Corbin and M. Bidoit.
2538: \newblock A rehabilitation of Robinson's
2539: unification algorithm.
2540: \newblock In R.Mason ed., \emph{Information
2541: Processing 1983}, Elevisier Science Publishers (North
2542: Holland), pp. 909--914.
2543:
2544: \bibitem{DV99}
2545: E. Dantsin and A. Voronkov.
2546: \newblock A Nondeterministic Polynomial-Time
2547: Unification Algorithm for Bags, Sets and Trees.
2548: \newblock In W. Thomas ed., \emph{Foundations of Software Science and
2549: Computation Structure}, Lecture Notes in Computer Science,
2550: Vol.~1578, pages 180--196, 1999.
2551:
2552: \bibitem{DM79}
2553: N. Dershowitz and Z. Manna.
2554: \newblock {Proving Termination with Multiset Ordering}.
2555: \newblock {\em Communication of the ACM 22}, 8 (1979),
2556: 465--476.
2557:
2558: \bibitem{DPP00-nancy}
2559: A.~Dovier, C. Piazza, and A.~Policriti.
2560: \newblock Comparing expressiveness of set constructor symbols.
2561: \newblock In H. Kirchner and C. Ringeissen, eds., \emph{FROCOS'00},
2562: LNCS No. 1794, pp. 275--289, 2000.
2563:
2564: \bibitem{DPR98-fuin}
2565: A.~Dovier, A.~Policriti, and G.~Rossi.
2566: \newblock A uniform axiomatic view of lists, multisets, and
2567: sets, and the relevant unification algorithms.
2568: \newblock {\em Fundamenta Informaticae}, 36(2/3):201--234,
2569: 1998.
2570:
2571: \bibitem{JLP1}
2572: A.~Dovier, E.~G. Omodeo, E.~Pontelli, and G.~Rossi.
2573: \newblock \{log\}: {A} {L}anguage for {P}rogramming in
2574: {L}ogic with {F}inite {S}ets.
2575: \newblock {\em Journal of Logic Programming}, 28(1):1--44,
2576: 1996.
2577:
2578: \bibitem{DPPR00}
2579: A.~Dovier, C. Piazza, E.~Pontelli, and G.~Rossi.
2580: \newblock Sets and constraint logic programming.
2581: \newblock \emph{ACM Transaction on Programming Language and
2582: Systems}, 22(5):861--931, 2000.
2583:
2584: \bibitem{DR93}
2585: A.~Dovier and G.~Rossi.
2586: \newblock Embedding {E}xtensional {F}inite {S}ets in {CLP}.
2587: \newblock In D.~Miller, editor, {\em Proc. of International
2588: Logic Programming Symposium, ILPS'93}. The MIT Press, Cambridge,
2589: Mass., October 1993, pages 540--556.
2590: %\newblock Vancouver, BC, Canada.
2591:
2592: \bibitem{End73}
2593: H.~B. Enderton.
2594: \newblock {\em A mathematical introduction to logic}.
2595: \newblock Academic Press, 1973.
2596: \newblock $2^{nd}$ printing.
2597:
2598: \bibitem{Ger97}
2599: C.~Gervet.
2600: \newblock Interval {P}ropagation to {R}eason about {S}ets:
2601: {D}efinition and
2602: {I}mplementation of a {P}ractical {L}anguage.
2603: \newblock {\em Constraints}, 1:191--246, 1997.
2604:
2605: \bibitem{GM96}
2606: S.~Grumbach and T.~Milo.
2607: \newblock Towards tractable algebras for bags.
2608: \newblock {\em Journal of Computer and System Sciences},
2609: 52(3):570--588, 1996.
2610:
2611: \bibitem{HL94}
2612: P.~M. Hill and J.~W. Lloyd.
2613: \newblock {\em {T}he {G\"odel} {P}rogramming {L}anguage}.
2614: \newblock The MIT Press, Cambridge, Mass., 1994.
2615:
2616: \bibitem{JM94}
2617: J.~Jaffar and M.~J. Maher.
2618: \newblock Constraint {L}ogic {P}rogramming: {A} {S}urvey.
2619: \newblock {\em Journal of Logic Programming},
2620: 19--20:503--581, 1994.
2621:
2622: %\bibitem{JMMS98}
2623: %J.~Jaffar, M.~J. Maher, K. Marriott, and P.~J. Stuckey.
2624: %\newblock {The Semantics of Constraint Logic Programs}.
2625: %\newblock {\em Journal of Logic Programming\/}~{\em 37,\/}~1--3, 1--46.
2626:
2627: %\bibitem{KN86}
2628: %{D. Kapur and P. Narendran}.
2629: %\newblock {{NP}-Completeness of the Set Unification and
2630: %Matching Problems},
2631: %\newblock In {J. H. Siekmann ed.},
2632: %{8th International Conference on Automated Deduction},
2633: %LNCS n. 230,
2634: %pp. {489--495}, Springer-Verlag, 1986.
2635:
2636: %\bibitem{Kun80}
2637: %K.~Kunen.
2638: %\newblock {\em Set {T}heory. An {I}ntroduction to
2639: %{I}ndependence {P}roofs}.
2640: %\newblock {S}tudies in {L}ogic. North Holland, 1980.
2641:
2642: \bibitem{Mal71}
2643: A.~Mal'cev.
2644: \newblock {A}xiomatizable {C}lasses of {L}ocally {F}ree
2645: {A}lgebras of {V}arious {T}ypes.
2646: \newblock In {\em The Metamathematics of Algebraic Systems},
2647: Collected Papers,
2648: chapter~23. North Holland, 1971.
2649:
2650: %\bibitem{MM82}
2651: %A.~Martelli and U.~Montanari.
2652: %\newblock An efficient unification algorithm.
2653: %\newblock {\em ACM Transactions on Programming Languages and
2654: %Systems},
2655: % 4:258--282, 1982.
2656:
2657: %\bibitem{PW79}
2658: %M.~S. Paterson and M.~N. Wegman.
2659: %\newblock Linear unification.
2660: %\newblock {\em Journal of Computer and System Science},
2661: %16(2):158--167, 1978.
2662:
2663: \bibitem{PST96}
2664: B. Potter, J. Sinclair, and D. Till.
2665: \newblock \emph{An Introduction to Formal Specification and Z},
2666: Second Edition.
2667: \newblock Prentice Hall, 1996.
2668:
2669: \bibitem{SDDS86}
2670: J.~T. Schwartz, R. B.~K. Dewar, E. Dubinsky, and E. Schonberg.
2671: \newblock {\em Programming with sets, an introduction to SETL.}
2672: \newblock Springer-Verlag, Berlin, 1986.
2673:
2674: \bibitem{Sie90}
2675: J.~H. Siekmann.
2676: \newblock Unification theory.
2677: \newblock In C.~Kirchner, editor, {\em Unification}.
2678: Academic Press, 1990.
2679:
2680: \bibitem{Stu95}
2681: P.~J. Stuckey.
2682: \newblock Negation and {C}onstraint {L}ogic {P}rogramming.
2683: \newblock {\em Information and Computation\/}~{\em 1}, 12--33.
2684:
2685:
2686: \bibitem{TZO98}
2687: A. Tzouvaras.
2688: \newblock The Linear Logic of Multisets.
2689: \newblock \emph{Logic Journal of the IGPL}, Vol. 6,
2690: No. 6,. pp. 901--916, 1998.
2691:
2692: \end{thebibliography}
2693:
2694: \newpage
2695: \appendix
2696:
2697: \section{Proofs of Model Properties}\label{modellistiche}
2698:
2699: We recall some technical definitions.
2700: Given two $\Sigma$-structures ${\cal A}$ and ${\cal B}$, $ {\cal
2701: B} = \langle B, (\cdot)^{\cal B}\rangle$ is a \emph{substructure}
2702: of ${\cal A} = \langle A, (\cdot)^{\cal A}\rangle$ if $B \subseteq
2703: A$ and for all $x \in B$ it holds that $(x)^{\cal A} = (x)^{\cal B}$.
2704: Given two
2705: $\Sigma$-structures ${\cal A}$ and ${\cal B}$, a function
2706: $h:A\longrightarrow B$ is said to be an \emph{homomorphism} from
2707: $\cal A$ to $\cal B$ if: $(i)$ $\forall f\in {\cal F}, a_1,\dots,
2708: a_n\in A \: (h(f^{\cal A}(a_1,\dots,a_n))=f^{\cal
2709: B}(h(a_1),\dots,h(a_n))) $ and $(ii)$ $ \forall p\in \Pi,
2710: a_1,\dots,a_m\in A \:(p^{\cal A}(a_1,\dots,a_m)\rightarrow p^{\cal
2711: B}(h(a_1),\dots,h(a_m)))\,.$ $h$ is said to be an
2712: \emph{isomorphism} if $f$ is bijective and in the property~$(ii)$
2713: also the $\leftarrow$ implication holds. Given two
2714: $\Sigma$-structures $\cal A$ and $\cal B$\/, an \emph{embedding} of
2715: $\cal A$ in $\cal B$ is an isomorphism from $\cal A$ to a
2716: substructure of $\cal B$\/.
2717:
2718:
2719: \begin{lemma}[\cite{CK73}]\label{logica}
2720: Let $\cal A$ and $\cal B$ be two $\Sigma$-structures
2721: and let $h$
2722: be an embedding of $\cal A$ in $\cal B$\/.
2723: If $\varphi$ is an open formula of ${\cal
2724: L} = \langle \Sigma, {\cal V}\rangle $\/,
2725: then for each valuation $\sigma$ on $A$
2726: it holds that:
2727: $${\cal A}\models \sigma(\varphi) \leftrightarrow {\cal
2728: B}\models h(\sigma(\varphi))\,.$$
2729: \end{lemma}
2730:
2731:
2732: %\noindent {\bf Lemma \ref{versofacile}.}~
2733: \begin{lemma}\label{versofacile}
2734: $\cal MSET$ is a model of the theory \bag.
2735: \end{lemma}
2736: %\par\smallskip\par\noindent
2737:
2738: \begin{proof}
2739: For each axioms/axiom schemata $(A)$ of the theory \bag\ we need
2740: to prove that ${\cal MSET}$ models $(A)$ (briefly, ${\cal MSET}
2741: \models (A)$). We give only the sketch of the proof.
2742: \begin{description}
2743:
2744: \item[$(K),(W)$\/:]
2745: The fact that ${\cal MSET}$ is a model of $(K)$ and $(W)$ is a
2746: consequence of the interpretation of the membership predicate in
2747: $\cal MSET$ (cf.\ point (4) of Def.~\ref{defstruttura}).
2748:
2749: \item[$(F^m_1)$\/:] This axiom holds in $\cal MSET$\/, since
2750: $f(t_1,\dots,t_n)$ and $f(s_1,\dots,s_n)$ can be in the same class
2751: in $\cal MSET$\/, only if for all $i=1,\dots, n$ it holds that
2752: $t_i$ and $s_i$ belong to the same class.
2753:
2754: \item[$(F_2)$\/:] It holds trivially, by definition of $\cal
2755: MSET$\/, since terms beginning with different free symbols belong
2756: to different classes.
2757:
2758: \item[$(F_3),(F_3^m)$\/:]
2759: The fact that ${\cal MSET} \models (F_3)$ and ${\cal MSET} \models
2760: (F_3^m)$ holds in virtue of the finite size of each ground term;
2761: it can be formally proved by induction on the complexity of the
2762: terms.
2763:
2764: \item[$(E_p^m)$\/:]
2765: $\cal MSET$ is a model of $(E_p^m)$\/, since for any equational
2766: theory $E$\/, $T({\cal F})/\equiv_E$ is a model of
2767: $E$~\cite{Sie90}.
2768:
2769: \item[$(E_k^m)$\/:]
2770: $\cal MSET$ is a model of $(E_p^m)$\/, as seen in the previous
2771: point, but it is also the \emph{initial} model, namely two terms
2772: $s$ and $t$ are in the same class if and only if $(E_p^m)$ can
2773: prove that $s=t$\/. This is exactly the meaning of the axiom
2774: $(E_k^m)$.
2775: \end{description}
2776: \end{proof}
2777:
2778: %\noindent {\bf Lemma \ref{versodifficile}.}
2779: \begin{lemma}\label{versodifficile}
2780: If $\cal M$ is a model of \bag, then the function $ h: T({\cal
2781: F}_{MSet})/\equiv_{E_{MSet}} \longrightarrow { M}$\/, defined as
2782: $h(\rappr{t}) = t^{\cal M}$ is an embedding of ${\cal MSET}$ in
2783: ${\cal M}$. \par\smallskip\par\noindent
2784: \end{lemma}
2785: \begin{proof}
2786: We will prove the following facts:
2787:
2788: \begin{enumerate}
2789: \item The definition of $h(\rappr{t})$ does not depend on the
2790: choice of the representative of the class;
2791: \item $h$ is an homomorphism;
2792: \item $h$ is injective;
2793: \item if $h(\rappr{t})\in^{\cal M}h(\rappr{s})$\/,
2794: then $\rappr{t}\in^{\cal MSET}\rappr{s}$\/.
2795: \end{enumerate}
2796:
2797: \noindent These facts imply the thesis.
2798:
2799: \begin{enumerate}
2800: \item If $t_1$ and $t_2$ are two terms such that
2801: $\rapprmedio{t_1}=\rapprmedio{t_2}$\/, then by
2802: definition $(E_p^m)\models t_1=t_2$\/.
2803: Since ${\cal A}\models t_1=t_2$ holds in
2804: every model ${\cal A}$ of
2805: $(E_p^m)$\/, then in particular it holds in
2806: $\cal M$\/, i.e.,
2807: $t_1^{\cal M}=t_2^{\cal M}$\/.
2808:
2809: \item We need to prove that:
2810: \begin{enumerate}
2811: \item for all $f\in {\cal F}_\bag$
2812: and for all terms $t_1,\dots,t_n \in T({\cal F}_\bag)$
2813: it holds that
2814: $$h(f^{{\cal MSET}}(\rapprmedio{t_1},\dots,\rapprmedio{t_n})) = f^{\cal
2815: M}(h(t_1),\dots,h(t_n))$$ Now,
2816: $$\begin{array}{rcll}
2817: h(f^{{\cal MSET}}(\rapprmedio{t_1},\dots,\rapprmedio{t_n})) & = &
2818: h(f(t_1,\dots,t_n)) & \mbox{By fact (1) above}\\
2819: &=& (f(t_1,\dots,t_n))^{\cal M} & \mbox{By def. of
2820: $h$}\\
2821: &=& f^{{\cal M}}(t_1^{\cal
2822: M},\dots,t_n^{\cal M}) & \mbox{By def.
2823: of structure} \\
2824: &=& f^{{\cal M}}
2825: (h(t_1),\dots,h(t_n))& \mbox{By def. of $h$}
2826: \end{array}$$
2827: \item for all terms $t$ and $s$,
2828: if $\rappr{t}\in^{{\cal MSET}}\rappr{s}$\/, then
2829: $h(\rappr{t})\in^{\cal M}h(\rappr{s})$. From $\rappr{t}\in^{{\cal
2830: MSET}}\rappr{s}$, using fact 1. above, we have that there is a
2831: term $s'$ in $\rappr{s}$ of the form $\mo t\:|\:r\mc$ and that
2832: $h(\rappr{s})=s'^{\cal M}$\/. Hence, we have that
2833: $h(\rappr{s})=\mo t^{\cal M}\,|\,r^{\cal M}\mc^{\cal M}$\/; $(W)$
2834: ensures that $h(\rappr{t})=t^{\cal M}$ belongs to it.
2835: \end{enumerate}
2836:
2837: \item We prove, by structural induction on $t_1$,
2838: that if $h(\rapprmedio{t_1})=h(\rapprmedio{t_2})$\/, then
2839: $\rapprmedio{t_1}=\rapprmedio{t_2}$\/.
2840:
2841: \Base Let $t_1$ be a constant $c$.
2842: Since $\cal M$ is a model of axiom schema $(F_2)$\/, it can
2843: not be
2844: that $t_2 = f(s_1,\dots,s_n)$\/, with $f$ different from $c$\/.
2845: Hence, it must be that $t_2 = c$\/.
2846:
2847: \Step Let $t_1$ be $f(s_1,\dots,s_n)$\/, with $f\not\equiv
2848: \mf$\/.
2849: It cannot be $t_2\equiv g(r_1,\dots,r_m)$\/, with
2850: $g\not\equiv
2851: f$\/, since ${\cal M}$ is a model of $(F_2)$\/.
2852: So, it must be $t_2\equiv f(r_1,\dots,r_n)$\/, and, by $(F_{1})$,
2853: $s_i^{{\cal M}}= r_i^{{\cal M}}$\/, for all $i\leq n$\/.
2854: Using the inductive hypothesis
2855: we have $\rapprmedio{t_1}=\rapprmedio{t_2}$\/.
2856:
2857: Let $t_1$ be $\mo s_1,\dots, s_n \,|\, r\mc$\/, with $r$ not of
2858: the form $\mo r_1\,|\,r_2\mc$\/. Since it cannot be that
2859: $t_2$ is $f(v_1,\dots, v_n)$ (from the previous case applied to
2860: $t_2$), then it must be $t_2$ is $\mo u_1,\dots, u_m\,|\,
2861: v\mc$\/, for some $v$ not of the form $\mo v_1\,|\,v_2\mc$\/. Let
2862: us assume, by contradiction, that $\rapprmedio{t_1}\neq \rapprmedio{t_2}$\/, and
2863: $t_1^{\cal M}=t_2^{\cal M}$\/, while the thesis holds for all
2864: terms of lower complexity. From $t_1^{\cal M}=t_2^{\cal M}$ we
2865: obtain that the two terms have in $\cal M$ the same elements.
2866: Since $\cal M$ is a model of $(W)$\/, the elements of $t_1^{\cal
2867: M}$ are exactly $s_1^{\cal M},\dots, s_n^{\cal M}$ and the
2868: elements of $t_2^{\cal M}$ are exactly $u_1^{\cal
2869: M},\dots,u_m^{\cal M}$\/. So, by inductive hypothesis, there is a
2870: bijection $b:\{1,\dots,n\}\longrightarrow \{1,\dots,m\}$ such
2871: that $\rapprmedio{s_i}=\rapprmediocre{u_{b(i)}}\,\,$\/. This means that $m=n$ and that there
2872: is a term $t_2'$ in $\rapprmedio{t_2}$ of the form $\mo s_1,\dots, s_m\,|\,
2873: v\mc$\/. Applying $n$ times $(E_k^m)$\/, in all possible ways, we
2874: obtain that $r^{\cal M}=v^{\cal M}$\/, hence by inductive
2875: hypothesis $\rappr{r}=\rappr{v}$\/. From this fact, we conclude that
2876: $\rapprmedio{t_2}=\rapprmedio{t_2'}=\rapprlungo{\mo s_1,\dots,s_n\,|\,r\mc}=\rapprmedio{t_1}$\/, which is in
2877: contradiction with our assumption.
2878:
2879: \item If $h(\rappr{t})\in^{\cal M}h(\rappr{s})$\/, then $t^{\cal M}\in^{\cal
2880: M}s^{\cal M}$ and hence $(K)$ implies that $s$ must be a term of
2881: the form $\mo t_1\,|\,t_2\mc$\/. By induction on $s$ using
2882: $(W)$\/, we can prove that in particular $s$ must be a term of the
2883: form $\mo t_1,\dots, t_i,\dots ,t_n\,|\,r\mc$\/, with $t_1^{\cal
2884: M}=t^{\cal M}=h(\rappr{t})$\/. We have already proved that $h$ is
2885: injective, hence it must be $t_1\in\rappr{t}$\/, and from this we
2886: obtain $\rappr{t}\in^{\cal MSET}\rappr{s}$\/.
2887: \end{enumerate}
2888: \end{proof}
2889:
2890:
2891: %\noindent {\bf Lemma \ref{convergente}.}~
2892: \begin{lemma}\label{convergente}
2893: If $C$ is a constraint in pre-solved form and acyclic,
2894: then $\sigma_C$ is
2895: stabilizing.
2896: \end{lemma}
2897: %\par\smallskip\par\noindent
2898: \begin{proof}
2899: We prove that $\sigma_C^*\equiv \sigma_C^{q-1}$\/, where $q$ is
2900: the number of variables which occur in the right-hand side of
2901: membership atoms.
2902:
2903: The acyclicity condition ensures that there are no loops in the
2904: graph ${\cal G}_{C}^{\in}$\/. Consider now the substitution
2905: $\sigma_C$ and let $B$ be the set of the nodes of the graph that
2906: belong to its domain (we identify variables and corresponding
2907: nodes). Each application of $\sigma_C$ on the terms of its
2908: codomain can be intuitively mimicked by a game that updates the
2909: value of $B$ with the nodes corresponding to the variables
2910: occurring in the terms $\sigma_C(B)$. These nodes can be computed
2911: by collecting the nodes that can be reached by crossing an edge
2912: from a node of $B$ (new variables $F_i,M_i$ are all different, and
2913: they are not in the domain of $\sigma_C$, so we can forget them).
2914: The process will terminate when either $B$ is empty or it contains
2915: only variables that are not in the domain of $\sigma_C$. Since
2916: ${\cal G}_{C}^{\in}$ is acyclic, this process must terminate, and
2917: since the longest path in the graph is shorter than $q$, it is
2918: plain o see that $q-1$ is an upper bound to the number of
2919: iterations.
2920: \end{proof}
2921:
2922:
2923:
2924: %\noindent {\bf Lemma \ref{listisolved}.}~
2925: \begin{lemma}\label{listisolved}
2926: Let $\Th$ be one of the theories \lst, \bag, \clist, ${\cal
2927: A}_{\Th}$ the model (structure) which corresponds with $\Th$\/, and
2928: $E_\Th$ the associated equational theory. Let $t, t'$ be two
2929: terms and $C$ a solved form constraint over the language ${\cal
2930: L}_\Th$, such that $FV(t)\cup FV(t')\subseteq FV(C)$. If ${\cal
2931: A}_{\Th} \not\models{\forall}(t=t')$, then
2932: $E_\Th\not\models{\forall}(\sigma_C^*(t)=\sigma_C^*(t'))$\/.
2933: \end{lemma}
2934: %\par\medskip\par\noindent
2935: \begin{proof}
2936: Let $R=\{X_1,\dots,X_n\}$ be the set of variables over which
2937: $\sigma_C$ is defined.
2938: By induction on the sum of the complexities of $t$ and $t'$ we prove
2939: the following property that
2940: implies the thesis of the lemma.
2941: \begin{quote}
2942: {\it
2943: If there exists $\theta$ such that ${\cal A}_{\Th}\models \theta(t)\neq
2944: \theta(t')$, then there exists $\theta'$ such that ${\cal A}_{\Th}\models
2945: \theta'(\sigma_C^*(t)) \neq \theta'(\sigma_C^*(t'))$.}
2946: \end{quote}
2947:
2948: Let us consider the valuation $\theta''$ defined as:
2949: $$\theta''(Y)=\left\{\begin{array}{ll}\theta(Y) & \mbox{if }Y\not\in R\\
2950: \theta(X_i) & \mbox{if }Y\equiv M_{X_i}
2951: \end{array}\right .$$
2952: Observe that $\theta''$ is not defined over the variables $F_{X_1},\dots,
2953: F_{X_n}$.
2954:
2955: Let $m=\max\{size(\theta''(\sigma_C^*(t))),
2956: size(\theta''(\sigma_C^*(t')))\}+1$. We can now define the
2957: valuation $\theta'$ in the following way:
2958: $$\theta'(Y)=
2959: \left\{
2960: \begin{array}{ll}
2961: {[} \nil ]^{m*i} ({\mo} \nil \mc^{m*i}, {\clo} \nil \clc^{m*i}) &
2962: \mbox{if }Y\equiv F_{X_i}\\
2963: \theta''(Y) & \mbox{otherwise }
2964: \end{array}\right .$$
2965: \noindent If $t = Y_1$ and $t'= Y_2$ are variables then:
2966: \begin{itemize}
2967: \item if $\sigma_C$ is not defined neither on $Y_1$ nor on $Y_2$, then
2968: $\theta'(\sigma_C^*(Y_1))=\theta'(Y_1)=\theta(Y_1)\neq
2969: \theta(Y_2)=\theta'(Y_2)=\theta'(\sigma_C^*(Y_2))$;
2970: \item if $\sigma_C$ is defined on $Y_1$ and not on $Y_2$ (or
2971: viceversa), then $\size(\theta'(\sigma_C^*(Y_1)))\geq \size(\theta'(F_{Y_1}))>
2972: size(\theta'(Y_2))$;
2973: \item if $\sigma_C$ is defined both on $Y_1$ and on $Y_2$, then:
2974: \begin{description}
2975: \item[\lst\ {\rm and} \clist:]
2976: $\theta'(\sigma_C^*(Y_1))$
2977: and $\theta'(\sigma_C^*(Y_2))$ differ on their first element.
2978: \item[\bag:]
2979: $\theta'(\sigma_C^*(Y_1))$
2980: and $\theta'(\sigma_C^*(Y_2))$ differ on their elements $\theta'(F_{Y_1})$
2981: and $\theta'(F_{Y_2})$.
2982: \end{description}
2983: \end{itemize}
2984:
2985: \noindent If $t = Y$ is a variable and $t'$ is $f(t_1',\dots, t_h')$,
2986: also when $f$ is of the form $\lf,\lcf,\mf$, then:
2987: \begin{itemize}
2988: \item if $\sigma_C$ is not defined on $FV(t')\cup Y$, then we have
2989: immediately the thesis since $\theta'(\sigma_C^*(Y))=\theta(Y)$
2990: and $\theta'(\sigma_C^*(t'))=\theta(t')$;
2991: \item if $\sigma_C$ is defined on $Y$, but not on $FV(t')$, then
2992: we have the thesis since
2993: $size(\theta'(\sigma_C^*(Y)))>size(\theta(t'))$;
2994: \item if $\sigma_C$ is defined on at least one variable of $t'$
2995: and not on $Y$, then as in the previous case we have the thesis;
2996: \item if $\sigma_C$ is defined on $Y$ and on at least one of the
2997: variables of $t'$, then:
2998: \begin{description}
2999: \item[$\lst$ {\rm and} $\clist$:] it can never be the case that the first
3000: element of $\theta'(\sigma_C^*(Y))$---i.e. $\theta'(F_Y)$---is
3001: equal to the first element of $\theta'(\sigma_C^*(t'))$\/; this
3002: follows from the conditions we have imposed on all the
3003: $\theta'(F_{X_i})$.
3004: \item[$\bag$:] two cases are possible:
3005: $\theta'(F_Y)$ is not an element of $\theta'(\sigma_C^*(t'))$,
3006: from which we have the thesis. \\
3007: $\theta'(F_Y)$ is an element of $\theta'(\sigma_C^*(t'))$:
3008: this means that ${\sf tail}(t')=Y$, hence the thesis follows.
3009: \end{description}
3010: \end{itemize}
3011:
3012: \noindent If $t$ is $f(t_1,\dots,t_h)$ and $t'= g(t_1',\dots,t_k')$,
3013: with $f$ different from $g$, then it is trivial.
3014:
3015: \noindent If $t$ is $f(t_1,\dots,t_h)$ and $t'$ is $f(t_1',\dots,t_h')$,
3016: with $f$ different from $ \lf,\lcf,\mf$, then by inductive hypothesis we have the
3017: thesis.
3018:
3019: \noindent If $t$ is $[ t_1\,|\,t_2]$ and
3020: $t'$ is $[t_1'\,|\,t_2']$, then from ${\cal LIST}\models\theta(t)\neq
3021: \theta(t')$ we have that it must be ${\cal LIST}\models\theta(t_1)\neq
3022: \theta(t_1')$ or ${\cal LIST}\models\theta(t_2)\neq
3023: \theta(t_2')$, hence, in both cases, we obtain the thesis by inductive
3024: hypothesis.
3025:
3026: \noindent If $t$ is $\clo t_1\,|\,t_2\clc$ and $t'$ is
3027: $\clo t_1'\,|\,t_2'\clc$, then from ${\cal CLIST}\models\theta(t)\neq
3028: \theta(t')$ we have that it must be ${\cal CLIST}\models\theta(t_1)\neq
3029: \theta(t_1')$ or ${\cal CLIST}\models\theta(t_2)\neq
3030: \theta(t_2')\wedge \theta(t_2)\neq
3031: \clo\theta(t_1')\,|\,\theta(t_2')\clc\wedge \theta(t_2')\neq
3032: \clo\theta(t_1)\,|\,\theta(t_2)\clc$, hence:
3033: \begin{itemize}
3034: \item in the first case we obtain the thesis by inductive
3035: hypothesis on $t_1$ and $t_1'$.
3036: \item in the second case by inductive hypothesis on $t_2$ and
3037: $t_2'$, on $t_2$ and $\clo t_1'\,|\,t_2'\clc$, on $t_2'$ and $\clo
3038: t_1\,|\,t_2\clc$, we obtain that ${\cal CLIST}\models \theta'(\sigma_C^*(t_2))
3039: \neq \theta'(\sigma_C^*(t_2'))$ and ${\cal CLIST}\models
3040: \theta'(\sigma_C^*(t_2))
3041: \neq \theta'(\sigma_C^*(\clo t_1'\,|\,t_2'\clc))$ and ${\cal CLIST}\models
3042: \theta'(\sigma_C^*(t_2'))
3043: \neq \theta'(\sigma_C^*(\clo t_1\,|\,t_2\clc))$, which implies our
3044: thesis.
3045: \end{itemize}
3046:
3047: \noindent If $t$ is $\mo t_1\,|\,t_2\mc$ and $t'$ is
3048: $\mo t_1'\,|\,t_2'\mc$, then:
3049: \begin{itemize}
3050: \item if ${\sf tail}(t_2)$ and ${\sf tail}(t_2')$ are the same
3051: variable, the we obtain the thesis by inductive hypothesis on
3052: ${\sf untail}(\mo
3053: t_1\,|\,t_2\mc)$ and ${\sf untail}(\mo t_1'\,|\,t_2'\mc)$;
3054: \item if ${\sf tail}(t_2)=Y$ and ${\sf tail}(t_2')=Y'$ are not the
3055: same variable and $\sigma_C$ is not defined on $Y$ or on $Y'$,
3056: then $\theta'(F_Y)$ or $\theta'(F_{Y'}$ is not an element of both
3057: $\theta'(\sigma_C^*(t))$ and $\theta'(\sigma_C^*(t'))$;
3058:
3059: \item if ${\sf tail}(t_2)=Y$ and ${\sf tail}(t_2')=Y'$ are not the
3060: same variable and $\sigma_C$ is not defined on $Y$ and on $Y'$,
3061: then we can restrict ourselves to the case in which there is an
3062: element $s$ of $\theta(t)$ which is not an element of
3063: $\theta(t')$ (in the general case we would have to consider that
3064: there exists $s$ such that there are $m$
3065: occurrences of $s$ in $\theta(t)$ and $n$ occurrences in
3066: $\theta(t')$ with $m\neq n$):
3067: \begin{itemize}
3068: \item if $s$ is an element of $\theta(Y)$, then, from the fact that
3069: $\sigma_C$ is not defined on $Y$, we have the thesis, since it cannot be
3070: the case that one of the elements of ${\sf untail}(t')$ becomes equal to
3071: $\theta(s)$ (the new elements have a size which is greater);
3072: \item if $s$ is an element of ${\sf
3073: untail}(t)$, then we have $t = \mo u_1,\dots,
3074: u_h,\dots,u_m\,|\,Y\mc$ and $s = \theta(u_h)$, hence, from the
3075: inductive hypothesis, we have that $\theta'(\sigma_C^*(u_h))$ is
3076: still different from all elements of $\theta'(\sigma_C^*({\sf
3077: untail}(t')))$, and it is immediate that it is different from all
3078: the elements of $\theta'(Y')$, hence $\theta'(\sigma_C^*(u_h))$ is
3079: an element of $\theta'(\sigma_C^*(t))$ which is not in
3080: $\theta'(\sigma_C^*(t'))$.
3081: \end{itemize}
3082: \end{itemize}
3083: \end{proof}
3084:
3085: \begin{lemma}\label{uffa}
3086: Let $\Th$ be one of the theories \lst, \clist, \bag\ and \set,
3087: and $C$ a constraint in pre-solved form over the language of
3088: $\Th$. If ${\sf is\_solved_\Th(C)}$ returns $\false$, then $C$ is
3089: not satisfiable in the model ${\cal A}_{\Th}$
3090: which corresponds with $\Th$.
3091: \end{lemma}
3092: \begin{proof}
3093: If ${\sf is\_solved_\Th(C)}$ returns $\false$ because ${\cal
3094: G}_{C}^{\in}$ has a cycle then the result is trivial, since all
3095: aggregates in $\cal A$ are well-founded. Otherwise:
3096: \begin{description}
3097: \item[{\rm For} \lst, \bag, \clist: ] From Lemma \ref{listisolved} we know
3098: that $\Th\models\forall(\sigma_C^*(t)=\sigma_C^*(t'))$
3099: implies ${\Th}\models \forall(t=t')$, hence, since $t\in
3100: X$ and $t'\not\in X$ are in $C$, $C$ is not satisfiable in the
3101: model $\cal A$ which corresponds with $\Th$.
3102: \item[{\rm For} \set: ] Let
3103: $\sigma_C^*\equiv [X_1/\{ F_1, p_1^1,\dots, p_1^{k_1}\,|\,M_1\},\dots,
3104: X_q/\{F_q,p_q^{1},\dots,p_q^{k_q}\,|\,M_q\}]$, we have that
3105: if ${\cal SET}\models C\gamma$, then ${\cal SET}\models
3106: (C\sigma_C^*)\gamma'$, where $\gamma'$ is defined as follows
3107: $$\gamma'(Y)=\left\{\begin{array}{ll}
3108: \gamma(X_i) & \mbox{ if } Y\equiv M_i\\
3109: p_i^1 & \mbox{ if } Y\equiv F_i\\
3110: \gamma(Y) & \mbox{ otherwise}
3111: \end{array}\right. $$
3112: Hence, if ${\sf is\_solved_\set}$ returns $\false$ this means that
3113: $C\sigma_C^*$ is not satisfiable in $\cal SET$, which implies
3114: that $C$ is not satisfiable in ${\cal SET}$.
3115: \end{description}
3116: \end{proof}
3117:
3118: \section{Termination Proofs (Theorem \ref{termina-lists})} \label{termination}
3119:
3120:
3121: \subsection*{Termination of ${\sf SAT}_{\lst}$}
3122: Using the same measure as for ${\sf SAT}_{\bag}$ termination follows.\qed
3123:
3124:
3125: \subsection*{Termination of ${\sf SAT}_{\clist}$}
3126: Finding a global decreasing
3127: measure implies that this measure is decreased by each rule of each
3128: algorithm involved. The measure developed in~\cite{DPR98-fuin} for proving
3129: termination of {\sf Unify\_clists} is rather complex. This is due to the
3130: fact that new variables are (apparently) freely introduced in the
3131: constraint by this procedure. Instead of extending such complex measure to
3132: the general case, we use here a different approach for proving termination.
3133: The proof is based:
3134: \begin{itemize}
3135: \item on the fact that each single rewriting procedure
3136: terminates
3137: (for {\sf Unify\_clists} it follows from~\cite{DPR98-fuin};
3138: for the other three procedures the result is trivial) and
3139: \item on the fact that it is possible to find a bound on
3140: the number of possible {\sf repeat} cycles.
3141: \end{itemize}
3142:
3143: The remaining part of the proof is devoted to find this
3144: bound.
3145: First of all observe that:
3146: \begin{itemize}
3147: \item After the execution of {\sf in-CList} there are only
3148: membership atoms of the form $t \in X$ with $X \notin
3149: \vars(t)$\/. New equations can be introduced.
3150: \item After the execution of {\sf in-CList} there are only
3151: not-membership literals of the form $t \notin X$ with $X \notin
3152: \vars(t)$\/. New disequality constraints can be introduced. Membership atoms
3153: are not introduced.
3154: \item After the execution of {\sf neq-CList} there are
3155: only disequality constraints of the form $X \neq t$ with $X \notin
3156: \vars(t)$\/. New equations can be introduced. $\in$ and
3157: $\notin$-constraints are not introduced.
3158: \item {\sf Unify\_clists} eliminates all equality
3159: constraints producing a substitution. This substitution, when
3160: applied to membership, not-membership, and disequality literals in
3161: pre-solved form can force a new execution of the procedures {\sf
3162: in-CList}, {\sf nin-CList}, and {\sf neq-CList}. However, new
3163: executions of {\sf Unify\_clists} are possible only if {\sf
3164: in-CList} and {\sf neq-CList} introduce new equations. In the
3165: following we will find a bound on the number of possible new
3166: equations inserted.
3167: \end{itemize}
3168:
3169: Let us analyze membership constraints. Each membership atom of
3170: the form $t \in \clo s' \,|\, s'' \clc$ is rewritten to \false\
3171: or to $t = s' \vee t \in s''$\/. This means that in each
3172: non-deterministic branch of the rewriting process \emph{at most}
3173: one equation is introduced for each initial membership atom. Thus,
3174: if $k$ is the number of membership atoms in $C$ at the beginning
3175: of the computation, at most $k$ equality atoms (that can fire
3176: {\sf Unify\_clists}) can be introduced. If we prove termination
3177: with $k = 0$ then full termination easily follows, since it is the
3178: same as considering $k$ successive (terminating) executions.
3179:
3180: Let us consider the procedure {\sf neq-CList}. Action $(7.2)$ can
3181: replace a disequality constraint of the form: $X \neq \clo
3182: t_1,\dots,t_n \,|\, X \clc$ with the following equations,
3183: identifying a substitution:
3184: \begin{eqnarray}
3185: \label{Xnil} X & = & \nil\\
3186: \label{Xcli}
3187: X & = & \clo N_1\,|\,N_2 \clc\,\mbox{ with $N_1,N_2$ new
3188: variables.}
3189: \end{eqnarray}
3190:
3191: Let us analyze the various cases in which substitutions of
3192: this form have
3193: some effects on the constraint.
3194: \begin{itemize}
3195: \item there is $t \in X$ in $C$\/. This is not possible by
3196: hypothesis,
3197: since $k=0$\/.
3198: \item $t \notin X$ or $X \neq t$ and we know that $X$ does not
3199: occur in $t$\/. This implies a finite number of executions
3200: of rules of
3201: {\sf nin-CList} or {\sf neq-CList}. Since $X$ is not in $t$ and
3202: the variables $N_1$ and $N_2$ are newly introduced, it is impossible
3203: to generate a situation firing rule $(7.2)$\/.
3204: \item Assume there are more than one equation introduced for
3205: the same variable $X$\/.
3206: \begin{itemize}
3207: \item If they are all of the form (\ref{Xnil}), then
3208: {\sf Unify\_clists} will apply the substitution and
3209: remove the redundant equations.
3210:
3211: \item If they are all of the form (\ref{Xcli}), then
3212: {\sf Unify\_clists} will perform a unification process between
3213: these new equations. The particular form of the equations allows us
3214: to see that the effect is to introduce new equations of the form
3215: $N_1 = N'_1$ between all the new variables used as elements
3216: and equations of the form $N_2 = N'_2$ or
3217: $N_2 = \clo N'_1 \,|\, N'_2 \clc$ between the new
3218: variables used as rests.
3219: The situation is similar to that in which a unique
3220: substitution is computed.
3221:
3222: \item If there are both equations of the form
3223: (\ref{Xnil}) and of the form (\ref{Xcli}), then
3224: a failing (thus, terminating) situation will be detected by
3225: {\sf Unify\_clists}.\qed
3226:
3227: \end{itemize}
3228: \end{itemize}
3229:
3230:
3231: \subsection*{Termination of ${\sf SAT}_{\set}$}
3232:
3233: Finding a global decreasing measure
3234: implies that this measure is decreased by each rule of each algorithm
3235: involved. This is rather complex since it must subsume the measure
3236: developed in~\cite{DPR98-fuin} for proving termination of {\sf
3237: Unify\_sets}. Thus, instead of extending such complex measure, we use here
3238: a different approach for proving termination. The proof is based:
3239: \begin{itemize}
3240: \item on the fact that each single rewriting procedure
3241: terminates
3242: (for {\sf Unify\_sets} it follows from~\cite{DPR98-fuin};
3243: for the other three procedures the result is trivial) and
3244: \item on the fact that it is possible to control the number
3245: of new
3246: calls to unification.
3247: \end{itemize}
3248: In order to simplify the proof we assume a strategy for handling the
3249: non-determinism. The strategy will be pointed out during the discussion.
3250:
3251: As observed in the proof of ${\sf SAT}_{\clist}$\/, if $k$ is the
3252: number of membership atoms in $C$ at the beginning of the
3253: computation, at most $k$ equality atoms (that can fire {\sf
3254: Unify\_sets}) can be introduced. For this reason, we can safely
3255: forget this kind of constraints from the whole reasoning.
3256:
3257: The only problem for termination is given by rules $(6a)$ and
3258: $(6b)$ of {\sf neq-CList}. As a strategy, we can unfold the
3259: application of this rules (actually, adding a bit of determinism
3260: to the whole procedure). This means that rule $(6a)$ (for $(6b)$
3261: the situation is symmetrical) is as follows:
3262: assume that $\{ t_1 \,|\, s_1 \}$ is $\{
3263: v_1,\dots,v_m\,|\,h\}$ and
3264: $\{ t_2 \,|\, s_2 \}$ is $\{w_1,\dots,w_n\,|\,k\}$\/,
3265: with $h,k$
3266: variables or terms of the form $f(\dots),g(\dots)$\/, $f$
3267: and $g$
3268: different from $\sef$\/.
3269: The global effect of the subcomputation is that of
3270: returning a
3271: constraint of the form ($1 \leq i \leq m$):
3272: \begin{eqnarray}
3273: \label{primoset}
3274: N = v_i, v_i \neq w_1, \dots, v_i \neq w_n, v_i \notin k
3275: \end{eqnarray}
3276: or one constraint of the form
3277: \begin{eqnarray}
3278: \label{secondoset}
3279: h = \{ N \,|\, N'\}, N \neq w_1,\dots,N \neq w_n, N
3280: \notin k
3281: \end{eqnarray}
3282: if $h$ is a variable. Notice that the application of this
3283: substitution is a sort of application of rule $(4)$ of the
3284: procedure {\sf in-Set}.
3285:
3286: In the following discussion let us assume that termination by
3287: failure do not occur (but, in this case, termination follows
3288: trivially). Suppose to have already executed the first cycle of
3289: the {\sf repeat} loop. Local termination ensures that this can be
3290: done in finite time. In the constraint there are no equations,
3291: while there can be negated membership and disequality literals not
3292: necessarily in pre-solved form.
3293:
3294: Let us execute procedure {\sf nin-Set}. No equations are
3295: introduced. In the constraint there are not-membership literals in
3296: pre-solved form and disequality constraints not necessarily in pre-solved
3297: form.
3298:
3299: Let us execute the procedure {\sf neq-Set}.
3300: We adopt a weak strategy to face the
3301: non-determinism:
3302: delay the constraints that fire action $(6)$ as much as
3303: possible.
3304: This means that after a finite time the constraint is
3305: composed
3306: by a number of constraints of the form $X \neq t$ or
3307: $t \notin X$ with $X\notin \vars(t)$ plus a (possibly empty)
3308: constraint $\tilde C$ of constraints all firing action $(6)$
3309: of
3310: {\sf neq-Set}. Pick one constraint $c$ from $\tilde C$
3311: and consider the possible non-deterministic executions.
3312:
3313: \begin{itemize}
3314: \item Assume that the situation of
3315: case (\ref{secondoset}) above does not occur in a
3316: non-deterministic branch. Then (see case (\ref{primoset}))
3317: the constraint $c$ is replaced in $ C$ by
3318: a number of constraints $v_i \neq w_j$ of fewer size. If
3319: they do not fire
3320: action $(6)$ they can be directly
3321: processed to reach a pre-solved form.
3322: Otherwise, they are inserted in $\tilde C$\/, but since
3323: they are of fewer size, if the situation of
3324: case (\ref{secondoset}) never occur, this again implies
3325: termination.
3326: \item Assume now that the situation of
3327: case (\ref{secondoset}) occurs when processing
3328: the constraint $c$\/. Constraints
3329: $$N \neq w_1,\dots,N \neq w_n, N \notin k$$
3330: are introduced. Constraints in pre-solved form
3331: of the form above, with $N$ a variable introduced as element
3332: of a set by action $(6)$\/, are said \emph{passive constraints}.
3333: Variables $N$ of this form are inserted in the constraint
3334: only by this step. We will see that passive disequality constraints
3335: remain in pre-solved form forever while negated membership
3336: passive literals have a controlled growth.
3337:
3338: Assume to apply immediately the
3339: substitution $h / \{ N \,|\, N' \}$\/. Its effect can be
3340: the following, according to the position of $h$ in a
3341: constraint:
3342: \begin{itemize}
3343: \item $X \neq t[h]$ or $t[h] \notin X$\/: the terms gets
3344: changed
3345: but the constraints remain in pre-solved form.
3346: \item $s[h] \neq t $ or $s \neq t[h]$
3347: or $s[h] \neq t[h]$\/: the terms change
3348: but the constraints remain in $\tilde C$ to be
3349: processed
3350: later.
3351: \item $t \notin h$ is transformed to
3352: $t \notin \{ N \,|\, N' \}$\/.
3353: One step of {\sf nin-Set} is applied to obtain:
3354: $t \neq N \wedge t \notin N'$\/.
3355: The first constraint is immediately transformed into
3356: $N \neq t$ (a passive constraint) while the second is in
3357: pre-solved form. Observe that if $t \notin h$ is
3358: passive (i.e., $t$ is a variable of type $N$\/), then only
3359: passive constraints are introduced.
3360:
3361: \item $h \neq t$ is transformed to $\{ N \,|\, N' \} \neq
3362: t$\/. Observe that $h \neq t$ can not be a passive constraint
3363: since $h$ is a `rest' variable while the variables
3364: of passive constraints are `element' variables, like $N$ here.
3365: A constraint in pre-solved form is no longer in pre-solved
3366: form. Let us apply the rewriting rules to it.
3367: It is immediately rewritten to \true\ (e.g., when $t$ is
3368: $f(\cdots)$\/, $f \neq \sef$\/) or it becomes in pre-solved form
3369: (when $t$ is a variable) or action (6) can be applied.
3370:
3371: Both in cases (\ref{primoset}) and in the case
3372: (\ref{secondoset})
3373: we introduce a number of passive constraints and, in the
3374: last case, a substitution $N' / \{ N_1 \,|\, N_1' \}$
3375: is applied. Notice that the global effect on the system it
3376: the fact that in the other constraints the original variable
3377: $h$ is replaced by $\{N,N_1\,|\,N'_1\}$\/.
3378: This means that this situation can be performed at most once
3379: per each occurrence of $h$\/. And, the reasoning starting
3380: from substitutions of the form
3381: $\{N,N_1,\dots,N_{\ell}\,|\,N'_{\ell}\}$
3382: is the same as that done here for $N' / \{ N_1 \,|\,N_1' \}$\/.
3383: At the end of the process,
3384: the number of constraints in $\tilde C$ is decreased and
3385: we have only introduced pre-solved form and passive constraints.\qed
3386: \end{itemize}
3387: \end{itemize}
3388:
3389:
3390:
3391: \end{document}
3392: