Lambda演算表达式测试平台？

Question

我想测试我编写的Lambda演算解释器，使用一组相当大的Lambda演算表达式进行测试。 有人知道我可以使用的Lambda Calc表达式生成器吗（在Google上的初始搜索中找不到任何内容）？ 这些表达式显然必须是正确形成的。

更好的是，虽然我自己创建了各种示例并解决了问题以便检查结果，但是否有一个包含解决方案的良好（且大量的）Lambda演算简化问题集？ 我可以自己输入表达式，因此更重要的是具有一组较简单（且较大）的Lambda演算表达式，以便我可以测试我的解释器（目前模拟正常顺序和按名称调用评估策略）。

非常感谢任何帮助或指导。

- 9codeMan9

---

这个有帮助吗？http://stackoverflow.com/a/15171626/1243762 和 http://cs.stackexchange.com/questions/9001/test-cases-for-calculus - Guy Coder

是的，这确实很有帮助。谢谢！ - 9codeMan9

你有没有读过聊天室的讨论？ - Guy Coder

再次感谢您！此外，您在聊天中的评论是关于Church-Rosser定理（http://en.wikipedia.org/wiki/Church%E2%80%93Rosser_theorem），该定理认为如果一个正常形式存在，那么一个约简方法将找到它。特别地，如果存在这样的正常形式，正则序将找到该正常形式。以防您好奇！再次感谢您的点赞。我将发布我如何设置我的评估测试平台的方式，该平台将利用您引用的工作台。 - 9codeMan9

感谢 Church-Rosser 定理。我知道它，但不确定能否在聊天中应用到问题上。现在我更自信地引用它了。你会公开你的代码吗？也许是在 GitHub 上？如果是这样，请在这里放一个链接，我很想看看另一个例子。 - Guy Coder

没问题！这是我在编译器研究中必须了解的定理。目前我不确定，但我一直在为教授开发解释器以供其课堂使用，因此是否可以公开发布取决于教授，但我没有任何理由不这样做。当然，解释器更专注于使用Lambda演算（宏、表达式、注释行等）编写程序，因此与您提到的工作台相比，它只有两种评估方法（我甚至不知道头脊还原哈哈）。 - 9codeMan9

Answer 1

Asperti和Guerrini（1998年，《函数式编程语言的最优实现》，CUP出版社；特别是第5章和第6章）描述了一些更痛苦的lambda术语，这些术语来自Jean-Jacques Levy的redex家族理论和标记约简：这些给出了相互碰撞的beta约简之间交互复杂性的度量，其中减少任何一个redex都会为另一个创建工作。

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

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

这段内容涉及到IT技术，它有两个beta-redexes，并且可以简化为(y y)。通过常规替代，你可以减少其中任何一个，从而创建两个新的redexes，每个redex都与原始术语的一个结构相关。

迭代Church数是相同的好处：

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

(它将65,536的Church数减少)，这将生成大量碰撞的redexes。

通常，无论高阶术语是否“良好类型化”或显而易见的意义，将它们应用于彼此都是一种艰苦工作的良好来源，会产生复杂的中间结构。

- Charles Stewart

---

你的第二个例子是错误的。它应该计算为65536的Church数。 - mk12

@mk12：非常正确。我会修正我的回答。 - Charles Stewart