Lambda微积分表达式测试台？

我想测试一下Lambda微积分解释器，我已经写了一个相当大的Lambda微积分表达式测试集。有谁知道我可以使用的Lambda Calc表达式生成器（在Google上进行初始搜索时找不到任何内容）？这些表达式显然必须适当形成。更好的是，尽管我自己创建了各种示例并制定了解决方案，以便检查结果，但是有谁知道一个好的（和很大的）一套解决Lambda Calculus减少问题的方法吗？我可以自己输入表达式，所以更重要的是只要有一些简单的（和更大的）lambda微积分表达式，我可以测试我的解释器（目前模拟正常顺序和按名称调用评估策略）。Lambda微积分表达式测试台？

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

来源

2013-03-28 9codeMan9

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

是的，这确实很重要。谢谢！ – 9codeMan9

您是否阅读过[聊天]（http://chat.stackoverflow.com/rooms/25426/lambda-calculus）？ –

Asperti和圭里尼（1998年，函数式编程语言，银联新闻的最佳实现;尤其见第5,6章）介绍一些从redexes家庭的让 - 雅克·利维的理论出现的更痛苦的lambda项的并标记为减少：这些措施衡量了相互作用的复杂性，这些相互作用是在相互影响的β值降低之间进行的，在这种情况下，redex可以为另一个创建工作。

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

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

其中有两个β-redexes，并减少了(y y)：减少它们中的一个定期替换和您将创建两个新的redexes，每个与原始术语中的一个结构有关。

迭代Church数是在以相同的方式好：

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

（这减少了65 536教会标记），在生成大量碰撞redexes的。

通常，相互应用更高阶的术语，无论它们是“良好类型的”还是明显的意义，都是生成复杂中间结构的努力工作的良好来源。

来源

2013-05-02 07:44:23

你的第二个例子是错误的。它应该评估教会的数字为65536. – mk12

@ mk12：确实如此。我会解决我的答案。 –

Lambda微积分表达式测试台？

回答

相关问题