Skip to content
Surf Wiki
Save to docs
general/boolean-algebra

From Surf Wiki (app.surf) — the open knowledge base

Boole's expansion theorem

Theorem in Boolean algebra


Theorem in Boolean algebra

Boole's expansion theorem, often referred to as the Shannon expansion or Shannon decomposition, is the identity F = x \cdot F_x + x' \cdot F_{x'}, where F is any Boolean function, x is a variable, x' is the complement of x, and F_xand F_{x'} are F with the argument x set 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 the \operatorname{restrict} operator, \operatorname{restrict}(F, x, 0) and \operatorname{restrict}(F, x, 1).

The theorem has been called the "fundamental theorem of Boolean algebra". Besides its theoretical importance, it paved the way for binary decision diagrams (BDDs), satisfiability solvers, and many other techniques relevant to computer engineering and formal verification of digital circuits. In such contexts, particularly in BDDs, the expansion is interpreted as an if-then-else, with the variable x being the condition and the cofactors being the branches (F_x when x is true and respectively F_{x'} when x is false).

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)

Variations and implications

; XOR-Form : The statement also holds when the disjunction "+" is replaced by the XOR operator: : f(X_1, X_2, \dots , X_n) = X_1 \cdot f(1, X_2, \dots , X_n) \oplus X_1' \cdot f(0, X_2, \dots , X_n) ; Dual form: There is a dual form of the Shannon expansion (which does not have a related XOR form): : f(X_1, X_2, \dots , X_n) = (X_1 + f(0, X_2, \dots , X_n)) \cdot (X_1' + f(1, X_2, \dots , X_n))

Repeated application for each argument leads to the Sum of Products (SoP) canonical form of the Boolean function f. For example for n=2 that would be

:\begin{align} f(X_1, X_2) & = X_1 \cdot f(1, X_2) + X_1' \cdot f(0, X_2)\ & = X_1 X_2 \cdot f(1, 1) + X_1 X_2' \cdot f(1, 0) + X_1' X_2 \cdot f(0, 1) + X_1' X_2' \cdot f(0, 0) \end{align}

Likewise, application of the dual form leads to the Product of Sums (PoS) canonical form (using the distributivity law of + over \cdot):

:\begin{align} f(X_1, X_2) & = (X_1 + f(0, X_2)) \cdot (X_1' + f(1, X_2))\ & = (X_1 + X_2 + f(0, 0)) \cdot (X_1 + X_2' + f(0, 1)) \cdot (X_1' + X_2 + f(1, 0)) \cdot (X_1' + X_2' + f(1, 1)) \end{align}

Properties of cofactors

; Linear properties of cofactors: : For a Boolean function F which is made up of two Boolean functions G and H the following are true: : If F = H' then F_x = H'x : If F = G \cdot H then F_x = G_x \cdot H_x : If F = G + H then F_x = G_x + H_x : If F = G \oplus H then F_x = G_x \oplus H_x ; Characteristics of unate functions: : If F is a unate function and... : If F is positive unate then F = x \cdot F_x + F{x'} : If F is negative unate then F = F_x + x' \cdot F_{x'}

Operations with cofactors

; Boolean difference: : The Boolean difference or Boolean derivative of the function F with respect to the literal x is defined as: : \frac{\partial F}{\partial x} = F_x \oplus F_{x'} ; Universal quantification: : The universal quantification of F is defined as: : \forall x F = F_x \cdot F_{x'} ; Existential quantification: : The existential quantification of F is defined as: : \exists x F = F_x + F_{x'}

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), and it was "widely applied by Boole and other nineteenth-century logicians".

Claude Shannon mentioned this expansion, among other Boolean identities, in a 1949 paper, and showed the switching network interpretations of the identity. In the literature of computer design and switching theory, the identity is often incorrectly attributed to Shannon.

Application to switching circuits

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

References

References

  1. G. D. Hachtel and F. Somenzi (1996), ''Logic Synthesis and Verification Algorithms'', p. 234
  2. (1950). "The Elements of Mathematical Logic".
  3. (1854). "An Investigation of the Laws of Thought: On which are Founded the Mathematical Theories of Logic and Probabilities".
  4. (2012). "Boolean Reasoning - The Logic of Boolean Equations". [[Dover Publications, Inc.]].
  5. (January 1949). "The Synthesis of Two-Terminal Switching Circuits". [[Bell System Technical Journal]].
  6. (1995-11-20). "A Survey of Literature on Function Decomposition". Functional Decomposition Group, Department of Electrical Engineering, Portland University, Portland, Oregon, USA.
Info: Wikipedia Source

This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page.

Want to explore this topic further?

Ask Mako anything about Boole's expansion theorem — get instant answers, deeper analysis, and related topics.

Research with Mako

Free with your Surf account

Content sourced from Wikipedia, available under CC BY-SA 4.0.

This content may have been generated or modified by AI. CloudSurf Software LLC is not responsible for the accuracy, completeness, or reliability of AI-generated content. Always verify important information from primary sources.

Report