P. Wadler的论文中的“严格单子”中的“⊥”是什么意思？
有人能帮助我理解Wadler的题为“理解单子”的论文中的下列定义吗？ （摘录来自3.2节/第9页，即“严格单子”小节。）
有时候需要在懒惰的功能程序中控制评估顺序。 这通常是通过严格定义的可计算函数来实现的
严格的fx =如果x≠⊥然后fx else⊥。
在操作上，通过首先将x减小到弱头标准形式（WHNF）然后减小应用f x来减小严格的fx。 或者，可以并行减少x和fx，但在x处于WHNF之前不允许访问结果。
在这篇论文中，我们还没有看到使用由两条垂直线组成的符号（不知道它叫什么），所以它从某种意义上来说是无处不在的。
鉴于Wadler继续说“我们将使用[严格]理解来控制懒惰程序的评估”，这似乎是一个非常重要的概念。
你描述的符号是“底部”。 它来自有序理论（特别是晶格理论）。 部分有序集合的“底部”元素（如果存在的话）是所有其他元素之前的元素。 在编程语言语义中，它指的是一个比其他任何“定义更少”的值。 将“底部”值分配给每个产生错误或无法终止的计算是很常见的，因为试图区分这些条件会极大地削弱数学运算并使程序分析变得复杂。
为了将事情联系到另一个答案中，逻辑“假”值是真值的格子的底层元素，“真”是最高元素。 在古典逻辑中，这是唯一的两个，但也可以考虑具有无限多的真值的逻辑，比如直觉主义和各种形式的建构主义。 这些概念在一个相当不同的方向。
在标准的布尔逻辑中，符号⊥ ，读为falsum或bottom，就是一个总是为false的语句，相当于编程语言中的false常量。 这个形式是符号⊤ （ ⊤或顶部）的倒置（颠倒）版本，它与true值相同 - 并且在符号看起来像大写字母T的事实中存在助记符值（名称为verum和falsum对于“真”和“假”是拉丁语;名称“顶部”和“底部”来自使用有序集理论中的符号，它们是根据水平横条的位置选择的。）
在可计算性理论中， ⊥也是一个不可计算的计算值，所以你也可以把它看作未定义的值。 不管为什么计算是无法计算的 - 无论是因为它有未定义的输入，或者从不终止，或者其他什么。 你的代码片段是第一个原因的形式化：它将strict定义为一个函数，它使得任何计算（另一个函数）在其输入（参数）未定义时都是未定义的。
上一篇: What does “⊥” mean in “The Strictness Monad” from P. Wadler's paper?