Formulas

Formulas are expressions that evaluate to either true or false. In Rel true and false are zero-arity relations: see Boolean Constant Relations. So the values of formulas, just like the values of other expressions, are relations.

Formulas are often used not only for their values, but also for their effects on variables. For example, if P and Q are unary relations, then the formula P(x) and Q(x) constrains the variable x to be a member of both P and Q. The formula will evaluate to false only if there are no such common members.

Sometimes a formula cannot be evaluated. For example, the formula forall(x in Int : exists(y in Int : y = x + 1)) cannot be evaluated, because its variables range over infinite sets. In such cases Rel will typically provide an informative error message.

Formulas are the core of the Rel language. This means that other constructs are compiled to formulas.

Just as in first-order logic, a formula with free variables cannot be true or false. In this context it is worth knowing that variables appearing on the left-hand side of a definition are implicitly universally quantified. This is also the case for variables that appear in the “bindings” part of a relational abstraction.

For example, you can read def P(x, y) = Q(x) and R(y) as “for every x and y, x and y are in relation P if x is in relation Q and y is in relation R.”

To give another example, in def P(x) = Q(x, y) the variable x is universally quantified, but y is free, so the compiler will complain about y being undefined. This can be fixed by quantifying it explicitly: def P(x) = exists(y : Q(x, y)). Rel also has another syntax for this: def P(x) = Q(x, y) from y. A more convenient solution is to use an anonymous variable: def P(x) = Q(x, _). The identifier _ represents a fresh variable that is implicitly existentially quantified.

Note: In the example above it was assumed that y is a variable. It could also be a relation — see Relational Application.

Boolean Constant Relations

Expr := "true"
      | "false"
      | "{()}"
      | "{}"

The constants true and false are relations, not scalar values. The constant true is equivalent to {()}, which is the zero-arity relation containing the only value of arity 0, i.e., the empty tuple. The constant false is equivalent to the relation {} — the empty set. You can consider the empty set as a zero-arity relation. These are the only two relations of arity 0.

Because true and false are relations, there is never a relation persisted in the database that has true or false occurring as a value in the tuples — otherwise that relation would not be first-order.

The Rel compiler statically eliminates any occurrences of true and false according to the laws of the language.

Rel also provides a data type, Boolean, whose values are boolean_true and boolean_false. This is useful mostly when importing data. If you use it outside that context you will usually find that there are better and more idiomatic ways to achieve your goal in Rel.

Relational Application

Expr := Expr "(" (Expr {"," Expr}*)? ")"

A relational application is sometimes referred to as an atom. It should not be confused with a partial relational application, which is written with square brackets instead of parentheses.

The first expression denotes a relation. The other expressions, if any, are the arguments. They often correspond to the parameters of a definition or of a relational abstraction.

The arity of the resulting expression must be 0. For example, if the arity of P is 3, then in P(x, y, z) all three arguments are necessary.

If the arity of P is 3, then the formula P(x, y) will evaluate to false because there is no binary tuple in P.

Note, however, that in general a Rel relation might not have a fixed arity, that is, it may contain tuples of different lengths. If the relation P does not have a fixed arity, then both P(x, y, z) and P(x, y) may evaluate to true.

The section Partial Relational Application introduces a syntax with square brackets that supports partial application of a relation. For example, age["Martin"] has the value {(39)}.

A name that consists of an identifier immediately followed by one or more Symbols is shorthand for a partial relational application. For example, person:address:city(x, y) is equivalent to person[:address][:city](x, y), which is equivalent to person(:address, :city, x, y).

Some relational applications can be expressed with infix operators. For example, {(5,)}(x) can be written as x = 5, and add(x, y, z) as z = x + y.

An expression such as x = y is also a relational application. It is just a convenient notation for eq(x, y).

There is also a special form of relational application, x in P, which is conceptually — though not syntactically — equivalent to P(x). See Bindings for more information.

Evaluation

The evaluation of a relational application can be described as follows:

• The applied relation is filtered by selecting the subset of tuples that match the arguments.
• If the selected subset is empty, the relational application evaluates to false.
• If the selected subset is not empty, the relational application evaluates to true. Additionally, if any of the arguments are variables, then these variables are constrained to the sets of values in the corresponding positions of the selected tuples. If two or more arguments are variables, the variables are constrained together.

This is illustrated with relational applications of the relation P defined below:

// model
 
def P = {
  (1, 1);
  (1, 2);
  (2, 2);
  (2, 3)
}

The relational application P(x, 1) selects those tuples whose second element is 1, and constrains x to be one of the first elements of the selected tuples. In this case the only such tuple is (1, 1):

// read query
 
def output(x) = P(x, 1)

The relational application P(x, x) selects the tuples whose two elements are equal, and constrains x to the set of data values contained in the selected tuples. In this case the selected tuples are (1, 1) and (2, 2):

// read query
 
def output(x) = P(x, x)

The relational application P(x, x + 1) selects every tuple whose second element is greater by 1 than the first element, and constrains x to the set of the first elements of the tuples with that property. In this case the selected tuples are (1, 2) and (2, 3):

// read query
 
def output(x) = P(x, x + 1)

The relational application P(x - 1, x) selects the same tuples, but constrains x to the set of the second elements of the selected tuples:

// read query
 
def output(x) = P(x - 1 , x)

If x and y are not constrained by anything else, then the relational application P(x, y) selects all the tuples of P and constrains the pair x and y to the set of these tuples. The variable x represents the first element of each tuple, while the variable y represents the second element:

// read query
 
def output(x, y) = P(x, y)

When taken separately, however, each of the variables can be thought of as representing the corresponding column of P. For instance:

// read query
 
def output(x) = exists(y : P(x, y))

The example below illustrates how constraining several otherwise ungrounded variables may be regarded as a projection of the relation consisting of the selected tuples onto the positions in which those variables appear:

// read query
 
def Q = (1, 2, 3); (1, 3, 3); (2, 2, 4); (2, 3, 5)
 
def output(x, y) = Q(x, 2, y)

The relational application Q(x, 2, y) selects the tuples whose second element is 2, thus forming the intermediate relation {(1, 2, 3); (2, 2, 4)}. This relation is then projected onto the positions of x and y, that is, the second element of each tuple is removed, forming the relation {(1, 3); (2, 4)}. The pair of variables x and y is constrained to the set of tuples in this relation.

If the variables are not otherwise ungrounded but are constrained by other relational applications in a conjunction, then those constraints are taken into account.

Here is what happens when you add and P(z, y) to the previous example:

// read query
 
def Q = (1, 2, 3); (1, 3, 3); (2, 2, 4); (2, 3, 5)
 
def output(x, y, z) = Q(x, 2, y) and P(z, y)

The relational application Q(x, 2, y) constrains y to the set containing 3 and 4, as before. The relational application P(z, y) constrains y to the set containing 1, 2, and 3. The only element in both sets is 3, so y must be 3. The relation P contains only one matching tuple, namely (2, 3), so z must be 2. The relation Q contains only one tuple whose third element is 3 and second element is 2, namely (1, 2, 3), so x must be 1.

Finally, it is worth noting that an argument of a relational application can be a unary relation. The selected tuples will be those whose corresponding element matches any unary tuple of that relation:

// read query
 
def output(x) = P(x, {2; 3})

Grounded Variables

A variable v is said to be grounded when Rel can determine that v represents an element of a finite — possibly empty — set of values. As noted in Evaluation, v is then said to be constrained to that set of values.

If a variable is not grounded, some error messages may inform you that it is “not ground” or “not bound.” These differences currently indicate whether the error was detected by the front-end compiler (“not bound”) or by the back-end optimizer (“not ground”). All these terms refer to the same concept. The term used in this manual is “ungrounded.”

See the Error Code: UNTYPED VARIABLE guide for advice on what to do if the compiler reports that some variables are unbound.

Relational application is the only mechanism through which a variable x can be grounded. If x occurs as an argument of a finite relation, it thereby becomes grounded. If x occurs as an argument of an infinite relation, it will be grounded if there are enough other arguments — either grounded or nonvariable — to make x an element of a finite set. For example, if x occurs only in x = y, then it is grounded if and only if y is grounded. Other examples will be shown below.

Relations such as Int are considered to be infinite, even though, strictly speaking, they are just very large. So x in Int or Int(x) does not ground x.

In the following two examples, x and y are grounded. In the first example both variables occur in relational applications of finite relations. The equality is just an additional constraint. In the second example x is grounded by a relational application of a finite relation, and y is grounded by x = y.

// read query
 
def P {1; 2; 3}
def Q {2; 4; 6}
def output(x, y) {x = y and P(x) and Q(y)}

// read query
 
def P {1; 2; 3}
def Q {2; 4; 6}
def output(x, y) {x = y and P(x)}

In the example below, neither x nor y is grounded, so an error will be raised:

def P {1; 2; 3}
def Q {2; 4; 6}
def output(x, y) {x = y}

The necessity of making variables grounded may make seemingly equivalent models behave differently. For instance, x is grounded here:

// read query
 
def output(x) = {-2; -1; 0; 1; 2}(x) and -2 < x < 2

However, in the following x is ungrounded, which is an error:

def output(x) = Int(x) and -2 < x < 2

Here is a slightly more complicated example:

// read query
 
def small_int = -2; -1; 0; 1; 2
def square_add[x in small_int, y in small_int] = x * x + y
def output(x, y, z) = square_add(x, y, z) and z = -1

Notice that the example above worked, because x and y were constrained to be members of the finite set small_int. If they were not so constrained, there would be an error:

def square_add[x in Int, y in Int] = x * x + y
def output(x, y, z) = square_add(x, y, z) and y = -1 and z = -1

However, the following is fine:

// read query
 
def square_add[x in Int, y in Int] = x * x + y
def output(x, y, z)  { square_add(x, y, z) and x = -1 and z = -1 }

Why does this this example work?

The expression x * x + y is just convenient notation for add[multiply[x, x], y]. The relations add and multiply are infinite. However, the entire definition of square_add is not recursive, so the compiler inlines it automatically at each point of use. In this case the definition of output becomes equivalent to the following:

def output(x, y, z)  {
   multiply(x, x, v) and add(v, y, z) and x = -1 and z = -1
}

The variable x is grounded, so v is also grounded. The second argument of add is ungrounded, but the first and third are grounded. In such a case the compiler’s built-in rules about arithmetic allow it to replace add(v, y, z) with sub(z, v, y). For each pair of values z and v there will be only one possible value of y that satisfies sub(z, v, y), so y is also grounded.

In the previous example, by contrast, the problem of insufficiently grounded arguments occurs in the context of multiplication. Unlike in the case of addition, this cannot be easily resolved because of difficulties with 0: see multiply.

See also the description of annotations @inline and @ondemand in Annotations.

Less Conventional Forms of Relational Application

Note: Most users do not need to be aware of the details described in this section.

Recall from Values that a free-standing data value represents a singleton relation, and that, accordingly, the value of a variable is also a singleton relation.

Since an expression such as {(5,)}(x) is a relational application, so is 5(x). Such an application constrains the value of x to be 5, that is, {(5,)}. So it stands to reason that x(y) is also a relational application. It has the same semantics as x = y, and the latter form is the one that is the most frequently used.

For reasons of general symmetry, x(5) is also a relational application. It can ground x, just as x = 5.

In general, if p is a relation and x is a variable, then the following expressions are equivalent:

• p(x).
• x(p).
• p = x.
• x = p.

This also applies if p is a grounded variable. If x is otherwise ungrounded, then each of the expressions above will ground it:

// read query
 
def P = 1; 3; 5; 6
def Q = 2; 3; 4; 6; 8
def output(x, y, z) = P(x) and Q(y) and x(y) and z(x)

As noted above,5(x) is a valid relational application, regardless of whether this is the only relational application that grounds x. If x is also grounded for other reasons, for instance as in 5(x) and 6(x), then 5(x) is an application of a relation to a relation. The principle of referential transparency requires that 5(6) — in other words, {(5,)}({(6,)}) — also be a relational application. Similarly, given the definitions def P = 5 and def Q = 6, the expression P(Q) must be a valid relational application.

An application of a relation to a relation is not restricted only to singletons. In the case of P(Q) such a restriction might be difficult to enforce at compile time. For general relations P and Q, the meaning of P(Q) is a natural extension of the meaning for singletons. P(Q) is equivalent to exists(x, y : P(x) and Q(y) and x(y)). In other words, the expression evaluates to true if and only if the intersection of P and Q is not empty.

Similar considerations apply to relations with arity greater than 1. For instance, if P is a binary relation, and both Q and R are unary relations, then the application P(Q, R) is equivalent to exists(x, y : P(x, y) and Q(x) and R(y)).

Conjunction

Expr := Expr "and" Expr

This construct is logical conjunction. It evaluates to true if and only if both the left and the right expression evaluate to true.

The arguments of and must be formulas, that is, both must denote relations that have arity 0.

The comma operator can be used instead of and, but is more general in that it does not require arguments of arity 0. If the arguments both have arity 0, the and syntax can help catch mistakes and disambiguate overloaded logic. The arity of e1, e2 can be anything — it depends entirely on the arity of e1 and e2. The arity of e1 and e2, by contrast, is always 0. If e1 and e2are used with an incorrect assumption of their arity, then e1 and e2 will result in an error, whereas e1, e2 will not.

The value of e1 and e2 depends on the values of e1 and e2, as follows:

A simple example:

// read query
 
def P = 1; 2; 3
def Q = 2; 3; 4
 
def output(x) = P(x) and Q(x)

Disjunction

Expr := Expr "or" Expr

This construct is logical disjunction. It evaluates to false if and only if both the left and the right expressions evaluate to false.

The arguments of or must be formulas, that is, both must denote relations that have arity 0.

The semicolon operator is a generalization of or, just like the comma operator is a generalization of and. The semicolon operator computes the union of its arguments. If both the arguments have arity 0, then this is equivalent to disjunction, just as in the case of or. In that case it is better to use or — this can help catch mistakes and disambiguate overloaded logic. For more details, see Semicolon (Union and Disjunction).

The value of e1 or e2 depends on the values of e1 and e2, as follows:

A simple example:

// read query
 
def P = 1; 2; 3
def Q = 2; 3; 4
 
def output(x) = P(x) or Q(x)

Negation

Expr := "not" Expr

This construct is logical negation. It evaluates to true if and only if the negated expression evaluates to false.

The argument of not must be a formula, that is, it must denote a relation that has arity 0.

The value of not e depends on the value of e, as follows:

A simple example:

// read query
 
def P = 1; 2; 3
def Q = 2; 3; 4
 
def output(x) = not P(x) and Q(x)

Note that the following may look like a straightforward variation of the above, but it will produce an error message:

def P = 1; 2; 3
def Q = 2; 3; 4
 
def output(x) = not P(x) or Q(x)

The following will result in an error, too:

def P = 1; 2; 3
def Q = 2; 3; 4
 
def output(x) = not P(x)

The problem is that the relation not P(x) is infinite. In the first example the conjunction constrained x to be a member of Q, but disjunction obviously cannot have such an effect. You can make the domain of x finite in other ways, for example like this:

// read query
 
def P = 1; 2; 3
def Q = 2; 3; 4
def R = range[0, 5, 1]
 
def output(x in R) = not P(x) or Q(x)

Implication

Expr := Expr "implies" Expr

This construct is logical implication: e1 implies e2 is defined as e2 or not e1.

The arguments of implies must be formulas, that is, both must denote relations that have arity 0.

The value of e1 implies e2 depends on the values of e1 and e2, as follows:

A simple example:

// read query
 
def P = 1; 2; 3
def Q = 2; 3; 4
def R = range[0, 5, 1]
 
def output(x in R) = P(x) implies Q(x)

Compare this with the example at the end of Disjunction: P(x) implies Q(x) is exactly equivalent to not P(x) or Q(x).

It is important to note that the meaning of implies is different from the intuitive meaning of the word “implies” in everyday language. When you say “being a fish implies living in water” you usually mean that the set of fish is a subset of the set of creatures that live in water; you do not interpret the statement as saying anything about a bird. Contrast this with the example above: 0 is present neither in P nor in Q, yet it is shown in the results, because not P(0) is true.

To approximate the usual intuitive understanding of implication, you should use universal quantification:

// read query
 
def P = 1; 2; 3
def Q = 2; 3; 4
def R = range[0, 5, 1]
 
def output:A = forall(x : P(x) implies Q(x))
def output:B = forall(x : P(x) implies R(x))

Without an explicit forall it is easy to make a mistake. For instance, you might write:

def P = 1; 2; 3
def Q = 2; 3; 4
def R = range[0, 5, 1]
 
def output:A = P(x) implies Q(x)
def output:B = P(x) implies R(x)

This gives error messages about x being unbound, so you might try to avoid them by binding the variable with from:

// read query
 
def P = 1; 2; 3
def Q = 2; 3; 4
def R = range[0, 5, 1]
 
def output:A = P(x) implies Q(x) from x
def output:B = P(x) implies R(x) from x

The results are quite unexpected, because from introduces existential quantification: P(x) implies Q(x) from x is equivalent to exists(x : P(x) implies Q(x)). This, in turn, is equivalent to exists(x : Q(x) or not P(x)). In other words, this formula will be true if there exists even one value in the domain of x such that Q(x) is true or P(x) is false. In this case such values are 0, 2, 3, 4, and 5.

Comparison Operators

Expr := Expr "<" Expr
      | Expr ">" Expr
      | Expr "=" Expr
      | Expr "!=" Expr
      | Expr "≠" Expr
      | Expr "<=" Expr
      | Expr "≤" Expr
      | Expr ">=" Expr
      | Expr "≥" Expr

Comparison operators are translated into applications of infinite relations defined in the Standard Library. For example, e1 = e2 is translated to eq(e1, e2).

Examples: x < 5, x > 5, x != 0, "abc" < "abd", and 1 < 1.2.

The comparison operators can be used to compare numbers with numbers, or strings with strings. A number can be compared with a string only for equality and inequality.

Two DateTime values can be compared only for equality and inequality. A DateTime value can be compared with a number or a string only for equality and inequality.

Two unary tuples can be compared if their contents can be compared.

Non-unary tuples cannot be compared even for equality.

The comparison operators can be used to compare unary relations. For example, 4 > {1; 2; 3} is true, because there is a number in the relation that is smaller than 4. By contrast, {1; 2; 3} < 1 is false, because there is no number in the relation that is smaller than 1.

The example below applies the same principle:

// read query
 
def P = 1; 2
def Q = 0; 3
def output:LT = Q < P
def output:GT = Q > P

Evaluating the comparison Q < P yields true, because Q contains a data value that is smaller than some data value in P. Similarly, evaluating Q > P also yields true.

The comparison operators cannot be used to compare relations that contain only non-unary tuples. However, if two relations, P and Q, contain unary tuples as well as non-unary ones, then comparison is possible, but will be restricted only to comparing the unary parts of the relations:

// read query
 
def P = 1; 2; (2, 3)
def Q = 2; 1; (1, 2)
def output:EQ = P = Q
def output:LT = P < Q
def output:GT = P > Q

Next: Conditional Expression