使用原始递归添加二进制自然数

Question

给定二进制自然数，零情况下是“两倍”情况和“两倍加一”情况。如何使用原始递归（仅使用函数foldBNat）表示加法？

-- zero | n * 2 | n * 2 + 1
data BNat = Z | T BNat | TI BNat
  deriving (Show)

foldBNat :: BNat -> t -> (BNat -> t -> t) -> (BNat -> t -> t) -> t
foldBNat n z t ti =
  case n of
    Z -> z
    T m -> t m (foldBNat m z t ti)
    TI m -> ti m (foldBNat m z t ti)

div2 :: BNat -> BNat
div2 n = foldBNat n Z (\m _ -> m) (\m _ -> m)

pred :: BNat -> BNat
pred n = foldBNat n Z (\_ r -> TI r) (\m _ -> T m)

succ :: BNat -> BNat
succ n = foldBNat n (TI Z) (\m _ -> TI m) (\_ r -> T r)

Answer 1

想法：要计算a + b，我们需要增加b a 倍。所以：

0 + b = b
1 + b = succ b
2 + b = succ (succ b)
3 + b = succ (succ (succ b))
...

我们可以从写作开始

plus a b = foldBNat a b (\m r -> ...

但是在这里我们卡住了：m 代表 a 的一半（因为这里的a = T m，即a = 2 * m）和r 是递增bm 倍的结果（即@987654333 @)。我们对此无能为力。我们想要的是a + b = 2*m + b，我们不能直接从m + b获得。应用T只会给我们2 * (m + b) = 2*m + 2*b，太大了，根据规则我们不能直接在plus上递归计算m + (m + b) = 2*m + b。

我们需要的是一种更直接的方法来操纵succ 操作的数量。

理念：不要直接计算数字；而是计算一个函数（将其参数增加一定次数）。所以：

incBy 0 = id
incBy 1 = succ
incBy 2 = succ . succ
incBy 3 = succ . succ . succ
...

我们可以直接实现：

incBy :: BNat -> (BNat -> BNat)
incBy n = foldBNat n id (\_ r -> r . r) (\_ r -> succ . r . r)

这里r . r 为我们提供了一个函数，它使数字递增的频率是r 的两倍（通过应用r 两次）。

现在我们可以简单地将加法定义为：

plus :: BNat -> BNat -> BNat
plus n m = (incBy n) m

（恰好是多余的，因为plus = incBy）。