Signatures¶
Propositional signatures¶
A propositional signature is a family \(\Sigma=\{\Sigma_k\}_{k\in\omega}\) such that each \(\Sigma_k\) is a collection of \(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 \(\#\) of arity \(2\) (or binary):
ct4l::Connective c {"#", 2};
The class representing propositional signatures, namely ct4l::PropSignature
,
stores a mapping between symbols and pointers to objects of the 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 \(\#\) repeatedly for each \(\#\)headed formula.
See below an example where we build a usual signature for Classical Logic:
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 ct4l::PropSignature::operator[]()
, which
produces a pointer to the desired connective:
auto and = cl_signature["and"];
We also allow for iterating over the connectives:
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:
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:
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¶

class
ct4l
::
Connective
¶ Represents a propositional connective, with a symbol and an arity.
 Author
Vitor Greati
Public Functions

inline
Connective
()¶ Empty constructor, which builds a nullary connective with “#” as default symbol.

inline
Connective
(const decltype(_symbol) &symbol, const decltype(_arity) arity)¶ Constructs a connective from its symbol and its arity.
 Parameters
symbol
: the connective symbolarity
: the connective arity
 Exceptions
invalid_argument
: in case a negative arity is given

inline decltype(_symbol)
symbol
() const¶ Get symbol.
 Return
the symbol of the connective

inline decltype(_arity)
arity
() const¶ Get connective arity.
 Return
the arity of the connective

inline bool
operator==
(const Connective &other) const¶ Equality occurs with respect to the symbol and the arity.
 Return
if the present connective is equal to the given one
 Parameters
other
: the other connective

inline bool
operator<
(const Connective &other) const¶ Less than operator.
 Return
if the present connective is less than the given one
 Parameters
other
: the other connective

inline bool
operator!=
(const Connective &other) const¶ Not equal operator.
 Return
if the present connective is not equal w.r.t. another
 Parameters
other
: the other connective

class
ct4l
::
PropSignature
¶ Represents a propositional signature.
It is assumed that two connectives must differ by their symbols.
 Author
Vitor Greati
Public Functions

inline
PropSignature
()¶ Empty constructor, which produces an empty signature.

PropSignature
(const std::initializer_list<Connective> &connectives)¶ Construct a propositional signature from a list of connectives.
Stores the connectives as pointers.
 Parameters
connectives
: list of connectives

PropSignature
operator()
(const int &arity) const¶ Produce the subsignature with connectives of the given arity.
 Return
the subsignature with connectives of the given arity
 Parameters
arity
: arity of the connectives to be collected

inline auto
begin
() const¶ Begin iterator of the underlying map.
Allows iterating over the connectives.
 Return
begin iterator

inline auto
end
() const¶ End iterator of the underlying map.
Allows iterating over the connectives.
 Return
end iterator

inline bool
is_empty
() const¶ Indicates whether the signature is empty.
 Return
whether the signature is empty

inline void
add
(const Connective &connective)¶ Add a connective to the signature inplace.
Replace if a connective with the same symbol already exists.
 Parameters
connective
: the connective to be added
Add a connective to the signature specified by a pointer.
Replace if a connective with the same symbol already exists.
 Parameters
connective
: the connective pointer to be added

inline PropSignature &
operator+=
(const Connective &connective)¶ Add a connective to the signature inplace.
Syntax sugar for add(const Connective&).
Replace if a connective with the same symbol already exists.
 Parameters
connective
: the connective to be added
Add a connective to the signature specified by a pointer.
Replace if a connective with the same symbol already exists. Syntax sugar for add(std::shared_ptr<Connective>).
 Parameters
connective
: the connective pointer to be added

inline PropSignature
operator+
(const Connective &connective)¶ Add a connective to the signature producing a new signature.
Replace if a connective with the same symbol already exists.
 Parameters
connective
: the connective to be added
Add a connective specified by a pointer to the signature, producing a new signature.
Replace if a connective with the same symbol already exists.
 Parameters
connective
: the connective to be added

void
join
(const PropSignature &other)¶ Add to the current signature (inplace) the connectives of another signature.
In case of repeated elements, keeps the elements already present in the signature (in the lhs).
 Parameters
other
: the other signature

inline PropSignature &
operator+=
(const PropSignature &other)¶ Add to the current signature the connectives of another signature.
Syntax sugar for join(const PropSignature&).
 Return
a reference to modified signature
 Parameters
other
: the other signature

PropSignature
operator+
(const PropSignature &other) const¶ Produce a new signature by adding other two.
 Return
the joined signature
 Parameters
other
: the other signature

inline auto
size
() const¶ Return the amount of connectives in the signature.
 Return
number of connectives in the signature

std::shared_ptr<Connective>
operator[]
(const std::string &symbol) const¶ Return a pointer to the connective in the signature by its symbol.
 Return
a pointer to the connective in the signature
 Parameters
symbol
: the symbol of the connective
 Exceptions
invalid_argument
: in case the connective is not present in the signature

bool
operator==
(const PropSignature &other) const¶ Compare two signatures for equality.
 Return
if both signatures are the same
 Parameters
other
: rhs

inline bool
operator!=
(const PropSignature &other) const¶ Compare two signatures for inequality.
 Return
if both signatures are the same
 Parameters
other
: rhs