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 set of 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"];

Note

If you have more than one connective with the same symbol in the signature, 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 signature("and", 2). You can also get the set of pointers to each connective having the given symbol, by simply calling 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, int arity)¶

Constructs a connective from its symbol and its arity.

Parameters

symbol: the connective symbol
arity: 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.

Connectives with same symbol but different arities are accepted.

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

inline PropSignature(const decltype(_connectives) &connectives)¶

Construct a propositional signature from a set of pointers to connectives.

Parameters

connectives: set of pointers to 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 set.

Allows iterating over the connectives.

Return: begin iterator

inline auto end() const¶

End iterator of the underlying set.

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

inline void add(std::shared_ptr<Connective> connective)¶

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

inline PropSignature &operator+=(std::shared_ptr<Connective> connective)¶

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

inline PropSignature operator+(std::shared_ptr<Connective> connective)¶

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

SharedPtrSet<Connective> operator()(const std::string &symbol) const¶

Return a set of pointers to connectives of the signature having the same symbol.

An empty set is returned if no connective with this symbol is present.

Return

a set of pointer to the connective in the signature having the given symbol

Parameters

symbol: the symbol of the connective

std::shared_ptr<Connective> operator()(const std::string &symbol, int arity) const¶

Return a pointer to the connective in the signature by its symbol and arity.

Return

a pointer to the connective in the signature

Parameters

symbol: the symbol of the connective
arity: the arity of the connective

Exceptions

invalid_argument: in case the connective is not present in the signature

std::shared_ptr<Connective> operator[](const std::string &symbol) const¶

Return a pointer to the connective with the least arity in the signature having the given symbol.

Return

a pointer to the connective of the least arity having the given symbol

Parameters

symbol: the symbol to search for

Exceptions

invalid_argument: in case no connective with the symbol is present

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

Signatures¶

Propositional signatures¶

API¶

ct4l-lib

Navigation

Related Topics