Menu
▾
▴
[Xsb-commits] CVS: XSB/docs/userman debugging.tex, 1.28, 1.29 incr_tabling.tex, 1.20, 1.21 manual.bib, 1.56, 1.57 manual1.pdf, 1.76, 1.77 manual1.tex, 1.52, 1.53 table_builtins.tex, 1.55, 1.56 tables.tex, 1.52, 1.53
|
From: Terrance S. <ts...@us...> - 2012-11-28 16:16:39
|
Update of /cvsroot/xsb/XSB/docs/userman In directory sfp-cvs-1.v30.ch3.sourceforge.com:/tmp/cvs-serv7278 Modified Files: debugging.tex incr_tabling.tex manual.bib manual1.pdf manual1.tex table_builtins.tex tables.tex Log Message: Updates to document get_residual_sccs and friends. Index: debugging.tex =================================================================== RCS file: /cvsroot/xsb/XSB/docs/userman/debugging.tex,v retrieving revision 1.28 retrieving revision 1.29 diff -u -r1.28 -r1.29 --- debugging.tex 12 Aug 2012 17:49:47 -0000 1.28 +++ debugging.tex 28 Nov 2012 16:15:19 -0000 1.29 @@ -444,7 +444,7 @@ made only if the table for $S$ is incomplete (see the explanation below). -\index{strongly donnected somponents (SCCs)} +\index{strongly donnected components (SCCs)} \item {\em Subgoal completion} \bi \item When a set $\cS$ of subgoals is determined to be completely Index: incr_tabling.tex =================================================================== RCS file: /cvsroot/xsb/XSB/docs/userman/incr_tabling.tex,v retrieving revision 1.20 retrieving revision 1.21 diff -u -r1.20 -r1.21 --- incr_tabling.tex 30 Oct 2012 23:07:55 -0000 1.20 +++ incr_tabling.tex 28 Nov 2012 16:15:21 -0000 1.21 @@ -631,6 +631,8 @@ incr\_table\_update/[0,1,2]} or updated lazily. \end{description} +\index{residual dependency graph} +\index{incremental dependency graph} \paragraph{Introspecting Dependencies among Incremental Subgoals} % In order to efficiently perform incremental updates, each @@ -640,16 +642,21 @@ nodes are incrementally tabled subgoals present in XSB; a given subgoal in the graph may or may not have been completed. In addition, there is an edge from $S_1$ to $S_2$ labelled depends (affects) if -$S_1$ directly depends on (affects) $S_2$. We call this graph the -{\em incrementally tabled subgoal dependency graph}, or just the -dependency graph if the context is clear. The predicates in this -section allow a user to inspect properties of the dependency graph -that can be useful in debugging or profiling a computation. +$S_1$ directly depends on (directly affects) $S_2$. We call this +graph the {\em incrementally tabled subgoal dependency graph}, or just +the incremental dependency graph. The predicates in this section +allow a user to inspect properties of the dependency graph that can be +useful in debugging or profiling a computation~\footnote{The + predicates for traversing the incremental dependency graph are + somewhat analogous to those for traversing the residual dependency + graph (Section~\ref{sec:table-inspection}).}. As explained below, nodes for the dependency graph can be accessed via -{\tt is\_incremental\_subgoal/1}, while edges can be accessed via {\tt - incr\_directly\_depends/2}. {\tt get\_incr\_scc/[1,2]} can be also -used to produce SCC information for the dependency graph. +the predicate {\tt is\_incremental\_subgoal/1}, while edges can be +accessed via {\tt incr\_directly\_depends/2}. The predicates {\tt + get\_incr\_scc/[1,2]} and {\tt get\_incr\_scc\_with\_deps/[3,4]} can +be used to efficiently materialize the dependency graph in Prolog, +including SCC information. \begin{description} @@ -674,18 +681,18 @@ {\bf Error Cases} \bi -\item Neither {\tt Goal} nor {\tt DependentGoal} is bound +\item Neither {\tt Goal$_1$} nor {\tt Goal$_2$} is bound \bi \item {\tt instatiation\_error} \ei -\item {\tt Goal} or {\tt DependentGoal} is bound, but is not +\item {\tt Goal$_1$} and/or {\tt Goal$_2$} is bound, but is not incrementally tabled \bi \item {\tt table\_error} \ei \ei -\ourmoditem{incr\_trans\_depends(?Goal$_1$,?Goal$_2$}{incr\_trans\_depends/2}{increval} +\ourmoditem{incr\_trans\_depends(?Goal$_1$,?Goal$_2$)}{incr\_trans\_depends/2}{increval} is similar to {\tt incr\_directly\_depends/2} except that it returns goals according to the transitive closure of the ``directly depends'' relation. Error conditions are the same as {\tt @@ -696,21 +703,21 @@ \ourrepeatmoditem{get\_incr\_sccs(+SubgoalList,?SCCList)}{get\_incr\_sccs/2}{increval} \ourmoditem{get\_incr\_sccs\_with\_deps(+SubgoalList,?SCCList,?DepList)}{get\_incr\_sccs\_with\_deps/3}{increval} % -Most algorithms for SCC detection over a graph use destructive +Most linear algorithms for SCC detection over a graph use destructive assignment on a stack to maintain information about the connecteness -of a component; as a result such algorithms are difficult to write -efficiently in Prolog. +of a component; as a result such algorithms are +difficult to write efficiently in Prolog. {\tt get\_incr\_sccs/1} unifies {\tt SCCList} with SCC information for -the dependency graph that is represented as a list whose elements are -of the form +the incremental dependency graph that is represented as a list whose +elements are of the form \begin{center} {\tt ret(Subgoal,SCC)}. \end{center} {\tt SCC} is a numerical index for the SCCs of Subgoal. Two subgoals are in the same SCC iff they have the same index, however no other dependency information can be otherwise directly inferred from the -index. +index. If dependency information is also desired, {\tt get\_incr\_scc\_with\_dependencies/2} should be called. In addition @@ -733,6 +740,13 @@ affects relations, unions these sets together, and finds the SCCs of all subgoals in the unioned set. +These predicates implement Tarjan's algorithm~\cite{Tarj72} in C +working directly on XSB's data structures. The algorithm is $\cO(|V| ++ |E|)$ where $|V|$ is the number of vertices and $|E|$ the number of +edges in the dependency graph. As a result, these predicates provide +an efficient means to materialize the dependency graph, even if SCC +information per se is not required. + {\bf Error Cases} \bi \item {\tt SCCList} contains a predicate that is not tabled Index: manual.bib =================================================================== RCS file: /cvsroot/xsb/XSB/docs/userman/manual.bib,v retrieving revision 1.56 retrieving revision 1.57 diff -u -r1.56 -r1.57 --- manual.bib 11 Aug 2012 21:42:38 -0000 1.56 +++ manual.bib 28 Nov 2012 16:15:21 -0000 1.57 @@ -2589,6 +2589,15 @@ %%% T %%% + +@article{Tarj72, +author = "R.E. Tarjan", +Title = "Depth-first search and linear graph algorithms", +Journal = "{SIAM} Journal on Computing", +volume = 1, +pages = "146-160", +year = 1972} + @inproceedings{ TAKI1, AUTHOR = "Kazuo Taki and K. Nakajima and H. Nakashima and Morohito Ikeda", TITLE = "Performance and Architectural Evaluation of the PSI Machine", Index: manual1.pdf =================================================================== RCS file: /cvsroot/xsb/XSB/docs/userman/manual1.pdf,v retrieving revision 1.76 retrieving revision 1.77 diff -u -r1.76 -r1.77 Binary files /tmp/cvsarrnol and /tmp/cvsFxcLHF differ Index: manual1.tex =================================================================== RCS file: /cvsroot/xsb/XSB/docs/userman/manual1.tex,v retrieving revision 1.52 retrieving revision 1.53 diff -u -r1.52 -r1.53 --- manual1.tex 15 Aug 2012 19:01:21 -0000 1.52 +++ manual1.tex 28 Nov 2012 16:15:58 -0000 1.53 @@ -128,6 +128,7 @@ % ------------------ \newcommand{\code}[1]{\textup{\texttt{#1}}} % program code fragment \newcommand{\cA}{{\cal A}} +\newcommand{\cO}{{\cal O}} \newcommand{\cS}{{\cal S}} \newcommand{\mif}{\mbox{ :- }} Index: table_builtins.tex =================================================================== RCS file: /cvsroot/xsb/XSB/docs/userman/table_builtins.tex,v retrieving revision 1.55 retrieving revision 1.56 diff -u -r1.55 -r1.56 --- table_builtins.tex 10 Oct 2012 19:02:38 -0000 1.55 +++ table_builtins.tex 28 Nov 2012 16:16:03 -0000 1.56 @@ -1,4 +1,4 @@ -%======================================================== +%======================================================= \newcommand{\retn}{\code{ret/n}} @@ -326,7 +326,7 @@ %-------------------------------------------------------------------------- -\subsection{Predicates for Table Inspection} +\subsection{Predicates for Table Inspection} \label{sec:table-inspection} \label{sec:TablePred:Inspection} \index{tabling!table inspection} \index{tabling!call subsumption} @@ -889,12 +889,12 @@ % \ourstandarditem{variant\_get\_residual(\#CallTerm,?DelayList)}{variant\_get\_residual/2}{Tabling} % -{\tt get\_residual/2} backtracks through the answer set of each +{\tt get\_residual/2} backtracks through the answers to each \emph{completed} subgoal in the table that unifies with \code{CallTerm}. With each successful unification, this argument is further instantiated as well as that of the \code{DelayList}. -\begin{example} +\begin{example} \label{ex:residual-program} For the following program and table \begin{center} \begin{tabular}{cc} @@ -908,7 +908,7 @@ \end{minipage} & \begin{tabular}{||l|l||} \hline - {\em Call} & {\em Returns} \\ \hline \hline + {\em Subgoal} & {\em Answers} \\ \hline \hline p(1,X) & p(1,2) \\ & p(1,3):- tnot(p(2,3)) \\ \hline p(1,3) & p(1,3):- tnot(p(2,3)) \\ \hline @@ -948,17 +948,19 @@ \end{center} \end{example} +\index{residual program} Since the delay list of an answer consists of those literals whose truth value is unknown in the well-founded model of the program (see Chapter~\ref{chap:TablingOverview}) \code{get\_residual/2} is useful to examin the residual program (e.g. for XASP). For other purposes, it may be desired to examine the answers for a -particular call -- not for all calls that unifiy with {\tt CallTerm}. -In this case, {\tt variant\_get\_residual/2} can be used, which -backtracks through all answers for {\tt CallTerm} if {\tt CallTerm} is -a tabled subgoal with answers, and fails otherwise. For the above -example, {\tt variant\_get\_residual/2} behaves as follows: +particular subgoal, rather than for all subgoals that unifiy with {\tt + CallTerm}. In this case, {\tt variant\_get\_residual/2} can be +used, which backtracks through all answers for {\tt CallTerm} if {\tt + CallTerm} is a tabled subgoal with answers, and fails otherwise. +For the above example, {\tt variant\_get\_residual/2} behaves as +follows: \begin{center} \begin{small} @@ -1055,7 +1057,7 @@ \end{small} \end{center} -\ourrepeatmoditem{table\_dump(\#Term,+OptionList)}{table\_dump/2}{dump\_table} +\ourrepeatmoditem{table\_dump(+OptionList)}{table\_dump/2}{dump\_table} % \ourmoditem{table\_dump(+Stream,\#Term,+OptionList)}{table\_dump/3}{dump\_table} % @@ -1343,6 +1345,124 @@ \ei \ei +\index{residual program} +\index{\texttt{get\_residual/2}} +\index{\texttt{variant\_get\_residual/2}} +\index{incremental dependency graph} +\index{residual dependency graph} +\ourrepeatmoditem{get\_residual\_sccs(+Subgoal,+Answer,-SCCList)}{get\_residual\_sccs/3}{tables} +\ourmoditem{get\_residual\_sccs(+Subgoal,+Answer,-SCCList,-DepList,-SignList)}{get\_residual\_sccs/3}{tables} +% +As discussed in Section~\ref{sec:non-strat}, answers that are +undefined in the well-founded semantics are stored in XSB along with +their delay lists, forming a residual program. This residual program +can be materialized through the various predicates discussed above, in +particular {\tt get\_residual/2} and {\tt variant\_get\_residual/2}. + +At times it can be useful to view the residual program as a directed +graph, for instance in order to understand why a given answer might be +undefined. In a manner somewhat analogous to the incremental +dependency graph (Section ~\ref{sec:incremental_tabling}) this graph +is a directed graph whose nodes are atoms and whose edges are labelled +with: 1) a sign indicating whether the edge is positive or negative; +and 2) the label {\em depends on} or {\em affects}. + +\begin{example} \rm +Consider the program +% +{\tt +\begin{tabbing} +fooo\=fooooooooooooooooooooooooooooooo\=ooooooooooooo\=\kill + \> :- table p/2. \\ +\> p(1,2). \\ +\> p(1,3):- tnot(p(2,3)). \\ +\> p(2,3):- tnot(p(1,3)). \> p(2,3):- r(a).\\ +\> r(a):- tnot(r(b)) \\ +\> r(b):- tnot(r(a)). +\end{tabbing} +} +% +to which the query {?- p(1,X)} was made, generating the tables: +\begin{center} +\begin{tabular}{||l|l||} \hline + {\em Subgoal} & {\em Answers} \\ \hline \hline + p(1,X) & p(1,2) \\ + & p(1,3):- tnot(p(2,3))| \\ \hline + p(1,3) & p(1,3):- tnot(p(2,3))| \\ \hline + p(2,3) & p(2,3):- tnot(p(1,3))| \\ \hline + & p(2,3):- tnot(r(a))| \\ \hline + r(a) & r(a):- tnot(r(b))| \\ \hline + r(b) & r(b):- tnot(r(a))| \\ \hline +\end{tabular} +\end{center} + +The residual dependency graph for this program and query would have a +node for each subgoal/answer combination with an undefined truth +value, and a dependency edge for nodes $S_1/A_1$ and $S_2/A_2$ if +$A_2$ occurs in a literal in the delay list for $S_1/A_1$, and the +original subgoal for $A_2$ was $S_2$ in the subcomputation for $S_1$. +The edge also has a sign indicating whether $A_2$ occurs positively or +negatively in the delay list for $A_1$. In this example, the residual +dependency graph can be represented as +% +\begin{verbatim} + edge(p(1,X),p(1,3),p(2,3),p(2,3),neg). + edge(p(1,3),p(1,3),p(2,3),p(2,3),neg). + edge(p(2,3),p(2,3),p(1,3),p(1,3),neg). + edge(p(2,3),p(2,3),r(a),r(a),pos). + edge(r(a),r(a),r(b),r(b),neg). + edge(r(b),r(b),r(a),r(a),neg). +\end{verbatim} +\end{example} + +\index{termination!bounded rationality} \index{\texttt{u\_not/1}} +% +Using the residual dependency graph, a user may be able to determine +why an answer $A$ to a subgoal $S$ was unexpectedly undefined either +because $S/A$ was involved in or depended on a loop through negation; +or because $S/A$ depended on some other answer that was undefined +because of the use of bounded rationality +(Section~\ref{sec:tabling-termination}) or because of floundering and +the use of {\tt u\_not/1}. + +The dependency graph connected to a given subgoal/answer pair can be +obtained through {\tt get\_residual\_sccs/[3,5]}. Each predicate +returns the list of subgoal / answer pairs along with an SCC index in +a term of the form +% +\begin{center} +{\tt ret(Subgoal,Answer,SCCIndex)}. +\end{center} +% +{\tt get\_residual\_sccs/5} also returns a list indicating the direct +dependencies among the SCCs, along with a list indicating whether +given SCCs contain a negative edge. For the example above, the SCC +information would have a form such as: +\begin{verbatim} +[ ret(p(1,X),p(1,3),1), ret(p(1,3),p(1,3),2), ret(p(2,3),p(2,3),2), + ret(r(a),r(a),3), ret(r(b),r(b),3) ] +\end{verbatim} +% +The dependency list would have a form such as: +\begin{verbatim} +[ depends(1,2), depends(2,3) ] +\end{verbatim} +while the sign list would have a form such as: +\begin{verbatim} +[ sign(1,no_neg), sign(2,neg), sign(3,neg) ] +\end{verbatim} + +These predicates implement Tarjan's algorithm~\cite{Tarj72} in C +working directly on XSB's data structures. The algorithm is $\cO(|V| ++ |E|)$ where $|V|$ is the number of vertices and $|E|$ the number of +edges in the dependency graph. As a result, these predicates provide +an efficient means to materialize the dependency graph, even if SCC +information per se is not required~\footnote{The actual number for + each SCC index depends on how the residual dependency graph happens + to be traversed; as a result it is best to rely on the index only as + a ``generated'' name for each SCC.}. + +\comment{ \ourmoditem{explain\_u\_val(+Answer,?Reason,?Type)}{explain\_u\_value/3}{tables} % {\tt explain\_u\_val/3} can be used to query why {\tt Answer} is @@ -1376,7 +1496,7 @@ that {\tt p} also indirectly depends on {\tt q} which is itself involved in a loop through negation. \end{example} - +} % - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Index: tables.tex =================================================================== RCS file: /cvsroot/xsb/XSB/docs/userman/tables.tex,v retrieving revision 1.52 retrieving revision 1.53 diff -u -r1.52 -r1.53 --- tables.tex 10 Oct 2012 19:02:38 -0000 1.52 +++ tables.tex 28 Nov 2012 16:16:07 -0000 1.53 @@ -1269,7 +1269,7 @@ XSB\@. \subsection{On Beyond Zebra: Implementing Other Semantics for -Non-stratified Programs} +Non-stratified Programs} \label{sec:non-strat} \index{stable models} The Well-founded semantics is not the only semantics for @@ -1296,6 +1296,8 @@ stable model semantics through the {\em residual program}, to which we now turn. +\index{residual program} + \paragraph*{The Residual Program} Given a program $P$ and query $Q$, the residual program for $Q$ and @@ -1885,7 +1887,7 @@ \index{termination!bounded rationality} \index{abstraction!subgoal} \index{abstraction!answer} -\section{Tabling for Termination} +\section{Tabling for Termination} \label{sec:tabling-termination} % As noted throughout this manual, tabling adds important termination properties to programs and queries. In this section we state more @@ -2115,6 +2117,7 @@ which in a delay list indicates that an answer was made undefined through bounded-rationality based answer abstraction. +\comment{ \index{\texttt{explain\_u\_value/3}} The XSB predicate @@ -2150,7 +2153,7 @@ indirect}. Note that {\tt p} also indirectly depends on {\tt q} which is itself involved in a loop through negation. \end{example} - +} \subsubsection{Using Bounded Rationality} % Bounded rationality is currently implemented only for tabling with |