.. index:: data; specification

Data specifications
===================

.. highlight:: mcrl2 

This page describes all built-in data types with their associated functions and 
operators, and describes how custom data types can be defined.

A data specification consists of a number of *sorts*, a number of *constructors*
for each sort, a number of *mappings*, and a set of *equations*. A data 
specification is an equational specification, in which sorts denote data types. 
The semantics of a sort is a non-empty set. The elements of the semantics of a 
sort are described by its constructors, whereas the mappings are functions 
defined on the semantics of sorts. The equations (axioms) describe equational 
properties of functions and elements of the semantics.

Note that every element of the semantics of a sort can be constructed from its
constructors (this is a property also known as "no junk"). It may however be the
case that an element can be described by several constructors (in which case it
violates a property commonly known as "no confusion"). The only exception to
this are the booleans; ``true`` and ``false`` are distinct elements.

In mCRL2, a sort is either a :ref:`predefined sort <predefinedsorts>`, a 
:ref:`constructed sort <constructedsorts>`, or a sort that was declared in a 
:ref:`sort specification <sortspec>`. The grammar of a sort description is given
by the non-terminal :token:`SortExpr`. 

.. dparser:: ProjDecl ProjDeclList ConstrDecl ConstrDeclList SortExpr

.. _sortspec:

.. index:: sort, cons

Specifying sorts
----------------

In an mCRL2 specification, sorts may be declared in a sort specification. In the
grammar below, a sort specification is generated by the non-terminal 
:token:`SortSpec` in the grammar below.

.. dparser:: SortDecl SortSpec IdsDecl ConsSpec

Sort specifications are best understood by looking at an example. We will define
a sort ``Natural``, representing the natural numbers. We will do so by defining 
a constructor ``zero`` for it, and a successor relation ``succ``::

  sort Natural;
  cons zero: Natural;
       succ: Natural -> Natural;

Note that if we leave out the ``cons`` statement, we have still defined the sort
``Natural``. In that case, however, mCRL2 will not know anything about this sort
except that it represents a non-empty set. There are cases in which such 
underspecification can be used, for instance to model user data that passes 
through a system, but that does not influence the behaviour of a system.

The syntax of constructor specifications is given by the :token:`ConsSpec` 
non-terminal above. Every constructor for a sort *S* must be specified in a 
``cons`` block, and is specified by a name and a sort that is a mapping to *S*.
Note that *S* can be seen as a nullary mapping to *S*. 


A sort can either be one one of the 
predefined sorts, or a sort that you specified yourself (or will specify later
in the specification, as the order of the statements in an mCRL2 specification
does not change the meaning of the specification).

.. _binaryint:

Let's have a look at a slightly more complicated encoding of numbers, in this
case the positive numbers. We will use the predefined sort ``Bool``, which 
consists of the (distinct) elements ``true`` and ``false``::

  sort Positive;
  cons one: Positive;
       cdub: Bool # Positive -> Positive;

If we now interpret the term :samp:`cdub(true, {num})` (where *num* is a term
of sort ``Positive``) as "twice the number that *num* represents, plus 1", and interpret
:samp:`cdub(false, {num})` as "twice the number that *num* represents", 
then we have created a binary encoding of the positive numbers. For 
instance, ``cdub(true, one)`` represents the number 3, and 
``cdub(false, cdub(true, cdub(false, one)))`` represents the number 10.

.. note::

   In mCRL2, the encoding of numbers (integers, positive numbers and natural 
   numbers) is binary, much like the example above. 

.. hint::

   If you need a more complex sort than described above, you will usually be 
   able to make a :ref:`constructed sort <constructedsorts>` that suits your 
   needs.

.. index:: data; expression, whr, where clause

Data expressions
----------------

Data expressions are descriptions of an element of a sort. Therefore, any 
closed, well-typed expression is a data expression. The full grammar is given
below. 

.. dparser:: DataExpr DataExprList BagEnumElt BagEnumEltList IdList VarDecl 
   VarsDecl VarsDeclList Assignment AssignmentList

A notable construction that is not standard is the *where clause*, which can be
used to substitute subexpressions in a data expression. Where clauses can be 
useful for efficiency reasons. For example, we can define a function that 
computes the square of the sum of two numbers as follows::

  map square_sum: Int # Int -> Int;
  var x, y: Int;
  eqn square_sum(x, y) = (x + y) * (x + y);

When evaluating ``square_sum(2, 3)``, this will rewrite to ``(2 + 3) * (2 + 3)``, 
which causes the expression ``2 + 3`` to be evaluated twice.

Using a where clause we enforce that the right-hand sides of local definitions
is evaluated exactly once::

  var x, y: Int;
  eqn square_sum(x,y) = z * z whr z = x + y end;

Note that technically a where clause just introduces a beta-redex, so we could
also have defined the following::

  var x, y: Int;
  eqn square_sum(x, y) = (lambda z: Int . z * z)(x + y);

.. index:: map, var, eqn

Specifying mappings
-------------------

Mappings, like constructors, are functions that take zero or more arguments. The
difference lies in the fact that mappings say nothing about the sort that is 
their image (where constructors show you how to construct elements of that 
sort). 

To be more precise, mappings are aliases for an element of a specific sort, and
can be specified by the following grammar:

.. dparser:: IdsDecl MapSpec

Equational specifications give further information about how the elements that
these aliases represent behave. Equational specifications are given by the 
grammar below.

.. dparser:: VarsDecl VarsDeclList VarSpec EqnDecl EqnSpec

Equation systems are optionally preceded by a ``var`` block that defines 
variables that are used in the ``eqn`` block that follows. Variables are used to
do pattern matching in equation systems. To illustrate this, let us look at a
specification of the Fibonacci sequence::

   map fib: Nat -> Nat;
   var n: Nat;
   eqn n <= 1 -> fib(n) = n;
       n > 1 -> fib(n) = fib(Int2Nat(n - 1)) + fib(Int2Nat(n - 2))
   
Going through the code line by line, we see a mapping ``fib`` being defined that
maps natural numbers to natural numbers. Then a variable ``n`` of sort ``Nat``
is declared. 

On the third line, the first rewrite rule is declared, that says that if a term 
of the form ``fib(n)`` is encountered, where ``n`` is the variable and can hence
match any term of sort ``Nat``, then it can be rewritten to the value that
matches the variable, *if* that value is at most 1. 

The second rewrite rule says that if a term of the form ``fib(n)`` is
encountered, then it can be rewritten to ``fib(Int2Nat(n - 1)) + fib(Int2Nat(n 
- 2))`` if ``n`` was larger than 1.

In the above, we need to use ``Int2Nat`` to convince the type checking system 
that ``n-1`` and ``n-2`` will indeed be natural numbers. In general this is not
true (for ``n <= 1``), but we are making the executive decision that we know 
better than the type checker, because we know that the condition of the rewrite
rule will prevent us from getting into trouble.

.. admonition:: Example (underspecification)
   :class: collapse

   Consider the following data specification::

     sort A, B;
     cons b: B;
     map f: A;
         g: B;
         h: A -> B;
     var a: A;
     eqn h(a) = b; 

   The sort ``B`` is defined as the singleton set ``{b}``, but ``A`` is left 
   unspecified. Therefore, we cannot know what element ``f`` maps to. For ``g``
   on the other hand, we know that ``g`` maps to ``b``, as it is the only
   element of ``B``, but as this is not specified in the equational
   specification, mCRL2 will not detect this. However, the data expression
   ``h(f)`` will be rewritten to ``b``, as it matches the only rule in this
   equation system.

.. admonition:: Example (rewrite rules)
   :class: collapse

   In order to describe the behaviour of mappings, we need to
   give mCRL2 an equational specification of the mapping we wish to define. As an
   example, we will specify the exclusive or operation on booleans::

    map xor: Bool # Bool -> Bool;
    eqn xor(false, false) = false;
        xor(false, true) = true;
        xor(true, false) = true;
        xor(true, true) = false;

   This is rather verbose if we know that we already have a definition of
   inequality of booleans. We could therefore also specify it as follows::

     map xor: Bool # Bool -> Bool;
     var a, b: Bool;
     eqn xor(a, b) = a != b;

   Yet another way of specifying the same mapping would be to use the rewrite
   conditions to test for equality::

     map xor: Bool # Bool -> Bool;
     var a, b: Bool;
     eqn a == b -> xor(a, b) = false;
         a != b -> xor(a, b) = true;

.. warning::

   Functional programmers might have written down the following specification for
   the Fibonacci sequence::

     map fib: Nat -> Nat;
     var n: Nat;
     eqn fib(0) = 0;
         fib(1) = 1;
         fib(n + 2) = fib(n) + fib(n + 1);

   This, however, will not work in mCRL2: ``fib(10)`` will not rewrite at all. 
   The reason is that the pattern matching used in the rewrite system fails to 
   match ``n + 2`` to ``10``, because the number 10 is internally represented
   using a :ref:`binary encoding <binaryint>`, and therefore has a different
   structure than ``n + 2``.

   This kind of pattern matching can still be used, but it is advisable to only
   match terms that consist of only constructors and variables. One particularly
   useful example is that of lists, for which the constructors ``[]`` and ``|>``
   are defined::

     map remove: List(Nat) # Nat -> List(Nat);
     var x, y: Nat;
         l: List(Nat);
     eqn remove([], x) = []; 
         x == y -> remove(x |> l, y) = l;
         x != y -> remove(x |> l, y) = x |> remove(l, y);

.. _predefinedsorts:

.. index:: ==;equality,==,
           <,<;less than, <;subset, <;lexicographical ordering,
           >,>;greater than, >;superset, >;lexicographical ordering,
           <=,<=;less than or equal to, <=;subset or equal to, <=;lexicographical ordering,
           >=,>=;greater than or equal to, >=;subset or equal to, >=;lexicographical ordering,
   single: if(_,_,_)

Predefined mappings
-------------------

The mappings in the following table are defined on all sorts, even on 
user-defined sorts.

.. list-table:: Predefined operations on *all* sorts
   :header-rows: 1
   :widths: 7 12 50

   * - Name
     - Sort(s)
     - Semantics
   * - :samp:`{a} == {b}`
     - :samp:`{S} # {S} -> Bool`
     - Equality
   * - :samp:`{a} != {b}`
     - :samp:`{S} # {S} -> Bool`
     - Inequality, always equivalent to :samp:`!({a} == {b})`
   * - :samp:`{a} < {b}`
     - :samp:`{S} # {S} -> Bool`
     - Less than
   * - :samp:`{a} > {b}`
     - :samp:`{S} # {S} -> Bool`
     - Greater than, always equivalent to :samp:`{b} < {a}`
   * - :samp:`{a} <= {b}`
     - :samp:`{S} # {S} -> Bool`
     - Less than or equal to, always equivalent to :samp:`{a} < {b} || {a} == {b}`.
   * - :samp:`{a} >= {b}`
     - :samp:`{S} # {S} -> Bool`
     - Greater than or equal to, always equivalent to :samp:`{b} <= {a}`
   * - :samp:`if({c}, {a}, {b})`
     - :samp:`Bool # {S} # {S} -> {S}`
     - Conditional value

For any sort ``S`` (even for user defined sorts), the mappings have the 
following equational properties::

  var s, t: S;
      b: Bool;
  eqn s == s -> true;
      s < s -> false;
      s <= s -> true;
      if(true, s, t) = s;
      if(false, s, t) = t;
      if(b, s, s) = s;

For mapping sorts and user defined sorts, only these equations are specified.

For the predefined sorts, the mappings work as expected (so ``12 < 16`` and
``23/12 == 46/24``). For lists, the ``<`` and ``<=`` operators define the
lexicographical ordering (so ``[2, 3] > [1, 2, 3]``, and ``[] < [1]``). For sets
and bags, they define the subset (resp. subbag) relation.

Finally, for structured sorts, the definitions of ``<`` and ``<=`` are a bit 
more involved; they are described in the section about :ref:`structured sorts
<structuredsorts>`.

.. note::

   The fact that every predefined and constructed sort has a strict ordering 
   associated with it makes it possible for mCRL2 to define a fairly efficient 
   implementation of sets. 

.. warning:: 

   Be careful when specifying user defined sorts: the above operations are only
   partially defined. Trying to compare two syntactically different data 
   expressions may not lead to the desired result, unless additional rewrite
   rules for ``==``, ``<`` and ``<=`` are added.

   In particular, the following will not work as expected::

     sort S;
     cons a, b: S;
     map x: Set(S);
     eqn x = {a} + {b};

   Evaluating ``x`` will show you that it is equal to 
   ``@fset_union(@false_, @false_, {a}, {b})``, which may not be what you were
   expecting to see. Completing the definition of ``<`` for ``S`` fixes the 
   problem::

     sort S;
     cons a, b: S;
     map x: Set(S);
     eqn x = {a} + {b};
         a < b = true;
         b < a = false;

   Now, ``x`` evaluates to ``{a, b}``.

.. index:: Bool, Nat, Pos, Int, Real, true, false

Predefined sorts
----------------

To make modelling more convenient, mCRL2 provides a number of predefined sorts.
These sorts are listed in the table below. In section :ref:`predefinedmappings` standard operations 
are defined on all predefined sorts.

.. table:: Basic sorts in mCRL2

   ======== ================
   Sort     Semantics       
   ======== ================
   ``Bool`` Booleans         
   -------- ----------------
   ``Pos``  Positive numbers 
   -------- ----------------
   ``Nat``  Natural numbers
   -------- ----------------
   ``Int``  Integers
   -------- ----------------
   ``Real`` Rationals
   ======== ================


The constants ``true`` and ``false`` are defined as the only constructors for
the sort ``Bool``.

Any :token:`Number` that occurs in mCRL2 input is interpreted as a constant of
one of the integral sorts. All datatypes, including the standard data types, are
internally represented using abstract data types. This has the advantage that
numbers do not have a limited range. In particular, there is no largest number
in any of these domains, and there are no smallest integers and reals.

.. admonition:: Example

   If the mCRL2 toolset encounters the string ``1024`` in a context where a 
   ``Pos``, ``Nat``, ``Int`` or ``Real`` was expected, then it will be 
   interpreted as the decimal number ``1024`` of sort ``Pos``, as this is the
   most specific type that matches.

.. admonition:: Example

   To specify the decimal fractional value ``3.141592``, you will need to 
   specify it as a fraction, *i.e.*, ``3141592/1000000``.

.. index:: min, max, mod, div, exp, 
           succ, pred, forall, exists, round, floor, ceil
   triple: mathematical;addition;+
   triple: mathematical;multiplication;*
   triple: mathematical;subtraction;-
   triple: mathematical;negation;-
   triple: logical;not;!
   triple: logical;and;&&
   triple: logical;or;||
   triple: logical;implication;=>


.. _predefinedmappings:

Mappings on predefined sorts
""""""""""""""""""""""""""""

For the predefined sorts, mCRL2 defines some common operations. The predefined
operations on the Booleans are given in the table below.

.. list-table:: Predefined operations on Booleans
   :header-rows: 1
   :widths: 20 30 50

   * - Name
     - Sort(s)
     - Semantics
   * - :samp:`! {a}`
     - ``Bool -> Bool``
     - Logical negation
   * - :samp:`{a} && {b}`
     - ``Bool # Bool -> Bool``
     - Logical and
   * - :samp:`{a} || {b}`
     - ``Bool # Bool -> Bool``
     - Logical or
   * - :samp:`{a} => {b}`
     - ``Bool # Bool -> Bool``
     - Logical implication
   * - :samp:`forall {V} . {b}`
     - ``Bool -> Bool``
     - Universal quantifier
   * - :samp:`exists {V} . {b}`
     - :samp:`Bool -> Bool`
     - Existential quantifier

The universal and existential quantifier need some extra clarification. Their
concrete syntax (as given by the non-terminal :token:`DataExpr`) is illustrated
in the example below::

  exists n, m: Nat, p: Pos . n + m == p;

The :samp:`{V}` in the table above is a specification of locally bound 
variables, that occur in the expression after the period (``.``). Evaluation of
quantifiers is done by using the constructors of a sort to enumerate all 
possible values of that sort, and then check for each such value whether the
expression holds. This means that evaluation some quantifiers will not 
terminate::

  exists n: Nat . n + 1 == n + 2
  exists n: Nat . n - 1 == n - 2

The upper expression will evaluate to ``false``, because the rewriter happens to
rewrite ``n + 1`` and ``n + 2`` to a form in which it can prove that they are
not equal. The expression below that, however, will be rewritten forever, 
because the rewriter will decide to check the equality for every value of ``n``.

For the numeric sorts, the predefined mappings are listed in the table below.
Where :samp:`{N}` is used in the sort of a mapping, any numeric sort may be
substituted.

.. list-table:: Predefined operations on numeric sorts
   :header-rows: 1
   :widths: auto
   :width: 100%

   * - Name
     - Sort(s)
     - Semantics
   * - :samp:`- {a}`
     - | ``Pos -> Int``
       | ``Nat -> Int``
       | ``Int -> Int``
       | ``Real -> Real``
     - Negation
   * - :samp:`min({a}, {b})`
     - :samp:`{N} # {N} -> {N}`
     - Minimum of :samp:`{a}` and :samp:`{b}`.
   * - :samp:`max({a}, {b})`
     - :samp:`{N} # {N} -> {N}`
     - Maximum of :samp:`{a}` and :samp:`{b}`.
   * - :samp:`{a} + {b}`
     - | ``Pos # Pos -> Pos``
       | ``Pos # Nat -> Pos``
       | ``Nat # Pos -> Pos``
       | ``Nat # Nat -> Nat``
       | ``Int # Int -> Int``
       | ``Real # Real -> Real``
     - Sum (addition) of :samp:`{a}` and :samp:`{b}`.
   * - :samp:`{a} - {b}`
     - | ``Pos # Pos -> Int``
       | ``Nat # Nat -> Int``
       | ``Int # Int -> Int``
       | ``Real # Real -> Real``
     - Difference (subtraction) of :samp:`{a}` and :samp:`{b}`.
   * - :samp:`{a} * {b}`
     - :samp:`{N} # {N} -> {N}`
     - Product (multiplication) of :samp:`{a}` and :samp:`{b}`
   * - :samp:`{a} / {b}`
     - :samp:`{N} # {N} -> Real`
     - Quotient (division) of :samp:`{a}` and :samp:`{b}`
   * - :samp:`succ({a})`
     - | ``Pos -> Pos``
       | ``Nat -> Pos``
       | ``Int -> Int``
       | ``Real -> Real``
     - Successor (equivalent to :samp:`a + 1`)
   * - :samp:`pred({a})`
     - | ``Pos -> Nat``
       | ``Nat -> Int``
       | ``Int -> Int``
       | ``Real -> Real``
     - Predecessor (equivalent to :samp:`a - 1`)
   * - :samp:`{a} div {b}`
     - | ``Nat # Pos -> Nat``
       | ``Int # Pos -> Int``
     - Integer division
   * - :samp:`{a} mod {b}`
     - | ``Nat # Pos -> Nat``
       | ``Int # Pos -> Nat``
     - Remainder of :samp:`{a}` divided by :samp:`{b}`.
   * - :samp:`exp({a}, {b})`
     - | ``Pos # Nat -> Pos``
       | ``Nat # Nat -> Nat``
       | ``Int # Nat -> Int``
       | ``Real # Int -> Real``
     - Exponentiation (:samp:`{a}` raised to the power :samp:`{b}`).
   * - :samp:`abs({a})`
     - | ``Int -> Nat``
       | ``Real -> Real``
     - Absolute value of :samp:`{a}`.
   * - :samp:`floor({a})`
     - ``Real -> Int``
     - The greatest integer smaller than :samp:`{a}`.
   * - :samp:`ceil({a})`
     - ``Real -> Int``
     - The least integer larger than :samp:`{a}`.
   * - :samp:`round({a})`
     - ``Real -> Int``
     - Equal to :samp:`floor({a} + 1/2)`.
   * - ``Pos2Nat(_)``
     - ``Pos -> Nat``
     - Cast
   * - ``Nat2Pos(_)``
     - ``Nat -> Pos``
     - Cast

.. index:: Casts;Pos2Nat, Casts;Nat2Pos, Casts;Int2Nat, Casts;Nat2Int,
           Casts;Pos2Int, Casts;Int2Pos, Casts;Pos2Real, Casts;Real2Pos,
           Casts;Nat2Real, Casts;Real2Nat, Casts;Int2Real, Casts;Real2Int

Lastly, there are a number of casts that allow the user to interpret a numeric
value as if it were of a different sort. To this end, the mappings :samp:`{A2B}`
are defined, where :samp:`{A}` and :samp:`{B}` are either of ``Pos``, ``Nat``,
``Int`` or ``Real``.

.. _constructedsorts:

Constructed sorts
-----------------

To enable users to quickly specify more complicated sorts without having to 
resort to manually specifying constructors and operations on those sorts, mCRL2
provides some standard constructs to build new sorts out of existing ones. 

.. dparser:: SortExpr

.. index:: ->, #, lambda, ();function application, function application

Mapping sorts
"""""""""""""

If ``D1``, ``D2``, ..., ``DN`` are sorts, and ``I`` is a sort, then ``D1 # D2
# ... # DN -> I`` is the sort of a mapping from the carthesian product of
``D1`` through ``DN`` to ``I``. Note that ``#`` and ``->`` are distinct operators,
the first creating the carthesian product of two sorts, and the second creating
a sort that represents the mapping of one sort to another. The use of carthesian
products as sorts is however limited in mCRL2: they may only occur as the domain
of mapping sorts. One further exception will be made later, when we look at the
process language, where we will see that also actions are allowed to have a sort
that is a carthesian product.

.. list-table:: Predefined operations on mapping sorts
   :header-rows: 1
   :widths: 15 20 50

   * - Name
     - Sort(s)
     - Semantics
   * - :samp:`{a}({b1}, ..., {bN})`
     - :samp:`({S1} # ... # {SN} -> {I}) # {S1} # ... # {SN} -> {I}`
     - Function application (applies :samp:`{a}` to arguments :samp:`{b1}` 
       through :samp:`{bN}`).
   * - :samp:`{a}[{b} -> {c}]`
     - :samp:`({S} -> {I}) # {S} # {I} -> ({S} -> {I})`
     - Function update; returns a mapping that maps :samp:`{b}` to :samp:`{c}`,
       and that maps all other elements like :samp:`{a}` does.
   * - :samp:`lambda {V} . {a}`
     - :samp:`{S} -> {I}`
     - Lambda abstraction.

The syntax of lambda abstraction is similar to that of quantifiers. As an 
example, we define the mapping ``f`` that returns ``true`` if the sum of its 
first two arguments is equal to the third argument::

  map f: Nat # Nat # Pos -> Bool;
  eqn f = lambda x,y: Nat, p: Pos . x + y == p

For mappings that take one argument, we can use function updates to change a
mapping locally, which can be useful to model (infinite) arrays::

  sort Array = Nat -> Bool;
  map set: Array # Nat -> Array;
      clear: Array # Nat -> Array;
  var a: Array;
      n: Nat;
  eqn set(a, n) = a[n -> true];
      clear(a, n) = a[n -> false];

.. index:: in, List, Set, Bag

Lists, sets and bags
""""""""""""""""""""

mCRL2 defines a number of "containers": meta-sorts that allow you to specify a
list, set or bag (multiset) of a certain sort.

.. table:: Container sorts in mCRL2

   =================== =======================================
   Sort                Semantics
   =================== =======================================
   :samp:`List({S})`   Lists with elements of sort :samp:`{S}`
   ------------------- ---------------------------------------
   :samp:`Set({S})`    Sets with elements of sort :samp:`{S}`
   ------------------- ---------------------------------------
   :samp:`Bag({S})`    Bags with elements of sort :samp:`{S}`
   =================== =======================================

For these container sorts, a number of operations is defined. One operation is
defined on all containers (substitute ``List``, ``Set`` or ``Bag`` for 
:samp:`{C}`):

.. list-table:: Predefined operations on containers
   :header-rows: 1
   :widths: 10 20 60

   * - Name
     - Sort(s)
     - Semantics
   * - :samp:`{a} in {b}`
     - :samp:`{C}(S) # S -> {C}(S)``
     - True if :samp:`{a}` occurs in :samp:`{b}`, false otherwise.

.. index:: head, tail, rhead, rtail, empty;list
   triple: list;constructor;[]
   triple: list;enumeration;[]
   triple: list;constructor;|>
   triple: list;snoc;<|
   triple: list;length;#
   triple: list;concatenation;++
   triple: list;element extraction;.

Lists
'''''

For a given sort :samp:`{S}`, mCRL2 defines the ``[]`` as a constructor of 
sort ``List(S)``, representing the empty list. Furthermore, the constructor
``|>`` (pronounce "cons") of sort ``S # List(S) -> List(S)`` is defined. List
enumeration is defined as a shorthand to denote lists::

  [a, b, ...] == a |> b |> ... |> []

.. list-table:: Predefined operations on lists
   :header-rows: 1
   :widths: 15 30 40

   * - Name
     - Sort(s)
     - Semantics
   * - :samp:`{a} <| {b}` ("snoc")
     - ``List(S) # S -> List(S)``
     - :samp:`{a}` with :samp:`{b}` appended to it.
   * - :samp:`{a} in {b}`
     - ``S # List(S) -> Bool``
     - True if :samp:`{a}` occurs in :samp:`{b}`, false otherwise.
   * - :samp:`# {a}`
     - ``List(S) -> Nat``
     - The length of :samp:`{a}`.
   * - :samp:`{a} . {b}`
     - ``List(S) # Nat -> S``
     - The element of :samp:`{a}` at position :samp:`{b}`. Indices are zero-based.
   * - :samp:`{a} ++ {b}`
     - ``List(S) # List(S) -> List(S)``
     - :samp:`{a}` concatenated with :samp:`{b}`.
   * - :samp:`head({a})`
     - ``List(S) -> S``
     - The first element of :samp:`{a}`.
   * - :samp:`tail({a})`
     - ``List(S) -> List(S)``
     - :samp:`{a}` without its first element.
   * - :samp:`rhead({a})`
     - ``List(S) -> S``
     - The last element of :samp:`{a}`.
   * - :samp:`rtail({a})`
     - ``List(S) -> List(S)``
     - :samp:`{a}` without its last element.
  
.. warning::

   Lists are implemented as singly-linked lists. This means that the ``#``
   operation is quite expensive (it has to run through the entire list), as 
   are the ``<|``, ``rhead`` and ``rtail`` operations.

.. warning::

   The ``head`` (or ``rhead``) of an empty list is not defined. In practice, 
   this means that ``head([])`` will not be rewritten any further.

.. index:: empty;set
   triple: set;constructor;{}
   triple: set;enumeration;{}
   triple: set;comprehension;{}
   triple: set;difference;-
   triple: set;union;+
   triple: set;intersection;*
   triple: set;complement;!

Sets
''''

Sets are defined in a similar fashion to lists. For every sort``S``, ``Set(S)``
denotes the sort of sets of elements from ``S``. One constructor is publicly
available: ``{}``, the empty set. The other constructors are hidden from the 
user, as they are implementation specific. Sets can, like lists, be enumerated: 
``{a, b, c}`` denotes the set containing elements ``a``, ``b`` and ``c``.
Operations on sets are given by the following table.

.. list-table:: Predefined operations on sets
   :header-rows: 1
   :widths: 15 30 40

   * - Name
     - Sort(s)
     - Semantics
   * - :samp:`{ {a} : {S} | {b(a)} }`
     - :samp:`({S} -> Bool) -> Set({S})`
     - Set comprehension: denotes the set of elements :samp:`{a}` in :samp:`{S}`
       for which :samp:`{b(a)}` is true.
   * - :samp:`!{a}`
     - :samp:`Set({S}) -> Set({S})`
     - Set complement of :samp:`{a}`.
   * - :samp:`{a} + {b}`
     - :samp:`Set({S}) # Set({S}) -> Set({S})`
     - Set union of :samp:`{a}` and :samp:`{b}`.
   * - :samp:`{a} - {b}`
     - :samp:`Set({S}) # Set({S}) -> Set({S})`
     - Set difference of :samp:`{a}` and :samp:`{b}`.
   * - :samp:`{a} * {b}`
     - :samp:`Set({S}) # Set({S}) -> Set({S})`
     - Set intersection of :samp:`{a}` and :samp:`{b}`.

A typical use of the set comprehension is for instance the following definition
of the set of all prime numbers::

  { n: Pos | n > 1 && forall m, m': Pos . (m > 1 && m' > 1) => n != m * m' }

.. index:: empty;bag, count, Set2Bag, Bag2Set
   triple: bag;constructor;{}
   triple: bag;enumeration;{}
   triple: bag;comprehension;{}
   triple: bag;difference;-
   triple: bag;union;+
   triple: bag;intersection;*
   triple: bag;complement;!

Bags
''''

Bags (or multisets) are denoted much like sets, but require a count for every
element::

  {a:1, b:4, c:0} == {a:1, b:2, b:2} == {a:1, b:4}

The same operations as for sets are defined on bags, with the difference that
bag comprehensions specify the number of times an element occurs in that bag.
For example, the bag that contains every natural number twice is defined as
follows::

  { n: Nat | 2 }

One additional operation is defined on bags to count how often an element occurs in a bag:

.. list-table:: Predefined operations on sets
   :header-rows: 1
   :widths: 15 30 40

   * - Name
     - Sort(s)
     - Semantics
   * - :samp:`count({a}, {b})`    
     - :samp:`{S} # Bag({S}) -> Nat`
     - The number :samp:`{a}`s in :samp:`{b}`.

To make it easy to interpret sets as bags, and to convert bags to sets, the 
following operations are also defined:

.. list-table:: Predefined operations on sets
   :header-rows: 1
   :widths: 10 15 40

   * - Name
     - Sort(s)
     - Semantics
   * - :samp:`Set2Bag({a})`
     - :samp:`Set({S}) -> Bag({S})`
     - The bag ``b`` such that for all ``x`` in :samp:`{S}`, 
       ``count(b, x)`` is 1 if :samp:`x in {a}`, and 0 otherwise.
   * - :samp:`Bag2Set({a})`
     - :samp:`Bag({S}) -> Set({S})`
     - The set ``b`` such that for all ``x`` in :samp:`{S}`, ``x in b`` iff 
       :samp:`x in {a}`.

.. _structuredsorts:

Structured sorts
""""""""""""""""

Structured sorts are a short way to specify recursive data types as are 
commonly used in functional programming languages. 

A structured type is of the following form::

  struct c_1(p_1_1: S_1_1, ..., p_1_k1: S_1_k1)?r_1
         c_2(p_2_1: S_2_1, ..., p_2_k2: S_2_k2)?r_2
         ...
         c_n(p_n_1: S_n_1, ..., p_n_kn: S_n_kn)?r_n

This defines the type which we designate by ``S`` for brevity, together with the 
following functions::

  cons c_i: S_i_1 # ... # S_i_ki -> S;
  map p_i_j: S -> S_i_j;
      r_i: S -> Bool;

Here, ``p_i_j`` are projection functions, and ``r_i`` are recogniser functions.
Projection and recogniser functions are optional; if a projection function is
not specified the subsequent ``:`` symbol should also be left out, likewise if a
recogniser function is not specified its preceding ``?`` symbol should also be 
left out (see below for examples).

Note that structured sorts are often used in combination with sort references::

  sort S = struct ... ;

This defines a structured sort which has ``S`` as an alias.

.. note::

   The constructors of a structured sorts can be compared with the ``<`` and 
   ``<=`` operators. They are defined as lexicographical orderings on the 
   constructors and their elements: the first constructor specified is the least
   element, the last constructor the greatest; if a constructor has arguments,
   then two terms that have the same constructor as outermost symbol are 
   compared by comparing their arguments lexicographically (left-to-right).

.. admonition:: Example
   :class: example collapse

   A well known and illustrative example of a structured sort is the definition
   of the tree data structure in which elements of some sort ``A`` can be 
   stored::

     sort Tree = struct leaf(A) | node(Tree, Tree);

   This specifies that a tree is either an expression of the form ``leaf(a)``
   where ``a`` is an expression of sort ``A``, or a tree is an expression of the
   form ``node(u, v)`` where ``u`` and ``v`` are expressions of sort ``Tree``.
   What is actually generated out of this one line, is the following data 
   specification::

      sort Tree;
      cons leaf: A -> Tree;
           node: Tree # Tree -> Tree;
      var a, a': A;
          l, r, l', r': Tree;
      eqn leaf(a) == leaf(a') = a == b;
          leaf(a) == node(l, r) = false;
          node(l, r) == leaf(a) = false;
          node(l, r) == node(l', r') = l == l' && r == r';
          leaf(a) < leaf(a') = a < a';
          leaf(a) < node(l, r) = true;
          node(l, r) < leaf(a) = false;
          node(l, r) < node(l', r') = l < l' || (l == l' && r < r');
          leaf(a) <= leaf(a') = a <= a';
          leaf(a) <= node(l, r) = true;
          node(l, r) <= leaf(a) = false;
          node(l, r) <= node(l', r') = l < l' || (l == l' && r <= r');

   We can extend our tree to also have recogniser and projection functions::

     sort Tree = struct leaf(value: A) ? is_leaf 
                      | node(left: Tree, right: Tree) ? is_node;

   This causes the following additional data specification to be added::

     map value: Tree -> A;
         left: Tree -> Tree;
         right: Tree -> Tree;
         is_leaf: Tree -> Bool;
         is_node: Tree -> Bool;
     var a: A;
         l, r: Tree;
     eqn value(leaf(a)) = a;
         left(node(l, r)) = l;
         right(node(l, r)) = r;
         is_leaf(leaf(a)) = true;
         is_leaf(node(l, r)) = false;
         is_node(leaf(a)) = false;
         is_node(node(l, r)) = true;

   The projection functions now enable you to extract data from trees::

     map dfs: Tree -> List(A);
     var t: Tree;
     eqn is_leaf(t) -> dfs(t) = [value(t)];
         is_node(t) -> dfs(t) = dfs(left(t)) ++ dfs(right(t));

.. admonition:: Example
   :class: example collapse

   An often used structured type is the enumerated type that consists of a
   finite number of elements. For instance, the sort ``MachineMode`` can be 
   declared by
   ::

     sort MachineMode = struct idle ? is_idle 
                             | running ? is_running 
                             | broken ? is_broken;

   Note that ``idle < running`` and ``running < broken``: there is a strict 
   ordering on the constructors of the structured sort.

.. admonition:: Example
   :class: example collapse

   A common example is the sort of pairs for given sorts ``A`` and ``B``::

     sort Pair = struct pair(fst: A, snd: B);

   For a pair ``p`` the expression ``fst(p)`` gives its first element and 
   ``snd(p)`` the second element.

.. index:: glob

Global variables
----------------

.. dparser:: GlobVarSpec

In process specifications and in parameterised boolean equation systems (PBESs),
it is possible to use free variables. An example is the following::

  act a;
  glob x: Nat;
  proc P = a(x) . P;
  init P;

This represents a whole class of processes, namely for every value of x this
process has a different value. The keyword ``glob`` stands for *global variable*. In
each specification the keyword ``glob`` can be used an arbitrary number of times.

All ``glob`` declarations are grouped together. The names of the variables cannot
coincide with other declared functions, processes, actions, variables (both in
equations and in sum operators) and process and PBES parameters. Global
variables can occur in process equations, in parameterised fixed point formulas
and in ``init`` sections.

Global variables can be used in the common mathematical way. Consider for 
instance the equation: :math:`ax^2 + bx + c = 0`. There are four variables in 
this equation, namely :math:`a, b, c` and :math:`x`. The use of the variables 
:math:`a, b` and :math:`c` allow to study this polynomial in a far more general 
setting than when these variables would have concrete values.

In some cases, the concrete values for global variables do not have influence
on the process. In such a case instantiating the global variables to various
concrete values will mean that the process has the same behaviour modulo
strong bisimulation, or the same solution as a parameterised boolean equation
system. In this case we call the process or PBES *global variable insensitive*. 

An example is the following linearisation of a buffer::

  sort D;
  glob dummy1, dummy2: D;
  act read, send: D;
  proc P(b: Bool, d: D) = 
         sum e: D . b -> read(e) . P(false, e) + 
                   !b -> send(d) . P(true, dummy1);
  init P(true, dummy2);

The idea is that if the parameter ``b`` is true, the value of the second 
parameter is not relevant anymore. Therefore, it can be set to any arbitrary 
value, which is indicated by the use of ``dummy1`` and ``dummy2``. As this 
specification is global variable insensitive, arbitrary concrete values can be 
chosen for these global variables if this is opportune.

The tool :ref:`tool-mcrl22lps` may generate linear processes with global
variables. It guarantees that the resulting specification is global variable
insensitive. Certain transformation tools, like :ref:`tool-lpsconstelm` and
:ref:`tool-lps2pbes` yield global variable insensitive output, provided the
input in global variable insensitive. In case systems are not global variable
insensitive the output of these tools can be garbage. It is the responsibility
of those who apply the tools that the tools are used in a proper way. It is
likely that most tools leave global variables untouched, unless a switch
indicates that global variable insensitivity can be used.