Что означает "⊥" в "Строгости Монады" из бумаги П. Вадлера?

Может ли кто-нибудь помочь мне понять следующее определение из документа Вадлера под названием "Понимание монадов"? (Выдержка из раздела 3.2/стр. 9, т.е. Подразделение "Строгость Монады".)

Иногда необходимо контролировать порядок оценки в ленивой функциональной программе. Обычно это достигается с помощью вычислимой функции strict, определенной

strict f x = если x ≠ ⊥, то f x else ⊥.

Оперативно строгое f x сводится к первому уменьшению x до слабой нормальной формы головы (WHNF), а затем уменьшению приложения f x. В качестве альтернативы безопасно уменьшать x и f x параллельно, но не разрешать доступ к результату до тех пор, пока x не будет в WHNF.

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

Учитывая, что Вадлер продолжает утверждать, что "мы будем использовать [строгие] понимания для контроля оценки ленивых программ", кажется, это довольно важная концепция для понимания.

Ответ 1

Символ, который вы описываете, "нижний". Оно исходит из теории порядка (в частности, теории решетки). "Нижний" элемент частично упорядоченного множества, если он существует, является тем, который предшествует всем остальным. В семантике языка программирования это означает значение, которое "менее определено", чем любое другое. Общепринято присваивать "нижнее" значение каждому вычислению, которое либо создает ошибку, либо не завершается, поскольку попытка отличить эти условия значительно ослабляет математику и усложняет анализ программ.

Чтобы связать вещи с другим ответом, логическое "ложное" значение является нижним элементом решетки значений истинности, а "true" является верхним элементом. В классической логике это единственные два, но можно также рассматривать логику с бесконечно многими значениями правдивости, такими как интуиционизм и различные формы конструктивизма. Они принимают понятия в совершенно другом направлении.

Ответ 2

В стандартной логической логике символ ⊥, читающий falsum или bottom, является просто оператором, который всегда является ложным, что эквивалентно константе false в языках программирования. Форма представляет собой инвертированную (перевернутую) версию символа ⊤ (verum или top), что эквивалентно true - и мнемоническое значение в том, что символ выглядит как заглавная буква T. ( Имена verum и falsum являются латинскими для "true" и "false", имена "top" и "bottom" исходят из использования символов в теории упорядоченных множеств, где они были выбраны в зависимости от местоположения горизонтали перекладина.)

В теории вычислимости ⊥ также является значением невычислимого вычисления, поэтому вы можете также считать его значением undefined. Не имеет значения, почему вычисление является бесспорным - независимо от того, имеет ли он undefined входы или никогда не заканчивается или что-то еще. Ваш фрагмент является формализацией первой причины: он определяет строгую как функцию, которая делает любое вычисление (другая функция) undefined, когда его входы (аргументы) undefined.