.. _relational-logic:

A relational logic primer
*************************

.. index::
   ! relational logic

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 :ref:`structural-design`, whose signatures and
fields are detailed below.

.. code-block::

   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.

.. image:: instance1.png
   :width: 500 px
   :align: center

Occasionally we will also refer to the ternary relation
:code:`contents` used in the alternative version presented in
:ref:`higher-arity`, whose content for the same instance of a file
system is depicted below.

.. image:: instance2.png
   :width: 500 px
   :align: center

           

Everything is a relation
========================

.. index::
   ! relation
   ! relation; arity

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.

.. index::
   ! relation; binary

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

.. code-block::

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

.. index::
   ! single: predicate, logic

In logic a relation is also known as a *predicate*, and the fact that
predicate :code:`name` holds for tuple :code:`(x,y)` is usually denoted
as :code:`name(x,y)`. As explained later, in Alloy this fact can be
denoted by :code:`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 :code:`name` is depicted below.

.. table:: 
   :align: center

   +----------------+---------------+
   | :code:`Entry0` | :code:`Name0` |
   +----------------+---------------+
   | :code:`Entry1` | :code:`Name2` |
   +----------------+---------------+
   | :code:`Entry2` | :code:`Name1` |
   +----------------+---------------+
   | :code:`Entry3` | :code:`Name1` |
   +----------------+---------------+

This is also the standard way to present the value of relations in the
Alloy Analyzer's evaluator.

.. image:: evaluator1.png
   :width: 600 px
   :align: center

.. index::
   ! relation; ternary
           
Relation :code:`contents` is a relation of arity 3 (a *ternary*
relation), relating directories, names, and objects. It contains four
triples, namely:

.. code-block::

   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 :code:`Dir` has the value:

.. code-block::

   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
:code:`Root`, declared with multiplicity :code:`one`, has the following value.

.. code-block::

   Root = {(Root)}

.. warning:: Singleton signature names vs atom names.
   
   Do not confuse the two occurrences of the word :code:`Root` in the
   above definition. On the left-hand side, we have the signature
   :code:`Root` that was declared in our specification to denote the root of
   the file system. On the right-hand side, we have the atom
   :code:`Root` of the universe, whose name was automatically
   generated by the Analyzer to populate signature :code:`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 :code:`Root0`, and that is the name that will be
   depicted in the evaluator if you ask for the value of signature
   :code:`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.

.. index::
   instance
   instance; snapshot
   
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.

.. code-block::

   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: :code:`none` (the empty set), :code:`univ` (the universe of all atoms), and :code:`iden` (the identity relation on the universe). In our example instance their value is the following.

.. code-block::

   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
===============================

.. index::
   ! first-order logic
   ! propositional logic
   ! proposition

*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.

.. index::
   ! logical operator; negation
   ! logical operator; conjunction
   ! logical operator; disjunction
   ! logical operator; implication
   ! logical operator; equivalence

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

.. index::
   ! logical operator; else

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 :code:`implies` operator can also
have an optional :code:`else` to state what should be true when the
condition on the left-hand side is false. Given arbitrary formulas
:code:`P`, :code:`Q`, :code:`T`, :code:`P implies Q else T` is the
same as :code:`(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 :code:`∀ x . P` checks if a formula :code:`P` (possibly
referring to variable :code:`x`) is true for all :code:`x` in the
domain; and the existential quantifier :code:`∃ x . P` checks if a
formula :code:`P` (possibly referring to variable :code:`x`) is true
for some :code:`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: :code:`A`
is denotes an arbitrary set (a unary relation) and :code:`P` an arbitrary
formula. The first two are the standard universal and existential
quantifiers. 

.. index::
   ! quantifier
   ! quantifier; universal
   ! quantifier; existential

+--------------------------+--------------------------------------------------------------+
| *Quantifier*             | *Informal meaning*                                           |
+--------------------------+--------------------------------------------------------------+
| :code:`all x : A | P`    | :code:`P` is true for all :code:`x` in set :code:`A`         |
+--------------------------+--------------------------------------------------------------+
| :code:`some x : A | P`   | :code:`P` is true for some :code:`x` in set :code:`A`        |
+--------------------------+--------------------------------------------------------------+
| :code:`no x : A | P`     | :code:`P` is false for all :code:`x` in set :code:`A`        |
+--------------------------+--------------------------------------------------------------+
| :code:`lone x : A | P`   | :code:`P` is true for at most one :code:`x` in set :code:`A` |
+--------------------------+--------------------------------------------------------------+
| :code:`one x : A | P`    | :code:`P` is true for exactly one :code:`x` in set :code:`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, :code:`some x : A | P` is the same as
:code:`not (all x : A | not P)` and :code:`no x : A | P` is the same
as :code:`all x : A | not P`. 

.. index::
   ! quantifier; disj

As mentioned above in Alloy everything is a relation. The same is true
for quantified variables: the quantified :code:`x` that can be
referred in :code:`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 :code:`all x,y : A | P` or :code:`all
x : A, y : B | P`. In the latter, the expression :code:`B` can also refer to
the first quantified variable :code:`x`. It is 
also possible to add keyword :code:`disj` to quantify over all different values of the bound variables.
For example, writing :code:`all disj x,y : A | P`
abbreviates :code:`all x,y : A | x != y implies P`.

.. index::
   ! single: function, logic

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 :code:`R`
and :code:`S` are arbitrary relations of the same arity, including
sets.

+------------------+---------------------------------------------+
| *Atomic formula* | *Informal meaning*                          |
+------------------+---------------------------------------------+
| :code:`R in S`   | :code:`R` is a subset or equal to :code:`S` |
+------------------+---------------------------------------------+
| :code:`R = S`    | :code:`R` is equal to :code:`S`             |
+------------------+---------------------------------------------+
| :code:`some R`   | :code:`R` contains at least one tuple       |
+------------------+---------------------------------------------+
| :code:`lone R`   | :code:`R` contains at most one tuple        |
+------------------+---------------------------------------------+
| :code:`one R`    | :code:`R` contains exactly one tuple        |
+------------------+---------------------------------------------+
| :code:`no R`     | :code:`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 :code:`not (R in S)` it is possible
to write :code:`R not in S` or :code:`R !in S`.

Since quantified variables are also (singleton) relations, although :code:`in`
stands for the `subset or equal` operator (:math:`⊆`) it can also be used to
check set membership (:code:`∈`). As we will see below, given
variables :code:`x₁`, ..., :code:`xₐ`, it is possible to define
expression :code:`x₁->…->xₐ` that denotes a relation with a single
tuple with those variables. Formula :code:`x₁->…->xₐ in R` can then
be used to check that this tuple belongs to a relation :code:`R` with
arity :code:`a`, something that in the standard mathematical notation
of first-order logic is written as :code:`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 :code:`R`
and :code:`S` have arity :code:`a`.


+------------------+------------------------------------------------------------------------------------------------------+
| *Atomic formula* | *Formal meaning*                                                                                     |
+------------------+------------------------------------------------------------------------------------------------------+
| :code:`R in S`   | :code:`all x₁,…,xₐ : univ | x₁->…->xₐ in R implies x₁->…->xₐ in S`                                   |
+------------------+------------------------------------------------------------------------------------------------------+
| :code:`R = S`    | :code:`R in S and S in R`                                                                            |
+------------------+------------------------------------------------------------------------------------------------------+
| :code:`some R`   | :code:`some x₁,…,xₐ : univ | x₁->…->xₐ in R`                                                         |
+------------------+------------------------------------------------------------------------------------------------------+
| :code:`lone R`   | :code:`all x₁,…,xₐ,y₁,…,yₐ : univ | x₁->…->xₐ in R and y₁->…->yₐ in R implies x₁=y₁ and … and xₐ=yₐ` |
+------------------+------------------------------------------------------------------------------------------------------+
| :code:`one R`    | :code:`some R and lone R`                                                                            |
+------------------+------------------------------------------------------------------------------------------------------+
| :code:`no R`     | :code:`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 :code:`∀ x . File(x)
→ Object(x)` or, in Alloy's notation, :code:`all x : univ | x in File
implies x in Object`. However, with Alloy's relational logic we can
just write :code:`File in Object`.

.. warning:: Be careful with membership checks!

   It is important to always recall that :code:`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), :code:`in` behaves like membership. For
   example, to test that :code:`Root` is a :code:`Dir` we can write
   :code:`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 :code:`Root` was declared with
   multiplicity :code:`lone` instead of :code:`one`, the check
   :code:`Root in Dir` will also be true if :code:`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.

   .. code-block::

      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.

.. index::
   ! relational operator; union
   ! relational operator; intersection
   ! relational operator; difference
   ! relational operator; composition
   see: dot join; composition
   ! relational operator; box join
   ! relational operator; Cartesian product
   ! relational operator; domain restriction
   ! relational operator; range restriction
   ! relational operator; override
   ! relational operator; transpose
   see: converse; transpose
   ! relational operator; transitive closure
   ! relational operator; reflexive transitive closure

+------------+------------------------------+
| *Operator* | *Name*                       |
+------------+------------------------------+
| :code:`+`  | Union                        |
+------------+------------------------------+
| :code:`&`  | Intersection                 |
+------------+------------------------------+
| :code:`-`  | Difference                   |
+------------+------------------------------+
| :code:`.`  | Composition, Dot join        |
+------------+------------------------------+
| :code:`[]` | Box join                     |
+------------+------------------------------+
| :code:`->` | (Cartesian) Product          |
+------------+------------------------------+
| :code:`<:` | Domain restriction           |
+------------+------------------------------+
| :code:`:>` | Range restriction            |
+------------+------------------------------+
| :code:`++` | Override                     |
+------------+------------------------------+
| :code:`~`  | Transpose, Converse          |
+------------+------------------------------+
| :code:`^`  | Transitive closure           |
+------------+------------------------------+
| :code:`*`  | 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
:code:`File` and :code:`Dir` we can compose them with union to obtain
the derived predicate :code:`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):

.. code-block::

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

By using the union operator we can simplify this to:

.. code-block::

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

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

.. code-block::

   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*                                                                                       |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`+`   | :code:`x₁->…->xₐ in R+S               iff  x₁->…->xₐ in R or x₁->…->xₐ in S`                           |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`&`   | :code:`x₁->…->xₐ in R&S               iff  x₁->…->xₐ in R and x₁->…->xₐ in S`                          |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`-`   | :code:`x₁->…->xₐ in R-S               iff  x₁->…->xₐ in R and x₁->…->xₐ !in S`                         |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`.`   | :code:`x₁->…->xₐ₋₁->y₂->…->yₑ in R.S  iff  x₁->…->xₐ in R and y₁->…->yₑ in S and xₐ = y₁`              |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`[]`  | :code:`x₁->…->xₐ in R[S]              iff  x₁->…->xₐ in S.R`                                           |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`->`  | :code:`x₁->…->xₐ->y₁->…->yₑ in R->S   iff  x₁->…->xₐ in R and y₁->…->yₑ in S`                          |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`<:`  | :code:`x₁->…->xₐ in A<:R              iff  x₁ in A and x₁->…->xₐ in R`                                 |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`:>`  | :code:`x₁->…->xₐ in R:>A              iff  x₁->…->xₐ in R and xₐ in A`                                 |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`++`  | :code:`x₁->…->xₐ in R++S              iff  x₁->…->xₐ in S or (x₁->…->xₐ in R and x₁->y₂->…->yₐ !in S)` |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`~`   | :code:`x₁->x₂ in ~R                   iff  x₂->x₁ in R`                                                |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`^`   | :code:`x₁->x₂ in ^R                   iff  x₁->x₂ in R + R.R + R.R.R + …`                              |
+-------------+--------------------------------------------------------------------------------------------------------+
| :code:`*`   | :code:`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

  .. code-block::

     Root.entries
     = {(Root)}.{(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}
     = {(Entry0),(Entry1),(Entry2)}

* The names of the entries inside the root

  .. code-block::

     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

  .. code-block::

     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

  .. code-block::

     entries.Entry
     = {(Root,Entry0),(Root,Entry1),(Root,Entry2),(Dir0,Entry3)}.{(Entry0),(Entry1),(Entry2),(Entry3)}
     = {(Root),(Dir0)}

  .. code-block::

     (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

  .. code-block::

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

* The directories inside the root

  .. code-block::

     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

  .. code-block::
     
     File->Name
     = {(File)} -> {(Name0),(Name1),(Name3)}
     = {(File,Name0),(File,Name1),(File,Name3)}

     

Domain and range restriction
----------------------------

* The identity relation on objects

  .. code-block::

     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

  .. code-block::

     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

  .. code-block::

     ~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

  .. code-block::

     ~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

  .. code-block::

     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

  .. code-block::

     ^(entries.object)
     = ^{(Root,File),(Root,Dir0),(Dir0,Dir1)}
     = {(Root,File),(Root,Dir0),(Root,Dir1),(Dir0,Dir1)}

* All objects in the file system

  .. code-block::

     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

  .. code-block::

     { 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 :code:`content` is injective.
          
   The pure first-order (or point-wise) style.
         
   .. code-block::

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

   The most common Alloy navigational style.
      
   .. code-block::
     
      all o : Object | lone object.o

   The pure relational (or point-free) style.
      
   .. code-block::

      object.~object in iden


     

A type-system for relational specifications
===========================================

.. caution:: This section is still under construction