如何在球拍中应用lambda演算规则？

我想测试一下我使用Racket编写的lambda微积分函数，但没有太多运气与测试用例。例如，给定的定义如何在球拍中应用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.:

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

来源

2015-09-04 Urler

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

球拍，你可以有匿名函数，可以写在λ符号（如(λ(x) (+ x 1))返回一个整数的继任者，使((λ(x) (+ x 1)) 1)回报2）
在Pure Lambda Calculus你只有lambda项，用类似的符号书写，并且可以解释为功能。

在第二个领域，你没有自然数一样0, 1, 2, ...，但你只拉姆达条款，并表示数字本身。举例来说，如果你使用了所谓Church numerals，你代表（在技术术语编码）与拉姆达项λf.λx.x人数0，1与λf.λx.f x，2与λf.λx.f (f x)等。

因此，（这个编码代表了数字）功能successor对应于一个术语，在球拍符号，是你写的功能，但不能将其应用到数字像0，1等，但只给其他lambda表达式，那就是你可以写这样的事情：

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

(successor zero)

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

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

产生#f，因为如果你在拍比较两个程序，你得始终为假（如(equal? (λ(x)x) (λ(x)x))产生#f），除非你比较“相同”（在“同一个存储单元”的意义上）值（(equal? zero zero)给出#t）。这是因为，为了比较正确的两个函数，你应该比较无限组的夫妇（输入，输出）！

另一种可能性是将lambda术语表示为球拍中的某种结构，因此您可以表示教会数字以及“正常”lambda术语，并定义一个函数apply（或更好的reduce）执行lambda-reduction 。

来源

2015-09-04 06:02:03 Renzo

如何在球拍中应用lambda演算规则？

回答

相关问题