P. Wadler的论文中的“严酷莫纳德"中的“⊥"是什么意思? [英] What does “⊥” mean in “The Strictness Monad” from P. Wadler's paper?
问题描述
Can someone help me understand the following definition from Wadler's paper titled "Comprehending Monads"? (Excerpt is from section 3.2/page 9, i.e., the "Strictness Monad" subsection.)
有时，有必要在懒惰的功能程序中控制评估的顺序.这通常是通过可计算函数 strict 来实现的，该函数由
严格 f x =如果 x ≠⊥则 f x 其他
strict f x = if x ≠ ⊥ then f x else ⊥.
操作上，首先通过将 x 简化为弱头范式(WHNF)来降低 strict f x 然后减少应用程序 f x .另外，可以安全地并行减少 x 和 f x ，但是直到 x 在WHNF中.
Operationally, strict f x is reduced by first reducing x to weak head normal form (WHNF) and then reducing the application f x. Alternatively, it is safe to reduce x and f x in parallel, but not allow access to the result until x is in WHNF.
在本文中，我们还没有看到由两条垂直线组成的符号的使用(不确定其被称为什么)，所以它有点冒出来.
In the paper, we have yet to see use of the symbol made up of the two perpendicular lines (not sure what it's called) so it sort of comes out of nowhere.
鉴于Wadler继续说我们将使用[严格]理解来控制懒惰程序的评估"，这似乎是一个非常重要的概念.
Given that Wadler goes on to say that "we will use [strict] comprehensions to control the evaluation of lazy programs", it seems like a pretty important concept to understand.
推荐答案
您描述的符号是底部".它来自顺序理论(尤其是晶格理论).如果存在部分排序集的底部"元素，则该元素位于所有其他元素之前.在编程语言语义中，它指的是比其他任何定义都少"的值.通常会为每个产生错误或无法终止的计算分配最低"值，因为试图区分这些条件会极大地削弱数学功能并使程序分析变得复杂.
The symbol you describe is "bottom". It comes from order theory (particularly lattice theory). The "bottom" element of a partially ordered set, if one exists, is the one that precedes all others. In programming language semantics, it refers to a value that is "less defined" than any other. It's common to assign the "bottom" value to every computation that either produces an error or fails to terminate, because trying to distinguish these conditions greatly weakens the mathematics and complicates program analysis.
要将事物与另一个答案联系在一起，逻辑假"值是真值格的底部元素，而真"是顶部元素.在古典逻辑中，这是仅有的两种，但也可以考虑具有无限多个真实性值的逻辑，例如直觉主义和各种形式的建构主义.这些将观念带入了一个截然不同的方向.
To tie things into another answer, the logical "false" value is the bottom element of a lattice of truth values, and "true" is the top element. In classical logic, these are the only two, but one can also consider logics with infinitely many truthfulness values, such as intuitionism and various forms of constructivism. These take the notions in a rather different direction.
这篇关于P. Wadler的论文中的“严酷莫纳德"中的“⊥"是什么意思?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
