An experimental study of lambda expression?

Question

I would like to check out the Lambda Calculus interpreter, which I wrote against the rather large test suite of Lambda Calculus expressions. Does anyone know a Lambda Calc expression generator that I can use (could not find anything in the initial Google search)? Obviously, these expressions must be correctly formed.

Even better, although I myself have created various examples and developed solutions so that I can check the results, does anyone know of a good (and large) set of developed Lambda Calculus reduction problems with solutions? I can enter expressions myself, so it’s important to have a simple set of simpler (and larger) expressions of lambda calculus on which I can test my interpreter (which currently models the evaluation strategies “Normal Order” and “Call by Name”).

Any help or guidance is appreciated.

Answer 1

Asperti and Guerrini (1998, Optimal Implementation of Functional Programming Languages, CUP Press, see especially Chapters 5 and 6) describe some of the more painful lambda terms that arise from Jean-Jacques Levy's theory of families of rudiments and labeled reduction: they give measures of complexity interactions between colliding beta contractions, where a reduction or redex creates work for another.

A relatively simple example of colliding abbreviations:

let D = λx(xx); F= λf.(f (fy)); and I= λx.x in (D (FI)) 

which has two beta redefinitions and boils down to (yy) : reduces either one of them by regular substitution, and you will create two new redexes, each of which is associated with a part of the structure in the original terminal.

Church iterative numbers are equally good:

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

(which reduces the size of the Church to 65,536), which generates a lot of counter alterations.

As a rule, applying higher-order terms to each other, whether they are “typical” or have an obvious meaning, is a good source of hard work that generates a complex intermediate structure.