Haskell实现Lambda演算高阶递归子及前驱/加/乘函数方法

你之前定义的rn逻辑本身没有错，问题在于把递归子的类型参数σ硬编码为Int，且没有理清柯里化下的参数传递逻辑，导致乘法函数无法正确写出。首先给出符合定义的多态版递归子，完全匹配给出的递归规则：

-- 对应递归规则 R_σ A B 0 = A; R_σ A B (S C) = B (R_σ A B C) C
-- 用Int作为自然数类型的实现，(+1)对应后继构造子S
r :: sigma -> (sigma -> Int -> sigma) -> Int -> sigma
r base step 0 = base
r base step n = step (r base step (n-1)) (n-1)

这个版本是通用的：σ既可以是基础自然数类型Int，也可以是函数类型（比如Int -> Int），不需要为不同递归场景修改递归子本身的实现。

前驱函数 Pred #

按照定义Pred = R_N 0 (λa b. b)，逻辑是：0的前驱返回0，对任意大于0的数n=S(k)，直接返回当前递归步数k（也就是n的前驱），不需要用到之前的累积值。

pred :: Int -> Int
pred n = r 0 (\_ b -> b) n

测试：pred 0 = 0，pred 10 = 9，符合预期。

加法函数 Add #

按照定义Add = λx. R_N x (λa b. S a)，逻辑是计算x + y时，以x作为初始累积值，每递归一次对累积值做一次后继操作，共递归y次，最终累积值就是和。

-- 自然数后继函数
s :: Int -> Int
s = (+1)

add :: Int -> Int -> Int
add x y = r x (\a _ -> s a) y

此处step函数的第二个参数为当前递归步数，加法定义中不需要用到该值，因此用通配符忽略，与文献给出的lambda项行为完全一致。测试：add 3 4 = 7，符合预期。

乘法函数 Mult #

按照定义Mult = λx. R_N 0 (λa b. Add a x)，逻辑是计算x * y时，以0作为初始累积值，每递归一次把当前累积值加x，共递归y次，最终累积值就是乘积。

mult :: Int -> Int -> Int
mult x y = r 0 (\a _ -> add a x) y

卡乘法的核心原因是没有把被乘数x作为闭包变量传入step函数：递归子的step逻辑是固定的「加x」，只需要在传入step的时候把x捕获进去即可，不需要修改递归子结构。此处同样不需要用到递归步数参数，用通配符忽略即可。测试：mult 6 7 = 42，符合预期。

当需要定义超越原始递归的函数（比如阿克曼函数）时，只需要把σ实例化为函数类型Int -> Int即可，不需要修改递归子r的代码，这也是这个递归子作为高阶原始递归推广形式的核心能力。

内容的提问来源于stack exchange，提问作者Jii