BARS: A Term Rewriting System for Boolean Algebra
BARS: A Term Rewriting System for Boolean Algebra
Anders Lindman, March 7, 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
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
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
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.
BARS Foundation
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.
BARS replaces the variables in the Boolean expressions 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 and (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 values.
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
Variable Substitution
(*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];Echo[expr];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,{x1,y0}];rewrite[init,10]
Out[]=
init=or[xor[and[or[0,0],or[0,1]],1],and[1,1]];ResourceFunction["MultiwayCombinator"][rules,init,10,"StatesGraphStructure"]