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 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.

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

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

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