Chapter 10. Formulas

Roughly speaking, a formula is a LogiQL construct that may be true or false, depending on the information currently in the database. If a formula contains variables, then it is, in general, the choice of instantiations for these variables that makes the formula false or true: the same formula may be false for some instantiations and true for others. For example, the simple formula x < y is true if we instantiate x to 7 and y to 8, but false if we instantiate both variables to 5.

The evaluation of a formula usually results in computing variable instantiations that make it true, or checking that there are no such instantiations, i.e., that the formula is always false. All this is explained in more detail below.

A formula that is true is often said to hold, and a false formula does not hold.

10.1. Atoms

Formula = Atom .

Atom = BasicAtom         | FunctionalAtom
     | ReferenceModeAtom | ExternalDiffAtom .

BasicAtom = PredicateDescriptor "(" [ ArgumentList ] ")" .

ArgumentList = Expression { "," Expression } .

ReferenceModeAtom = PredicateDescriptor "(" Expression ":" Expression ")".

PredicateDescriptor = PredicateName [ "@" Suffix ].
PredicateName       = Identifier.
Suffix              = Identifier.

The optional suffix in PredicateDescriptor can be a reference to a transaction stage (Section 19.4.4, “Stage suffixes”) or the name of a branch (Chapter 41, Database Branching). In the text below we will simply talk about a predicate name, tacitly assuming that in most contexts it can be augmented with a suffix. It is important to note that the suffix cannot be present if the atom occurs in the head of a clause.

(There is one exception to the rule: one is allowed to declare constraints for predicates with stage names, e.g., p@prev(x) -> x > 0.. However, such constraints currently have no effect.)

There are four kinds of atoms: basic atoms, functional atoms, reference-mode atoms and external diff atoms.

Functional atoms are described in Section 10.1.4, “Functional atoms”.

A reference-mode atom consists of a predicate name followed by two expressions, separated by a colon and enclosed in parentheses. The first of these expressions must be an identifier (i.e., the name of a variable), and the second must be either an identifier or a literal. The predicate must be a reference mode predicate. See Section 8.3.2, “Reference-Mode Predicates” for more information.

External diff atoms are described in Section 10.1.5, “External diff atoms”.

A basic atom consists of a predicate name followed by a list of arguments, which may be empty. A non-empty list of arguments is a list of expressions separated by commas.

The number of expressions must be equal to the arity of the predicate, and the type of each expression must be the type of the corresponding position in tuples that belong to the predicate. The predicate may be a functional predicate, but in the case of a single-value functional predicate it is better style not to use a basic atom, but a functional atom, e.g., f[x, y] = z instead of f(x, y, z).

Note

In the rest of this section we use the unadorned term "atom" to denote a basic atom. Most of what we write will be applicable (with simple mutations) also to atoms that are not basic atoms.

In general, an atom is a formula meant to express a certain relation between its arguments (see Example 10.1, “Atoms”). By contrast, a predicate is essentially a relation in the mathematical sense, i.e., a set of tuples. (The main difference is that, unlike a mathematical relation, a predicate can evolve over time, as its contents change.)

An atom is fully instantiated if all the variables occurring in its arguments are instantiated. A fully instantiated atom is true if the values of its arguments form a tuple that is (currently) in the named predicate. (We say "the values of its arguments", because the arguments are expressions.)

Example 10.1. Atoms

square_of(2, 3*3)          // 9 is a square of 2
Person(p)                  // p is a person
loves(p, _)                // p loves something
loves(p, "Juliet")         // p loves Juliet
loves("Romeo", "Juliet")   // Romeo loves Juliet

As we can see from the first example, whatever an atom expresses need not necessarily be true. (However, if this atom were a fact, we would probably not put it in our program: given some intended intepretation of the predicates, we try to make our databases reflect reality.)

There is a certain amount of leeway in how we interpret an atom. For example, we have chosen to read the last atom above as expressing "Romeo loves Juliet", but we might as well have chosen another reading: "Juliet loves Romeo". The choice is a matter of convention, and the syntax does not reflect it directly.

(The usual convention is the one we have adopted above. For the the second possibility we would normally have switched the arguments, or chosen another name for the predicate, e.g., is_loved_by.)

The exact meaning of an atom depends on the context in which it occurs. There are three possibilities:

  • an atom may be a fact;
  • an atom may occur in the head of a rule;
  • an atom may occur in the body of a rule.

10.1.1. Atoms as facts

A stand-alone atom followed by a period is called a fact. It represents a tuple in the predicate named by the atom.

Example 10.2. A fact

p(2 * 2, 2 + 3).

The above indicates that tuple (4, 5) belongs to predicate p. From the form of the atom we can see that p is a binary predicate (i.e., its arity is two), and that both its arguments are of type int.

The arguments of a fact must be expressions that evaluate to values. In particular, none of them may contain variables (such variables would be unbound).

The type of each argument must be the type of the corresponding position of tuples in the predicate.

Example 10.3. Bad facts

p(3 + x, 8).

The above will be rejected by the system (with an appropriate diagnostic message), because x is not a value: it is an unbound variable (see the section called “Bound variables and their instantiations”).

p("alpha", "beta").

If we had already submitted the fact in Example 10.2, “A fact”, then the above will be rejected, because p has been implicitly declared as

p(x, y) -> int(x), int(y).

The possibility of implicitly declaring a predicate by supplying a fact is a special case of the mechanism described in Section 11.1.1, “Predicate Inference”. Please note that in this case the implicit declaration is that of an IDB predicate (see the section called “Kinds of rules”).

As noted in Chapter 8, Predicates, predicates contain sets of tuples. It is not an error to have a number of facts that correspond to the same tuple, but the predicate will contain only one of those tuples.

Example 10.4. Predicates do not contain duplicates

p(1 * 2, 2 * 2).
p(2 * 3, 3 * 3).
p(2 * 1, 2 + 2).
p(3 * 2, 3 + 3).

If the above is all the information that we have about predicate p, then p will contain only three tuples:

p(2, 4).
p(6, 9).
p(6, 6).

10.1.2. Atoms in heads of rules

Rules are described in Chapter 11, Rules.

An atom in the head of a rule is not dissimilar to a fact. There are two main differences:

The atom may be thought of as a shorthand for the set of facts to which it can be converted by systematically replacing its variables with those of their instantiations for which the body is true.

(The careful reader will notice that a fact can be regarded as a degenerate form of a rule: one where the non-existent body is trivially true.)

Example 10.5. A simple rule

q(0). q(1). q(2).

r(x + y, x * y) <- q(x), q(y).

If these are all the facts for q, and q will not change, then the rule is equivalent to the following set of facts:

r(0, 0).
r(1, 0).
r(2, 0).
r(2, 1).
r(3, 2).
r(4, 4).

(In the above, we have removed duplicate facts that would have no effect: see Example 10.4, “Predicates do not contain duplicates”.)

Of course, the advantage of using the rule is that it will cause the system to automatically update the contents of predicate r whenever tuples are added to (or removed from) q.

Example 10.8, “An illustration of the use of atoms” might make things a little more clear.

10.1.3. Atoms in bodies of rules

Rules are described in Chapter 11, Rules. To simplify this introductory description, we will assume that none of the atoms discussed here is in the scope of a negation. Negated atoms will be discussed in the section called “Negation”.

An atom in the body of a rule is either true or false, depending, in general, both on its form and on the contents of the database. This is clarified below.

An atom in the body is true if and only if it matches at least one of the tuples that are in the database and belong to the predicate named by the atom.

An atom matches a tuple if each of its arguments matches the value in the corresponding position of the tuple, as follows:

  • If the argument is an expression that does not contain uninstantiated variables, then it matches a value v if and only if the value of the expression is identical to v.
  • If the argument contains a variable x, the attempt to match will involve an attempt to instantiate x, so that the value of the entire argument will become identical to the corresponding value in the tuple: if such an instantiation can be found, the match will be successful. Once the variable is instantiated, all its other occurrences are effectively replaced by its value.

This is perhaps easier to understand if one treats the expressions in an atom as syntactic sugar, as shown in the following example:

Example 10.6. Expressions in the arguments of a body atom

The rule

q(x) <- p(x, x * x). 

is equivalent to

q(x) <- p(x, y), y = x * x. 

In the second version, (x, y) is matched against all the tuples of p, thus instantiating variables x and y. The resulting instantiations are accepted only if they satisfy y = x * x, and q is populated only with those instantiations of x that form a part of the accepted instantiations. These are exactly the instantiations of x for which p(x, x * x) is true.

See Chapter 11, Rules and the section called “Conjunction and Disjunction”. See also Example 10.7, “Instantiating a collection of variables”.

In general, an atom may match a number of tuples. If the process of matching involves instantiating some variables, we may consider each variable as being instantiated to a set of values, as discussed in the section called “Bound variables and their instantiations”. This, however, is a simplification. If the atom contains occurrences of two or more variables, then we should not think of each variable as being instantiated independently: it is, rather, the entire collection of variables occurring in the atom that is being instantiated. This is illustrated by the example below.

Example 10.7. Instantiating a collection of variables

p(1, 3).  p(2, 4).

q(x * y) <- p(x, y).

The predicate q will contain two values: 3 and 8. This is because x is instantiated to 1 only when y is instantiated to 3, and to 2 only when y is instantiated to 4.

In other words, the atom in the body can be thought of as instantiating an ordered tuple (x, y): the instantiation consists of the set{(1, 3), (2, 4)}. This is essentially equivalent to the following table in a relational database:

x y
1 3
2 4

If we regarded the atom as instantiating the variable x to {1, 2} and the variable y to {3, 4}, then we would incorrectly think of q as containing 3, 4, 6 and 8.

As we can see from the example and the preceding discussion, an atom in the body of a rule may be regarded as playing two roles:

  • it is a filter that rejects those tuples of the named predicate that do not match the arguments;
  • it is a generalized projection operation that extracts a table of instantiations for the variables that occur in its arguments.

The following example might help to illustrate the three uses of atoms. See Chapter 11, Rules for more information.

Example 10.8. An illustration of the use of atoms

p(1, 2).  p(1, 3).  p(2, 4).  p(4, 5).  p(5, 5).

q(x, x * 2) <- p(x, x + 1).

r(x) <- p(x - 1, x).

s(x) <- p(x - 1, x + 1). 

Assume the predicate p contains only tuples declared explicitly by the facts above, i.e.,

(1, 2)
(1, 3)
(2, 4)
(4, 5)
(5, 5)

Then the predicate q will contain the following tuples:

(1, 2)
(4, 8)

This is because the atom in the body of the rule for q matches only

(1, 2)
(4, 5)

so x can be thought of as instantiated to the set {1, 4}.

It is now clear that predicate r will contain the values (one-tuples) 2 and 5, while s will contain 2 and 3.

It should be noted that the expressions that may be used for matching-and-instantiating must be relatively simple. For example, the following rule will not be accepted by the LogicBlox compiler, even though we might have no trouble determining what tuples should belong to t (given the definitions in Example 10.8, “An illustration of the use of atoms”):

t(x, y) -> int(x), int(y).

t(x, y) <- p(x - y, x + y).

By contrast, the following is quite acceptable (though not very useful):

t(x, y) <- p(x, x + y).

The compiler will usually provide us with sufficient explanations if we get carried away and write things that it cannot handle.

An outline of an explanation for the curious.  Expressions in arguments are just syntactic sugar. The compiler converts an atom such as p(x, x + y) into

p(x, z), z = x + y

Matching (x, z) against the tuples in predicate p is trivial. Since x and z are bound, the compiler can make y bound by rewriting z = x + y to y = z - x. It is not difficult to see that in the case of p(x - y, x + y) such simple rewriting will not make y bound. We could instantiate y to the set of all integers, and then use p as a filter, but that is not a practical proposition.

10.1.4. Functional atoms

FunctionalAtom = FunctionalExpression "=" Expression
               | PredicateDescriptor "(" KeyArguments ";" ValueArguments ")"
               | PredicateDescriptor "(" KeyArguments ";" )"
               | PredicateDescriptor "(" ";" ValueArguments ")"
               .

FunctionalExpression = PredicateDescriptor "[" [ KeyArguments ] "]" .

KeyArguments   = Expressions .
ValueArguments = Expressions .

Expressions = Expresssion { "," Expression } .

PredicateDescriptor = PredicateName [ "@" Suffix ] .
PredicateName       = Identifier .
Suffix              = Identifier .

Functional atoms of the first kind have the syntactic form of comparisons (see Section 10.2, “Comparisons”). We list them here, because semantically they are atoms.

A functional atom is used to refer to a functional predicate (see Section 8.2, “Functional Predicates”). As always, if the atom occurs in the head of a rule (or in a fact), then the PredicateDescriptor must be a simple PredicateName.

If the functional predicate has only one value argument, we use the first form, as in the following example:

Example 10.9. Single-valued functional atoms

The following program declares and populates two functional predicates, f and g.

create --unique

addblock <doc>
  f[x] = y -> int(x), int(y).
  g[x] = y -> int(x), int(y).

  f[1] = 2.
  f[2] = 4.
  f[3] = 6.

  g[x + 1] = f[x] * 3.
</doc>
print g

close --destroy

This results in

created workspace 'unique_workspace_2017-01-14-23-54-28'
added block 'block_1Z1B35MR'
2 6
3 12
4 18
deleted workspace 'unique_workspace_2017-01-14-23-54-28'

This form of functional atom can be thought of as convenient syntactic sugar for a basic atom. One must not forget, however, that by using it in a declaration we also trigger the automatic generation of constraints that ensure the predicate will always be a function (i.e., will contain at most one tuple for each combination of the key arguments). Moreover, functional notation cannot be used for predicates that have not been declared to be single-valued functions.

Example 10.10.  Variants of Example 10.9, “Single-valued functional atoms”

create --unique

addblock <doc>
  f(x, y) -> int(x), int(y).
  g(x, y) -> int(x), int(y).

  f(1, 2).
  f(2, 4).
  f(3, 6).

  g(x + 1, y * 3) <- f(x, y).
</doc>
print g

close --destroy

To ensure that f and g are functions, one could also do this:

create --unique

addblock <doc>
  f[x] = y -> int(x), int(y).
  g[x] = y -> int(x), int(y).

  f(1, 2).
  f(2, 4).
  f(3, 6).

  g(x + 1, y * 3) <- f(x, y).
</doc>
print g

close --destroy

It is strongly recommended that such a mixture of styles be avoided. We should use the style shown in Example 10.9, “Single-valued functional atoms”.

The second form of functional atoms is used to reference multi-valued functional predicates (see the section called “Multi-valued functional predicates”). They are exactly like basic atoms, except that the list of key arguments is separated from the list of value arguments by a semicolon. Using such an atom in a declaration ensures that the predicate will indeed be a function. When used elsewhere, the atom can be replaced with a corresponding basic atom, but this is not recommended.

Example 10.11. Multi-valued functional atoms

The following is a declaration of a multi-valued functional predicate:

m(a ; b, c) -> int(a), int(b), int(c).

The following two facts add two tuples to m. (Notice that there is no semicolon in the second one: this is legal, but not recommended.)

m(1; 2, 3).
m(11, 2, 3).

However, if we now tried to add m(1; 3, 4)., we would get an error message that begins with

Error: Function cannot contain conflicting records: attempt to insert [1,3,4,1], but conflicting record [1,2,3,1] exists.

Example 10.12. Functional atoms without key arguments

The following creates (and implicitly declares) a multi-valued functional predicate with no key arguments. Since there is only one (implicit) key, such a predicate can contain only one tuple, so it is effectively a constant pair of values.

n(; 2, 3).

The following two forms may be used to retrieve the two values:

n(; x, y)
n(x, y)

10.1.5. External diff atoms

ExternalDiffAtom = ExternalDiffSpecifier "(" [ ArgumentList ] ")"
                 | ExternalDiffSpecifier "[" [ ArgumentList ] "]" "=" Expression
                 .

ExternalDiffSpecifier = "(" PredicateDescriptor "\" PredicateDescriptor ")" .

PredicateDescriptor = PredicateName [ "@" Suffix ] .
PredicateName       = Identifier .
Suffix              = Identifier .

ArgumentList = Expression { "," Expression } .

An external diff (or ediff) atom is a reference to an external diff predicate: see Section 8.11, “External Diff Predicates”. An ediff atom can occur only in the body of a transaction-lifetime delta rule. An external diff predicate is computed only when it is referred to by some ediff atom.

The predicate name in both occurrences of PredicateDescriptor must be the same.

The suffix can be the name of a branch (Chapter 41, Database Branching) or of a transaction stage (either previous or initial, see Section 19.4.4, “Stage suffixes”). A PredicateDescriptor has only one suffix, so it can refer to a particular stage only on the current branch. A predicate name p without a suffix is equivalent to p@initial.

10.2. Comparisons

Comparison         = Expression ComparisonOperator Expression .
ComparisonOperator = "=" | "!=" | "<" | ">" | "<=" | ">=" .

A comparison formula compares two expressions with each other. The two expressions must have the same type.

If the comparison operator is equality (=), then the formula is true if the two values are equal. If the operator is a disequality (!=), the formula is true if the two values are different. Equality and disequality can be used to compare two values of any type, either a primitive type or an entity type.

The operators < (less than), > (greater than), <= (less or equal), and >= (greater or equal) can be applied only to ordered primitive types, such as numbers, strings, and dates. Strings have a lexicographic ordering, e.g., "Ann" < "Bob" and "Ann" < "Anne".

A formula with a single comparison operator is just a more convenient notation ("syntactic sugar") for an atom that refers to a built-in predicate: see the section called “Comparison Operations”.

Note

A single-valued functional atom (see Section 10.1.4, “Functional atoms”) has a syntactic form that is indistinguishable from that of a comparison, but the two are quite different. For example, for integer x and y the comparison x * 2 = y - 1 is syntactic sugar for the atom int:eq_2(x * 2, y - 1), while the functional atom f[x * 2] = y - 1 is syntactic sugar for f(x * 2, y - 1).

10.2.1. Chained Comparison Formulas

Formula = Expression ComparisonOperator Expression
             { ChainComparisonOperator Expression } .

ChainComparisonOperator = "<" | ">" | "<=" | ">=" .

Ordered comparison operators may be chained. This is just a more convenient notation ("syntactic sugar") for a conjunction of simple comparison formulas (see the section called “Conjunction and Disjunction”).

Example 10.13. Chained comparison with the same operator

3 < 4 < 5

The above formula evaluates to true, because it has the same meaning as:

3 < 4, 4 < 5

Example 10.14. Chained comparison with different operators

3 < 4 > 2

Similarly to the previous example, the above formula has the same meaning as:

3 < 4, 4 > 2

The first comparison operator in a chained comparison formula can be = or !=.

Example 10.15. (In)equality in chained comparison

5 = 3 < 5
5 != 3 < 4

The first formula above evaluates to false, while the second evaluates to true.

10.3. Complex Formulas

Atoms can be composed into more complex formulas by means of logical operators. There are three logical operators: conjunction, disjunction, and negation.

Conjunction and Disjunction

Formula = Formula ("," | ";") Formula .

A conjunction is written as two formulas separated by a comma (,). A conjunction is true whenever both constituent formulas are true.

Example 10.16. Conjunction

3 < 4, 4 < 5   // true, because both are true
3 < 4, 4 > 5   // false, because only the first is true

A disjunction is written as two formulas separated by a semicolon (;). A disjunction is true if at least one of the two formulas is true.

Example 10.17. Disjunction

3 < 4; 4 > 5  // true, because the first of the two is true
3 < 4; 4 < 5  // true, because both are true

The precedence of the disjunction operator (;) is lower than that the conjunction operator (,).

Example 10.18. Combining conjunction with disjunction

The following two rules are equivalent:

p(x, y) <- q(x), r(y) ; s(y), t(y, x).
p(x, y) <- (q(x), r(y)) ; (s(y), t(y, x)).

Each of these rules is equivalent to the following two rules:

p(x, y) <- q(x), r(y).
p(x, y) <- s(y), t(y, x).

To get rid of the disjunction from the following rule

p(x, y) <- q(x), (r(x, y); s(y, x)).

we would have to introduce an auxiliary predicate

p(x, y) <- q(x), t(x, y).
t(x, y) <- r(x, y).
t(x, y) <- s(y, x).

Please note that the usual convention is to write a space after, but not before, the comma. We sometimes make the semicolon more visible by adding extra whitespace, as in the first example above.

Both the conjuncts (disjuncts) may contain occurrences of the same variables.

If there is only one common variable, and we consider a variable as a set of all its instantiations, then for that variable the conjunction (disjunction) corresponds roughly to the intersection (union) of the sets of instantiations for which the conjuncts (disjuncts) are true.

Example 10.19. Conjunction and disjunction: the simplest case

p(1). p(2). p(3).
q(2). q(3). q(4).
r(3). r(4). r(5).

s(x) <- p(x), q(x), r(x).

t(x) <- p(x); q(x), r(x).

The predicate s contains only 3.

The predicate t contains 1, 2, 3 and 4 (but not 5).

In general the situation is more complicated. As discussed in Example 10.7, “Instantiating a collection of variables”, an atom in the body of a rule instantiates a tuple of variables to a set of tuples, i.e., it essentially produces a relation ("table") similar to the ones used in relational databases (the main difference being that LogiQL has set semantics, while SQL has multiset semantics). Given this view, conjunction can be thought of as corresponding to a generalised natural join; disjunction would then be a generalised union. This is illustrated by the following example.

Example 10.20. Conjunction and disjunction: a more general case

p(1, 3).   p(2, 4).   p(2, 20).
q(1, 10).  q(2, 20).  q(3, 30).

r(x + y + z) <- p(x, y), q(x, z).

s(x + y + z) <- p(x, y), z = 0; q(x, z), y = 0.

The predicate r contains the values 14. 26 and 42. In this case the conjunction acts as a natural join. Given the following tables:

x y
1 3
2 4
2 20
x z
1 10
2 20
3 30

we produce

x y z
1 3 10
2 4 20
2 20 20

The predicate s contains 4, 6, 11, 22, and 33. In this case the disjunction is equivalent to the union of the following two tables:

x y z
1 3 0
2 4 0
2 20 0
x y z
1 0 10
2 0 20
3 0 30

The union is

x y z
1 3 0
2 4 0
1 0 10
2 0 20
2 20 0
3 0 30

and the duplicate 22 was removed from s. In general, both the join and the union will always be sets (i.e., will contain no duplicate tuples).

Note that in the rule for s we had to add explicit instantiations for z and y: otherwise the compiler would have complained about unbound variables. The rule is equivalent to:

s(x + y + z ) <-  p(x, y), z = 0.
s(x + y + z ) <-  q(x, z), y = 0.

Negation

Formula = "!" Formula .

A negation holds when the negated formula is false. For example, !(0 > 1) is true.

Example 10.21. Negations

!p(x, y)
!(p(x), q(x))

Negation has higher precedence than conjunction, and conjunction has higher precedence than disjunction. However, negation has a lower precedence than a comparison operator.

Example 10.22. Precedence of negation, disjunction and conjunction

p(); q(), r()  // a disjunction: equivalent to p(); (q(), r())
!a(), b()      // a conjunction: equivalent to (!a()), b()
! f[x] = y     // a negation:    equivalent to !(f[x] = y)

If we allowed the negated formula to produce instantiations for a variable, then negation would be tantamount to taking the complement of the set of instantiations. This would, in general, be too expensive (and sometimes even impossible).

Example 10.23. No binding under negation

Given the declarations

p(a)     -> int(a).
q(a)     -> int(a).
f[a] = b -> int(a), int(b).

the rule

p(x) <- ! f[7] = x.

would not be accepted by the compiler (the diagnostic message being variable 'x' is not bound; it must be used outside a negation). Indeed, the instantiation of x would consist of the entire set of integers, except the one which is the value of f[7].

The following, however, would be accepted, because of the binding occurrence of x in q.

p(x) <- ! f[7] = x, q(x).

For this reason a LogiQL rule must satisfy the following condition: all variables that appears in the head must be positively bound. "Positively" means simply: in a formula that is not negated.

A more precise statement of this rule would be: every variable that occurs in the head must have a binding occurrence outside the scope of a negation.

(A brief explanation for the curious: a variable that has a binding occurrence outside the scope of a negation may also have binding occurrences inside the scope of a negation, but the compiler will ensure that these will not actually produce any instantiations. There is a distinction between so-called iterable positions of a variable, which are used to actually extract instantiations from the database, and searching positions, which are used to check for the presence of already-extracted instantiations, by means of an index. The latter are allowed inside negations.)

A bound variable is usually positively bound. There is an exception in the case of variables that have no occurrences outside the scope of a negation.

The instantiations of a variable whose occurrences appear only in the scope of a negation are not "exported" outside the negation, so there is no conceptual or major practical difficulty in allowing it to be instantiated there. However, for somewhat obscure technical reasons, in LogiQL this is allowed only if the binding occurrence is in the value position of a functional predicate.

Example 10.24. A legal use of negatively bound variable

p(a)     -> int(a).
q(a)     -> int(a).
f[a] = b -> int(a), int(b).

p(x) <- !(f[x] = y, y < x), q(x).

The rule above is accepted by the compiler. Variable y has only a negative binding occurrence, but that is in the value position of f. Note that the argument of f is bound by the occurrence in q(x).

The rule has a somewhat artificial form, because we wanted to keep the example simple. This particular rule would normally be written as

p(x) <- ! f[x] < x, q(x).

Example 10.25. An illegal use of a negatively bound variable

p(x)    -> int(x).
q(x)    -> int(x).
s(x, y) -> int(x), int(y).

p(x) <- !(s(x, y), y < x), q(x).

The rule above is not accepted by the compiler, which produces the following error message: existentially quantified variable 'y' occurs negatively in an iterable position.

For this simple example this is not a real limitation, since the rule can be rewritten to a legal one by introducing an auxiliary predicate:

t(x) <- s(x, y), y < x.
p(x) <- !t(x), q(x).

Unfortunately such rewriting is not always possible: see Example 11.12, “IDB rules and general recursion”.

It is worth noting that in some cases negation in LogiQL is not quite the same as what one might naively expect. This is illustrated by the following table.

Table 10.1. Treatment of negation and equality

Scenario Observations
A[x] = α, B[x] = α A[x] = B[x], !(A[x] != B[x])
A[x] = α, B[x] = β, α ≠ β !(A[x] = B[x]), A[x] != B[x]
A[x] = α, B[x] undefined !(A[x] = B[x]), !(A[x] != B[x])
A[x] undefined, B[x] = α !(A[x]=B[x]), !(A[x] != B[x])
A[x] undefined, B[x] undefined !(A[x] = B[x]), !(A[x] != B[x])

The last three examples are particularly instructive. Because either A[x] or B[x] (or both) is missing, the checks for equality and disequality will fail. The outer negation operations will therefore succeed.

Please note that these examples do not violate classical logic. For example, !(A[x] = B[x]) is actually shorthand for there does not exist a y such that A[x] = y and B[x] = y, which is not the same as A[x] != B[x].

Tip

The interaction of negation and equality/disequality is slightly different in LogicBlox 4.x than in earlier releases. In LogicBlox 4.x (A[x] != B[x]) always has the same meaning as (B[x] != A[x]).

Parenthesized Formulas

Formula = "(" Formula ")" .

A formula surrounded by parentheses is also a formula. The two formulas have the same truth value.

Example 10.26. Parenthesized Formulas

(p(); q()), r() // this is a conjunction