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.

Coster

Does this help? https://mcmap.net/q/1917074/-is-my-lambda-calculus-grammar-unambiguous and cs.stackexchange.com/questions/9001/test-cases-for-calculus – Fumatorium

Yes, this does, a great deal. Thank you! – Coster

Did you read the chat? – Fumatorium

Thank you yet again! Also, you're comment on that chat is the Church-Rosser Theorem (en.wikipedia.org/wiki/Church%E2%80%93Rosser_theorem), which posits that if a normal exists, a reduction method will find it. Particularly, Normal Order will find that normal form if that normal form exists. Just in case you were curious! Thanks again for the upvotes. I will post how I end up setting up for my evaluation test-bed, which will make use of that workbench you cite. – Coster

Thanks for the Church-Rosser Theorem. I knew about it but wasn't sure I could apply it to the question during the chat. I now feel more comfortable quoting it. Are you going to make your code public? Maybe GitHub? If so, drop a link here, I wouldn't mind seeing another example. – Fumatorium

No problem! It's a theorem I had to become acquainted with in my compiler research. I'm not sure at the moment, I may, but I have been developing the interpreter for a Professor to use in his class, so it will be up to the Professor if I can release it publicly, but I do not see any reason why not. Of course, the interpreter focuses more on writing programs in Lambda Calculus (macros, expressions, commented lines, etc.), so it will only have 2 evaluation methods as compared to the impressive set of reductions the workbench you point out has (I didn't even know about headspine reduction haha) – Coster

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.

Punchinello

Your second example is wrong. It should evaluate to the Church numeral for 65536. – Kingship

@mk12: Quite so. I shall fix my answer. – Punchinello