encoding - Mogensen 二进制编码的继任者和前任存在问题

Question

我想将二进制数添加到我的无类型 lambda 演算库中，但我坚持使用 succ 和 pred 函数。我正在使用 paper by T. Mogensen 中概述的表示，虽然那里定义的大多数函数都可以工作，但 succ 和 pred 返回了错误的结果。

我很确定我的表示是正确的:

dec bin   De Bruijn       classic
0   0     λλλ3            λa.λb.λc.a
1   1     λλλ13           λa.λb.λc.c a
2   10    λλλ2(13)        λa.λb.λc.b (c a)
3   11    λλλ1(13)        λa.λb.λc.c (c a)
4   100   λλλ2(2(13))     λa.λb.λc.b (b (c a))
5   101   λλλ1(2(13))     λa.λb.λc.c (b (c a))
6   110   λλλ2(1(13))     λa.λb.λc.b (c (c a))
7   111   λλλ1(1(13))     λa.λb.λc.c (c (c a))
8   1000  λλλ2(2(2(13)))  λa.λb.λc.b (b (b (c a)))

元组和投影看起来也不错:

tuple         De Bruijn               classic
[T, F]        λ1(λλ2)(λλ1)            λa.a (λb.λc.b) (λb.λc.c)
[T, F, F]     λ1(λλ2)(λλ1)(λλ1)       λa.a (λb.λc.b) (λb.λc.c) (λb.λc.c)
[T, F, F, T]  λ1(λλ2)(λλ1)(λλ1)(λλ2)  λa.a (λb.λc.b) (λb.λc.c) (λb.λc.c) (λb.λc.b)

πkn  De Bruijn  classic
π12  λ1(λλ2)    λa.a (λb.λc.b)
π22  λ1(λλ1)    λa.a (λb.λc.c)

使用 0 位 ( shl0 ) 和 1 位 ( shl1 ) 上移在测试中效果很好:

SHL0 ≡ λnbzo.z (n b z o) = λ λ λ λ 2 (4 3 2 1)
SHL1 ≡ λnbzo.o (n b z o) = λ λ λ λ 1 (4 3 2 1)

但是依赖于上面列出的术语的 succ 和 pred 不:

SUCC ≡ λn.π22 (n Z A B) ≡ λ π22 (1 Z A B) where
Z ≡ [ZERO, ONE] // encoded like in the first piece of code
A ≡ λp.p (λnm.[SHL0 n, SHL1 n]) ≡ λ 1 (λ λ [SHL0 2, SHL1 2])
B ≡ λp.p (λnm.[SHL1 n, SHL0 m]) ≡ λ 1 (λ λ [SHL1 2, SHL0 1])

PRED ≡ λn.π22 (n Z A B) ≡ λ π22 (1 Z A B) where
Z ≡ [ZERO, ZERO] // encoded like in the first piece of code
A ≡ λp.p (λnm.[SHL0 n, SHL1 m]) ≡ λ 1 (λ λ [SHL0 2, SHL1 1])
B ≡ λp.p (λnm.[SHL1 n, SHL0 n]) ≡ λ 1 (λ λ [SHL1 2, SHL0 2])

结果示例:

succ 0 = λa.λb.λc.c a / λλλ13 ok
succ 1 = λa.λb.λc.b (b c) / λλλ2(21) wrong, expected λλλ2(13)
succ 2 = λa.λb.λc.c (b (c (λd.λe.λf.e (b d e f)) (λd.λe.λf.f (b d e f)))) / λλλ1(2(1(λλλ2(5321))(λλλ1(5321)))) wrong, expected λλλ1(13)
succ 3 = λa.λb.λc.b (b c) / λλλ2(21) wrong, expected λλλ2(2(13))

pred 1 = λa.λb.λc.b a / λλλ23 wrong-ish, expected λλλ3; it's just a leading zero, but it's stated that those should only be caused by inputs that are powers of 2
pred 2 = λa.λb.λc.c (b c) / λλλ1(21) wrong, expected λλλ13
pred 3 = λa.λb.λc.b (b a) / λλλ2(23) wrong, expected λλλ2(13)
pred 4 = λa.λb.λc.c (b c) / λλλ1(21) wrong, expected λλλ1(13)

我的术语评估器已经过数百个术语的测试，所以我对它非常有信心；我怀疑要么是我误读了某些东西，要么是打印错误。我错过了什么吗？

Answer 1

因此，正如 ljedrz 所提到的，我们设法让摩根森数字在单独的聊天中工作。在这个答案中，我将简要描述它的一般工作原理。

问题是:« 我怀疑要么是我误读了某些内容，要么是某些内容打印错误。我错过了什么吗？ »

tl;dr:结果是一些与评估顺序相关的棘手问题导致了问题。问题中提出的摩根森数字确实有效。

更长的答案:如何succ工作 ？

注意:在以下b_n始终假定为 1 ，就像在原始论文中一样。

摩根森数字背后的想法是有一个数字 n = b_n ... b_2 b_1编码为 \z.\x_0.\x_1. x_{b_1} ( x_{b_2} (... ( x_{b_n} z ) ...) ) .这是非常难以理解的，但如果这样说，它会变得更清楚:

A number n is a term which expects 3 arguments, and when applied, returns x_{b_1} ( x_{b_2} (... ( x_{b_n} z ) ...) )

嗯，这还不清楚。如果我们看得更深，我们会看到一个数字 n递归应用 x_0或 x_1 , 从词条 z 开始.请注意，递归调用是“从左到右”进行的，即，如果我有一个数字 b_n b_{n-1} ... b_2 b_1 ，然后按以下顺序评估递归调用:

第一 b_n z ，让它成为i_{n-1}

然后 b_{n-1} i_{n-1} ，让它成为i_{n-2}

...

最后是 i_1 b_1

(好吧，评估策略决定了确切的评估顺序，我认为很容易认为它是这样评估的)

与 fold 的关系列表中的函数

其实，当我意识到这一点时，我才想起 fold_left位列表的功能:假设您有一个位列表 l = [b_n; ... ; b_2; b_1] ，那么您可以执行以下操作:

fold_left (fun prev_acc -> fun b -> if b = 0 then x_0 prev_acc else x_1 prev_acc) z l

让 f是

fun prev_acc -> fun b -> if b = 0 then x_0 prev_acc else x_1 prev_acc

返回(根据 Ocaml doc )

f (f (... (f z b_n) ...) b_2) b_1

其评估为:

f z b_n计算结果为 x_{b_n} z ，即 i_{n-1}如上。

...

f i_{1} b_1 ， 如上。

结论，您绝对可以将摩根森数字视为 fold_left在列表中(或 fold_right ，取决于您对列表的想象)。

获取 succ一个数字

获取 succ一个数字正在获取 n+1 .二进制增量作为一个很好的属性:

if m = bn ... bi bj bk ... b1 with bj being the first 0 (i.e. bk = ... = b1 = 1), then m + 1 = bn ... bi 1 0 ... 0

这可以说明:

bn ... bi  0  1  1  1  1  1

如果我添加 1 ，然后我得到(通过详细说明所有步骤):

bn ... bi  0  1  1  1  1  1
                         +1
--------------------------
bn ... bi  0  1  1  1  1  0
                      +1     < I have a carry here, which gets propagated
...
--------------------------
bn ... bi  0  0  0  0  0  0
          +1                 < The carry ends up here
--------------------------
bn ... bi  1  0  0  0  0  0  < This is our result of doing a +1.

一个很好的注释是注意 (bn ... bi 0 1 ... 1) + 1是 (bn ... bi 0) + 1附加到 0 ... 0 ，更一般地说，它也适用于任何 bj : (bn ... bi bj 1 ... 1) + 1是 (bn ... bi bj) + 1附加到 0 ... 0 .

这看起来不错，只有一个问题，进位是从右到左传播的(LSB 到 MSB)，而摩根森数字是从 MSB 到 LSB。

为了解决最后一个问题，我们可以进行推测:假设我有一个数字 b_n ... bi bj bk ... b1 ，我想有它的继任者。我将不得不递归计算它，但只能从 MSB 到 LSB。

也就是说，如果我在“步骤 bj”，我只能使用子序列 bn ... bi和 bj本身。

例如，这允许我们计算 succ的 bn ... bi .现在是投机部分:

我知道，如果在 bj 之后，只有1 ，那么在前面的评论之后，那么继任者是((bn ... bi bj) + 1)::(0 ... 0)

但是，如果有 0在 bk ... b1 ，则位 (bn ... bi bj) 保持不变。

所以这个想法是在一个元组中返回每个位的两种可能性。非正式地，函数传递给 fold_left看起来像这样:

fun tuple_msb -> fun bj -> 
(original_msb, incr_msb)

其中 (1) tuple_msb是一个包含 (bn ... bi, (bn ... bi) + 1) 的元组;哪里 (2) original_msb和 incr_msb计算取决于 bj .的确:

如果 bj是 0 ，然后 (bn ... bi bj) + 1 = (bn ... bi 0) + 1 = (bn ... bi 1)

如果 bj是 1 ，然后 (bn ... bi bj) + 1 = (bn ... bi 1) + 1 = ((bn ... bi) + 1)::0 .

也就是传递给 fold_left的完整函数如下:

(* We keep the original sequence on the left of the tuple, the incremented `bn ... bi bj` on the right *)
fun tuple_msb -> fun bj ->
if bj = 0 then
  (tuple_msb._1 :: 0, tuple_msb._1 :: 1) 
else 
  (tuple_msb._1 :: 1, tuple_msb._2 :: 0) 

和基本情况(即起始元素是元组 (0, 1) )

从这里开始，很容易回到 Morgensen 不可读的术语(这里有一个关于参数顺序的隐藏的小捷径，但这真的无关紧要):

我们可以识别 fun tuple_msb -> (tuple_msb._1 :: 0, tuple._1 :: 1)作为 x_0和 fun tuple_msb -> (tuple_msb._1 :: 1, tuple_msb._2 :: 0)作为 x_1根据我们在开始时为 x_0 使用的符号和 x_1 ，和基本情况(即 z 开头是 (0, 1) )。

为了得到最终的后继者，我们必须得到返回元组的正确部分，因此最终的

let succ n =
  let ret_tuple = n z x_0 x_1 in
  ret_tuple._2

或在 lambda 术语中:

succ' = λn. π22 (n z x_0 x_1)

与所有 π22 , z , x_0和 x_1相应定义。

我们的 succ'与提议的 succ 有点不同，即 x_0不完全是 A和 x_1不完全是 B ，但这最后一步很简单，留给感兴趣的读者;-)