3
$\begingroup$

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.

| cite | improve this question | |
$\endgroup$
  • 2
    $\begingroup$ You could try to enumerate the $\lambda$-terms and see if that gets you anywhere. $\endgroup$ – Andrej Bauer Jun 4 '18 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 '18 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$ – Paul Gustafson Jun 6 '18 at 14:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.