I'm experimenting with optimizing reduction strategies for the untyped lambda calculus. Is there any (publicly available) dataset of (terminating) lambda terms I could use?

Maybe it would be possible to scrape code from commonly used programming languages and compile it down to LC...

Best, Paul Gustafson

P.S. Please let me know if there's a better forum for this question.

  • 2
    $\begingroup$ You could try to enumerate the $\lambda$-terms and see if that gets you anywhere. $\endgroup$ Jun 4, 2018 at 12:27
  • 1
    $\begingroup$ In a similar vein, here is a paper that shows how to enumerate (for a given $n$) the $SK$ combinators which normalize in exactly $n$ steps (for the normal-order reduction strategy): arxiv.org/abs/1603.01758 $\endgroup$
    – cody
    Jun 4, 2018 at 14:08
  • $\begingroup$ @AndrejBauer, thanks for the reference! I had seen this before since I've also worked with graphs on surfaces (in a physics context), but it was nice to look at it again. Unfortunately, I don't think the choice of reduction strategy really matters for linear lambda terms, but cody 's paper should remedy this. $\endgroup$ Jun 6, 2018 at 14:58


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.