Теорема о разложении Буля

Разложение Шеннона , часто называют расширением Шеннона или разложения , является тождество : , где любая булева функция , переменная, является дополнением , а и являются с аргументом устанавливается равным и соответственно.${\displaystyle F=x\cdot F_{x}+x'\cdot F_{x'}}$${\displaystyle F}$${\displaystyle x}$${\displaystyle x'}$${\displaystyle x}$${\displaystyle F_{x}}$${\displaystyle F_{x'}}$${\displaystyle F}$${\displaystyle x}$${\displaystyle 1}$${\displaystyle 0}$

Члены и иногда называют положительным и отрицательным кофакторами Шеннона соответственно по отношению к . Это функции, вычисляемые оператором ограничения и (см. Оценку (логику) и частичное применение ).${\displaystyle F_{x}}$${\displaystyle F_{x'}}$${\displaystyle F}$${\displaystyle x}$${\displaystyle \operatorname {restrict} (F,x,0)}$${\displaystyle \operatorname {restrict} (F,x,1)}$

Ее назвали «основной теоремой булевой алгебры». ^[1] Помимо своей теоретической важности, он проложил путь для диаграмм двоичных решений (BDD), решателей выполнимости и многих других методов, относящихся к компьютерной инженерии и формальной верификации цифровых схем. В таких технических контекстах (особенно в BBD) расширение интерпретируется как if-then-else , где переменная является условием, а кофакторы - ветвями ( когда истинно, а когда ложно). ^[2]${\displaystyle x}$${\displaystyle F_{x}}$${\displaystyle x}$${\displaystyle F_{x'}}$${\displaystyle x}$

Формулировка теоремы [ править ]

Более явный способ формулировки теоремы:

${\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})}$

Варианты и последствия [ править ]

XOR-форма

Утверждение также выполняется, когда дизъюнкция «+» заменяется оператором XOR :

${\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})}$

Двойная форма

Существует двойная форма расширения Шеннона (которая не имеет связанной формы XOR):

${\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}))}$

Повторное применение для каждого аргумента приводит к канонической форме суммы произведений (SoP) логической функции . Например, для этого будет${\displaystyle f}$${\displaystyle n=2}$

${\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}}}$

Кроме того, применение двойных форм приводят к продукту из сумм (Pos) каноническая форма ( с использованием дистрибутивностью закона о Овере ):${\displaystyle +}$${\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}}}$

Свойства кофакторов [ править ]

Линейные свойства кофакторов:

Для булевой функции F, состоящей из двух булевых функций G и H , верно следующее:

Если тогда${\displaystyle F=H'}$${\displaystyle F_{x}=H'_{x}}$

Если тогда${\displaystyle F=G\cdot H}$${\displaystyle F_{x}=G_{x}\cdot H_{x}}$

Если тогда${\displaystyle F=G+H}$${\displaystyle F_{x}=G_{x}+H_{x}}$

Если тогда${\displaystyle F=G\oplus H}$${\displaystyle F_{x}=G_{x}\oplus H_{x}}$

Характеристики unate-функций:

Если F - функция unate и ...

Если F положительный unate, то${\displaystyle F=x\cdot F_{x}+F_{x'}}$

Если F отрицательное unate, то${\displaystyle F=F_{x}+x'\cdot F_{x'}}$

Операции с кофакторами [ править ]

Логическая разница:

Логическая разность или логическая производная функции F относительно литерала x определяется как:

${\displaystyle {\frac {\partial F}{\partial x}}=F_{x}\oplus F_{x'}}$

Универсальная количественная оценка:

Универсальная количественная оценка F определяется как:

${\displaystyle \forall xF=F_{x}\cdot F_{x'}}$

Экзистенциальная количественная оценка:

Экзистенциальная количественная оценка F определяется как:

${\displaystyle \exists xF=F_{x}+F_{x'}}$

История [ править ]

Джордж Буль представил это расширение как свое Предложение II «Расширять или развивать функцию, включающую любое количество логических символов» в своих Законах мысли (1854 г.) ^[3], и оно «широко применялось Булем и другими людьми XIX века. логики ». ^[4]

Клод Шеннон упомянул это расширение среди других булевых тождеств в статье 1949 года ^[5] и показал интерпретации тождества коммутационной сети. В литературе по компьютерному дизайну и теории переключений личность часто ошибочно приписывается Шеннону. ^{[6] [4]}

Применение к коммутационным схемам [ править ]

1. Диаграммы двоичных решений следуют из систематического использования этой теоремы.
2. Любая логическая функция может быть реализована непосредственно в схеме переключения с использованием иерархии базового мультиплексора путем повторного применения этой теоремы.

Ссылки [ править ]

См. Также [ править ]

• Разложение Рида – Мюллера

Внешние ссылки [ править ]

• Пример разложения Шеннона с мультиплексорами.
• Оптимизация последовательных циклов с помощью декомпозиции Шеннона и повторной синхронизации (PDF) Документ по применению.