Boole's expansion theorem

Boole's expansion theorem, often referred to as the Shannon expansion or decomposition, is the identity: $F = x \cdot F_x + x' \cdot F_x'$ , where $F$ is any Boolean function and $F_x$ and $F_x'$ are $F$ with the argument $x$ equal to $1$ and to $0$ respectively.

The terms $F_x$ and $F_x'$ are sometimes called the positive and negative Shannon cofactors, respectively, of $F$ with respect to $x$ . These are functions, computed by restrict operator, $restrict(F, x, 0)$ and $restrict(F, x, 1)$ (see valuation (logic) and partial application).

It has been called the "fundamental theorem of Boolean algebra".^[1] Besides its theoretical importance, it paved the way for binary decision diagrams, satisfiability solvers, and many other techniques relevant to computer engineering and formal verification of digital circuits.

Statement of the theorem

A more explicit way of stating the theorem is-

f(X_1, X_2, \dots , X_n) = X_1 \cdot f(1, X_2, \dots , X_n) + X_1' \cdot f(0, X_2, \dots , X_n)

Proof for the statement follows from direct use of mathematical induction, from the observation that $f(X_1) = X_1.f(1) + X_1'.f(0)$ and expanding a 2-ary and n-ary Boolean functions identically.

History

George Boole presented this expansion as his Proposition II, "To expand or develop a function involving any number of logical symbols", in his Laws of Thought (1854),^[2] and it was "widely applied by Boole and other nineteenth-century logicians".^[3]

Claude Shannon, noted information-theorist and communications pioneer, mentioned this expansion, among other Boolean identities, in a 1948 paper,^[4] and showed the switching network interpretations of the identity. In the literature of computer design and switching theory, it is often attributed to Shannon.^[3]

Application to switching circuits

Binary decision diagrams follow from systematic use of this theorem
Any Boolean function can be implemented directly in a switching circuit using a hierarchy of basic multiplexer by repeated application of this theorem.

Notes

↑ Paul C. Rosenbloom, The Elements of Mathematical Logic, 1950, p. 5
↑ George Boole, An Investigation of the Laws of Thought: On which are Founded the Mathematical Theories of Logic and Probabilities, 1854, p. 72 full text at Google Books
1 2 Frank Markham Brown, Boolean Reasoning: The Logic of Boolean Equations, 2nd edition, 2003, p. 42
↑ Claude Shannon, "The Synthesis of Two-Terminal Switching Circuits", Bell System Technical Journal 28:59–98, full text, p. 62

External links

Shannon’s Decomposition Example with multiplexers.
Optimizing Sequential Cycles Through Shannon Decomposition and Retiming (PDF) Paper on application.

This article is issued from Wikipedia - version of the Sunday, November 29, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.