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

Posted 2023-02-24

【中文标题】P. Wadler 论文的“The Strictness Monad”中的“⊥”是啥意思？

【英文标题】：What does “⊥” mean in “The Strictness Monad” from P. Wadler's paper?P. Wadler 论文的“The Strictness Monad”中的“⊥”是什么意思？

【发布时间】：2014-12-13 06:17:11

【问题描述】：

有人可以帮我理解 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 继续说“我们将使用 [严格] 推导来控制惰性程序的评估”，这似乎是一个非常重要的概念。

【问题讨论】：

俗称底。

你的问题和 monad 有什么关系？

它被称为底部，或者在 Haskell 中专门称为 undefined。这只是它的一种形式，尽管从技术上讲，底部也是一种非终止计算，例如length [1..]

见bottom type。底部基本上意味着，这个表达式不可计算/永远运行/从不返回值/抛出异常/等等。规则是：如果x 是可计算的，那么strict f x 计算为f x，但如果x 是不可计算的，那么strict f x 计算为“不可计算”。换句话说：说f x = 2 * x。 f (1 / 0) 是什么？你无法评估它，因为你无法评估(1 / 0)。

@leftaroundabout：我可能应该在我的原始帖子中更清楚地说明这一点。摘录自一篇题为“理解单子”的论文。具体的小节称为“严格单子”。

【参考方案1】：

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

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

【参考方案2】：

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

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

【讨论】：

除了在惰性函数式语言中，即使x 未定义，f x 也可以定义！例如如果f = const 1。 Wadler 不仅观察到如果输入未定义函数的结果是未定义的（因为这并不总是正确的），他正在定义函数strict 将任何函数转换为具有此属性。