# 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`

.

Examples |
---|

`age("Martin", 39)` |

`parent(x, y)` |

`foo()` |

`{(1, 10); (2, 20)}(x, y)` |

`{v, w : P(x) and w = v + 1}(x, y)` |

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.

A relational application consists of two elements: the expression that identifies the applied relation, and the arguments in parentheses.
The two are combined with an implicit operator.
The precedence of this operator is lower than that of the composition operator, `.`

.
So an expression such as `R . Q(x)`

is equivalent to `(R . Q)(x)`

.
If that is not what you want, you should put the relational application in parentheses: `R . (Q(x))`

.

### 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 Error Code: `UNBOUND_VARIABLE`

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.

Examples |
---|

`flying(x) and mammal(x)` |

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 `e2`

are 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:

`e1` | `e2` | `e1 and e2` |
---|---|---|

`false` | `false` | `false` |

`false` | `true` | `false` |

`true` | `false` | `false` |

`true` | `true` | `true` |

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.

Examples |
---|

`flying(x) or floating(x)` |

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:

`e1` | `e2` | `e1 or e2` |
---|---|---|

`false` | `false` | `false` |

`false` | `true` | `true` |

`true` | `false` | `true` |

`true` | `true` | `true` |

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.

Examples |
---|

`not mammal(x)` |

The value of `not e`

depends on the value of `e`

, as follows:

`e` | `not e` |
---|---|

`false` | `true` |

`true` | `false` |

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.

Examples |
---|

`mammal(x) implies drinks_milk(x)` |

The value of `e1 implies e2`

depends on the values of `e1`

and `e2`

, as follows:

`e1` | `e2` | `e1 implies e2` |
---|---|---|

`false` | `false` | `true` |

`false` | `true` | `true` |

`true` | `false` | `false` |

`true` | `true` | `true` |

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.

If `P(x)`

is false, then `P(x) implies Q(x)`

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