Boole's expansion theorem, often referred to as the Shannon expansion or Shannon decomposition, is the identity
F
=
x
⋅
F
x
+
x
′
⋅
F
x
′
{\displaystyle F=x\cdot F_{x}+x'\cdot F_{x'}}
, where
F
{\displaystyle F}
is any Boolean function,
x
{\displaystyle x}
is a variable,
x
′
{\displaystyle x'}
is the complement of
x
{\displaystyle x}
, and
F
x
{\displaystyle F_{x}}
and
F
x
′
{\displaystyle F_{x'}}
are
F
{\displaystyle F}
with the argument
x
{\displaystyle x}
set equal to
1
{\displaystyle 1}
and to
0
{\displaystyle 0}
respectively.
The terms
F
x
{\displaystyle F_{x}}
and
F
x
′
{\displaystyle F_{x'}}
are sometimes called the positive and negative Shannon cofactors, respectively, of
F
{\displaystyle F}
with respect to
x
{\displaystyle x}
. These are functions, computed by the
restrict
{\displaystyle \operatorname {restrict} }
operator,
restrict
(
F
,
x
,
0
)
{\displaystyle \operatorname {restrict} (F,x,0)}
and
restrict
(
F
,
x
,
1
)
{\displaystyle \operatorname {restrict} (F,x,1)}
. (See also valuation and partial application.)
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
{\displaystyle x}
being the condition and the cofactors being the branches (
F
x
{\displaystyle F_{x}}
when
x
{\displaystyle x}
is true and respectively
F
x
′
{\displaystyle F_{x'}}
when
x
{\displaystyle x}
is false).
Contents
Statement of the theorem
A more explicit way of stating the theorem is:
f
(
X
1
,
X
2
,
…
,
X
n
)
=
X
1
⋅
f
(
1
,
X
2
,
…
,
X
n
)
+
X
1
′
⋅
f
(
Variations and implications
XOR-Form
The statement also holds when the disjunction "+" is replaced by the XOR operator:
f
(
X
1
,
X
2
,
…
,
X
n
)
=
X
1
⋅
f
(
1
,
X
2
,
…
,
X
n
)
⊕
X
1
′
⋅
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
′
{\displaystyle F=H'}
then
F
x
=
H
x
′
{\displaystyle F_{x}=H'_{x}}
If
F
=
G
⋅
H
{\displaystyle F=G\cdot H}
then
F
x
=
G
x
⋅
H
x
{\displaystyle F_{x}=G_{x}\cdot H_{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:
∂
F
∂
x
=
F
x
⊕
F
x
′
{\displaystyle {\frac {\partial F}{\partial x}}=F_{x}\oplus F_{x'}}
Universal quantification:
The universal quantification of F is defined as:
∀
x
F
=
F
x
⋅
F
x
′
{\displaystyle \forall xF=F_{x}\cdot F_{x'}}
Existential quantification:
The existential quantification of F is defined as:
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
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.