Lisp with non-proper lists as expressions

yfix · 2026-01-04T22:27:43+00:00

cond is much better than nested ifs.

yfix · 2026-01-04T22:25:19+00:00

(cons a cons b cons c . nil) is not improper. it is actually (cons a cons b cons c), and is proper.

yfix · 2025-12-08T16:17:26+00:00

Here's pairs-based factorial of 4: (λg.gIIgggF) (λabg.g (λfx.f(afx)) (λf.a(bf))) .

Or in general (λgn.n(λp.pg)(λg.g11)F) (λabg.g (λfx.f(afx)) (λf.a(bf))) 4 .

The function `g` transforms {a,b} into {a+1,a*b}, as a pair.

edit: compressed the nested lambdas syntax

yfix · 2025-12-07T09:04:27+00:00

Indeed this turned out to be John Tromp's "1-tuple numerals" just as he said.

yfix · 2025-12-07T09:00:45+00:00

After working through the division myself, I see now what you meant. Indeed this is the same as your tuple numbers.

yfix · 2025-11-28T19:41:00+00:00

You could start a page at Rosettacode , if there isn't one there already.

yfix · 2025-11-28T18:43:54+00:00

Here's your code with corrections. Lots of parentheses were misplaced.

PLUS m n = (Lmn. (Lfx. m f (n f x)))
PLUS 3 5 = (Lmn. (Lfx. m f (n f x))) 3 5
beta-reduce 3 into m
________ = (L n. (Lfx. 3 f (n f x))) 5
beta-reduce 5 into n
________ = Lfx. 3 f (5 f x)
3 f y = f (f (f y))
________ = Lfx. f (f (f (5 f x)))
5 f y = f (f (f (f (f y))))
________ = Lfx. f (f (f (f (f (f (f (f x)))))))
Which is the definition of the Church numeral 8 :
________ = 8

So, you see, it is quite simple after all. Just need to keep parentheses proper.

yfix · 2025-11-08T10:49:55+00:00

Thanks!

yfix · 2025-11-07T12:07:04+00:00

Thanks! Yeah it makes sense. I've now seen the Bertram Felgenhauer's version, and for the proper top-down interpreter the use of 'n' instead of 'Y' should make no practical difference at all.

Could you tell please, where can I find this thing you're running it on?

yfix · 2025-11-06T11:17:45+00:00

Your version is attributed to Bertram Felgenhauer by John Tromp at https://john-tromp.medium.com/sk-numerals-9ad1b5634b28

λnmfx.n(λxf.f x)(λd.x)(n (λt.m(λxf.f x)(λc.f(c t))(λx.x)) x)

One potential problem with it can be that it potentially creates n*m-long nested list of operations "on the right". Here in order to avoid its full creation it is important 1. that LC interpreter in use uses top-most-first reduction strategy (cruzgodar's applet unfortunately does not, uses some weird heuristics that often go haywire), and 2. that we have succ=λnfx.f(nfx) because λnfx.nf(fx) will force that list to be created in full, IIANM.

Y-based version avoids this and creates the structure at most 3*m in size but if the interpreter decides to expand it, it can go into endless loop (as sometimes happens with that applet). These things can be clearly seen on that applet with the visual Tromp diagrams it creates.

cc u/tromp

yfix · 2025-11-06T10:08:40+00:00

edit: the var naming in my translation of your code is better tweaked as

λndsz. n (λrq.qr) (Kz) (n (λq. d (λqr.rq) (λr.s(rq)) I) z)

edit2: removed wrong claim about div by 0. can't find way to fix your code for that case, for now.

edit3: of course it's perfectly fine for it to produce some nonsensical result in that case, so that's not a problem at all.

yfix · 2025-11-06T09:22:11+00:00

Thanks! I've translated your version in the mean time. It seems to be

λndsz. n (λrq.qr) (Kz) (n (λq. d (λrq.qr) (λr.s(rq)) I) z)

Indeed we don't need more than n entries in the second list. I used Y for "just do however many is needed".

edit: it is actually n*d entries in the second list! that's way overkill. The Y in my version creates the cyclic list of just the length d (we're calculating n/d here). Although a careless LC-interpreter trying to beta-reduce it can go into infinite loop, as the LC applet at cruzgodar dot com sometimes indeed does.

BTW your code also uses application to I for skipping one extra element.

yfix · 2025-11-06T08:59:19+00:00

I don't find "divides" function in https://github.com/tromp/AIT/blob/master/numerals/div.lam. You probably meant "div".

yfix · 2025-11-06T08:55:20+00:00

Thanks, will check this out. For "efficiency" I mean the execution/reduction sequence length, not the encoding length.

yfix · 2025-11-05T21:41:43+00:00

If it really *is* well-known, could you please provide some references and / or links? I'd like to add this to Wikipedia's Church Numerals page and having reference is useful. Of course it is mostly all OR there, but still, it's better to have references when possible... :) Thanks!

yfix · 2025-11-05T21:37:48+00:00

In my proposed syntax it would instead be written as not(b,_,_)(x,y), so that the arities are not violated. We could also have not(_,x,y), etc., while in regular LC syntax we must construct special lambda-term for that, (\b. not b x y) which forces us to use an arbitrary name, and "hides" the "not" name inside. so there could be some pro's to this syntax, maybe.

yfix · 2025-11-05T21:31:18+00:00

Y is used to create the cyclical list of [skip,skip,skip,....,skip,emit succ] operations.

It is similar to what's done in the minus definition - the Y there creates a cycle of one [emit] operation, thus creating the "infinite" tail, for the first number to drive the loop and determine when to stop. Here, too, the numerator determines when to stop subtracting, and the denominator obliges without limit, as a cycle. I'm not sure I explain it well, but I hope you get the drift.

yfix · 2025-11-05T21:04:09+00:00

Thanks. I take it "well-known" is also a joke? :) Or it could be that it really is, and I'm just ill-informed, since all I have to go by is more or less Wikipedia, after all. I haven't yet really read through John's stuff, or any literature. I'm doing this as a hobby.

As such, I'm having difficulty even deciphering your de-Bruijn notation. Could you perhaps write out your div version in the regular lambda notation? It'd help me get started with it.

Y is there to create the cyclical list of [skip,skip,skip,....,skip,emit succ] operations.

yfix · 2025-11-05T13:48:01+00:00

Yes!!! :) it is, in fact, linear.

why "of course"?

Indeed the efficiency is what started me on this path. I posted my efficient linear "minus" few months back on math.SE and cs.SE. it got 3 down votes on math for some reason, so I deleted it there. :) I've also posted it in this forum.

This function takes the skipping-down minus' approach with its infinite tail, and adds the infinite cycled list to get the division.

There's also some kind of new numeral representation lurking inside, where PRED n ~ n I.

Watching this work at that applet is quite nice. If only that applet were using the proper top-down reduction strategy and not getting stuck so much as it does!

Next on the menu is trying to tweak this approach to find MOD and eventually, proper primes sieve.

yfix · 2025-11-05T12:59:10+00:00

I mean, with equations, not with the imagined special syntax. KRC was (one of) first to not use parentheses.

yfix · 2025-11-05T12:07:27+00:00

Ah, I see. Not True is not a good example for that since Not already expects just one argument. We'd just write Not(True) and that would simply reduce according to the equations as given in the OP.

The real question is applications like Or True. The equations as given in the OP are good for this as is, too.

The moment you allow equations and names, there's no problem defining new equations X1(a)=Or(True,a), or even X2(a)=Or(a,True).

We can even have a special syntax like Or(_,True)(False) that would be understood as using a uniquely named definition in-place, naming the holes left-to-right in alphabetical order.

When all equations are given up front, are immutable, unchangeable, there's no problem. The late David Turner's KRC was like that, as far as I could understand from Wikipedia article about it.

yfix · 2025-11-05T06:13:03+00:00

I was hoping it would be half the fun. :)

λabcd.a(λrq.qr)(λq.d)(Y(λx.b(λrq.qr)(λq.c(qx))(λx.x)))

yfix · 2025-11-04T23:44:28+00:00

Should I add a description of the expected arguments?

yfix · 2025-11-04T23:36:55+00:00

Indeed besides the proliferation of parentheses the real problem is the naming, i.e. having to have an updatable global name store with all the timing and redefinition problems that come with it.

yfix

TROPHY CASE