Алгебра Гейтинга и Bool

Алгебра Гейтинга

Алгебра Гейтинга представляют собой ограниченные решетки, которые также снабжены дополнительной бинарной операцией imp (для импликации, также записываемой как →).

Импликация подчиняется следующим законам:

a → a = 1
a ∧ (a → b) = a ∧ b
b ∧ (a → b) = b
a → (b ∧ c) = (a → b) ∧ (a → c)

В алгебрах Гейтинга and эквивалентно meet и or эквивалентно join; доступны оба метода.

Алгебра Гейтинга также определяет операцию дополнения (complement) (иногда записываемую как ¬a). Дополнение к a эквивалентно (a → 0), и выполняются следующие законы:

а ∧ ¬а = 0

Однако в алгебрах Гейтинга эта операция является лишь псевдодополнением, поскольку алгебры Гейтинга не обязательно обеспечивают закон исключенного третьего. Это означает, что нет никакой гарантии, что (a ∨ ¬a) = 1.

Алгебры Гейтинга моделируют интуиционистскую логику. Для модели классической логики см. ниже класс типов булевой алгебры, реализованный как Bool.

Heyting[A] - типы, образующие алгебру Гейтинга

complement (унарное ~): логическое отрицание
and (&, meet): конъюнкция ("И")
or (|, join): дизъюнкция ("ИЛИ")
xor (^): исключающее дизъюнкция: or(and(a, complement(b)), and(complement(a), b))
imp: следствие ("НЕ a или b"), эквивалентно ~a | b
nand: "не И", эквивалентно ~(a & b): complement(and(a, b))
nor: "не ИЛИ", эквивалентно ~(a | b): complement(or(a, b))
nxor: "не xor", эквивалентно ~(a ^ b): complement(xor(a, b))

Bool

Bool поддерживает булеву алгебру — абстракцию знакомых побитовых логических операторов.

Булевы алгебры являются алгебрами Гейтинга с дополнительным ограничением, заключающимся в истинности закона исключенного третьего (что эквивалентно истинному двойному отрицанию). Это означает, что помимо законов, которым подчиняются алгебры Гейтинга, булевы алгебры также подчиняются следующим:

(а ∨ ¬а) = 1
¬¬а = а

Булевы алгебры обобщают классическую логику: единица эквивалентна "истине", а ноль эквивалентен "ложности". Булевы алгебры предоставляют дополнительные часто используемые логические операторы, такие как xor, nand, nor и nxor. У каждой булевой алгебры есть двойственная алгебра, которая включает в себя изменение местами истинное/ложное, а также и/или.

complement (унарное ~): логическое отрицание
and (&, meet): конъюнкция ("И")
or (|, join): дизъюнкция ("ИЛИ")
xor (^): исключающее дизъюнкция: or(and(a, complement(b)), and(complement(a), b))
imp: следствие ("НЕ a или b"), эквивалентно ~a | b
nand: "не И", эквивалентно ~(a & b): complement(and(a, b))
nor: "не ИЛИ", эквивалентно ~(a | b): complement(or(a, b))
nxor: "не xor", эквивалентно ~(a ^ b): complement(xor(a, b))

Экземпляры Bool существуют не только для Boolean, но и для Byte, Short, Int, Long, UByte, UShort, UInt и ULong.

Ссылки: