这个 haskell 表达式是什么意思

Question

我刚开始学习 Haskell，我正在尝试在 Haskell 中使用 lambda 演算。我找到了这个将教堂数字转换为数字的表达式，但我似乎无法弄清楚这个表达式中的 0 是什么意思。我到处都找不到它：

zero = (\f -> \x -> x)
one = (\f -> \x -> f x)
two = (\f -> \x -> f (f x))

getNum church = church (\x-> (x + 1)) 0

让我困惑的是最后一个零。它是基本情况还是此 lambda 表达式的某些参数？

Answer 1

这是 "church" 函数的第二个参数。教会数字是在 Lambda 微积分中进行计数的一种方式。它们的工作方式与 Peano 数类似。在你这样算的人中

Z = 0
S Z = 1
S S Z = 2

将"Z"读作"Zero"，将"S"读作"Successor"。所以1是0的后继，2是1的后继。实际上是一元计数。

在 Lambda 微积分中，您只有函数应用程序，因此您可以将 2 定义为一个接受参数 "f" 并应用它两次的函数。

在您的示例中，定义了教堂编号零、一和二。每个都是一个带有两个参数的函数。第一个参数是要应用的函数，第二个是要应用的值。 getnum 函数使用函数 succ（即 \x -> x+1），然后将其应用 N 次到基本情况“0”。

你也可以定义

getPeano church = church ('S':) "Z"

这会将 "S" 的正确数量添加到 Z 之前，以将 Church 编号转换为 Peano 编号。

What does this haskell expression mean