What is the meaning of this pseudo-code function?

Question

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.

Answer 1

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.

Answer 2

"Implies" in the English language indicates that there is room for subjectivity. But this is not standard English you're looking at. When you read A⟹B as "A implies B" in Discrete Mathematics, it is just another way to say, "If A is true, then B is true." Formally, this is called material implication.

So the two ways you thought to read it are the same - as far as Comp.Sci. goes. Left to right and minimal imagination it reads (out loud), "Return the truth of this assertion: For all q-sub-i that are members of subtreeNodes of q, isLeaf of q-sub-i implies eof of T-sub-sub-i."