如何在 Racket 中应用 lambda 演算规则？答案

【问题标题】：How to apply lambda calculus rules in Racket?如何在 Racket 中应用 lambda 演算规则？
【发布时间】：2015-09-04 02:41:27
【问题描述】：

我正在尝试测试一些我使用 Racket 编写的 lambda 演算函数，但在测试用例上运气不佳。例如给定一个定义

; successor function
(define my_succ (λ (one)
                 (λ (two)
                   (λ (three)
                     (two ((one two) three))))))

我正在尝试将它应用到 1 2 3，期望 2 的继任者是 3 做

(((my_succ 1) 2) 3)

逻辑是因为 my_succ 是一个函数，它接受一个 arg 并将其传递给另一个接受一个 arg 的函数，该函数将它传递给第三个接受一个 arg 的函数。但我明白了

application: not a procedure;
 expected a procedure that can be applied to arguments
  given: 1
  arguments.:

我尝试了谷歌搜索并找到了很多规则代码，但没有应用这些规则的示例。我应该如何调用上面的后继函数来测试它？

【问题讨论】：

标签： racket lambda-calculus

【解决方案1】：

您正在混合两种完全不同的东西：Racket 中的 lambda 术语和函数。

在 Racket 中，您可以使用匿名函数，这些函数可以用 λ 表示法编写（如 (λ(x) (+ x 1)) 返回整数的后继，因此 ((λ(x) (+ x 1)) 1) 返回 2），
在Pure Lambda Calculus 中，您只有 lambda 项，它们以类似的符号书写，并且可以解释为函数。

在第二个域中，您没有像0, 1, 2, ... 这样的自然数，但您只有 lambda 项，并且可以这样表示数字。例如，如果你使用所谓的Church numerals，你用 lambda 术语 λf.λx.x 表示（技术术语encode）数字0，1 用λf.λx.f x， 2 和 λf.λx.f (f x) 等等。

所以，函数successor（对于用这种编码表示的数字）对应于一个术语，在 Racket 表示法中，是您编写的函数，但您不能将其应用于像 0、@987654335 这样的数字@ 等，但仅限于其他 lambda 表达式，也就是说你可以这样写：

(define zero (λ(f) (λ (x) x)))   ; this correspond to λf.λx.x

(successor zero)

Racket 中的结果是一个过程（会打印为：#<procedure>），但是如果你尝试测试你的结果是否正确，将它与1 的函数编码进行比较，你会发现有些奇怪.事实上：

(equal? (successor zero) (λ(f) (λ(x) (f x))))

产生#f，因为如果你比较Racket中的两个过程，你总是得到错误的（例如(equal? (λ(x)x) (λ(x)x))产生#f），除非你比较“相同”（在“相同存储单元”的意义上）值（(equal? zero zero) 给出#t）。这是因为，为了正确比较两个函数，您应该比较无限组的对（输入、输出）！

另一种可能性是将 lambda 项表示为 Racket 中的某种结构，因此您可以表示 Church 数字以及“正常”的 lambda 项，并定义一个函数 apply（或更好的 reduce）执行减少 lambda。

【讨论】：

【解决方案2】：

您正在尝试应用柯里化。

(define my_succ
  (lambda(x)(
     lambda(y)(
       lambda(z)(
              (f x y z)))))

(define (add x y z)
  (+  x y z))

((( (my_succ add)1)2)3)

在 DR Racket 中的实现：

【讨论】：