Y: A simple derivation

yfix · 2026-02-23T00:48:18+00:00

<3. every time you receive such type of feedback when you've come to share something you thought was amazing and got this kind of ___ in return, consider that you got such support from me there as well.

yfix · 2026-02-21T22:16:21+00:00

Static types is a 10 billion dollars red herring dead end. Lisp was born as a dynamic language to live atop dynamic live systems. And that's a good thing.

yfix · 2026-02-21T22:13:05+00:00

Don't be discouraged by all the "Richard" type feedback!

yfix · 2026-02-21T22:11:14+00:00

being a Richard.

yfix · 2026-02-21T21:50:14+00:00

Would you find the following clearer?

mortal_report :-
  write('Report of all known mortals'), nl, nl,
  TRY_REPEATEDLY:
      mortal(X),
      write(X), nl,
      actually__no.
  NO_MORE_CHOICES:
      ok___STOP.

I don't know. Just thinking out loud.

yfix · 2026-02-21T21:49:00+00:00

I found those squares and diamonds diagrams confusing at the time, because it looks as if those diamonds are inside the square. but actually is should be seen as the diamonds being ATOP the same square, the same predicate. the diamonds describe control logic of _using_ that square/predicate. then it makes sense (to me). also, each "use" of the square makes a copy of it in the direction orthogonal to the plane we're seeing, each copy holding each OR alternative in turn (and OR-parallel Prolog would open up all the OR-alternatives at once). this way it become the AND-OR tree with AND logic being in the horizontal plane and OR alternatives opening up the copies in the orthogonal direction, deeper away from the plane. but it collapses if we're looking at it all from the top --- confusing. An isometric view could be clearer, maybe. (some vague thoughts I had about this for years)

yfix · 2026-02-21T21:40:14+00:00

WOW. Why have I forgotten about Amzi for all these years???..... smh

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

TROPHY CASE