.. _relational-logic: :tocdepth: 2 .. index:: relational logic 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. Recall the file system model from the :ref:`structural-modeling` chapter, and consider the following instance of this specification, that will be used to illustrate the result of relational operators throughout the chapter. .. image:: instance1.png :width: 500 px :align: center :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/relational-logic/instance_01/filesystem.als#L75-L86 :alt: Get the code to generate this instance. 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 :alloy:`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:: predicate In classical 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 :alloy:`x->y in name`. 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 :alloy:`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 :alloy:`Root`, declared with multiplicity :alloy:`one`, has the following value. .. code-block:: Root = {(Root)} Do not confuse the two occurrences of the word :alloy:`Root` in the above definition. On the left-hand side, we have the signature :alloy:`Root` that was declared in our specification to denote the root of the file system. On the right-hand side, we have the atom :alloy:`Root`, whose name was automatically generated by the Analyzer to populate signature :alloy:`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 :alloy:`Root0`, and that is the name that will be depicted in the evaluator if you ask for the value of signature :alloy:`Root`. However, in the visualizer, if there is only a single atom with a given name prefix, the numeric suffix is omitted by default. Here we will use the names chosen by the visualizer. 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 An *instance* of an Alloy specification without mutable declarations is 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)} An instance also includes the values of the three predefined relations: :alloy:`none` (the empty set), :alloy:`univ` (the universe of all atoms), and :alloy:`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)} .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/relational-logic/everything-is-a-relation :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. .. card:: The instance evaluator :link-type: ref :link: evaluator_instance :octicon:`beaker` Further reading ^^^ Learn how to use the evaluator to ask for the values of relational expressions. First-order logic in a nutshell ------------------------------- .. index:: first-order logic propositional logic *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:: operators; Boolean single: ! (not) not keyword && (and) and keyword || (or) or keyword => (implies) implies keyword <=> (iff) iff keyword +-------------------------------+------------------------------+ |**Operator** |**Name** | +-------------------------------+------------------------------+ | :alloy:`!`, :alloy:`not` | Negation | +-------------------------------+------------------------------+ | :alloy:`&&`, :alloy:`and` | Conjunction | +-------------------------------+------------------------------+ | :alloy:`||`, :alloy:`or` | Disjunction | +-------------------------------+------------------------------+ | :alloy:`=>`, :alloy:`implies` | Implication | +-------------------------------+------------------------------+ | :alloy:`<=>`, :alloy:`iff` | Equivalence | +-------------------------------+------------------------------+ .. index:: else keyword 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 :alloy:`implies` operator can also have an optional :alloy:`else` to state what should be true when the condition on the left-hand side is false. Given arbitrary formulas :alloy:`P`, :alloy:`Q`, :alloy:`T`, :alloy:`P implies Q else T` is the same as :alloy:`(P and Q) or (not P and T)`. In first-order logic we have a domain of discourse (or universe), and propositions are generalized 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 :math:`\forall x \cdot` `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 :math:`∃ x \cdot` `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: :alloy:`A` is denotes an arbitrary set (a unary relation) and :alloy:`P` an arbitrary formula. The first two are the standard universal and existential quantifiers. .. index:: all keyword some keyword; as quantifier one keyword; as quantifier lone keyword; as quantifier no keyword; as quantifier +--------------------------+-----------------------------------------------------------------+ |**Quantifier** |**Informal meaning** | +--------------------------+-----------------------------------------------------------------+ | :alloy:`all x : A | P` | :alloy:`P` is true for all :alloy:`x` in set :alloy:`A` | +--------------------------+-----------------------------------------------------------------+ | :alloy:`some x : A | P` | :alloy:`P` is true for some :alloy:`x` in set :alloy:`A` | +--------------------------+-----------------------------------------------------------------+ | :alloy:`no x : A | P` | :alloy:`P` is false for all :alloy:`x` in set :alloy:`A` | +--------------------------+-----------------------------------------------------------------+ | :alloy:`lone x : A | P` | :alloy:`P` is true for at most one :alloy:`x` in set :alloy:`A` | +--------------------------+-----------------------------------------------------------------+ | :alloy:`one x : A | P` | :alloy:`P` is true for exactly one :alloy:`x` in set :alloy:`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, :alloy:`some x : A | P` is the same as :alloy:`not (all x : A | not P)` and :alloy:`no x : A | P` is the same as :alloy:`all x : A | not P`. .. index:: disj keyword Alloy's rule that everything is a relation also applies to quantified variables: the quantified :alloy:`x` that can be referred in :alloy:`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 :alloy:`all x, y : A | P` or :alloy:`all x : A, y : B | P`. In the latter, the expression :alloy:`B` can also refer to the first quantified variable :alloy:`x`. It is also possible to add keyword :alloy:`disj` to quantify over all different values of the bound variables. For example, writing :alloy:`all disj x, y : A | P` abbreviates :alloy:`all x, y : A | x != y implies P`. Note that the `disj` keyword only applies to groups of variables quantified over the same set. This means that in formula `all disj x, y : A , w, z : B | P`, `w` and `z` may take the same value (but not `x` and `y`). Also, be aware that although these multi-variable quantifications are equivalent to their expansion for `all` and `some`, that is not the case for `one`, `lone` and `no`. For example, consider formulas `one x, y : A | x->y in r` and `one x : A | one y : A | x in r`, and let `r = {(A0,A0),(A0,A1),(A1,A0)}`. The former formula is false because there are three tuples in `r`. However, the latter is true because there is exactly one `x` (`A1`) for which there is exactly one `y` (`A0`) in `r`. .. index:: function 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 :alloy:`R` and :alloy:`S` are arbitrary relations of the same arity, including sets. .. index:: operators; relational in keyword; as subset or equal operator = (equality) equality operator some keyword; as multiplicity lone keyword; as multiplicity one keyword; as multiplicity no keyword; as multiplicity +---------------------+-----------------------------------------------+ | **Atomic formula** | **Informal meaning** | +---------------------+-----------------------------------------------+ | :alloy:`R in S` | :alloy:`R` is a subset or equal to :alloy:`S` | +---------------------+-----------------------------------------------+ | :alloy:`R = S` | :alloy:`R` is equal to :alloy:`S` | +---------------------+-----------------------------------------------+ | :alloy:`some R` | :alloy:`R` contains at least one tuple | +---------------------+-----------------------------------------------+ | :alloy:`lone R` | :alloy:`R` contains at most one tuple | +---------------------+-----------------------------------------------+ | :alloy:`one R` | :alloy:`R` contains exactly one tuple | +---------------------+-----------------------------------------------+ | :alloy:`no R` | :alloy:`R` is empty | +---------------------+-----------------------------------------------+ .. index:: not in keyword single: !in (not in) 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 :alloy:`not (R in S)` it is possible to write :alloy:`R not in S` or :alloy:`R !in S`. Since quantified variables are also (singleton) relations, although :alloy:`in` stands for the 'subset or equal' operator (:math:`\subseteq`) it can also be used to check set membership (:math:`\in`). As we will see below, given variables :math:`x_1, \ldots, x_a`, it is possible to define expression :alloy:`x₁->…->xₐ` that denotes a relation with a single tuple with those variables. Formula :alloy:`x₁->…->xₐ in R` can then be used to check that this tuple belongs to a relation :alloy:`R` with arity :math:`a`, something that in the standard mathematical notation of first-order logic is written as `R`:math:`(x_₁,\ldots,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 :alloy:`R` and :alloy:`S` have arity :math:`a`. +--------------------+------------------------------------------------------------------------------------------------------+ | **Atomic formula** | **Formal meaning** | +--------------------+------------------------------------------------------------------------------------------------------+ | :alloy:`R in S` | :alloy:`all x₁,…,xₐ : univ | x₁->…->xₐ in R implies x₁->…->xₐ in S` | +--------------------+------------------------------------------------------------------------------------------------------+ | :alloy:`R = S` | :alloy:`R in S and S in R` | +--------------------+------------------------------------------------------------------------------------------------------+ | :alloy:`some R` | :alloy:`some x₁,…,xₐ : univ | x₁->…->xₐ in R` | +--------------------+------------------------------------------------------------------------------------------------------+ | :alloy:`lone R` | :alloy:`all x₁,…,xₐ,y₁,…,yₐ : univ | x₁->…->xₐ in R and y₁->…->yₐ in R implies x₁=y₁ and … and xₐ=yₐ`| +--------------------+------------------------------------------------------------------------------------------------------+ | :alloy:`one R` | :alloy:`some R and lone R` | +--------------------+------------------------------------------------------------------------------------------------------+ | :alloy:`no R` | :alloy:`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 :math:`\forall x \cdot` `File`:math:`(x) \rightarrow` `Object`:math:`(x)` or, in Alloy's notation, :alloy:`all x : univ | x in File implies x in Object`. However, with Alloy's relational logic we can just write :alloy:`File in Object`. It is important to always recall that :alloy:`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), :alloy:`in` behaves like membership. For example, to test that :alloy:`Root` is a :alloy:`Dir` we can write :alloy:`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 :alloy:`Root` was declared with multiplicity :alloy:`lone` instead of :alloy:`one`, the check :alloy:`Root in Dir` will also be true if :alloy:`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 .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/relational-logic/first-order-logic-in-a-nutshell :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. .. card:: Working with integers :link-type: ref :link: integers :octicon:`beaker` Further reading ^^^ Read about integers in Alloy, namely learn which arithmetic operators are available. Relational operators -------------------- Likewise 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:: operators; relational + (union) union operator & (intersection) intersection operator - (difference) difference operator . (dot-join) dot-join operator composition operator; see dot-join operator [] (box-join) box-join operator -> (Cartesian product) Cartesian product operator <: (domain restriction) domain restriction operator :> (range restriction) range restriction operator ++ (override) override operator ~ (converse) converse operator transpose operator; see converse operator ^ (transitive closure) transitive closure operator * (reflexive transitive closure) reflexive transitive closure operator +-------------+------------------------------+ |**Operator** | **Name** | +-------------+------------------------------+ | :alloy:`+` | Union | +-------------+------------------------------+ | :alloy:`&` | Intersection | +-------------+------------------------------+ | :alloy:`-` | Difference | +-------------+------------------------------+ | :alloy:`.` | Composition, Dot join | +-------------+------------------------------+ | :alloy:`[]` | Box join | +-------------+------------------------------+ | :alloy:`->` | (Cartesian) Product | +-------------+------------------------------+ | :alloy:`<:` | Domain restriction | +-------------+------------------------------+ | :alloy:`:>` | Range restriction | +-------------+------------------------------+ | :alloy:`++` | Override | +-------------+------------------------------+ | :alloy:`~` | Transpose, Converse | +-------------+------------------------------+ | :alloy:`^` | Transitive closure | +-------------+------------------------------+ | :alloy:`*` | 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 :alloy:`File` and :alloy:`Dir` we can compose them with union to obtain the derived predicate :alloy:`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 (the redundant) "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 : Object | x in File or x in Dir By using the union operator we can simplify this to: .. code-block:: all x : Object | 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** | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`+` | :alloy:`x₁->…->xₐ in R + S iff x₁->…->xₐ in R or x₁->…->xₐ in S` | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`&` | :alloy:`x₁->…->xₐ in R & S iff x₁->…->xₐ in R and x₁->…->xₐ in S` | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`-` | :alloy:`x₁->…->xₐ in R - S iff x₁->…->xₐ in R and x₁->…->xₐ !in S` | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`.` | :alloy:`x₁->…->xₐ₋₁->y₂->…->yₑ in R.S iff x₁->…->xₐ in R and y₁->…->yₑ in S and xₐ = y₁` | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`[]` | :alloy:`x₁->…->xₐ in R[S] iff x₁->…->xₐ in S.R` | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`->` | :alloy:`x₁->…->xₐ->y₁->…->yₑ in R->S iff x₁->…->xₐ in R and y₁->…->yₑ in S` | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`<:` | :alloy:`x₁->…->xₐ in A <: R iff x₁ in A and x₁->…->xₐ in R` | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`:>` | :alloy:`x₁->…->xₐ in R :> A iff x₁->…->xₐ in R and xₐ in A` | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`++` | :alloy:`x₁->…->xₐ in R ++ S iff x₁->…->xₐ in S or (x₁->…->xₐ in R and x₁->y₂->…->yₐ !in S)` | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`~` | :alloy:`x₁->x₂ in ~R iff x₂->x₁ in R` | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`^` | :alloy:`x₁->x₂ in ^R iff x₁->x₂ in R + R.R + R.R.R + …` | +-------------+---------------------------------------------------------------------------------------------------------+ | :alloy:`*` | :alloy:`x₁->x₂ in *R iff x₁->x₂ in ^R + iden` | +-------------+---------------------------------------------------------------------------------------------------------+ Below we 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)} 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)} * 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.entries & object.o } = {(Root,File),(Root,Dir0),(Dir0,Dir1)} .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/relational-logic/the-pre-defined-relations :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. .. card:: Higher-arity relations :link-type: ref :link: nary-relations :octicon:`beaker` Further reading ^^^ Most of these operators can also be applied to higher-arity relations. Learn how to use these in Alloy models. The predefined relations -------------------------------- .. index:: relation; predefined none keyword iden keyword univ keyword There are three predefined relations in Alloy: * :alloy:`none`, that denotes the empty set. * :alloy:`univ`, the set of all atoms in all signatures. * :alloy:`iden`, the binary relation that associates each atom in :alloy:`univ` to itself. It is important to know that :alloy:`iden` relates every element of :alloy:`univ` to itself. This means that, for example, to check that a binary relation :alloy:`R` (defined on a signature :alloy:`A`) is reflexive it is not correct to write :alloy:`iden in R`, as :alloy:`iden` will not only contain elements in :alloy:`A` but also elements in other declared top-level signatures. To obtain the identity relation on signature :alloy:`A` we could, for example, intersect it with the binary relation containing all pairs of elements drawn from :alloy:`A`, computed with the Cartesian product operator :alloy:`->`, as follows: :alloy:`iden & (A -> A)`. We could also use the domain restriction operator for the same effect: :alloy:`A <: iden` filters relation :alloy:`iden` to obtain only the pairs whose first element belongs to :alloy:`A`. Dually, we could have restricted the range: :alloy:`iden :> A` filters relation :alloy:`iden` to obtain only the pairs whose last element belongs to :alloy:`A`. Thus, to check that the relation :alloy:`R` is reflexive we could write, for example, :alloy:`(A <: iden) in R`. Another thing to recall is that :alloy:`none` denotes the empty set and is a unary relation. So, if we write :alloy:`R = none`, to check if :alloy:`R` is empty, we will get a type error since the relations have different arities (:alloy:`none` is unary and :alloy:`R` is binary). The empty binary relation is denoted by the Cartesian product :alloy:`none -> none`: this expression denotes the empty set like :alloy:`none`, but for the type system it is a binary relation, so writing :alloy:`R = (none -> none)` does not raise a type error. Of course, a simpler way to check that :alloy:`R` is empty is to write :alloy:`no R`, since the cardinality check keywords like :alloy:`no` can be used with relational expressions of arbitrary arity. .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/relational-logic/the-pre-defined-relations :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book. .. _nomenclature: .. index:: predicate; Alloy vs logic nomenclature function; Alloy vs logic nomenclature model; see instance model; Alloy vs logic nomenclature Alloy vs. classical logic nomenclature -------------------------------------- Although Alloy is a formal language based on first-order logic, there are some nuances in the nomenclature that differ from that of traditional logic. When reasoning about semantics in logic, an *instance* (or interpretation) of a formula is usually known as a *model*: a model of a formula defines a domain (or universe) of discourse and a valuation of its non-logical symbols that makes the formula true. In contrast, in Alloy the term *model* is frequently used to denote the specification of a system, and the term *instance* is used to denote a satisfying universe and valuation. In particular, the Analyzer processes models (and the commands defined within) and generates instances (when the problem is satisfiable). This use of the term model in Alloy parlance is consistent with other techniques and languages for software design, namely the `Unified Modeling Language `_, where a software model is precisely the kind of artefact we have been denoting by a specification. Another concept that has a different meaning in the Alloy language than in classical logic is that of *predicate* and *function*. In first-order logic (also known as predicate logic), predicates and functions are non-logical symbols of arbitrary arity for which an interpretation must be provided when evaluating a formula. Their counter-part in Alloy are the free relations of a model that arise from the signature and field declarations. In contrast, *predicates* (:alloy:`pred`) and *functions* (:alloy:`fun`) in Alloy models are merely re-usable parametrisable formulas and expressions, respectively, and do not introduce any new free variables. .. card-carousel:: 2 .. card:: Full model for the section :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/relational-logic/alloy-vs-classical-logic-nomenclature :octicon:`file-badge` Alloy model ^^^ Download and explore the files relevant for the model at this point of the book.