6

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

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

4

2 回答 2

17

递归数据类型的 Church 编码正是它的折叠（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)
于 2013-08-23T12:54:58.770 回答
6

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

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

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

于 2013-08-24T00:01:44.090 回答