BARS: A Term Rewriting System for Boolean Algebra

Anders Lindman, March 9, 2023
This notebook presents a term rewriting system for Boolean algebra called BARS (acronym for Boolean Algebra Rewriting System) which uses an initial substitution that replaces variables with constant Boolean values. This initial substitution significantly reduces the complexity of the rewriting sequence for Boolean expressions compared to traditional term rewriting systems.

Term Rewriting Systems

A term rewriting system (TRS) is a formal system used to manipulate symbolic expressions. It consists of a set of rules or equations, which specify how certain terms can be rewritten as other terms. In a TRS, terms are constructed from a set of variables, constants, and function symbols, using operations such as function application and variable substitution. The rules of the system define how these terms can be transformed into other terms, by replacing certain subterms with other terms. A rule in a TRS consists of two terms, called the left-hand side (LHS) and the right-hand side (RHS), separated by an arrow. The rule specifies that whenever the LHS appears in an expression, it can be replaced with the RHS. Multiple rules can be applied in a given expression, leading to a sequence of transformations until no more rules can be applied. Term rewriting systems are used in a variety of fields, including computer science, mathematics, and linguistics. They are often used in the development of programming languages and compilers, and in the study of formal languages and automata theory.
Term rewriting systems have several benefits over other forms of computation, including:
Simplicity: TRS are relatively simple and easy to understand formal systems, which makes them useful for teaching and research purposes.
Modularity: TRS can be decomposed into smaller sub-systems or modules, which can be developed and tested separately. This modularity makes TRS useful for software engineering and program verification.
Formal correctness: TRS can be used to specify and verify the correctness of programs and algorithms. This is particularly useful in safety-critical systems, where errors can have serious consequences.
Expressiveness: TRS can express complex computations and algorithms using a simple and elegant notation. This makes TRS useful in domains such as mathematics, artificial intelligence, and natural language processing.
Automation: TRS can be automated using software tools, which can generate code, check correctness, and perform optimization. This automation reduces the time and effort required for software development and verification.

TRS for parallel computation

Term rewriting systems can be implemented for massively parallel computation in hardware. Term rewriting systems are a form of rule-based computation that can be parallelized. In particular, term rewriting systems can be implemented using techniques such as systolic arrays, which are a type of parallel processing architecture commonly used in hardware implementations.
GPUs can be programmed using parallel programming models such as CUDA (Compute Unified Device Architecture) or OpenCL (Open Computing Language), which allow programmers to write code that can be executed in parallel across the many processing cores of the GPU. Term rewriting systems can be implemented in these parallel programming models, allowing them to take advantage of the massive parallelism offered by GPUs.
Other methods for implementing term rewriting systems for parallel computation include Multi-core CPUs: Modern CPUs typically have multiple processing cores, which can be used for parallel computation. Distributed computing: In addition to parallel computing on a single machine, term rewriting systems can also be implemented for distributed computing, which involves multiple machines working together to solve a problem. Cloud computing: Cloud computing platforms such as Amazon Web Services (AWS) or Google Cloud Platform (GCP) provide access to powerful computing resources, including CPUs, GPUs, and FPGAs, which can be used to implement term rewriting systems.

TRS Properties

There are several properties that are important for term rewriting systems, including:
Normalization: A term rewriting system has the normalization property if every term can be rewritten to a normal form (i.e., a term that cannot be further rewritten).
Strong normalization: A term rewriting system has the strong normalization property if every term has a unique normal form, and every reduction sequence terminates under any reduction strategy.
Completeness: Completeness is a property of a computational system that guarantees that the system can compute all possible results that can be obtained from a given input. Formally, a term rewriting system is said to be complete if, for any given term, there exists a finite sequence of rewrites that leads to every possible normal form of that term.
Termination: A term rewriting system is said to be terminating if there exists no infinite sequence of rewrites starting from any given term. In other words, there is no way to apply the rewriting rules repeatedly and indefinitely without eventually reaching a term that cannot be further rewritten.
Confluence: Confluence is a property of a computational system that guarantees that any two possible ways of computing a given result will always lead to the same final result. Confluence is an important property for several reasons. First, it ensures that the computational system will always produce the same result regardless of the order in which the computations are performed, which is essential for ensuring the correctness of the system. Second, it enables us to reason about the behavior of the system and to prove important properties such as completeness and termination. Finally, it allows us to optimize the system by identifying and eliminating redundant computations.
Church-Rosser property: This property states that if a term can be rewritten in two different ways, then there exists a common descendant term that can be reached by further rewriting. In other words, it ensures that any two parallel reductions can be joined together by further reductions to a common term.
Non-ambiguity : This property ensures that each term has at most one normal form.
Length-reducing property: A term rewriting system has the length-reducing property if every rewrite rule strictly decreases the length of the term (i.e., the number of function symbols and variables used in the term). The length-reducing property is important for ensuring termination and confluence of a term rewriting system.

BARS Foundation

BARS is a Boolean term rewriting system. A Boolean TRS is a type of term rewriting system in which the terms are Boolean expressions (i.e., expressions that evaluate to True or False), and the rules are Boolean equations or inequalities. The Church-Rosser property holds for Boolean TRSs because Boolean expressions have unique normal forms (i.e., a canonical form that is equivalent to the original expression), which can be obtained by applying a standard normalization algorithm such as the Knuth-Bendix algorithm. Since any two reducible Boolean expressions can be reduced to a common normal form, the Church-Rosser property holds for Boolean TRSs. This property is important for ensuring that the evaluation of Boolean expressions is well-defined and unambiguous, which is important in programming and logical reasoning.
The Church-Rosser property provides:
Uniqueness of normal forms: If a TRS has the Church-Rosser property, then any reducible term has a unique normal form. This means that regardless of the order in which rules are applied to reduce a term, the final result will always be the same.
Confluence: The Church-Rosser property states that, for any two reducible terms in a TRS, there exists a common, irreducible term to which both terms can be rewritten. Since the irreducible term is unique (by definition of irreducibility), any two reduction paths from the original terms to the common term must coincide at the irreducible term. Therefore, any two reductions of a term to a common term can be connected by a third reduction, and the TRS is said to be confluent.
Reduction strategies: The Church-Rosser property allows for different reduction strategies to be used in a TRS, which can be useful for optimizing computations or for defining different semantics of a language.
Computability theory: The Church-Rosser property is closely related to the concept of computability, which is a fundamental concept in computer science and mathematics. The Church-Rosser property provides a criterion for deciding whether a given TRS is computable or not.
In general, since many rewriting systems have the Church-Rosser property and other properties mentioned, the main difference compered to traditional TRSs is that BARS uses a substitution procedure on the input expressions and has a specific constraint for the use of variable names that ensures that the system is acyclic, in the sense that all the possibilities of cyclic references within the initial expressions are eliminated.
The way BARS replaces the variables in the Boolean expressions is with constant Boolean values, e.g. (0 And 1) Or (0 And (0 Or 1)), which guarantees that the resulting basic expressions will always be reduced to a single constant Boolean value (either 0 or 1). Basic expression here means a Boolean expression with only constant Boolean values without any variable assignments.
BARS allows acyclic variable assignments in the Boolean expressions for unsubstituted variables. Each variable assignment is left unchanged until the expression is reduced to a form where the variable assignment can be replaced by its assigned value, such as x=(0) or x=(1), which further is reduced to either 0 or 1 (in BARS, 0 represents False and 1 represents True).
BARS also allows variables with assignment to be used in the Boolean expressions. A variable with assignment can be used anywhere in the Boolean expressions repeatedly except for the constraint that the name of the variable with assignment must have less alphanumerical order than the variables in the expression it is assigned to. When a variable with assignment is reduced to its constant Boolean value, all occurrences of that variable in the other expressions are replaced by that constant value. BARS is therefore guaranteed to terminate since all expressions always reduce to either 0 or 1.
The alphanumerical order constraint produces a directed structure of variable names, with the variable name of least alphanumerical order as the root. When the constraint is applied, each variable can only be assigned to variables that come alphanumerically after it. This creates a directed acyclic graph (DAG) of variable assignments, where each node represents a variable and each edge represents a dependency between two variables.
Proof:
Let S be the set of all variable names in the expressions. We can assume that S is a non-empty set, since otherwise there are no variable assignments to consider.
Let s be the variable name in S with the least alphanumerical order. We can assume that s exists and is unique, since S is non-empty and the variable names are assumed to be distinct.
Since only variables with assignment are allowed in the expressions, the variable name with greatest alphanumerical order is assigned to an expression with only constant Boolean value(s).
Consider the directed graph G = (V, E), where V is the set of variable names in S, and E is the set of directed edges between variables, defined as follows:
For each variable v in V, if there exists an expression of the form "v = (w ...)", where w is another variable in V and v has a smaller alphanumerical order than w, then there is a directed edge from v to w in E.
By construction, G is a directed acyclic graph (DAG), since it only contains edges that go from variables with smaller alphanumerical order to variables with larger alphanumerical order. This ensures that there are no cycles in the graph.
The DAG contains a variable with greatest alphanumerical order assigned to an expression with only constant Boolean value(s) which ensures that all expressions are reduced to constant Boolean values.
Q.E.D

Variable Substitution

In traditional rewriting systems and in methods like SK combinators, the expressions often become extremely large even for relativity simple calculations. One of the key concepts behind BARS is that by replacing variables with their constant input values the expressions in the rewriting system quickly reduces to the normal form of just a single Boolean value. Even when the input expression is very large the substitution step is simple and can easily be computationally efficient, even in software.
As an illustration, an input expression containing 100 Boolean variables represents up to 2^100 possible combinations*), compared to BARS doing 100 substitutions after which the expression represents 1 possible combination, namely the constant value of the input expression.
The implementation of BARS starts with the initial substitution where variables are replaced by their constant Boolean values. To illustrate the method of initial substitution, for clarity without using the more compact syntax of BARS bytecode, the general idea is that Boolean input expressions such as `x and y` becomes for example `0 and 1` after the initial substitution. The TRS rules for rewriting are then applied to the input expression until the expression is reduced to a constant Boolean value of 0 or 1. The Boolean operators `and`, `or`, `xor` and `not` are rewritten into constant values step by step until the entire input expression is reduced to its normal form, i.e. in BARS either 0 or 1.
*) When a Boolean expression has only two possible outcomes (True or False), we can say that the expression itself has only two possible combinations. However, in order to determine whether the expression evaluates to True or False, we need to know the truth values of its variables. Since each variable can take on one of two possible truth values, there are multiple combinations of truth values that can result in the expression evaluating to True or False.
Here is a trivial example using the same principle as in BARS:
In[]:=
(*Booleanreplacementrules*)​​rules={not[1]0,not[0]1,​​and[0,0]0,and[0,1]0,and[1,0]0,and[1,1]1,​​or[0,0]0,or[0,1]1,or[1,0]1,or[1,1]1,​​xor[0,0]0,xor[0,1]1,xor[1,0]1,xor[1,1]0};​​(*Functionforsubstitutingvariableswithconstantvalues*)​​substitute[expr_,values_]:=ReplaceAll[expr,values]​​(*Functionforrewritesystem*)​​rewrite[init_,maxIterations_]:=(​​expr=init;​​prevExpr={expr};​​Do[​​expr=ResourceFunction["MultiwayCombinator"][rules"Sequential",expr,1];​​expr=Part[expr,2];​​Print[i];​​Print[expr];​​If[expr=={},Break[]];​​prevExpr=expr,​​{i,maxIterations}];​​StringForm["Final expression: ``",Part[prevExpr,1]])​​(*Testtherewritingsystem*)​​init=and[or[x,x],or[y,x]];​​init=substitute[init,{x1,y0}];​​rewrite[init,100]
1
{and[1, or[0, 1]]}
2
{and[1, 1]}
3
{1}
4
{}
Out[]=
Final expression: 1
The MultiwayCombinator function used in the rewrite[] function is set to "Sequential" which means that it applies the first possible replacement (sequential substitution system). The same result is generated when used in multiway mode:
In[]:=
ResourceFunction["MultiwayCombinator"][rules,init,10,"StatesGraphStructure"]
Out[]=

BARS Specification

Instead of `and`, `or`, `xor` and `not` and spaces, BARS has a more compact syntax with `&`, `|`, `^` and `!` for the Boolean operators where & represents And, | represents Or, ^ represents Xor, and ! represents negation. In addition to the Boolean operators, the BARS bytecode allows parentheses, `0` and `1` for Boolean values, `=` for variable assignment with alphanurerical variable names beginning with a letter, e.g. `variable1`.
Here is the BARS bytecode syntax in BNF form:
<expression> ::= <assignment> | <term> | <term> "&" <term> | <term> "|" <term> | <term> "^" <term>
<term> ::= <boolean> | <not> <term> | "(" <expression> ")"
<boolean> ::= "0" | "1"
<not> ::= "!"
<assignment> ::= <variable> "=" "(" <expression> ")"
<variable> ::= <identifier>
<identifier> ::= <letter> | <identifier> <letter> | <identifier> <digit>
<letter> ::= "A" | "B" | "C" | "D" | "E" | "F" | "G" | "H" | "I" | "J" | "K" | "L" | "M" | "N" | "O" | "P" | "Q" | "R" | "S" | "T" | "U" | "V" | "W" | "X" | "Y" | "Z" | "a" | "b" | "c" | "d" | "e" | "f" | "g" | "h" | "i" | "j" | "k" | "l" | "m" | "n" | "o" | "p" | "q" | "r" | "s" | "t" | "u" | "v" | "w" | "x" | "y" | "z"
<digit> ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
The algorithm for BARS in Structured English is:
ALGORITHM BARS
INPUT initial_boolean_expression, constant_input_values
​
FUNCTION rewrite(expression)
reduce_constant_terms(expression)
  variable_values = replace_finalized_variables(expression)
RETURN variable_values
END FUNCTION
​
expression = replace_unassigned_variables(initial_boolean_expression, constant_input_values)
​
DO UNTIL terminated
finalized_variables = rewrite(expression)
  variables_output = add_finalized_variables(variables_output, finalized_variables)
  IF is_empty(expression)
   terminated = true
  END IF
END DO
​
RETURN variables_output

Implementation

Notice that this implementation is without error checks and that in a more realistic situation there would likely be checks for validating inputs to ensure that they meet the BARS requirements, especially the constraint for variable names which can lead to cyclic references if ignored.
The BARS rewrite function can be implemented like this:
The BARS algorithm can be implemented like this:

Examples

Here is a simple example of running the `bars[]` function for the expression `a | b` with `a = 0` and `b = 1`:
In this next example a variable `x` is assigned to an expression. The value of `x` is returned in the second item in the list and the first item in the list is the result of the expression as a whole.
A full adder is a circuit that can add two binary digits (bits) and a carry input bit, and produces a sum bit and a carry output bit. This is how a full adder can be implemented in BARS:
For adding two 4-bit numbers (nibbles), four full adders can be connected in series where the output carry bit from previous adder goes into the input carry of the next adder (for convenience this example ignores the BARS restriction for assigned variable names since the expression is free from cyclic references):