4

在页面https://en.wikibooks.org/wiki/Haskell/Denotational_semantics#Pattern_Matching有以下练习：

考虑具有or以下属性的两个布尔参数的函数：

  • 或⊥ ⊥ = ⊥</li>
  • 或真 ⊥ = 真
  • 或 ⊥ 真 = 真
  • 或假 y = y
  • 或 x 假 = x

这个函数是联合严格性的另一个例子，但更清晰：如果两个参数都是（至少当我们将参数限制为 True 和 ⊥ 时），结果只是 ⊥。在 Haskell 中可以实现这样的功能吗？

该函数可以用下表表示：

      |   ⊥   | False | True
------|-----------------------
  ⊥   |   ⊥   |   ⊥   | True
False |   ⊥   | False | True
True  | True  | True  | True

根据https://en.wikibooks.org/wiki/Haskell/Denotational_semantics#Monotonicity中给出的定义，这个函数是单调的，所以我认为没有理由排除在 Haskell 中实现这个函数的可能性。尽管如此，我没有看到实现它的方法。

练习的答案是什么？

PS：我知道答案是“不，你不能”。我正在寻找的是一个严格的证明。我觉得我错过了一些关于可以定义哪些功能的重要限制。绝对不是所有的单调函数。

4

2 回答 2

7

假设您要尝试评估or x y. 为此，您必须选择一个或另一个参数来查看评估它是否会导致Trueor False。如果你猜对了，你会知道结果是否应该True评估False另一个参数（可能是 ⊥）。

但是，如果您猜错了，您将永远无法完成对论证的评估；要么你会陷入无限循环，要么你会遇到运行时错误。

并发使您可以并行评估两个参数[1]。假设两个参数之一的计算结果为适当Boolean的，则两个分支之一将成功找到它。另一个分支将引发错误（在这种情况下，您可以简单地丢弃该分支并忽略错误）或陷入循环（当另一个分支成功时您可以强制终止该循环）。无论哪种方式，您最终都可以得到正确的答案。

如果两个参数都导致⊥，当然，隐含的结果or仍然是⊥；你不能完全绕过停机问题。

[1] “并行”并不一定是指分叉另一个进程并同时评估它们。您可以评估N步骤的一个参数（对于某些值N以及“步骤”的含义）；如果出现错误，放弃并尝试另一个参数，如果你还没有终止，暂停这个线程并尝试另一个N步骤。继续在两者之间来回跳动，直到其中一个产生具体值。

于 2019-11-28T17:44:25.107 回答
6

unamb包unsafePerformIO使用chepner 的回答中描述的并发（和）来实现可以定义并行的原语or。

parOr :: Bool -> Bool -> Bool
parOr x y = (x || y) `unamb` (y || x)  -- unamb from Data.Unamb
于 2019-11-28T17:51:12.973 回答