Boole's expansion theorem, often referred to as the Shannon expansion or decomposition, is the
identity:
, where
is any
Boolean function
In mathematics, a Boolean function is a function whose arguments and result assume values from a two-element set (usually , or ). Alternative names are switching function, used especially in older computer science literature, and truth function ...
,
is a variable,
is the complement of
, and
and
are
with the argument
set equal to
and to
respectively.
The terms
and
are sometimes called the positive and negative Shannon cofactors, respectively, of
with respect to
. These are functions, computed by restrict operator,
and
(see
valuation (logic) In logic and model theory, a valuation can be:
*In propositional logic, an assignment of truth values to propositional variables, with a corresponding assignment of truth values to all propositional formulas with those variables.
*In first-ord ...
and
partial application
In computer science, partial application (or partial function application) refers to the process of fixing a number of arguments to a function, producing another function of smaller arity. Given a function f \colon (X \times Y \times Z) \to N , ...
).
It has been called the "fundamental theorem of Boolean algebra".
Besides its theoretical importance, it paved the way for
binary decision diagram
In computer science, a binary decision diagram (BDD) or branching program is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed representation of sets or relations. ...
s (BDDs),
satisfiability solvers, and many other techniques relevant to
computer engineering and
formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal met ...
of digital circuits.
In such engineering contexts (especially in BDDs), the expansion is interpreted as a
if-then-else
In computer science, conditionals (that is, conditional statements, conditional expressions and conditional constructs,) are programming language commands for handling decisions. Specifically, conditionals perform different computations or actio ...
, with the variable
being the condition and the cofactors being the branches (
when
is true and respectively
when
is false).
[G. D. Hachtel and F. Somezi (1996), ''Logic Synthesis and Verification Algorithms'', p. 234]
Statement of the theorem
A more explicit way of stating the theorem is:
:
Variations and implications
; XOR-Form : The statement also holds when the
disjunction
In logic, disjunction is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is raining or it is snowing" can be represented in logic using the disjunctive formula R \lor S ...
"+" is replaced by the
XOR operator:
:
; Dual form: There is a dual form of the Shannon expansion (which does not have a related XOR form):
:
Repeated application for each argument leads to the
Sum of Products (SoP) canonical form of the Boolean function
. For example for
that would be
:
Likewise, application of the dual form leads to the
Product of Sums
In Boolean algebra, any Boolean function can be expressed in the canonical disjunctive normal form ( CDNF) or minterm canonical form and its dual canonical conjunctive normal form ( CCNF) or maxterm canonical form. Other canonical forms inclu ...
(PoS) canonical form (using the
distributivity law of
over
):
:
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
then
: If
then
: If
then
: If
then
; Characteristics of unate functions:
: If ''F'' is a
unate function A unate function is a type of boolean function which has monotonic properties.
They have been studied extensively in switching theory.
A function f(x_1,x_2,\ldots,x_n) is said to be positive unate in x_i
if for all possible values of x_j, j\neq i
...
and...
: If ''F'' is positive unate then
: If ''F'' is negative unate then
Operations with cofactors
; Boolean difference:
: The Boolean difference or
Boolean derivative of the function F with respect to the literal x is defined as:
:
; Universal quantification:
: The universal quantification of F is defined as:
:
; Existential quantification:
: The existential quantification of F is defined as:
:
History
George Boole
George Boole (; 2 November 1815 – 8 December 1864) was a largely self-taught English mathematician, philosopher, and logician, most of whose short career was spent as the first professor of mathematics at Queen's College, Cork in ...
presented this expansion as his Proposition II, "To expand or develop a function involving any number of logical symbols", in his ''
Laws of Thought
The laws of thought are fundamental axiomatic rules upon which rational discourse itself is often considered to be based. The formulation and clarification of such rules have a long tradition in the history of philosophy and logic. Generally th ...
'' (1854),
and it was "widely applied by Boole and other nineteenth-century logicians".
Claude Shannon
Claude Elwood Shannon (April 30, 1916 – February 24, 2001) was an American mathematician, electrical engineer, and cryptographer known as a "father of information theory".
As a 21-year-old master's degree student at the Massachusetts Inst ...
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
#
Binary decision diagrams follow from systematic use of this theorem
# Any Boolean function can be implemented directly in a
switching circuit
Switching circuit theory is the mathematical study of the properties of networks of idealized switches. Such networks may be strictly combinational logic, in which their output state is only a function of the present state of their inputs; or may ...
using a hierarchy of basic
multiplexer
In electronics, a multiplexer (or mux; spelled sometimes as multiplexor), also known as a data selector, is a device that selects between several analog or digital input signals and forwards the selected input to a single output line. The sel ...
by repeated application of this theorem.
References
{{Reflist, refs=
[{{cite book , author-first=Paul Charles , author-last=Rosenbloom , author-link=Paul Charles Rosenbloom , title=The Elements of Mathematical Logic , date=1950 , page=5]
[{{cite book , author-first=George , author-last=Boole , author-link=George Boole , title=An Investigation of the Laws of Thought: On which are Founded the Mathematical Theories of Logic and Probabilities , date=1854 , page=72 , url=https://books.google.com/books?id=SWgLVT0otY8C&pg=PA73]
[{{cite book , title=Boolean Reasoning - The Logic of Boolean Equations , author-first=Frank Markham , author-last=Brown , edition=reissue of 2nd , publisher= Dover Publications, Inc. , location=Mineola, New York , date=2012 , orig-year=2003, 1990 , isbn=978-0-486-42785-0 , page=42}]
https://web.archive.org/web/20170416231752/http://www2.fiit.stuba.sk/~kvasnicka/Free%20books/Brown_Boolean%20Reasoning.pdf -->
/ref>
[{{cite journal , author-last=Shannon , author-first=Claude , author-link=Claude Shannon , title=The Synthesis of Two-Terminal Switching Circuits , journal= Bell System Technical Journal , volume=28 , pages=59–98 2, date=January 1949 , doi=10.1002/j.1538-7305.1949.tb03624.x , issn=0005-8580 , url=https://archive.org/download/bstj28-1-59/bstj28-1-59.pdf]
[{{citation , title=A Survey of Literature on Function Decomposition , chapter=6. Historical Overview of the Research on Decomposition , version=Version IV , author-first1=Marek A. , author-last1=Perkowski , author-first2=Stanislaw , author-last2=Grygiel , publisher=Functional Decomposition Group, Department of Electrical Engineering, Portland University, Portland, Oregon, USA , date=1995-11-20 , citeseerx=10.1.1.64.1129 , page=21 (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.
Boolean algebra
Theorems in lattice theory