1: \documentclass{tlp}
2: \usepackage{graphicx}
3: \usepackage{rotating}
4:
5: \usepackage{aopmath}
6: \usepackage{amssymb}
7: \usepackage{proof}
8: \usepackage{euscript}
9: \usepackage{amsfonts}
10: \usepackage{latexsym}
11: \usepackage{epic,eepic}
12:
13:
14: %\setlength{\textwidth}{16.8truecm} %original is 12.2
15: %\setlength{\textheight}{22.5truecm} %original is 19.3
16: %\setlength{\oddsidemargin}{-0,6truecm}
17: %\setlength{\evensidemargin}{-0.61truecm}
18: %\setlength{\topmargin}{-1truecm}
19: \newtheorem{definition}{Definition}[section]
20:
21: \renewcommand{\theenumi}{\mbox {\rm ${\roman{enumi}}$}}
22:
23: % \newtheorem {proposition}[definition]{Proposition}
24: % \newtheorem {lemma}[definition]{Lemma}
25: % \newtheorem {theorem}[definition]{Theorem}
26: % \newtheorem {corollary}[definition]{Corollary}
27:
28: \newtheorem {remark}[definition]{Remark}
29:
30: % \newenvironment{proof}
31: % {\begin{trivlist}\item[]{\bf Proof\ }}
32: % {\hspace*{\fill}{$\Box$}\end{trivlist}}
33:
34: \newtheorem {es}[definition]{Example}
35: \newenvironment {example} {\begin{es}\rm}{\hspace*{\fill}$\Box$\end{es}}
36: \newcommand {\comment}[1]{}
37: \newcommand {\Line} {{\bf -----------------------------------------------------------------------------------------}}
38: \newcommand {\Lline} {{\bf ------------------------------------------------------------------------------------------------------}}
39: \newenvironment {summary} {\begin{quote}\Line\nl
40: [\medskipamount] {\bf Summary of the Chapter.}\small\sl}
41: {\vspace{0.2cm}\nl \normalsize \Line\end{quote}}
42:
43:
44: %%%%%%%% macro %%%%%%%
45:
46: \input{macro}
47:
48: %%%%%%% fine macro %%%%%%%
49:
50:
51: \title[Model Checking Linear Logic Specifications]
52: {Model Checking Linear Logic Specifications}
53: \author[M. Bozzano, G. Delzanno and M. Martelli]
54: {MARCO BOZZANO${\mbox {}^{1,2}}$, GIORGIO DELZANNO${\mbox {}^{2}}$ and MAURIZIO
55: MARTELLI${\mbox {}^{2}}$\\
56: \begin{tabular}{c}
57: \begin{tabular}{c}
58: \\
59: ${\mbox {}^{1}}$ITC-IRST\\
60: Via Sommarive 18, Povo, 38050 Trento, Italy\\
61: \email{bozzano@irst.itc.it}
62: \end{tabular}
63: \bigskip\\
64: \begin{tabular}{c}
65: ${\mbox {}^{2}}$Dipartimento di Informatica e Scienze dell'Informazione\\
66: Universit\`a di Genova\\
67: Via Dodecaneso 35, 16146 Genova - Italy \\
68: \email{\{giorgio,martelli\}@disi.unige.it}
69: \end{tabular}
70: \end{tabular}
71: }
72:
73: \pagerange{\pageref{firstpage}--\pageref{lastpage}}
74:
75: \volume{}
76: \jdate{}
77: \setcounter{page}{1}
78: \pubyear{}
79:
80: \begin{document}
81:
82: \label{firstpage}
83:
84: \maketitle
85:
86: \begin{abstract}
87: The overall goal of this paper is to investigate the theoretical
88: foundations of {\em algorithmic} verification techniques for
89: {\em first order linear logic} specifications.
90: The fragment of linear logic we consider in this paper is based on the linear
91: logic programming language called LO \cite{AP90} enriched with {\em universally
92: quantified goal formulas}. Although LO was originally introduced
93: as a theoretical foundation for extensions of {\em logic
94: programming} languages, it can also be viewed as a very general
95: language to specify a wide range of {\em infinite-state concurrent systems}
96: \cite{And92,Cer95}.
97:
98: Our approach is based on the relation between {\em backward
99: reachability} and {\em provability} highlighted in our previous
100: work on {\em propositional} LO programs \cite{BDM02a}. Following this
101: line of research, we define here a general framework for the {\em
102: bottom-up} evaluation of {\em first order} linear logic specifications.
103: The evaluation procedure is based on an effective fixpoint
104: operator working on a symbolic representation of infinite
105: collections of first order linear logic formulas. The theory of
106: well quasi-orderings \cite{ACJT96,FS01} can be used to provide sufficient conditions
107: for the termination of the evaluation of non trivial fragments of
108: first order linear logic.
109: \end{abstract}
110:
111: \begin{keywords}
112: Linear logic, fixpoint semantics, bottom-up evaluation
113: \end{keywords}
114:
115: \section{Introduction}
116: \label{introsec}
117:
118: The algorithmic techniques for the analysis of Petri Nets are based on
119: very well consolidated theoretical foundations
120: \cite{EM00,KM69,May84,EFM99,Fin93,STC98}. However, several interesting
121: problems, e.g., the {\em coverability} problem,
122: become undecidable when considering
123: specification languages more expressive than basic Petri Nets. In
124: this setting, {\em validation} of complex specifications is often
125: performed through {\em simulation} and {\em testing}, i.e., by
126: ``executing'' the specification looking for design errors, e.g., as in
127: the methodology based on the construction of the reachability graph of
128: Colored Petri Nets \cite{Jen97}. In order to study algorithmic
129: techniques for the analysis of a vast range of concurrency models it
130: is important to find a uniform framework to reason about their
131: characteristic features.
132:
133: In our approach we will adopt {\em linear logic} \cite{Gir87}
134: as a unified logical framework for concurrency.
135: Linear logic provides a logical characterization of concepts and
136: mechanisms peculiar of concurrency like {\em locality}, {\em recursion}, and
137: {\em non determinism} in the definition of a process \cite{AP90,KY95,MM91};
138: communication via {\em synchronization} and {\em value passing} \cite{Cer95,Mil93};
139: {\em internal state and updates to its current value} \cite{AP90,Mil96};
140: and {\em generation of fresh names} \cite{CDLMS99,Mil93}.
141: {\em Provability} in fragments of linear logic can be used as a
142: formal tool to reason about behavioral aspects of the {\em concurrent systems}
143: \cite{BDM02a,MMP96}.
144:
145: The overall goal of this paper is to investigate the theoretical
146: foundations of {\em algorithmic} verification techniques for specifications
147: based on {\em first order linear logic}.
148: The fragment we consider in this paper is based on the linear
149: logic programming language called LO \cite{AP90} enriched with
150: {\em universally quantified goal formulas}. Apart from being a logic programming
151: language, the appealing feature of LO is that it can also be viewed as a
152: rich {\em specification} language for concurrent systems:
153: \begin{itemize}
154: \item Specification languages like Petri Nets and multiset
155: rewriting over first order atomic formulas
156: can be naturally embedded into {\em propositional LO}
157: (see, e.g., \cite{Cer95,BDM02a}).
158: \item {\em First order LO specifications} can be used to specify the internal state
159: of processes with structured data represented as terms, thus
160: enlarging the class of systems that can be formally specified in
161: the logic. In this context universal quantification in goal
162: formulas has several interesting interpretations: it can be viewed
163: either as a sort of {\em hiding} operator in the style of
164: $\pi$-calculus \cite{Mil93}, or as a mechanism to generate {\em
165: fresh names} as in \cite{CDLMS99}.
166: \end{itemize}
167: %
168: Before discussing in more details the technical contributions of our
169: work, we will briefly illustrate the connection
170: between Petri Nets and linear logic, and between reachability and
171: provability in the corresponding formal settings. The bridge between
172: the two paradigms is the {\em proofs as computations} interpretation
173: of linear logic proposed in \cite{And92} and in \cite{Mil96}.
174: %
175: \paragraph{Linear Logic and Concurrency}
176: %
177: A Petri Net can be represented by means of a multiset-rewriting
178: system over a finite alphabet, say $p,q,r,\ldots$, of {\em place} names.
179: One possible way of expressing multiset rewrite rules in linear logic is based on the following
180: idea. The connective $\para$ (multiplicative disjunction) is interpreted as a
181: multiset constructor, whereas the connective $\lollo$ (reversed linear implication) is
182: interpreted as the rewrite relation.
183: Both connectives are allowed in the LO fragment.
184: For instance, as shown in \cite{Cer95} the LO clause
185: $$
186: p\para q~\lollo~p \para p \para q \para t
187: $$
188: can be viewed as a Petri Net {\em transition} that removes a token from places
189: $p$ and $q$ and puts two tokens in place $p$, one in $q$, and one in $t$.
190: According to the proofs as computations interpretation \cite{And92},
191: a {\em top-down} derivation in linear logic consists of a goal-directed sequence of rule
192: applications. If we look at the initial goal as a multiset of atomic formulas (places)
193: representing the initial marking of a Petri Net, then each application of an LO clause
194: like the one illustrated above ({\em backchaining} in the terminology of \cite{And92}) simulates
195: the firing of a Petri Net transition at the corresponding marking. Furthermore, the overall
196: top-down derivation corresponds to one of the possible executions of the net,
197: leading from the initial marking to one of the target states.
198:
199: Thanks to the presence of other connectives, LO supports more sophisticated mechanisms
200: than the ones available in simple Petri Nets.
201: For instance, in \cite{AP90} Andreoli and Pareschi use LO clauses with
202: occurrences of $\para$ and $\with$ (additive conjunction) in their {\em body}
203: to express what they called {\em external} and {\em internal} concurrency.
204: Additive conjunction can be used, in fact, to simulate independent threads of execution
205: running in parallel.
206:
207: In our previous work \cite{BDM02a}, we made a first attempt to connect
208: techniques used for the validation of Petri Nets with evaluation strategies
209: of LO programs.
210: Specifically, in \cite{BDM02a} we defined an effective procedure to compute the
211: set of linear logic {\em goals} (multisets of atomic formulas)
212: that are consequences of a given propositional program, i.e.,
213: a ``bottom-up'' evaluation procedure for {\em propositional} LO programs.
214: Our construction is based on the {\em backward reachability}
215: algorithm of \cite{ACJT96} used to decide the so called
216: {\em control state reachability problem} of Petri Nets
217: (i.e., the problem of deciding if a given set of {\em upward closed} configurations are
218: reachable from an initial one).
219: The algorithm works as follows.
220: Starting from a set of {\em target states},
221: the algorithm computes symbolically the transitive closure of
222: the {\em predecessor} relation (i.e., the transition relation read backwards)
223: of the Petri Net taken into consideration.
224: The algorithm is used to check safety properties:
225: if the algorithm is executed starting from the set of {\em unsafe states},
226: then the corresponding safety property holds if and only if the
227: initial marking is not in the resulting fixpoint.
228:
229: In order to illustrate the connection between backward reachability for
230: Petri Nets and provability in LO, we first observe that LO program clauses
231: of the form
232: $$
233: p\para q\para q~\lollo~\all
234: $$
235: succeed in any context containing {\em at least} one occurrence of $p$ and two occurrences
236: of $q$.
237: In other words they can be used to symbolically represent sets of markings
238: that are closed upwards with respect to the multiset inclusion relation.
239: Now, suppose we represent a Petri Net via an LO program $P$ and
240: the set of {\em target states} using a collection $T$ of LO program clauses with $\all$ in
241: the body.
242: Then, the set of {\em facts} (i.e., multisets of atomic formulas)
243: that are {\em logical consequences} of the LO program $P\cup T$
244: will represent the set of markings that are {\em backward reachable}
245: from the target states.
246:
247: The algorithm we presented in \cite{BDM02a} is based on this idea, and it
248: extends the backward reachability algorithm for Petri Nets of \cite{ACJT96}
249: to the more general case of propositional LO programs (i.e., with nested conjunctive
250: and disjunctive goals).
251: %
252: \paragraph{First Order Linear Logic}
253: %
254: By lifting the logic language to {\em first order},
255: the resulting specification language becomes much more interesting and flexible than
256: basic Petri Nets.
257: In the extended setting, the logic representation of processes
258: can be enriched with a notion of {\em internal state} and with communication mechanisms
259: in which {\em values} can be passed between different processes.
260: As an example, the following LO clause
261: $$
262: idle(Y)\para p(alice,wait,stored(Y))~\lollo~p(alice,use,stored(Y))
263: $$
264: can be interpreted as a transaction of a protocol during which the {\em process} named Alice
265: (currently knowing $Y$) synchronizes with a monitor controlling the resource $Y$,
266: checks that the monitor is {\em idle} and then enters the critical section in which she uses
267: the resource $Y$.
268: By instantiating the free variables occurring in such a rule, we obtain a family of transition
269: rules that depend on the domain used to define the content of messages.
270: In this setting the universal quantification in goal formulas can be used to generate
271: {\em fresh values}, as in the following rule:
272: $$
273: init \lollo~\foralx{~idle(x)~\para~init}
274: $$
275: Intuitively, the demon process $init$ creates new resources labeled with fresh
276: identifiers.
277:
278: %As in the propositional case, starting from a multiset of {\em ground}
279: %atomic formulas, the application (in a backchaining step) of {\em
280: %ground instances} of rules like the previous one can be used to
281: %simulate the execution of the protocol.
282:
283: The above illustrated connection between {\em provability} and {\em
284: reachability} immediately gives us a well-founded manner of extending
285: the algorithmic techniques used for the analysis of Petri Nets to the
286: general case of first order linear logic specifications.
287: %What we have
288: %to do is to define a general framework for the {\em bottom-up}
289: %evaluation of first order specifications.
290: %
291: \paragraph{Our Contribution}
292: The conceptual and technical contributions of our work can be summarized
293: as follows.
294: \begin{itemize}
295: \item[(1)] Combining ideas coming from the semantics of logic programming \cite{BGLM94,FLMP93}
296: and from symbolic model checking for infinite state systems \cite{ACJT96,FS01},
297: in this paper we present the theoretical foundations for the definition of a procedure
298: for the {\em bottom-up} evaluation of first order LO programs with universally quantified goals.
299: By working in the general setting of linear logic, we obtain a framework that can
300: be applied to other specification languages for concurrent systems like
301: {\em multiset rewriting over first order atomic formulas} \cite{CDLMS99}.
302:
303: The bottom-up evaluation procedure can also be viewed as a {\em fixpoint}
304: semantics that allows us to compute the set of all goals that are
305: linear logical consequences of a given (extended) LO program.
306: The fixpoint semantics is based on an {\em effective} fixpoint operator and on a
307: {\em symbolic}
308: and {\em finite} representation of an {\em infinite} collection of first order
309: provable LO goals. As previously mentioned, the possible infiniteness of the set of
310: provable goals is due to LO program clauses with the constant $\all$, which represent
311: sets of goals which
312: are upward-closed with respect to the multiset inclusion relation.
313: The symbolic representation is therefore crucial when trying to prove properties of
314: infinite systems like {\em parameterized} systems, i.e., systems in which the number of
315: individual processes is left as a parameter of the specification
316: (e.g., mutual exclusion protocols for {\em multi-agent} systems \cite{Boz02}).
317: Intuitively, such a representation is obtained by restricting our attention to logical
318: consequences represented via multisets of first order atomic formulas.
319: As an example, the formula
320: $$
321: p(A,use,stored(X))~\para~p(B,use,stored(X))~\lollo~\all
322: $$
323: can be used to denote all multisets of {\em ground} atomic formulas
324: {\em containing} an instance of the clause head. As the constant
325: $\all$ is provable in any context, in the previous example we obtain a
326: {\em symbolic representation} of the infinite set of {\em unsafe
327: states} generated by the following minimal violation of mutual
328: exclusion for a generic resource represented via the shared variable
329: $X$: {\em at least two different processes are in their critical
330: section using a shared resource}.
331: %
332: \item[(2)] Besides the connection with verification of concurrent
333: systems, the new fixpoint semantics for first order LO programs
334: represents an alternative to the traditional top-down execution of
335: linear logic programs studied in the literature \cite{And92}. Thus,
336: also from the point-of-view of logic programming, we extend the
337: applicability of our previous work \cite{BDM02a} (that was restricted
338: to the propositional case) towards more interesting classes of linear
339: logic programs.
340: %\smallskip\\
341: \item[(3)] The termination of the fixpoint computation cannot be
342: guaranteed in general; first order LO programs are in fact Turing
343: complete. However, we present here sufficient conditions under which
344: we can compute a {\em symbolic representation of all logical
345: consequences} of a non trivial first order fragment of LO with
346: universal quantification in goal formulas. As a direct consequence of
347: this result, we obtain that provability is decidable in the considered
348: fragment. To our knowledge, this result uncovers a new decidable
349: fragment of first order linear logic. The fragment taken into
350: consideration is not only interesting from a theoretical point of
351: view, but also as a possible abstract model for ``processes'' with
352: identifiers or local values.
353: \end{itemize}
354: %\smallskip\\
355:
356: Though the emphasis of this work is on the theoretical grounds of our
357: method, we will illustrate the practical use of our framework with the
358: help of a verification problem for a {\em mutual exclusion protocol}
359: defined for a concurrent system which is parametric in the number of
360: {\em clients}, {\em resources}, and related {\em monitors}. Other
361: practical applications of this method are currently under
362: investigation. Preliminary results in this direction are shown in the
363: PhD thesis of Marco Bozzano \cite{Boz02}.
364:
365: Finally, we remark that a very preliminary version of this work appeared
366: in the proceedings of FLOPS 2001 \cite{BDM01a}.
367:
368: \subsection{Outline of the Paper}
369: The terminology and some notations used in the paper are presented in
370: Appendix \ref{prelimsec}. To improve the readability of the paper,
371: the proofs of some lemmas are given in Appendix \ref{proofsapp}. In
372: Section \ref{relatedworks}, we will discuss related works. In Section
373: \ref{losec} we will recall the main definitions of the fragment LO of
374: \cite{AP90}, presented here with universal quantification in goal
375: formulas. In order to illustrate the use of LO as a specification
376: logic for concurrent systems, in the same section we will briefly
377: describe how {\em multiset rewriting} (extended with quantification)
378: can be embedded into LO. This connection represents a natural entry
379: point into the world of concurrency. In fact, the relationship
380: between multiset rewriting, (Colored) Petri Nets, and process calculi
381: has been extensively studied in the literature (see e.g.,
382: \cite{Cer95,Far99,Far00,Mes92,MM91}). Finally, we will present an example
383: of use of LO as a specification language for concurrent systems, and
384: discuss the relationships between (bottom-up) LO provability and
385: verification techniques based on (infinite-state) model checking. In
386: Section \ref{fobottomupsec}, we will introduce a {\em non effective}
387: fixpoint semantics for linear logic programs. To simplify the
388: manipulation of non ground terms, we will first lift the top-down
389: (proof theoretical) semantics of LO to the non ground level, by
390: introducing a new proof system in which sequents may have formulas
391: with free variables. In Section \ref{foeffectivesec}, we will
392: introduce a general framework for the bottom-up evaluation of LO
393: programs. The bottom-up procedure is based on a finite representation
394: of infinite sets of logical consequences, and on an effective fixpoint
395: operator working on sets of symbolic representations. The bottom-up
396: procedure can be seen as a symbolic version of the semantics presented
397: in Section \ref{fobottomupsec}. The reason for introducing two
398: different semantic definitions is to ease the proof of soundness and
399: completeness, which is split into the proof of equivalence of the
400: effective semantics with respect to the non-effective one, and the
401: proof of equivalence of the non-effective semantics with respect to
402: the operational one. In Section \ref{foterminatsec}, we will
403: investigate sufficient conditions for the termination of the bottom-up
404: evaluation. In Section \ref{examplessec}, we will discuss the
405: possible application of the resulting method as a verification
406: procedure for {\em infinite-state parameterized systems}. In Section
407: \ref{reachability}, we will address possible future directions of
408: research. In Section \ref{conclusions}, we will address some
409: conclusions.
410: %
411: \section{Related Works}
412: \label{relatedworks}
413: To our knowledge, our work is the first attempt
414: to connect algorithmic techniques used in symbolic model checking
415: with declarative and operational aspects of {\em first order} linear logic programming.
416: In \cite{BDM02a}, we have considered the relation
417: between {\em propositional} LO and Petri Nets.
418: Specifically, in \cite{BDM02a} we have shown that the bottom-up semantics
419: is computable for propositional LO programs
420: (because of the relationship of this problem with the coverability problem of Petri Nets).
421: Furthermore, in \cite{BDM02a} we have shown that the bottom-up
422: evaluation of propositional LO programs enriched with the constant $\one$
423: is not computable in a finite number of steps (otherwise
424: one could decide the equivalence problem for Petri Nets).
425:
426: We point out here that an original contribution of the paper
427: consists in extending the construction we used for proving the computability
428: of the bottom-up construction of propositional LO programs to {\em first order}
429: LO specifications. This way, we have established a link with more complex
430: models of concurrency.
431: Clearly, in the first order case provability becomes undecidable.
432: In the paper we present a non trivial special case of first order LO programs
433: in which the bottom-up semantics is still computable.
434: Extending the bottom-up evaluation to LO programs enriched with
435: the constant $\one$ is a possible future direction of research (see Section
436: \ref{reachability} for a discussion).
437:
438: In \cite{HW98}, Harland and Winikoff present an abstract deductive system
439: for bottom-up evaluation of linear logic programs.
440: The left introduction plus weakening and cut rules are used to compute
441: the logical consequences of a given formula.
442: Though the framework is given for a more general fragment than {LO},
443: it does not provide an {\em effective} procedure to evaluate
444: programs.
445: In \cite{APC97}, Andreoli, Pareschi and Castagnetti define an improved
446: {\em top-down} strategy for {\em propositional} LO based on the
447: Karp-Miller's covering graph of Petri Nets, i.e., a {\em forward} exploration
448: with accelerations.
449:
450: The relation between Rewriting, (Colored) Petri Nets and Linear Logic has been
451: investigated in previous works like \cite{Cer94b,Cer95,EW90,Mes92,MM91}.
452: Our point-of-view is based on the proofs as computations metaphor proposed in
453: \cite{AP90,And92,Mil96}, whereas
454: our connection with models for concurrency is inspired to works in this field like
455: \cite{Cer94b,Cer95,DM01,KY94,Mil93,Mil96}. As an example, in \cite{Cer94b,Cer95},
456: Cervesato shows how to encode Petri Nets in different fragments of linear logic like
457: {LO}, Lolli \cite{HM89}, and Forum \cite{Mil96} exploiting the different
458: features of these languages. Algorithmic aspects for verification of properties of the
459: resulting linear logic specifications are not considered in the works mentioned above.
460: In \cite{Far99,Far00}, Farwer presents a possible encoding of Colored Petri Nets in Linear Logic
461: and proposes a combination of the two formalisms that could be used to model object systems.
462:
463:
464: The problem of the {\em decidability} of provability in fragments of linear logic has been
465: investigated in several works in recent years \cite{Lin95,LMSS92,LSce94}.
466: Specifically, in \cite{Kop95}, Kopylov has shown that the full {\em propositional} linear
467: {\em affine} logic containing all the multiplicatives, additives, exponentials,
468: and constants is decidable. Affine logic can be viewed as linear logic with the
469: {\em weakening rule}. Propositional LO belongs to such a sub-structural logic.
470: Provability in full first order linear logic is undecidable as shown by Girard's
471: translation of first order logic into first order linear logic \cite{Gir87}.
472: The same holds for first order affine logic (Girard's encoding can also be viewed as
473: an encoding into affine logic \cite{Lin95}).
474: First order linear logic {\em without modalities}, i.e.,
475: without the possibility of re-using formulas, is decidable \cite{LSce94}.
476: In \cite{CDLMS99}, Cervesato et al. use a formalism based on
477: multiset-rewriting and existential quantification that can be embedded into our fragment
478: of linear logic to specify protocol rules and actions of intruders.
479: In \cite{DLMS99}, it is shown that reachability in
480: multiset rewriting with existential quantification is undecidable by a reduction
481: from Datalog with quantification in goal formulas. The fragment they consider however
482: is much more general than the {\em monadic} fragment of \LOfws.
483: Monadic \LOf can be viewed as a fragment of first order linear affine logic
484: with restricted occurrences of the exponentials (program clauses are re-usable)
485: and severe restrictions on the form of atomic formulas.
486: We are not aware of previous results on similar fragments.
487: %
488: %
489: \sectionl{The Logic Programming Language LO}{losec}
490: %
491: LO \cite{AP91a} is a logic programming language based on a fragment of
492: LinLog \cite{And92}.
493: Its mathematical foundations lie on a proof-theoretical presentation of
494: a fragment of linear logic defined over the linear connectives
495: $\lolli$ ({\em linear implication}, we use the reversed notation
496: $H\lollo G$ for $G\lolli H$), $\with$ ({\em additive conjunction}),
497: $\para$ ({\em multiplicative disjunction}), and the constant $\all$
498: ({\em additive identity}). In this section we present the proof-theoretical
499: semantics, corresponding to the usual {\em top-down}
500: operational semantics for traditional logic programming languages,
501: for an extension of LO. First of all, we consider a slight extension of LO
502: which admits the constant $\anti$ in goals and clause heads. More importantly,
503: we allow the universal quantifier to appear, possibly nested, in goals.
504: This extension is inspired by
505: {\em multiset rewriting with universal quantification} \cite{CDLMS99}.
506: The resulting language will be called \LOf hereafter.
507: Following \cite{AP91a}, we give the following definitions.
508: %
509: \begin{definition}[Atomic Formulas]
510: Let $\Sigma$ be a signature with predicates
511: including a set of constant and function symbols
512: $\calL$ and a set of predicate symbols $\calP$, and let $\calV$ be a
513: denumerable set of variables. An atomic formula over $\Sigma$ and $\calV$
514: has the form $p(t_1,\ldots,t_n)$ (with $n\geq 0$),
515: where $p\in\calP$ and $t_1,\ldots,t_n$
516: are (non ground) terms in $\TsigmaX{\calV}$.
517: We denote the set of such atomic formulas as $A_\Sigma^\calV$.
518: \end{definition}
519: %
520: We are now ready to define \LOf programs. The class of $\formula{D}$-formulas
521: correspond to multiple-headed program clauses, whereas $\formula{G}$-formulas
522: correspond to {\em goals} to be evaluated in a given program.
523: %
524: \begin{definition}[\LOf programs]
525: Let $\Sigma$ be a signature with predicates and $\calV$ a denumerable set
526: of variables. The classes of $\formula{G}$-formulas (goal formulas),
527: $\formula{H}$-formulas (head formulas), and $\formula{D}$-formulas
528: (program clauses) over $\Sigma$ and $\calV$ are defined by the following
529: grammar:
530: $$
531: \begin{array}{l}
532: \formula{G}\ ::=\ \formula{G}\ \para\ \formula{G}\ \ |\ \formula{G}\ \with\
533: \formula{G}\ \ |\ \ \foralx{\formula{G}}\ \ |\ \
534: \formula{A}\ \ |\ \ \all\ \ |\ \ \anti\\
535: [\smallskipamount]
536: \formula{H}\ ::=\ \formula{A}\para\ \ldots\para\ \formula{A}\ \ |\ \
537: \anti\\
538: [\smallskipamount]
539: \formula{D}\ ::=\ \formula{H}\ \lollo\ \formula{G}\ \ |\ \
540: \formula{D}\ \with\ \formula{D}\ \ |\ \ \foralx{\formula{D}}
541: \end{array}$$
542: where $\formula{A}$ stands for an atomic formula over $\Sigma$ and $\calV$.
543: An \LOf program over $\Sigma$ and $\calV$ is a $\formula{D}$-formula
544: over $\Sigma$ and $\calV$.
545: A multiset of goal formulas will be called a {\em context} hereafter.
546: \end{definition}
547: %
548: \begin{remark}\rm
549: \label{programremark}
550: Given an \LOf program $P$, in the rest of the paper
551: we often find it convenient to view $P$ as the {\em set} of clauses
552: $D_1,\ldots,D_n$. Every {\em program clause} $D_i$ has the form
553: $\forall\,(H\lollo G)$ standing for $\forall x_1\ldots x_k\ldotp(H\lollo G)$,
554: where $\fvar{H\lollo G}=\{x_1,\ldots,x_k\}$.
555: \\
556: Formally, this is justified by the following logical equivalences \cite{Gir87}:
557: $$
558: \begin{array}{c}
559: !(D_1\with D_2)~\equiv~!D_1~\tensor~!D_2\\
560: \foralx{(D_1\with D_2)}~\equiv~~\foralx{D_1}~\with~\foralx{D_2}
561: \end{array}
562: $$
563: \end{remark}
564: For the sake of simplicity, in the following we usually omit the universal
565: quantifier in $\formula{D}$-formulas, i.e., we consider free variables as
566: being {\em implicitly} universally quantified.
567: \begin{definition}[\LOf Sequents]
568: Let $\Sigma$ be a signature with predicates and $\calV$ a denumerable set
569: of variables. An \LOf sequent has the form $\dedloP{\Sigma'}{G_1,\ldots,G_k}$,
570: where $P$ is an \LOf program over $\Sigma$ and $\calV$,
571: $G_1,\ldots,G_k$ is a context (i.e., a multiset of goals)
572: over $\Sigma$ and $\calV$, and $\Sigma'$ is a signature such that
573: $\Sigma\subseteq\Sigma'$.
574: \end{definition}
575: %
576:
577: %
578: According to Remark \ref{programremark}, structural rules
579: ({\em exchange}, {\em weakening} and {\em contraction}) are allowed
580: on the left-hand side, while on the
581: right-hand side only the rule of exchange is allowed
582: (for the fragment under consideration, it turns out that the
583: rule of weakening is admissible, while contraction is forbidden).
584: We now define provability in \LOfws.
585: %
586: \begin{definition}[Ground Instances]
587: \label{logroundinstdef}
588: Let $\Sigma$ be a signature with predicates and $\calV$ a denumerable set
589: of variables. Given an \LOf program $P$ over $\Sigma$ and $\calV$,
590: the set of ground instances of $P$, denoted $\gnd{P}$, is defined as follows:
591: $\gnd{P}\eqdef\{(H\lollo G)\,\theta\st\forall\,(H\lollo G)\in P\}$,
592: where $\theta$ is a grounding substitution for $H\lollo G$ (i.e., it maps
593: variables in $\fvar{H\lollo G}$ to ground terms in $\Tsigma$).
594: \end{definition}
595: %
596: The execution of a multiset of $\formula{G}$-formulas $G_1,\ldots,G_k$
597: in $P$ corresponds to a {\em goal-driven} proof for the sequent
598: $\dedloP{\Sigma}{G_1,\ldots,G_k}$.
599: According to this view, the operational semantics
600: of \LOf
601: is given via the {\em uniform} ({\em focusing}) \cite{And92} proof system
602: presented in Figure \ref{system_for_lof}, where
603: $P$ is a set of clauses, ${\cal A}$ is a multiset of atomic formulas,
604: and $\Delta$ is a multiset of $\formula{G}$-formulas.
605: We have used the notation $\ms{H}$, where $H$ is a
606: linear disjunction of atomic formulas $A_1\para\ldots\para A_n$,
607: to denote the multiset $A_1,\ldots,A_n$ (by convention, $\ms{\anti}=\Eps$,
608: where $\Eps$ is the empty multiset).
609: %
610: \begin{definition}[\LOf provability]
611: Let $\Sigma$ be a signature with predicates and $\calV$ a denumerable set
612: of variables. Given an \LOf program $P$ and a goal $G$,
613: over $\Sigma$ and $\calV$, we say that $G$ is provable from $P$ if
614: there exists a proof tree, built over the proof system of Figure
615: \ref{system_for_lof}, with root $\dedloPS{G}$, and such that every branch
616: is terminated with an instance of the $\all_r$ axiom.
617: \end{definition}
618: %
619: The concept of {\em uniformity} applied to LO
620: requires that the right rules $\all_r$, $\para_r$, $\with_r$, $\anti_r$,
621: $\forall_r$ have priority
622: over $bc$, i.e., $bc$ is applied only when the right-hand side of a sequent
623: is a multiset of {\em atomic} formulas (as suggested by the notation $\calA$
624: in Figure \ref{system_for_lof}).
625: The proof system of Figure \ref{system_for_lof} is a specialization of
626: more general uniform proof systems for linear logic like Andreoli's
627: focusing proofs \cite{And92} and Forum \cite{Mil96}.
628: %
629: \begin{figure*}
630: $$
631: \begin{array}{c}
632: \infer[\all_r]
633: {\dedloPS{\all,\Delta}}
634: {}
635: \ \ \ \
636: \infer[\para_r]
637: {\dedloPS{G_1\para G_2,\Delta}}
638: {\dedloPS{G_1,G_2,\Delta}}
639: \ \ \ \
640: \infer[\with_r]
641: {\dedloPS{G_1\with G_2,\Delta}}
642: {\dedloPS{G_1,\Delta} &
643: \dedloPS{G_2,\Delta}}
644: \\
645: \\
646: \infer[\anti_r]
647: {\dedloPS{\anti,\Delta}}
648: {\dedloPS{\Delta}}
649: \ \ \ \
650: \infer[\forall_r\ \ (c\not\in\Sigma)]
651: {\dedloPS{\foralx{G},\Delta}}
652: {\dedloP{\Sigma,c}{G[c/x],\Delta}}
653: \ \ \
654: \infer[bc\ \ (H\lollo G\ \in\gnd{P})]
655: {\dedloPS{\ms{H},\calA}}
656: {\dedloPS{G,\calA}}
657: \end{array}
658: $$
659: \caption{A proof system for \LOf}
660: \label{system_for_lof}
661: \end{figure*}
662: %
663: Rule {\em bc} is analogous to a backchaining (resolution) step in
664: traditional logic programming languages.
665: Note that according to the concept of resolution explained above,
666: {\em bc} can be executed only if the right-hand side of
667: the current \LOf sequent consists of atomic formulas.
668: As an instance of rule $bc$, we get the following proof fragment, which
669: deals with the case of clauses with empty head:
670: $$
671: \begin{array}{c}
672: \infer[bc] {\dedloPS{\calA}}
673: {\infer*{\dedloPS{\calA,G}}{}}
674: \medskip\\
675: provided\ \anti\lollo G\in\gnd{P}
676: \end{array}
677: $$
678: Given that clauses with empty head are always applicable in atomic
679: {\em contexts},
680: the degree of non-determinism they introduce in proof search is usually
681: considered unacceptable \cite{Mil96} and in particular they are forbidden in
682: the original presentation of LO \cite{AP91a}. However, the computational
683: model we are interested in, i.e., bottom-up evaluation, does not suffer
684: this drawback. Clauses with empty head often allow more flexible
685: specifications.
686:
687: LO clauses having the form $H\lollo\bot$ simply remove
688: the resources associated with $H$ from the right-hand side of the current sequent
689: ($H$ is rewritten into the empty multiset).
690: On the contrary, LO clauses having the form $H\lollo\all$ can be viewed as {\em termination}
691: rules.
692: In fact, when a backchaining step over such a clause is possible,
693: we get a {\em successful} (branch of a) computation,
694: independently of the current {\em context} $\calA$,
695: as shown in the following proof scheme:
696: $$
697: \begin{array}{c}
698: \infer[bc]
699: {\dedloPS{\ms{H},\calA}}
700: {\infer[\all_r]
701: {\dedloPS{\all,\calA}}{}
702: }
703: \medskip\\
704: provided\ H\lollo\all\in\gnd{P}
705: \end{array}
706: $$
707: This observation is formally stated in the following proposition
708: (we recall that $\submult$ is the multiset inclusion relation).
709: %
710: \begin{proposition}[Admissibility of the Weakening Rule]
711: \label{foaffine}
712: Given an \LOf program $P$ and two multisets of goals $\Delta,\Delta'$
713: such that $\Delta\submult\Delta'$, if
714: $\dedloPS{\Delta}$ then $\dedloPS{\Delta'}$.
715: \end{proposition}
716: %
717: \begin{proof}
718: By simple induction on the structure of \LOf proofs.
719: \end{proof}
720: %
721: Admissibility of the weakening rule makes \LOf an
722: {\em affine} fragment of linear logic \cite{Kop95}.
723: Note that all structural rules are admissible on the left hand side
724: (i.e., on the program part) of \LOf sequents.
725:
726: Finally, rule $\forall_r$ can be used to {\em dynamically} introduce new
727: {\em names} during the computation. The initial signature $\Sigma$ must
728: contain at least the constant, function, and predicate symbols of a given
729: program $P$, and it can dynamically grow thanks to rule $\forall_r$.
730:
731: \begin{remark}\rm
732: \label{extrusion}
733: Particular attention must be paid to the constants introduced in a derivation.
734: They cannot be extruded from the scope of the corresponding universal
735: quantifier. For this reason, every time rule $\forall_r$ is applied, a new
736: constant $c$ is added to the current signature, and the resulting goal is
737: proved in the new signature.
738: The idea is that all terms appearing on the right-hand
739: side of a sequent are implicitly assumed to range over the relevant signature.
740: This behavior is standard in logic programming languages \cite{MNPS91}.
741: \end{remark}
742: %
743: \begin{example}
744: \label{lofex}
745: Let $\Sigma$ be a signature with a constant symbol $a$, a function symbol $f$
746: and predicate symbols $p,q,r,s$.
747: Let $\calV$ be a denumerable set of variables, and
748: $u,v,w,\ldots\in\calV$. Let $P$ be the program
749: %
750: $$\begin{array}{l}
751: 1\ldotp\ \ r(w)\lollo q(f(w))\para s(w)\\
752: [\smallskipamount]
753: 2\ldotp\ \ s(z)\lollo\foralx{p(f(x))}\\
754: [\smallskipamount]
755: 3\ldotp\ \ \anti\lollo q(u)\with r(v)\\
756: [\smallskipamount]
757: 4\ldotp\ \ p(x)\para q(x)\lollo\all\\
758: \end{array}$$
759: %
760: The goal $s(a)$ is provable from $P$. The corresponding proof is shown
761: in Figure \ref{LOfprooffig} (where we have denoted by $bc^{(i)}$ the
762: application of the backchaining rule over clause number $i$ of $P$).
763: %
764: \begin{figure*}
765: $$
766: \infer[bc^{(2)}]{\dedloPS{s(a)}}
767: {\infer[\forall_r]{\dedloPS{\foralx{p(f(x))}}}
768: {\infer[bc^{(3)}]{\dedloPSc{p(f(c))}}
769: {\infer[\with_r]{\dedloPSc{p(f(c)),q(f(c))\with r(c)}}
770: {\infer[bc^{(4)}]{\dedloPSc{p(f(c)),q(f(c))}}
771: {\infer[\all_r]{\dedloPSc{\all}}{}}
772: &
773: \infer[bc^{(1)}]{\dedloPSc{p(f(c)),r(c)}}
774: {\infer[\para_r]{\dedloPSc{p(f(c)),q(f(c))\para s(c)}}
775: {\infer[bc^{(4)}]{\dedloPSc{p(f(c)),q(f(c)),s(c)}}
776: {\infer[\all_r]{\dedloPSc{\all},s(c)}{}
777: }}}}}}}
778: $$
779: \captionl{An example of \LOf proof}{LOfprooffig}
780: \end{figure*}
781: %
782: Note that the notion of {\em ground instance} is now relative to the current
783: signature. For instance, backchaining over clause 3 is possible because
784: the corresponding signature contains the constant $c$ (generated one level
785: below by the $\forall_r$ rule), and therefore
786: $\anti\lollo q(f(c))\with r(c)$ is a valid instance of clause 3.
787:
788: \end{example}
789: %
790: \subsectionl{Simulating Multiset Rewriting over First Order Atoms}{unified}
791: %
792: In this section we will focus our attention on the relationship between
793: {\em multiset rewriting over first order atoms} and
794: {\em first order LO theories}.
795: We will conclude by showing how enriching logic theories with universal
796: quantification can provide a way to generate {\em new values}.
797:
798:
799:
800: The connection between multiset rewriting systems over (first order) atomic
801: formulas and (first order) LO theories has been studied, e.g.,
802: in \cite{Cer94b,CDLMS99}.
803: In \cite{Cer94b} Cervesato presents different possible encodings of multiset
804: rewriting (without function symbols) in linear logic.
805: Specifically, he first presents an encoding in the multiplicative fragment
806: of intuitionistic linear logic (MILL),
807: where multiplicative conjunction $\tensor$ (``tensor'') and linear implication are used as
808: multiset constructor and rewrite relation, respectively.
809: As an example, the formula $p \tensor q \lolli r \tensor s$
810: represents a rewrite rule in which $p$ and $q$ are rewritten into $r$ and $s$
811: ($\tensor$ denotes the ``tensor'').
812:
813: As highlighted in Remark 5.12 of \cite{Cer94b} an equivalent encoding can
814: be given by choosing a fragment of classical linear logic contained
815: in LO in which
816: multiplicative disjunction and reverse linear implication are used as
817: multiset constructor and rewrite relation, respectively.
818: As an example, the formula $p \para q \lollo r \para s$
819: represents a rewrite rule in which $p$ and $q$ are rewritten into $r$ and $s$.
820: This is the encoding we will adopt in our work.
821:
822: The duality of the two encodings is a consequence of the following property:
823: $
824: (p \tensor q \lolli r \tensor s)^\bot \equiv
825: p^\bot \para
826: q^\bot \lollo r^\bot
827: \para ~s^\bot
828: $,
829: where $a^\bot$ is the linear logic negation of $a$.
830: Furthermore, it depends on the way proofs are interpreted as computations,
831: i.e., on whether ``rewrite rules'' are encoded as formulas that occur
832: on the left- or on the right-hand side of a sequent.
833:
834: In Section 5.2.2 of \cite{Cer94b} Cervesato also presents an encoding of Petri Nets
835: in LO that allows one to simulate the execution of a net using an LO top-down
836: derivation of the resulting program.
837: In Section 5 of \cite{CDLMS99} the encoding of multiset rewriting over first
838: order atomic formulas (MSR) is
839: extended to first order MILL with existential quantifiers.
840: Thanks to its logical nature, the duality with the first order fragment
841: of LO still holds.
842:
843: To illustrate the main ideas behind the interpretation of LO
844: as multiset rewriting, let us first define the following class of LO formulas.
845: \begin{definition}\label{lorewrite}
846: We call {\em LO rewrite rule} any LO formula having the following form
847: $$
848: \forall(A_1\para\ldots\para A_n~\lollo~B_1\para\ldots\para B_m)
849: $$
850: where $A_1,\ldots,A_n$ and $B_1,\ldots,B_m$ are atomic formulas over $\Sigma$ and $\calV$.
851: \end{definition}
852: As usual, the notation $\forall\,(H\lollo G)$ stands for the universal
853: quantification of clause $H\lollo G$ over its free variables.
854:
855: LO formulas having the form depicted above can be interpreted as
856: {\em multiset rewriting rules} in which rewriting can be performed
857: only at the level of atomic formulas as in the MSR framework
858: defined in \cite{CDLMS99}.
859:
860: Specifically, let $P$ be a set of LO rewrite rules
861: (as in Def. \ref{lorewrite}).
862: Now, consider a goal formula $G$ having the form
863: $C_1\para\ldots\para C_k$ where $C_1,\ldots,C_k$ are {\em ground} atomic formulas over $\Sigma$.
864: It is easy to verify that any derivation starting from $\dedloPS{G}$
865: and built using LO proof rules amounts to a sequence of multisets rewriting steps,
866: where $\para$ is interpreted as multiset constructor.
867: \begin{example}
868: \label{msrex}
869: Let $\Sigma$ be a signature with two constant symbols $a$ and $b$, one
870: function symbol $f$ and two predicate symbols $p,q$.
871: Let $\calV$ be a denumerable set of variables and $x,y\in\calV$.
872: Let $P$ consists of the LO clause
873: $$
874: \forall x,y\ldotp p(x)\para q(f(y)) \lollo p(f(x))\para q(y)\para q(f(x))
875: $$
876: and $G=p(a)\para p(b)\para q(f(b))$. Figure \ref{LOmsr} shows
877: one possible sequence of applications of the above clause that
878: starts from the sequent $\dedloPS{G}$ (we have underlined atomic
879: formulas selected in the application of the $bc$ rule).
880: %
881: \begin{figure*}
882: {\footnotesize
883: $$
884: \begin{array}{cc}
885: \begin{array}{c}
886: \infer*[\para_r]{\dedloPS{p(a)\para p(b)\para q(f(b))}}
887: {\infer[bc]{\dedloPS{p(a),{\underline{p(b),q(f(b))}}}}
888: {\infer*[\para_r]{\dedloPS{p(a)\para p(f(b))\para q(b)\para q(f(b))}}
889: {\infer[bc]{\dedloPS{p(a),\underline{p(f(b))},q(b),\underline{q(f(b))}}}
890: {\infer*[\para_r]{\dedloPS{p(a)\para p(f(f(b)))\para q(b)\para q(b)\para q(f(f(b)))}}
891: {\dedloPS{p(a),p(f(f(b))),q(b),q(b),q(f(f(b)))}}
892: }
893: }
894: }
895: }
896: \end{array}
897: &
898: \begin{array}{c}
899: \{p(a),p(f(f(b))),q(b),q(b),q(f(f(b)))\}\\
900: \\
901: \uparrow\\
902: \\
903: \{p(a),\underline{p(f(b))},q(b),\underline{q(f(b))}\}\\
904: \\
905: \uparrow\\
906: \\
907: \{p(a),\underline{p(b),q(f(b))}\}
908: \end{array}
909: \\
910: \\
911: \mathrm{Derivation}
912: &
913: \mathrm{Rewriting}
914: \end{array}
915: $$}
916: \caption{Multiset rewriting over first order atomic formulas as LO proof construction}
917: \label{LOmsr}
918: \end{figure*}
919: \end{example}
920: From the previous example, we can observe the following properties.
921: All derivations built using {\em LO rewrite rules} of
922: Def. \ref{lorewrite} consist of applications of $\para_r$ and $bc$.
923: Thus, they have no branching (all derivations form a single line).
924: The combination of a sequence of applications of the
925: $\para_r$ rule and of the backchaining rule has the following effect:
926: the head of a ground instance of a rule in $P$ is matched against a sub-multiset
927: in the current goal; the selected multiset is replaced by the body of the rule.
928: Clearly, this property allows us to {\em simulate} multiset rewriting over first order
929: atomic formulas by using LO rewrite rules.
930:
931:
932: Now, let $F_1$ be the clause
933: $$
934: p(a)\para p(f(f(b)))\para q(b)\para q(b)\para q(f(f(b)))\lollo \top
935: $$
936: If we enrich $P$ with $F_1$, then we can transform the partial derivation of
937: Figure \ref{LOmsr} into an LO proof as shown below (where $\delta$ stands for
938: the derivation fragment of Figure \ref{LOmsr}):
939: $$
940: \infer[bc]{\delta}
941: {\infer[\top_r]{\dedloPS{\top}}{}}
942: $$
943: It is important to note that the same effect can be achieved by adding any formula
944: with $\top$ that contains a {\em sub-multiset} of the right-hand side of the
945: last sequent in the derivation of Figure \ref{LOmsr}.
946: As an example, let $F_2$ be the formula
947: $$
948: p(a)\para q(b)\lollo \top
949: $$
950: If we enrich $P$ with $F_2$, then we can transform the partial derivation of
951: Figure \ref{LOmsr} into an LO proof as shown below (again, $\delta$ stands for
952: the derivation fragment of Figure \ref{LOmsr}):
953: $$
954: \infer[bc]{\delta}
955: {\infer[\top_r]{\dedloPS{\top,p(f(f(b))),q(b),q(f(f(b)))}}{}}
956: $$
957:
958: More in general, let $P$ be a set of LO rewrite rules over $\Sigma$ and
959: $\calV$, and $\calM,\calM'$ two multisets of ground atomic
960: formulas (two configurations). Furthermore, let $H$, $G$ the
961: (possibly empty) $\,\para$-disjunctions of ground atomic formulas
962: such that $\ms{H}=\calM'$ and $\ms{G}=\calM$. Then, the
963: provability of the sequent $\dedLO{P,H\lollo\top}{G}$ precisely
964: characterizes the problem of {\em coverability} for the multiset (configuration)
965: $\calM'$, namely $\dedLO{P,H\lollo\top}{G}$ is provable if and only if
966: there exists a sequence of multiset rewriting steps defined over the theory $P$
967: that, starting from $\calM$, reaches a configuration $\calN$ that {\em covers}
968: $\calM'$, i.e., such that $\calM'\submult\calN$.
969:
970: This is a straightforward consequence of the properties of clauses like $H\lollo\top$
971: (it succeeds only if a sub-multiset of the right-hand side of the current
972: sequent matches $\ms{H}$) and of
973: the fact that, when working with LO rewrite rules, derivations have no branching.
974: In other words the only way we can transform a partial derivation like the one in Figure
975: \ref{LOmsr} into a {\em proof} is to apply (once and only once since derivations form a
976: single line) the clause with $\top$ (i.e., the target configuration is reached).
977:
978: Coverability is strictly related to the verification problem of
979: {\em safety properties} for concurrent systems \cite{ACJT96,FS01}.
980: For instance, as shown in \cite{BDM02a},
981: this property allows one to describe properties like {\em coverability} for a marking of
982: a Petri Net. In Section \ref{llmcsec}, we will show how to exploit this property in
983: the more general case of {\em first order} specifications.
984:
985: In Section \ref{reachability} we will discuss a possible characterization of
986: {\em reachability} for two configurations using derivability in an extension of LO.
987:
988: We conclude this section by discussing how {\em universal quantification} can be used
989: in order to enrich the expressiveness of LO rewrite rules.
990: \paragraph{The Role of Universal Quantification}
991: In the {\em proofs as computations} interpretation of logic programs,
992: universal quantification
993: is a logical operator which provides a way to generate {\em new values}.
994: From a logical perspective, this view of universal quantification is based
995: on its proof-theoretical semantics in intuitionistic
996: logic \cite{MNPS91}.
997: We will define first order rewrite rules with
998: universal quantification taking inspiration from \cite{CDLMS99}, where
999: a similar logic fragment, called MSR, is defined. In \cite{CDLMS99},
1000: MSR is used for the specification and analysis of {\em security protocols}.
1001:
1002: Given the direct relationship between (first order) multiset rewriting
1003: and (first order) linear logic, it should be evident that multiset rewriting
1004: with universal quantification is the counterpart of LO with universal
1005: quantification.
1006: Having this idea in mind,
1007: we extend the notion of LO rewrite rule as follows.
1008: \begin{definition}\label{qlorewrite}
1009: We call {\em LO quantified rewrite rule} any LO formula having the following form
1010: $$
1011: \forall(A_1\para\ldots\para A_n~\lollo \forall x_1,\ldots,x_n.(B_1\para\ldots\para B_m))
1012: $$
1013: where $A_1,\ldots,A_n$ and $B_1,\ldots,B_m$ are atomic formulas over $\Sigma$ and $\calV$.
1014: \end{definition}
1015: The operational semantics of LO theories consisting of LO quantified rewrite rules
1016: should be clear by looking at the LO proof rule for universally quantified
1017: goal formulas: they are eliminated by introducing new constants.
1018: This operational behavior naturally corresponds to the extension of multiset rewriting with
1019: fresh name generation defined in \cite{CDLMS99}.
1020:
1021: \begin{remark}\rm
1022: As mentioned at the beginning of this section, we remark that in \cite{CDLMS99} the logic
1023: MSR is compared with a fragment of linear logic which turns out to be {\em dual} with respect to
1024: ours, and therefore {\em existential} quantification is used in place of
1025: universal quantification.
1026: Specifically, an MSR rule is defined as $A \lolli\exists x\ldotp B$, meaning
1027: that $A$ evolves into $B$ by creating a new name for $x$.
1028: In LO with universal quantification the same effect is obtained via the
1029: clause $A \lollo\forall x\ldotp B$.
1030: In fact, in the goal driven proof system of LO a
1031: computation step is obtained by resolution (i.e., reducing the conclusion
1032: of a clause to its premise).
1033: \end{remark}
1034:
1035: The reader may refer to \cite{Cer94b,Cer95,CDLMS99,CDKS00} for a more formal treatment of
1036: the relationship between multiset rewriting and LO.
1037:
1038: \subsectionl{Specification of Concurrent Systems}{testlocksec}
1039: %
1040: The connection with multiset rewriting allows us to think about
1041: LO as a specification language for concurrent systems.
1042: We will illustrate this idea with the help of the following example.
1043: %
1044: We consider here a distributed {\em test-and-lock} protocol for a net with multiple resources, each of which is
1045: controlled by a monitor.
1046:
1047:
1048: The protocol is as follows. A set of {\em resources}, distinguished by means
1049: of {\em resource identifiers}, and an arbitrary set of processes are given.
1050: Processes can non-deterministically request access to any resource.
1051: Access to a given resource must be exclusive (only one process at a time).
1052: Mutual exclusion is enforced by providing each resource with a {\em semaphore}.
1053:
1054: Given a propositional symbol $init$,
1055: we can encode the initial states of the system as follows:
1056: %
1057: $$\begin{array}{l}
1058: 1\ldotp\ \ init\lollo init\para think\\
1059: [\smallskipamount]
1060: 2\ldotp\ \ init\lollo init\para m(x,unlocked)\\
1061: [\smallskipamount]
1062: 3\ldotp\ \ init\lollo\anti
1063: \end{array}$$
1064: %
1065: The atom $think$ represents a thinking (idle) process, while the first order
1066: atom $m(x,s)$ represents a {\em monitor} for the resource with identifier
1067: $x$ and associated semaphore $s$. The semaphore $s$ can assume one of
1068: the two values $locked$ or $unlocked$. Clause 1 and clause 2 can modify the
1069: initial state by adding, respectively, an arbitrary number of thinking
1070: processes and an arbitrary number of resources (with an initially
1071: unlocked semaphore).
1072: Finally, using clause 3 the atom $init$ can be removed after the initialization
1073: phase.
1074:
1075: The core of the protocol works as follows:
1076: %
1077: $$\begin{array}{l}
1078: 4\ldotp\ \ think\lollo wait(x)\\
1079: [\smallskipamount]
1080: 5\ldotp\ \ wait(x)\lollo think\\
1081: [\smallskipamount]
1082: 6\ldotp\ \ wait(x)\para m(x,unlocked)\lollo use(x)\para m(x,locked)\\
1083: [\smallskipamount]
1084: 7\ldotp\ \ use(x)\para m(x,locked)\lollo think\para m(x,unlocked)
1085: \end{array}$$
1086: %
1087: Using clause 4, a process can non-deterministically request access to any
1088: resource with identifier $x$, moving to a waiting state represented by the
1089: atom $wait(x)$. Clause 5 allows a process to go back to thinking from a waiting
1090: state. By clause 6, a waiting process can synchronize with the relevant
1091: monitor and is granted access provided the corresponding semaphore is
1092: unlocked. As a result, the semaphore is locked.
1093: The atom $use(x)$ represents a process which is currently using the resource
1094: with identifier $x$. Clause 7 allows a process to release a resource and
1095: go back to thinking, unlocking the corresponding semaphore.
1096:
1097: \begin{remark}\rm
1098: In the previous specification we have intentionally introduced a flaw which we will disclose later
1099: (see Section \ref{examplessec}). Uncovering of this flaw will allow us to explain and better
1100: motivate the use of the universal quantifier for the generation of new names.
1101: \end{remark}
1102:
1103:
1104: \subsectionl{Linear Logic and Model Checking}{llmcsec}
1105: %
1106: One of the properties we would like to establish for the specification given
1107: in the previous example is that it ensures mutual exclusion for any resource
1108: used in the system.
1109: One of the difficulties for proving this kind of properties is that the
1110: specification taken into consideration has an infinite number of possible
1111: configurations (all possible rewritings of the goal $init$).
1112:
1113: In this paper we will define techniques that can be used to attack this kind of verification
1114: problems by exploiting an interesting connection between verification and
1115: bottom-up evaluation of LO programs.
1116:
1117: Let us consider again the protocol specification given in Example
1118: \ref{testlocksec}. The mutual exclusion property can be formulated
1119: as the following property over reachable configurations. Let $S$
1120: be the set of multiset of atomic formulas (i.e., a configuration)
1121: reachable in any derivation from the goal $init$. The protocol
1122: ensures mutual exclusion for resource $x$ if and only if for any
1123: $\calA\in S$, i.e., any reachable configuration,
1124: $\{use(x),use(x)\}$ is not a sub-multiset of $\calA$. In other
1125: words, all goal formulas containing two occurrences of the formula
1126: $use(x)$ represent possible violations of mutual exclusion for
1127: resource $x$.
1128:
1129: Following from the previous observation, a possible way of proving
1130: mutual exclusion for our sample protocol is to show that no
1131: configurations having the form $\{use(x),use(x),\ldots\}$ can be
1132: reached starting from the initial states.
1133: This verification methodology can be made effective using a
1134: backward exploration of a protocol specification as described in
1135: \cite{ACJT96}. Specifically, the idea is to saturate the set of
1136: predecessor configurations (i.e., compute all possible predecessor
1137: configurations of the potential violations) and then check that no
1138: initial state occurs in the resulting set.
1139:
1140: This verification strategy can be reformulated in a natural way in
1141: our fragment of linear logic. First of all, LO formulas with the
1142: $\all$ constant can be used to finitely represent all possible
1143: violations as follows:
1144: %
1145: $$\begin{array}{l}
1146: U \eqdef \foralx~{use(x)\para use(x)\lollo\all}
1147: \end{array}$$
1148: %
1149: Backward reachability amounts then to
1150: compute all possible {\em logical consequences} of the LO
1151: specification of the protocol and of the formula $U$. In logic
1152: programming this strategy is called {\em bottom-up provability}.
1153: If the goal $init$ is in the resulting set, then there exists an
1154: execution (derivation) terminated by an instance of the axiom
1155: $\all$ that leads from $init$ to a multiset of the form
1156: $use(x),use(x),\calA$ for some $x$ and some multiset of atomic
1157: formulas $\calA$.
1158: Thus, the use of clauses with $\all$ to represent violations (and
1159: admissibility of weakening) allows us to reason independently of
1160: the number of processes in the initial states. Following
1161: \cite{ACJT96}, formulas like $\forall x\ldotp use(x)\para use(x)\lollo\all$ can be
1162: viewed as a symbolic representation of {\em upward-closed} sets of
1163: configurations.
1164:
1165: On the basis of these observations, the relationship between
1166: reachability and derivability sketched in the previous sections
1167: can be extended as shown in Figure \ref{prerelfig}.
1168: %
1169: \begin{figure*}[t]
1170: \begin{center}
1171: \begin{tabular}{c|c}
1172: {\bf Infinite State Concurrent Systems} & {\bf Linear Logic Specification}\\
1173: & \\
1174: transition system & LO program and proof system\\
1175: transition & rule instance\\
1176: current state & goal formula\\
1177: initial state & initial goal\\
1178: upward-closed set of states & LO clause with $\top$\\
1179: forward reachability & top-down provability\\
1180: backward reachability & bottom-up provability
1181: \end{tabular}
1182: \end{center}
1183: \captionl{Reachability versus provability}{prerelfig}
1184: \end{figure*}
1185: %
1186:
1187: In order to exploit this connection and extend the backward
1188: reachability strategy in the rest of the paper we will define a
1189: {\em bottom-up semantics} for first order LO programs. We will
1190: define our semantics via a fixpoint operator similar to the $T_P$
1191: operator used for logic programs. The fixpoint semantics will give
1192: us an effective way to evaluate bottom-up an LO program, and thus
1193: solve verification problems for infinite-state concurrent systems
1194: as the one described in this section.
1195:
1196: \sectionl{A Bottom-up Semantics for \LOf}{fobottomupsec}
1197: %
1198: The proof-theoretical semantics for \LOf corresponds to the {\em top-down}
1199: operational semantics based on resolution for traditional logic
1200: programming languages like Prolog.
1201: In this paper we are interested in finding a suitable definition of
1202: {\em bottom-up}
1203: semantics that can be used as an alternative operational semantics for \LOf
1204: programs. More precisely, we will define an {\em effective} and
1205: {\em goal-independent} procedure to compute
1206: all goal formulas which are provable from a given program $P$.
1207: This semantics extends the one described in \cite{BDM02a}, which was limited
1208: to propositional LO programs.
1209: In the following, given an \LOf program $P$,
1210: we denote by $\SigmaP$ the signature comprising the set
1211: of constant, function, and predicate symbols in $P$.
1212:
1213: \subsectionl{Non-ground Semantics for \LOf}{nongroundsec}
1214: %
1215: Before discussing the bottom-up semantics, we
1216: lift the definition of operational semantics to \LOf programs.
1217: Following \cite{BDM02a}, we would like to define the operational semantics of a
1218: program $P$ as the set of multisets of {\em atoms} which are provable from $P$.
1219: This could be done by considering the {\em ground instances} of \LOf program
1220: clauses (see Definition \ref{logroundinstdef}).
1221: However, in presence of universal quantification in goals, this solution is
1222: not completely satisfactory. Consider, in fact, the following example.
1223: Take a signature with a
1224: predicate symbol $p$ and two constants $a$ and $b$, and consider the \LOf
1225: program consisting of the axiom $\foralx{p(x)}\lollo\all$
1226: and the program consisting of the two clauses $p(a)\lollo\all$ and
1227: $p(b)\lollo\all$. The two programs would have the same {\em ground} semantics
1228: (i.e., consisting of the two singleton multisets $\{p(a)\}$ and $\{p(b)\}$).
1229: However, the \LOf goal $\foralx{p(x)}$ succeeds only in the
1230: first program, as the reader can verify.
1231: In order to distinguish the two programs, we need to consider the
1232: {\em non ground} semantics. In particular, our aim in this section will be
1233: to extend the so-called {\em C-semantics} of \cite{FLMP93}
1234: to first order LO.
1235:
1236: First of all, we give the following definition.
1237: %
1238: \begin{definition}[Clause Variants]
1239: \label{fovariantdef}
1240: Given an \LOf program $P$,
1241: the set of variants of clauses in $P$,
1242: denoted $\vrn{P}$, is defined as follows:
1243: $$\begin{array}{l}
1244: \vrn{P}\eqdef\{(H\lollo G)\,\theta\st\forall\,(H\lollo G)
1245: \in P\ \hbox{and}\ \theta\ \hbox{is a renaming}\\
1246: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \,
1247: \hbox{of the variables in}\ \fvar{H\lollo G}
1248: \ \hbox{with new variables}\}\ldotp
1249: \end{array}$$
1250: \end{definition}
1251:
1252: Now, we need to reformulate the
1253: proof-theoretical semantics of Section \ref{losec} (see Figure
1254: \ref{system_for_lof}). According to the C-semantics of \cite{FLMP93},
1255: our goal is to define the set of {\em non ground} goals which are provable
1256: from a given program $P$ with an {\em empty answer substitution}.
1257: Slightly departing from \cite{FLMP93}, we modify the proof system of
1258: Figure \ref{system_for_lof} as follows.
1259: Sequents are defined now over non ground goals.
1260: The backchaining rule of Figure \ref{system_for_lof} is replaced by the
1261: new rule shown in Figure \ref{csystem_for_lof} (where, as usual, $\calA$
1262: denotes a multiset of atomic formulas).
1263: The right-introduction rules and the axioms are as in Figure \ref{system_for_lof}.
1264: %
1265: \begin{figure*}
1266: $$
1267: \begin{array}{c}
1268: \infer[bc\ \ {\mbox {($H\lollo G)\ \in\vrn{P}$}}]
1269: {\dedloPS{\ms{H}\theta,\calA}}
1270: {\dedloPS{G\theta,\calA}}
1271: \end{array}
1272: $$
1273: \caption{Backchaining rule working over non ground goals}
1274: \label{csystem_for_lof}
1275: \end{figure*}
1276: %
1277: This proof system is based on the
1278: idea of considering a first order program as the (generally {\em infinite})
1279: collection of ({\em non ground})
1280: instances of its clauses. By {\em instance} of a clause
1281: $H\lollo G$, we mean a clause $H\theta\lollo G\theta$, where $\theta$ is
1282: {\em any} substitution.
1283: The reader can see that, with this intuition, the set of goals
1284: provable from the system modified with the backchaining rule shown
1285: in Figure \ref{csystem_for_lof} corresponds
1286: to the set of non ground goals which are provable with an empty answer
1287: substitution according to \cite{FLMP93}.
1288: This formulation of the proof system is the
1289: proof-theoretical counterpart of the bottom-up semantics
1290: we will define in the following.
1291:
1292: All formulas
1293: (and also substitutions) on the right-hand side of the sequents in the proof system
1294: obtained from Figure \ref{system_for_lof} by replacing the
1295: backchaining rule with the rule of Figure \ref{csystem_for_lof} are implicitly
1296: assumed to range over the set of {\em non ground} terms over $\Sigma$.
1297: Every time rule $\forall_r$ is fired, a new
1298: constant $c$ is added to the current signature, and the resulting goal is
1299: proved in the new signature (see Remark \ref{extrusion}).
1300: Rule $bc$ denotes a backchaining (resolution) step, where $\theta$ indicates
1301: {\em any} substitution.
1302: For our purposes, we can assume $\Dom{\theta}\subseteq\fvar{H}\Union\fvar{G}$
1303: (we remind that $\fvar{F}$ denotes the {\em free} variables of $F$).
1304: Note that $H\lollo G$ is assumed to be a variant, therefore it has
1305: no variables in common with $\calA$.
1306: According to the usual concept of {\em uniformity},
1307: $bc$ can be executed only if the right-hand side of
1308: the current sequent consists of atomic formulas.
1309: Rules $\all_r$, $\,\para_r$, $\with_r$ and $\anti_r$
1310: are the same as in propositional LO.
1311: A sequent is provable if all branches of its proof tree
1312: terminate with instances of the $\all_r$ axiom.
1313:
1314: Clearly, the proof system
1315: obtained by considering the rule of Figure \ref{csystem_for_lof} is not {\em effective},
1316: however it will be
1317: sufficient for our purposes. An effective way to compute the set of goals which
1318: are provable from the above proof system will be discussed in Section
1319: \ref{foeffectivesec}.
1320:
1321: We give the following definition, where $\ded_{\Sigma}$ denotes the provability
1322: relation defined by the proof system of Figure \ref{system_for_lof} in which
1323: the backchaining rule has been replaced by the rule of Figure \ref{csystem_for_lof}.
1324: %
1325: \begin{definition}[Operational Semantics]
1326: \label{foopsemdef}
1327: Given an \LOf program $P$, its operational semantics,
1328: denoted $\osP$, is given by
1329: $$ \osP \eqdef \{\calA\st\calA\ \hbox{is a multiset of (non ground) atoms in}\
1330: \AsigmaPV\ \hbox{and}\ \dedloP{\SigmaP}{\calA}\}\ldotp $$
1331: \end{definition}
1332: %
1333: Intuitively, the set $\osP$ is closed by {\em instantiation}, i.e.,
1334: $\calA\theta\in\osP$ for any substitution $\theta$, provided $\calA\in\osP$.
1335: Note that the operational semantics only include multisets of (non ground)
1336: {\em atoms}, therefore no connective (including the {\em universal quantifier})
1337: can appear in the set $\osP$. However, the intuition will be that the variables
1338: appearing in a multiset in $\osP$ must be implicitly considered
1339: {\em universally quantified} (e.g., $\{p(x),q(x)\}\in\osP$ implies that the goal
1340: $\foralx{(p(x)\para q(x))}$ is provable from $P$).
1341: Also note that the information on provable {\em facts} from a given program $P$
1342: is all we need to decide whether a general goal
1343: (possibly with nesting of connectives) is provable from
1344: $P$ or not. In fact, according to \LOf proof-theoretical semantics,
1345: provability of a compound goal can always be
1346: reduced to provability of a finite set of atomic multisets.
1347:
1348: \subsectionl{Fixpoint Semantics for \LOfws}{fixpointsec}
1349: %
1350: We will now discuss the {\em bottom-up} semantics.
1351: In order to deal with universal quantification
1352: (and therefore signature augmentation),
1353: we extend the definitions of Herbrand base and (concrete)
1354: interpretations given in \cite{BDM02a} as follows.
1355: Let $\SigP$ be the set of all possible extensions of the signature $\Sigma_P$
1356: associated to a program $P$ with new constants.
1357: The definition of Herbrand base now depends explicitly on the
1358: signature, and interpretations can be thought of as infinite tuples, with
1359: one element for every signature $\Sigma\in\SigP$.
1360: From here on the powerset of a given set $D$ will be indicated as $\Part{D}$.
1361:
1362: We give then the following definitions.%
1363: \begin{definition}[Herbrand Base]
1364: Given an \LOf program $P$ and a signature $\Sigma\in\SigP$, the Herbrand base
1365: of $P$ over $\Sigma$, denoted $\hbS{P}$, is given by
1366: $$ \hbS{P}\eqdef\MS{\AsigmaV}=\{\calA\st\calA\ \hbox{is a multiset of (non ground)
1367: atoms in}\ \AsigmaV\}\ldotp $$
1368: \end{definition}
1369: %
1370: \begin{definition}[Interpretations]
1371: \label{fointerpdef}
1372: Given an \LOf program $P$,
1373: a (concrete) interpretation is a family of sets $\Fam{I}$,
1374: where $I_\Sigma\in\Part{\hbS{P}}$ for every $\Sigma\in\SigP$.
1375: \end{definition}
1376: %
1377: In the following we often
1378: use the notation $I$ for an interpretation to denote the
1379: family $\Fam{I}$.
1380:
1381: Interpretations form a complete lattice where inclusion and least upper bound
1382: are defined like (component-wise) set inclusion and union. In the following
1383: definition we therefore overload the symbols $\subseteq$ and $\Union$ for sets.
1384: %
1385: \begin{definition}[Interpretation Domain]
1386: \label{fodomaindef}
1387: Interpretations form a complete lattice
1388: $\couple{\calD}{\subseteq}$, where:
1389: \begin{itemize}
1390: \item $\calD=\{I\st I\ \hbox{is an interpretation}\}$;
1391: \item $I\subseteq J$ if and only if $I_\Sigma\subseteq J_\Sigma$ for every
1392: $\Sigma\in\SigP$;
1393: \item the least upper bound of $I$ and $J$ is
1394: $\{I_\Sigma\Union J_\Sigma\}_{\Sigma\in\SigP}$;
1395: \item the bottom and top elements are
1396: $\eset=\Fam{\eset}$ and
1397: $\{\hbS{P}\}_{\Sigma\in\SigP}$, respectively.
1398: \end{itemize}
1399: \end{definition}
1400: %
1401: Before introducing the definition of fixpoint operator,
1402: we need to define the notion of satisfiability of a context $\Delta$ (a multiset of
1403: goal formulas) in a
1404: given interpretation $I$. For this purpose, we introduce the judgment
1405: $\valS{I}{\Delta}{\calC}$,
1406: where $I$ is an {\em input} interpretation, $\Delta$ is an {\em input} context,
1407: and $\calC$ is an {\em output}
1408: fact (a multiset of atomic formulas).
1409: The judgment is also parametric with respect to a given signature $\Sigma$.
1410:
1411: The need for this judgment, with respect to the familiar logic programming
1412: setting \cite{GDL95}, is motivated by the arbitrary nesting of
1413: connectives in \LOf clause bodies. The satisfiability judgment is modeled
1414: according to the right-introduction rules of the connectives. In other words,
1415: the computation performed by the satisfiability judgment corresponds to
1416: {\em top-down} steps inside our {\em bottom-up} semantics. Intuitively,
1417: the parameter $\calC$ must be thought of as
1418: an {\em output} fact such that $\calC+\Delta$ is valid in $I$.
1419: The notion of output fact will simplify the
1420: presentation of the algorithmic version of the judgment which we will present
1421: in Section \ref{foeffectivesec}.
1422: The notion of {\em satisfiability} is modeled according to the
1423: right-introduction (decomposition) rules of the proof system, as follows
1424: (we remind that '+' denotes multiset union).
1425: \begin{definition}[Satisfiability Judgment]
1426: \label{satjdef}
1427: Let $P$ be an \LOf program,
1428: $\Sigma\in\SigP$, and $I=\Fam{I}$ an interpretation.
1429: The satisfiability judgment $\satS$ is defined as follows:
1430: $$\begin{array}{l}
1431: \valS{I}{\all,\Delta}{\calC}\ \hbox{for any fact}\ \calC\ \hbox{in}\
1432: \AsigmaV;\\
1433: [\medskipamount]
1434: \valS{I}\calA{\calC}\ \hbox{if}\ \calA+\calC \in I_\Sigma;\\
1435: [\medskipamount]
1436: \valS{I}{\foralx{G},\Delta}{\calC}\ \hbox{if}\
1437: \val{I}{\Sigma,c}{G[c/x],\Delta}{\calC},\ \hbox{with}\ c\not\in\Sigma
1438: \ \hbox{{\rm (}see remark \ref{satexportremark}{\rm )}};\\
1439: [\medskipamount]
1440: \valS{I}{G_1\with G_2,\Delta}{\calC}\ \hbox{if}\
1441: \valS{I}{G_1,\Delta}{\calC}\ \hbox{and}\
1442: \valS{I}{G_2,\Delta}{\calC};\\
1443: [\medskipamount]
1444: \valS{I}{G_1\para G_2,\Delta}{\calC}\ \hbox{if}\
1445: \valS{I}{G_1,G_2,\Delta}{\calC};\\
1446: [\medskipamount]
1447: \valS{I}{\anti,\Delta}{\calC}\ \hbox{if}\
1448: \valS{I}{\Delta}{\calC}\ldotp
1449: \end{array}$$
1450: \end{definition}
1451: %
1452: %
1453: %
1454: \begin{remark}\rm
1455: \label{satexportremark}
1456: When using the notation $\valS{I}{\Delta}{\calC}$
1457: we {\em always} make the {\em implicit} assumption that $\Delta$ is
1458: a context defined over $\Sigma$ (i.e., term constructors in $\Delta$ must
1459: belong to $\Sigma$). As a result, also the output fact $\calC$ must be
1460: defined over $\Sigma$. This assumption, which is the counterpart
1461: (see Remark \ref{extrusion}) of an
1462: analogous assumption for proof systems like the one in Figure
1463: \ref{system_for_lof}, i.e., with explicit signature notation,
1464: will {\em always} and {\em tacitly} hold in the following.
1465: For example, note that in the $\forall$-case of the $\satS$ definition below,
1466: the newly introduced constant $c$ {\em cannot be exported} through the
1467: output fact $\calC$. This is crucial to capture the operational semantics
1468: of the universal quantifier.
1469: \end{remark}
1470: %
1471:
1472:
1473: The satisfiability judgment $\satS$ satisfies the following properties.
1474: %
1475: \begin{lemma}
1476: \label{fomovelemma}
1477: For every interpretation $I=\Fam{I}$,
1478: context $\Delta$, and fact $\calC$,
1479: $$ \valS{I}{\Delta}{\calC}\ \hbox{if and only if}\ \valS{I}{\Delta,\calC}{\Eps}\ldotp $$
1480: \end{lemma}
1481: %
1482: \begin{proof}
1483: See Appendix \ref{proofsapp}.
1484: \end{proof}
1485: %
1486: \begin{lemma}
1487: \label{fovallemma}
1488: For any interpretations $I_1=\Fam{(I_1)}$, $I_2=\Fam{(I_2)}$, \ldots,
1489: context $\Delta$, and fact $\calC$,
1490: \begin{enumerate}
1491: \item if $I_1\subseteq I_2$ and $\valS{I_1}{\Delta}{\calC}$ then
1492: $\valS{I_2}{\Delta}{\calC}$;
1493: \item if $I_1\subseteq I_2\subseteq\ldots$ and
1494: $\valS{\Un{i}{\Inf}I_i}{\Delta}{\calC}$ then there exists $k\in\Nat$
1495: s.t. $\valS{I_k}{\Delta}{\calC}$.
1496: \end{enumerate}
1497: \end{lemma}
1498: %
1499: \begin{proof}
1500: See Appendix \ref{proofsapp}.
1501: \end{proof}
1502: %
1503: We are now ready to define the fixpoint operator $\Tp$.
1504: %
1505: \begin{definition}[Fixpoint Operator {\boldmath $\Tp$}]
1506: \label{Tpdef}
1507: Given an \LOf program $P$ and an interpretation $I=\Fam{I}$,
1508: the fixpoint operator $\Tp$ is defined as follows:
1509: $$
1510: \begin{array}{l}
1511: \Tp(I)\eqdef\Fam{(\Tp(I))};\\
1512: [\medskipamount]
1513: (\Tp(I))_\Sigma\eqdef\{\ms{H}\theta+\calC\st
1514: (H\lollo G)\in\vrn{P},\ \theta\ \hbox{is}\\
1515: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
1516: \hbox{any substitution,}\ \hbox{and}\
1517: \valS{I}{G\theta}{\calC}\}\ldotp\\
1518: \end{array}
1519: $$
1520: \end{definition}
1521: %
1522: \begin{remark}\rm
1523: In the previous definition, $\theta$ is implicitly assumed to be defined over
1524: $\Sigma$, i.e., $\theta$ can only map variables in $\Dom{\theta}$ to terms in
1525: $\TsigmaX{\calV}$.
1526: \end{remark}
1527: %
1528: The following property holds.
1529: \begin{proposition}[Monotonicity and Continuity]
1530: \label{monconttpprop}
1531: For every \LOf program $P$, the fixpoint operator $\Tp$ is monotonic and
1532: continuous over the lattice $\couple{\calD}{\subseteq}$.
1533: \end{proposition}
1534: %
1535: \begin{proof}
1536: {\em Monotonicity}.\nl
1537: Immediate from the definition of $\Tp$ and item $i$ of Lemma \ref{fovallemma}.
1538: \vsep
1539: {\em Continuity}.\nl
1540: We prove that
1541: $\Tp$ is finitary, i.e., for any sequence of interpretations
1542: $I_1\subseteq I_2\subseteq\ldots$ we have that
1543: $\Tp(\Un{i}{\Inf}I_i)\subseteq\Un{i}{\Inf}\Tp(I_i)$, i.e.,
1544: for every $\Sigma\in\SigmaP$,
1545: $(\Tp(\Un{i}{\Inf}I_i))_\Sigma\subseteq(\Un{i}{\Inf}\Tp(I_i))_\Sigma$.
1546: Let $\calA\in(\Tp(\Un{i}{\Inf}I_i))_\Sigma$.
1547: By definition of $\Tp$, there exist a variant
1548: $H\lollo G$ of a clause in $P$, a substitution $\theta$, and
1549: a fact $\calC$ s.t.
1550: $\calA=\ms{H}\theta+\calC$ and $\valS{\Un{i}{\Inf}I_i}{G\theta}{\calC}$.
1551: By item $ii$ of Lemma \ref{fovallemma}, we have that there exists
1552: $k\in\Nat$ s.t. $\valS{I_k}{G\theta}{\calC}$. Again by definition of $\Tp$,
1553: we get $\calA=\ms{H}\theta+\calC\in(\Tp(I_k))_\Sigma\subseteq
1554: (\Un{i}{\Inf}{\Tp(I_i)})_\Sigma$.
1555: \end{proof}
1556: %
1557: Monotonicity and continuity of the $\Tp$ operator imply, by Tarski's Theorem,
1558: that $\lfp{\Tp}=\itp{\omega}$. The fixpoint semantics of a program $P$ is
1559: then defined as follows.
1560: %
1561: \begin{definition}[Fixpoint Semantics]
1562: Given an \LOf
1563: program $P$, its fixpoint semantics, denoted $\fsP$, is defined as
1564: follows:
1565: $$ \fsP\eqdef(\lfp{\Tp})_\SigmaP=(\Itp{\omega}{\Fam{\eset}})_\SigmaP\ldotp $$
1566: \end{definition}
1567: %
1568: We conclude this section by proving the
1569: following fundamental result, which states that the fixpoint semantics is sound
1570: and complete with respect to the operational semantics (see Definition \ref{foopsemdef}).
1571: %
1572: \begin{theorem}[Soundness and Completeness]
1573: \label{fofixpoint_operational}
1574: For every \LOf program $P$, $\fsP$ $=$ $\osP$.
1575: \end{theorem}
1576: %
1577: \begin{proof}
1578: $\fsP\subseteq\osP$.
1579: \nl
1580: We prove that for every $k\in\Nat$, for every signature
1581: $\Sigma\in\SigP$, and for every context $\Delta$,
1582: $\valS{\itp{k}}{\Delta}{\Eps}$ implies
1583: $\dedloPS{\Delta}$. The proof is by lexicographic induction on $(k,h)$, where
1584: $h$ is the length of the derivation of $\valS{\itp{k}}{\Delta}{\Eps}$.
1585: \begin{itemize}
1586: \item[-] If $\Delta=\all,\Delta'$, obvious;
1587: \item[-] if $\Delta=\calA$ and $\calA\in(\itp{k})_\Sigma$, then there exist
1588: a variant $H\lollo G$ of a clause in $P$, a fact $\calC$
1589: and a substitution $\theta$ s.t.
1590: $\calA=\ms{H}\theta+\calC$ and $\valS{\itp{k-1}}{G\theta}{\calC}$.
1591: By Lemma \ref{fomovelemma}, this implies
1592: $\valS{\itp{k-1}}{G\theta,\calC}{\Eps}$.
1593: Then by the inductive hypothesis we have $\dedloPS{G\theta,\calC}$, from
1594: which $\dedloPS{\ms{H}\theta,\calC}$, i.e., $\dedloPS{\calA}$ follows
1595: by $bc$ rule;
1596: \item[-] if $\Delta=\foralx{G},\Delta'$ and
1597: $\val{\itp{k}}{\Sigma,c}{G[c/x],\Delta'}{\Eps}$, with $c\not\in\Sigma$,
1598: then by the inductive hypothesis we have $\dedloP{\Sigma,c}{G[c/x],\Delta'}$
1599: from which $\dedloPS{\foralx{G},\Delta'}$ follows by $\forall_r$ rule;
1600: \item[-] if $\Delta=G_1\with G_2,\Delta'$,
1601: $\valS{\itp{k}}{G_1,\Delta'}{\Eps}$, and
1602: $\valS{\itp{k}}{G_2,\Delta'}{\Eps}$, then
1603: by the inductive hypothesis we have
1604: $\dedloPS{G_1,\Delta'}$ and $\dedloPS{G_2,\Delta'}$, from which
1605: $\dedloPS{G_1\with G_2,\Delta'}$ follows by $\with_r$ rule;
1606: \item[-] if $\Delta=G_1\para G_2,\Delta'$ and
1607: $\valS{\itp{k}}{G_1,G_2,\Delta'}{\Eps}$, then
1608: by the inductive hypothesis we have $\dedloPS{G_1,G_2,\Delta'}$, from
1609: which $\dedloPS{G_1\para G_2,\Delta'}$ follows by $\para_r$ rule;
1610: \item[-] if $\Delta=\anti,\Delta'$ and
1611: $\valS{\itp{k}}{\Delta'}{\Eps}$, then
1612: by the inductive hypothesis we have $\dedloPS{\Delta'}$, from
1613: which $\dedloPS{\anti,\Delta'}$ follows by $\anti_r$ rule.
1614: \end{itemize}
1615: $\osP\subseteq\fsP$.
1616: \nl
1617: We prove that for every signature $\Sigma\in\SigP$ and for every context
1618: $\Delta$, if $\dedloPS{\Delta}$ then there exists $k\in\Nat$ s.t.
1619: $\valS{\itp{k}}{\Delta}{\Eps}$. The proof is by induction on the derivation of
1620: $\dedloPS{\Delta}$.
1621: \begin{itemize}
1622: \item[-] If $\Delta=\all,\Delta'$, then for every $k\in\Nat$,
1623: $\valS{\itp{k}}{\Delta}{\Eps}$;
1624: \item[-] if $\Delta=\ms{H}\theta,\calA$, with $H\lollo G$ a variant of a clause
1625: in $P$, $\theta$ substitution, and $\dedloPS{G\theta,\calA}$, then
1626: by the inductive hypothesis we have that there exists $k\in\Nat$ s.t.
1627: $\valS{\itp{k}}{G\theta,\calA}{\Eps}$. Then, by Lemma \ref{fomovelemma},
1628: $\valS{\itp{k}}{G\theta}{\calA}$. By definition of $\Tp$,
1629: $\ms{H}\theta+\calA\in(\itp{k+1})_\Sigma$, which implies
1630: $\valS{\itp{k+1}}{\ms{H}\theta+\calA}{\Eps}$;
1631: \item[-] if $\Delta=\foralx{G},\Delta'$ and
1632: $\dedloP{\Sigma,c}{G[c/x],\Delta'}$, with $c\not\in\Sigma$, then by
1633: the inductive hypothesis we have that there exist $k\in\Nat$ s.t.
1634: $\val{\itp{k}}{\Sigma,c}{G[c/x],\Delta'}{\Eps}$, from which
1635: $\valS{\itp{k}}{\foralx{G},\Delta'}{\Eps}$ follows;
1636: \item[-] if $\Delta=G_1\with G_2,\Delta'$,
1637: $\dedloPS{G_1,\Delta'}$ and $\dedloPS{G_2,\Delta'}$, then
1638: by the inductive hypothesis we have that there exist $k_1,k_2\in\Nat$ s.t.
1639: $\valS{\itp{k_1}}{G_1,\Delta'}{\Eps}$ and
1640: $\valS{\itp{k_2}}{G_2,\Delta'}{\Eps}$. By taking $k=max\{k_1,k_2\}$,
1641: by item $i$ of Lemma \ref{fovallemma} and monotonicity of $\Tp$ (Proposition \ref{monconttpprop})
1642: we get
1643: $\valS{\itp{k}}{G_1,\Delta'}{\Eps}$ and
1644: $\valS{\itp{k}}{G_2,\Delta'}{\Eps}$, from which
1645: $\valS{\itp{k}}{G_1\with G_2,\Delta'}{\Eps}$ follows;
1646: \item[-] if $\Delta=G_1\para G_2,\Delta'$ or $\Delta=\anti,\Delta'$,
1647: the conclusion follows by a
1648: straightforward application of the inductive hypothesis.
1649: \end{itemize}
1650: \end{proof}
1651: %
1652: \begin{example}
1653: Let $\Sigma$ be a signature including the constant symbols $a$ and $b$,
1654: a function symbol $f$, and the predicate symbols $p,q,r$, let $\calV$ be a
1655: denumerable set of variables and $x,y\in\calV$, and let $P$ be the
1656: following \LOf program:
1657: $$\begin{array}{l}
1658: 1\ldotp\ \ r(f(b))\para p(a)\lollo\all\\
1659: [\smallskipamount]
1660: 2\ldotp\ \ p(x)\lollo\all\\
1661: [\smallskipamount]
1662: 3\ldotp\ \ q(y)\lollo(\foralx{p(x)})\with r(y)
1663: \end{array}$$
1664: Let $I_0=\Fam{\eset}$, and let us compute $I_1=\Tp(I_0)$.
1665: Using clauses 1 and 2, we get that (see Definitions \ref{satjdef} and \ref{Tpdef})
1666: $(I_1)_\Sigma$ contains the multisets of
1667: atoms of the form $\{r(f(b)),p(a)\}+\calA$, and
1668: $\{p(t)\}+\calA$, where $\calA$ is
1669: any multiset of (possibly non-ground) atoms in $\AsigmaV$, while $t$ is any
1670: (possibly non ground) term in $\TsigmaV$.
1671: Similarly $(I_1)_{\Sigma'}$, for a
1672: generic signature $\Sigma'$ such that $\Sigma\subseteq\Sigma'$, contains all
1673: multisets of the above form where $\calA$ and $t$ are taken from,
1674: respectively, $\AsigV{\Sigma'}$ and $\TsigV{\Sigma'}$. For instance, let
1675: $c$ be a new constant not appearing in $\Sigma$. The set $(I_1)_{\Sigma'}$ will
1676: contain, e.g., the multisets $\{p(c)\}$, $\{p(f(c)),q(b)\}$, and so on.
1677:
1678: Now, consider the substitution $\theta=[\substbind{y}{f(b)}]$ and the
1679: following corresponding instance of clause 3:
1680: $q(f(b))\lollo(\foralx{p(x)})\with r(f(b))$.
1681: Assume we want to compute an output fact $\calC$ for the judgment
1682: $$ \valS{I_1}{(\foralx{p(x)})\with r(f(b))}{\calC}\ldotp $$
1683: By definition of $\satP$, we have to compute
1684: $\valS{I_1}{(\foralx{p(x)})}{\calC}$ and
1685: $\valS{I_1}{r(f(b))}{\calC}$. For the latter judgment we have that, e.g.,
1686: $\valS{I_1}{r(f(b))}{p(a)}$. For the first judgment, by definition of $\satP$,
1687: we must compute $\val{I_1}{\Sigma,c}{{p(c)}}{\calC}$, where $c$ is a
1688: new constant not in $\Sigma$. As $\{p(c)\}$
1689: is contained in $(I_1)_{\Sigma,c}$, we
1690: can get that $\val{I_1}{\Sigma,c}{{p(c)}}{\Eps}$. We can also get
1691: $\val{I_1}{\Sigma,c}{{p(c)}}{p(a)}$ (in fact $\{p(c),p(a)\}$ is also
1692: contained in $(I_1)_{\Sigma,c}$. By applying the $\with$-rule for $\satP$,
1693: we get that $\valS{I_1}{(\foralx{p(x)})\with r(f(b))}{p(a)}$.
1694: Therefore, by applying clause 3 we get that, e.g., the multiset $\{q(b),p(a)\}$ is in
1695: $(I_2)_\Sigma=(\Tp(I_1))_\Sigma$.
1696: \end{example}
1697: %
1698: \sectionl{An Effective Semantics for \LOf}{foeffectivesec}
1699: %
1700: The fixpoint operator $\Tp$ defined in the previous section
1701: does not enjoy one of the crucial properties we required for our
1702: bottom-up semantics, namely its definition is {\em not} effective.
1703: This is a result of both the definition of the satisfiability judgment
1704: (whose clause for $\all$ is clearly not effective) and the definition of
1705: interpretations as infinite tuples. In order to solve these problems, we first
1706: define the (abstract) Herbrand base and (abstract) interpretations as
1707: follows.
1708: %
1709: \begin{definition}[Abstract Herbrand Base]
1710: Given an \LOf
1711: program $P$, the Herbrand
1712: base of $P$, denoted $\hb{}{P}$, is given by
1713: $$ \hb{}{P}\eqdef\hb{\SigmaP}{P}\ldotp $$
1714: \end{definition}
1715: %
1716: \begin{definition}[Abstract Interpretations]
1717: \label{foainterpdef}
1718: Given an \LOf program $P$, an
1719: interpretation $I$ is any subset of $\hb{}{P}$,
1720: i.e., $I\in\Part{\hb{}{P}}$.
1721: \end{definition}
1722: %
1723: In order to define the abstract domain of interpretations, we need the
1724: following definitions.
1725: %
1726: \begin{definition}[Instance Operator]
1727: \label{foinstopdef}
1728: Given an interpretation $I$ and a signature $\Sigma\in\SigP$,
1729: we define the operator $\instS$ as follows:
1730: $$ \InstS{I}=\{\calA\theta\st\calA\in I,\ \theta\ \hbox{substitution over}\
1731: \Sigma\}\ldotp $$
1732: \end{definition}
1733: %
1734: \begin{definition}[Upward-closure Operator]
1735: \label{foupclosdef}
1736: Given an interpretation $I$ and a signature $\Sigma\in\SigP$,
1737: we define the operator $\upS$ as follows:
1738: $$ \UpS{I}=\{\calA+\calC\st\calA\in I,\ \calC\ \hbox{fact over}\ \Sigma\}\ldotp $$
1739: \end{definition}
1740: %
1741: \begin{remark}\rm
1742: Note that, as usual,
1743: in the previous definitions we assume the substitution
1744: $\theta$ and the fact $\calC$ to be defined over the signature $\Sigma$.
1745: \end{remark}
1746: %
1747: The following definition provides the connection between the (abstract)
1748: interpretations defined in Definition \ref{foainterpdef} and the (concrete)
1749: interpretations of Definition \ref{fointerpdef}. The idea behind the
1750: definition is that an interpretation implicitly {\em denotes}
1751: the set of elements
1752: which can be obtained by either {\em instantiating}
1753: or {\em closing upwards} elements in the
1754: interpretation itself (where the concepts of instantiation and upward-closure
1755: are made precise by the above definitions). The operation of instantiation
1756: is related to the notion of C-semantics \cite{FLMP93} (see Definition
1757: \ref{foopsemdef}), while the operation of upward-closure is justified by
1758: Proposition \ref{foaffine}. Note that the operations of
1759: instantiation and upward-closure are performed for every possible
1760: signature $\Sigma\in\SigP$.
1761: %
1762: \begin{definition}[Denotation of an Interpretation]
1763: \label{fodenotdef}
1764: Given an (abstract) interpretation $I$, its denotation $\den{I}$
1765: is the (concrete) interpretation $\Fam{\den{I}}$ defined as follows:
1766: $$ \den{I}_\Sigma\eqdef\InstS{\UpS{I}}\ \ \
1767: (\hbox{or,\ equivalently,}\ \den{I}_\Sigma\eqdef\UpS{\InstS{I}}). $$
1768: Two interpretations $I$ and $J$ are said to be equivalent, written
1769: $I\iequiv J$, if and only if $\den{I}=\den{J}$.
1770: \end{definition}
1771: %
1772: The equivalence of the two different equations in Definition \ref{fodenotdef}
1773: is stated in the following proposition.
1774: %
1775: \begin{proposition}
1776: For every interpretation $I$, and signature $\Sigma\in\SigP$,
1777: $$ \InstS{\UpS{I}}=\UpS{\InstS{I}}. $$
1778: \end{proposition}
1779: %
1780: \begin{proof}
1781: Let $(\calA+\calC)\theta\in\InstS{\UpS{I}}$, with $\calA\in I$. Then
1782: $(\calA+\calC)\theta=(\calA\theta)+\calC\theta\in\UpS{\InstS{I}}$.
1783: Conversely, let $\calA\theta+\calC\in\UpS{\InstS{I}}$, with $\calA\in I$.
1784: Let $\calB$ be a variant of $\calC$ with new variables (not appearing in
1785: $\calA$, $\theta$, and $\calC$) and $\theta'$ be the substitution with
1786: domain $\Dom{\theta}\Union\fvar{\calB}$ and s.t.
1787: $\restr{\theta'}{\Dom{\theta}}=\theta$ and
1788: $\theta'$ maps $\calB$ to $\calC$. Then
1789: $\calA\theta+\calC=\calA\theta'+\calB\theta'=(\calA+\calB)\theta'\in
1790: \InstS{\UpS{I}}$.
1791: \end{proof}
1792: %
1793: We are now ready to define the symbolic interpretation domain. In the following
1794: we will use the word {\em abstract} to stress the connection between our symbolic
1795: semantics and the theory of {\em abstract interpretation}.
1796: Our abstraction does not loose precision but it allows us to finitely represent
1797: infinite collections of formulas.
1798: As previously mentioned, the idea is that of considering interpretations as implicitly
1799: defining the sets of elements contained in their denotations. Therefore,
1800: differently from Definition \ref{fodomaindef}, now we need to check containment between
1801: {\em denotations}. Furthermore,
1802: as we do not need to distinguish between interpretations having the same
1803: denotation, we simply identify them using equivalence classes with respect
1804: to the corresponding equivalence relation $\iequiv$.
1805: %
1806: \begin{definition}[Abstract Interpretation Domain]
1807: \label{foadomaindef}
1808: Abstract interpretations form
1809: a complete lattice $\couple{\calI}{\asubseteq}$, where
1810: \begin{itemize}
1811: \item $\calI=\{\iclass{I}\st I\ \hbox{is an interpretation}\}$;
1812: \item $\iclass{I}\asubseteq\iclass{J}$ if and only if $\den{I}\subseteq\den{J}$;
1813: \item the least upper bound of $\iclass{I}$ and $\iclass{J}$,
1814: written $\alub{\iclass{I}}{\iclass{J}}$, is $\iclass{I\Union J}$;
1815: \item the bottom and top elements are
1816: $\iclass{\eset}$ and $\iclass{\Eps}$, respectively.
1817: \end{itemize}
1818: \end{definition}
1819: %
1820: The following proposition provides an {\em effective} and equivalent condition
1821: for testing the $\asubseteq$ relation (which we call {\em entailment} relation)
1822: over interpretations. We will need this result later on.
1823: %
1824: \begin{proposition}[Entailment between Interpretations]
1825: \label{foasubseteqprop}
1826: Given two interpretations $I$ and $J$, $\den{I}\subseteq\den{J}$ if and only if
1827: for every $\calA\in I$, there exist $\calB\in J$, a substitution
1828: $\theta$, and a fact $\calC$ (defined over $\SigmaP$) s.t.
1829: $\calA=\calB\theta+\calC$.
1830: \end{proposition}
1831: %
1832: \begin{proof}
1833: {\em If part}. We prove that for every $\Sigma\in\SigP$,
1834: $\den{I}_\Sigma\subseteq\den{J}_\Sigma$.
1835: Let $\calA'=\calA\theta'+\calC'\in\UpS{\InstS{I}}=\den{I}_\Sigma$,
1836: with $\calA\in I$ and
1837: $\theta'$, $\calC'$ defined over $\Sigma$.
1838: By hypothesis, there exist $\calB\in J$, a substitution
1839: $\theta$, and a fact $\calC$ (defined over $\SigmaP$) s.t.
1840: $\calA=\calB\theta+\calC$.
1841: Therefore, $\calA'=\calA\theta'+\calC'=(\calB\theta+\calC)\theta'+\calC'=
1842: \calB\theta\theta'+(\calC\theta'+\calC')\in\UpS{\InstS{J}}=\den{J}_\Sigma$
1843: (note that $\theta\theta'$ and $\calC\theta'+\calC'$ are both defined over
1844: $\Sigma$ because $\SigmaP\subseteq\Sigma$).
1845: \medskip\\
1846: {\em Only if part}.
1847: Let $\calA\in I$, then $\calA\in\den{I}_\SigmaP$ (note that
1848: $\calA$ is defined over $\SigmaP$ by definition of interpretation).
1849: Then, by the hypothesis we have that
1850: $\calA\in\den{J}_\SigmaP=\Up{\SigmaP}{\Inst{\SigmaP}{J}}$, i.e.,
1851: there exist $\calB\in J$, a substitution $\theta$, and a fact $\calC$
1852: (defined over $\SigmaP$) s.t. $\calA=\calB\theta+\calC$.
1853: \end{proof}
1854: %
1855: We now define the abstract
1856: satisfiability judgment $\avalS{I}{\Delta}{\calC}{\theta}$, where
1857: $I$ is an {\em input} interpretation, $\Delta$ is an {\em input} context, $\calC$ is an
1858: {\em output} fact, and $\theta$ is an {\em output} substitution.
1859: %
1860: \begin{remark}\rm
1861: \label{asatexportremark}
1862: As usual, the notation $\avalS{I}{\Delta}{\calC}{\theta}$ requires that
1863: $\Delta$, $\calC$, and $\theta$ are defined over the signature $\Sigma$. As a consequence,
1864: the newly introduced constant $c$ in the $\forall$-case of the $\asatS$
1865: definition below {\em cannot be exported} through the output parameters
1866: $\calC$ or $\theta$.
1867: \end{remark}
1868: %
1869: The judgment $\asatS$ can be thought of as an abstract version of the
1870: judgment $\satS$ (compare Definition \ref{satjdef}).
1871: We now need one more parameter, namely an {\em output}
1872: substitution. The idea behind the definition is that the output fact
1873: $\calC$ and the output substitution $\theta$ are {\em minimal}
1874: (in a sense to be clarified) so that they can be computed effectively given
1875: a program $P$, an interpretation $I$, and a signature $\Sigma$. The output
1876: substitution $\theta$ is needed in order
1877: to deal with clause instantiation, and its
1878: minimality is ensured by using most general unifiers in the definition.
1879: As the reader can note, the sources of non-effectiveness which are present
1880: in Definition \ref{satjdef} (e.g., in the rule for $\all$))
1881: are removed in Definition \ref{foasatdef} below.
1882: We recall that the notation $\theta_1\slub\theta_2$ denotes the least upper
1883: bound of substitutions (see Appendix \ref{prelimsec}).
1884: %
1885: \begin{definition}[Abstract Satisfiability Judgment]
1886: \label{foasatdef}
1887: Let $P$ be an \LOf program, $I$ an interpretation, and
1888: $\Sigma\in\SigP$. The abstract
1889: satisfiability judgment $\asatS$ is defined as follows:
1890: $$\begin{array}{l}
1891: \avalS{I}{\all,\Delta}{\Eps}{nil};\\
1892: [\medskipamount]
1893: \avalS{I}{\calA}{\calC}{\theta}\ \hbox{if there exist}\ \calB\in I\
1894: \hbox{(variant)},\ \calB'\submult\calB,\ \calA'\submult\calA,\
1895: \card{\calB'}=\card{\calA'},\\
1896: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \calC=\calB\diff\calB',\ \hbox{and}\ \
1897: \theta=\restr{\Mmgu{\calB'}{\calA'}}{\fvar{\calA,\calC}};\\
1898: [\medskipamount]
1899: \avalS{I}{\foralx{G},\Delta}{\calC}{\theta}\ \hbox{if}\
1900: \aval{I}{\Sigma,c}{G[c/x],\Delta}{\calC}{\theta},
1901: \ \hbox{with}\ c\not\in\Sigma
1902: \ \hbox{{\rm (}see Remark \ref{asatexportremark}{\rm )}};\\
1903: [\medskipamount]
1904: \avalS{I}{G_1\with G_2,\Delta}{\calC}{\theta}\ \hbox{if}\
1905: \avalS{I}{G_1,\Delta}{\calC_1}{\theta_1},\
1906: \avalS{I}{G_2,\Delta}{\calC_2}{\theta_2},\\
1907: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
1908: \calD_1\submult\calC_1,\ \calD_2\submult\calC_2,\
1909: \card{\calD_1}=\card{\calD_2},\ \theta_3=\Mmgu{\calD_1}{\calD_2},\\
1910: \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
1911: \calC=\calC_1+(\calC_2\diff\calD_2),\ \hbox{and}\ \
1912: \theta=\restr{(\theta_1\slub\theta_2\slub\theta_3)}
1913: {\fvar{G_1,G_2,\Delta,\calC}};\\
1914: [\medskipamount]
1915: \avalS{I}{G_1\para G_2,\Delta}{\calC}{\theta}\ \hbox{if}\
1916: \avalS{I}{G_1,G_2,\Delta}{\calC}{\theta};\\
1917: [\medskipamount]
1918: \avalS{I}{\anti,\Delta}{\calC}{\theta}\ \hbox{if}\
1919: \avalS{I}{\Delta}{\calC}{\theta}\ldotp
1920: \end{array}$$
1921: \end{definition}
1922: %
1923: We recall that two multisets in general may have more than one
1924: (not necessarily equivalent) most general unifier
1925: and that using the notation $\Mmgu{\calB'}{\calA'}$ we mean any
1926: unifier which is {\em non-deterministically} picked from the set of most
1927: general unifiers of $\calB'$ and $\calA'$ (see Appendix
1928: \ref{prelimsec}).
1929: %
1930: \begin{example}
1931: \label{foasatex}
1932: Let us consider a signature with a function symbol $f$ and predicate symbols
1933: $p,q,r,s$. Let $\calV$ be a denumerable set of variables, and
1934: $u,v,w,\ldots\in\calV$.
1935: Let $I$ be the interpretation consisting of the two multisets
1936: $\{p(x),q(x)\}$ and $\{r(y),p(f(y))\}$
1937: (for simplicity, hereafter we omit brackets in
1938: multiset notation), and $P$ the program
1939: %
1940: $$\begin{array}{l}
1941: 1\ldotp\ \ r(w)\lollo q(f(w))\\
1942: [\smallskipamount]
1943: 2\ldotp\ \ s(z)\lollo\foralx{p(f(x))}\\
1944: [\smallskipamount]
1945: 3\ldotp\ \ \anti\lollo q(u)\with r(v)\\
1946: \end{array}$$
1947: %
1948: Let us consider (a renaming of) the body of the first clause, $q(f(w'))$,
1949: and (a renaming of) the first element in $I$, $p(x'),q(x')$.
1950: Using the second case for the
1951: $\asat{\SigmaP}$ judgment, with $\calA=\calA'=q(f(w'))$,
1952: $\calB=p(x'),q(x')$, $\calB'=q(x')$, we get
1953: $$ \aval{I}{\SigmaP}{q(f(w'))}{p(x')}{[\substbind{x'}{f(w')}]}\ldotp $$
1954: %
1955: Let us consider now (a renaming of)
1956: the body of the second case, $\foralx{p(f(x))}$,
1957: and another renaming of the first element, $p(x''),q(x'')$.
1958: From the $\forall$-case of the definition of $\asat{\SigmaP}$,
1959: $\aval{I}{\SigmaP}{\foralx{p(f(x))}}{\calC}{\theta}$ if
1960: $\aval{I}{\SigmaP,c}{p(f(c))}{\calC}{\theta}$, with $c\not\in\SigmaP$.
1961: Now, we can apply the second case for $\asat{\SigmaP,c}$. Unfortunately,
1962: we can't choose $\calA'$ to be $p(f(c))$ and $\calB'$ to be $p(x'')$. In fact,
1963: by unifying $p(f(c))$ with $p(x'')$, we should get the substitution
1964: $\theta=[\substbind{x''}{f(c)}]$
1965: and the output fact $q(x'')$ (note that $x''$ is a free
1966: variable in the output fact)
1967: and this is not allowed because the substitution $\theta$ must be defined on
1968: $\SigmaP$, in order for $\aval{I}{\SigmaP}{\foralx{p(f(x))}}{\calC}{\theta}$
1969: to be meaningful. It turns out that the only way to use the second clause for
1970: $\asat{\SigmaP,c}$ is to choose $\calA'=\calB'=\Eps$, which is useless in
1971: the fixpoint computation (see Example \ref{foSPex}).
1972: Finally, let us consider (a renaming of)
1973: the body of the third clause, $\anti\lollo q(u')\with r(v')$.
1974: According to the $\with$-rule for the $\asat{\SigmaP}$ judgment, we must
1975: first compute $\calC_1$, $\calC_2$, $\theta_1$ and $\theta_2$ such that
1976: $\aval{I}{\SigmaP}{q(u')}{\calC_1}{\theta_1}$ and
1977: $\aval{I}{\SigmaP}{r(v')}{\calC_2}{\theta_2}$.
1978: To this aim, take two variants of the multisets in $I$,
1979: $p(x'''),q(x''')$ and $r(y'),p(f(y'))$.
1980: Proceeding as above, we get that
1981: $$ \aval{I}{\SigmaP}{q(u')}{p(x''')}{[\substbind{u'}{x'''}]} \ \
1982: \hbox{and}\ \ \aval{I}{\SigmaP}{r(v')}{p(f(y'))}{[\substbind{v'}{y'}]}\ldotp $$
1983: Now, we can apply the $\with$-rule for the $\asat{\SigmaP}$ judgment,
1984: with $\calD_1=p(x''')$, $\calD_2=p(f(y'))$, and
1985: $\theta_3=[\substbind{x'''}{f(y')}]$.
1986: We have that $\theta_1\slub\theta_2\slub\theta_3=[\substbind{u'}{f(y')},
1987: \substbind{v'}{y'},\substbind{x'''}{f(y')}]$.
1988: Therefore, we get that
1989: $$ \aval{I}{\SigmaP}{q(u')\with r(v')}{p(x''')}{[\substbind{u'}{f(y')},
1990: \substbind{v'}{y'},\substbind{x'''}{f(y')}]}\ldotp $$
1991: \end{example}
1992: %
1993: The following lemma states a simple property of the substitution domain,
1994: which we will need in the following.
1995: \begin{lemma}
1996: \label{fodomainlemma}
1997: For every interpretation $I$, context $\Delta$, fact $\calC$, and substitution
1998: $\theta$, if $\avalS{I}{\Delta}{\calC}{\theta}$ then
1999: $\Dom{\theta}\subseteq\fvar{\Delta}\Union\fvar{\calC}$.
2000: \end{lemma}
2001: %
2002: \begin{proof}
2003: Immediate by induction on the definition of $\asatS$.
2004: \end{proof}
2005: %
2006: The connection between the satisfiability judgments $\satS$ and $\asatS$ is
2007: clarified by the following lemma (in the following we denote
2008: by $\supmult$ the converse of the sub-multiset relation, i.e.,
2009: $\calA\supmult\calB$ if and only if $\calB\submult\calA$).
2010: %
2011: \begin{lemma}
2012: \label{fovalavalrellemma}
2013: For every interpretation $I$, context $\Delta$, fact $\calC$, and substitution
2014: $\theta$,
2015: \begin{enumerate}
2016: \item if $\avalS{I}{\Delta}{\calC}{\theta}$ then
2017: $\valS{\den{I}}{\Delta\theta\theta'}{\calC'\theta'}$ for every substitution
2018: $\theta'$ and fact $\calC'\supmult\calC\theta$;
2019: \item if $\valS{\den{I}}{\Delta\theta}{\calC}$ then there exist a fact
2020: $\calC'$, and substitutions $\theta'$ and $\sigma$ s.t.
2021: $\avalS{I}{\Delta}{\calC'}{\theta'}$,
2022: $\restr{\theta}{\fvar{\Delta}}=
2023: \restr{(\compos{\theta'}{\sigma})}{\fvar{\Delta}}$,
2024: $\calC'\theta'\sigma\submult\calC$.
2025: \end{enumerate}
2026: \end{lemma}
2027: %
2028: \begin{proof}
2029: See Appendix \ref{proofsapp}.
2030: \end{proof}
2031: %
2032: The satisfiability judgment $\asatS$ also satisfies the following properties.
2033: \begin{lemma}
2034: \label{foavallemma}
2035: For any interpretations $I_1$, $I_2$, \ldots,
2036: context $\Delta$, fact $\calC$, and substitution $\theta$,
2037: \begin{enumerate}
2038: \item if $I_1\asubseteq I_2$ and $\avalS{I_1}{\Delta}{\calC}{\theta}$
2039: then there exist a fact $\calC'$, and substitutions $\theta'$ and $\sigma$
2040: s.t. $\avalS{I_2}{\Delta}{\calC'}{\theta'}$,
2041: $\restr{\theta}{\fvar{\Delta}}=
2042: \restr{(\compos{\theta'}{\sigma})}{\fvar{\Delta}}$,
2043: $\calC'\theta'\sigma\submult\calC\theta$;\smallskip
2044: \item if $I_1\asubseteq I_2\asubseteq\ldots$ and
2045: $\avalS{\aUn{i}{\Inf}I_i}{\Delta}{\calC}{\theta}$
2046: then there exist $k\in\Nat$, a fact $\calC'$, and substitutions
2047: $\theta'$ and $\sigma$ s.t.
2048: $\avalS{I_k}{\Delta}{\calC'}{\theta'}$,
2049: $\restr{\theta}{\fvar{\Delta}}=
2050: \restr{(\compos{\theta'}{\sigma})}{\fvar{\Delta}}$,
2051: $\calC'\theta'\sigma\submult\calC\theta$.
2052: \end{enumerate}
2053: \end{lemma}
2054: %
2055: \begin{proof}
2056: See Appendix \ref{proofsapp}.
2057: \end{proof}
2058: %
2059: We are now ready to define the abstract fixpoint operator
2060: $\SP:\calI\rightarrow\calI$.
2061: We will proceed in two steps. We will first define an operator working over
2062: interpretations (i.e., elements of $\Part{\hb{}{P}}$).
2063: With a little bit of overloading, we will call
2064: the operator with the same name, i.e., $\SP$.
2065: This operator should satisfy the equation
2066: $\den{\SP(I)}=\Tp(\den{I})$ for every interpretation $I$.
2067: This property ensures soundness and completeness of the
2068: {\em symbolic} representation.
2069:
2070: After defining the operator over $\Part{\hb{}{P}}$,
2071: we will lift it to our abstract domain $\calI$ consisting
2072: of the equivalence classes of elements of $\Part{\hb{}{P}}$ w.r.t.
2073: the relation $\iequiv$ defined in Definition \ref{fodenotdef}.
2074: Formally, we first introduce the following definition.
2075: %
2076: \begin{definition}[Symbolic Fixpoint Operator {\boldmath $\SP$}]
2077: \label{fosymfixopdef}
2078: Given an \LOf
2079: program $P$ and an interpretation $I$, the symbolic fixpoint operator
2080: $\SP$ is defined as follows:
2081: $$
2082: \begin{array}{l}
2083: \SP(I)\eqdef\{(\ms{H}+\calC)\,\theta\st
2084: (H\lollo G)\in\vrn{P},\
2085: \aval{I}{\SigmaP}{G}{\calC}{\theta}\}\ldotp\\
2086: \end{array}
2087: $$
2088: \end{definition}
2089: %
2090: Note that the $\SP$ operator is defined using the
2091: judgment $\asat{\SigmaP}$.
2092:
2093: Proposition \ref{fotpspprop} states that $\SP$ is sound and complete
2094: w.r.t $\Tp$. In order to prove this, we need to formulate Lemma
2095: \ref{fotpsplemma} below.
2096: %
2097: \paragraph*{Notation}
2098: Let $P$ be an \LOf program,
2099: and $\Sigma,\Sigma_1\in\SigP$ be two signatures such that
2100: $\Sigma_1\subseteq\Sigma$. Given a fact $\calC$, defined on $\Sigma$,
2101: we use $\Til{\calC}{\Sigma}{\Sigma_1}$
2102: to denote any fact which is obtained in the following way. For every constant
2103: (eigenvariable) $c\in(\Sigma\diff\Sigma_1)$, pick a new variable in $\calV$
2104: (not appearing in $\calC$), let it be $x_c$ (distinct variables must be
2105: chosen for distinct eigenvariables). Now, $\Til{\calC}{\Sigma}{\Sigma_1}$
2106: is obtained by
2107: $\calC$ by replacing every $c\in(\Sigma\diff\Sigma_1)$ with $x_c$.
2108: For instance, if $\calC=\{p(x,f(c)),q(y,d)\}$,
2109: with $c\in(\Sigma\diff\Sigma_1)$ and $d\in\Sigma_1$, we have that
2110: $\Til{\calC}{\Sigma}{\Sigma_1}=\{p(x,f(x_c)),q(y,d)\}$.
2111:
2112: Given a context (multiset of goals) $\Delta$, defined on $\Sigma$,
2113: we define $\Til{\Delta}{\Sigma}{\Sigma_1}$ in the same way.
2114: Similarly, given a substitution $\theta$, defined on $\Sigma$, we use the
2115: notation $\Til{\theta}{\Sigma}{\Sigma_1}$
2116: to denote the substitution obtained from $\theta$
2117: by replacing every $c\in(\Sigma\diff\Sigma_1)$ with a new variable $x_c$
2118: in every binding of $\theta$.
2119: For instance, if $\theta=[\substbind{u}{p(x,f(c))},\substbind{v}{q(y,d)}]$,
2120: with $c\in(\Sigma\diff\Sigma_1)$ and $d\in\Sigma_1$, we have that
2121: $\Til{\theta}{\Sigma}{\Sigma_1}=
2122: [\substbind{u}{p(x,f(x_c))},\substbind{v}{q(y,d)}]$.
2123:
2124: Using the notation
2125: $\val{\den{I}}{\Sigma_1}{\Til{\Delta}{\Sigma}{\Sigma_1}}
2126: {\Til{\calC}{\Sigma}{\Sigma_1}}$ we mean the judgment obtained
2127: by replacing every $c\in(\Sigma\diff\Sigma_1)$ with $x_c$ simultaneously
2128: in $\Delta$ and $\calC$. Newly introduced variables must not appear in
2129: $\Delta$, $\calC$, or $I$.
2130:
2131: When $\Sigma$ and $\Sigma_1$ are clear from the context, we simply write
2132: $\til{\calC}$, $\til{\Delta}$, and $\til{\theta}$ for
2133: $\Til{\calC}{\Sigma}{\Sigma_1}$, $\Til{\Delta}{\Sigma}{\Sigma_1}$, and
2134: $\Til{\theta}{\Sigma}{\Sigma_1}$.
2135:
2136: Finally, we use $\Xis{\Sigma_1}{\Sigma}$ (or simply $\xis$ if it is not
2137: ambiguous) to denote the substitution which maps every
2138: variable $x_c$ back to $c$ (for every $c\in(\Sigma\diff\Sigma_1)$),
2139: i.e., consisting of all bindings of
2140: the form $\substbind{x_c}{c}$ for every $c\in\Sigma\diff\Sigma_1$.
2141: Clearly, we have that $\til{F}\xis=F$, for
2142: any fact or context $F$, and
2143: $\compos{\til{\theta}}{\xis}=\theta$ for any substitution $\theta$.
2144:
2145: Note that, by definition,
2146: $\Til{\calC}{\Sigma}{\Sigma_1}$ and $\Til{\Delta}{\Sigma}{\Sigma_1}$
2147: are defined on $\Sigma_1$, while $\Xis{\Sigma_1}{\Sigma}$ is defined on
2148: $\Sigma$.
2149:
2150: \begin{lemma}
2151: \label{fotpsplemma}
2152: Let $P$ be an \LOf program, $I$ an interpretation,
2153: and $\Sigma,\Sigma_1\in\SigP$ two signatures, with $\Sigma_1\subseteq\Sigma$.
2154: \begin{enumerate}
2155: \item If $\aval{I}{\Sigma_1}{\Delta}{\calC}{\theta}$ then
2156: $\avalS{I}{\Delta}{\calC}{\theta}$;
2157: \item If $\valS{\den{I}}{\Delta}{\calC}$ then
2158: $\val{\den{I}}{\Sigma_1}{\Til{\Delta}{\Sigma}{\Sigma_1}}
2159: {\Til{\calC}{\Sigma}{\Sigma_1}}$.
2160: \end{enumerate}
2161: \end{lemma}
2162: %
2163: \begin{proof}
2164: See Appendix \ref{proofsapp}.
2165: \end{proof}
2166: %
2167: \begin{proposition}
2168: \label{fotpspprop}
2169: For every \LOf program $P$ and interpretation $I$,
2170: $\den{\SP(I)}=\Tp(\den{I})$.
2171: \end{proposition}
2172: %
2173: \begin{proof}
2174: $\den{\SP(I)}\subseteq\Tp(\den{I})$.
2175: \vsep
2176: We prove that for every $\Sigma\in\SigP$,
2177: $\den{\SP(I)}_\Sigma\subseteq\Tp(\den{I})_\Sigma$.
2178: Assume $(\ms{H}+\calC)\theta\in\SP(I)$, with $H\lollo G$ a variant of a clause
2179: in $P$ and $\aval{I}{\SigmaP}{G}{\calC}{\theta}$. Assume also that
2180: $\calA=((\ms{H}+\calC)\theta+\calD)\theta'\in\InstS{\UpS{\SP(I)}}=
2181: \den{Sp(I)}_\Sigma$.
2182: We have that $\aval{I}{\SigmaP}{G}{\calC}{\theta}$ implies
2183: $\avalS{I}{G}{\calC}{\theta}$ by item $i$ of Lemma \ref{fotpsplemma} (remember that
2184: $\SigmaP\subseteq\Sigma$).
2185: Therefore, by item $i$ of Lemma \ref{fovalavalrellemma}, we get
2186: $\val{\den{I}}{\Sigma}{G\theta\theta'}{\calC'\theta'}$ for any fact
2187: $\calC'\supmult\calC\theta$. Taking $\calC'=\calC\theta+\calD$, it follows that
2188: $\val{\den{I}}{\Sigma}{G\theta\theta'}{\calC\theta\theta'+\calD\theta'}$.
2189: Therefore, by definition of $\Tp$, we have
2190: $\ms{H}\theta\theta'+\calC\theta\theta'+\calD\theta'\in(\Tp(\den{I}))_\Sigma$,
2191: i.e., $\calA\in(\Tp(\den{I}))_\Sigma$.
2192: %
2193: \vsep
2194: $\Tp(\den{I})\subseteq\den{\SP(I)}$.
2195: \vsep
2196: We prove that for every $\Sigma\in\SigP$,
2197: $Tp(\den{I})_\Sigma\subseteq\den{\SP(I)}_\Sigma$.
2198: Assume $\calA\in(\Tp(\den{I}))_\Sigma$. By definition of $\Tp$,
2199: there exist a variant of a clause $H\lollo G$ in $P$,
2200: a fact $\calC$ and a substitution $\theta$ (defined over $\Sigma$) s.t.
2201: $\calA=\ms{H}\theta+\calC$ and $\val{\den{I}}{\Sigma}{G\theta}{\calC}$.
2202: \vsep
2203: By item $ii$ of Lemma \ref{fotpsplemma}
2204: we have that $\valS{\den{I}}{G\theta}{\calC}$
2205: implies $\val{\den{I}}{\SigmaP}{\til{G\theta}}{\til{\calC}}$
2206: (hereafter, we use the notation $\til{\cdot}$ for
2207: $\Til{\cdot}{\Sigma}{\SigmaP}$).
2208: From $H\lollo G$ in $P$, we know that $G$ is defined on $\SigmaP$. It follows
2209: easily that $\til{G\theta}=G\til{\theta}$, so that
2210: $\val{\den{I}}{\SigmaP}{G\til{\theta}}{\til{\calC}}$.
2211: By item $ii$ of Lemma \ref{fovalavalrellemma}, there exist a fact $\calC'$, and
2212: substitutions $\theta'$ and $\sigma$ (defined over $\SigmaP$) s.t.
2213: $\aval{I}{\SigmaP}{G}{\calC'}{\theta'}$,
2214: $\restr{\til{\theta}}{\fvar{G}}=\restr{(\compos{\theta'}{\sigma})}{\fvar{G}}$,
2215: and $\calC'\theta'\sigma\submult\til{\calC}$.
2216: \vsep
2217: By definition of $\SP$, we have $(\ms{H}+\calC')\theta'\in\SP(I)$.
2218: \vsep
2219: Now, $\calA=\ms{H}\theta+\calC=\ms{H}\til{\theta}\xis+\til{\calC}\xis=$
2220: (note that by hypothesis $\compos{\theta'}{\sigma}$ and $\til{\theta}$ coincide
2221: for variables in $G$, and are not defined on variables in $H$ which do not
2222: appear in $G$ because $H\lollo G$ is a variant)
2223: $\ms{H}\theta'\sigma\xis+\til{\calC}\xis\supmult$
2224: $\ms{H}\theta'\sigma\xis+\calC'\theta'\sigma\xis=$
2225: $((\ms{H}+\calC')\theta')\sigma\xis\in$
2226: $\den{(\ms{H}+\calC')\theta'}_\Sigma\subseteq\den{\SP(I)}_\Sigma$.
2227: \end{proof}
2228: %
2229: The following corollary holds.
2230: %
2231: \begin{corollary}
2232: \label{equivcor}
2233: For every \LOf
2234: program $P$ and interpretations $I$ and $J$, if $I\iequiv J$ then
2235: $\SP(I)\iequiv\SP(J)$.
2236: \end{corollary}
2237: %
2238: \begin{proof}
2239: If $I\iequiv J$, i.e., $\den{I}=\den{J}$, we have that
2240: $\Tp(\den{I})=\Tp(\den{J})$.
2241: By Proposition \ref{fotpspprop}, it follows that
2242: $\den{\SP(I)}=\den{\SP(J)}$, i.e., $\SP(I)\iequiv\SP(J)$.
2243: \end{proof}
2244: %
2245: Corollary \ref{equivcor} allows us to safely lift the definition of $\SP$
2246: from the lattice $\couple{\Part{\hb{}{P}}}{\subseteq}$ to
2247: $\couple{\calI}{\asubseteq}$. Formally, we define the abstract fixpoint
2248: operator as follows.
2249: %
2250: \begin{definition}[Abstract Fixpoint Operator {\boldmath $\SP$}]
2251: Given an \LOf program $P$ and an equivalence class $\iclass{I}$ of $\calI$,
2252: the abstract fixpoint operator $\SP$ is defined as follows:
2253: $$ \SP(\iclass{I})\eqdef\iclass{\SP(I)} $$
2254: where $\SP(I)$ is defined in Definition \ref{fosymfixopdef}.
2255: \end{definition}
2256: %
2257: For the sake of simplicity,
2258: in the following we will often use $I$ to denote its class $\iclass{I}$,
2259: and we will simply use the term {\em (abstract) interpretation} to refer to
2260: an equivalence class, i.e., an element of $\calI$.
2261: The abstract fixpoint operator $\SP$ satisfies the following property.
2262: %
2263: \begin{proposition}[Monotonicity and Continuity]
2264: For every \LOf program $P$, the abstract fixpoint operator $\SP$ is
2265: mon\-o\-ton\-ic and continuous over the lattice $\couple{\calI}{\asubseteq}$.
2266: \end{proposition}
2267: %
2268: \begin{proof}
2269: {\em Monotonicity}.
2270: \nl
2271: We prove that if $I\asubseteq J$, then $\SP(I)\asubseteq\SP(J)$, i.e.,
2272: $\den{\SP(I)}\subseteq\den{\SP(J)}$.
2273: To prove the latter condition, we will use the characterization given
2274: by Proposition \ref{foasubseteqprop}.
2275: Assume $\calA=(\ms{H}+\calC)\theta\in\SP(I)$, with $H\lollo G$ a variant of a
2276: clause in $P$ and $\aval{I}{\SigmaP}{G}{\calC}{\theta}$.
2277: \vsep
2278: By item $i$ of Lemma \ref{foavallemma},
2279: there exist a fact $\calC'$, and substitutions $\theta'$ and $\sigma$
2280: (note that they are defined over $\SigmaP$)
2281: s.t. $\aval{J}{\SigmaP}{G}{\calC'}{\theta'}$,
2282: $\restr{\theta}{\fvar{G}}=\restr{(\compos{\theta'}{\sigma})}{\fvar{G}}$,
2283: $\calC'\theta'\sigma\submult\calC\theta$.
2284: Let $\calC\theta=\calC'\theta'\sigma+\calD$, with $\calD$ a fact defined
2285: over $\SigmaP$.
2286: By definition of $\SP$, $\calB=(\ms{H}+\calC')\theta'\in\SP(J)$.
2287: \vsep
2288: Now, $\calA=(\ms{H}+\calC)\theta=\ms{H}\theta+\calC\theta=
2289: \ms{H}\theta'\sigma+\calC'\theta'\sigma+\calD$ (note in fact that by
2290: hypothesis $\theta'\sigma$ and $\theta$ coincide for variables in $G$, and
2291: are not defined on variables in $H$ which do not appear in $G$ because
2292: $H\lollo G$ is a variant).
2293: Therefore, we have that
2294: $\calA=\ms{H}\theta'\sigma+\calC'\theta'\sigma+\calD=\calB\sigma+\calD$.
2295: \vsep
2296: {\em Continuity}.
2297: \nl
2298: We show that $\SP$ is finitary, i.e.,
2299: if $I_1\asubseteq I_2\asubseteq\ldots$, then
2300: $\SP(\aUn{i}{\Inf}I_i)$ $\asubseteq$ $\aUn{i}{\Inf}\SP(I_i)$, i.e.,
2301: $\den{\SP(\aUn{i}{\Inf}I_i)}\subseteq\den{\aUn{i}{\Inf}\SP(I_i)}$.
2302: Again, we will use the characterization given
2303: by Proposition \ref{foasubseteqprop}.
2304: Assume $\calA=(\ms{H}+\calC)\theta\in\SP(\aUn{i}{\Inf}I_i)$, with
2305: $H\lollo G$ a variant of a
2306: clause in $P$ and $\aval{\aUn{i}{\Inf}I_1}{\SigmaP}{G}{\calC}{\theta}$.
2307: \vsep
2308: By item $ii$ of Lemma \ref{foavallemma}, there exist $k\in\Nat$,
2309: a fact $\calC'$, and substitutions $\theta'$ and $\sigma$
2310: (note that they are defined over $\SigmaP$)
2311: s.t. $\aval{I_k}{\SigmaP}{G}{\calC'}{\theta'}$,
2312: $\restr{\theta}{\fvar{G}}=\restr{(\compos{\theta'}{\sigma})}{\fvar{G}}$,
2313: $\calC'\theta'\sigma\submult\calC\theta$.
2314: Let $\calC\theta=\calC'\theta'\sigma+\calD$, with $\calD$ a fact defined
2315: over $\SigmaP$.
2316: By definition of $\SP$, $\calB=(\ms{H}+\calC')\theta'\in\SP(I_k)$.
2317: \vsep
2318: Exactly as above, we prove that
2319: $\calA=(\ms{H}+\calC)\theta=\ms{H}\theta'\sigma+\calC'\theta'\sigma+\calD=
2320: \calB\sigma+\calD$.
2321: \end{proof}
2322: %
2323: \begin{corollary}
2324: \label{fofixpoint_equivalence}
2325: For every \LOf program $P$, $\den{\lfp{\SP}}=\lfp{\Tp}$.
2326: \end{corollary}
2327: %
2328: Let $\SymbF{P}=\lfp{\SP}$, then we have the following main theorem.
2329: %
2330: \begin{theorem}[Soundness and Completeness]
2331: For every \LOf program $P$, $\osP$ $=$ $\fsP$ $=$ $\den{\SymbF{P}}_\SigmaP$.
2332: \end{theorem}
2333: %
2334: \begin{proof}
2335: From Theorem \ref{fofixpoint_operational} and Corollary
2336: \ref{fofixpoint_equivalence}.
2337: \end{proof}
2338: %
2339: The previous results give us an algorithm to compute the operational and
2340: fixpoint semantics of a program $P$ via the fixpoint operator $\SP$.
2341: %
2342: \begin{example}
2343: \label{foSPex}
2344: Let us consider a signature with a constant symbol $a$,
2345: a function symbol $f$ and predicate symbols
2346: $p,q,r,s$. Let $\calV$ be a denumerable set of variables, and
2347: $u,v,w,\ldots\in\calV$.
2348: Let us consider the program $P$ given below.
2349: %
2350: $$\begin{array}{l}
2351: 1\ldotp\ \ r(w)\lollo q(f(w))\\
2352: [\smallskipamount]
2353: 2\ldotp\ \ s(z)\lollo\foralx{p(f(x))}\\
2354: [\smallskipamount]
2355: 3\ldotp\ \ \anti\lollo q(u)\with r(v)\\
2356: [\smallskipamount]
2357: 4\ldotp\ \ p(x)\para q(x)\lollo\all\\
2358: \end{array}$$
2359: %
2360: From clause 4, and using the first rule for $\asat{\SigmaP}$, we
2361: get $\SP(\eset)=\iclass{\{\{p(x),q(x)\}\}}$. For simplicity, we omit the
2362: class notation, and we write
2363: $$ \isp{1}=\SP(\eset)=\{\{p(x),q(x)\}\}\ldotp $$
2364: We can now apply the remaining clauses to the element
2365: $I=\{p(x),q(x)\}$ (remember that $\SP(\iclass{I})=\iclass{\SP(I)}$).
2366: From the first clause (see Example \ref{foasatex}) we have
2367: $\aval{I}{\SigmaP}{q(f(w'))}{p(x')}{[\substbind{x'}{f(w')}]}$.
2368: It follows that $(r(w'),p(x'))[\substbind{x'}{f(w')}]=
2369: r(w'),p(f(w'))\in\isp{2}$. As the reader can verify (see discussion
2370: in Example \ref{foasatex}), clause 2 does not yield any further element,
2371: and the same holds for clause 3, therefore (changing $w'$ into
2372: $y$ for convenience)
2373: $$ \isp{2}=\{\{p(x),q(x)\},\{r(y),p(f(y))\}\}\ldotp $$
2374: %
2375: Now, we can apply clause 3 to the elements in $\isp{2}$. According
2376: to Example \ref{foasatex}, we have that $
2377: \aval{I}{\SigmaP}{q(u')\with
2378: r(v')}{p(x''')}{[\substbind{u'}{f(y')},
2379: \substbind{v'}{y'},\substbind{x'''}{f(y')}]}. $
2380: Therefore we get that $(p(x'''))[\substbind{u'}{f(y')},
2381: \substbind{v'}{y'},\substbind{x'''}{f(y')}]=p(f(y'))\in\isp{3}$.
2382: Clause 2 cannot be applied yet, for the same reasons as above.
2383: Also, note that the element $r(y),p(f(y))$ is now subsumed by $p(f(y'))$.
2384: Therefore we can assume
2385: $$ \isp{3}=\{\{p(x),q(x)\},\{p(f(y'))\}\}\ldotp $$
2386: %
2387: Finally, we can apply clause 2 to $\isp{3}$, using the
2388: $\forall$-rule for the $\asat{\SigmaP}$ judgment.
2389: Take $c\not\in\SigmaP$, and consider a renaming of the last element in
2390: $\isp{3}$, $p(f(y''))$. Consider (a renaming of) clause 2,
2391: $s(z')\lollo\foralx{p(f(x))}$. We have that
2392: $\aval{I}{\SigmaP,c}{p(f(c))}{\Eps}{nil}$, with $nil$ being the empty
2393: substitution. Therefore we get that
2394: $\aval{I}{\SigmaP}{\foralx{p(f(x))}}{\Eps}{nil}$, from which
2395: $s(z')\in\isp{4}$.
2396: The reader can verify that no further clauses can be applied and
2397: that $\isp{4}$ is indeed the fixpoint of $\SP$, therefore we have that
2398: $$ \isp{4}=\isp{\omega}=\{\{p(x),q(x)\},\{p(f(y'))\},\{s(z')\}\}\ldotp $$
2399: Note that $F(P)$ is defined to be $\den{\lfp{\SP}}_\SigmaP$, therefore
2400: it includes, e.g., the elements
2401: $s(a)$ (see Example \ref{lofex}), $p(f(f(y'')))$ and $p(f(f(y''))),q(x'')$.
2402: \end{example}
2403: %
2404: \sectionl{Ensuring Termination}{foterminatsec}
2405: %
2406: In general the symbolic fixpoint semantics of first order LO programs is not
2407: computable (see also the results in \cite{CDLMS99}).
2408: In fact, the use of first order terms can easily lead to LO programs that
2409: encode operations over natural numbers.
2410: In this section, however,
2411: we will isolate a fragment of \LOf for which termination of the
2412: bottom-up evaluation algorithm presented in Section \ref{foeffectivesec}
2413: is guaranteed. An application of these results will be presented in Section
2414: \ref{examplessec}.
2415: %
2416: First of all, we will introduce some preliminary notions that we will use later on to
2417: prove the decidability of our fragment.
2418:
2419: \subsection{The Theory of Well Quasi-Orderings}
2420: \label{theoryWQO}
2421: %
2422: In the following we summarize some basic definitions and results on the
2423: theory of {\em well quasi-orderings} \cite{Hig52,Mil85,ACJT96}.
2424: A {\em quasi-order} $\sqsubseteq$
2425: on a set $A$ is a binary relation over $A$ which is reflexive and transitive.
2426: In the following it will be denoted $(A,\sqsubseteq)$.
2427: %
2428: \begin{definition}[Well Quasi-Ordering]\rm
2429: \label{wqodef}
2430: A quasi-order $(A,\sqsubseteq)$
2431: is a {\em well quasi-ordering} (wqo) if for each
2432: infinite sequence $a_0~a_1~a_2~\ldots$ of elements in $A$ there exist indices
2433: $i<j$ such that $a_j\sqsubseteq a_i$.\footnote{Note that our $\sqsubseteq$ operator
2434: corresponds to the $\sqsupseteq$ operator of \cite{AJ01a}.
2435: Here we adhere to the classical logic programming convention.}
2436:
2437: \end{definition}
2438: %
2439: We have the following results, according to which
2440: a hierarchy of well quasi-orderings can be built starting from known ones.
2441: In the following $\widehat{r}$ will denote the set $\{1,\ldots,r\}$, $r$ being a natural number,
2442: and $|w|$ the length of a string $w$.
2443: %
2444: \begin{proposition}[From \cite{Hig52}]\rm
2445: \label{wqoresults}
2446: %
2447: \begin{enumerate}
2448: \item If $A$ is a finite set, then $(A,=)$ is a wqo;
2449:
2450: \item let $(A,\sqsubseteq)$ be a wqo, and let $A^s$ denote the set of
2451: finite multisets over $A$. Then, $(A^s,\entailSet)$ is a
2452: wqo, where $\entailSet$ is the quasi-order on $A^s$ defined as follows:
2453: given $S=\{a_1,\ldots,a_n\}$ and $S'=\{b_1,\ldots,b_r\}$,
2454: $S'\entailSet S$ if and only if there exists an {\em injection}
2455: $h:\widehat{n}\rightarrow\widehat{r}$ such that
2456: $b_{h(j)}\sqsubseteq a_j$ for $1\leq j\leq n$;
2457:
2458: \item let $(A,\sqsubseteq)$ be a wqo, and let $A^*$ denote the set
2459: of finite strings over $A$. Then, $(A^*,\sqsubseteq^*)$ is a wqo, where
2460: $\sqsubseteq^*$ is the quasi-order on $A^*$ defined in the following way:
2461: $w'\sqsubseteq^*w$ if and only if there exists a strictly monotone (meaning that
2462: $j_1<j_2$ if and only if $h(j_1)<h(j_2)$) {\em injection}
2463: $h:\widehat{|w|}\rightarrow\widehat{|w'|}$ such that
2464: $w'(h(j))\sqsubseteq w(j)$ for $1\leq j\leq |w|$.
2465: \end{enumerate}
2466: \end{proposition}
2467: %
2468: We are ready now to study the class of monadic \LOf specifications.
2469:
2470: \subsection{Monadic \LOf Specifications}
2471: The class of specifications we are interested in consists of {\em monadic} predicates
2472: without function symbols.
2473: Intuitively, in this class we can represent process that carry along a single
2474: information taken from a possibly infinite domain (universal quantification
2475: introduces fresh names during a derivation).
2476: %
2477: \begin{definition}[Monadic \LOf Specifications]
2478: \label{separablespecdef}
2479: The class of monadic \LOf specifications
2480: consists of \LOf programs built over a signature $\Sigma$
2481: including a {\em finite} set of constant symbols $\calL$,
2482: no function symbols, and
2483: a {\em finite} set of predicate symbols $\calP$
2484: with arity at most {\em one}.
2485: \end{definition}
2486: %
2487: \begin{definition}[Monadic Multisets and Interpretations]
2488: \label{separablemultdef}
2489: The class of monadic multisets
2490: consists of multisets of (non ground) atomic formulas
2491: over a signature $\Sigma$ including a {\em finite} set of constant symbols
2492: $\calL$, no function symbols, and a {\em finite} set of
2493: predicate symbols $\calP$ with arity at most {\em one}.
2494: An interpretation consisting of monadic
2495: multisets is called a {\em monadic interpretation}.
2496: \end{definition}
2497: %
2498: \begin{example}
2499: Let $\Sigma$ be a signature including a constant symbols $a$, no
2500: function symbols, and predicate symbols $p$, $q$ and $r$
2501: (with arity one), and $s$ (with arity zero).
2502: Let $\calV$ be a denumerable set of variables, and
2503: $x,y,\ldots\in\calV$. Then the clause
2504: $$
2505: p(x)\para q(x)\para r(x)\para s\lollo(p(x)\para p(a))\with
2506: \forall v_{.}r(v)
2507: $$
2508: is a monadic \LOf specification, and the multiset
2509: $\{p(x),q(y),q(x),s\}$ is a monadic multiset.
2510: \end{example}
2511: %
2512: We have the following result.
2513: %
2514: \begin{proposition}
2515: \label{MMnFOclosedprop}
2516: The class of monadic multisets is closed under applications of $\SP$, i.e.,
2517: for every interpretation $I$, if $I$ is monadic then $\SP(I)$ is monadic.
2518: \end{proposition}
2519: %
2520: \begin{proof}
2521: Immediate by Definition \ref{fosymfixopdef} and Definition
2522: \ref{foasatdef}.
2523: \end{proof}
2524: %
2525: Following Proposition \ref{foasubseteqprop}, we define the {\em entailment}
2526: relation between multisets of (non ground) atomic formulas, denoted
2527: $\entailm$, as follows.
2528: %
2529: For the sake of simplicity, in the rest of this section we will apply the following
2530: convention.
2531: Consider a monadic multiset.
2532: First of all, we can eliminate constant symbols by
2533: performing the following transformation (note that there are no other
2534: ground terms other than constants in this class).
2535: For every atom $p(a)$, where $p$ is a predicate symbol with arity one and
2536: $a$ is a constant symbol in $\Sigma$, we
2537: introduce a new predicate symbol
2538: with arity zero, let it be $p_a$, and we transform the original multiset
2539: by substituting $p_a$ in place of $p(a)$.
2540: The resulting set of predicate symbols is still finite
2541: (note that the set of constant and predicate symbols of the program is finite).
2542: It is easy to see that entailment between multisets transformed in the
2543: above way is a {\em sufficient} condition for entailment of the original
2544: multisets (note that the condition is not {\em necessary}, e.g., I cannot
2545: recognize that $p(a)$ entails $p(x)$).
2546:
2547: Without loss of generality, we assume hereafter to deal with a set of
2548: predicate symbols with arity {\em one} (if it is not the case, we can complete
2549: predicate with arity less than one with {\em dummy} variables)
2550: and without constant symbols (otherwise, we operate the transformation
2551: previously described).
2552: \begin{definition}
2553: \label{MCentail}
2554: Given two multisets $\calA$ and $\calB$,
2555: $\calA\entailm\calB$ if and only if there exist a substitution $\theta$ and a multiset
2556: $\calC$ such that $\calA=\calB\theta+\calC$.
2557: \end{definition}
2558: %
2559: Then, we have the following property.
2560: \begin{proposition}
2561: \label{MCentailissound}
2562: If $\calA\entailm\calB$ then $\den{\calA}\subseteq\den{\calB}$.
2563: \end{proposition}
2564: %
2565: \begin{proof}
2566: It follows from Definition \ref{fodenotdef} and Proposition \ref{foasubseteqprop}.
2567: \end{proof}
2568: %
2569: Let $\calM$ be a monadic multiset with variables $x_1,\ldots,x_k$.
2570: We define $M_{i}$ as the {\em multiset} of predicate symbols
2571: having $x_i$ as argument in $\calM$, and $S(\calM)$ as the
2572: multiset $\{ M_{1},\ldots, M_{k}\}$. For instance, given the
2573: monadic multiset $\calM$ defined as
2574: $\{p(x_1),q(x_1),p(x_1),q(x_2),r(x_2),q(x_3),r(x_3)\}$,
2575: $S(\calM)$ is the multiset consisting of the elements
2576: $M_1~=~ppq$, $M_2~=~qr$, and $M_3~=~qr$, i.e.,
2577: $S(\calM)=\{ppq,qr,qr\}$ (where $ppq$ denotes the multiset with
2578: two occurrences of $p$ and one of $q$, and so on).
2579: \smallskip\\
2580: Given two multisets of multisets of predicate symbols
2581: $S~=~\{M_1,M_2,\ldots M_k\}$ and $T~=~\{N_1,N_2,\ldots,N_r\}$,
2582: let $S\entailSet T$ if and only if there exists an {\em injective}
2583: mapping $h$ from $\{1,\ldots,r\}$ to $\{1,\ldots,k\}$ such that
2584: $N_{i}\submult M_{h(i)}$ for $i:1,\ldots,r$.
2585: As an example, $\{ppp,tt, qq, rrr\}~\entailSet~\{pp, q, rr\}$ by mapping:
2586: $pp$ into $ppp$ ($pp\submult ppp$),
2587: $q$ into $qq$ ($q\submult qq$), and $rr$ into $rrr$ ($rr\submult rrr$).
2588: On the contrary, $\{ppp,rr,t,qq\}\not\entailSet\{pq,q,rr\}$, in fact
2589: there is no multiset in the set on the left hand side of the previous relation of which $pq$
2590: is a sub-multiset.
2591: \smallskip\\
2592: The following property relates the quasi order $\entailSet$ and the entailment
2593: relation $\entailm$.
2594: \begin{lemma}\label{ent-set}
2595: Let $\calM$ and $\calN$ be two monadic multisets.
2596: Then $S(\calM)\entailSet S(\calN)$ implies $\calM \entailm \calN$.
2597: \end{lemma}
2598: \begin{proof}
2599: Let $S(\calM)~=~\{M_1,M_2,\ldots M_k\}$ and
2600: $S(\calN)~=~\{N_1,N_2,\ldots,N_r\}$.
2601: Furthermore, let $h$ be the injective mapping from $\{1,\ldots,r\}$
2602: to $\{1,\ldots,k\}$ such that $N_{i}\submult M_{h(i)}$.
2603: By construction of $M$ and $N$, it is easy to see that
2604: for every $i\in\{1,\ldots,r\}$ we can isolate atomic formulas
2605: $A_{i1},\ldots,A_{iz}$ in $\calN$ (corresponding to the cluster of
2606: variables $N_i$), where $z$ is the cardinality of $N_i$,
2607: and atomic formulas $B_{i1},\ldots,B_{iz}$ in $\calM$ (corresponding to the
2608: cluster of variables $M_{h(i)}$), such that
2609: the conditions required by Definition \ref{MCentail} are satisfied.
2610: \end{proof}
2611: As an immediate consequence of this lemma, we obtain the following property.
2612: \begin{proposition}
2613: \label{MMnFOwqoprop}
2614: The entailment relation $\entailm$ between monadic multisets
2615: is a well-quasi-ordering.
2616: \end{proposition}
2617: %
2618: \begin{proof}
2619: The conclusion follows from the observations below
2620: (in the following we denote by $\supmult$ the converse of the sub-multiset relation, i.e.,
2621: $\calA\supmult\calB$ if and only if $\calB\submult\calA$):
2622: \begin{itemize}
2623: \item[-] the $\supmult$ relation is a well quasi-ordering by Dickson's Lemma
2624: (which is a consequence of Proposition \ref{wqoresults}, see also \cite{Dic13}). Intuitively,
2625: multiset inclusion
2626: is equivalent to the component-wise ordering of tuples of integers denoting
2627: the occurrences of the finite set of predicate symbols in a multiset;
2628: \item[-] since $\entailSet$ is built over elements ordered with respect to
2629: the well quasi-ordering
2630: $\supmult$, $\entailSet$ is in turn a well quasi-ordering by
2631: item $ii$ of Proposition \ref{wqoresults};
2632: \item[-] as a consequence of Lemma \ref{ent-set}, $\entailSet$ being a well quasi-ordering
2633: implies that $\entailm$ is a well quasi-ordering.
2634: \end{itemize}
2635: \end{proof}
2636: %
2637: We can now formulate the following proposition, which
2638: states that the bottom-up fixpoint semantics is
2639: computable in finite time for monadic \LOf specifications.
2640: This results relies on the following facts: in the case of monadic specifications,
2641: each interpretation computed via bottom-up evaluation consists of monadic multisets, and
2642: the entailment relation between monadic multisets is a well quasi-ordering (therefore
2643: eventually the fixpoint computation stabilizes).
2644: %
2645: \begin{proposition}
2646: \label{PnFOprop}
2647: Let $P$ be a monadic \LOf specification.
2648: Then there exists $k\in\Nat$ such that
2649: $\SymbF{P}$ $=$ $\bigsqcup_{i=0}^k \isp{k}(\eset)$.
2650: \end{proposition}
2651: %
2652: \begin{proof}
2653: We first note that the denotation of a monadic interpretation $I$
2654: is defined in terms of the denotation of its elements (monadic multisets).
2655: Thus, a monadic interpretation $I$ represents an {\em upward closed} set w.r.t. to the ordering
2656: $\entailm$.
2657: Furthermore, the sequence of interpretations computed during a fixpoint computation
2658: forms an increasing sequence with respect to their denotation.
2659: The result follows then from Propositions \ref{MMnFOclosedprop}, \ref{MCentailissound},
2660: \ref{MMnFOwqoprop}, and known results on well quasi-orderings which guarantee that
2661: any infinite increasing sequence of upward-closed sets eventually
2662: stabilizes (see \cite{FS01}).
2663: \end{proof}
2664: %
2665:
2666:
2667: \sectionl{An Example}{examplessec}
2668: %
2669: In this section we show how the bottom-up semantics of
2670: Section \ref{foeffectivesec} can be applied for verifying the
2671: test-and-lock protocol given in Section \ref{testlocksec}.
2672: In order to run the experiments described hereafter, we have built a
2673: prototypical verification tool
2674: implementing the bottom-up fixpoint procedure (backward reachability algorithm)
2675: described in Section \ref{foeffectivesec}.
2676: Following the guidelines and programming style
2677: described in \cite{EP91}, we have implemented an interpreter for the relevant
2678: first order fragment of LO, enriched with the bottom-up evaluation procedure described in Section
2679: \ref{foeffectivesec}. The verification tool has been implemented
2680: in Standard ML.
2681: Let us consider again the test-and-lock protocol given in Section \ref{testlocksec}.
2682: Using our verification tool, we can now automatically
2683: verify the {\em mutual exclusion} property for the
2684: protocol. The specification of unsafe states is simply as follows:
2685: %
2686: $$\begin{array}{l}
2687: 8\ldotp\ \ use(x)\para use(x)\lollo\all
2688: \end{array}$$
2689: %
2690: Note that the test-and-lock specification can be transformed into a {\em monadic} one.
2691: In fact, the second argument can be embedded into the predicate $m$ so as to
2692: define the two predicates $m_{unlocked}$ and $m_{locked}$.
2693: In some sense, the specification is {\em implicitly} monadic since
2694: the second argument is defined over a finite set of states.
2695: Therefore termination of the fixpoint computation is
2696: {\em guaranteed} by Proposition \ref{PnFOprop}.
2697: Running the verification algorithm, we actually find a mutual exclusion violation.
2698: The corresponding trace is shown in Figure \ref{testlockflawfig},
2699: where $bc^{(i^*)}$ denotes multiple applications of clause number $i$.
2700: The problem of the above specification lies in clause 2:
2701: $$
2702: 2\ldotp\ \ init\lollo init\para m(x,unlocked)\\
2703: $$
2704: %
2705: \begin{figure*}[t]
2706: $$
2707: \infer[bc^{(1^*)}]{\dedloPS{init}}
2708: {\infer[bc^{(2^*)}]{\dedloPS{init,think,think}}
2709: {\infer[bc^{(4^*)}]{\dedloPS{init,think,think,m(a,unlocked),m(a,unlocked)}}
2710: {\infer[bc^{(6^*)}]{\dedloPS{init,wait(a),wait(a),m(a,unlocked),
2711: m(a,unlocked)}}
2712: {\infer[bc^{(8)}]{\dedloPS{init,use(a),use(a),m(a,locked),m(a,locked)}}
2713: {\infer[\all_r]{\dedloPS{init,\all,m(a,locked),m(a,locked)}}{}
2714: }}}}}
2715: $$
2716: \captionl{Incorrect test-and-lock protocol: a trace violating mutual exclusion}
2717: {testlockflawfig}
2718: \end{figure*}
2719: %
2720: \begin{figure*}[t]
2721: $$\begin{array}{l}
2722: \{init\}\\
2723: \{use(x),\ use(x)\}\\
2724: \{m(x,unlocked),\ use(x),\ wait(y)\}\\
2725: \{m(x,unlocked),\ use(x),\ use(y),\ m(y,locked)\}\\
2726: \{m(x,locked),\ use(x),\ m(y,unlocked),\ m(y,unlocked),\ think\}\\
2727: \{m(x,unlocked),\ m(x,unlocked),\ wait(y),\ think\}\\
2728: \{m(x,unlocked),\ m(x,unlocked),\ use(y),\ m(y,locked),\ use(z),\
2729: m(z,locked)\}\\
2730: \{m(x,unlocked),\ m(x,unlocked),\ use(y),\ m(y,locked),\ wait(z)\}\\
2731: \{wait(x),\ m(y,unlocked),\ m(y,unlocked),\ wait(z)\}\\
2732: \{m(x,unlocked),\ m(x,unlocked),\ think,\ think\}\\
2733: \{use(x),\ m(x,unlocked),\ think\}
2734: \end{array}$$
2735: \captionl{Fixpoint computed for the incorrect test-and-lock protocol}{testlockincevalfig}
2736: \end{figure*}
2737: %
2738: \begin{figure*}[t]
2739: %pezzo3
2740: $$
2741: \infer[bc^{(1^*)}]{\dedloPS{init}}
2742: {\infer[bc^{({2'}^*)}]{\dedloPS{init,think,think,think}}
2743: {\infer[bc^{(3)}]{\dedloPScd{init,think,think,think,m(c,unlocked),
2744: m(d,unlocked)}}
2745: {\infer[bc^{(4)}]{\dedloPScd{think,think,think,m(c,unlocked),
2746: m(d,unlocked)}}
2747: {\infer[bc^{(4)}]{\dedloPScd{think,think,wait(c),m(c,unlocked),
2748: m(d,unlocked)}}
2749: {\infer[bc^{(4)}]{\dedloPScd{think,wait(d),wait(c),m(c,unlocked),
2750: m(d,unlocked)}}
2751: {\infer[bc^{(6)}]{\dedloPScd{wait(c),wait(d),wait(c),m(c,unlocked),
2752: m(d,unlocked)}}
2753: {\infer[bc^{(7)}]{\dedloPScd{wait(c),wait(d),use(c),m(c,locked),
2754: m(d,unlocked)}}
2755: {\infer[bc^{(6)}]{\dedloPScd{wait(c),wait(d),think,m(c,unlocked),
2756: m(d,unlocked)}}
2757: {\infer*[]{\dedloPScd{use(c),wait(d),think,m(c,locked),
2758: m(d,unlocked)}}
2759: {}}}}}}}}}}
2760: $$
2761: \captionl{A correct version of the test-and-lock protocol: example trace}{testlocktracefig}
2762: \end{figure*}
2763: %
2764: \begin{figure*}[t]
2765: $$\begin{array}{l}
2766: \{use(x),\ use(x)\}\\
2767: \{m(x,unlocked),\ use(x),\ init\}\\
2768: \{m(x,unlocked),\ use(x),\ wait(y)\}\\
2769: \{m(x,unlocked),\ use(x),\ use(y),\ m(y,locked)\}\\
2770: \{m(x,locked),\ use(x),\ m(y,unlocked),\ m(y,unlocked),\ think\}\\
2771: \{m(x,unlocked),\ m(x,unlocked),\ wait(y),\ think\}\\
2772: \{m(x,unlocked),\ m(x,unlocked),\ use(y),\ m(y,locked),\ use(z),\
2773: m(z,locked)\}\\
2774: \{m(x,unlocked),\ m(x,unlocked),\ use(y),\ m(y,locked),\ wait(z)\}\\
2775: \{wait(x),\ m(y,unlocked),\ m(y,unlocked),\ wait(z)\}\\
2776: \{m(x,unlocked),\ m(x,unlocked),\ init\}\\
2777: \{m(x,unlocked),\ m(x,unlocked),\ think,\ think\}\\
2778: \{use(x),\ m(x,unlocked),\ think\}
2779: \end{array}$$
2780: \captionl{Fixpoint computed for the correct test-and-lock protocol}{testlockevalfig}
2781: \end{figure*}
2782: %
2783: \begin{figure*}[t]
2784: $$\begin{array}{l}
2785: \{use(x)\ ,use(x)\}\\
2786: \{m(x,y)\ ,m(x,z)\}\\
2787: \{m(x,unlocked)\ ,use(x)\ ,use(y)\ ,m(y,z)\}\\
2788: \{m(x,unlocked)\ ,use(x)\ ,wait(y)\}\\
2789: \{m(x,unlocked)\ ,use(x)\ ,init\}\\
2790: \{use(x)\ ,m(x,unlocked)\ ,think\}
2791: \end{array}$$
2792: \captionl{Fixpoint computed using invariant strengthening for the
2793: test-and-lock protocol}
2794: {testlockinvarevalfig}
2795: \end{figure*}
2796: %
2797: In fact, using
2798: an (externally quantified) variable $x$ does not prevent the creation of
2799: multiple monitors for the same resource. This causes a violation of mutual
2800: exclusion when different processes are allowed to concurrently access a given
2801: resource by different monitors. Figure \ref{testlockincevalfig}
2802: (where, for readability, we re-use the same variables in
2803: different multisets) also shows
2804: the fixpoint computed for the incorrect version of the protocol: note that the
2805: singleton multiset containing the atom $init$ is in the fixpoint (this amounts
2806: to saying that there exists a state violating mutual exclusion
2807: which is reachable from the initial configuration of the protocol).
2808:
2809: Luckily, we can fix the above problem in a very simple way.
2810: As we do not care about what resource identifiers actually are,
2811: we can elegantly encode them using universal quantification in the body of
2812: clause 2, as follows:
2813: $$
2814: 2'\ldotp\ \ init\lollo init\para\foralx{m(x,unlocked)}
2815: $$
2816: Every time
2817: a resource is created, a new constant, acting as the corresponding identifier,
2818: is created as well. Note that by the operational semantics of universal
2819: quantification, {\em different} resources are assigned {\em different}
2820: identifiers. This clearly prevents the creation of multiple monitors
2821: for the same resource.
2822: An example trace for the modified specification
2823: is shown in Figure \ref{testlocktracefig} (where
2824: $P$ is the program consisting of clauses 1, 2', 3 through 8 (see Section \ref{testlocksec})).
2825:
2826: Now, running again our verification tool on the corrected specification
2827: (termination is still guaranteed by Proposition \ref{PnFOprop}), with
2828: the same set of unsafe states, we get the fixpoint shown in Figure
2829: \ref{testlockevalfig}. The fixpoint contains 12 elements and is reached
2830: in 7 steps. As the fixpoint does not contain $init$, mutual exclusion
2831: is verified, {\em for any number of processes and any number of resources}.
2832:
2833: We conclude by showing how it is possible to optimize the fixpoint computation.
2834: Specifically, we show that it is possible to use the so called
2835: {\em invariant strengthening} technique in order to reduce the dimension of the sets
2836: computed during the fixpoint evaluation. Invariant strengthening consists of enlarging the
2837: theory under consideration with new clauses (e.g., additional clauses
2838: representing further
2839: unsafe states). We remark that this technique is perfectly sound, in the sense that if no
2840: property violations are found in the extended theory, then no violations can be found in the
2841: original one (i.e., proofs in the original theory are still proofs in the extended one).
2842:
2843: One possibility might be to apply the so-called {\em counting abstraction},
2844: i.e., turn the above \LOf specification into a
2845: propositional program (i.e., a Petri net) by abstracting first order atoms into
2846: propositional symbols (e.g., $wait(x)$ into $wait$, and so on),
2847: and compute the structural invariants of the corresponding Petri net.
2848: However, this strategy is not helpful in this case (no meaningful invariant
2849: is found). We can still try some invariants using some {\em ingenuity}.
2850: For instance, consider the following invariant:
2851: $$
2852: 9.\ \ m(x,y)\para m(x,z)\lollo\all
2853: $$
2854: For what we said previously ({\em different} resources
2855: are assigned {\em different} identifiers) this invariant must hold for our
2856: specification. Running the verification tool on this extended specification
2857: we get the fixpoint in Figure \ref{testlockinvarevalfig}, containing only 6
2858: elements and converging in 4 steps.
2859: %
2860: A further optimization could be obtained by adding the invariant
2861: $use(x)\para m(x,unlocked)\lollo\all$ (intuitively, if someone is using a given
2862: resource, the corresponding semaphore cannot be unlocked). In this case the
2863: computation converges immediately at the first step.
2864:
2865: \section{Reachability and Extensions of LO}
2866: \label{reachability}
2867: In this paper we have focused our attention on the relationship between
2868: provability in LO and {\em coverability} for the configuration of a concurrent system.
2869:
2870: Following \cite{BDM02a}, in order to characterize {\em reachability}
2871: problems between two ``configurations'' (goal formulas)
2872: we need an extra feature of linear logic, namely the logical constant $\one$.
2873: Differently from clauses with $\top$, clauses of the form
2874: $A_1\para\ldots\para A_n\lollo\one$ make a
2875: derivation succeed if and only if the right-hand side of the current sequent matches an
2876: instance of $A_1\para\ldots\para A_n$, i.e., all
2877: resources must be used in the corresponding derivation.
2878:
2879: Going back to the notation used in Section \ref{unified},
2880: let $P$ be a set of LO rewrite rules over $\Sigma$ and
2881: $\calV$, and $\calM,\calM'$ two multisets of ground atomic
2882: formulas (two configurations). Furthermore, let $H$, $G$ the
2883: (possibly empty) $\,\para$-disjunctions of ground atomic formulas
2884: such that $\ms{H}=\calM'$ and $\ms{G}=\calM$. Then, the
2885: provability of the sequent $\dedLOo{P,H\lollo\one}{G}$ precisely
2886: characterizes the {\em reachability} of configuration $\calM'$ from the
2887: initial configuration $\calM$ via a sequence of multiset rewriting
2888: steps defined over the theory $P$ (see \cite{BDM02a}).
2889: Again, this is a straightforward consequence of the properties of clauses like
2890: $H\lollo\one$ and of the fact that, when working with LO rewrite rules, derivations
2891: have no branching.
2892: \begin{example}
2893: \label{msrex1}
2894: Let us go back to Example \ref{msrex} of Section \ref{unified}
2895: (compare the definitions of the formulas $F_1$ and $F_2$ given there).
2896: Let $F_1'$ be the formula
2897: $$
2898: p(a)\para p(f(f(b)))\para q(b)\para q(b)\para q(f(f(b)))\lollo \one
2899: $$
2900: and $F_2'$ be the formula
2901: $$
2902: p(a)\para q(b)\lollo \one
2903: $$
2904: and $G=p(a)\para p(b)\para q(f(b))$.
2905: If we enrich $P$ with $F_1'$, instead of $F_1$, then we can transform the partial derivation of
2906: Figure \ref{LOmsr} into an LO proof as shown below
2907: (where $\delta$ stands for the derivation fragment of Figure \ref{LOmsr}):
2908: $$
2909: \infer[bc]{\delta}
2910: {\infer[\one_r]{\dedloPS{\one}}{}}
2911: $$
2912: The resulting LO proof also shows that
2913: from the multiset $\{p(a),p(b),q(f(b))\}$ we can reach the
2914: multiset $\{p(a),p(f(f(b))),q(b),q(b),q(f(f(b)))\}$ after a finite number of rewriting steps
2915: defined in accordance with $P$.
2916: Note that on the contrary (compare with Example \ref{msrex}),
2917: if we enrich $P$ with $F_2'$, it is {\em not}
2918: possible to turn the partial derivation
2919: of Figure \ref{LOmsr} into an LO proof. In fact, every rewriting step will give us
2920: larger and larger multisets and the formula $F_2'$ never becomes applicable.
2921: \end{example}
2922: \begin{figure*}[t]
2923: $$
2924: \infer[bc^{(1)}]{\dedlo{P,D}{\Sigma}{p(f(a)),p(b),q(f(b))}}
2925: {\infer[bc^{(D)}]{\dedlo{P,D}{\Sigma,c}{p(f(a)),p(f(b)),q(b),q(c)}}
2926: {\infer[\one_r]{\dedlo{P,D}{\Sigma,c}{\one}}{}
2927: }
2928: }
2929: $$
2930: \captionl{Reachability as provability in \LOfws}{LOfder}
2931: \end{figure*}
2932: %
2933: Particular attention must be paid to the constants introduced in a derivation.
2934: They cannot be extruded from the scope of the corresponding universal quantifier.
2935: For this reason, the formulas representing {\em target} configurations must be generalized
2936: by introducing universally quantified variables in place of constants introduced in a
2937: derivation.
2938: For the sake of brevity, we will illustrate the connection between provability and
2939: reachability in the extended setting through the following example.
2940: %
2941: \begin{example}\label{msrex2}
2942: Let $\Sigma$ be the signature of Example \ref{msrex}.
2943: Let $P$ consists of the clause
2944: $$
2945: 1\ldotp\ \ p(x)\para q(f(y))\lollo\forall w\ldotp (p(f(x))\para q(y)\para q(w))
2946: $$
2947: Now, let $D$ be the clause $\forall x\ldotp p(f(a))\para p(f(b))\para q(b)\para q(x)\lollo\one$,
2948: and let $G$ be the goal $p(f(a))\para p(b)\para q(f(b))$.
2949: The universal quantifier is used here to generalize the representation of the target
2950: configuration. In fact, new constants will be introduced and associated to
2951: the predicate $q$ in the derivation of the goal $G$.
2952: As an example, a possible derivation is shown in Figure \ref{LOfder}
2953: (where we have omitted applications of the $\para_r$ rule for simplicity).
2954: %
2955: The last backchaining step in Figure \ref{LOfder} is possible because
2956: of the universal quantifier used in $D$.
2957: It would not be possible to define $D$ as
2958: $p(f(a))\para p(f(b))\para q(b)\para q(c)\lollo\one$.
2959: In fact, the resulting initial sequent would violate the
2960: side condition of the $\forall_r$ proof rule that requires the
2961: freshness of the new constants introduced in a proof.
2962: \end{example}
2963: The extension of the fixpoint semantics presented in this paper to more
2964: general linear logic languages (e.g., languages that include $\one$) is a possible
2965: future direction for our research.
2966: %
2967: \sectionl{Conclusions}{conclusions}
2968: In this paper we have investigated the connections between techniques used
2969: for {\em symbolic model checking} of infinite-state systems \cite{ACJT96,FS01}
2970: and provability in fragments of linear logic \cite{AP90}.
2971: The relationship between the two fields is illustrated in Figure \ref{relfig}.
2972: %
2973: \begin{figure*}[t]
2974: \begin{center}
2975: \begin{tabular}{c|c}
2976: {\bf Infinite State Concurrent Systems} & {\bf Linear Logic Specification}\\
2977: & \\
2978: transition system & LO program and proof system\\
2979: transition & rule instance\\
2980: current state & goal formula\\
2981: initial state & initial goal\\
2982: single final state & axiom with $\one$\\
2983: upward-closed set of states & axiom with $\top$\\
2984: reachability & provability\\
2985: $\Pre$ operator & $\Tp$ operator\\
2986: $\Pres$ operator & $\lfp{\Tp}$\\
2987: \end{tabular}
2988: \end{center}
2989: \captionl{Reachability versus provability}{relfig}
2990: \end{figure*}
2991: %
2992: From our point of view, linear logic can be used as a unifying
2993: framework for reasoning about concurrent systems (e.g., Petri Nets,
2994: multiset rewriting, and so on). In \cite{BDM02a}, we have applied
2995: algorithms previously developed for Petri Nets in order to derive
2996: bottom-up evaluation strategies for proposition linear logic.
2997: Conversely, in the current paper we have shown that the use of linear
2998: logic and the related bottom-up evaluation strategies can have
2999: interesting application for the automated verification of
3000: infinite-state systems in which processes are described via {\em
3001: colored} formulas. Several applications of the ideas presented in
3002: this paper can be found in \cite{Boz02}, and \cite{BD02a}.
3003:
3004: Apart from verification purposes, the new fixpoint semantics can also
3005: be useful to study new applications of linear logic programming (e.g.,
3006: for active databases as discussed in \cite{HW98}). For this purpose,
3007: it might be interesting to extend the bottom-up evaluation framework
3008: to richer linear logic languages. Possible directions of research include
3009: languages with a richer set of connectives (e.g., Linlog \cite{And92}),
3010: or languages with more powerful type theories (e.g., LLF \cite{CP02}).
3011: %
3012: \subsection*{Acknowledgments}
3013: %
3014: We would like to thank the anonymous reviewers of the paper
3015: for their helpful comments.
3016:
3017: \appendix
3018:
3019: \sectionl{Some Notations}{prelimsec}
3020: %
3021: \paragraph{Multisets}
3022: A multiset with elements in $D$ is a function $\funct{\calM}{D}{\Nat}$.
3023: If $d\in D$ and $\calM$ is a multiset on $D$, we say
3024: that $d\in\calM$ if and only if $\calM(d)> 0$.
3025: For convenience, we often use the notation for sets
3026: (allowing duplicated elements) to
3027: indicate multisets, when no ambiguity arises from the context. For instance,
3028: $\{a,a,b\}$, where $a,b\in D$, denotes the multiset $\calM$ such that
3029: $\calM(a)=2$, $\calM(b)=1$, and $\calM(d)=0$ for all $d\in D\diff\{a,b\}$.
3030: Sometimes we simply write $a,a,b$ for $\{a,a,b\}$.
3031: Finally, given a set $D$, $\MS{D}$ denotes the set of multisets
3032: with elements in $D$. We define the following operations on multisets.
3033: %
3034: Let $D$ be a set, $\calM_1,\calM_2\in\MS{D}$, and $n\in\Nat$, then:
3035: $\Eps$ is defined s.t.
3036: $\Eps(d)=0$ for all $d\in D$ {\rm ({\em empty multiset})};
3037: $(\calM_1+\calM_2)(d)=\calM_1(d)+\calM_2(d)$ for all $d\in D$
3038: {\rm ({\em union})};
3039: $(\calM_1\diff\calM_2)(d)=max\{0,\calM_1(d)-\calM_2(d)\}$
3040: for all $d\in D$ {\rm ({\em difference})};
3041: $(\calM_1\intersect\calM_2)(d)=min\{\calM_1(d),\calM_2(d)\}$
3042: for all $d\in D$ {\rm ({\em intersection})};
3043: $(n\scalar\calM)(d)=n\calM(d)$ for all $d\in D$
3044: {\rm ({\em scalar product})};
3045: $\calM_1\not=\calM_2$ if and only if there exists $d\in D$ s.t.
3046: $\calM_1(d)\not=\calM_2(d)$ {\rm ({\em comparison})};
3047: $\calM_1\submult\calM_2$ if and only if $\calM_1(d)\leq\calM_2(d)$ for all
3048: $d\in D$ {\rm ({\em inclusion})};
3049: $(\mlub{\calM_1}{\calM_2})(d)=
3050: max\{\calM_1(d),\calM_2(d)\}$ for all $d\in D$
3051: {\rm ({\em merge})};
3052: $\card{\calM_1}=\Sigma_{d\in D}\calM_1(d)$
3053: {\rm ({\em cardinality})}.
3054: %
3055: We use the notation of a formal sum $\SummL{i\in I}{\calM_i}$
3056: to denote the union
3057: of a family of multisets $\calM_i$, with $i\in I$, $I$ being a finite set.
3058: It turns out that $(\MS{D},\submult)$ has the structure of a
3059: lattice (the lattice is complete provided a greatest element is added).
3060: In particular, merge and intersection are, respectively, the least
3061: upper bound and the greatest lower bound operators with respect to the multiset
3062: inclusion operator $\submult$.
3063:
3064: \paragraph{Signatures}
3065: Given a set of formulas $P$, we denote by $\SigmaP$ the signature comprising the set
3066: of constant, function, and predicate symbols in $P$.
3067: We assume to have an infinite set $\calV$ of variable symbols, usually noted
3068: $x$, $y$, $z$, etc. In order to deal with signature augmentation
3069: (due to the presence of universal quantification over goals)
3070: we also need an infinite set $E$ of new constants
3071: (called {\em eigenvariables}). We denote by $\SigP$ the set of
3072: signatures which comprise at least the symbols in $\SigmaP$ (and possibly
3073: some eigenvariables).
3074:
3075: $\TsigmaV$ denotes the set of {\em non ground} terms
3076: over $\Sigma$, i.e., the set of terms built over $\Sigma\cup V$ where $V$
3077: is a denumerable set of variables. (A non ground term {\em may} have free variables;
3078: a {\em ground} term is also {\em non ground}).
3079:
3080: $\AsigmaV$ denotes the set of {\em non ground} atoms over $\Sigma$, i.e., atomic formulas
3081: built over non ground terms over $\Sigma$.
3082:
3083: Multisets of atoms over $\AsigmaV$ are also called {\em facts} throughout the paper, and
3084: usually noted $\calA$, $\calB$, $\calC$, $\ldots$.
3085:
3086:
3087: \paragraph{Substitutions and Multiset Unifiers}
3088: %
3089: We inherit the usual concept of {\em substitution} (mapping from variables
3090: to terms) from traditional logic programming.
3091: We always consider a denumerable set of variables $\calV$, and
3092: substitutions are usually noted $\theta$, $\sigma$, $\tau$, \ldots
3093: We use the notation $[\substbind{x}{t},\ldots]$, where $x$ is a variable
3094: and $t$ is a term, to denote substitution bindings, with $nil$ denoting the
3095: empty substitution.
3096: The application of a substitution $\theta$ to $F$, where
3097: $F$ is a generic expression (e.g., a formula, a term, \ldots) is denoted
3098: by $F\theta$. A substitution $\theta$ is said to be {\em grounding} for
3099: $F$ if $F\theta$ is ground, in this case $F\theta$ is called a
3100: {\em ground instance} of $F$.
3101: Composition of two substitutions $\theta$ and $\sigma$ is
3102: denoted $\compos{\theta}{\sigma}$, e.g., $F(\compos{\theta}{\sigma})$ stands
3103: for $(F\theta)\sigma$. We indicate the domain of a substitution $\theta$
3104: by $\Dom{\theta}$, and we say ``$\theta$ defined on a signature $\Sigma$''
3105: meaning that $\theta$ can only map variables in $\Dom{\theta}$ to terms in
3106: $\TsigmaX{\calV}$.
3107: Substitutions are ordered with respect to the ordering $\leq$
3108: defined in this way: $\theta\leq\tau$ if and only if there exists a
3109: substitution $\sigma$ s.t. $\tau=\compos{\theta}{\sigma}$. If $\theta\leq\tau$,
3110: $\theta$ is said to be {\em more general} than $\tau$; if $\theta\leq\tau$
3111: and $\tau\leq\theta$, $\theta$ and $\tau$ are said to be {\em equivalent}.
3112: Finally, $\fvar{F}$, for an expression $F$,
3113: denotes the set of {\em free} variables of $F$, and
3114: $\restr{\theta}{W}$, where $W\subseteq \calV$, denotes the
3115: {\em restriction} of $\theta$ to $\Dom{\theta}\intersect W$.
3116:
3117: We need the notion of {\em most general unifier} (mgu).
3118: The definition of most
3119: general unifier is somewhat delicate. In particular, different classes of
3120: substitutions (e.g., idempotent substitutions)
3121: have been considered for defining most general unifiers. We refer
3122: the reader to \cite{Ede85,LMM88,Pal90} for a discussion. Most general unifiers
3123: form a complete lattice with respect to the ordering $\leq$, provided a
3124: greatest element is added. For our purposes, we do not choose a particular
3125: class of most general unifiers, we only require the operation of
3126: {\em least upper bound}
3127: of two substitutions w.r.t $\leq$ to be defined and effective.
3128: The least upper bound of $\theta_1$ and $\theta_2$ is indicated
3129: $\theta_1\slub\theta_2$. We refer the reader to \cite{Pal90} for the definition of the
3130: least upper bound. The only property which we use in this paper is that
3131: $\theta_1\leq(\theta_1\slub\theta_2)$ and $\theta_2\leq(\theta_1\slub\theta_2)$,
3132: for any substitutions $\theta_1$ and $\theta_2$.
3133: We assume $\slub$ to be commutative and associative.
3134: %
3135:
3136: We need to lift the definition of {\em most general unifier} from
3137: expressions to multisets of expressions. Namely, given two multisets
3138: $\calA=\{a_1,\ldots,a_n\}$ and $\calB=\{b_1,\ldots,b_n\}$
3139: (note that $\card{\calA}=\card{\calB}$), we define a most
3140: general unifier of $\calA$ and $\calB$, written $\Mmgu{\calA}{\calB}$, to be
3141: the most general unifier (defined in the usual way) of the two vectors of
3142: expressions $\tuple{a_1,\ldots,a_n}$ and $\tuple{b_{i_1},\ldots,b_{i_n}}$,
3143: where $\{i_1,\ldots,i_n\}$ is a permutation of $\{1,\ldots,n\}$.
3144: Depending on the choice of the permutation, in general there is more
3145: than one way to unify two given multisets (the resulting class of mgu in
3146: general will include unifiers which are not equivalent).
3147: We use the notation
3148: $\theta=\Mmgu{\calA}{\calB}$ to denote any unifier which is
3149: {\em non deterministically} picked from the set of most general unifiers of
3150: $\calA$ and $\calB$.
3151:
3152: \sectionl{Proofs of Some Lemmas}{proofsapp}
3153: %
3154: \paragraph{Proof of Lemma \ref{fomovelemma}}
3155: \nl
3156: {\em If part}.
3157: By induction on the derivation of $\valS{I}{\Delta,\calC}{\Eps}$.
3158: \begin{itemize}
3159: \item[-] If $\Delta=\all,\Delta'$, obvious;
3160: \item[-] if $\Delta=\calA$ and $\calA+\calC\in I_\Sigma$, then also
3161: $\valS{I}{\calA}{\calC}$ holds;
3162: \item[-] if $\Delta=\foralx{G},\Delta'$ and
3163: $\val{I}{\Sigma,c}{G[c/x],\Delta',\calC}{\Eps}$, with $c\not\in\Sigma$,
3164: then by the inductive
3165: hypothesis $\val{I}{\Sigma,c}{G[c/x],\Delta'}{\calC}$, which implies
3166: $\valS{I}{\foralx{G},\Delta'}{\calC}$;
3167: \item[-] if $\Delta=G_1\with G_2,\Delta'$,
3168: $\valS{I}{G_1,\Delta',\calC}{\Eps}$ and
3169: $\valS{I}{G_2,\Delta',\calC}{\Eps}$,
3170: by the inductive hypothesis $\valS{I}{G_1,\Delta'}{\calC}$ and
3171: $\valS{I}{G_2,\Delta'}{\calC}$, which implies
3172: $\valS{I}{G_1\with G_2,\Delta'}{\calC}$;
3173: \item[-] if $\Delta=G_1\para G_2,\Delta'$ or $\Delta=\anti,\Delta'$,
3174: the conclusion follows by a
3175: straightforward application of the inductive hypothesis.
3176: \end{itemize}
3177: {\em Only if part}.
3178: By induction on the derivation of $\valS{I}{\Delta}{\calC}$.
3179: \begin{itemize}
3180: \item[-] If $\Delta=\all,\Delta'$, obvious;
3181: \item[-] if $\Delta=\calA$ and $\calA+\calC\in I_\Sigma$, then also
3182: $\valS{I}{\calA,\calC}{\Eps}$ holds;
3183: \item[-] if $\Delta=\foralx{G},\Delta'$ and
3184: $\val{I}{\Sigma,c}{G[c/x],\Delta'}{\calC}$, with $c\not\in\Sigma$,
3185: then by the inductive
3186: hypothesis $\val{I}{\Sigma,c}{G[c/x],\Delta',\calC}{\Eps}$, which implies
3187: $\valS{I}{\foralx{G},\Delta',\calC}{\Eps}$;
3188: \item[-] if $\Delta=G_1\with G_2,\Delta'$,
3189: $\valS{I}{G_1,\Delta'}{\calC}$ and $\valS{I}{G_2,\Delta'}{\calC}$,
3190: by the inductive hypothesis $\valS{I}{G_1,\Delta',\calC}{\Eps}$ and
3191: $\valS{I}{G_2,\Delta',\calC}{\Eps}$, which implies
3192: $\valS{I}{G_1\with G_2,\Delta',\calC}{\Eps}$;
3193: \item[-] if $\Delta=G_1\para G_2,\Delta'$ or $\Delta=\anti,\Delta'$,
3194: the conclusion follows by a
3195: straightforward application of the inductive hypothesis.
3196: \end{itemize}
3197:
3198: \paragraph{Proof of Lemma \ref{fovallemma}}
3199: %
3200: \begin{enumerate}
3201: \item By induction on the derivation of $\valS{I_1}{\Delta}{\calC}$.
3202: \begin{itemize}
3203: \item[-] If $\Delta=\all,\Delta'$, obvious;
3204: \item[-] if $\Delta=\calA$ and $\calA+\calC\in (I_1)_\Sigma$,
3205: then $\calA+\calC\in (I_2)_\Sigma$, because $I_1\subseteq I_2$,
3206: therefore $\valS{I_2}{\calA}{\calC}$;
3207: \item[-] if $\Delta=\foralx{G},\Delta'$ and
3208: $\val{I_1}{\Sigma,c}{G[c/x],\Delta'}{\calC}$, with $c\not\in\Sigma$,
3209: then by the inductive hypothesis
3210: $\val{I_2}{\Sigma,c}{G[c/x],\Delta'}{\calC}$, which implies
3211: $\valS{I_2}{\foralx{G},\Delta'}{\calC}$;
3212: \item[-] if $\Delta=G_1\with G_2,\Delta'$,
3213: $\valS{I_1}{G_1,\Delta'}{\calC}$ and $\valS{I_1}{G_2,\Delta'}{\calC}$,
3214: by the inductive hypothesis
3215: $\valS{I_2}{G_1,\Delta'}{\calC}$ and $\valS{I_2}{G_2,\Delta'}{\calC}$,
3216: which implies $\valS{I_2}{G_1\with G_2,\Delta'}{\calC}$;
3217: \item[-] if $\Delta=G_1\para G_2,\Delta'$ or $\Delta=\anti,\Delta'$,
3218: the conclusion follows by a
3219: straightforward application of the inductive hypothesis.
3220: \end{itemize}
3221: \item By induction on the derivation of
3222: $\valS{\Un{i}{\Inf}I_i}{\Delta}{\calC}$.
3223: \begin{itemize}
3224: \item[-] If $\Delta=\all,\Delta'$, then for every $k\in\Nat$,
3225: $\valS{I_k}{\Delta}{\calC}$;
3226: \item[-] if $\Delta=\calA$ and $\calA+\calC\in(\Un{i}{\Inf}I_i)_\Sigma$,
3227: there exists $k\in\Nat$ s.t.
3228: $\calA+\calC\in(I_k)_\Sigma$, i.e.,
3229: $\valS{I_k}{\calA}{\calC}$;
3230: \item[-] if $\Delta=\foralx{G},\Delta'$ and
3231: $\val{\Un{i}{\Inf}I_i}{\Sigma,c}{G[c/x],\Delta'}{\calC}$,
3232: with $c\not\in\Sigma$,
3233: then by the inductive hypothesis there exists $k\in\Nat$ s.t.
3234: $\val{I_k}{\Sigma,c}{G[c/x],\Delta'}{\calC}$,
3235: therefore $\valS{I_k}{\foralx{G},\Delta'}{\calC}$;
3236: \item[-] if $\Delta=G_1\with G_2,\Delta'$,
3237: $\valS{\Un{i}{\Inf}I_i}{G_1,\Delta'}{\calC}$ and
3238: $\valS{\Un{i}{\Inf}I_i}{G_2,\Delta'}{\calC}$,
3239: by the inductive hypothesis there exist $k_1,k_2\in\Nat$ s.t.
3240: $\valS{I_{k_1}}{G_1,\Delta'}{\calC}$ and
3241: $\valS{I_{k_2}}{G_2,\Delta'}{\calC}$.
3242: By taking $k=max\{k_1,k_2\}$, by $i$ we get
3243: $\valS{I_{k}}{G_1,\Delta'}{\calC}$ and
3244: $\valS{I_{k}}{G_2,\Delta'}{\calC}$, which implies
3245: $\valS{I_{k}}{G_1\with G_2,\Delta'}{\calC}$;
3246: \item[-] if $\Delta=G_1\para G_2,\Delta'$ or $\Delta=\anti,\Delta'$,
3247: the conclusion follows by a
3248: straightforward application of the inductive hypothesis.
3249: \end{itemize}
3250: \end{enumerate}
3251:
3252: \paragraph{Proof of Lemma \ref{fovalavalrellemma}}
3253: %
3254: \begin{enumerate}
3255: \item By induction on the derivation of
3256: $\avalS{I}{\Delta}{\calC}{\theta}$.
3257: \begin{itemize}
3258: \item[-] If $\Delta=\all,\Delta'$, obvious;
3259: \item[-] assume $\Delta=\calA$, with $\calB\in I$ (variant),
3260: $\calB'\submult\calB$, $\calA'\submult\calA$, $\calC=\calB\diff\calB'$,
3261: and $\theta=\restr{\Mmgu{\calB'}{\calA'}}{\fvar{\calA,\calC}}$. We want
3262: to prove that $\valS{\den{I}}{\calA\theta\theta'}{\calC'\theta'}$
3263: for every substitution $\theta'$ and fact $\calC'\supmult\calC\theta$,
3264: i.e., $\calA\theta\theta'+\calC\theta\theta'+\calD\theta'\in
3265: \den{I}_\Sigma$ for every substitution $\theta'$ and
3266: fact $\calD$.
3267: \vsep
3268: Now, $\calA\theta\theta'+\calC\theta\theta'+\calD\theta'=
3269: (\calA\theta+\calC\theta+\calD)\theta'=
3270: (\calA'\theta+(\calA\diff\calA')\theta+(\calB\diff\calB')\theta+\calD)
3271: \theta'=$
3272: (remember that $\calB'\submult\calB$)
3273: $(\calA'\theta+(\calA\diff\calA')\theta+(\calB\theta\diff\calB'\theta)+
3274: \calD)\theta'=$
3275: $\calB\theta\theta'+((\calA\diff\calA')\theta\theta'+\calD\theta')\in
3276: \den{I}_\Sigma$;
3277: \item[-] if $\Delta=\foralx{G},\Delta'$ and
3278: $\aval{I}{\Sigma,c}{G[c/x],\Delta'}{\calC}{\theta}$,
3279: with $c\not\in\Sigma$, then
3280: by the inductive hypothesis we have that
3281: $$
3282: \val{\den{I}}{\Sigma,c}{G[c/x]\theta\theta',\Delta'\theta\theta'}
3283: {\calC'\theta'}
3284: $$
3285: for every substitution $\theta'$ and fact
3286: $\calC'\supmult\calC\theta$ (where $\theta'$ and $\calC'$ are defined
3287: over $\Sigma,c$).
3288: \vsep
3289: Assuming that the variable $x$ is not in the domain
3290: of $\theta\theta'$ (it is always possible to rename the universally
3291: quantified variable $x$ in $\foralx{G}$), we have that
3292: $\val{\den{I}}{\Sigma,c}{G\theta\theta'[c/x],\Delta'\theta\theta'}
3293: {\calC'\theta'}$, and, by definition of the judgment, we get
3294: $\valS{\den{I}}{\foralx{(G\theta\theta')},\Delta'\theta\theta'}
3295: {\calC'\theta'}$, i.e.,
3296: $\valS{\den{I}}{(\foralx{G},\Delta')\theta\theta'}{\calC'\theta'}$,
3297: for every substitution $\theta'$ and fact $\calC'$ defined
3298: over $\Sigma,c$ (and therefore also for every substitution $\theta'$
3299: and fact $\calC'$ defined over $\Sigma$),
3300: with $\calC'\supmult\calC\theta$;
3301: \item[-] assume $\Delta=G_1\with G_2,\Delta'$ and
3302: $\avalS{I}{G_1\with G_2,\Delta'}{\calC}{\theta}$. \\
3303: We need to prove that
3304: $\valS{\den{I}}{(G_1\with G_2,\Delta')\theta\theta'}{\calC'\theta'}$
3305: for every substitution $\theta'$ and fact $\calC'\supmult\calC\theta$,
3306: i.e., that
3307: $\valS{\den{I}}{(G_1\with G_2,\Delta')\theta\theta'}
3308: {\calC\theta\theta'+\calF\theta'}$ for every substitution $\theta'$ and
3309: fact $\calF$.
3310: \vsep
3311: By definition of $\asatS$, we have that
3312: there exist facts $\calC_1'\submult\calC_1$,
3313: $\calC_2'\submult\calC_2$ with $\card{\calC_1'}=\card{\calC_2'}$,
3314: and substitutions $\theta_1,\theta_2,\theta_3$ s.t.
3315: $$
3316: \theta_3=\Mmgu{\calC_1'}{\calC_2'},\ \ \
3317: \calC=\calC_1+(\calC_2\diff\calC_2'),\ \ \
3318: \theta=\restr{(\theta_1\slub\theta_2\slub\theta_3)}
3319: {\fvar{\Delta,\calC}},
3320: $$
3321: $$
3322: \avalS{I}{G_1,\Delta'}{\calC_1}{\theta_1}\hand
3323: \avalS{I}{G_2,\Delta'}{\calC_2}{\theta_2}.
3324: $$
3325: By the inductive hypothesis, we have that
3326: $$\begin{array}{l}
3327: \valS{\den{I}}{(G_1,\Delta')\theta_1\theta_1'}
3328: {\calC_1\theta_1\theta_1'+\calD_1\theta_1'}\hand\\
3329: \valS{\den{I}}{(G_2,\Delta')\theta_2\theta_2'}
3330: {\calC_2\theta_2\theta_2'+\calD_2\theta_2'}
3331: \end{array}$$
3332: for every
3333: substitutions $\theta_1',\theta_2'$ and facts $\calD_1,\calD_2$.
3334: \vsep
3335: By choosing $\calD_1=(\calC_2\diff\calC_2')\theta_1+\calF_1$ and
3336: $\calD_2=(\calC_1\diff\calC_1')\theta_2+\calF_2$, we have,
3337: for every substitutions $\theta_1',\theta_2'$
3338: and facts $\calF_1,\calF_2$,
3339: $$\begin{array}{l}
3340: \valS{\den{I}}{(G_1,\Delta')\theta_1\theta_1'}
3341: {(\calC_1+(\calC_2\diff\calC_2'))\theta_1\theta_1'+
3342: \calF_1\theta_1'},\\
3343: [\smallskipamount]
3344: \valS{\den{I}}{(G_2,\Delta')\theta_2\theta_2'}
3345: {(\calC_2+(\calC_1\diff\calC_1'))\theta_2\theta_2'+
3346: \calF_2\theta_2'}.
3347: \end{array}$$
3348: By definition of $\theta$, we have that there exist substitutions
3349: ${\gamma_1},{\gamma_2},{\gamma_3}$ and $\tau$ s.t.
3350: $$
3351: \tau=\compos{\theta_1}{{\gamma_1}},\ \
3352: \tau=\compos{\theta_2}{{\gamma_2}},\ \
3353: \tau=\compos{\theta_3}{{\gamma_3}},\hand
3354: \theta=\restr{\tau}{\fvar{\Delta,\calC}}.
3355: $$
3356: Now, let $\calF_1$ be a variant of $\calF\theta'$ with new variables,
3357: and define the substitution $\theta_1'$ s.t.
3358: $\Dom{\theta_1'}=
3359: \Dom{\compos{{\gamma_1}}{\theta'}}\Union\fvar{\calF_1}$
3360: (clearly these two latter sets are disjoint),
3361: $\restr{\theta_1'}{\Dom{\compos{{\gamma_1}}{\theta'}}}=
3362: \compos{{\gamma_1}}{\theta'}$ and $\calF_1\theta_1'=\calF\theta'$.
3363: Do the same for $\calF_2$, i.e., let it be another variant of
3364: $\calF\theta'$ with new variables, and define $\theta_2'$ in the same
3365: way, so that $\Dom{\theta_2'}=
3366: \Dom{\compos{{\gamma_2}}{\theta'}}\Union\fvar{\calF_2}$,
3367: $\restr{\theta_2'}{\Dom{\compos{{\gamma_2}}{\theta'}}}=
3368: \compos{{\gamma_2}}{\theta'}$, and $\calF_2\theta_2'=\calF\theta'$.
3369: \vsep
3370: From the definition of $\tau$ it follows that
3371: $(G_1,\Delta')\theta_1\theta_1'=
3372: (G_1,\Delta')\theta_1{\gamma_1}\theta'=(G_1,\Delta')\theta\theta'$,
3373: and similarly $(G_2,\Delta')\theta_2\theta_2'=
3374: (G_2,\Delta')\theta\theta'$.
3375: Also, $(\calC_1+(\calC_2\diff\calC_2'))\theta_1\theta_1'=
3376: \calC\theta_1\theta_1'=\calC\theta\theta'$.
3377: \vsep
3378: We also have that
3379: $(\calC_2+(\calC_1\diff\calC_1'))\theta_2\theta_2'=
3380: (\calC_2+(\calC_1\diff\calC_1'))\theta_2{\gamma_2}\theta'=
3381: (\calC_2+(\calC_1\diff\calC_1'))\tau\theta'=
3382: (\calC_2+(\calC_1\diff\calC_1'))\theta_3{\gamma_3}\theta'=$
3383: (remember that $\calC_1'\submult\calC_1$)
3384: $(\calC_2\theta_3+(\calC_1\theta_3\diff\calC_1'\theta_3))
3385: \gamma_3\theta'=$
3386: (remember that $\theta_3$ is a unifier of
3387: $\calC_1'$ and $\calC_2'$)
3388: $(\calC_2\theta_3+(\calC_1\theta_3\diff\calC_2'\theta_3))
3389: \gamma_3\theta'=$
3390: (note that $\calC_2'\theta_3=\calC_1'\theta_3\submult\calC_1\theta_3$)
3391: $((\calC_2\theta_3+\calC_1\theta_3)\diff\calC_2'\theta_3)
3392: \gamma_3\theta'=$
3393: (note that $\calC_2'\submult\calC_2$)
3394: $(\calC_1\theta_3+(\calC_2\theta_3\diff\calC_2'\theta_3))
3395: \gamma_3\theta'=$
3396: $(\calC_1+(\calC_2\diff\calC_2'))\theta_3{\gamma_3}\theta'=$
3397: $\calC\theta_3{\gamma_3}\theta'=\calC\theta\theta'$.
3398: \vsep
3399: By putting everything together,
3400: the inductive hypotheses become
3401: $\valS{\den{I}}{(G_1,\Delta')\theta\theta'}
3402: {\calC\theta\theta'+\calF\theta'}$ and
3403: $\valS{\den{I}}{(G_2,\Delta')\theta\theta'}
3404: {\calC\theta\theta'+\calF\theta'}$, from which
3405: the thesis follows by definition of $\satS$;
3406: \item[-] if $\Delta=G_1\para G_2,\Delta'$ and
3407: $\avalS{I}{G_1,G_2,\Delta'}{\calC}{\theta}$, then
3408: by the inductive hypothesis we have that
3409: $\valS{\den{I}}{(G_1,G_2,\Delta')\theta\theta'}{\calC'\theta'}$, for
3410: every substitution $\theta'$ and fact $\calC'\supmult\calC\theta$.\\
3411: Therefore,
3412: $\valS{\den{I}}{
3413: G_1\theta\theta',G_2\theta\theta',\Delta'\theta\theta'}
3414: {\calC'\theta'}$, and, by definition of the judgment, we get
3415: $\valS{\den{I}}{(G_1\para G_2,\Delta)\theta\theta'}{\calC'\theta'}$;
3416: \item[-] if $\Delta=\anti,\Delta'$, the conclusion follows by a
3417: straightforward application of the inductive hypothesis.
3418: \end{itemize}
3419: \item By induction on the derivation of
3420: $\valS{\den{I}}{\Delta\theta}{\calC}$.
3421: \begin{itemize}
3422: \item[-] If $\Delta=\all,\Delta'$, take $\calC'=\Eps$, $\theta'=nil$,
3423: and $\sigma=\theta$;
3424: \item[-] assume $\valS{\den{I}}{\calA\theta}{\calC}$ and
3425: $\calA\theta+\calC\in\den{I}_\Sigma=\UpS{\InstS{I}}$. Then there exist
3426: $\calB\in I$, a fact $\calD$, and a substitution $\tau$ (defined on
3427: $\Sigma$) s.t. $\calA\theta+\calC=\calB\tau+\calD$. We can safely
3428: assume, thanks to the substitution $\tau$, that $\calB$ is a
3429: {\em variant} of an element in $I$. Also, we can assume that
3430: $\Dom{\tau}\subseteq\fvar{\calB}$ and
3431: $\Dom{\theta}\intersect\Dom{\tau}=\eset$.
3432: \vsep
3433: Now, take the
3434: substitution $\gamma$ s.t.
3435: $\Dom{\gamma}=(\Dom{\theta}\intersect\fvar{\calA})\Union\Dom{\tau}$,
3436: $$
3437: \restr{\gamma}{\Dom{\theta}\intersect\fvar{\calA}}=
3438: \restr{\theta}{\Dom{\theta}\intersect\fvar{\calA}}\hand
3439: \restr{\gamma}{\Dom{\tau}}=\tau.
3440: $$
3441: We have that
3442: $\calA\gamma+\calC=\calB\gamma+\calD$.
3443: Let $\calA'\submult\calA$ and $\calB'\submult\calB$ be two
3444: {\em maximal} sub-multisets s.t. $\calA'\gamma=\calB'\gamma$,
3445: $\rho=\Mmgu{\calA'}{\calB'}$, and
3446: $\theta'=\restr{\rho}{\fvar{\calA}\Union\fvar{\calB\diff\calB'}}$.
3447: By definition of the $\asatS$ judgment, we have that
3448: $\avalS{I}{\calA}{\calC'}{\theta'}$, where $\calC'=\calB\diff\calB'$.
3449: \vsep
3450: As $\gamma$ is a unifier for $\calA'$,$\calB'$, while
3451: $\rho=\Mmgu{\calA'}{\calB'}$, we have that there exists
3452: a substitution $\sigma$ s.t. $\gamma=\compos{\rho}{\sigma}$.
3453: Therefore, $\restr{\theta}{\fvar{\calA}}=
3454: \restr{\gamma}{\fvar{\calA}}=
3455: \restr{(\compos{\rho}{\sigma})}{\fvar{\calA}}=
3456: \restr{(\compos{\restr{\rho}
3457: {(\fvar{\calA}\Union\fvar{\calB\diff\calB'})}}{\sigma})}{\fvar{\calA}}=
3458: \restr{(\compos{\theta'}{\sigma})}{\fvar{\calA}}$, as required.
3459: \vsep
3460: Furthermore, since $\calA\gamma+\calC=\calB\gamma+\calD$ and
3461: $\calA'\submult\calA$, it follows that
3462: $\calA'\gamma+(\calA\diff\calA')\gamma+\calC=
3463: \calB'\gamma+(\calB\diff\calB')\gamma+\calD$, i.e.,
3464: $(\calA\diff\calA')\gamma+\calC=(\calB\diff\calB')\gamma+\calD$.
3465: By this equality and maximality of $\calA'$ and $\calB'$, we get
3466: that necessarily $(\calB\diff\calB')\gamma\submult\calC$
3467: (otherwise, $(\calB\diff\calB')\gamma$ and
3468: $(\calA\diff\calA')\gamma$ would have elements in common).
3469: Therefore, $\calC'\theta'\sigma=(\calB\diff\calB')\theta'\sigma=
3470: (\calB\diff\calB')\rho\sigma=(\calB\diff\calB')\gamma\submult\calC$,
3471: as required;
3472: \item[-] if $\Delta=\foralx{G},\Delta'$ and
3473: $\val{\den{I}}{\Sigma,c}{(G[c/x],\Delta')\theta}{\calC}$, with
3474: $c\not\in\Sigma$, then by the inductive hypothesis
3475: there exist a fact
3476: $\calC'$, and substitutions $\theta'$ and $\sigma$
3477: (defined over $\Sigma,c$) s.t.
3478: $$
3479: \aval{I}{\Sigma,c}{G[c/x],\Delta'}{\calC'}{\theta'},
3480: $$
3481: $\restr{\theta}{\fvar{G[c/x],\Delta'}}=
3482: \restr{(\compos{\theta'}{\sigma})}{\fvar{G[c/x],\Delta'}}$,
3483: and $\calC'\theta'\sigma\submult\calC$.
3484: By definition of the $\asatS$ judgment, we get that
3485: $$
3486: \avalS{I}{\foralx{G},\Delta'}{\calC'}{\theta'}.
3487: $$
3488: The conclusion follows (remember that we must ensure that
3489: $\calC'$, $\theta'$ and $\sigma$ are
3490: defined over $\Sigma$) by the following crucial observations:
3491: \begin{itemize}
3492: \item[$\cdot$] $\Dom{\theta'}\subseteq(\fvar{G[c/x],\Delta'}\Union\fvar
3493: {\calC'})$ by Lemma \ref{fodomainlemma};
3494: \item[$\cdot$] $\theta'$ does not map variables in $G[c/x],\Delta'$ to
3495: the eigenvariable $c$. In fact we know that $\theta$ does not map
3496: variables in $G[c/x],\Delta'$ to $c$ (by hypothesis) and we know that
3497: $\restr{(\compos{\theta'}{\sigma})}{\fvar{G[c/x],\Delta'}}=
3498: \restr{\theta}{\fvar{G[c/x],\Delta'}}$;
3499: \item[$\cdot$] $\theta'$ does not map variables in $\calC'$ to $c$
3500: and $\calC'$ itself does not contain $c$. In fact we know that
3501: $\calC$ does not contain $c$ (by hypothesis) and also that
3502: $\calC'\theta'\sigma\submult\calC$;
3503: \item[$\cdot$] we can safely assume that $\Dom{\sigma}$ does not
3504: contain variables mapped to $c$. Intuitively, these bindings are
3505: useless. Formally, we can restrict
3506: the domain of $\sigma$ to variables that are not mapped to $c$:
3507: with this restriction, the equalities
3508: $\restr{\theta}{\fvar{G[c/x],\Delta'}}=
3509: \restr{(\compos{\theta'}{\sigma})}{\fvar{G[c/x],\Delta'}}$ and
3510: $\calC'\theta'\sigma\submult\calC$ still hold.
3511: \end{itemize}
3512: \item[-] assume $\Delta=G_1\with G_2,\Delta'$ and
3513: $\valS{\den{I}}{(G_1\with G_2\Delta')\theta}{\calC}$.
3514: We need to prove that
3515: there exist a fact $\calC'$ and substitutions $\theta'$ and $\sigma$
3516: s.t. $\avalS{I}{G_1\with G_2,\Delta'}{\calC'}{\theta'}$,
3517: $\restr{\theta}{\fvar{G_1,G_2,\Delta'}}=
3518: \restr{(\compos{\theta'}{\sigma})}{\fvar{G_1,G_2,\Delta'}}$,
3519: $\calC'\theta'\sigma\submult\calC$.
3520: By definition of $\satS$, we have that
3521: $$
3522: \valS{I}{(G_1,\Delta')\theta}{\calC}\hand
3523: \valS{I}{(G_2,\Delta')\theta}{\calC}.
3524: $$
3525: By the inductive hypothesis, we have that there exist
3526: facts $\calC_1,\calC_2$ and substitutions
3527: $\theta_1,\theta_2$, $\sigma_1,\sigma_2$ s.t.
3528: $$
3529: \avalS{I}{G_1,\Delta'}{\calC_1}{\theta_1}\hand
3530: \avalS{I}{G_2,\Delta'}{\calC_2}{\theta_2},
3531: $$
3532: $\restr{\theta}{\fvar{G_1,\Delta'}}=
3533: \restr{(\compos{\theta_1}{\sigma_1})}{\fvar{G_1,\Delta'}}$,
3534: $\restr{\theta}{\fvar{G_2,\Delta'}}=$
3535: $\restr{(\compos{\theta_2}{\sigma_2})}{\fvar{G_2,\Delta'}}$,
3536: \linebreak
3537: $\calC_1\theta_1\sigma_1\submult\calC$ and
3538: $\calC_2\theta_2\sigma_2\submult\calC$.
3539: \vsep
3540: Now, let $\calD_1\submult\calC_1$ and $\calD_2\submult\calC_2$ s.t.
3541: $\calD_1\theta_1\sigma_1$ = $\calD_2\theta_2\sigma_2$ =
3542: $\calC_1\theta_1\sigma_1\intersect\calC_2\theta_2\sigma_2$.
3543: Let $\tau$ be the substitution
3544: $\restr{(\compos{\theta_1}{\sigma_1})}
3545: {\fvar{G_1,\Delta',\calC_1}}\Union
3546: \restr{(\compos{\theta_2}{\sigma_2})}{\fvar{G_2,\Delta',\calC_2}}$;
3547: $\tau$ is well defined because
3548: $\compos{\theta_1}{\sigma_1}$ and $\compos{\theta_2}{\sigma_2}$
3549: both behave like $\theta$ on variables in
3550: $\fvar{G_1,\Delta'}\intersect\fvar{G_2,\Delta'}$,
3551: and $\calC_1,\calC_2$ do not have variables in common except for
3552: variables in $G_1,G_2,\Delta'$ (note that new variants of elements in
3553: $I$ are chosen every time the judgment $\asatS$ is computed).
3554: \vsep
3555: Now, $\calD_1$ and $\calD_2$ are unified by $\tau$,
3556: because $\calD_1\tau=\calD_1\theta_1\sigma_1=\calD_2\theta_2\sigma_2=
3557: \calD_2\tau$. Therefore, there exists
3558: $\theta_3=\Mmgu{\calD_1}{\calD_2}$ s.t. $\tau\geq\theta_3$
3559: ($\theta_3$ is more general than $\tau$). Also,
3560: $\tau\geq\theta_1\sigma_1\geq\theta_1$ and
3561: $\tau\geq\theta_2\sigma_2\geq\theta_2$. Therefore,
3562: $\tau$ is an upper bound for $\{\theta_1,\theta_2,\theta_3\}$
3563: and there exist
3564: $\theta'=\restr{(\theta_1\slub\theta_2\slub\theta_3)}
3565: {\fvar{G_1,G_2,\Delta',\calC}}$, and a substitution ${\gamma}$ s.t.
3566: $\tau=\compos{\theta'}{{\gamma}}$.
3567: Now we can apply the definition of $\asatS$ (rule for $\with$) and
3568: we get that
3569: $$
3570: \avalS{I}{G_1\with G_2,\Delta'}{\calC'}{\theta'},
3571: $$
3572: where $\calC'=\calC_1+(\calC_2\diff\calD_2)$.
3573: Letting $\sigma={\gamma}$, we can prove the thesis.
3574: \vsep
3575: First of all, since
3576: $\compos{\theta'}{\sigma}=\compos{\theta'}{\gamma}=\tau$, and by
3577: definition of $\tau$, we have that
3578: $\restr{\theta}{\fvar{G_1,G_2,\Delta'}}=
3579: \restr{(\compos{\theta'}{\sigma})}{\fvar{G_1,G_2,\Delta'}}$.
3580: It remains to prove that $\calC'\theta'\sigma\submult\calC$ holds.
3581: Now, we have $\calC'\theta'\sigma$ = $\calC'\tau$ =
3582: $\calC_1\tau+\calC_2\tau\diff\calD_2\tau$ =
3583: $\calC_1\tau+\calC_2\tau\diff\calD_2\theta_2\sigma_2$ =
3584: $\calC_1\tau+\calC_2\tau\diff
3585: (\calC_1\theta_1\sigma_1\intersect\calC_2\theta_2\sigma_2)$ =
3586: $\calC_1\tau+\calC_2\tau\diff(\calC_1\tau\intersect\calC_2\tau)$
3587: $\submult$ $\calC$.
3588: The last passage holds because $\calC_1\tau\submult\calC$ and
3589: $\calC_2\tau\submult\calC$ (by definition of $\tau$ and by the inductive
3590: hypothesis) and relies on the following property of multisets:
3591: $\calA\submult\calD$ and $\calB\submult\calD$ implies
3592: $\calA+\calB\diff(\calA\intersect\calB)\submult\calD$;
3593: \item[-] if $\Delta=G_1\para G_2,\Delta'$ of $\Delta=\anti,\Delta'$,
3594: the conclusion follows by a
3595: straightforward application of the inductive hypothesis.
3596: \end{itemize}
3597: \end{enumerate}
3598:
3599: \paragraph{Proof of Lemma \ref{foavallemma}}
3600: %
3601: \begin{enumerate}
3602: \item Assume $\avalS{I_1}{\Delta}{\calC}{\theta}$ and
3603: $I_1\asubseteq I_2$.
3604: By item $i$ of Lemma \ref{fovalavalrellemma},
3605: $\valS{\den{I_1}}{\Delta\theta}{\calC\theta}$.
3606: By item $i$ of Lemma \ref{fovallemma},
3607: $\valS{\den{I_2}}{\Delta\theta}{\calC\theta}$.
3608: The conclusion then follows from item $ii$ of Lemma \ref{fovalavalrellemma};
3609: \item Assume $\avalS{\aUn{i}{\Inf}I_i}{\Delta}{\calC}{\theta}$ and
3610: $I_1\asubseteq I_2\asubseteq\ldots$.
3611: By item $i$ of Lemma \ref{fovalavalrellemma},
3612: $\valS{\den{\aUn{i}{\Inf}I_i}}{\Delta\theta}{\calC\theta}$, i.e.,
3613: as it can be readily verified from Definition \ref{fodenotdef} and
3614: Definition \ref{foadomaindef},
3615: $\valS{\Un{i}{\Inf}\den{I_i}}{\Delta\theta}{\calC\theta}$.
3616: By item $ii$ of Lemma \ref{fovallemma}, there exists $k\in\Nat$ s.t.
3617: $\valS{\den{I_k}}{\Delta\theta}{\calC\theta}$.
3618: The conclusion then follows from item $ii$ of Lemma \ref{fovalavalrellemma}.
3619: \end{enumerate}
3620:
3621: \paragraph{Proof of Lemma \ref{fotpsplemma}}
3622: %
3623: \begin{enumerate}
3624: \item By simple induction on the derivation of
3625: $\aval{I}{\Sigma_1}{\Delta}{\calC}{\theta}$.
3626: \item By induction on the derivation of $\valS{\den{I}}{\Delta}{\calC}$.
3627: \begin{itemize}
3628: \item[-] If $\valS{\den{I}}{\all,\Delta}{\calC}$, immediate;
3629: \item[-] assume $\valS{\den{I}}{\calA}{\calC}$ and
3630: $\calA+\calC\in\den{I}_\Sigma$. It follows that there exist $\calB\in I$,
3631: a fact $\calD$, and a substitution $\theta$ (defined on $\Sigma$) such that
3632: $\calA+\calC=\calB\theta+\calD$. Note that $\calB$ is defined on $\SigmaP$
3633: by definition of (abstract) interpretation.
3634: \vsep
3635: Now, $\til{\calA}+\til{\calC}=\til{\calA+\calC}=$
3636: $\til{\calB\theta+\calD}=\til{\calB\theta}+\til{\calD}=$
3637: (remember that $\calB$ is defined on $\SigmaP\subseteq\Sigma_1$)
3638: $\calB\til{\theta}+\til{\calD}$.
3639: We can conclude that $\til{\calA}+\til{\calC}\in\den{I}_{\Sigma_1}$
3640: (note that $\calB\in I$ and $\til{\theta}$, $\til{\calD}$ are defined on
3641: $\Sigma_1$), it follows that
3642: $\val{\den{I}}{\Sigma_1}{\til{\calA}}{\til{\calC}}$;
3643: \item[-] assume $\valS{\den{I}}{\foralx{G},\Delta}{\calC}$ and
3644: $\val{\den{I}}{\Sigma,c}{G[c/x],\Delta}{\calC}$, with $c\not\in\Sigma$.
3645: From $\Sigma_1\subseteq\Sigma$ we get $\Sigma_1,c\subseteq\Sigma,c$,
3646: therefore we can apply the inductive hypothesis.
3647: It follows that
3648: $\val{\den{I}}{\Sigma_1,c}{\til{G[c/x],\Delta}}{\til{\calC}}$ if and only if
3649: $\val{\den{I}}{\Sigma_1,c}{\til{G[c/x]},\til{\Delta}}{\til{\calC}}$ if and only if
3650: (remember that $c\not\in\Sigma\diff\Sigma_1$ because $c\not\in\Sigma$)
3651: $\val{\den{I}}{\Sigma_1,c}{\til{G}[c/x],\til{\Delta}}{\til{\calC}}$.
3652: By definition of $\satP$ (remember that $c\not\in\Sigma$ implies
3653: $c\not\in\Sigma_1$), we get
3654: $\val{\den{I}}{\Sigma_1}{\foralx{\til{G}},\til{\Delta}}{\til{\calC}}$ if and only if
3655: $\val{\den{I}}{\Sigma_1}{\til{\foralx{G},\Delta}}{\til{\calC}}$
3656: (we assume $x$ to be disjoint with the variables introduced by the
3657: $\til{\cdot}$ construction);
3658: \item[-] the remaining cases follow by a straightforward application of the
3659: inductive hypothesis.
3660: \end{itemize}
3661: \end{enumerate}
3662:
3663: \bibliographystyle{acmtrans}
3664: \bibliography{biblio}
3665:
3666: \end{document}
3667: