有人可以帮我理解 Wadler 题为“理解单子”的论文中的以下定义吗？（摘自第 3.2 节/第 9 页，即“Strictness Monad”小节。）
有时有必要控制惰性函数程序中的评估顺序。这通常通过可计算函数strict来实现，定义为
严格 f x = 如果x ≠ ⊥ 那么f x else ⊥。
在操作上，通过首先将x减少为弱头范式 (WHNF) 然后减少应用程序f x来减少严格的 f x。或者，并行减少x和f x是安全的，但在x处于 WHNF 中之前不允许访问结果。
在论文中，我们还没有看到使用由两条垂直线组成的符号（不确定它叫什么），所以它有点不知从何而来。
鉴于 Wadler 继续说“我们将使用 [严格] 推导来控制惰性程序的评估”，这似乎是一个需要理解的非常重要的概念。
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.