问用Haskell编写lambda微积分高阶递归格式

EN

我在这里有新的理由，可能有些模棱两可

考虑递归(它是对高级类型的原始递归的推广)。

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

R为乙型，A为乙型，B为σ->型，N型为->型，C型为N型。

如果把σ的类型看作自然数，则递归是本原递归，用它我们可以定义原语递归函数。现在，如果我们将sigma的类型改为N -> N，我们可以使用R来定义超越原始递归函数的函数，例如Ackermann函数，但是定义的所有函数都是完全的。我感兴趣的是了解递归器是如何工作的，因为这个概念在另一个上下文中似乎很有用。

我遇到了一篇文章，将R定义为上述，并使用lambda演算来定义前任函数、加法函数和乘法函数，如下所示(很抱歉，我不喜欢发布图片)

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、Add和Mult函数？