.. _recursion: 

Handling recursion
==================

.. index::
  recursion

The transitive closure operator supported by the Alloy language allows the
specification of many reachability constraints that otherwise would have to be specified 
through recursive definitions. Let us get back to the file system model defined
in the  :ref:`structural-modeling` chapter. Assertion :alloy:`no_partitions`
required computing  all objects indirectly contained in the root,
traversing the complete file hierarchy. In a concrete implementation, this would
probably be computed with a recursive procedure. In Alloy, we easily collected
all objects using the transitive closure on :alloy:`entries.object`. While
extremely useful, transitive closure cannot be used to specify all constraints that can be specified with recursion.
For instance, let us try to compute the (maximum) depth of a file in the file
system. We could use the transitive closure of :alloy:`entries.object` to
retrieve all ancestors of a certain file. However, files can be shared among
directories, and the result of the transitive closure would be a flat set of
objects without information about their provenance within the file system. Thus,
it cannot be used to calculate file depth.

The predefined :alloy:`natural` module
---------------------------------------

.. index::
  util/natural module

To calculate the maximum depth of a file, we will need to calculate the depth of
its ancestors, select the maximum depth among them, and increment by 1. Since
the depth of the file system is always a positive integer number, we can encode
it as a natural number. Alloy provides a predefined library
:alloy:`util/natural` that provides a codification of natural numbers in plain
Alloy, and allows us to refrain from using the built-in type :alloy:`Int`. To
use this library, we need only to import it at the beginning of the Alloy model,
as follows.

.. code::

    open util/natural

This module introduces a signature :alloy:`Natural` with two distinguished singleton signatures, :alloy:`Zero` and :alloy:`One`. You can inspect all functions and predicates provided for :alloy:`Natural` by opening :alloy:`util/natural` in the menu :menuselection:`File --> Open Sample Models...`. These include functions :alloy:`inc[n : Natural]` and :alloy:`dec[n : Natural]` to increment and decrement a natural by 1, respectively, and arithmetic operations such as :alloy:`add[n1, n2 : Natural]` and :alloy:`sub[n1, n2 : Natural]`, for addition and subtraction, respectively. A total order is also imposed over :alloy:`Natural` using the predefined Alloy module :alloy:`ordering`, which introduces function such as :alloy:`max[ns : set Natural]` and :alloy:`min[ns : set Natural]`, and predicates such as :alloy:`gt[n1, n2 : Natural]` and :alloy:`lt[n1, n2 : Natural]`.

Note that by encoding naturals as a signature, they are bounded by the scope
specified for signature :alloy:`Natural`. For instance, if you increment a
natural beyond those allowed by the scope, it will just yield an empty set
(without any kind of error or warning). Luckily, in this example it is easy to
identify the maximum natural number needed, since we cannot have a file depth
larger than maximum number of :alloy:`Object` atoms specified in the scope.

.. card-carousel:: 2

   .. card:: Full model for the section
      :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/recursion/the-predefined-natural-module

      :octicon:`file-badge` Alloy model 
      ^^^
      Download and explore the files relevant for the model at this point of the book.

Recursive Alloy functions
-------------------------

.. index::
  function; recursive

Let us try to calculate the depth of the file system with the most obvious
strategy: a recursive Alloy function. Although not a particularly simple
function, it is possible to define it in Alloy. One possibility is to define it
as follows.

.. code::

    fun depth [o : Object] : Natural {
      o in Root implies Zero
      else inc[max[{n : Natural | some x : entries.object.o | n = depth[x]}]
    }

Given an object, if it is the root then return 0; else, calculate all naturals
that correspond to the depth of the directories that contain that object, select
the maximum and increment it by 1. The tricky part here is calculating the set
of depths of all the ancestors of an object. We've defined it by comprehension
by collecting all naturals for which there is a parent directory directory with
that depth.

We can now use this function to define a :alloy:`run` command that generates a
file system with a file at a certain depth. For instance, for depth 2, we could
execute the following command.

.. code::

    run depth2 {
      some f : File | depth[f] = inc[One]
    } for 5 but 3 Name

.. index::
  SAT solving
  Options menu
  Recursion depth menu option

The scope of 5 applies to both :alloy:`Object` and :alloy:`Natural`, so the
bound on naturals is enough to encode all possible file depths. However, you'll
actually get the following error from the Analyzer: *fun this/depth cannot call
itself recursively!* The fact is, the Analyzer's procedures, based on SAT
solving, cannot handle recursive definitions. Any recursive call to a function
would have to be explicitly unrolled, but it is not possible to know how many
unrolls would be needed in each case. Nonetheless, Alloy does support recursive
function definitions, but in a very restrictive manner since we have to impose a
bound on the number of function unrolls. This feature is disabled by default,
and must be turned on the options, and is limited to a maximum of 3 unrolls due
to performance issues. So, if we follow the menu option :menuselection:`Options
--> Recursion depth` and set it to :menuselection:`2` rather than
:menuselection:`disabled`, and then run the command again, we will finally
obtain the following instance.

.. image:: instance1.png
   :width: 500 px
   :align: center
   :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/recursion/instance_01_02/filesystem.als#L94-L106
   :alt: Get the code to generate this instance.

Now, let us try instead to find a file system with depth 3 with the following command.

.. code::

    run depth3 {
      some f : File | depth[f] = inc[inc[One]]
    } for 5 but 3 Name

Perhaps unsurprisingly, there is no such instance. That is because with a
recursion depth of 2, it is not possible for :alloy:`depth` to ever calculate
value 3 (it actually just returns :alloy:`none` in those cases). If we set menu
option :menuselection:`Options --> Recursion depth` to 3, we will now get the
following instance.

.. image:: instance2.png
   :width: 500 px
   :align: center
   :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/recursion/instance_01_02/filesystem.als#L109-L121
   :alt: Get the code to generate this instance.

It's evident that this approach can easily lead to unpredictable results. The
outcome of a command is dependent on an Analyzer option, which in general is a
bad practice in Alloy where models are expected to be self-contained. When the
maximum recursion depth allowed is exceeded, it just "fails silently" by
returning an empty relation. Moreover, the maximum recursion depth allowed by
the Analyzer is just 3, so we will never be able to calculate a file
:alloy:`depth` of 4 with this approach. Luckily, we can use a specification
pattern that allows us to circumvent these issues altogether. It is very rare
that recursive functions are useful in Alloy, so let's just keep
:menuselection:`Options --> Recursion depth` as :menuselection:`disabled`. 

.. card-carousel:: 2

   .. card:: Full model for the section
      :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/recursion/recursive-alloy-functions

      :octicon:`file-badge` Alloy model 
      ^^^
      Download and explore the files relevant for the model at this point of the book.

Recursion through memoization
-----------------------------

The alternative approach follows a strategy that resembles *memoization*: we
introduce a new field in the signature that is to be recursively traversed, and
store in this field the local result of the recursive call. Then, we
declaratively specify the value of this field for all atoms using only the
the value for its ancestors. There is, of course, a
trade-off: now the recursive result will be computed for all atoms of the
signature, and not only for a specific atom when called in a function.

In our example, we start by introducing a field to represent the depth of each
object, as follows.

.. code::

    abstract sig Object {
      depth : one Natural
    }

Next, we have to restrict the value of this field to the correct depth. This can
be done declaratively through the following fact.

.. code::

    fact calculate_depth {
      all o : Object | 
        o in Root implies o.depth = Zero 
        else o.depth = inc[max[(entries.object.o).depth]]]
    }

This fact defines the depth of each object :alloy:`o` as follows: if :alloy:`o` is
the root, it has depth 0; else it collects all the depths of the ancestors of
:alloy:`o`, selects the maximum, and increments it by 1. Notice that we no longer
need a relation by comprehension to collect the depths of the contents, since
they are already stored in a field.

The :alloy:`run` commands above could be executed exactly as they are due to the
dual syntax of dot join and box join. However, let us define them using dot join
to make it clear that :alloy:`depth` is now a field.

.. code::

    run depth2 {
      some f : File | f.depth = inc[One]
    } for 5 but 3 Name

After a few theme customizations (showing :alloy:`depth` as an attribute rather
than an edge, hiding :alloy:`Natural` atoms, and removing the namespace from
their labels), we obtain instances such as the following.

.. image:: instance3.png
   :width: 500 px
   :align: center
   :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/recursion/instance_03_04/filesystem.als#L94-L106
   :alt: Get the code to generate this instance.

We can now ask for file systems with a depth as big as that supported by the
scope on naturals. For instance, the following command still generates
instances, namely the example shown below.

.. code::

    run depth4 {
      some f : File | f.depth = inc[inc[inc[One]]]
    } for 5 but 3 Name

.. image:: instance4.png
   :width: 500 px
   :align: center
   :target: https://github.com/practicalalloy/models/blob/2024-02-28/structural-topics/recursion/instance_03_04/filesystem.als#L108-L120
   :alt: Get the code to generate this instance.

Beyond depth 4, with the current scope it is not possible to generate instances,
since there are obviously not enough objects. But even if we increase the scope
on objects and entries, it will not be possible to generate instances since the
natural 5 requires a scope of 6 on :alloy:`Natural` (natural 0 is also an atom).
So be careful to always update the scope of :alloy:`Natural` as needed.

.. card-carousel:: 2

   .. card:: Full model for the section
      :link: https://github.com/practicalalloy/models/tree/2024-02-28/structural-topics/recursion/recursion-through-memoization

      :octicon:`file-badge` Alloy model 
      ^^^
      Download and explore the files relevant for the model at this point of the book.