Part 5: Design and implementation of the to_string method

In this section, we design and implement a method to transform a WFF back to a string. The string will have correct UTF-8 characters for the logical connectives. This is a very simple example to highlight the simplicity and usefulness of textX models.

There are two main approaches to implement a method that returns a string:

Recursive approach: The method calls itself multiple times, from different objects, until the string is built. Simplicity and conciseness are the main reasons to use this approach, but it can also lead to a stack overflow due to excessively deep recursion.
Iterative approach: Use a loop to traverse the AST and build the string. This method also needs a stack to keep track of the nodes but is less likely to overflow and often performs better than the recursive approach.

A recursive approach may be more elegant and simple to implement, so we choose this approach.

Recursive approach

We will recursively create the string representation of each wff in a WFF object at instantiation and will store the string in a formula attribute. Storing the string avoids regenerating it each time at the price of memory usage. We can then simply override the __str__ method to return the formula attribute.

Here’s a refresher on how to design a recursive algorithm:

Identify the base case: The case that will stop the recursion and prevent it from infinitely calling itself.
Identify the recursive case: Break the problem into smaller subproblems and call the function to recursively solve them.
Combine the results: Combine the results of the recursive calls to solve the original problem.

Step 1: Identify the base case

The recursion will stop with the leaf nodes of the AST. The leaf node will always be of type Atom, which stores the propositional variable name in the id attribute.

class Atom(WFF):
    def __init__(self, parent: Any, id: Variable):
        self.parent = parent
        self.id = id
        self.formula = id

Step 2: Identify the recursive case

The connectives, however, will keep recursing until they reach a leaf node. In contrast to the unary connective Negation, the binary connective will call the __str__ method on both the left-hand and right-hand side wffs.

Step 3: Combine the results

The substrings are combined using either string concatenation or formatting methods. Here we will use F-strings also called formatted string literals.

To improve the aesthetics of the string representation, we use UTF-8 characters representing logical connectives. The symbols can be found on the following Wikipedia page.

class Negation(WFF):
    def __init__(self, parent: Any, wff: WFF):
        self.parent = parent
        self.wff = wff
        self.formula = f"¬{self.wff}"
        

class Conjunction(WFF):
    def __init__(self, parent: Any, lhs: WFF, rhs: WFF):
        self.parent = parent
        self.lhs = lhs
        self.rhs = rhs
        self.formula = f"({self.lhs} ∧ {self.rhs})"


class Disjunction(WFF):
    def __init__(self, parent: Any, lhs: WFF, rhs: WFF):
        self.parent = parent
        self.lhs = lhs
        self.rhs = rhs
        self.formula = f"({self.lhs} ∨ {self.rhs})"


class Implication(WFF):
    def __init__(self, parent: Any, lhs: WFF, rhs: WFF):
        self.parent = parent
        self.lhs = lhs
        self.rhs = rhs
        self.formula = f"({self.lhs} → {self.rhs})"


class Equivalence(WFF):
    def __init__(self, parent: Any, lhs: WFF, rhs: WFF):
        self.parent = parent
        self.lhs = lhs
        self.rhs = rhs
        self.formula = f"({self.lhs} ↔ {self.rhs})"

Finally, we override the __str__ method to return the formula attribute.

# ... previous code

type Formula = str

class WFF(ABC):
    formula: Formula = ""

    def __str__(self) -> Formula:
        return self.formula

Part 6 is a bonus section for those interested in learning about precedence rules and an iterative approach to building the string representation.