Part 2: Building the truth table

Types and Helper function

Type aliases

To enhance code readability, we can utilize type aliases, which help simplify complex type signatures. Since Python 3.12, we can declare type aliases using the type statement. We’ll leverage this new feature to improve the clarity of our code.

Below are the type aliases we will be using:

type TruthValue = bool # Added to parser file
type Row = List[TruthValue]
type Valuation = Dict[Variable, TruthValue]
type Evaluation = OrderedDict[Formula, TruthValue]

Note: Some type aliases (i.e. Variable and Formula) have been defined in the parser module.

Tree traversal helper

We are going to make use of the post-order tree traversal introduced in the bonus part of the previous subproject. For your convenience, here it is again.

def build_traversal_post_order(wff: WFF)-> List[WFF]:
    traversal = []
    stack = []
    lastVisited = None
    while len(stack) > 0 or wff != None:
        if wff != None:
            stack.append(wff)
            wff = match_case_next(wff)
        else:
            peeked = stack[-1]
            if match_case_not_visited(peeked, lastVisited):
                wff = match_case_next(peeked, left_direction=False)
            else:
                traversal.append(peeked)
                lastVisited = stack.pop()
    return traversal

Variables and valuations

Given the AST traversal, it is straightforward to obtain the variables. We iterate over the wffs and push them to a list when two conditions are met. The first condition checks if the current wff is an atom, and the second checks for duplicated variables. Consequently, after the iterations, we added to our list each variable exactly once.

def find_variables(traversal: List[WFF]) -> List[Variable]:
    variables: List[Variable] = []
    for wff in traversal:
        if (not is_connective(wff)) and (wff.id not in variables):
            variables.append(wff.id)  
    return variables

def is_connective(wff: WFF) -> bool:
    return wff.__class__.__name__ != Atom.__name__

With the variables, we can generate each valuation. An approach to generate each combination of truth values is to take the Cartesian product of $n$ sets of truth values, where $n$ is the number of variables. Then for each combination, we assign the values to each variable. In other words, each valuation is a different mapping from variables to truth values.

def generate_valuations(variables: List[Variable]) -> List[Valuation]:
    cartesian_product = itertools.product([False, True], repeat=len(variables))
    return [dict(zip(variables, values)) for values in cartesian_product]

Subformulas and evaluations

Simple wffs evaluation

To simplify the evaluation logic, we create an evaluate method for each WFF. Each evaluate method implementation follows the rules defined by propositional logic. It is important to note that evaluate is a static method and does not use the classes’s attributes to return a value, but instead receives truth values as parameters.

For completeness, the Atom class’s evaluate method will be implemented, even though it is not necessary. The method takes no parameter and returns nothing (or None in Python).

class Atom(WFF):
    # ... other methods

    @staticmethod
    def evaluate() -> None:
        return None

Please note that we have omitted the __init__ method for the sake of brevity.

Evaluation of the logical connectives is straightforward and only requires boolean operators. The evaluate method for Negation takes one parameter, and returns the negation of its parameter (using the not operator).

class Negation(WFF):
    # ... other methods

    @staticmethod
    def evaluate(value: TruthValue) -> TruthValue:
        return not value

For Disjunction, Conjunction, Implication and Equivalence classes each evaluate method takes 2 parameters. Evaluating a disjunction can be done with the or operator. Likewise, for conjunction we use the and operator. The implication evaluation requires negating its first parameter and then taking the disjunction of the parameters. Finally, the evaluation of equivalence can be achieved with the equality operator ==.

class Disjunction(WFF):
    # ... other methods

    @staticmethod
    def evaluate(lhs: TruthValue, rhs: TruthValue) -> TruthValue:
        return lhs or rhs


class Conjunction(WFF):
    # ... other methods

    @staticmethod
    def evaluate(lhs: TruthValue, rhs: TruthValue) -> TruthValue:
        return lhs and rhs


class Implication(WFF):
    # ... other methods

    @staticmethod
    def evaluate(lhs: TruthValue, rhs: TruthValue) -> TruthValue:
        return (not lhs) or rhs


class Equivalence(WFF):
    # ... other methods

    @staticmethod
    def evaluate(lhs: TruthValue, rhs: TruthValue) -> TruthValue:
        return lhs == rhs

To summarize, we implemented a static evaluate method for each WFF subclass. Each method can be implemented in terms of boolean operators. Furthermore, the evaluate methods may take a different number of parameters. Those methods will simplify the process of iteratively evaluating each subformula of a wff.

Subformulas evaluations

Evaluating a subformula can be done iteratively. We start with a given valuation and a post-order traversal of the formula. Each wff in the traversal is visited. If the visited wff is an Atom, its truth value with respect to the valuation is added to a stack. We keep track of the truth values to use them as parameters for evaluating the connectives. When wff is not an Atom, it is considered as a subformula, hence it is evaluated with parameters removed from the stack. Then we create a mapping from the wff string representations and its associated truth value with respect to the valuation. The resulting truth value is also added to the stack as it serves as a parameter for the next evaluation.

The number of parameters for an evaluate method can be different depending on the WFF. An Atom takes no parameter, a Negation takes one parameter, and binary connectives take two parameters. Fortunately, we can count the parameters at runtime using the signature function and pop the needed number of truth values to be used in the evaluation. The order of truth values must be reversed, because they are removed in reverse order and the order of values affects the evaluation of theImplication connective.

def evaluate_subformulas(traversal: List[WFF], valuation: Valuation) -> Evaluation:
    stack: List[TruthValue] = []
    evaluation: Evaluation = OrderedDict()
    for wff in traversal:
        params: List[WFF] = reversed([stack.pop() for _ in signature(wff.evaluate).parameters])  
        value: TruthValue = wff.evaluate(*params)  
        if value != None:
            stack.append(value) 
            evaluation[str(wff)] = stack[-1]
        else:
            stack.append(valuation[wff.id])  
    return evaluation

Truth table

There are several ways to represent a truth table. One simple approach is to define it as a tuple of components, such as (variables, valuations, subformulas, evaluations), or more succinctly as (header, rows). However, this tuple structure lacks clarity regarding its contents and intended use. To enhance comprehension and usability, a more explicit solution is to define a TruthTable class that encapsulates the concept of a truth table.

Below we define a TruthTable class that takes a header and rows at instantiation time. Additionally, we can implement validation checks to ensure that the lengths of the header and rows are consistent.

@dataclass(frozen=True)
class TruthTable:
    header: List[Formula]
    rows: List[Row]

    def __post_init__(self) -> None:
        header_length = len(self.header)
        for row in self.rows:
            if len(row) != header_length:
                raise ValueError("Row length must be equal to header length.")

Finally, we can combine the previous functions and build a truth table. First, we build a traversal and use it to find the variables. Then we generate valuations from the variables. After that, we can evaluate the subformulas for each valuation and the traversal. The table header is obtained by appending the subformulas to the variables. For that, we need to use the valuations and evaluations keys. Similarly, each row can be obtained by appending the valuation and evaluation values.

def build_table(wff: WFF) -> TruthTable:
    traversal = build_traversal_post_order(wff)
    variables = find_variables(traversal)
    valuations = generate_valuations(variables)
    evaluations = [
        evaluate_subformulas(traversal, valuation) for valuation in valuations
    ]
    header = list(valuations[0].keys()) + list(evaluations[0].keys())
    rows = [
        list(valuations[i].values()) + list(evaluations[i].values())
        for i in range(len(evaluations))
    ]
    return TruthTable(header, rows)

By now you should have learned several techniques. How to find specific objects in a tree data structure, how to generate data such as valuations, how to evaluate simple and compound formulas with an iterative approach and finally, how to combine them to achieve our goal.

In part 2, we will design and implement a truth table visualizer. This will allow us to show the truth table in a console or a web browser.