if 0 {[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 } if 0 {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 } if 0 {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)) } if 0 {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 with 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 which ends with B and has premises A1,...,An, then one writes A1,...,An|-B (this |- is really a \x22A2). A formula B is a ''theorem'' in a theory if |-B, i.e., if there is a proof of it without any additional assumptions. ---- See also [Parsing Polish notation] - [A little proving engine] - [NAND] - [Boolean Functions and Cellular Automata] ---- [Arts and crafts of Tcl-Tk programming] [Category Mathematics] }