Lambda 演算表达式测试平台？答案

【问题标题】：Lambda Calculus Expression Test-bed?Lambda 演算表达式测试平台？
【发布时间】：2013-03-28 19:51:46
【问题描述】：

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

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

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

【问题讨论】：

这有帮助吗？ stackoverflow.com/a/15171626/1243762 和 cs.stackexchange.com/questions/9001/test-cases-for-calculus
是的，确实如此，非常重要。谢谢！
你读过chat吗？
再次感谢您！此外，您对该聊天的评论是 Church-Rosser 定理 (en.wikipedia.org/wiki/Church%E2%80%93Rosser_theorem)，它假定如果存在法线，则减少方法会找到它。特别是，如果该范式存在，Normal Order 将找到该范式。以防你好奇！再次感谢您的支持。我将发布我最终如何设置我的评估测试平台，它将利用您引用的工作台。
感谢 Church-Rosser 定理。我知道这一点，但不确定我是否可以在聊天期间将其应用于问题。我现在觉得引用它更舒服。你打算公开你的代码吗？也许是 GitHub？如果是这样，请在此处放一个链接，我不介意再看一个例子。

标签： testing expression lambda-calculus

【解决方案1】：

Asperti 和 Guerrini（1998，函数式编程语言的最佳实现，CUP Press；特别参见第 5 章和第 6 章）描述了一些源自 Jean-Jacques Levy 理论的更痛苦的 lambda 术语redexs 和标记化归约的家族：这些衡量了碰撞 beta 归约之间相互作用的复杂性，其中减少任何一个 redex 都会为另一个 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)

（将 Church 数字减少为 65 536），这会产生大量冲突的 redexes。

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

【讨论】：

你的第二个例子是错误的。它应该评估为 65536 的教堂数字。
@mk12：确实如此。我会修正我的答案。