Richard Suchenwirth 2005-04-12 - Boolean functions, in which arguments and result are in the domain {true, false}, or {1, 0} as expr has it, and operators are e.g. {AND, OR, NOT} resp. {&&, ||, !}, can be represented by their truth table, which for example for {$a && $b} looks like:
a b a&&b 0 0 0 1 0 0 0 1 0 1 1 1
As all but the last column just enumerate all possible combinations of the arguments, first column least-significant, the full representation of a&&b is the last column, a sequence of 0s and 1s which can be seen as binary integer, reading from bottom up: 1 0 0 0 == 8. So 8 is the associated integer of a&&b, but not only of this - we get the same integer for !(!a || !b), but then again, these functions are equivalent.
To try this in Tcl, here's a truth table generator that I borrowed from a little proving engine, but without the lsort used there - the order of cases delivered makes best sense when the first bit is least significant:
proc truthtable n { # make a list of 2**n lists, each with n truth values 0|1 set res {} for {set i 0} {$i < (1<<$n)} {incr i} { set case {} for {set j 0} {$j <$n} {incr j } { lappend case [expr {($i & (1<<$j)) != 0}] } lappend res $case } set res }
Now we can write n(f), which, given a Boolean function of one or more arguments, returns its characteristic number, by iterating over all cases in the truth table, and setting a bit where appropriate:
proc n(f) expression { set vars [lsort -unique [regsub -all {[^a-zA-Z]} $expression " "]] set res 0 set bit 1 foreach case [truthtable [llength $vars]] { foreach $vars $case break set res [expr $res | ((($expression)!=0)*$bit)] incr bit $bit ;#-- <<1, or *2 } set res }
Experimenting:
% n(f) {$a && !$a} ;#-- contradiction is always false 0 % n(f) {$a || !$a} ;#-- tautology is always true 3 % n(f) {$a} ;#-- identity is boring 2 % n(f) {!$a} ;#-- NOT 1 % n(f) {$a && $b} ;#-- AND 8 % n(f) {$a || $b} ;#-- OR 14 % n(f) {!($a && $b)} ;#-- de Morgan's laws: 7 % n(f) {!$a || !$b} ;#-- same value = equivalent 7
So the characteristic integer is not the same as the Goedel number of a function, which would encode the structure of operators used there.
% n(f) {!($a || $b)} ;#-- interesting: same as unary NOT 1 % n(f) {!$a && !$b} 1
Getting more daring, let's try a distributive law:
% n(f) {$p && ($q || $r)} 168 % n(f) {($p && $q) || ($p && $r)} 168
Daring more: what if we postulate the equivalence?
% n(f) {(($p && $q) || ($p && $r)) == ($p && ($q || $r))} 255
Without proof, I just claim that every function of n arguments whose characteristic integer is 2^(2^n) - 1 is a tautology (or a true statement - all bits are 1). Conversely, postulating non-equivalence turns out to be false in all cases, hence a contradiction:
% n(f) {(($p && $q) || ($p && $r)) != ($p && ($q || $r))} 0
So again, we have a little proving engine, and simpler than last time.
In the opposite direction, we can call a Boolean function by its number and provide one or more arguments - if we give more than the function can make sense of, non-false excess arguments lead to constant falsity, as the integer can be considered zero-extended:
proc f(n) {n args} { set row 0 set bit 1 foreach arg $args { set row [expr {$row | ($arg != 0)*$bit}] incr bit $bit } expr !!($n &(1<<$row)) }
Trying again, starting at OR (14):
% f(n) 14 0 0 0 % f(n) 14 0 1 1 % f(n) 14 1 0 1 % f(n) 14 1 1 1
So f(n) 14 indeed behaves like the OR function - little surprise, as its truth table (the results of the four calls), read bottom-up, 1110, is decimal 14 (8 + 4 + 2). Another test, inequality:
% n(f) {$a != $b} 6 % f(n) 6 0 0 0 % f(n) 6 0 1 1 % f(n) 6 1 0 1 % f(n) 6 1 1 0
Trying to call 14 (OR) with more than two args:
% f(n) 14 0 0 1 0 % f(n) 14 0 1 1 0 53 % f(n) 14 1 1 1 0
The constant 0 result is a subtle indication that we did something wrong :)
Implication (if a then b, a -> b) can in expr be expressed as $a <= $b - just note that the "arrow" seems to point the wrong way. Let's try to prove "Modus Barbara" - "if a implies b and b implies c, then a implies c":
% n(f) {(($a <= $b) && ($b <= $c)) <= ($a <= $c)} 255
With less abstract variable names, one might as well write
% n(f) {(($Socrates <= $human) && ($human <= $mortal)) <= ($Socrates <= $mortal)} 255
But this has been verified long ago, by Socrates' death :^)
Lars H: A remark concerning the use of the word "proof" above. Strictly speaking, the above doesn't prove any implications; it verifies that the given formula is a tautology (evaluates to true for any assignment of true/false to its variables). While from one point of view these things are the same -- a formula is a theorem of standard propositional logic if and only if it is a tautology -- they are also quite different, because "proof" is a concept that has meaning only in relation to a particular theory, whereas "tautology" is defined with respect to a particular model. It is possible to deduce from the fact that a formula is a tautology that there is a proof of it, but that deduction relies on a result in the metatheory of propositional logic.
More formally, a proof in a theory T is defined to be a sequence of formulae where each formula is (i) a premise, (ii) an axiom of the theory T, or (iii) a formula that follows (using one of the rules of inference of T) from some previous formulae in the proof. If there is a proof in the theory under consideration that ends with B and has premises A1,...,An, then one writes A1,...,An|-B (this |- is really a \u22A2). A formula B is a theorem in a theory if |-B, i.e., if there is a proof of it without any additional assumptions.
CL applauds Lars' exposition of the distinction between model and theory.
The way back from an integer to a logical expression is shown on Disjunctive Normal Form.
See also Parsing Polish notation - A little proving engine - NAND - Boolean Functions and Cellular Automata