Problem Detail: While reading the paper Holistic twig joins: optimal XML pattern matching I came across the pseudo code for liststack algorithm. (available through google scholar) A function in the algorithm confused me, since I can understand what it is supposed to do, but can’t deconstruct the notation: $qquad mathtt{Function} mathtt{end}(qmathtt) qquadqquad mathtt{return} forall q_i in mathtt{subtreeNodes}(q) : mathtt{isLeaf}(q_i) implies mathtt{eof}(T_{q_i})$ This function is supposed to return a single boolean result. It is supposed to be true when all lists associated to leaf nodes of a query pattern node are at their end. So true means there are no more nodes in the query pattern to process. But what is the meaning of the set builder(ish?) notation here? Is it $qquad$ “for all subtree nodes of $q$ for which $mathtt{isLeaf}(q_i)$ is true $mathtt{eof}(T_{q_i})$ is also true” (which means that the list is at the end position)? Or is it $qquad$ “for all subtree nodes of $q$, $mathtt{isLeaf}(q_i)$ implies $mathtt{eof}(T_{q_i})$ is true”? Is double arrow representing implies with its truth table? As you can see, I’m having a bit difficulty in associating the colon and its precedence.
Asked By : mahonya
Answered By : Raphael
Let us abstract what you have there to$ renewcommand{models}{mathop{|!!!=}}newcommand{rmodels}{mathop{=!!!|}} newcommand{semeq}{models!rmodels}$ $qquad mathtt{return} forall x in X., P(x) implies Q(x)$. For evaluation, remember that $qquad A implies B quad models!rmodels quad lnot A lor B$. What this means is that you return true if and only if for all $x$ it is true that $qquad$”whenever $P(x)$ holds, then $Q(x)$ holds”. In your example, that translates to $qquad$ return true if all subtree nodes that are leaves have also reached the end of their respective files. This is exactly what you expected, up to semantics of the eof function.
It is supposed to be true when all lists associated to leaf nodes of a query pattern node are at their end.
Note that the only other way to apply operator precendences, i.e. $qquad mathtt{return} bigl(forall x in X., P(x)bigr) implies Q(x)$, does not make sense: in the term $Q(x)$, variable $x$ is not bound and there is no global interpretation shadowed by the $forall$, so it’s free. Hence, the term does not have a (fixed) truth value.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/13675
