CDM Boole s World 1 Algebra of Circuits Klaus Sutner Carnegie Mellon University Boolean Algebras Fall 2018 Proofs A Design Challenge 3 No Feedback 4 H

Size: px

Start display at page:

Download "CDM Boole s World 1 Algebra of Circuits Klaus Sutner Carnegie Mellon University Boolean Algebras Fall 2018 Proofs A Design Challenge 3 No Feedback 4 H"

怒郦
5 years ago
Views:

CDM Boole s World 1 Algebra of Circuits Klaus Sutner Carnegie Mellon University Boolean Algebras Fall 2018 Proofs A Design Challenge 3 No Feedback 4 How does one build complicated digital circuits?

1 CDM Boole s World 1 Algebra of Circuits Klaus Sutner Carnegie Mellon University Boolean Algebras Fall 2018 Proofs A Design Challenge 3 No Feedback 4 How does one build complicated digital circuits? Back to basics: consider only feedback-free circuits. Half Adder x c y s 2-bit Adder This one has feedback, and is a bit too messy for our purposes. x y c c HA s HA c s s c A Definition 5 And Algebra? 6 More precisely, we can formally define these circuits as follows: We have an acyclic digraph G = V, E that has several nodes of in-degree 0 (input nodes) and nodes of out-degree 0 (output nodes). The underlying ugraph is connected. The internal nodes of G are labeled by Boolean operators and, or and not. The indegree (here usually referred to as fan-in) of these nodes has to be appropriate. One can limit the fan-in to 2 for and and or nodes, or allow unlimited fan-in. Negation requires fan-in 1. The combinatorial definition of a circuit is not particularly helpful when it comes to building one, or to optimize the design. Question: Can one use algebra to describe a circuit? In our circuits, there are two physical states (such as high/low voltage) can be interpreted as representing a binary choice, 0 or 1, truth values. We need to understand the natural algebra of these objects.

Translation to Propositional Logic 7 Claude Shannon 8 Using standard propositional logic, we can express the half adder like so: c = x y s = c (x y) = x y Note that equality here really corresponds

2 Translation to Propositional Logic 7 Claude Shannon 8 Using standard propositional logic, we can express the half adder like so: c = x y s = c (x y) = x y Note that equality here really corresponds to logical equivalence. This representation turns out to be quite useful for hand-computations. The connection between electronic circuits and logic (in the guise of Boolean algebras) was first clearly recognized by Shannon in Boolean Functions 9 Zero or One Inputs 10 To model circuits we use the two-element Boolean algebra B = {ff, tt}. For the sake of readability we often use 0 for false, and 1 for true. Definition A Boolean function is a map of the form B n B where n 0. What kind of Boolean functions are there for small values of n? Case n = 0: 2 functions All we get is 2 constant functions 0 and 1. Note that we only consider single outputs here rather than f : B n B f : B n B m There is no problem with this, we can always use vectors of Boolean functions if multiple outputs are needed. Case n = 1: 4 functions 2 constants, plus H id = x, the identity, and H not(x) = 1 x, negation. Incidentally, the latter two are reversible. Binary Boolean Functions 11 Circuits as Boolean Functions 12 Case n = 2 much more interesting: 16 functions. Some correspond to the typical gates used in circuits. x y H and(x, y) H or(x, y) H imp(x, y) x y H equ(x, y) H xor(x, y) H nand(x, y) We can think of circuits as compositions of Boolean functions. In fact, there is a clone hiding here. For the half-adder from above we have: and c = H and(x, y) s = H and(h not(h and(x, y)), H or(x, y)) This may not look particularly impressive, but the important point is that we are one step away from a purely algebraic interpretation. We will see later that all Boolean functions can be constructed from these.

3 Changing Notation 13 Building a 2-bit Adder 14 Yes, notation helps. We write + for H or, for H and, and x for H not. But then a digital circuit is just a term t T (+,, ) of a particular Boolean algebra where the inputs correspond to the free variables. We are interested in smaller/simpler terms t such that t = t and we can use the machinery of Boolean algebra to establish such equalities. We can use truth tables to construct an actual circuit. Here inputs are x, y and z and the outputs are s (sum) and c (carry). The table describes the functionality of the circuit. x y z s c From the table we can read off immediately that s = x yz + xyz + xy z + xyz c = xyz + xyz + xyz + xyz Simplify 15 These expressions are mildly complicated, but we can simplify them considerably using equational reasoning in Boolean algebra. To simplify, let u = xy + xy = (x + y) xy Algebra of Circuits then s = uz + uz c = uz + xy 2 Boolean Algebras Not too bad. u is essentially the half-adder from above, and the last two formulae represent the 2-bit adder. Note that this simplification process would be rather difficult using circuit diagrams! Proofs History 17 George Boole ( ) 18 Boolean algebra dates back to work by George Boole in the middle of the 19th century. Other early contributions were made by William S. Jevons Augustus de Morgan Charles S. Pierce Ernst Schröder And Marshall Stone Alfred Tarski created the modern theory in the 1930s.

4 G. Boole 19 Laws of Boolean Algebra 20 The design of the following treatise is to investigate the fundamental laws of the operations of the mind by which reasoning is performed; to give expression to them in the symbolical language of a calculus, and to open this foundation to establish the science of logic and construct its method The Mathematical Analysis of Logic 1854 An Investigation of the Laws of Thought A Boolean algebra is a structure B = B,,,, 0, 1 and signature (2, 2, 1, 0, 0) where the following system of equations (BA) is valid: x (y z) = (x y) z x (y z) = (x y) z x y = y x x y = y x x 0 = x x 1 = x x (y z) = (x y) (x z) x (y z) = (x y) (x z) x x = 1 x x = 0 Here is a modern axiomatization. So we have two commutative monoids that coexist peacefully via distributivity, plus a complementation operation. Here is called join, is called meet, is called complement. Digression: Boole s Early Approach 21 Note that some of laws of Boolean algebra are intuitively easy to grasp, in particular the ones that coexist peacefully with ordinary arithmetic. Alas, the logical laws that clash with the laws of numbers are far more problematic and take much effort to get used to. It may come as a relief to you that even G. Boole had problems with his very own algebra. For example, here is an argument he proposed that has some major problems: assuming F (x) = 0, show that F (0)F (1) = 0. The first step is to use what is now often and inaccurately called Shannon expansion to argue A little rearrangement then yields F (x) = F (1)x + F (0)(1 x) = 0 (F (1) F (0))x + F (0) = 0 Then we can conclude and hence x = Substituting into x(1 x) = 0 we get and the claim follows. Discuss the merits of this argument. F (0) F (0) F (1) F (1) 1 x = F (0) F (1) F (0)F (1) 0 = (F (0) F (1)) 2 Two Standard Models 23 Two More Models 24 The trivial one-point model is useless, it is important to check if there are interesting models. Here are two standard models for (BA). Truth values The Boolean values true and false together with disjunction, conjunction and negation: B = {ff, tt},,,, ff, tt Power sets The power set of any set, together with union, intersection and complement: P(A),,,,, A Verify that these structures are indeed Boolean algebras. Divisor Lattices For any positive natural number n let Div(n) be the set of all divisors of n. Then Div(n), lcm, gcd, n/x, 1, n is a Boolean algebra provided that n is square-free. Finite/cofinite Sets Let P (A) be the set of all subsets of A that are either finite or cofinite (the complement is finite). P (N),,,,, N Show that the divisor lattice is a Boolean algebra if, and only if, n is square-free. Do these structures look familiar?

5 Duality 25 Duality Principle 26 There is a remarkable symmetry between the axioms: interchanging and, as well as 0 and 1, takes the identities on the left-hand side to the right, and conversely. Definition Given a term t(x 1,..., x n) over a Boolean algebra, its dual t is defined as t(x 1,..., x n). The term t(x 1,..., x n) is sometimes called the counterdual. Typical example, using de Morgan s law (see below): As noted, for any axiom s = t, there is another axiom ŝ = t. This has the following pleasant consequence: If an identity s = t is provable from the axioms, then so is ŝ = t. So we get two for the price of one. x y = x y = x y Self-Duality 27 Alternative I: Partial Orders 28 Note that we can associate a partial order with every Boolean algebra: Note that a term may well be self-dual: applying the duality operations takes the term to an equivalent one. For example, the threshold function at least two out of three is self-dual: (x y) (x z) (y z) x y x y = y Alternatively, x y x y = x. In the standard two-element algebra B this corresponds just to the usual order ff < tt. For P(A) we have x y x y. Show that a self-dual term must have an odd number of variables. Conversely, if the poset is properly behaved, we can define binary operations inf(x, y) = max ( z A z x, y ) sup(x, y) = min ( z A x, y z ) and obtain a Boolean algebra. Alternative II: Boolean Rings 29 Power Sets 30 A commutative ring R = A,,, 0, 1 is called a Boolean ring if it has chararacteristic 2 and is idempotent: x x = 0 x x = x Note that Z/(2) is a Boolean ring. Given a Boolean ring, we can obtain a Boolean algebra, and conversely: x y = x y x y x y = (x y) (x y) x y = x y x = x 1 x y = x y For example, the Boolean algebra P(A) can be interpreted as a Boolean ring via P(A) = A 2 where addition and multiplication on these functions are defined pointwise, using modular arithmetic on 2. So, for most practical intents and purposes, these two interpretations are the same.

6 Notation 31 Sheffer Stroke 32 To make notation slightly more manageable, one often uses standard ring notation also for Boolean algebra (and typically writes x y as xy). Using three basic operations in a Boolean algebra is very convenient, but not really necessary: we could get away with a single binary operation that corresponds intuitively to rejection (nand): x y is short for x y. Note that this operation is not associative. We can recover the standard operations like so: x + (y + z) = (x + y) + z x (y z) = (x y) z x + y = y + x x y = y x x + 0 = x x 1 = x x + (y z) = (x + y) (x + z) x (y + z) = (x y) + (x z) x + x = 1 x x = 0 For hand-calculations this turns out to be the better notation system. x y = (x x) (y y) x y = (x y) (x y) x = x x Figure out what the axioms for should be. Then discuss nor, x y = x y. Other Operations 33 Atoms 34 A number of other defined operations are of interest: Arbitrary Boolean algebras are rather complicated objects, but in the finite case it is easy to give a complete description. Let B = B, +,,, 0, 1 be a Boolean algebra. x y = xy x y = (x y) + (y x) x y = x + y x y = xy + xy Thus x y is the dual of y x, and x y is the dual of x y. Definition (Atoms) An element a B is an atom if a 0 but x a implies x = 0 or x = a. A Boolean algebra is atomic if whenever x y there is an atom a x but a y. A Boolean algebra is atomless if it has no atoms. For example, in P(A) the atoms are the singletons {a}. Hasse Diagram 35 Finite Boolean Algebras Lemma Every finite Boolean algebra is atomic. Proof. Since x = xy + xy it follows from x y that xy 0. If xy is an atom we are done. Otherwise let a be such that 0 < a < xy. If a is an atom we are done. Otherwise we repeat finding 0 < a < a and so on. The process must terminate since the algebra is finite. 1 As a consequence, for every 0 b B there exists an atom a such that a b. The atoms for the divisor lattice of 30 (which is isomorphic to P([3])).

7 Characterization 37 Representing Boolean Algebras 38 It is easy to push this argument a little to show that in any finite Boolean algebra we have One might hope that the last theorem also takes care of arbitrary Boolean algebras, but there are problems. b = { a b a atom } Theorem Every finite Boolean algebra B is isomorphic to a powerset. Proof. Let A be the set of all atoms in B. It is straightforward to check that B is isomorphic to P(A). A Boolean algebra is complete if, in the corresponding partial order, every subset has an infimum and a supremum. Every atomic complete Boolean is isomorphic to a power set. Alas, in general things become much more complicated and one needs to consider subalgebras of the full power set: needs topology to produce good characterizations. B P(A) closed under the operations union, intersection and complement. These algebras are called fields of sets. Using ultrafilters, one can show that in essence there are no other Boolean algebras. Theorem (Stone Representation Theorem, 1936) Up to isomorphism, every Boolean algebra is a field of sets. Digression: Topology 39 Atomless Boolean Algebras 40 Fields of sets are perhaps the most natural way to obtain a Boolean algebra, but one can also exploit topology to construct Boolean algebras on B P(A) using somewhat more complicated operations. Write x for the complement of the closure of x A. An open set x is regular if x = x. Then we can define Boolean operations on the regular sets: x y = (x y) x y = x y x = x To see that the argument for the finite case collapses in the infinite case, note that there are atomless Boolean algebras. Call A N periodic if a A a + p A for some p 1. So A = A 0 + pn where A 0 {0, 1,..., p 1}. Note that complementation does not change the period, and the union of A and B produces a period at most lcm(p, q). Hence the collection of all periodic subsets of N forms a Boolean algebra. But if A then B = A 0 + 2pN lies strictly between and A: the algebra is atomless. How about ultimately periodic sets? Other Properties 42 Algebra of Circuits Boolean Algebras (BA) has many interesting semantic consequences. Some particularly important ones are: x + x = x x + x y = x x x = x x (x + y) = x x + 1 = 1 x 0 = 0 x + y = x y x = x x y = x + y 3 Proofs It is easy to see that these all hold in the models above, but the point is that they hold in all models of (BA). But showing that turns out to be harder than you might think. Verify that these equations hold in the two standard models.

8 Proofs? 43 Sample Proofs 44 So how do we go about proving that the Boolean laws have these other equations as consequences? We have to rely on reasoning about equations. For example, if we know that s = t and t = u hold in a structure, then we can conclude that s = u also holds. Likewise, we are allowed to substitute arbitrary terms for variables, very much in the way we dealt with associativity above. The crucial point is that all our manipulations must preserve syntactic consequence. We ll make this more precise in a minute, first some examples. Claim (BA) = x + x = x Proof. x + x = (x + x) 1 = (x + x) (x + x) = x + x x = x + 0 = x Note that the third step uses distributivity of plus over times in the opposite direction. By duality, we also have xx = x. More Proofs 45 Freshman s Dream 46 Claim (BA) = 1 + x = 1 Proof. 1 + x = (x + x) + x = (x + x) + x = x + x = 1 The arguments just given are perfectly correct and really not very complicated but most humans do not like this kind of reasoning: replacing simple expressions by more complex ones is counterintuitive. Question: Could we automate these arguments? Claim (BA) = x + xy = x Proof. x + xy = x (1 + y) = x 1 = x More precisely, could we build a theorem prover that, given the axioms, would generate these consequences? Or, at least, could we build a proof assistant that, given an alleged argument, will check correctness and maybe fill in a few steps here and there? Example: Associativity 47 Associativity Everywhere 48 A binary operation is associative if it satisfies (x y) z = x (y z) This is usually explained more casually by saying parens don t matter : it does not matter where we place the parentheses in an expression involving only : the final result of an evaluation is always the same. We could essentially flatten out any expression to x 1 x 2 x 3... x n Associative operations abound in algebra, addition and multiplication of various kinds of numbers (naturals, integers, rationals, reals, complexes) or matrices are always associative. Typical associative operations in CS are concatenation of words and join of lists. The usual counterexample is exponentiation: 2 32 (2 3 ) 2. Pairing operations when implemented by some kind of record data structure also fail to be associative: a, b, c is usually not the same as a, b, c (though they are in some sense equivalent ; this is one of the tips of the misery-of-set-theory iceberg).

9 Proof? 49 An Equational Proof 50 So how do we get from the equation to the assertion parens don t matter? (x y) z = x (y z) At first glance, this associativity axiom may seem to be rather weak, it only handles expressions with two occurrences of the operation. But how about, say, ((a b) c) d versus a (b (c d)) The last two expressions are in fact equal by associativity. Exactly how does this follow? More importantly, can we generate such a proof automatically? Here is a proof that uses only the associativity assumption and some equational reasoning. We need to determine which terms have to be assigned to the variables in the axiom to get the desired effect. ((a b) c) d (a b) (c d) a (b (c d)) a b/x, c/y, d/z a/x, b/y, c d/z Here a b/x means: substitute a b for x and so on. Hence the application of the given associativity equation requires some sort of pattern matching: we have to determine how to bind the variables to terms. Moving Parens Around 51 A Proof 52 Emboldened by first success, let s try something more ambitious. Claim Associativity implies that left associated multiplication is the same as right associated multiplication: Proof. (... (x 1 x 2)... x n 1) x n = x 1 (x 2 (... (x n 1 x n)...) Note that this is really not just one claim but infinitely many: one for each value of n 0; there will induction somewhere. First we establish a little auxiliary result: we can pull out the first term in the left associated product: We prove (... ((a x 1) x 2)... x n 1) x n = a ((... (x 1 x 2)... x n 1) x n) by induction on n. n = 0 is easy, so assume the claim holds for n 1 0. ((... ((a x 1) x 2)... x n 1) x n = by induction hypothesis (a (... (x 1 x 2)... x n 1)) x n = by associativity a ((... (x 1 x 2)... x n 1) x n) (... ((a x 1) x 2)... x n 1) x n = a ((... (x 1 x 2)... x n 1) x n) Main Argument 53 Some Comments on the Proof 54 Case n = 3 is just the associativity axiom. So assume we have the claim for n 3. Then by auxiliary claim by IH (... ((a x 1) x 2)... x n 1) x n = a ((... (x 1 x 2)... x n 1) x n) = a (x 1 (x 2 (... (x n 1 x n)...)) It is important to note that each single one of the formulae ϕ n : (... (x 1 x 2)... x n 1) x n = x 1 (x 2 (... (x n 1 x n)...) can be proven from the associativity axiom, using a separate proof for each n. We are not currently interested in a proof of a much more powerful statement such as n ϕ n, this would require a much stronger logical system. And don t even think about forming an infinite conjunction infinitary logics are very complicated. ϕ 0 ϕ 1 ϕ 2... ϕ n...

10 A Challenge 55 Frivolous Picture 1 56 So we have proven that the associativity axiom has the consequence (... (x 1 x 2)... x n 1) x n = x 1 (x 2 (... (x n 1 x n)...) Of course, this is just one way to parenthesize these expressions, a more ambitious project would be to show that a similar equation can be established for all possible parenthesizations. Which brings up the question what exactly is meant by all possible parenthesizations. A good model is the parse tree of an expression: internal nodes denote on occurrence of and the leaves are labeled by the arguments: if we read off the frontier of the tree from left to right we get x 1, x 2,..., x n. Note that these trees are full binary trees. We need to show that the associativity axiom, when construed as an equation on full binary trees, allows us to transform all full binary trees with n leaves into one another. Frivolous Picture 2 57 A Non-Theorem 58 Here is a formula that can not be derived from associativity: x y = y x Operations that satisfy this property are called commutative or Abelian. Note that in order to show that this formula is not derivable from the associativity axiom it is enough to find just one structure in which associativity holds but this formula is false: the single counterexample shows that ϕ is not a semantic consequence of the associativity axiom, and so it cannot be derivable either. Non-commutative associative operations are plentiful: take all words over a two-letter alphabet, say, {a, b}, with concatenation. Clearly ab ba so commutativity fails. Matrix multiplication is another classical example. An Equational Argument 59 And Beyond 60 Commutativity may follow from other properties, though. Recall that a group is Boolean if it satisfies x 2 = 1 We claim that every Boolean group is also Abelian. To show: ab = ba. equation justification 1 abab = 1 substitute ab/x in (B) 2 aabab = a L a, simplify (1) (B) 3 bab = a substitute a/x in (B), simplify (2) 4 babb = ab R b, simplify (3) 5 ba = ab substitute b/x in (B), simplify (4) Proving identities from (BA) is important, but note that we often are interested in more complicated assertions such as: Lemma x + y = 1 and xy = 0 implies x = y. Lemma x (x + y = x) implies y = 0. How does one prove these assertions?

11 Decidability 61 Who Cares? 62 Discussions of Boolean algebras in general often lead right into the swamp of set theory, Stone s theorem notwithstanding. It is therefore not clear whether the Entscheidungsproblem for Boolean algebras is solvable. Theorem (A. Tarski 1940) The first-order theory of Boolean algebra is decidable. This is in sharp contrast to formalizations of (small fragments of) arithmetic. Equational reasoning in the context of an axiomatic system has become the gold standard in some areas of mathematics, in particular in algebra. More generally, Bourbaki s work shows clearly that describing mathematical structures in terms of well-chosen axioms is an excellent way to guarantee rigor and precision. In the future, the set-theoretic approach embraced by Bourbaki may ultimately give way to a more categoric/type-theoretic approach, but that will argue even more strongly in favor of equational reasoning.

CDM [2ex]Boole's World

CDM [2ex]Boole's World CDM Boole s World Klaus Sutner Carnegie Mellon University Fall 2018 1 Algebra of Circuits Boolean Algebras Proofs A Design Challenge 3 How does one build complicated digital circuits? This one has feedback,