Formulas¶

Logics express consecutions involving fundamental linguistic (or syntactical) objects called formulas. The set of all formulas that may be present in consecutions of a given logic is the object-language, or simply the language, of such logic. Currently, ct4l supports only propositional languages, as we describe below.

Propositional languages
- Parsing propositional formulas
- Working with sets of formulas
First-order languages
API

Propositional languages ¶

A propositional language $\mathbf{L}_\Sigma(P)$ over a propositional signature $\Sigma$ is the absolutely free algebra over $\Sigma$ freely generated by the set $P = \{p_i : i \in \omega\}$ of propositional variables. The elements of the carrier $L_\Sigma(P)$ of this algebra are called propositional formulas, commonly denoted by Greek letters (like $\varphi$, $\psi$, $\phi$, $\ldots$).

In ct4l, we have an interface for propositional formulas called ct4l::PropFmla, and two specializations:

ct4l::PropVar represents propositional variables:
ct4l::PropVar p {"p"};
ct4l::PropCompound represents compound formulas, holding a pointer to a $k$-ary connective (a ct4l::Connective object) and a vector of pointers to $k$ ct4l::PropFmla objects.

For example, the formula $p\,\mathsf{and}\,q$ can be constructed in the following way:
using namespace std;
using namespace ct4l;

auto and = make_shared<Connective> {"and", 2};
auto p = make_shared<PropVar> {"p"};
auto q = make_shared<PropVar> {"q"};
PropCompound p_and_q {and, {p, q}};
We recommend, however, to use a parser to build formulas. See Parsing propositional formulas for more details.

On propositional formulas we may perform the basic operations described below.

the set of subformulas of a given formula is given by:
\[\begin{split}\mathsf{subformulas}(\varphi) = \begin{cases} \{\varphi\} & \text{ if } \varphi \in P\\ \{\varphi\} \cup \bigcup_{i=1}^n \mathsf{subformulas}(\varphi_i) & \text{ if } \varphi=\#(\varphi_1,\ldots,\varphi_n)\\ \end{cases}\end{split}\]

Just call:
auto subfmlas = fmla.subformulas();
the set of propositional variables of a given formula is given by the function:
\[\begin{split}\mathsf{props}(\varphi) = \begin{cases} \{\varphi\} & \text{ if } \varphi \in P\\ \bigcup_{i=1}^n \mathsf{props}(\varphi_i) & \text{ if } \varphi=\#(\varphi_1,\ldots,\varphi_n)\\ \end{cases}\end{split}\]

Just call:
auto props = fmla.props();
the complexity of a formula is given by:
\[\begin{split}\mathsf{complexity}(\varphi)= \begin{cases} 0 & \text{ if } \varphi \in P\\ 1 + \sum_{i=1}^n \mathsf{complexity}(\varphi_i) & \text{ if } \varphi=\#(\varphi_1,\ldots,\varphi_n)\\ \end{cases}\end{split}\]

Just call:
auto complexity = fmla.complexity();
we infer the formula signature by (for operations on signatures, check ct4l::PropSignature):
\[\begin{split}\mathsf{signature}(\varphi)= \begin{cases} \mathsf{empty\_signature} & \text{ if } \varphi \in P\\ \sum_{i=1}^n(\mathsf{signature}(\varphi_i)) + \# & \text{ if } \varphi=\#(\varphi_1,\ldots,\varphi_n)\\ \end{cases}\end{split}\]

Just call:
auto signature = fmla.infer_signature();

Parsing propositional formulas ¶

We provide by default the parser ct4l::PropParser for propositional formulas, to produce ct4l::PropFmla instances from strings. Here is how you can parse a formula (see below for a more secure version):

ct4l::PropParser parser;
auto [fmla, msgs] = parser.parse("p and q");

In the code above, the variable msgs holds a list of messages (objects of class ct4l::RowColMessage) possibly produced during the parsing process. Any unexpected character during parsing produces a warning, while incompatibility with the grammar produces errors. We suggest to always check if this list is empty or not. Moreover, unrecoverable errors during parsing results in an exception that should be checked. Here is a code that securely parses a formula:

ct4l::PropParser parser;
try {
    auto [fmla, msgs] = parser.parse("p and q");
    if (msgs.empty()) {
        // secure to use the formula, no errors or warnings
    } else {
        // some warning was produced, maybe check with the user if they want to continue
    }
} catch (ParseException& e) {
    // deal with the error, messages are in e.messages()
}

By default, the parser logs the messages on the screen. You can overwrite this behaviour by passing a callback to the parser constructor that simply ignores the messages:

ct4l::PropParser parser {[](auto m){}};

You can actually give two callbacks to this constructor: the first one is called whenever the lexer produces a message (that is, whenever unexpected characters are produced), and the second one is called whenever a parsing problem occurs. The argument given to each callback is an instance of ct4l::RowColMessage. When you pass only one, it is used for both purposes.

The default parser implements the following grammar, using the Bison tool:

\[\begin{split}\begin{split} \mathsf{digit} &:= [0-9]\\ \mathsf{integer} &:= \{\mathsf{digit}\}+\\ \mathsf{alpha} &:= [\mathrm{a-zA-Z}]\\ \mathsf{symbol} &:= [\#\$ ! @ \% \& < > ?]\\ \mathsf{Id} &:= (\mathsf{alpha}|\mathsf{symbol})(\mathsf{alpha}|\mathsf{digit}|\mathsf{symbol})*\\ \mathsf{NullaryConn} &:= \text{top } \mid \text{ bot}\\ \mathsf{UnaryConn} &:= \text{neg} \mid - \\ \mathsf{BinaryConn} &:= \text{and} \mid \text{or} \mid \text{->} \mid + \mid - \mid * \mid /\\ \mathsf{Fmla} &:= \mathsf{Prop} \mid \mathsf{NullaryComp} \mid \mathsf{UnaryComp} \mid \mathsf{BinaryComp} \mid \mathsf{KAryComp}\\ \mathsf{Prop} &:= \mathsf{Id} \\ \mathsf{NullaryComp} &:= \mathsf{NullaryConn} \mid `\mathsf{Id}`\\ \mathsf{UnaryComp} &:= \mathsf{UnaryConn}\,\mathsf{Fmla} \mid `\mathsf{Id}`\,\mathsf{Fmla}\\ \mathsf{BinaryComp} &:= \mathsf{Fmla}\,\mathsf{BinaryConn}\,\mathsf{Fmla} \mid \mathsf{Fmla}\,`\mathsf{Id}`\,\mathsf{Fmla}\\ \mathsf{KAryComp} &:= \mathsf{Id}([\mathsf{Fmla}[,\mathsf{Fmla}]])\\ \end{split}\end{split}\]

Some examples of strings accepted by this parser (and their corresponding formulas) are:

"p": $p$ (a propositional variable)
"p and q": $p \, \mathsf{and} \, q$ (a binary compound)
"p 'foo' q": $p \, \mathsf{foo} \, q$ ($\mathsf{foo}$ is parsed as a binary connective)
"neg p": a unary compound
"'box' p": a unary compound, with $\mathsf{box}$ parsed as a unary connective
"pt(p, q, r)": a ternary compound, with $\mathsf{pt}$ parsed as a ternary connective
"top": the nullary formula called $\mathsf{top}$
"'botop'": the nullary formula called $\mathsf{botop}$
"p(q) and p": no problem with p being both a connective and a propositional variable

Now, some invalid cases:

"p and": and is binary
"p lor q": lor is not a default binary connective; it should be declared with quotes

Working with sets of formulas ¶

We provide the ct4l::PropFmlaPtrSet type to work with sets of formulas:

using namespace ct4l;

PropParser parser;
auto [f1, m1] = parser.parse("p and q");
auto [f2, m2] = parser.parse("p and r");
PropFmlaPtrSet s {f1, f2};

Note

As ct4l::PropFmla is abstract, sets of formulas here are actually sets of pointers to formulas. The comparator given for the set container uses the strict weak ordering of the underlying concrete formulas.

First-order languages ¶

Future work.

API ¶

class ct4l::PropFmla¶

Represents a propositional formula.

Author: Vitor Greati

Subclassed by ct4l::PropCompound, ct4l::PropVar

Public Functions

virtual PropFmlaPtrSet subformulas() const = 0¶

Compute the subformulas of the propositional formula.

Return: a set of pointers to the subformulas

virtual PropVarPtrSet props() const = 0¶

Compute the set of propositional variables in the propositional formula.

Return: the set of pointers to propositional variables of the formula

virtual int complexity() const = 0¶

The complexity of the formula.

Return: the complexity of the formula

virtual PropSignature infer_signature() const = 0¶

The least signature containing the connectives in the formula.

Return: the least signature containing the connectives in the formula.

virtual void accept(PropFmlaVisitor &visitor) const = 0¶

Accepts a visitor.

Parameters

visitor: a formula visitor

bool operator<(const PropFmla &rhs) const¶

Compare propositional formulas in a strict weak ordering.

Return

if lhs < rhs

Parameters

rhs: rhs

bool operator==(const PropFmla &rhs) const¶

Equality test for propositional formulas.

Return

if lhs == rhs

Parameters

rhs: rhs

inline bool operator!=(const PropFmla &rhs) const¶

Non-equality test for propositional formulas.

Return

if lhs == rhs

Parameters

rhs: rhs

class ct4l::PropVar : public ct4l::PropFmla ¶

Represents a propositional variable.

Author: Vitor Greati

Public Functions

inline PropVar(const std::string &symbol)¶

Build a propositional variable from symbol.

Parameters

symbol: the symbol

inline decltype(_symbol) symbol() const¶

The propositional variable symbol.

Return: the symbol

inline virtual PropFmlaPtrSet subformulas() const override¶

Compute the subformulas of the propositional formula.

Return: a set of pointers to the subformulas

inline virtual PropVarPtrSet props() const override¶

Compute the set of propositional variables in the propositional formula.

Return: the set of pointers to propositional variables of the formula

inline virtual int complexity() const override¶

The complexity of the formula.

Return: the complexity of the formula

inline virtual PropSignature infer_signature() const override¶

The least signature containing the connectives in the formula.

Return: the least signature containing the connectives in the formula.

inline virtual void accept(PropFmlaVisitor &visitor) const override¶

Accepts a visitor.

Parameters

visitor: a formula visitor

inline bool operator<(const PropVar &other) const¶

Compare propositional variables in a strict weak ordering.

Return

if lhs < rhs

Parameters

other: rhs

inline bool operator==(const PropVar &rhs) const¶

Equality test for propositional formulas.

Return

if lhs == rhs

Parameters

rhs: rhs

inline bool operator!=(const PropVar &rhs) const¶

Non-equality test for propositional formulas.

Return

if lhs == rhs

Parameters

rhs: rhs

class ct4l::PropCompound : public ct4l::PropFmla ¶

Represents a propositional compound.

Author: Vitor Greati

Public Functions

PropCompound(decltype(_connective) connective, const decltype(_components) &components)¶

Build a propositional compound.

Parameters

connective: a pointer to a connective
components: list of components of the formula

PropCompound(const Connective &connective, const decltype(_components) &components)¶

Build a propositional compound, passing a concrete connective.

Parameters

connective: a concrete connective
components: list of components of the formula

inline decltype(_connective) connective() const¶

The connective in the head of the compound.

Return: a pointer to the head connective

inline decltype(_components) components() const¶

Get pointers to the component formulas.

Return: the vector of component formulas

virtual PropFmlaPtrSet subformulas() const override¶

Compute the subformulas of the propositional formula.

Return: a set of pointers to the subformulas

virtual PropVarPtrSet props() const override¶

Compute the set of propositional variables in the propositional formula.

Return: the set of pointers to propositional variables of the formula

virtual int complexity() const override¶

The complexity of the formula.

Return: the complexity of the formula

virtual PropSignature infer_signature() const override¶

The least signature containing the connectives in the formula.

Return: the least signature containing the connectives in the formula.

inline virtual void accept(PropFmlaVisitor &visitor) const override¶

Accepts a visitor.

Parameters

visitor: a formula visitor

inline auto begin() const¶

Begin iterator to allow iterating over the components.

Return: begin iterator over the components

inline auto end() const¶

End iterator to allow iterating over the components.

Return: end iterator over the components

inline auto operator[](int i) const¶

Access a component of a given formula (unsafe).

Return

a pointer to the component formula

Parameters

i: the position of the component

bool operator==(const PropCompound &rhs) const¶

Equality test for propositional compounds.

Return

if lhs == rhs

Parameters

rhs: rhs

bool operator<(const PropCompound &rhs) const¶

Strick weak ordering test for propositional compounds.

Return

if lhs < rhs

Parameters

rhs: rhs

inline bool operator!=(const PropCompound &rhs) const¶

Non-equality test for propositional compounds.

Return

if lhs != rhs

Parameters

rhs: rhs

class ct4l::PropFmlaVisitor¶

Visitor of propositional formulas.

Allows to perform operations over the structure of formulas without touching the class hierarchy.

Author: Vitor Greati

Subclassed by ct4l::EqualityPropFmlaVisitor, ct4l::StrictOrderPropFmlaVisitor

Public Functions

virtual void visit(PropVar const &propvar) = 0¶

Visit a propositional formula.

Parameters

propvar: the propositional formula

virtual void visit(PropCompound const &procomp) = 0¶

Visit a propositional compound.

Parameters

procomp: a propositional compound

class ct4l::PropFmlaParserI¶

Interface for propositional formula parsers.

Author: Vitor Greati

Subclassed by ct4l::BisonPropFmlaParser

Public Types

using MessageCallback = std::function<void(RowColMessage)>¶: Alias for a parsing message list.

using ParserMessageList = std::vector<RowColMessage>¶: Parsing result.

Public Functions

virtual ~PropFmlaParserI()¶: Virtual destructor.

PropFmlaParserI()¶: Empty constructor.

PropFmlaParserI(const MessageCallback &lexer_callback, const MessageCallback &parser_callback)¶: Constructor accepting a location and message callbacks.

PropFmlaParserI(const MessageCallback &message_callback)¶: Constructor accepting only message callbacks message callbacks.

virtual ParsingResult parse(const std::string &str) = 0¶

Parse a string into a propositional formula.

Return

a pair containing a pointer to the parsed formula and a list of parsing messages

Parameters

str: the string to be parsed

Exceptions

parse: error if the parsing fails

class ct4l::BisonPropFmlaParser : public ct4l::PropFmlaParserI ¶

Flex/Bison-based parser of propositional formulas.An alias to this parser to ease utilization.

Author: Vitor Greati

Public Functions

BisonPropFmlaParser()¶: Empty constructor.

BisonPropFmlaParser(const MessageCallback &lexer_callback, const MessageCallback &parser_callback)¶: Constructor accepting only message callbacks message callbacks.

BisonPropFmlaParser(const MessageCallback &message_callback)¶: Constructor accepting only message callbacks message callbacks.

virtual PropFmlaParserI::ParsingResult parse(const std::string &str) override¶

Parse a string into a propositional formula.

Return

a pointer to the parsed formula and a list of parsing messages

Parameters

str: the string to be parsed

Exceptions

parse: error if the parsing fails

Formulas¶

Propositional languages ¶

Parsing propositional formulas ¶

Working with sets of formulas ¶

First-order languages ¶

API ¶

ct4l-lib

Navigation

Related Topics

Formulas¶

Propositional languages¶

Parsing propositional formulas¶

Working with sets of formulas¶

First-order languages¶

API¶

Propositional languages ¶

Parsing propositional formulas ¶

Working with sets of formulas ¶

First-order languages ¶

API ¶