我想测试一下Lambda微积分解释器,我是用一个相当大的Lambda微积分表达式测试集编写的.有谁知道我可以使用的Lambda Calc表达式生成器(在Google上进行初始搜索时找不到任何内容)？这些表达式显然必须正确形成.

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

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

最佳答案 Asperti和Guerrini(1998年,功能编程语言的最佳实现,CUP出版社;特别参见第5章和第6章)描述了Jean-Jacques Levy的redex家族理论和标记简化的一些更痛苦的lambda术语：这些测量碰撞β减少之间的相互作用的复杂性,其中减少redex为另一个减少redex.

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

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

它有两个beta-redexes并缩减为(y y)：通过常规替换减少其中任何一个,你将创建两个新的redex,每个redex与原始术语中的一个结构相关.

迭代教会数字以同样的方式是好的：

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

(这减少了教堂数字为65 536),这会产生很多碰撞的重新索引.

通常,将高阶项相互应用,无论它们是“良好类型”还是明显有意义,都是产生复杂中间结构的艰苦工作的良好来源.