Lambda 微积分：构建一个在每次迭代中接受更多参数的函数

Question

我正在尝试构建一个函数，它接受给定数量的参数并且总是 return 相同的值。

这是作业的一部分。提供了提示：

The "k-way T" is a function that takes k arguments and always returns T. A "0-way T" is just T.

其中 k 作为教会数字提供，T 是 True (\x.\y.x) 的 lambda 表达式。

完整的任务是提供一个计算 k 向或函数的 lambda 表达式。其中 'boolean' 参数的数量在 'boolean' 参数之前提供。例如：

((OR 3) F T F)

但现在我正在尝试创建接受 k 个参数并且 returns 总是 T。 k 作为第一个参数提供。

((TRUE 2) T F) == T

所以基本上我不想创建一个函数，每个教堂数字都有一个参数 'iteration'。

但不知何故我完全卡住了。

我可以只用一个教堂数字吗？还是我需要递归（Y-Combinator）？

总的来说：是否有任何支持创建 lambda 表达式的好工具（例如用于可视化）。

我对 lambda 演算的强大功能感到非常惊讶，我真的很想学习它。但是我不知道怎么...

提前致谢

Answer 1

我将展示如何实现 TRUE 功能。由于 k 不是固定的，因此您需要一个定点组合器（Y 可以，但它不是唯一的定点组合器）。首先，关于我在下面使用的符号的几句话：iszero（接受一个 Church 数字，检查它是否为 Church 零和 returns 一个 Church 布尔值），T（ Church 编码的真布尔值）、pred（Church 数字的前导函数）和 Y（定点组合器）。

let TRUE = Y (λr. λn. (iszero n) T (λx. (r (pred n))))

请注意 let 不是 lambda 演算语法的一部分，它是引入名称的元语法（对我们来说）。

它的工作原理如下：Y 某种将 r 参数转换为 "self" -- 当一个函数调用 r 它自称。为了说明这一点，我将把上面的代码重写为递归形式（警告：它仅用于说明目的，lambda 演算 不允许 这个；因为所有函数都是匿名的，你可以'不要用他们的名字来称呼他们——这是没有办法的):

let TRUE = λn. (iszero n) T (λx. (TRUE (pred n)))

我去掉了 λr. 部分并用 TRUE 替换了 r （再次强调，请不要在你的家庭作业中这样做，它不是有效的 lambda 演算）。

而且这个定义更容易理解：如果TRUE这样调用TRUE 0它只是returnsT，否则它returns一个函数一个参数的一个参数，它环绕着 (n - 1) 个参数的函数，本质上代表了一个 n 个参数的函数。

至于你关于工具的问题：一种方法是使用 Scheme/Racket -- 这将有助于检查你的 "lambda calculus code" 是否正常运行。例如，这里是 TRUE 在 Racket 中的一个实现：

(define (Y f)
  ((lambda (x) (x x))
   (lambda (x) (lambda (a) ((f (x x)) a)))))

(define TRUE
  (Y (lambda (r)
       (lambda (n)
         (if (zero? n)
             #t
             (lambda (x) (r (sub1 n))))))))

;; tests
> (TRUE 0)
#t
> ((TRUE 1) #f)
#t
> (((TRUE 2) #f) #f)
#t
> ((((((TRUE 5) #f) #f) #f) #f) #f)
#t

我应该补充一点，我在这里使用了内置的布尔值、整数、if 表达式、sub1、zero? 而不是 Church 编码的。否则会使这个例子变得更大（或不完整）。

Answer 2

我现在也在做那个确切的作业，我只是想告诉你和任何未来的读者，这个绝对不需要定点组合器。

要从对 Pk:=(k-way T, k-way OR) 到对 Pk+1:=(k+1-way T, k+1-way OR，您只需应用函数 lambda Pk. (lambda a b c. c a b) (lambda arg. Pk (lambda x y. x)) (lambda arg. Pk arg).

简而言之，这个函数解构你的对并构造一个新的对，多吃一个参数。新的 k+1-way OR 只是来自 Pk 的 k-way OR（如果参数是 F）或 k-way T（如果参数是 T）。

既然您拥有此功能，您唯一需要做的就是将它应用 n 次到起始对 P0:=(lambda a b c. c a b) (lambda x y. x) (lambda x y. y)，您可以使用教堂数字 n 来完成。最后你只需要拿这对的第二部分，你应该留下一个 n-way OR.

Lambda 微积分：构建一个在每次迭代中接受更多参数的函数

Lambda Calculus: build a function that takes more arguments with each iteration

lambda-calculus