交换函数的意外属性？答案

【问题标题】：An unexpected property of commutative functions?交换函数的意外属性？
【发布时间】：2020-08-04 16:14:26
【问题描述】：

我得出了一个令我困惑的陈述（定理？）。我想知道我的逻辑是否合理。

任何可交换非严格函数f :: a -> a -> b 都是一个常数。

理解包括底部在内的交换性，即f x y 和f y x 要么都终止，要么都不终止。

我的非正式推理如下。假设f 是一个非严格函数。然后存在a 使得f a ⊥ 或f ⊥ a 终止。如果f 是可交换的，那么两者都应该终止。但是f 无法审查它的任何一个论点。（如果它首先检查第一个参数，那么f ⊥ a 必须是⊥，反之亦然）。所以它一定是一个常数函数。

这个推理正确吗？

如果f 被允许同时检查两个参数，它显然失败，如果其中一个不是⊥，则成功。但是在 Haskell（一些相当保守的扩展）中允许这样的功能吗？

【问题讨论】：

换句话说，一个可交换函数（有底）要么在两个参数中都是严格的（例如+），要么没有（此时必须是常量）。似乎是对的，因为如果其中一个是严格的，而另一个则不是，那么当其中一个参数为底部时，翻转的调用之一将失败，而另一个成功。 FWIW 对我来说似乎是正确的。
hackage.haskell.org/package/unamb-0.2.7/docs/…
您是否以某种正式的方式使用“非严格”？我可以想象一个函数会部分检查其参数（即自然数上的 min 之类的东西），因此它可以为一些包含底部（min 3 inf）的输入产生答案，但是该语句“那么存在这样一个f a ⊥ 或 f ⊥ a 终止。”似乎不成立
您是对任何可以赋予类型forall a b. a -> a -> b 的函数f 作出这样的声明，还是对任何函数f 作出这样的声称，该函数可以赋予与forall a b. a -> a -> b?也就是说，如果我能找到Bool -> Bool -> Bool 类型的反例f，那么对于这个问题来说，这会是一个有趣的结果吗？（特别是，您似乎倾向于参数化，即如果 f a _|_ 和 f _|_ a 都终止，则 f 无法审查其任何一个论点。）
有人可能会说f :: Int -> Int -> [Int] ; f x y = [x+y] 是可交换的、非严格的、非恒定的。这依赖于[ _|_ ] 与_|_ 不同。如果您出于某种原因认为这是严格的，您应该更准确地定义您的严格概念。

【解决方案1】：

志写

有人可能会说
f :: Int -> Int -> [Int]
f x y = [x+y]
是可交换的、非严格的和非常量的。这依赖于[ _|_ ] 与_|_ 不同。如果您出于某种原因认为这是严格的，您应该更准确地定义您的严格概念。

确实如此！给定任何非常量、可交换函数f，您可以通过将f 的应用程序包装在一个或多个惰性构造函数中来编写非严格、非常量、可交换函数。

【讨论】：