The BoaC Programming Guide - Quantifiers

Quantifiers in BoaC provide an easy way to specify loops with conditions. While these are just sugars in the language, they are much more concise and thus easier to write and maintain.

The general form of quantifiers is given below:

The code above defines a loop. Inside the loop, the quantifier variable var is declared. There are three kinds of quantifier: foreach, exists, or ifall. The quantifier variable also defines a type (usually int). This variable is used inside the condition and determines if and how often the given statement executes.

The condition must be a bool statement. If it is not boolean, the condition is rewritten by the compiler to def(condition). This allows, for example, easily iterating over arrays.

Let's look at each kind of quantifier via some simple examples.

foreach Quantifiers

The foreach quantifier will evaluate the given condition for each possible value. If the condition evaluates to true, then the specified statement executes with the quantifier bound to the value that caused the condition to evaluate to true.

For example, what if we wanted to increment a counter each time a Author's declared affiliation's declared institution contains the string iowa state? We might write the following statement:

This statement declares the quantifier variable i to be of type int. The loop generated from this code will loop over all values in the array p.metadata.authors, binding i for each value and evaluating the condition. If the condition evaluates to true, then the value 1 is sent to the output table counts[lowercase(p.metadata.authors[i].affiliation.institution)]. Note that the value of i is bound inside the body of the statement.

For reference, a de-sugared form semantically equivilent to the above could be:

As you can see, the compiler automatically infers the bounds of the loop based on the given condition. If for example the condition was more complex and the quantifier variable used to index more than one expression, the generated length variable would use the minimum value from each expression.

exists Quantifiers

The exists quantifier will evaluate the given condition for each possible value. If there exists a condition that evaluates to true for at least one value, then the specified statement executes with the quantifier bound to a deterministically chosen value that caused the condition to evaluate to true.

For example, what if instead of incrementing the counter for each of a <Author's declared affiliation's declared institution that contains the string iowa state, we only want to increment it once if at least one contains that string? We might write the following statement:

This statement declares the quantifier variable i to be of type int. The loop generated from this code will loop over all values in the array p.metadata.authors[i], binding i for each value and evaluating the condition. If the condition evaluates to true for at least one value of i, then the value 1 is sent to the output table counts[lowercase(p.metadata.authors[i].affiliation.institution)]. This value is sent exactly 0 or 1 time. Note that the value of i is bound inside the body of the statement to a deterministically chosen value that caused the condition to evaluate to true.

For reference, a de-sugared form semantically equivilent to the above could be:

Again, as you can see, the compiler automatically infers the bounds of the loop based on the given condition.

ifall Quantifiers

The third kind of quantifier is the ifall quantifier. This quantifier evaluates the given condition for each possible value. If the condition evaluates to true for all values, then the specified statement executes exactly once. The quantifier variable is not available in the body of the statement.

For example, perhaps we want to count all papers with affiliations with iowa state. For this, we might write the following code:

This statement declares the quantifier variable i to be of type int. The loop generated from this code will loop over all values in the array p.metadata.authors, binding i for each value and evaluating the condition. If the condition evaluates to true for all values of i, then the value 1 is sent to the output table counts. This value is sent exactly 0 or 1 time.

For reference, a de-sugared form semantically equivilent to the above could be:

Again note the compiler inferred the loop bounds automatically. The quantifier variable is not available in the body, as the value of i in this case would be outside the bounds of the array.