找出以下 lambda 演算项的最一般类型
Find the most general types of the following lambda calculus terms
我无法理解为什么这些是各自教堂数字的最通用类型：
2 = λf.λx. f (f x) : (α → α) → α → α
1 = λf.λx. f x : (α → β) → α → β
0 = λf.λx. x : β → α → α
我以为所有的 Church 数字都有相同的类型 :
(α → α) → α → α
另外，我如何找到加法运算符的通用类型
λm.λn.λf.λx. m f (n f x)
非常感谢任何帮助，谢谢！
让我们从零的教会数字开始：
λf.λx. x : β → α → α
只看λf.λx.部分，可以推断我们有一个双参数函数，因此它的类型是α → β → γ，其中α和β代表参数类型和 γ 代表结果类型。现在，函数体 x 进一步限制了类型：我们函数的 return 类型必须与其第二个参数的类型相同。结果是 α → β → β，或者重命名后 (α ↔ β)：λf.λx. x : β → α → α。这是零的最一般类型，因为我们没有使用 f 应该是一个函数这一事实，事实上，untyped lambda 演算中的 Church 零数不是'不在乎：它只是忘记了它的第一个参数。由于 β 只是一个占位符，您可以 将其特化 为 α → α，这会产生更具体的零类型 —— λf.λx. x : (α → α) → α → α。
我们来看看1:
λf.λx. f x : (α → β) → α → β
同样，它是一个双参数函数：α → β → γ，但是这次（查看 1 的主体）我们知道第一个参数 f 是一个函数，所以f 有一些类型 δ → ε，我们应该用它代替 α：(δ → ε) → β → γ。现在，我们知道我们必须能够将 f 应用于 x，这意味着 x 的类型和 f 的参数类型必须相等： δ = β，因此，我们达到了 (β → ε) → β → γ。但这并不是我们所知道的全部，f x 有类型 ε，而我们的数字 returns 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 的 3、4 等具有与 2 相同的最通用类型，因为多功能应用程序没有给我们任何额外的信息来进一步专门化类型。
关于加法函数λm.λn.λf.λx. m f (n f x)，我说得再简洁一点：
- 假设表达式的类型为
α → β → γ → δ → ε.
m 是 2 个参数的函数：α 必须限制为 α' → α'' → α'''- 与
n 相同：β 必须限制为 β' → β'' → β'''
m的和n的第一个参数类型相同，是f的类型：α' = β' = γn的第二个参数的类型是δn的结果类型等于m的第二个参数类型：β''' = α''- 让我们结合以上所有知识进行
n : γ → δ → α''
m : γ → α'' → ε- 因此，结果类型是
(γ → α'' → ε) → (γ → δ → α'') → γ → δ → ε
让我们重命名变量以使其看起来更漂亮：
λm.λn.λf.λx. m f (n f x) 最常见的类型是
(β → γ → ε) → (β → α → γ) → β → α → ε.
让我们检查一下它是否可以专门用于人们期望的对教堂数字的二元运算
(β = α → α, γ = α, ε = α):
((α → α) → α → α) → ((α → α) → α → α) → (α → α) → α → α.
我无法理解为什么这些是各自教堂数字的最通用类型：
2 = λf.λx. f (f x) : (α → α) → α → α
1 = λf.λx. f x : (α → β) → α → β
0 = λf.λx. x : β → α → α
我以为所有的 Church 数字都有相同的类型 :
(α → α) → α → α
另外，我如何找到加法运算符的通用类型
λm.λn.λf.λx. m f (n f x)
非常感谢任何帮助，谢谢！
让我们从零的教会数字开始：
λf.λx. x : β → α → α
只看λf.λx.部分，可以推断我们有一个双参数函数，因此它的类型是α → β → γ，其中α和β代表参数类型和 γ 代表结果类型。现在，函数体 x 进一步限制了类型：我们函数的 return 类型必须与其第二个参数的类型相同。结果是 α → β → β，或者重命名后 (α ↔ β)：λf.λx. x : β → α → α。这是零的最一般类型，因为我们没有使用 f 应该是一个函数这一事实，事实上，untyped lambda 演算中的 Church 零数不是'不在乎：它只是忘记了它的第一个参数。由于 β 只是一个占位符，您可以 将其特化 为 α → α，这会产生更具体的零类型 —— λf.λx. x : (α → α) → α → α。
我们来看看1:
λf.λx. f x : (α → β) → α → β
同样，它是一个双参数函数：α → β → γ，但是这次（查看 1 的主体）我们知道第一个参数 f 是一个函数，所以f 有一些类型 δ → ε，我们应该用它代替 α：(δ → ε) → β → γ。现在，我们知道我们必须能够将 f 应用于 x，这意味着 x 的类型和 f 的参数类型必须相等： δ = β，因此，我们达到了 (β → ε) → β → γ。但这并不是我们所知道的全部，f x 有类型 ε，而我们的数字 returns 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 的 3、4 等具有与 2 相同的最通用类型，因为多功能应用程序没有给我们任何额外的信息来进一步专门化类型。
关于加法函数λm.λn.λf.λx. m f (n f x)，我说得再简洁一点：
- 假设表达式的类型为
α → β → γ → δ → ε. m是 2 个参数的函数：α必须限制为α' → α'' → α'''- 与
n相同：β必须限制为β' → β'' → β''' m的和n的第一个参数类型相同，是f的类型：α'=β'=γn的第二个参数的类型是δn的结果类型等于m的第二个参数类型：β'''=α''- 让我们结合以上所有知识进行
n : γ → δ → α'' m : γ → α'' → ε也一样
- 因此，结果类型是
(γ → α'' → ε) → (γ → δ → α'') → γ → δ → ε
让我们重命名变量以使其看起来更漂亮：
λm.λn.λf.λx. m f (n f x) 最常见的类型是
(β → γ → ε) → (β → α → γ) → β → α → ε.
让我们检查一下它是否可以专门用于人们期望的对教堂数字的二元运算
(β = α → α, γ = α, ε = α):
((α → α) → α → α) → ((α → α) → α → α) → (α → α) → α → α.