Chapter 16. Constraints

A LogiQL constraint is a language construct used to express an invariant property of a program. There are two types of constraints in LogiQL:

  • those that are statically checked by the compiler to always hold for any database instance;
  • those that are dynamically checked at runtime: a violation of such constraints will cause a transaction to abort.

The statically checked constraints are predicate declarations; in order to be recognized by the compiler as such, they must follow the specific format described in Section 16.3, “Constraints as Predicate Declarations”. Dynamic constraints are enforced whenever the state of the database changes: see Chapter 19, Transaction Logic.

When the system detects a constraint failure, the diagnostic message may be somewhat difficult to read. See the section called “Internal use of pulse predicates” for a short explanation and a concrete example.

16.1. Syntax and Interpretation

Constraints are sometimes called right-arrow rules because they most often take the following form:

Constraint = Formula "->" Formula "." .

Note that the arrow (->) points to the right.

The interpretation of a constraint is that whenever the formula on the left-hand-side of the arrow holds, the formula the right-hand-side of the arrow must hold as well.

A constraint of the form f1 -> f2 can thought of as equivalent to !(f1, !f2) (i.e., it is not the case that f1 holds, but f2 does not). You may see variants of the latter form in runtime error reports issued when a constraint violation is detected.

16.2. Common Forms of Constraints

The following table lists common forms of constraints:

Name Description Example
Equality constraint A restriction to ensure that the population of one or more predicate roles must be equal to the population of other roles (in this predicate or in another predicate). Patient p has a diastolic blood pressure reading if and only p has a systolic blood pressure reading.
diastolicBPof[p] = _ -> systolicBPof[p] = _.
systolicBPof[p] = _ -> diastolicBPof[p] = _.
Exclusion constraint A restriction on two or more roles to ensure that no tuple may instantiate more than one of those roles at the same time. No person authors and reviews the same book.
reviews(p, b) -> !authors(p, b).
Inclusive-Or constraint A restriction on two or more roles played by instances of a common type to ensure that each instance of that type plays at least one of those roles. Each valued employee is industrious or intelligent.
ValuedEmployee(p) -> isIndustrious(p) ; isIntelligent(p).
Exclusive-Or constraint A restriction on two or more roles played by instances of a common type to ensure that each instance of that type plays exactly one of those roles. Each person is male or female but not both.
Person(p) -> isMale(p) ; isFemale(p).
isMale(p) -> !isFemale(p).
Frequency constraint A restriction on a list of one or more roles to ensure that, at any given time, each instance in the population of that role list appears there a specified number of times. Each reviewer is assigned at most three papers to review.
positiveNrPapersAssignedTo[r] = n <-
    agg<<n = count()>> isAssigned(r, _).
positiveNrPapersAssignedTo[_] = n -> n <= 3.
Uniqueness constraint A restriction on a list of one or more roles to ensure that, at any given time, each instance in the population of that role list appears there at most once. (This is an important special case of a frequency constraint.) Each passport number is held by at most one person.
passportNrOf[p1] = n, passportNrOf[p2] = n ->
    p1 = p2.
Mandatory role constraint A restriction on a single role of a predicate to ensure that each instance in the population of the role’s type must play that role. Each person was born on some date.
Person(p) -> birthdateOf[p] = _.
Ring constraint A logical constraint on two type-compatible arguments of a predicate. Kinds of ring constraints include irreflexivity, asymmetry, intransitivity and acyclicity. No person is her/his own parent. (This is an example of an irreflexivity constraint.)
!isParentOf(p, p).
Subset constraint A restriction to ensure that the population of one or more predicate roles must be a subset of the population of other roles. If student s passed course c then s was enrolled in c.
passed(s, c) -> enrolledIn(s, c).
Value constraint A restriction on a role that specifies what values can populate that role. (This may, but need not, take the form of an Inclusive-Or constraint.) Possible gender codes are “M” and “F”.
hasGenderCode(_:gc) -> gc = "M" ; gc = "F".

Example 16.1. Constraints for a partial order

In the first block we introduce constraints that ensure the predicate leq is a partial order. (We assume leq can be defined only on a subset of items, which makes for a more interesting reflexivity constraint.)

In the exec block we add two tuples explicitly, and use delta rules to add those that must be there to satisfy the constraints.

create --unique

addblock <doc>

  item(x), item:nr(x:n) -> int(n).         // an entity type

  item:nr(_:n) <- int:range(0, 9, 1, n).   // populated

  // A partial order among items:
  leq(x, y) -> item(x), item(y).

  leq(x, _) ; leq(_, x) -> leq(x, x).      // reflexive
  leq(x, y) -> !(leq(y, x), x != y).       // antisymmetric
  leq(x, y), leq(y, z) -> leq(x, z).       // transitive

</doc>

exec <doc>
  // Introduce ordering among some items:
  +leq(x, y) <- item:nr(x:1), item:nr(y:2).
  +leq(x, y) <- item:nr(x:0), item:nr(y:1).

  // Ensure reflexivity and transitivity:
  +leq(x, x) <- +leq(x, _) ; +leq(_, x).
  +leq(x, z) <- +leq(x, y), +leq(y, z).
</doc>
print leq

close --destroy

The results are:

created workspace 'unique_workspace_2017-06-05-21-37-48'
added block 'block_1Z1FGZTM'
[10000000004] 1 [10000000004] 1
[10000000004] 1 [10000000007] 2
[10000000005] 0 [10000000004] 1
[10000000005] 0 [10000000005] 0
[10000000005] 0 [10000000007] 2
[10000000007] 2 [10000000007] 2
deleted workspace 'unique_workspace_2017-06-05-21-37-48'

If we comment out, say, the last rule in the exec block, we will see:

Error: Constraint failure(s):
block_1Z1FGZTM:6(3)--6(35):
    false <-
      Exists x::item,y::item,z::item .
         leq(x,y),
         leq(y,z),
         !(
            leq(x,z)
         ).
(1) x=[10000000005],y=[10000000004],z=[10000000007]

16.3. Constraints as Predicate Declarations

As described in Chapter 8, Predicates, predicate declarations have the syntactic form of constraints. A constraint is considered a predicate declaration if it satisfies the following specific requirements:

Left-hand side of the right-arrow symbol

The left-hand side of the right-arrow (->) determines what predicates are being declared. It must be one of the following:

  • a single atom, in which case the predicate of that atom is being declared;
  • two atoms, in which case an entity is being declared along with its reference mode predicate.

If the left-hand side is a single atom, then every argument of the atom must be a distinct variable.

If it is a conjunction of two atoms, one atom must declare the entity predicate, and it must be of the form p(x) for some predicate p and variable x. The other atom must declare the reference-mode predicate, and it must be of the form q(x : id), where x is the variable that is used in the first atom and id is the reference mode variable (see below).

Right-hand side of the right-arrow symbol

The right-hand-side of the right-arrow (->) may be either empty, or a conjunction of atoms.

If the left-hand side is a single unary atom, then the right-hand side is allowed to be empty: the constraint is then a top-level entity declaration.

If the left-hand side is a single atom and the right-hand side is not empty, then every variable that appears on the left-hand side must also appear in a unary atom on the right-hand side: each such unary atom forms the type bound of the variable it contains.

If the left-hand side contains a conjunction of two atoms, meaning that it declares an entity and its reference mode predicate, then the right-hand side must contain exactly one unary atom that provides a type bound for the reference mode variable.

All variables that appear on the right-hand side of the constraint must also appear on the left-hand side.

It is possible to have more than one declaration for the same predicate. Those multiple declarations can be exact duplicates, or some of them can be more specific than others, or they can each provide different information about the predicate.

Example 16.2. Examples of predicate declarations

earnings(r, a) -> region(r), int(a).
expenditures(r, _) -> region(r).
expenditures(_, a) -> int(a).
expenditures(_, a) -> int(a), a >= 0.
person(x), person:eid(x:id) -> int(id).
region(r) -> area(r).
area(r) -> .
success() -> .

Note that even though all of the above constraints can be used to determine the types of predicates, some of them cannot be completely statically guaranteed. For instance, the compiler cannot guarantee statically that each expenditures tuple has a number greater than or equal to 0 as its second value. This type of constraint is checked at runtime.