Boole's expansion theorem

Boole's expansion theorem   (Redirected from Shannon's expansion theorem) Jump to navigation Jump to search Boole's expansion theorem, often referred to as the Shannon expansion or decomposition, is the identity: {displaystyle F=xcdot F_{x}+x'cdot F_{x'}} , where {displaystyle F} is any Boolean function, {displaystyle x} is a variable, {displaystyle x'} is the complement of {displaystyle x} , and {displaystyle F_{x}} and {displaystyle F_{x'}} are {displaystyle F} with the argument {displaystyle x} set equal to {displaystyle 1} and to {displaystyle 0} respectively.

The terms {displaystyle F_{x}} and {displaystyle F_{x'}} are sometimes called the positive and negative Shannon cofactors, respectively, of {displaystyle F} with respect to {displaystyle x} . These are functions, computed by restrict operator, {displaystyle operatorname {restrict} (F,x,0)} and {displaystyle operatorname {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 (BDDs), satisfiability solvers, and many other techniques relevant to computer engineering and formal verification of digital circuits. In such engineering contexts (especially in BDDs), the expansion is interpreted as a if-then-else, with the variable {displaystyle x} being the condition and the cofactors being the branches ( {displaystyle F_{x}} when {displaystyle x} is true and respectively {displaystyle F_{x'}} when {displaystyle x} is false).[2] Contents 1 Statement of the theorem 2 Variations and implications 3 Properties of cofactors 4 Operations with cofactors 5 History 6 Application to switching circuits 7 References 8 See also 9 External links Statement of the theorem A more explicit way of stating the theorem is: {displaystyle 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: {displaystyle 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): {displaystyle 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 {displaystyle f} . For example for {displaystyle n=2} that would be {displaystyle {begin{aligned}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{aligned}}} Likewise, application of the dual form leads to the Product of Sums (PoS) canonical form (using the distributivity law of {displaystyle +} over {displaystyle cdot } ): {displaystyle {begin{aligned}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{aligned}}} 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 {displaystyle F=H'} then {displaystyle F_{x}=H'_{x}} If {displaystyle F=Gcdot H} then {displaystyle F_{x}=G_{x}cdot H_{x}} If {displaystyle F=G+H} then {displaystyle F_{x}=G_{x}+H_{x}} If {displaystyle F=Goplus H} then {displaystyle F_{x}=G_{x}oplus H_{x}} Characteristics of unate functions: If F is a unate function and... If F is positive unate then {displaystyle F=xcdot F_{x}+F_{x'}} If F is negative unate then {displaystyle 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: {displaystyle {frac {partial F}{partial x}}=F_{x}oplus F_{x'}} Universal quantification: The universal quantification of F is defined as: {displaystyle forall xF=F_{x}cdot F_{x'}} Existential quantification: The existential quantification of F is defined as: {displaystyle exists xF=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),[3] and it was "widely applied by Boole and other nineteenth-century logicians".[4] Claude Shannon mentioned this expansion, among other Boolean identities, in a 1949 paper,[5] 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.[6][4] 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. References ^ Rosenbloom, Paul Charles (1950). The Elements of Mathematical Logic. p. 5. ^ G. D. Hachtel and F. Somezi (1996), Logic Synthesis and Verification Algorithms, p. 234 ^ Boole, George (1854). An Investigation of the Laws of Thought: On which are Founded the Mathematical Theories of Logic and Probabilities. p. 72. ^ Jump up to: a b Brown, Frank Markham (2012) [2003, 1990]. Boolean Reasoning - The Logic of Boolean Equations (reissue of 2nd ed.). Mineola, New York: Dover Publications, Inc. p. 42. ISBN 978-0-486-42785-0. [1] ^ Shannon, Claude (January 1949). "The Synthesis of Two-Terminal Switching Circuits" (PDF). Bell System Technical Journal. 28: 59–98 [62]. doi:10.1002/j.1538-7305.1949.tb03624.x. ISSN 0005-8580. ^ Perkowski, Marek A.; Grygiel, Stanislaw (1995-11-20), "6. Historical Overview of the Research on Decomposition", A Survey of Literature on Function Decomposition, Version IV, Functional Decomposition Group, Department of Electrical Engineering, Portland University, Portland, Oregon, USA, p. 21, CiteSeerX (188 pages) See also Reed–Muller expansion External links Shannon’s Decomposition Example with multiplexers. Optimizing Sequential Cycles Through Shannon Decomposition and Retiming (PDF) Paper on application. Categories: Boolean algebraTheorems in lattice theory

Si quieres conocer otros artículos parecidos a Boole's expansion theorem puedes visitar la categoría Boolean algebra.

Deja una respuesta

Tu dirección de correo electrónico no será publicada.


Utilizamos cookies propias y de terceros para mejorar la experiencia de usuario Más información