Can Boolean function's value be computed by using a rewrite system?

Question

Suppose there is a function in e.g. CNF form. For example:

$$ (A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E) $$

For given A,B,C,D,E values it is possible to compute the value of the function with rewriting system (like Markov algorithm), correct? The rules would be:

$\neg 1 \rightarrow 0 $
$\neg 0 \rightarrow 1$
$1 \wedge 1 \rightarrow 1$
$1 \wedge 0 \rightarrow 0$
$\ldots$
$0 \vee 0 \rightarrow 0$
$\ldots$
$(0) \rightarrow 0$
$(1) \rightarrow 1$

At the end, there should be only single char: 0 or 1. Is this correct? I was trying to find confirmation in google but without success.

The above rules could also include the initial variable—to—input-value substitution rules, like e.g. $A \rightarrow 1$.

Answer 1

Not quite in this way -- you would need to have a fully parenthesized form. Otherwise you could get, for example, the reduction $\neg 1\land 0 \;\to\; \neg 0 \;\to\; 1$ if the rewriter happens to reduce the conjunction first. (I'm assuming that you're considering string rewriting systems rather than tree rewriting on abstract syntax trees; the latter case is too easy to be much interesting here).

On the other hand, rewriting systems are powerful enough that you can implement an parser for infix expressions as rewrite rules (for example, converting to Polish or reverse Polish form using Dijkstra's railroad algorithm) as a first step, and then apply straightforward rules like the ones you present to evaluate the Polish notation. In order to keep things sane you'd want to use different symbols each operator in infix, Polish and stack-intermediate forms, of course.

So in this sense rewrite systems can indeed evaluate Boolean functions.

(More generally, it is easy to see that you can simulate arbitrary Turing machines using rewrite rules, so they can compute literally everything that is computable in the first place).

Answer 2

First off, a CNF (or DNF for that matter) consists of a formula, or in other terms a "well-formed formula" or "statement form", by definition. So, the expression comes as unambiguous, and thus if you have values for the variables, the function will return a definite value. In fact, the very definition of a function means that if you all the variable(s) get assigned value(s), the function will take those value(s) and return a single output. When someone indicates something like (A∨B)∧(¬B∨C∨¬D)∧(D∨¬E) as a CNF they probably mean it as an abbreviation for a fully parenthesized form (it doesn't much matter if we left-associate or right-associate ^ and V here, since those CNFs come as equivalent), or they don't quite understand the definition of a CNF.

Now, that said I think you mean to ask if an expression which you can identify as a conjunction, looking like an abbreviation for a conjunctive normal form, will necessarily come as unambiguous, or equivalently evaluate to 0 or 1. Or in other terms if such an expression will necessarily also express a function. Well, consider

(A v ¬A) ^ (B V C ^ D) ^ (C v ¬C).

Say we have B->1, C->0, D->0. Well, then ((B v C) ^ D)->((1 v 0) ^ 0)->(1^0)->0, while (1 v (0 ^ 0))->(1 v 0)->1. It follows that even though we can tell that (A v ¬A) ^ (B V C ^ D) ^ (C v ¬C) should indicate a conjunction, it simply won't come as unambiguous, or equivalently evaluate to 0 or 1. In infix notation you either need everything fully parenthesized, some form of interpretation (which an algorithm basically doesn't allow for), some rules for order of operations (and you'll need such rules to cover all possible operations), or you've gotten lucky.