Алгебра Гейтинга и 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

.

---

Ссылки:

• Spire home page
• Learning Spire - Boolean Algebras are pretty cool