1

我很难理解为什么这些是各自教会数字的最通用类型：

2 = λf.λx. f (f x) : (α → α) → α → α 

1 = λf.λx. f x : (α → β) → α → β

0 = λf.λx. x : β → α → α

我认为所有教堂数字都有相同的类型：

(α → α) → α → α

另外，我将如何找到 add 运算符的通用类型

λm.λn.λf.λx. m f (n f x)

任何帮助将不胜感激，谢谢！

4

1 回答 1

2

让我们从零的教堂数字开始：

λf.λx. x : β → α → α

只看λf.λx.部分，可以推断出我们有一个双参数函数，因此它的类型是α → β → γ， whereα和β代表参数的类型，γ代表结果类型。现在，主体x进一步限制了类型：我们函数的返回类型必须与其第二个参数的类型相同。这导致α → β → β，或重命名后 (α ↔ β): λf.λx. x : β → α → α。这是最通用的零类型，因为我们没有使用f应该是函数的事实，事实上，无类型 lambda 演算中的 Church 零数字并不关心：它只是忘记了它的第一个参数。由于β它只是一个占位符，您可以将其专门用于α → α，这导致零的更具体的类型 - λf.λx. x : (α → α) → α → α。

让我们看看1：

λf.λx. f x : (α → β) → α → β

同样，它是一个有两个参数的函数：α → β → γ，但是这一次（看看 的主体1）我们知道第一个参数f是一个函数，所以f有一些类型δ → ε，我们应该用它来代替α: (δ → ε) → β → γ。现在，我们知道我们必须能够应用于f，x这意味着 的类型x和f的参数的类型必须相等：δ= β，因此，我们已经达到了(β → ε) → β → γ。但这并不是我们所知道的全部，f x有 type ε，我们的数字返回f x，应用这些信息，我们得到ε= γ。结合所有这些，我们到达(β → γ) → β → γ，或重命名后：λf.λx. f x : (α → β) → α → β. 同样，我们没有使用任何有关我们使用意图的信息，这就是为什么我们有最通用的类​​型，当然，它可以专门化（通过限制β= α）到λf.λx. f x : (α → α) → α → α.

现在2轮到了：

λf.λx. f (f x) : (α → α) → α → α

这次我不会重复所有步骤，但是（作为中间步骤）我们可以到达λf.λx. f (f x) : (α → β) → α → β. 但是请注意，这一次我们将f' 结果输入到自身中：f (f x)，这意味着f' 的输入和输出类型必须相等，因此β= α，最通用的类​​型是λf.λx. f (f x) : (α → α) → α → α这次。

(*)请注意，Church's 3、4等具有与 do 相同的最通用类型2，因为多功能应用程序不会为我们提供任何额外信息来进一步专门化该类型。

至于加法功能λm.λn.λf.λx. m f (n f x)，让我更简洁一点：

  • 假设表达式具有类型α → β → γ → δ → ε。
  • m是 2 个参数的函数：α必须限制为α' → α'' → α'''
  • 相同的n:β必须限制为β' → β'' → β'''
  • m's 和n' 的第一个参数具有相同的类型，即f: α'= β'=γ
  • n的第二个参数的类型是δ
  • n的结果类型等于m的第二个参数类型：β'''=α''
  • 让我们结合以上所有知识n : γ → δ → α''
  • 相同的m : γ → α'' → ε
  • 因此，结果类型是(γ → α'' → ε) → (γ → δ → α'') → γ → δ → ε

让我们重命名变量以使其看起来更漂亮：

最通用的类​​型λm.λn.λf.λx. m f (n f x)是

(β → γ → ε) → (β → α → γ) → β → α → ε.

让我们检查一下它是否可以专门用于对 Church 数字（β= α → α、γ= α、ε= α）进行二元运算的期望：

((α → α) → α → α) → ((α → α) → α → α) → (α → α) → α → α.

于 2016-05-09T16:24:38.530 回答