[Flora-commits] flora2/docs flora2.tex,1.126,1.127
Brought to you by:
kifer
Menu
▾
▴
[Flora-commits] flora2/docs flora2.tex,1.126,1.127
|
From: Michael K. <ki...@us...> - 2005-03-26 04:28:48
|
Update of /cvsroot/flora/flora2/docs In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv29989/docs Modified Files: flora2.tex Log Message: cleanup Index: flora2.tex =================================================================== RCS file: /cvsroot/flora/flora2/docs/flora2.tex,v retrieving revision 1.126 retrieving revision 1.127 diff -u -d -r1.126 -r1.127 --- flora2.tex 22 Mar 2005 06:20:56 -0000 1.126 +++ flora2.tex 26 Mar 2005 04:28:38 -0000 1.127 @@ -3284,11 +3284,10 @@ group(X)}. Variables in HiLog can range over terms, predicate and function symbols, and even over atomic formulas. However, when a variable appears as a predicate symbol, it has to be prefixed with -``\verb|!|'' or ``\verb|#|'' to indicate whether the HiLog predicate is -tabled or not, respectively. We will always assume that tabled HiLog -predicates are intended and thus use the ``\verb|!|'' prefix for such -variables until Section~\ref{sec-tabling-flora} which discusses tabling -in \FLORA. +``\verb|!|'' or ``\verb|#|'' to indicate whether the predicate is +supposed to be tabled (!) or not (\#). In most of our examples, we will +use tabled HiLog +predicates and thus use the prefix ``\verb|!|''. For instance, %% @@ -3303,7 +3302,7 @@ %% \begin{equation}\label{eq-hilog-notallowed} {\tt - ?- p(X), ~!X(p), ~X. + ?- p(X), ~!X(p), ~\#X(q). } \end{equation} %% @@ -3312,6 +3311,16 @@ a(b)} are all true in the database, then $\tt X=a(b)$ is one of the answers to the query in HiLog. +Note that if {\tt X}, {\tt !X}, and {\tt \#X} all appear in the same rule, +such as above, then they get bound to \emph{the same} value. +The prefix +affects only the question of whether tabled or untabled predicates are +going to be used with each particular occurrence of the variable. +For instance, if {\tt X} is bound to {\tt a(b)}, then {\tt !X(p)} will be +true if the tabled predicate {\tt a(b)(p)} is true. At the same time, +{\tt \#X(p)} will be true if the non-tabled predicate {\tt \#a(b)(p)} is +true. + \index{HiLog!translation} % Although HiLog has a higher order syntax, its semantics is first order @@ -3545,38 +3554,6 @@ {\tt (a[b->c]@foo)@N)} at run time and, due to the scoping rules, is the same as {\tt a[b->c]@foo}. -%% One more thing to know about meta-unification is that it is done at -%% the predicate level; the arguments of the predicates involved in a -%% meta-unification operation are not meta-unified. -%% Thus the following query will fail because although {\tt p@M} and -%% {\tt p@foo} meta-unify, they do not unify in the regular sense. -%% %% -%% \begin{quote} -%% \begin{verbatim} -%% ?- X ~ p@M, Y ~ p@foo, pp(X) ~ pp(Y). -%% \end{verbatim} -%% \end{quote} -%% %% -%% If the user wants meta-unification for the argument in the above -%% example, she can reify the arguments (see the next section). For instance, -%% the following query succeeds. -%% %% -%% \begin{quote} -%% \begin{verbatim} -%% ?- X ~ p@M, Y ~ p@foo, pp(${X@_M1}) ~ pp(${Y@_M2}). -%% \end{verbatim} -%% \end{quote} -%% %% -%% Notice that the following query still fails because reification does not -%% have any effect if the reified formula is a variable and therefore the -%% query is the same as the one without reification. -%% %% -%% \begin{quote} -%% \begin{verbatim} -%% ?- X ~ p@M, Y ~ p@foo, pp(${X}) ~ pp(${Y}). -%% \end{verbatim} -%% \end{quote} -%% %% \subsection{Reification} @@ -3960,8 +3937,44 @@ \end{quote} %% +Nonmonotonicity also arises due to multiple inheritance. The following +example, known as the Nixon Diamond, illustrates the problem. Let us assume +the following knowledge base: +%% +\begin{verbatim} + republican[policy *-> nonpacifist]. + quaker[policy *-> pacifist]. + nixon:quaker. +\end{verbatim} +%% +Since Nixon is a Quaker, we can derive {\tt nixon[policy -> pacifist]} +by inheritance from the second clause. Let us now assume that the following +information is added: +%% +\begin{verbatim} + nixon:republican. +\end{verbatim} +%% +Now we have a conflict. There are two conflicting inheritance candidates: +{\tt policy *-> pacifist} and {\tt policy *-> nonpacifist}. +In \FLORA, such conflicts cause previously established inheritance +to be withdrawn and the value of the attribute {\tt policy} becomes +undefined for object {\tt nixon}.\footnote{ + %% + This behavior can be altered by adding additional rules. For instance, + one could define a predicate {\tt hasPriority} and then define + %% + \begin{quote} + \tt + Obj[policy->P] :- Obj:Class, Class[policy*->P], not hasPriority(AnotherClass,Class). + \end{quote} + %% + %% +} +%% + Behavioral inheritance in \fl is discussed at length in -\cite{inheritance-odbase-02}. The above problem of non-monotonicity is +\cite{inheritance-odbase-02}. The above non-monotonic behavior is just the tip of an iceberg. Much more difficult problems arise when inheritance interacts with regular deduction. To illustrate, consider the following program: @@ -4018,13 +4031,13 @@ different, more cautious semantics for inheritance, which favors the first interpretation above. -The details of this semantics are described in +Details of this semantics are formally described in \cite{inheritance-odbase-02}. Under this semantics, {\tt clyde} will still inherit color white, but in the other two examples {\tt a[m->c]} is \emph{not} inherited. The basic intuition can be summarized as follows: %% \begin{enumerate} -\item Methods definitions in subclasses override the definitions that +\item Method definitions in subclasses override the definitions that appear in the superclasses. \item In case of a multiple inheritance conflict, the result of inheritance is undefined. More precisely, \FLORA is based on a three-valued logic and @@ -4038,8 +4051,8 @@ \end{verbatim} %% Even though we derive {\tt c[m*->f]} and {\tt d[m*->f]} by inheritance, - these two facts can be further inherited to {\tt a} since they came from - a single source {\tt e}. + these two facts can be further inherited to the object {\tt a}, since + they came from a single source {\tt e}. On the other hand, in a similar program %% @@ -4875,6 +4888,188 @@ %% +\section{Negation} \label{sec:negation} + + +\index{negation as failure} +\index{well-founded semantics for negation} +%% +\FLORA supports two kinds of negation: the usual Prolog's \emph{negation as + failure} \cite{Cla78} and negation based on \emph{well-founded semantics} +\cite{gelder-alternating-89,gelder-ross-schlipf-91}. Both types of negation +are compiled into clauses that invoke the corresponding operators in +Prolog. + +We should remark that originally, the term ``negation +as failure'' was used to denote the treatment of negation in Prolog. This +style of negation is unsatisfactory in many respects because it does not +have a model-theoretic characterization and because operationally it often +leads to infinite loops. To overcome this problem, several different +semantics were introduced, including the aforesaid well-founded semantics. +At some point later, the meaning of the term negation as failure was +broadened to refer to the class of all these forms of negation. +When ambiguity may arise, we will be referring to \emph{Prolog-style + negation as failure}. + +\subsection{Two Operators for Negation}\label{sec-negation} +\index{\TNOT} +\index{\NAF} +%% +Prolog-style negation as failure is specified using the operator \NAF. +Negation based on the well-founded semantics is specified using the +operator \TNOT. The well-founded negation, \TNOT, applies to predicates +that are tabled (i.e., predicates that do not have the {\tt \#} prefix) or +to F-molecules that do not contain procedural methods (i.e., methods that +are prefixed with a {\tt \#}). + +The semantics for negation as failure is simple. To find out whether {\tt + \NAF G} is true, the system first asks the query {\tt ?- G}. If the query +succeeds then {\tt \NAF G} is said to be satisfied. Unfortunately, this +semantics is problematic. It cannot be characterized model-theoretically +and in certain simple cases the procedure for testing whether {\tt \NAF G} +holds may send the system into an infinite loop. For instance, in the +presence of the rule {\tt \#p :- \NAF \#p}, the query {\tt ?- \#p} will not +terminate. Negation as failure is the recommended kind of negation for +non-tabled predicates (but caution needs to be exercised). + +The well-founded negation, \TNOT, has a model-theoretic semantics and is +much more +satisfactory from the logical point of view. +Formally, this semantics uses three-valued models where formulas can be +true, false, or undefined. For instance, if our program has the rule +{\tt p :- \TNOT p} then the truth value of {\tt p} is \emph{undefined}. +Although the details of this +semantics are somewhat involved \cite{gelder-ross-schlipf-91}, it is +usually not necessary to know them, because this type of negation yields +the results that the user normally expects. The implementation of +the well-founded negation in XSB requires that it is applied to goals that +consist entirely of tabled predicates or molecules. +Although \FLORA allows \TNOT to be applied to non-tabled goals, +this may lead to unexpected results. For instance, +Section~\ref{sec-updates} discusses what might happen if the +negated formula is defined in terms of an update primitive. + +For more information on the implementation of the negation operators in XSB +we refer the reader to the XSB manual. + +Both \NAF and \TNOT can be used as operators inside and outside \FLORA +molecules. For instance, +%% +\begin{alltt} + flora2 ?- \TNOT #p(a). + flora2 ?- \NAF #p(a). + flora2 ?- \TNOT X[foo->bar, bar->>foo]. + flora2 ?- X[\TNOT foo->bar, bar->>foo, \NAF #p(Y)]. +\end{alltt} +%% +are all legal queries. Note that \NAF applies only to non-tabled +constructs, such as non-tabled \FLORA predicates and procedural methods. + +We should warn against one pitfall however. Sometimes it is necessary to +apply negation to several separate literals and write something like +%% +\begin{alltt} + flora2 ?- \NAF(#p(a),#q(X)). + flora2 ?- \TNOT(p(a),q(X)). + flora2 ?- \TNOT(X[foo->bar], X[bar->>foo]). +\end{alltt} +%% +This is incorrect however, since in this context \FLORA (and Prolog as +well) will interpret \TNOT and \NAF as predicates with two arguments, +which are likely to be undefined. The correct syntax is: +%% +\begin{alltt} + flora2 ?- \NAF((#p(a),#q(X))). + flora2 ?- \TNOT((#p(a),#q(X))). + flora2 ?- \TNOT((X[foo->bar], X[bar->>foo])). +\end{alltt} +%% +{\it i.e.}, an additional pair of parentheses is needed to indicate that +the sequence of literals form a single argument. + +\subsection{True vs. Undefined Literals} + +The fact that the well-founded semantics for negation is three-valued +brings up the question of what exactly does the success or failure of a +call means. Is undefinedness covered by a success or by failure? The way +this is implemented in XSB is such that a call to a literal, $P$, succeeds +if and only if $P$ is true \emph{or} undefined. Therefore, it is sometimes +necessary to be able to separate true and undefined facts. In \FLORA, this +separation is accomplished by a call to the {\tt get\_residual/2} +predicate, which is provided by XSB. A call to +%% +\index{get\_residual/2} +%% +\begin{verbatim} + get_residual(Call,List)@prolog(tables) +\end{verbatim} +%% +succeeds if and only if {\tt Call} is either true or undefined according to +the well-founded semantics. Moreover, {\tt Call} is true iff {\tt List} is +nil ({\it i.e.}, {\tt []}). Thus, {\tt get\_residual(Call,[])@prolog(tables)} +succeeds if and only if {\tt Call} is true. + +\subsection{Unbound Variables in Negated Goals} + +When negation (either \NAF or \TNOT) is applied to a non-ground goal, one +should be aware of the following peculiarity. Consider {\tt \NAF Goal}, +where Goal has variables that are not bound. As mentioned before, +{\tt \NAF GOAL} is evaluated by posing {\tt Goal} as a query. If for +\emph{some} values of for the variables in {\tt Goal} the query succeeds, +then {\tt \NAF Goal} is false; it is true only if for \emph{all} possible +substitutions for the variables in {\tt Goal} the query is false +(fails). Therefore {\tt \NAF Goal} intuitively means $\tt\forall +Vars\,\neg\,Goal$, where {\tt Vars} represents all the nonbound variables +in {\tt Goal}. The well-founded negation has the same flavor: if {\tt + Goal} is non-ground then {\tt \TNOT GOAL} means $\tt\forall +Vars\,\neg\,Goal$. + +Of course, one should keep in mind that since neither {\tt \NAF} nor {\tt + \TNOT} is a classical negation, none of the above formulas is actually +equivalent to $\tt\forall Vars\,\neg\,Goal$, if $\neg$ is understood as +classical negation. A more precise meaning is that {\tt \TNOT Goal} is true +if and only if for every ground instance {\tt Goal$'$} of +{\tt Goal}, the literal {\tt \TNOT Goal$'$} is true in +the well-founded semantics. +Similarly, {\tt \NAF Goal} evaluates to true if and +only if for every ground instance {\tt Goal$'$} of {\tt Goal}, the query +{\tt \NAF Goal$'$} succeeds according to the negation-as-failure +semantics. + +To illustrate this, consider the following example: +%% +\begin{verbatim} + p(a,b). + q(X,Y) :- not p(X,Y). + flora ?- q(X,Y). +\end{verbatim} +%% +When {\tt not p(X,Y)} is called in the query evaluation process, the variables +are unbound, so for the query to return a positive answer, the literal {\tt + p(t,s)} should be false for every possible terms {\tt t} and {\tt s}. +Since {\tt p(a,b)} is true, our query {\tt q(X,Y)} fails. In contrast, the +query +%% +\begin{verbatim} + flora2 ?- q(b,Y). +\end{verbatim} +%% +will succeed because this will cause the query {\tt not p(b,Y)} to be +evaluated. But this query will return positive answer because {\tt p(b,Y)} +is false for all {\tt Y}. Note that even when the query succeeds the +unbound variable that occurs in the scope of the negation operator remains +unbound: +%% +\begin{verbatim} + flora2 ?- not p(b,Y). + + Y = _h1747 + + 1 solution(s) in 0.0000 seconds on speedy.foo.org +\end{verbatim} +%% + + \section{\FLORA and Tabling}\label{sec-tabling-flora} @@ -4911,13 +5106,14 @@ A predicate with the \verb|#| prefix is logically unrelated to the predicate without the \verb|#| prefix. Thus, {\tt p(a)(b)} being true does -not mean that {\tt \verb|#|p(a)(b)} is true, and vice versa. +not imply anything about {\tt \verb|#|p(a)(b)}, and vice versa. -When the predicate name is a variable, it is not clear whether the user -means tabled or non-tabled predicate. For this reason, we introduce -variables prefixed with the ``\verb|!|'' sign for tabled predicates as a -counterpart for variables prefixed with ``\verb|#|''. Therefore the -following are legal +When the predicate name is a variable, it is not possible to determine +whether the user intended it to be a tabled or a non-tabled predicate. For +this reason, \FLORA requires that the user must attach a prefix ``\verb|!|'' +to variables that stand for tabled predicates and prefix ``\verb|#|'' for +variables that stand for non-tabled predicates. Therefore the following +statements are legal %% \begin{quote} \begin{verbatim} @@ -4933,7 +5129,7 @@ \begin{quote} \begin{verbatim} ?- X(a). // ambiguity -?- !p(a). // ! is only allowed before variables +?- !p(a). // prefix ! is allowed only with variables \end{verbatim} \end{quote} %% @@ -4945,11 +5141,11 @@ %% \begin{quote} \begin{verbatim} -?- insert{#p(a)}, #_(X), !X(Y). // #_ is a variable. #_ and !X are predicate names +?- insert{#p(a)}, #_(X), !X(Y). // #_, !X - variables ranging over predicate names ?- a[#b(c)], a[#Y]. // #b and #Y are procedural Boolean methods -?- #X ~ #p(a). // #X is a variable, #p is a non-tabled predicate +?- #X ~ #p(a). // #X is a variable, #p - a non-tabled predicate ?- !X ~ p(a). // !X is a variable -?- a[!Y]. // !Y is a Boolean method +?- a[!Y]. // !Y is a variable ranging over Boolean methods \end{verbatim} \end{quote} %% @@ -4966,23 +5162,23 @@ \end{quote} %% The first formula is illegal because {\tt \#a} occurs as a term and not -as a predicate (it can be made legal by reification, however: {\tt +as a predicate (it can be made legal by reifying the argument: {\tt p(\$\{\#a\})}). In the second, third and fourth formulas {\tt \#a}, {\tt -\#X} and {\tt !X} likewise appear as unreified terms. The fifth -formula is illegal because {\tt \#b(c)} is not a Boolean method. The -last formula is illegal because variables prefixed with ``\verb|!|'' are -not allowed as methods. +\#X} and {\tt !X} also appear as unreified arguments. The last +formula is illegal because {\tt \#b(c)} is not a Boolean method. Occurrences of variables that are prefixed with {\tt \#} or {\tt !} are -treated specially. First, it should be kept in mind that {\tt \#X}, -{\tt !X} and {\tt X} represent the same variable. If {\tt X} is -\emph{already bound} to something then all three of them mean the same -thing. However, {\tt X} can range over not only predicates but also -terms, conjunction of predicates, and even rules. {\tt \#X} can be -bound to only non-tabled predicates and {\tt !X} can be bound to only -tabled predicates. Thus error messages ``non-tabled predicate -expected'' and ``tabled predicate expected'' are issued for the -following two queries, respectively. +treated specially. First, it should be kept in mind that {\tt \#X}, {\tt + !X} and {\tt X} represent the same variable. If {\tt X} is \emph{already + bound} to something then all three of them mean the same thing. However, +when {\tt X}, {\tt \#X}, or {\tt !X} appear as terms by themselves, +{\tt X} can range not only over predicates but also terms, +conjunctions/disjunctions of predicates, and even rules. In contrast, +{\tt \#X} can be +bound only to non-tabled formulas and {\tt !X} can be bound only to +tabled formulas. Thus error messages ``non-tabled predicate expected'' +and ``tabled predicate expected'' will be issued for the following two +queries: %% \begin{quote} \begin{verbatim} @@ -4991,10 +5187,10 @@ \end{verbatim} \end{quote} %% -The following queries fail for the reason that {\tt \#X}, {\tt !X} and -{\tt X} represent the same variable: in each case the first literal -determines the binding for {\tt X}, and this binding does not match with -the expression on the right side of $\sim$ in the second literal. +The following queries fail because {\tt \#X}, {\tt !X} and +{\tt X} represent the same variable: in each case the first conjunct +determines the binding for {\tt X}, and this binding does not match +the expression on the right side of $\sim$ in the second conjunct. %% \begin{quote} \begin{verbatim} @@ -5004,27 +5200,33 @@ \end{verbatim} \end{quote} %% +For instance, in the first query, {\tt X} is bound to the non-tabled +formula {\tt \#p(a)}, and this does not meta-unify with the tabled formula +{\tt p(a)}. In the second query, {\tt X} is bound to the tabled +\emph{formula} {\tt p(a)}, and this does not unify with the plain HiLog +term {\tt p(a)}. In the third case, {\tt X} is bound to the tabled formula +{\tt p(a)}, but this does not meta-unify with the non-tabled formula {\tt + \#p(a)}. When a bound variable occurs with an explicit module specification, then the following rules apply: %% \begin{itemize} - \item If {\tt X} or {\tt \#X} or {\tt !X} is bound to a predicate or - molecule formula (tabled or non-tabled), then {\tt X@module} has the - same meaning as {\tt X}, and similarly for {\tt \#X} and {\tt - !X}. That is, if the binding is already a formula (and thus its - module is already specified in it) then the additional explicit module - specification is discarded. +\item If {\tt X} or {\tt \#X} or {\tt !X} is bound to a predicate or + molecular formula (tabled or non-tabled), then {\tt X@module} has the + same meaning as {\tt X}, and similarly for {\tt \#X} and {\tt !X}. That + is, if the binding is already a formula (and thus its module is already + specified in it) then the explicit module specification is discarded. \item If {\tt !X} or {\tt \#X} is bound to a HiLog \emph{term} (not a predicate), e.g., {\tt p(a)(Z)}, then {\tt !X@module} represents the tabled predicate {\tt p(a)(Z)@module}. Similarly, {\tt \#X@module} represents the non-tabled predicate {\tt \#p(a)(Z)@module}. {\tt X@module} will - give an error because it is not clear whether the tabled or non-tabled + cause an error because it is not clear whether the tabled or non-tabled predicate is intended. \end{itemize} %% Due to these rules, the first query below succeeds, while the second -fails and the third gives an error. +fails and the third causes an error. %% \begin{verbatim} flora2 ?- X = p(a), #X@M ~ #p(a), !X@N ~ p(a)@foo. @@ -5032,16 +5234,17 @@ flora2 ?- X = p(a), X@M ~ p(a)@foo. \end{verbatim} %% -The first query succeeds because {\tt X} is bound to a term, which {\tt - \#X@M} converts to a non-tabled predicate with yet-to-be-determined - module. The meta-unification that follows therefore binds {\tt M} to - {\tt main}. Similarly {\tt !X@N} converts the term to a tabled - predicate and the meta-unification binds {\tt N} to {\tt foo}. The +The first query succeeds because {\tt X} is bound to the term {\tt p(a)}, +which {\tt \#X@M} promotes to a non-tabled predicate with yet-to-be-determined +module. The meta-unification that follows then binds {\tt M} to +{\tt main}. Similarly {\tt !X@N} promotes the term {\tt p(a)} to a tabled + predicate with a yet-to-be-determined module, + and meta-unification binds {\tt N} to {\tt foo}. The second query fails because {\tt X} is already bound to a tabled predicate and therefore {\tt !X@M} represents {\tt p(a)@main}, which does not meta-unify with {\tt p(a)@foo}. The third query gives an - error because {\tt X@M} does not specify to convert the term to a - tabled predicate or a non-tabled one. + error because {\tt X@M} is ambiguous: it is not clear whether the term + {\tt p(a)} should be promoted to a tabled or a non-tabled formula. When {\tt !X} (and thus {\tt \#X}) is \emph{unbound} then the occurrences of {\tt \#X} indicate that {\tt X} is expected to be bound @@ -5074,8 +5277,9 @@ or method and {\tt \verb|!|X} expects to be meta-unified only with a tabled predicate or method. -Unbound {\tt X} can meta-unify with both tabled and non-tabled -predicates. Therefore the following queries all succeed. +Unbound and unprefixed variable such as {\tt X} can meta-unify with both +tabled and non-tabled predicates. Therefore the following queries all +succeed. %% \begin{quote} @@ -5090,23 +5294,24 @@ \end{quote} %% -In the context of update operations, we have the same rules: {\tt \#X} - for non-tabled predicates, {\tt !X} for tabled predicates and {\tt X} - for both. The following example shows this. +In the context of update operations, \FLORA uses the same rules: {\tt \#X} + binds to non-tabled predicates, {\tt !X} to tabled predicates and {\tt X} + to both. The following example illustrates this. %% \begin{quote} \begin{verbatim} -?- insert{p(a),#q(b)}. //Yes -?- delete{!X}. //Yes with X = ${p(a)} -?- delete{#X}. //Yes with X = ${#q(b)} -?- insert{p(a),#q(b)}. //Yes -?- delete{X}. //Yes with X non-determinstically bound to ${p(a)} or ${#q(b)} +?- insert{p(a),#q(b)}. // Yes +?- delete{!X}. // Yes, with X is bound ${p(a)} +?- delete{#X}. // Yes, with X is bound ${#q(b)} +?- insert{p(a),#q(b)}. // Yes +?- delete{X}. // Yes, X is bound to ${p(a)} or ${#q(b)} \end{verbatim} \end{quote} %% -These rules also apply to querying rule bases with {\tt clause} or -deleting rules with {\tt deleterule}. +These rules also apply to queries issued against rule bases using +the {\tt clause} primitive or to deletion of rules with the {\tt deleterule} +primitive. %% \begin{quote} @@ -5114,25 +5319,28 @@ ?- insertrule{p(X) :- q(X)}. ?- insertrule{#t(X) :- #r(X)}. ?- insertrule{pp(X) :- q(X), #r(X)}. -?- clause{X,Y}. // all three rules match +?- clause{X,Y}. // all three inserted rules above would be retrieved ?- clause{#X,Y}. // X = #t(_var) and Y = #r(_var) ?- clause{!X,!Y}. // X = p(_var) and Y = q(_var) -?- clause{!X,Y}. // the first and third match +?- clause{!X,Y}. // the first and the third rules would be retrieved \end{verbatim} \end{quote} %% -For reified formulas that appear as predicate arguments, \FLORA uses -{\tt \$\{!X\}} to denote tabled predicates, {\tt \$\{\verb|#|X\}} to -denote non-tabled predicates, and {\tt \$\{X\}} or simply a variable -{\tt X} to unify with anything. +For reified formulas that appear as arguments to predicates, \FLORA uses +{\tt \$\{!X\}} to ensure that {\tt X} unifies only with tabled reified +formulas and {\tt \$\{\verb|#|X\}} to +force {\tt X} to unify only with non-tabled formulas. +{\tt \$\{X\}} is not allowed. Instead, +one should use plain {\tt X} to unify with anything. +For instance, %% \begin{quote} \begin{verbatim} -?- insert{p(${a}),p(${#b})}. //Yes -?- p(${!X}). //Yes with X = ${a} -?- p(${#X@M}). //Yes with X = ${#b} and M = main -?- p(X). //Yes with X = ${a} or ${#b} +?- insert{p(${a}),p(${#b})}. // Yes +?- p(${!X}). // Yes, X gets bound to ${a} +?- p(${#X@M}). // Yes, X gets bound to ${#b} and M to main +?- p(X). // Yes, X gets bound to ${a} or ${#b} \end{verbatim} \end{quote} %% @@ -5387,174 +5595,6 @@ alternative mechanism that achieves many of the goals a cut is used for. -\section{Negation} \label{sec:negation} - - -\FLORA supports two kinds of negation: the usual Prolog's \emph{negation as - failure} \cite{Cla78} and negation based on \emph{well-founded semantics} -\cite{gelder-alternating-89,gelder-ross-schlipf-91}. Both types of negation -are compiled into clauses that invoke the corresponding operators in -Prolog. - -\subsection{Two Operators for Negation}\label{sec-negation} -\index{\TNOT} -\index{\NAF} -%% -Negation as failure is specified using the operator \NAF. Negation based -on the well-founded semantics is specified using the operator \TNOT. The -well-founded negation, \TNOT, applies to predicates that are tabled (i.e., -predicates that do not have the {\tt \#} prefix) or to F-molecules that do -not contain procedural methods (i.e., methods that are prefixed with a {\tt - \#}). - -The semantics for negation as failure is simple. To find out whether {\tt - \NAF G} is true, the system first asks the query {\tt ?- G}. If the query -succeeds then {\tt \NAF G} is said to be satisfied. Unfortunately, this -semantics is problematic. It cannot be characterized model-theoretically -and in certain simple cases the procedure for testing whether {\tt \NAF G} -holds may send the system into an infinite loop. For instance, in the -presence of the rule {\tt \#p :- \NAF \#p}, the query {\tt ?- \#p} will not -terminate. Negation as failure is the recommended kind of negation for -non-tabled predicates. - -The well-founded negation, \TNOT, has a model-theoretic semantics and is -much more -satisfactory from the logical point of view. -Formally, this semantics uses three-valued models where formulas can be -true, false, or undefined. For instance, if our program has the rule -{\tt p :- \TNOT p} then the truth value of {\tt p} is \emph{undefined}. -Although the details of this -semantics are somewhat involved \cite{gelder-ross-schlipf-91}, it is -usually not necessary to know them, because this type of negation yields -the results that the user normally expects. The implementation of -the well-founded negation in XSB requires that it is applied to goals that -consist entirely of tabled predicates or molecules. -Although \FLORA allows \TNOT to be applied to non-tabled goals, -this may lead to unexpected results. For instance, -Section~\ref{sec-updates} discusses what might happen if the -negated formula is defined in terms of an update primitive. - -For more information on the implementation of the negation operators in XSB -we refer the reader to the XSB manual. - -Both \NAF and \TNOT can be used as operators inside and outside \FLORA -molecules. For instance, -%% -\begin{alltt} - flora2 ?- \TNOT #p(a). - flora2 ?- \NAF #p(a). - flora2 ?- \TNOT X[foo->bar, bar->>foo]. - flora2 ?- X[\TNOT foo->bar, bar->>foo, \NAF #p(Y)]. -\end{alltt} -%% -are all legal queries. Note that \NAF applies only to non-tabled -constructs, such as non-tabled \FLORA predicates and procedural methods. - -We should warn against one pitfall however. Sometimes it is necessary to -apply negation to several separate literals and write something like -%% -\begin{alltt} - flora2 ?- \NAF(#p(a),#q(X)). - flora2 ?- \TNOT(p(a),q(X)). - flora2 ?- \TNOT(X[foo->bar], X[bar->>foo]). -\end{alltt} -%% -This is incorrect however, since in this context \FLORA (and Prolog as -well) will interpret \TNOT and \NAF as predicates with two arguments, -which are likely to be undefined. The correct syntax is: -%% -\begin{alltt} - flora2 ?- \NAF((#p(a),#q(X))). - flora2 ?- \TNOT((#p(a),#q(X))). - flora2 ?- \TNOT((X[foo->bar], X[bar->>foo])). -\end{alltt} -%% -{\it i.e.}, an additional pair of parentheses is needed to indicate that -the sequence of literals form a single argument. - -\subsection{True vs. Undefined Literals} - -The fact that the well-founded semantics for negation is three-valued -brings up the question of what exactly does the success or failure of a -call means. Is undefinedness covered by a success or by failure? The way -this is implemented in XSB is such that a call to a literal, $P$, succeeds -if and only if $P$ is true \emph{or} undefined. Therefore, it is sometimes -necessary to be able to separate true and undefined facts. In \FLORA, this -separation is accomplished by a call to the {\tt get\_residual/2} -predicate, which is provided by XSB. A call to -%% -\index{get\_residual/2} -%% -\begin{verbatim} - get_residual(Call,List)@prolog(tables) -\end{verbatim} -%% -succeeds if and only if {\tt Call} is either true or undefined according to -the well-founded semantics. Moreover, {\tt Call} is true iff {\tt List} is -nil ({\it i.e.}, {\tt []}). Thus, {\tt get\_residual(Call,[])@prolog(tables)} -succeeds if and only if {\tt Call} is true. - -\subsection{Unbound Variables in Negated Goals} - -When negation (either \NAF or \TNOT) is applied to a non-ground goal, one -should be aware of the following peculiarity. Consider {\tt \NAF Goal}, -where Goal has variables that are not bound. As mentioned before, -{\tt \NAF GOAL} is evaluated by posing {\tt Goal} as a query. If for -\emph{some} values of for the variables in {\tt Goal} the query succeeds, -then {\tt \NAF Goal} is false; it is true only if for \emph{all} possible -substitutions for the variables in {\tt Goal} the query is false -(fails). Therefore {\tt \NAF Goal} intuitively means $\tt\forall -Vars\,\neg\,Goal$, where {\tt Vars} represents all the nonbound variables -in {\tt Goal}. The well-founded negation has the same flavor: if {\tt - Goal} is non-ground then {\tt \TNOT GOAL} means $\tt\forall -Vars\,\neg\,Goal$. - -Of course, one should keep in mind that since neither {\tt \NAF} nor {\tt - \TNOT} is a classical negation, none of the above formulas is actually -equivalent to $\tt\forall Vars\,\neg\,Goal$, if $\neg$ is understood as -classical negation. A more precise meaning is that {\tt \TNOT Goal} is true -if and only if for every ground instance {\tt Goal$'$} of -{\tt Goal}, the literal {\tt \TNOT Goal$'$} is true in -the well-founded semantics. -Similarly, {\tt \NAF Goal} evaluates to true if and -only if for every ground instance {\tt Goal$'$} of {\tt Goal}, the query -{\tt \NAF Goal$'$} succeeds according to the negation-as-failure -semantics. - -To illustrate this, consider the following example: -%% -\begin{verbatim} - p(a,b). - q(X,Y) :- not p(X,Y). - flora ?- q(X,Y). -\end{verbatim} -%% -When {\tt not p(X,Y)} is called in the query evaluation process, the variables -are unbound, so for the query to return a positive answer, the literal {\tt - p(t,s)} should be false for every possible terms {\tt t} and {\tt s}. -Since {\tt p(a,b)} is true, our query {\tt q(X,Y)} fails. In contrast, the -query -%% -\begin{verbatim} - flora2 ?- q(b,Y). -\end{verbatim} -%% -will succeed because this will cause the query {\tt not p(b,Y)} to be -evaluated. But this query will return positive answer because {\tt p(b,Y)} -is false for all {\tt Y}. Note that even when the query succeeds the -unbound variable that occurs in the scope of the negation operator remains -unbound: -%% -\begin{verbatim} - flora2 ?- not p(b,Y). - - Y = _h1747 - - 1 solution(s) in 0.0000 seconds on speedy.foo.org -\end{verbatim} -%% - - \section{Updating the Knowledge Base}\label{sec-updates} |