在 lambda 演算中编码二进制数字

Question

我没有看到任何在 lambda 演算中提到二进制数字。教会数字是一元系统。 我在这里问了一个关于如何在 Haskell 中执行此操作的问题：How to implement Binary numbers in Haskell 但即使在我看到并理解了这个答案之后，我仍然无法理解如何在纯无类型的 lambda 演算中做到这一点。

所以这是我的问题： 无类型 lambda 演算中是否定义了二进制数字，是否也为它们定义了后继函数和前导函数？

Answer 1

以下论文回答了您的问题。如您所见，已经调查了 在 lambda 演算中编码二进制数字的几种方法。

关于紧凑和高效数字表示的研究 纯 Lambda 微积分 托本 AE。摩根森 http://link.springer.com/content/pdf/10.1007%2F3-540-45575-2_20

抽象。我们认为一个紧凑的右关联二进制数 表示比 由 den Hoed 和 戈德堡调查。然后将该表示推广到 更高的数基数，有人认为 3 到 5 之间的基数可以 比二进制表示的效率更高。

Answer 2

递归数据类型的教堂编码正是它的折叠（catamorphism）。在我们冒险进入 Church 编码数据类型的混乱且不易读的世界之前，我们将根据上一个答案中给出的表示来实现这两个函数。而且因为我们想轻松地转移到 Church 编码的变体，所以我们必须通过 fold 来完成这两项工作。

这是上一个答案的表示（我选择了一个更容易使用的表示）及其变态：

data Bin = LSB | Zero Bin | One Bin

foldBin :: (r -> r) -- ^ Zero case.
        -> (r -> r) -- ^ One  case.
        -> r        -- ^ LSB  case.
        -> Bin
        -> r
foldBin z o l = go
  where
    go LSB      = l
    go (Zero n) = z (go n)
    go (One  n) = o (go n)

suc 函数将最低有效位加一，并继续传播我们得到的进位。一旦进位被添加到Zero（我们得到One），我们就可以停止传播。如果我们到达最高位并且仍然有一个进位要传播，我们将添加新的最高位（这是apLast 辅助函数）：

suc :: Bin -> Bin
suc = apLast . foldBin
    (\(c, r) -> if c
        then (False, One r)
        else (False, Zero r))
    (\(c, r) -> if c
        then (True,  Zero r)
        else (False, One r))
    (True, LSB)
  where
    apLast (True,  r) = One r
    apLast (False, r) = r

pre 函数非常相似，除了 Boolean 现在告诉我们何时停止传播 -1：

pre :: Bin -> Bin
pre = removeZeros . snd . foldBin
    (\(c, r) -> if c
        then (True,  One r)
        else (False, Zero r))
    (\(c, r) -> if c
        then (False, Zero r)
        else (False, One r))
    (True, LSB)

这可能会产生一个前导零位的数字，我们可以很容易地将它们切断。 full 是任何给定时间的整数，part 是 full，没有任何前导零。

removeZeros :: Bin -> Bin
removeZeros = snd . foldBin
    (\(full, part) -> (Zero full, part))
    (\(full, part) -> (One full, One full))
    (LSB, LSB)

---

现在，我们必须弄清楚 Church 编码。在开始之前，我们需要 Church 编码的 Booleans 和 Pairs。注意以下代码需要RankNTypes 扩展。

newtype BoolC = BoolC { runBool :: forall r. r -> r -> r }

true :: BoolC
true = BoolC $ \t _ -> t

false :: BoolC
false = BoolC $ \_ f -> f

if' :: BoolC -> a -> a -> a
if' (BoolC f) x y = f x y


newtype PairC a b = PairC { runPair :: forall r. (a -> b -> r) -> r }

pair :: a -> b -> PairC a b
pair a b = PairC $ \f -> f a b

fst' :: PairC a b -> a
fst' (PairC f) = f $ \a _ -> a

snd' :: PairC a b -> b
snd' (PairC f) = f $ \_ b -> b

现在，一开始我说过数据类型的 Church 编码是它的折叠。 Bin 有以下折叠：

foldBin :: (r -> r) -- ^ Zero case.
        -> (r -> r) -- ^ One  case.
        -> r        -- ^ LSB  case.
        -> Bin
        -> r

给定一个b :: Bin 参数，一旦我们将foldBin 应用于它，我们就可以得到b 的精确表示形式。让我们编写一个单独的数据类型来保持整洁：

newtype BinC = BinC { runBin :: forall r. (r -> r) -> (r -> r) -> r -> r }

在这里您可以清楚地看到它是 foldBin 的类型，没有 Bin 参数。现在，一些辅助函数：

lsb :: BinC
lsb = BinC $ \_ _ l -> l

zero :: BinC -> BinC
zero (BinC f) = BinC $ \z o l -> z (f z o l)

one :: BinC -> BinC
one (BinC f) = BinC $ \z o l -> o (f z o l)

-- Just for convenience.
foldBinC :: (r -> r) -> (r -> r) -> r -> BinC -> r
foldBinC z o l (BinC f) = f z o l

我们现在可以用 BinC 几乎以 1:1 的对应关系重写之前的定义：

suc' :: BinC -> BinC
suc' = apLast . foldBinC
    (\f -> runPair f $ \c r -> if' c
        (pair false (one r))
        (pair false (zero r)))
    (\f -> runPair f $ \c r -> if' c
        (pair true (zero r))
        (pair false (one r)))
    (pair true lsb)
  where
    apLast f = runPair f $ \c r -> if' c
        (one r)
        r

pre' :: BinC -> BinC
pre' = removeZeros' . snd' . foldBinC
    (\f -> runPair f $ \c r -> if' c
        (pair true (one r))
        (pair false (zero r)))
    (\f -> runPair f $ \c r -> if' c
        (pair false (zero r))
        (pair false (one r)))
    (pair true lsb)

removeZeros' :: BinC -> BinC
removeZeros' = snd' . foldBinC
    (\f -> runPair f $ \full part -> pair (zero full) part)
    (\f -> runPair f $ \full part -> pair (one full) (one full))
    (pair lsb lsb)

唯一显着的区别是我们不能在对上进行模式匹配，所以我们必须使用：

runPair f $ \a b -> expr

代替：

case f of
    (a, b) -> expr

---

这里是转换函数和一些测试：

toBinC :: Bin -> BinC
toBinC = foldBin zero one lsb

toBin :: BinC -> Bin
toBin (BinC f) = f Zero One LSB

numbers :: [BinC]
numbers = take 100 $ iterate suc' lsb

-- [0 .. 99]
test1 :: [Int]
test1 = map (toInt . toBin) numbers

-- 0:[0 .. 98]
test2 :: [Int]
test2 = map (toInt . toBin . pre') numbers

-- replicate 100 0
test3 :: [Int]
test3 = map (toInt . toBin) . zipWith ($) (iterate (pre' .) id) $ numbers

---

这是用无类型 lambda 演算编写的代码：

lsb  =      λ _ _ l. l
zero = λ f. λ z o l. z (f z o l) 
one  = λ f. λ z o l. o (f z o l)   
foldBinC = λ z o l f. f z o l

true  = λ t _. t
false = λ _ f. f
if' = λ f x y. f x y

pair = λ a b f. f a b
fst' = λ f. f λ a _. a
snd' = λ f. f λ _ b. b

(∘) = λ f g x. f (g x)


removeZeros' = snd' ∘ foldBinC
    (λ f. f λ full part. pair (zero full) part)
    (λ f. f λ full part. pair (one full) (one full))
    (pair lsb lsb)

apLast = λ f. f λ c r. if' c (one r) r

suc' = apLast ∘ foldBinC
    (λ f. f λ c r. if' c
        (pair false (one r))
        (pair false (zero r)))
    (λ f. f λ c r. if' c
        (pair true (zero r))
        (pair false (one r)))
    (pair true lsb)

pre' = removeZeros' ∘ snd' ∘ foldBinC
    (λ f. f λ c r. if' c
        (pair true (one r))
        (pair false (zero r)))
    (λ f. f λ c r. if' c
        (pair false (zero r))
        (pair false (one r)))
    (pair true lsb)