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

Теорема о разложении Буля , часто называемая разложением или разложением Шеннона , представляет собой тождество : , где — любая булева функция , — переменная, — дополнение , а и — это аргументы, равные и соответственно. ${\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), решателей выполнимости и многих других методов, имеющих отношение к компьютерной инженерии и формальной проверке цифровых схем. В таких инженерных контекстах (особенно в BDD) расширение интерпретируется как 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}}$

Характеристики унифицированных функций:

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

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

Если F отрицательный унат, то ${\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] и оно «широко применялось Булем и другими логиками девятнадцатого века». ^[4]

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

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

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

Ссылки

1. Розенблум, Пол Чарльз (1950). Элементы математической логики . стр. 5.
2. GD Hachtel и F. Somenzi (1996), Логический синтез и алгоритмы проверки , стр. 234
3. Буль, Джордж (1854). Исследование законов мышления: на которых основаны математические теории логики и вероятностей. стр. 72.
4. Brown, Frank Markham (2012) [2003, 1990]. Булевое рассуждение - Логика булевых уравнений (переиздание 2-го изд.). Минеола, Нью-Йорк: Dover Publications, Inc. стр. 42. ISBN 978-0-486-42785-0.[1]
5. Шеннон, Клод (январь 1949). «Синтез двухтерминальных коммутационных схем» (PDF) . Bell System Technical Journal . 28 : 59–98 [62]. doi :10.1002/j.1538-7305.1949.tb03624.x. ISSN  0005-8580.
6. Перковски, Марек А.; Грыгель, Станислав (1995-11-20), "6. Исторический обзор исследований по декомпозиции", Обзор литературы по декомпозиции функций , Версия IV, Группа функциональной декомпозиции, Кафедра электротехники, Портлендский университет, Портленд, Орегон, США, стр. 21, CiteSeerX 10.1.1.64.1129 (188 страниц)

Смотрите также

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

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

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