lambda-calculus - lambda 微积分 : build a function that takes more arguments with each iteration

Question

我正在尝试构建一个接受给定数量的参数并始终返回相同值的函数。

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

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 表达式。在“ bool ”参数之前提供“ bool ”参数的数量。例如:

((OR 3) F T F)

但现在我正在尝试创建接受 k 个参数并始终返回 T 的方法。 k 作为第一个参数提供。

((TRUE 2) T F) == T

所以基本上我不想为每个教会数字“迭代”创建一个具有多个参数的函数。

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

我可以只使用教堂数字吗？还是我需要递归(Y-Combinator)？

总的来说:是否有支持创建 lambda 表达式的好工具(例如用于可视化)。

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

提前致谢

Answer 1

我将展示如何实现 TRUE 函数。由于 k 不是固定的，因此您需要一个定点组合器(Y 可以，但它不是唯一的定点组合器)。首先是关于我在下面使用的符号的几句话:iszero(接受一个 Church 数字，检查它是否为 Church 零并返回一个 Church bool 值)，T (Church 编码的真 bool 值)、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. 部分并将 r 替换为 TRUE(再次强调，请不要在作业中这样做，它不是有效的 lambda 演算)。

而且这个定义更容易理解:如果像这样调用TRUE TRUE 0 它只返回T，否则返回一个函数一个参数的一个参数，它环绕着一个包含 (n - 1) 个参数的函数，本质上代表一个包含 n 个参数的函数。

关于您关于工具的问题:一种方法是使用 Scheme/Racket——这将有助于检查您的“lambda 演算代码”是否按预期运行。例如，这里是 Racket 中 TRUE 的实现:

(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

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