有人可以帮我理解瓦德勒题为“的论文中的以下定义吗？”“？（摘自第 3.2 节/第 9 页，即“Strictness Monad”小节。）
有时有必要控制惰性函数程序中的求值顺序。这通常是通过可计算函数来实现的strict， 被定义为
strict f x = if x≠ ⊥ 则f x else ⊥.
在操作上，strict f x通过首先减少来减少x弱头正常形式（WHNF），然后减少应用f x。或者，减少x and f x并行，但不允许访问结果，直到x位于 WHNF。
在论文中，我们还没有看到由两条垂直线组成的符号（不确定它叫什么）的使用，所以它有点凭空出现。
鉴于瓦德勒接着说“我们将使用[严格]推导式来控制惰性程序的评估”，这似乎是一个需要理解的非常重要的概念。
您描述的符号是“底部”。它来自有序理论（特别是晶格理论）。部分有序集合的“底部”元素（如果存在）是位于所有其他元素之前的元素。在编程语言语义中，它指的是比任何其他值“定义较少”的值。通常将“底部”值分配给每个产生错误或无法终止的计算，因为试图区分这些条件会极大地削弱数学并使程序分析复杂化。
为了将事物与另一个答案联系起来，逻辑“假”值是真值网格的底部元素，而“真”是顶部元素。在经典逻辑中，这是仅有的两种，但我们也可以考虑具有无限多个真实值的逻辑，例如直觉主义和各种形式的建构主义。这些将概念带向了一个相当不同的方向。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
