haskell - 从什么意义上说，一个函数的定义“定义”比另一个函数少？

Question

我的意思是，来自definition：


fix f是函数f的最小固定点


换一种说法：


最小定义的x，例如f x = x。


任何无效类型的最小定义值为undefined。这里仍有一些歧义，因为undefined可能表示“将引发错误”（更好）或“将永不终止”（更糟）。正如推理和试验所显示的那样，fix (+1)和fix pred :: Word似乎都从未接近终止（即使pred 0是一个错误），因此“永不终止”中较差的一个很可能总是在这两种选择之间选择。 （可以逃避fix的是无聊的const 1，但稍后再说。）

这不是应用fix的有用方法。

应用fix的有用方法是：

fix (\f x -> if x > 7 then f (x - 1) else x)

-即使用 fix神奇地产生一个递归函数。 （这永远不会使我感到惊奇。）这可以看作是在两个函数之间进行选择： \f x -> f (x - 1)和 \_ x -> x，其中一个从不求值第一个绑定变量。这是一个危险的玩具，因为我们可能仍然会获得不终止其一半域的功能，就像不小心将 >切换到 <或将 -切换到 +一样容易。

因此，这两个功能将以某种方式出现：

f1 = \f x -> f (x - 1)

f2 = \_ x -> x

-后者是“最不明确的”。如果我们斜视一下，实际上我们可以在其中找到我们无聊的同伴 const，只需 flip就可以了。

现在，这是违反直觉的。实际上， f2具有更高的容错能力，因此在某种意义上，它定义的输入值要比 f1更多。 （尤其是，这就是让它逃避 fix否则为无限循环的原因）。具体来说，为与 f2加上 (f, x)的所有相同输入对 f1定义 (undefined, x)。同样， const 1是所有一元函数中最容错的。

那么，我现在如何理解定义？



这个问题的一些理由

this answer nearby与 fix提出的直觉不同。它还强调，为了全面理解，必须转到有关指称语义学的外部教程。

我想提供一个答案，该答案可以支持或解释此处提出的直觉，而且，如果领域理论确实在评论中提出的草书顺序的背后，则至少应包括允许以下方面的经验法则：但是有限，但是领域理论的实际应用。我想看到的问题的一个特殊部分是，能否始终将 fix函数分解为常数函数和归约函数，这些函数的定义是什么。

我的愿望是在扎实的数学推理的支持下，在构建有用且安全的 fix编码的递归时获得实际可行的答案。

Answer 1

在Haskell中，函数是纯函数。他们接受输入并产生输出。因此自然而然地出现了一个问题：那些不终止的函数呢？

f x = 1 + f x

此函数将您的解释器锁定在无限循环中。但是从数学上讲，我们必须说它“返回”某些东西，否则它不是一个函数。我们将这种特殊的“出问题”值称为“底部”值，并用符号 ⊥表示。

因此，从数学上讲，Haskell Int类型包含每个整数，以及一个附加的特殊元素： ⊥。我们将包含 ⊥的类型称为“提升”类型，几乎在Haskell中使用的所有类型都将提升。[1]事实证明，无限循环不是调用 ⊥的唯一方法。我们还可以通过以其他方式“破坏”解释器来做到这一点。您将看到的最常见的方法是使用 undefined，它是一个内置函数，会因一般错误而暂停程序。

但是还有另一个问题。具体来说，就是停顿问题。如果 ⊥应该表示无限循环和其他不可预测的问题，则某些功能我们无法在Haskell中编写。例如，以下伪代码是无意义的。

doesItHalt :: a -> Bool
doesItHalt ⊥ = False
doesItHalt _ = True

这将检查结果值是否为 ⊥，这将解决暂停问题。显然，我们无法在Haskell中做到这一点。那么我们可以在Haskell中定义哪些功能？我们可以定义相对于定义顺序是单调的那些。我们将 ⊑定义为此排序。我们说 ⊥是定义最少的值，所以 ⊥ ⊑ x代表所有 x。 ⊑是部分排序，因此无法比较某些元素。 1 ⊑ 1时， 1 ⊑ 2或 2 ⊑ 1都不是正确的。用纯英语来说，我们说的是 1肯定比 1定义的要少或相等（显然；它们是相同的值），但是说 的定义比 1或多或少。它们只是...不同的价值。

在Haskell中，我们只能定义相对于此顺序为单调的函数。因此我们只能为所有值 2和 a定义函数，如果 b则 a ⊑ b。我们上面的 f a ⊑ f b失败，因为例如 doesItHalt但 ⊥ ⊑ "foo"和 f ⊥ = False。如我们之前所说，两个完全定义但不相等的值是不可比较的。因此，此功能无法正常工作。

简而言之，我们将排序方式定义为这种方式的原因是，当我们使用模式匹配“检查”一个值时，它断言必须至少对其进行足够的定义才能使我们看到匹配的部分。如果不是，那么我们将始终得到 f "foo" = True，因为该程序将崩溃。

值得一提的是，在我们讨论 ⊥之前，存在“部分定义”的值。例如， fix（在Haskell中，我们可以将其写为 1 : ⊥）是一个列表，其第一个元素已定义，但列表的末尾未定义。从某种意义上说，此值比简单的 1 : undefined“定义更多”，因为我们至少可以模式匹配并提取第一个值。所以我们要说 ⊥。因此，我们最终得到了“定义性”的层次结构。

现在， ⊥ ⊑ (1 : ⊥) ⊑ (1 : [])表示它返回定义最少的固定点。函数 fix的不动点是一个值 f，例如 x。让我们用一些示例进行尝试，看看是否可以弄清楚它为什么这么说。让我们定义一个函数

f 0 = 1
f x = x

此功能有很多固定点。对于除零以外的任何 x = f x， x。根据我们的“最不明确”原则，将返回哪一个？实际上，由于 f x = x将返回 ⊥，因此 f ⊥将有效。如果将 ⊥传递给 undefined，则第一个模式匹配将导致程序崩溃，因为我们正在将未定义的值与 f进行比较。所以 0是一个定点，并且由于它是最小的定义值，因此它将由 ⊥返回。在内部， fix f通过将函数无限地应用到自身而起作用，因此这很有意义。应用 fix将继续尝试将内部参数与 f (f (f ...))进行比较，并且永远不会终止。现在让我们尝试其他功能。

g x = 0

将此函数无限地应用到自身上，给出 0。事实证明， 0。为什么在这种情况下返回 fix g = 0而不返回 0？事实证明， ⊥不能成为该函数的定点。 ⊥。由于从未检查过参数并且Haskell是非严格语言，因此即使您通过 g ⊥ = 0或 g或一些荒谬的无限递归值作为参数， 0也会返回 undefined。因此，即使是提升类型， error "Oops!"的唯一固定点也是 g，因为 0。因此， g 0 = 0确实是 0的最小定义固定点。

因此，总而言之，我们定义一个数学框架，以便严格描述某些功能不会终止的概念。 “最不定义”只是一种非常精确的数学方式，它表示 g不适用于其参数始终严格严格的函数。如果 fix将返回 f ⊥，则 ⊥也将返回 fix f。



*此答案大部分由 the wiki page on Denotational Semantics解释和概括。我鼓励阅读该页面以获取更多信息；它被编写为非数学家非常容易理解，并且非常有用。

[1]一些原始类型尚未提出。例如，特定于GHC的 ⊥是不包含 Int#的整数类型，并且在某些地方内部使用。