在Haskell中编写Lambda微积分高阶递归方案

Question

[我在这里的新理由，可能有一些歧义]

考虑递归（这是对较高类型的原始递归的概括），

R_\sigma A B 0 = A
R_\sigma A B (S(C)) = B(R_\sigma A B C) C

其中r是Sigma型，A是Sigma类型的Sigma，B是Sigma类型 - ＆GT类型; n-＆gt; Sigma和C是N型。

如果我们将Sigma的类型视为自然数，则递归是原始的递归，因此我们可以定义原始的递归函数。现在，如果我们将Sigma的类型更改为n - ＆gt; n，我们可以使用r来定义超过原始递归函数的函数，一个示例是ackermann函数，但定义的所有函数将是总的。我的兴趣是了解递归的真正工作原理，因为该概念在另一种情况下似乎有用。

我遇到了一篇文章，该文章将R定义为上述，并使用lambda cyculus来定义前任，加法和乘法的功能，如下所示（对介绍 - 对介绍 - 我没有声誉来发布图像

Pred^{N->N} = R_N 0_N (\lambda a^N b^N.b)
Add^{N->N->N} = \lambda x^N. R_N x(\lambda a^N b^N.S_+ a)
Mult^{N->N->N} = \lambda x^N. R_N 0_N(\lambda a^N b^N. Add a x)

）能够定义Haskell中的功能或递归。我试图将递归定义为一个函数，

rn :: Int -> (Int -> Int -> Int) -> Int -> Int
rn a b 0 = a
rn a b c = b(rn a b (c-1)) (c-1)

但我不明白如何使用它来定义乘法，因为我不了解应如何馈送/定义参数。我应该为不同的递归方案实施两个不同的功能吗？

前任似乎在这样写时可以工作，我可以实现加法，但是乘法会越过我的脑海。

project2to2 :: Int -> Int -> Int
project2to2 m n = n

predecessor :: Int -> Int
predecessor a = rn 0 project2to2 a

在Haskell中，如何定义递归和PRED，添加和多函数？

Answer 1

这似乎主要是混凝土语法的问题：

predecessor :: Int -> Int
predecessor = rn 0 (\a b -> b)

add :: Int -> Int -> Int
add = \x -> rn x (\a b -> 1+a)

mult :: Int -> Int -> Int
mult = \x -> rn 0 (\a b -> add a x)