Существует эквивалентность между логическими операциями и операциями над множествами. Например, возьмем следующее логическое утверждение:

«Идет дождь, значит, на небе тучи».

Без облаков не было бы дождя. Мы можем взять два набора местоположений, «множество мест, где идет дождь» и «множество мест, где есть облака», и показать, что первое множество строго входит во второе множество.

Точно так же в информатике вывод типа основан на логических операциях между типами, и тип можно рассматривать как набор всех объектов, принадлежащих этому типу (если есть хотя бы один такой объект, вы можете сказать, что тип заполнен, иначе он пусто. )

Вывод типа использует логические доказательства и направлен на поиск заполненных типов, поскольку программы обрабатывают объекты, тип которых мы хотим найти.

Из-за приведенной выше эквивалентности я буду иллюстрировать логические операции, используя множества в духе Буля . Каждая операция над множествами будет выражаться с использованием логического соединителя и логической нотации.

Для обсуждения я буду использовать два интервала над целыми числами A и B в качестве входных наборов.

А: 0…10

Б: 5…18

Дополнение

Разъем: нет

Результат содержит все элементы, которых нет в A .

¬A: …-1, 11…

Союз

Разъем: или

Результат содержит все элементы, которые находятся в A или B .

А ∨ В: 0…18

Перекресток

Разъем: и

Результат содержит только те элементы, которые находятся как в A , так и в B .

А ∧ В: 5…10

Разделительный союз

Соединитель: иначе (xor)

Результат содержит элементы, которые есть только в A , иначе только в B.

А ⊕ В: 0…4, 11…18

Импликация

Соединитель: только если (подразумевается)

Результат содержит элементы, которые находятся в A , только если они находятся в B .

Это немного сложнее понять, чем предыдущие операции. Легко видеть, что результат содержит пересечение двух множеств: его элементы находятся в A и в B , что удовлетворяет условию.

Но как насчет остальной части B ?

Вы можете видеть, что элементы B вне пересечения не находятся в A . Значит ли это, что они удовлетворяют условию? Это зависит от того, как вы это читаете:

• Результат содержит элементы, которые находятся в A ( только если они находятся в B ).

• Результат содержит элементы (которые находятся в A , только если они находятся в B ).

А ⇒ Б: …-1, 5…

Другой пример: «Дождь идет только при наличии облаков». Если существует место, где идет дождь, но нет облаков, то условие не выполняется . В предложении не ставится условие для мест, где не идет дождь, поэтому они могут быть облачными или нет, либо в порядке.

Разница

Разъем: но не

Результат содержит только те элементы, которые находятся в A , но не в B.

Интересно, что на этот раз нет специального прочтения, но разница на самом деле заключается в дополнении импликации! Также обратите внимание, что порядок A и B имеет значение.

А - В: 0…4