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

Question

在lambda演算中我没有看到任何二进制数字的提及.教会数字是一元制.我在Haskell问了一个如何做到这一点的问题:如何在Haskell 中实现二进制数 但是即使在我看到并理解了这个答案后,我也无法理解如何在纯粹的无类型lambda演算中做到这一点.

所以这是我的问题:二进制数字是否在无类型lambda演算中定义,并且还为它们定义了后继函数和前导函数？

Answer 1

递归数据类型的教会编码正是它的折叠(catamorphism).在我们冒险进入Church编码数据类型的凌乱且不易阅读的世界之前,我们将在前一个答案中给出的表示中实现这两个函数.而且因为我们想轻易转移到教会编码的变体,我们必须通过折叠来做.

这是前一个答案的表示(我选择了一个更易于使用的答案)和它的变形:

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)

现在,我们必须弄清楚教会编码.在我们开始之前,我们需要教会编码的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

现在,在开始时我说教会编码的数据类型是它的折叠.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)

Answer 2

下面的论文回答了你的问题。如您所见，已经研究了几种在 lambda 演算中对二进制数字进行编码的方法。

纯 Lambda 演算 Torben AE 中紧凑有效数表示的研究。摩根森 http://link.springer.com/content/pdf/10.1007%2F3-540-45575-2_20

抽象的。我们认为，与 den Hoed 提出并由 Goldberg 研究的左关联二进制数表示相比，紧凑的右关联二进制数表示提供了更简单的运算符和更好的效率。然后将这种表示推广到更高的数字基数，并且有人认为 3 到 5 之间的基数可以提供比二进制表示更高的效率。