testing - Lambda 微积分表达式测试台？

Question

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

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

如有任何帮助或指导，我们将不胜感激。

Answer 1

Asperti 和 Guerrini(1998 年，The Optimal Implementation of Functional Programming Languages，CUP Press；尤其是第 5 章和第 6 章)描述了 Jean-Jacques Levy 理论中出现的一些更令人痛苦的 lambda 项redex 家族和标记还原:这些给出了碰撞 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，每个都与中的一个结构相关原始术语。

以同样的方式迭代教堂数字是好的:

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

(将教会数字减少为 65 536)，这会产生大量冲突的 redexes。

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