5

我想针对相当大的 Lambda Calculus 表达式测试集测试我编写的 Lambda Calculus 解释器。有谁知道我可以使用的 Lambda Calc 表达式生成器（在 Google 上进行初始搜索时找不到任何东西）？这些表达式显然必须正确形成。

更好的是，虽然我自己创建了各种示例并制定了解决方案，以便我可以检查结果，但有没有人知道一组好的（和大量的）已解决的 Lambda 微积分减少问题的解决方案？我可以自己输入表达式，因此更重要的是拥有多种更简单（和更大）的 lambda 演算表达式，我可以在这些表达式上测试我的解释器（目前模拟正常顺序和按名称调用评估策略）。

任何帮助或指导将不胜感激。

4

1 回答 1

2

Asperti 和 Guerrini (1998, The Optimal Implementation of Functional Programming Languages , CUP Press; 尤其参见第 5 章和第 6 章) 描述了一些来自 Jean-Jacques Levy 的 redexes 和标记归约理论的更痛苦的 lambda 项：这些给出衡量相互冲突的 beta 减少之间相互作用的复杂性，其中减少任何一个 redex 都会为另一个创造工作。

碰撞减少的一个相对简单的例子是：

let D =  λx(x x); F= λf.(f (f y)); and I= λx.x in
    (D  (F I))

它有两个 beta-redexes 并减少到(y y)：通过常规替换减少其中一个，您将创建两个新的 redexes，每个都与原始术语中的一个结构相关。

以同样的方式迭代 Church 数字也很好：

let T = λfx. f(f( x)) in 
    λfx.(T (T (T (T T))) f x)

（这减少了 65 536 的 Church 数字），这会产生很多冲突的 redexes。

通常，将高阶项相互应用，无论它们是否“类型良好”或是否具有明显意义，都是产生复杂中间结构的努力工作的良好来源。

于 2013-05-02T07:44:23.360 回答