纯lambda微积分中的测序或延续传递

Question

我正在尝试解决下面的练习。 这里.

考虑以下数字表示。如何定义加法？

|0| = λx.x
|1| = λx.λx.x
 ...
|n + 1| = λx.|n|

后继运算符和前继运算符很容易定义:

Succ n = λx.n
Pred n = n (λx.x)

定义加法的"明显"解决方案是使用后继操作加上零的测试以及固定点组合器，类似 (Y F) 为 F 下面给出（运算符 如果 和布尔值定义如常）:

F = λf.(λm n. if (Is0 m) n (Succ (f (Pred m) n))

但定义 Is0 似乎不是微不足道的。问题是数字 |N| 消耗N+1个参数，N个参数被它简单地擦除。因此，如果我应用这样的功能，当数字变得清晰时，停止其应用似乎是合理的，例如不是身份。我想这是某种延续，但我无法想象如何在纯lambda-微积分中对其进行建模。也许有人知道任何可能有帮助的提示？

测序运算符还可以帮助定义添加。如果一个数字的应用 |米| 被延迟到一个数字 |n| 应用于 全部 它的参数，结果将是一个数字 |n+m|.也许在纯lambda-微积分中存在这种测序组合器的变体？

由练习的作者提供的答案使用非纯操作（即, IsProcedure,IsProcedure 它检查它的参数是否是一个函数）。

UPD,UPD: 在lambda-calculus中做一个CPS并不难（可以找到CBV的详细信息 这里).看来这还不足以解决问题。

UPD,UPD:如果我们有某种版本的 报价-eval 函数对于纯lambda-微积分，那么必须有一个函数 $eq$, ，它识别引用的lambda表达式是否为 句法上 平等，我们可以构造 Is0 使用 $eq$.但我对此表示怀疑 $eq$ 是可定义的。原因是"genericity引理"（Barendregt book，引理14.3.24）。如果我们能够在引用的lambda项上测试相等性，那么（$eq$ (报价 $\欧米茄$) (报价 $\lambda x.x$））会回来 $False$, ，而泛性暗示（$eq$ (报价 $\lambda x.x$) (报价 $\lambda x.x$））也会返回 $False$.这是否与构建的可能性相矛盾 报价 在纯lambda-微积分中？

Answer 1

我不认为你会在纯粹的lambda演算中找到你正在寻找的东西。关键是你说的这句话:

测序运算符还可以帮助定义添加。如果一个数字|m|的应用被延迟，直到一个数字/n/被应用到它的所有参数，..

Lambda演算的模型应该是这样的:

$ $U\聪u^U$ $

和点 这 这是每个语义值吗？ $u\在U$ 可能适用于某些东西。因此，谈论"应用于其所有的论点"是没有意义的。"在纯lambda演算中，没有任何价值不能应用于更多的参数。

我不知道一个模型/论点的手，这种自然的表示使得它不可能实现 IsZero, ，虽然一些思考它使它看起来不太可能。但是，如果它在纯lambda演算中是可能的，它必须在语义上有意义，而不是基于仅仅是语法的概念。

编辑:这是一个论点的草图。的定义 $\mathsf{IsZero}$ 必须最终减少像:

$ $\mathsf{iszero} ightsquigarrow^*n\overrightarrow v$ $

原因是应用于某些数量的值是lambda演算中实际区分数字的唯一机制。需要的是: $ $0\overrightarrow v=\mathsf{true}\\\mathsf{s}n\overrightarrow v=\mathsf{false}$ $ 然而，对于每 overr\overrightarrow v$ 情况就是这样: $ $|/\overrightarrow v|+k|\overrightarrow v=/k/$ $ （哪里 $/\overrightarrow v/$ 是长度的 overr\overrightarrow v$).但只有 $/1/=\mathsf{false}$ （如果这是所选择的公约）。在英语中，通过应用数字获得布尔值所需的术语数量没有限制。所以不可能有一个 overr\overrightarrow v$ 它满足所有数字的方程，因此 $\mathsf{IsZero}$ 无法定义。

Answer 2

在lambda-calculus中定义加法的最直接的方式是处理数字，好像它们是链接的列表，并将列表被连接。为此，有必要使用额外的变量来替换每个数字的外部变量，因此可以代替第一个数字的所得表达式的内变量的结果表达式。这产生以下表达式：

  λw.λx.λy.λz.w y (x y z)

.