Lambda Calculus Expression Test-bed?

Question

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.

Answer 1

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 65 536), 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.