# A relational logic primer

In Alloy, constraints are specified in relational logic, an extension of first-order logic with a few operators to compose relations. In this chapter we will present this logic in detail, namely detail the semantics of each of the operators, illustrated with several usage examples. These examples will be based on the file system specification introduced in chapter Structural design with Alloy, whose signatures and fields are detailed below.

```abstract sig Object {}

sig File extends Object {}

sig Dir extends Object {
entries : set Entry
}

one sig Root extends Dir {}

sig Entry {
name : one Name,
object : one Object
}

sig Name {}
```

We will also use the following instance of this specification to illustrate the result of relational operators. Occasionally we will also refer to the ternary relation `contents` used in the alternative version presented in Using higher-arity relations, whose content for the same instance of a file system is depicted below. ## Everything is a relation

Structures are described in Alloy using only (mathematical) relations. A relation is a set of tuples of objects drawn from the universe of discourse. Every tuple in a relation must have the same size, which is known as the arity of the relation.

For example, field `name` is a relation of arity 2 (a binary relation) relating entries with their names. For the above instance, it has four pairs, namely:

```name = {(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}
```

In logic a relation is also known as a predicate, and the fact that predicate `name` holds for tuple `(x,y)` is usually denoted as `name(x,y)`. As explained later, in Alloy this fact can be denoted by `x->y in name`.

An alternative way to depict a relation (or predicate) is using a table, where each row corresponds to one of the tuples of the relation. The table view of relation `name` is depicted below.

 `Entry0` `Name0` `Entry1` `Name2` `Entry2` `Name1` `Entry3` `Name1`

This is also the standard way to present the value of relations in the Alloy Analyzer’s evaluator. Relation `contents` is a relation of arity 3 (a ternary relation), relating directories, names, and objects. It contains four triples, namely:

```contents = {(Root,Name1,Dir0),(Root,Name0,File),(Root,Name2,File),(Dir0,Name1,Dir1)}
```

A set can also be represented by a relation of arity 1. In Alloy, signatures are encoded in this way. For example, in the above instance, signature `Dir` has the value:

```Dir = {(Root),(Dir0),(Dir1)}
```

Moreover, in Alloy even the constants and (quantified) variables are represented by relations, namely singleton relations of arity 1. A singleton is a relation with a single tuple. For example, signature `Root`, declared with multiplicity `one`, has the following value.

```Root = {(Root)}
```

Warning

Singleton signature names vs atom names.

Do not confuse the two occurrences of the word `Root` in the above definition. On the left-hand side, we have the signature `Root` that was declared in our specification to denote the root of the file system. On the right-hand side, we have the atom `Root` of the universe, whose name was automatically generated by the Analyzer to populate signature `Root`. The name of this atom is actually irrelevant, but the Analyzer names atoms using the signature name as prefix and a sequential number as suffix. Actually, according to this naming convention, the name of this atom is `Root0`, and that is the name that will be depicted in the evaluator if you ask for the value of signature `Root`. However, in the visualiser, if there is only a single atom with a given name prefix the numeric suffix is omitted by default. In this chapter we will use the names chosen by the visualiser.

Since atom names are arbitrary, when specifying constraints in Alloy it is impossible to refer to them directly. If we need to distinguish a particular atom of the universe, we need to declare a singleton signature that will contain that atom and refer to that signature name instead. That was precisely what we did to distinguish the root of a file system.

An instance of an Alloy specification without mutable declarations is a single snapshot with a complete valuation for all declared signatures and fields, mapping each of them to a relation of the appropriate arity. The value of all signatures and fields in our example instance is the following.

```Object   = {(Root),(Dir0),(Dir1),(File)}
Dir      = {(Root),(Dir0),(Dir1)}
Root     = {(Root)}
File     = {(File)}
Entry    = {(Entry0),(Entry1),(Entry2),(Entry3)}
Name     = {(Name0),(Name1),(Name2)}

entries  = {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}
object   = {(Entry0,File),(Entry1,File),(Entry2,Dir0),(Entry3,Dir1)}
name     = {(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}
contents = {(Root,Name1,Dir0),(Root,Name0,File),(Root,Name2,File),(Dir0,Name1,Dir1)}
```

An instance also includes the values of the three predefined constants: `none` (the empty set), `univ` (the universe of all atoms), and `iden` (the identity relation on the universe). In our example instance their value is the following.

```none = {}
univ = {(Root),(Dir0),(Dir1),(File),(Entry0),(Entry1),(Entry2),(Entry3),(Name0),(Name1),(Name2)}
iden = {(Root,Root),(Dir0,Dir0),(Dir1,Dir1),(File,File),(Entry0,Entry0),(Entry1,Entry1),(Entry2,Entry2),(Entry3,Entry3),(Name0,Name0),(Name1,Name1),(Name2,Name2)}
```

## First-order logic in a nutshell

Relational logic is an extension of first-order logic, which in turn is an extension of propositional logic. In propositional logic the simplest (atomic) formula is a proposition that checks if a Boolean variable is true. Compound formulas can be built by connecting atomic formulas using the standard logic connectives (or operators): negation, conjunction, disjunction, implication, and equivalence. These connectives are also available in Alloy’s relational logic, and their syntax is the following.

 Operator Name `!`, `not` Negation `&&`, `and` Conjunction `||`, `or` Disjunction `=>`, `implies` Implication `<=>`, `iff` Equivalence

As you can see, Alloy has a dual syntax for these operators, one with programming language style symbols and the other with English words. In this book we tend to use the latter, as the resulting formulas are more readable. The `implies` operator can also have an optional `else` to state what should be true when the condition on the left-hand side is false. Given arbitrary formulas `P`, `Q`, `T`, `P implies Q else T` is the same as `(P and Q) or (not P and T)`.

In first-order logic we have a domain of discourse (or universe), and propositions are generalised by predicates that relate elements of this domain. Formulas can also be built using variables quantified over this domain. There are two standard quantifiers: the universal quantifier `∀ x . P` checks if a formula `P` (possibly referring to variable `x`) is true for all `x` in the domain; and the existential quantifier `∃ x . P` checks if a formula `P` (possibly referring to variable `x`) is true for some `x` in the domain. In Alloy all quantifications are bounded by a set, and English words are used instead of the standard mathematical notation. The following table presents all quantifiers that are available in Alloy: `A` is denotes an arbitrary set (a unary relation) and `P` an arbitrary formula. The first two are the standard universal and existential quantifiers.

 Quantifier Informal meaning `all x : A | P` `P` is true for all `x` in set `A` `some x : A | P` `P` is true for some `x` in set `A` `no x : A | P` `P` is false for all `x` in set `A` `lone x : A | P` `P` is true for at most one `x` in set `A` `one x : A | P` `P` is true for exactly one `x` in set `A`

It is well known that the existential quantifier can be specified with the universal one, and vice-versa, and the same is true for all other Alloy quantifiers. For example, `some x : A | P` is the same as `not (all x : A | not P)` and `no x : A | P` is the same as `all x : A | not P`.

As mentioned above in Alloy everything is a relation. The same is true for quantified variables: the quantified `x` that can be referred in `P` is a unary relation containing a single tuple with an atom of the universe. It is also possible to quantify more than one variable at once, as in `all x,y : A | P` or ```all x : A, y : B | P```. In the latter, the expression `B` can also refer to the first quantified variable `x`. It is also possible to add keyword `disj` to quantify over all different values of the bound variables. For example, writing `all disj x,y : A | P` abbreviates `all x,y : A | x != y implies P`.

Besides predicates, first-order logic also allows functions as non-logical symbols. Given some parameters a function returns an element of the domain. Since in Alloy the atoms of the universe are mostly uninterpreted there are very few predefined functions. The exception is when using integers, for which we have the standard arithmetic operations. If we do not consider functions, atomic formulas in first-order logic just check for equality of (quantified) variables or if a tuple of (quantified) variables satisfies (or is a member of) a predicate. In Alloy’s relational logic we have a few more atomic formulas, that are described in the following table, where `R` and `S` are arbitrary relations of the same arity, including sets.

 Atomic formula Informal meaning `R in S` `R` is a subset or equal to `S` `R = S` `R` is equal to `S` `some R` `R` contains at least one tuple `lone R` `R` contains at most one tuple `one R` `R` contains exactly one tuple `no R` `R` is empty

The negation of the subset or equality atomic formulas can also be written by placing the negation operator next to the comparison operator. For example, instead of `not (R in S)` it is possible to write `R not in S` or `R !in S`.

Since quantified variables are also (singleton) relations, although `in` stands for the subset or equal operator (`⊆`) it can also be used to check set membership (`∈`). As we will see below, given variables `x₁`, …, `xₐ`, it is possible to define expression `x₁->…->xₐ` that denotes a relation with a single tuple with those variables. Formula `x₁->…->xₐ in R` can then be used to check that this tuple belongs to a relation `R` with arity `a`, something that in the standard mathematical notation of first-order logic is written as `R(x₁,…,xₐ)`. Recall that, besides equality checks between variables, such membership checks are the only atomic formulas in first-order logic. Although Alloy also allows all the above ones, they all can be written using just these basic checks, so technically they do not add expressive power to first-order logic, but just a more succinct way to write formulas. The following table provides such formal definitions, assuming `R` and `S` have arity `a`.

 Atomic formula Formal meaning `R in S` `all x₁,…,xₐ : univ | x₁->…->xₐ in R implies x₁->…->xₐ in S` `R = S` `R in S and S in R` `some R` `some x₁,…,xₐ : univ | x₁->…->xₐ in R` `lone R` `all x₁,…,xₐ,y₁,…,yₐ : univ | x₁->…->xₐ in R and y₁->…->yₐ in R implies x₁=y₁ and … and xₐ=yₐ` `one R` `some R and lone R` `no R` `not (some R)`

As we can see, the reduction in formula size can be substantial. For example, to formalize the requirement that “every file is an object”, in plain first-order logic we would have to write ```∀ x . File(x) → Object(x)``` or, in Alloy’s notation, ```all x : univ | x in File implies x in Object```. However, with Alloy’s relational logic we can just write `File in Object`.

Warning

Be careful with membership checks!

It is important to always recall that `in` denotes the subset operator and not the membership test. Of course, if we are certain that the expression on the left-hand side is a singleton (a set with a single tuple), `in` behaves like membership. For example, to test that `Root` is a `Dir` we can write `Root in Dir`. However, if the expression on the left-hand side does not necessarily denote a singleton, this check may not work as expected. For example, if `Root` was declared with multiplicity `lone` instead of `one`, the check `Root in Dir` will also be true if `Root` is empty. In this case, to be certain to test for membership you also need to check that the left-hand expression is non-empty, as follows.

```some Root and Root in Dir
```

## Relational operators

As all the alternative atomic checks, most of the relational operators in Alloy do not technically add expressive power to first-order logic, but just a more succinct alternative to write formulas. The full list of operators is presented below.

 Operator Name `+` Union `&` Intersection `-` Difference `.` Composition, Dot join `[]` Box join `->` (Cartesian) Product `<:` Domain restriction `:>` Range restriction `++` Override `~` Transpose, Converse `^` Transitive closure `*` Reflexive transitive closure

These operators act like combinators, that can be used to put together relations (predicates) to obtain expressions denoting more complex relations. The most basic operators are the standard set operators of union, intersection, and difference. For example, given predicates `File` and `Dir` we can compose them with union to obtain the derived predicate `File + Dir` that can be used to directly check if an element is either a file or a directory. This simplifies the writing of requirements such as “every object is either a file or a directory”. In plain first-order logic we would write (using Alloy’s syntax):

```all x : univ | x in Object implies x in File or x in Dir
```

By using the union operator we can simplify this to:

```all x : univ | x in Object implies x in File + Dir
```

And finally by using the subset operator we can write just:

```Object in File + Dir
```

Below we present the formal semantics of all relational operators in terms of plain first-order logic. The formula in the right column formally specifies when a tuple belongs to an expression that uses each operator. To abbreviate, in this formula all variables are implicitly universally quantified over the universe. Notice that some of these operators (namely the transpose and the closure operators) are only defined for binary relations.

 Operator Formal meaning `+` `x₁->…->xₐ in R+S               iff  x₁->…->xₐ in R or x₁->…->xₐ in S` `&` `x₁->…->xₐ in R&S               iff  x₁->…->xₐ in R and x₁->…->xₐ in S` `-` `x₁->…->xₐ in R-S               iff  x₁->…->xₐ in R and x₁->…->xₐ !in S` `.` `x₁->…->xₐ₋₁->y₂->…->yₑ in R.S  iff  x₁->…->xₐ in R and y₁->…->yₑ in S and xₐ = y₁` `[]` `x₁->…->xₐ in R[S]              iff  x₁->…->xₐ in S.R` `->` `x₁->…->xₐ->y₁->…->yₑ in R->S   iff  x₁->…->xₐ in R and y₁->…->yₑ in S` `<:` `x₁->…->xₐ in A<:R              iff  x₁ in A and x₁->…->xₐ in R` `:>` `x₁->…->xₐ in R:>A              iff  x₁->…->xₐ in R and xₐ in A` `++` `x₁->…->xₐ in R++S              iff  x₁->…->xₐ in S or (x₁->…->xₐ in R and x₁->y₂->…->yₐ !in S)` `~` `x₁->x₂ in ~R                   iff  x₂->x₁ in R` `^` `x₁->x₂ in ^R                   iff  x₁->x₂ in R + R.R + R.R.R + …` `*` `x₁->x₂ in *R                   iff  x₁->x₂ in ^R + iden`

In the remainder of this section we will illustrate each operator with examples based on the file system specification presented above.

### Composition

• The entries inside the root

```Root.entries
= {(Root)}.{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}
= {(Entry0),(Entry1),(Entry2)}
```
• The names of the entries inside the root

```Root.entries.name
= {(Entry0),(Entry1),(Entry2)}.name
= {(Entry0),(Entry1),(Entry2)}.{(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}
= {(Name0),(Name2),(Name1)}
```
• The binary relation between directories and the contained objects

```entries.object
= {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}.{(Entry0,File),(Entry1,File),(Entry2,Dir0),(Entry3,Dir1)}
= {(Root,File),(Root,Dir0),(Dir0,Dir1)}
```
• Non-empty directories

```entries.Entry
= {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}.{(Entry0),(Entry1),(Entry2),(Entry3)}
= {(Root),(Dir0)}
```
```(contents.Object).Name
= ({(Root,Name1,Dir0),(Root,Name0,File),(Root,Name2,File),(Dir0,Name1,Dir1)}.{(Root),(Dir0),(Dir1),(File)}).Name
= {(Root,Name1),(Root,Name0),(Root,Name2),(Dir0,Name1)}.Name
= {(Root,Name1),(Root,Name0),(Root,Name2),(Dir0,Name1)}.{(Name0),(Name1),(Name2)}
= {(Root),(Dir0)}
```

### Set operators

• All directories except the root

```Dir - Root
= {(Root),(Dir0),(Dir1)} - {(Root)}
= {(Dir0),(Dir1)}
```
• The directories inside the root

```Root.entries.object & Dir
= Root.{(Root,File),(Root,Dir0),(Dir0,Dir1)} & Dir
= {(File),(Dir0)} & {(Root),(Dir0),(Dir1)}
= {(Dir0)}
```

### Cartesian product

• All possible associations between files and names

```File->Name
= {(File)} -> {(Name0),(Name1),(Name3)}
= {(File,Name0),(File,Name1),(File,Name3)}
```

### Domain and range restriction

• The identity relation on objects

```Object <: iden
= {(Root),(Dir0),(Dir1),(File)} <: {(Root,Root),(Dir0,Dir0),(Dir1,Dir1),(File,File),(Entry0,Entry0),(Entry1,Entry1),(Entry2,Entry2),(Entry3,Entry3),(Name0,Name0),(Name1,Name1),(Name2,Name2)}
= {(Root,Root),(Dir0,Dir0),(Dir1,Dir1),(File,File)}
```

### Override

• A modified entries relation where all files are removed from the root directory

```entries ++ (Root -> (Root.entries & object.Dir))
= entries ++ (Root -> ({(Root)}.{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)} & object.Dir))
= entries ++ (Root -> ({(Entry0),(Entry1),(Entry2)} & object.Dir))
= entries ++ (Root -> ({(Entry0),(Entry1),(Entry2)} & {(Entry0,File),(Entry1,File),(Entry2,Dir0),(Entry3,Dir1)}.{(Root),(Dir0),(Dir1)}))
= entries ++ (Root -> ({(Entry0),(Entry1),(Entry2)} & {(Entry2),(Entry3)}))
= entries ++ (Root -> {(Entry2)})
= entries ++ ({(Root)} -> {(Entry2)})
= entries ++ ({(Root,Entry2)})
= {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)} ++ ({(Root,Entry2)})
= {(Root,Entry2),(Dir0,Entry3)}
```

### Transpose

• The binary relation between objects (contained in directories) and their name

```~object.name
= ~{(Entry0,File),(Entry1,File),(Entry2,Dir0),(Entry3,Dir1)}.{(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}
= {(File,Entry0),(File,Entry1),(Dir0,Entry2),(Dir1,Entry3)}.{(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}
= {(File,Name0),(File,Name2),(Dir0,Name1),(Dir1,Name1)}

~(Object.contents)
= ~({(Root),(Dir0),(Dir1),(File)}.{(Root,Name1,Dir0),(Root,Name0,File),(Root,Name2,File),(Dir0,Name1,Dir1)})
= ~{(Name1,Dir0),(Name0,File),(Name2,File),(Name1,Dir1)}
= {(File,Name0),(File,Name2),(Dir0,Name1),(Dir1,Name1)}
```
• The binary relation between entries in the same directory

```~entries.entries
= ~{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}.{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}
= {(Entry0,Root),(Entry1,Root),(Entry2,Root),(Entry3,Dir0)}.{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}
= {(Entry0,Entry0),(Entry0,Entry1),(Entry0,Entry2),(Entry1,Entry0),(Entry1,Entry1),(Entry1,Entry2),(Entry2,Entry0),(Entry2,Entry1),(Entry2,Entry2),(Entry3,Entry3)}
```
• The binary relation between entries sharing names

```name.~name
= {(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}.~{(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}
= {(Entry0,Name0),(Entry1,Name2),(Entry2,Name1),(Entry3,Name1)}.{(Name0,Entry0),(Name2,Entry1),(Name1,Entry2),(Name1,Entry3)}
= {(Entry0,Entry0),(Entry1,Entry1),(Entry2,Entry2),(Entry2,Entry3),(Entry3,Entry2),(Entry3,Entry3)}
```

### Closures

• The binary relation between a directory and the objects contained in that directory or any sub-directory

```^(entries.object)
= ^{(Root,File),(Root,Dir0),(Dir0,Dir1)}
= {(Root,File),(Root,Dir0),(Root,Dir1),(Dir0,Dir1)}
```
• All objects in the file system

```Root.*(entries.object)
= Root.(^(entries.object) + iden)
= Root.({(Root,File),(Root,Dir0),(Root,Dir1),(Dir0,Dir1)} + iden)
= {(Root)}.{(Root,File),(Root,Dir0),(Root,Dir1),(Dir0,Dir1),(Root,Root),(Dir0,Dir0),(Dir1,Dir1),(File,File),(Entry0,Entry0),(Entry1,Entry1),(Entry2,Entry2),(Entry3,Entry3),(Name0,Name0),(Name1,Name1),(Name2,Name2)}
= {(Root),(Dir0),(Dir1),(File)}
```

### Set comprehension

• The binary relation between directories and the contained objects

```{ d : Dir, o : Object | some d.contents.o }
= {(Root,File),(Root,Dir0),(Dir0,Dir1)}
```

Note

A question of style!

An object is not contained in more one entry, or relation `content` is injective.

The pure first-order (or point-wise) style.

```all x,y : Entry, o : Object | x->o in object and y->o in object implies x=y
```

The most common Alloy navigational style.

```all o : Object | lone object.o
```

The pure relational (or point-free) style.

```object.~object in iden
```