[Solved]: What is the meaning of this pseudo-code function?

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}(q\mathtt) \\ \qquad\qquad \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