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

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$.

-
Well of course, how else would you evaluate the function? An expression involving operators and operands is evaluated in an inverted tree like fashion with those substitution rules. –  user18063 Jan 9 '12 at 23:07
User18063: by some sophisticated program, with loops, ifs, etc. Of course rewriting systems are universal, so they can evaluate logical expression anyway, but in my question they are used "directly". –  Mooncer Jan 9 '12 at 23:12

2 Answers

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).

-
Yes I am aware that universality of rewrite systems allow them to evaluate the Boolean function in general, I should make this explicit. My question is about the "direct" use that I described. I think the case you described: $\neg 1 \wedge 0 \rightarrow \neg 0$ will not occur because the order of list of rules matters. So the expression would be evaluated as $0 \wedge 0 \rightarrow 0$. –  Mooncer Jan 10 '12 at 0:37
You should also specify explicitly that the order of rules matters to you. There are many ways to do rewrite systems, and that principle is not followed by all of them. –  Henning Makholm Jan 12 '12 at 0:09

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.

-
I asked about evaluating the function on a machine/computer. The function can be perceived as string of chars. –  Mooncer Jan 10 '12 at 3:29
@Steffen I don't see how in principle it matters whether the expression gets evaluated by hand or on a machine/computer, so long as we strictly adhere to the rules given. –  Doug Spoonwood Jan 10 '12 at 14:08
You write: "you have values for the variables, the function will return a definite value." That is not true. Function needs to be implemented first. I am asking about the implementation. –  Mooncer Jan 10 '12 at 14:42
@Steffen I don't follow. If you consider the function of logical conjunction ^ you can define it as ^: (0, 0)->0, (0, 1)->0, (1, 0)->0, (1, 1)->1. So, if you have some formula such as (a^(b^c)), so long as you have the values for a, b, and c in {0, 1}, the function that (a^(b^c)) represents will return a definite value for the triple (a, b, c). So, why does the function need to get implemented first? –  Doug Spoonwood Jan 10 '12 at 15:45
That is weird if you do not follow. Please understand, that you have a string that defines mathematically the function, but does not implement it as a program that can be run. Are you familiar with C? char * f = "a OR b"; –  Mooncer Jan 12 '12 at 0:09