Skip to content

Definitions

Definitions give names to relations. As explained in Values, the same name can be given to a number of relations of different types. If that is the case, then it is often convenient to refer to all of those relations as if they were one relation.

General Forms

Declaration :=
     Annotation* "def" Id FormalParamsBracket* FormalParamsParen? "=" Expr
  |  Annotation* "def" Id FormalParamsBracket* FormalParamsParen? "{" Expr "}"
 
Id := Identifier Symbol*
 
FormalParamsBracket := "[" FormalParameterSpecification "]"
FormalParamsParen   := "(" FormalParameterSpecification ")"

Both forms of declaration are equivalent.

The part consisting of the name and the optional bracketed or parenthesized formal parameter specifications is often called the head of the definition. The expression after = (or between { and }) is often called the body of the definition.

You can read a definition as “the head is implied by the body.”

See Annotations for a discussion of the optional annotations. An unannotated definition of a relation will often cause the relation to be materialized, that is, its representation as a set of tuples is computed and stored. If the definition of a relation R depends on other relations, then R is automatically and incrementally updated whenever those relations change. This update process is referred to as maintenance.

There are some exceptions to the rule above, especially when Rel can determine that an infinite relation is meant to perform a simple computation. For instance, the following definition will be inlined by the backend of the system. From the user’s perspective, it is as if the definition were annotated with @ondemand or @inline:

def P(x, result) {result = x * x}

See also Automatic Inlining.

The name that follows def can contain Symbols: for example, name:label. This is just convenient notation for a definition with square brackets. Note that def name:label is equivalent to def name[:label], def person:address:city is equivalent to def person[:address][:city], etc:

// read query
 
def person:address:city = ("John", "Tampa"); ("Amy", "Duluth")
def output = person

See the end of Examples of Definitions for more information on using square brackets.

This manual calls variables introduced in the formal parameter specifications of a definition parameters. It also calls expressions used in the corresponding positions of relational applications arguments.

The definition def P = {} is correct, because {} is an expression that denotes the empty relation. However, its seemingly equivalent form def P {} is syntactically incorrect, because the curly braces are a part of the syntax of the definition, so the body is empty. To achieve the same effect as in the first form, you must write def P {{}}.

Examples of Definitions

ExampleDescription
def five = 5five is a unary, singleton relation {(5,)}.
def numbers = {1; 2; 3; 4}numbers is a unary relation.
def first_four = numbersThe same relation can be given several names.
def grandparent = a, b: ∃(t: parent(a, t) and parent(t, b))grandparent is a binary relation. See Relational Abstraction.
def grandparent(a, b) { ∃(t: parent(a, t) and parent(t, b)) }grandparent is a binary relation.
def netsales[x, y, z] = sales[x, y, z] - returns[x, y, z]Assuming sales and returns have arity 4, netsales has arity 4. See Partial Relational Application.

Note that in Rel any constant or variable can be used as a relation. For example, in def pi = 3.14 the value of pi is the singleton relation {(3.14,)}.

Definitions are similar to views in SQL, though Rel has fewer restrictions on what computations are supported in a view.

It is worth noting that the following two definitions are equivalent:

def square_add(x, y, z) { z = x * x + y }
def square_add[x, y] = x * x + y

For more information on square brackets syntax, see Partial Relational Application.

Writing Definitions

In the examples given so far, the head of each definition was either without formal parameter specifications or had formal parameter specifications that are just the names of parameters. In general, a formal parameter specification can be any binding, with two exceptions:

  1. A binding with where cannot appear in the head of a definition.
  2. A string in the head of a definition cannot feature string interpolation.

In each of the following three examples, all the definitions are equivalent. In some cases the body is a relational abstraction.

def pair = 1, "a"
def pair(1, "a") = true
def pair(1, x) {x = "a"}
def pair[1] = "a" : true
def pair[1]("a") = true
def pq(x in p, y in q) = x < y
def pq(x, y) = p(x) and q(y) and x < y
def pq = x in p, y in q : x < y
def pq = x, y : p(x) and q(y) and x < y
def qr(x in q) = r(x, _)
def qr = x in q where r(x, _) : true
def qr = x : q(x) and r(x, _)

The formal parameter specifications in the head do not provide any additional expressive power. It is always possible to write the definition of a named relation in such a way that the head consists only of the relation’s name. However, using formal parameter specifications can often make the definition easier to read.

For instance, the relation square_add shown in Examples of Definitions could be defined as follows:

def square_add = x, y : x * x + y

The intention is to use this relation for computing the value of the formula, for example, by writing square_add[7, 3.0] to obtain the value 52.0. Given this intention, the preferred form of the definition is:

def square_add[x in Number, y in Number] = x * x + y

If you will use the relation only for numbers of a particular kind, for example integers, then you will make it more efficient by using a more specific type:

def square_add[x in Int, y in Int] = x * x + y

The final example enumerates almost all of the possible ways of writing a definition equivalent to the following:

def output = range[1, 10, 1]

You can also write this as:

def output { range[1, 10, 1] }
def output(x) { x = range[1, 10, 1] }

You can also use relational application instead of partial relational application:

def output(x) = range(1, 10, 1, x)
def output(x) { range(1, 10, 1, x) }

You can write equivalent definitions with relational abstraction:

def output = x: range(1, 10, 1, x)
def output { x: range(1, 10, 1, x) }

If the number of arguments is equal to the arity of the applied relation, then a relational application is equivalent to partial relational application. So the following definitions are also equivalent, though their use is not recommended:

def output(x) = range[1, 10, 1, x]
def output(x) { range[1, 10, 1, x] }
def output = x: range[1, 10, 1, x]
def output { x: range[1, 10, 1, x] }

When the number of parameters in a definition of a relation is equal to the arity of that relation, then it does not matter whether you use round parentheses or square brackets in the head of the definition. The following definitions are all equivalent to the above, though it is recommended that you use square brackets in the head only if the number of parameter specifications is lower than the arity of the relation:

def output[x] { x = range[1, 10, 1] }
def output[x] = range(1, 10, 1, x)
def output[x] { range(1, 10, 1, x) }
def output[x] = range[1, 10, 1, x]
def output[x] { range[1, 10, 1, x] }

The following two definitions are also equivalent to the above, but you are strongly encouraged to avoid these forms, because of the juxtapositions of two = characters with two completely different meanings:

def output(x) = x = range[1, 10, 1]
def output[x] = x = range[1, 10, 1]

Multiple Definitions

If there is more than one definition of a relation with a given name, then the resulting relation is a union of the relations defined in each of the definitions. This is quite natural, because — as mentioned above — each definition can be read as “the body implies the head.”

The definitions for a relation do not need to be contiguous, and can be separated by definitions of other relations:

// read query
 
def five = 5
def seven = 7
def five = 6
def output = five

However, it is recommended that you keep multiple definitions for the same name together whenever possible.

A definition can give another name to a named relation. This is illustrated by the following example:

// model
 
def P = 1
def Q = P

According to the definitions above, P must contain (1,) and Q must contain the contents of P:

// read query
 
def output:P = P
def output:Q = Q

You can assign additional values to P and Q:

// read query
 
def Q = 2
def P = 3
def output:P = P
def output:Q = Q

Now, Q also contains (2,), and P also contains (3,). So Q will now be the union of two relations: P and {(2,)}. Since the name P will now refer to {(1,), (3,)}, Q will also contain 3:

You can think of the definition def Q = P as introducing a one-sided dependency: Q depends on P, but P does not depend on Q.

It is important to realize that relations defined within the Libraries are in the same name space as your own definitions. So if you define a relation that has the same name as a Library relation, the results may be surprising:

// read query
 
def abs[x] = -x
def output = abs[3]

It is also possible that user-defined relations may be modified when a new relation is added to the Library. Scoping user-defined relations within modules helps avoid this problem.

Next: Bound Declarations

Was this doc helpful?