testing - Lambda Calculus Expression Test-bed?

I would like to test out the Lambda Calculus interpreter that I've written against a fairly large test set of Lambda Calculus expressions. Does anyone know of a Lambda Calc expression generator I can use (couldn't find anything upon an initial search on Google)? These expressions would obviously have to be properly formed.

Better yet, while I have created various examples myself and worked out the solutions so I could check the results, does anyone know of a good (and large) set of worked out Lambda Calculus reduction problems with solutions? I can type in the expressions myself so it's more important to just have a good variety of simpler (and larger) lambda calculus expressions upon which I can test my interpreter (which at the moment models Normal Order and Call by Name evaluation strategies).

Any help or guidance would be greatly appreciated.

Asperti and Guerrini (1998, The 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 redexes and labelled reduction: these give measures of the complexity of interactions between colliding beta reductions, where reducing either redex creates work for the other.

A relatively simple example of colliding reductions is:

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

which has two beta-redexes and reduces to `(y y)`: reduce either one of them by regular substitution and you will create two new redexes, each of which is related to a piece of structure in the original term.

Iterating Church numerals is good in the same way:

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

(which reduces the Church numeral for 32), which generates a lot of colliding redexes.

Generally, applying higher-order terms to each other, regardless of whether they are "well-typed" or make obvious sense, is a good source of hard work that generates complex intermediate structure.