<p>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?</p>

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

<p>Best,
Paul Gustafson</p>

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

CC BY-SA 4.0
2018-06-04T12:27:33.817Z
You could try to [enumerate the $\lambda$-terms](https://arxiv.org/pdf/1509.07596.pdf) and see if that gets you anywhere.
Andrej Bauer
CC BY-SA 4.0
2018-06-04T14:08:10.687Z
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): https://arxiv.org/abs/1603.01758
cody
CC BY-SA 4.0
2018-06-06T14:58:14.107Z
@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.
Paul Gustafson
<lambda-calculus><data-sets>
Is there any dataset of lambda terms?
Paul Gustafson
# Is there any dataset of lambda terms?

(Asked by: username_0 on 2018-06-02)

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,
username_0

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

**Tags:** lambda-calculus, data-sets

> **Comments:**
> **username_1**: You could try to [enumerate the $\lambda$-terms](https://arxiv.org/pdf/1509.07596.pdf) and see if that gets you anywhere.  
> **username_2**: 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): https://arxiv.org/abs/1603.01758  
> **username_0**: @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 username_2 's paper should remedy this.  

---

## 0 answers

