我还没有看到在 lambda 演算中提到二进制数字。教会数字是一元系统。我在这里问了一个关于如何在 Haskell 中执行此操作的问题：How to implement Binary numbers in Haskell 但即使在我看到并理解了这个答案之后，我仍然无法理解如何在纯无类型的 lambda 演算中执行此操作。
所以这是我的问题：是否在无类型 lambda 演算中定义了二进制数字，并且是否也为它们定义了后继函数和前驱函数？
问问题
1914 次
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 回答