Теорема Буля о расширении

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

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

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

Формулировка теоремы

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

$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 :

$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):

$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) булевой функции. $f$. Например для $n=2$ это было бы

${\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) (с использованием дистрибутивности закона $+$ над $\cdot$):

${\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, справедливы следующие условия:

Если $F=H'$ затем $F_{x}=H'_{x}$

Если $F=G\cdot H$ затем $F_{x}=G_{x}\cdot H_{x}$

Если $F=G+H$ затем $F_{x}=G_{x}+H_{x}$

Если $F=G\oplus H$ затем $F_{x}=G_{x}\oplus H_{x}$

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

Если F — неопределенная функция и...

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

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

Операции с кофакторами

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

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

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

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

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

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

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

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

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

История

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

Клод Шеннон упомянул это расширение среди других булевых тождеств в статье 1949 года: и продемонстрировал интерпретацию идентичности коммутационной сетью. В литературе по компьютерному дизайну и теории переключения Шеннон часто ошибочно приписывают это имя.

Применение в коммутационных цепях

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

См. также

• Расширение Рида – Мюллера

Внешние ссылки

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