Multi-algebras

Let \(\Sigma\) be a propositional signature. A multi-algebra over \(\Sigma\) is a structure \(\mathbf{V} = \langle V, \cdot^{\mathbf{V}} \rangle\), where \(V\) is a non-empty collection, called the carrier of \(\mathbf{V}\) and, for each connective \(\# \in \Sigma_k\), the mapping \(\#^\mathbf{V}:V^k \to \mathsf{Power}(V)\) is the interpretation of \(\#\) in \(\mathbf{V}\).

In ct4l, we build a finite multi-algebra over a ct4l::PropSignature by constructing an object of the class ct4l::MultiAlgebra using a ct4l::Domain object to represent \(V\) and ct4l::TruthTableI objects to provide the interpretations.

Let us build an example, to be used in the remainder of this document.

Example: Building the two-element Boolean algebra

Let us build the algebra \(\mathbf{B}\) over the signature \(\Sigma\) such that

• \(\Sigma_0 = \{\mathsf{top}, \mathsf{bot}\}\)

• \(\Sigma_1 = \{\mathsf{not}\}\)

• \(\Sigma_2 = \{\mathsf{and}, \mathsf{or}\}\)

• \(\Sigma_k = \varnothing, k > 2\)

with the following interpretations:

\(x\)	\(y\)	\(\mathsf{and}(x,y)\)	\(\mathsf{or}(x,y)\)	\(\mathsf{not}(y)\)	\(\mathsf{top}\)	\(\mathsf{bot}\)
F	F	F	F	T	T	F
F	T	F	T	F
T	F	F	T
T	T	T	T

This algebra can be constructed in ct4l in the following way:

using namespace std;
using namespace ct4l;

// build the domain
auto domain = make_shared<Domain<string>>(vector<string>{"F", "T"});

// build the truth-tables
auto tt_and = make_shared<TruthTable<string>>({domain, 2, {"F"}, {{{"T", "T"}, {"T"}}}});
auto tt_or =  make_shared<TruthTable<string>>({domain, 2, {"T"}, {{{"F", "F"}, {"F"}}}});
auto tt_not = make_shared<TruthTable<string>>({domain, 1, {"T"}, {{{"T"}, {"F"}}}});
auto tt_top = make_shared<TruthTable<string>>({domain, 0, {"F"}});
auto tt_bot = make_shared<TruthTable<string>>({domain, 0, {"T"}});

// build the algebra
MultiAlgebra<string> algebra {
    domain,
    {
        {{"and", 2}, tt_and},
        {{"or",  2}, tt_or},
        {{"not", 1}, tt_not},
        {{"top", 0}, tt_top},
        {{"bot", 0}, tt_bot},
    }
};

Accessing the algebra operations

We provide two ways to access the algebra operations:

• by passing the symbol (if there are more than one connective with that symbol, gives the one with the least arity):

  auto tt_and_ptr = algebra["and"];
  

• by passing the connective, useful when you have connectives with the same symbol:

  auto tt_and_ptr = algebra[Connective{"and", 2}];
  

• by iterating:

  for (auto& [connective, truth_table_ptr] : algebra) {
      ...
  }
  

Adding interpretations

Use the ct4l::MultiAlgebra::interpret() to interpret a new connective in a given algebra (modifying its signature):

auto tt_botop = make_shared<TruthTable<string>>({domain, 0, {"T", "F"}});
algebra.interpret("botop", tt_botop);

API

template<typename T>
class ct4l::MultiAlgebra

Represents a multi-algebra: an structure containing a signature, a domain and an interpretation to each symbol of the signature.

Author

Vitor Greati

Public Functions

MultiAlgebra(decltype(_signature) signature, decltype(_domain) domain, const decltype(_interpretation) &interpretation)

Constructor taking a domain, a signature and an interpretation.

Parameters

• domain: a pointer to the domain of the algebra

• signature: o pointer to the signature

• interpretation: the interpretation for each signature symbol

MultiAlgebra(decltype(_domain) domain, const decltype(_interpretation) &interpretation)

Constructor that infers a signature from the interpretations.

Parameters

• domain: a pointer to the domain of the algebra

• interpretation: the interpretation for each signature symbol

inline decltype(_domain) domain() const

A pointer to the algebra domain.

Return

a pointer to the algebra domain

inline decltype(_signature) signature() const

A pointer to the algebra signature.

Return

a pointer to the algebra signature

inline decltype(_interpretation) interpretation() const

A pointer to the algebra interpretation.

Return

a pointer to the algebra signature

void interpret(const Connective &connective, std::shared_ptr<TruthTableI<T>> interpretation_func)

Set the interpretation of a symbol.

If the symbol is not present, add it to the signature and interpret.

Parameters

• symbol: the symbol

• interpretation_func: the interpretation function

const std::shared_ptr<TruthTableI<T>> &operator[](const Connective &connective) const

Access an interpretation by the connective, using [].

Return

a pointer to the interpretation of the symbol in the algebra

Parameters

• connective: the connective

const std::shared_ptr<TruthTableI<T>> &operator[](const std::string &symbol) const

Access the interpretation of the connective having the given symbol.

If there are more than one connective with this symbol, return the one with the least arity.

Return

a poiter to the interpretation

Parameters

• symbol: the connective symbol

inline auto begin() const

Gives the begin iterator of the interpretation.

Return

the begin iterator of the interpretation.

inline auto end() const

Gives the end iterator of the interpretation.

Return

the end iterator of the interpretation.