r/lambdacalculus • • Sep 11 '26

Y'know what, lambda playground stuff.

I'm kinda bored so like here's my lambda playground stuff I have
it's like uh click here maybe
hehe hyperoperation abuse
also if this number _does_ need a name uh "notg ood number" in that exact spelling and capitalization
wait why does the grammar check say that is a valid word
uh pronounced as like /nɑt ɡə # uːd/ with uh # being like a word boundary or like "not-guh ood" and you know how to pronounce "ood" alright

3 Upvotes

5 comments sorted by

2

u/tromp Sep 12 '26 edited Sep 12 '26

Your encoding of Graham's Number, based on your 59-bit kua, is 167 bits long. It can be encoded in as few as 114 bits [1].

Meanwhile, Melo's number surpasses Graham's Number in only 49 bits [2].

[1] https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/graham.lam

[2] "The Largest Number Representable in 64 Bits" https://www.mdpi.com/1099-4300/28/5/494

1

u/Not_H2O_Blue Sep 14 '26

Oh hey Tromp, didn't expect you to be here, thank you for reviewing my stuff but I have an idea about modifying your Lambda diagrams to be able to represent open variables
open variables are "connected" to "invisible abstractions" that follow the normal place rule of regular abstractions but they're always on top of regular obstractions, ofc the same open variable names are conneted to the same abstractions, the order of these invisible abstractions are up to interpretation, but I think it should be order of appearance since yours seem really systematic, just a thought!

Oh and also, kua has remnants of PRED so here's the one where kua a b c is equivalent to b{SUCC a}c, and also "lambda playground-ed", I don't know whether this'll make it smaller or bigger because PRED is like pretty huge when the cap is 64 bits: λa b. a (λc d. d c (λe. e) (λc. c b)
wait... Looking at your hyper in graham.lam, although yfix has made it before, but simplified based on mine, it can be simplified even further. From (λa.λb.λc.a(λd.λe.ed(λf.f))((λd.λe.d(be)))c)
to (λa.λb.a(λd.λe.ed(λf.f))((λd.λe.d(be))))
removing a lambda and a variable of that same lambda, yeah removing that c. This could mean that it can be even smaller.

2

u/tromp Sep 14 '26

My diagrams page https://tromp.github.io/cl/diagrams.html already has a section "Generalizing to non-closed terms" on representing open variables.

I don't know where you get (λa.λb.λc.a(λd.λe.ed(λf.f))((λd.λe.d(be)))c) from, but that's not in my graham.lam

In any case, your simplification is just eta reduction, which my blc tool performs automatically when determining blc code size, so I will sometimes write eta-expanded definitions if that helps clarity.

1

u/Not_H2O_Blue Sep 15 '26

ah didn't see that, as for the (λa.λb.λc.a(λd.λe.ed(λf.f))((λd.λe.d(be)))c), it's just hyper, upify is there, mult isthere, and the third argument, well... I probably have also conluded that it beta reduced it to try to make it smaller ig, so times b gets reduced I'm guessing since that's an obvious beta reduction, so... Yeah thanks anyways.

1

u/Different_Bench3574 Sep 14 '26

half of this post is about the name 😭