==========
Signatures
==========

Propositional signatures
------------------------

A *propositional signature* is a family :math:`\Sigma=\{\Sigma_k\}_{k\in\omega}`
such that each :math:`\Sigma_k` is a collection of :math:`k`-ary *connectives*.

In *ct4l*, we have a class that represents connectives, whose members are
simply a string referring to the connective symbol and an integer representing
the arity of the connective. For example, the code below creates a 
connective :math:`\#` of arity :math:`2` (or binary):

.. code-block:: cpp

    ct4l::Connective c {"#", 2};

The class representing propositional signatures, namely :cpp:class:`ct4l::PropSignature`, 
stores a set of pointers to objects of the class :cpp:class:`ct4l::Connective`.

.. note::

    We have chosen pointers instead of plain objects envisaging
    the creation of formulas based on the same signature.
    As each compound formula stores a connective inside it,
    having them as pointers avoids copying the same connective :math:`\#`
    repeatedly for each :math:`\#`-headed formula.

See below an example where we build a usual signature for Classical Logic:

.. code-block:: cpp

    ct4l::PropSignature cl_signature {
        {"and", 2},
        {"or", 2},
        {"not", 1},
        {"top", 0},
        {"bot", 0}
    };

If you want to access some of the connectives, you may just 
use :cpp:func:`ct4l::PropSignature::operator[]()`, which
produces a pointer to the desired connective:

.. code-block:: cpp

    auto and = cl_signature["and"];

.. note::

    If you have more than one connective with the same symbol in the
    signature, :cpp:func:`ct4l::PropSignature::operator[]()`
    gives a pointer to the one with the least arity. 
    If you want to access a connective by its symbol *and*
    arity, use :code:`signature("and", 2)`.
    You can also get the set of pointers to each connective having the given symbol,
    by simply calling :code:`signature("and")`.

We also allow for iterating over the connectives:

.. code-block:: cpp
    
    for (auto connective_ptr : cl_signature) {
        //connective_ptr is a pointer to a connective of the signature
    }

Moreover, you can add connectives to a signature by the following ways:

.. code-block:: cpp

    using namespace ct4l;

    cl_signature.add({"->", 2}); // or
    cl_signature += Connective {"->", 2}; // or
    cl_signature = cl_signature + Connective {"->", 2} + Connective {"xor", 2};

Given two signatures, we can join them using a similar syntax, as the following
example illustrates:

.. code-block:: cpp

    ct4l::PropSignature sigma1 {
        {"+", 2},
        {"~", 1}
    };
    ct4l::PropSignature sigma2 {
        {"*", 2},
        {"-", 1}
    };

    sigma1.join(sigma2); // or
    sigma1 += sigma2; // or
    auto sigma3 = sigma1.add(sigma2); // or
    auto sigma3 = sigma1 + sigma2;

API
---

.. doxygenclass:: ct4l::Connective
    :members:

.. doxygenclass:: ct4l::PropSignature
    :members: