<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,
Paul Gustafson

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 cody 's paper should remedy this.  

---

## 0 answers

