P. Wadler 论文的“The Strictness Monad”中的“⊥”是什么意思？

Question

有人可以帮我理解 Wadler 题为“Comprehending Monads”的论文中的以下定义吗？ （摘自第 3.2 节/第 9 页，即“Strictness Monad”小节。）

---

有时需要在惰性函数程序中控制求值顺序。这通常通过由

定义的可计算函数strict来实现

严格 f x = 如果 x ≠ ⊥ 那么 f x 其他 ⊥.

在操作上，strict f x 通过首先将 x 归约为弱头范式 (WHNF) 来归约然后减少应用f x。或者，并行减少 x 和 f x 是安全的，但在 x之前不允许访问结果> 在 WHNF 中。

---

在论文中，我们还没有看到使用由两条垂直线组成的符号（不知道它叫什么），所以它有点不知从何而来。

鉴于 Wadler 继续说“我们将使用 [严格] 推导来控制惰性程序的评估”，这似乎是一个非常重要的概念。

Answer 1

您描述的符号是“底部”。它来自有序理论（尤其是格理论）。部分有序集合的“底部”元素（如果存在）是所有其他元素之前的元素。在编程语言语义中，它指的是一个比任何其他值“定义较少”的值。为每个产生错误或未能终止的计算分配“底部”值是很常见的，因为试图区分这些条件会大大削弱数学运算并使程序分析复杂化。

为了将事物与另一个答案联系起来，逻辑“假”值是真值格的底部元素，而“真”是顶部元素。在经典逻辑中，只有这两种，但也可以考虑具有无限多个真实值的逻辑，例如直觉主义和各种形式的建构主义。这些将概念引向了一个完全不同的方向。

Answer 2

在标准布尔逻辑中，符号⊥，读作falsum 或bottom，只是一个始终为假的语句，相当于false 常量在编程语言中。该形式是符号⊤（verum 或top）的倒置（颠倒）版本，相当于true - 并且有助记符值事实上，这个符号看起来像一个大写字母 T。（名称 verum 和 falsum 在拉丁语中表示“真”和“假”；名称“top”和“底部”来自有序集合理论中符号的使用，它们是根据水平横杆的位置选择的。）

在可计算性理论中，⊥ 也是一个不可计算的计算值，所以你也可以把它看成是未定义的值。为什么计算不可计算并不重要——无论是因为它有未定义的输入，还是永远不会终止，或者其他什么。您的 sn-p 是第一个原因的形式化：它将 strict 定义为一个函数，只要其输入（参数）未定义，该函数就会使任何计算（另一个函数）未定义。