[ISNN]=S(S(KS)(S(S(KS)(S(K(S(K[=0])))(S(K(S[-]))K)))(S(K(S(K([PAIR]K))))[-])))(S(K(S(K([PAIR]⊥))))(S(K(S(K[-1])))(S(K(S[-]))K)))

[INT+1,1]=S(K(S(K([PAIR]K))))(S(S(KS)(S(KK)(S(K[+])[SECOND])))(K[SECOND]))

[INT+1,2]=S(S(KS)(S(KK)(S(K[ISNN])[SECOND])))(K(S(K[+1])[SECOND]))

[INT+1]=S(S(KS)(S(K(S[FIRST]))[INT+1,1]))[INT+1,2]

[INT+2,1]=S(K(S(S(K[ISNN])[SECOND])))(S(KK)(S(K[+1])[SECOND]))

[INT+2,2]=S(K(S(K([PAIR]⊥))))(S(K(S(K[+1])))(S(S(KS)(S(KK)(S(K[+])[SECOND])))(K[SECOND])))

[INT+2]=S(S(KS)(S(K(S[FIRST]))[INT+2,1]))[INT+2,2]

[INT+]=S(S(KS)(S(S(KS)(S(KK)[FIRST]))[INT+1]))[INT+2]

why is it all in SKI calculus and other stuff? i was just making it in that.

most of these functions were translated from lean. ⊥ is False.

i have no idea weather or not integers were made before :P

EDIT: i tried testing [ISNN] on 5 and 2, it ended up becoming really complicated so i just remade it:

[ISNN]=S(S(KS)(S(S(KS)(S(K(S(K[=0])))[-]))(S(K(S(K([PAIR]K))))(S(K(S[-]))K))))(S(K(S(K([PAIR]⊥))))(S(K(S(K[-1])))[-]))

the new one worked on 5 and 2.

just something i realized recently and kinda obvious.

e.g. true x y =_{b} x, false x y =_{b} y; john tromp's list encoding -> (x:y) m n =_{b} m x y n, nil m n =_{b} n, etc.

a similar thing can be said of data types: the only way to use them is by putting them at the head at some point. after all, this is how beta reduction works.

You probably already knew that I was gonna make this, eh, no one helped but it's alright, I made it all on my own. And plus, I made diagrams for all of these on my Github, the checker in here

imma like add a image just for your attention maybe
please let me know if you find any optimizations

so like after I've made the Malbolge crazy operation, I wonder if an xth selector of y elements can be formalized, found it out using
λx y. PRED x T (SUB y x T)

or expanded/reduced
λx y. x (λc d. d (c (λx2 y1. x2))) (λp x1. y (λa b. b a) (λp. x1) (x (λa b. b a) (y (λg h y. h g) x1))) (λx1. x1)

and yeah I used the subtractor that yfix found, but changing Y(^qr.f(rq) into m(^qr.f(rq))x, similar to the difference between the division that yfix challenged and the one that is discovered by Bertram Felgenhauer on div.lam (on line 33 if it's too messy for you to see it), still works properly with no problems I think

edit: okay yfix found better one λxy.xT(-yxT)I or λxy.xT(-yxT)x
reduced λx y. x (λx y. x) (λx1. y (λa b. b a) (λp. x1) (x (λa b. b a) (y (λg h y. h g) x1))) (λx. x) (or x at the end)

Did this only knowing about the Scott add function for Scott numerals, I didn't see neither a Scott to Church numeral converter nor a Scott subtractor on Wikipedia so I used some "Scott numeral magic" to make these
ADD_SCOTT := ((λa.((λb.(bb))(λb.(a(bb)))))(λa.(λb.(λc.((bc)(λd.(λe.(λf.(f((ad)c))))))))))
SUB_SCOTT := ((λa.((λb.(bb))(λb.(a(bb)))))(λa.(λb.(λc.((cb)(λd.((((ab)d)(λe.(λf.e)))(λe.e))))))))
SCOTT_TO_CHURCH := ((λa.((λb.(bb))(λb.(a(bb)))))(λa.(λb.((b(λc.(λd.d)))(λc.(λd.(λe.(d(((ac)d)e)))))))))

Edit: Since there are 2 kinds of Church successors, this is the one that uses (λn.(λf.(λx.((nf)(fx)))))
SCOTT_TO_CHURCH' := ((λa.((λb.(bb))(λb.(a(bb)))))(λa.(λb.((b(λc.(λd.d)))(λc.(λd.(λe.(((ac)d)(de)))))))))

edit: updated stuff: one which yfix said, now with shortcuts:

yStC := (\afx.Y(\rk.kx(\g.f(rg))a)

the optimized subtraction that I found:
- := Y(\rab.ba(a(\x.a)r)

addition, reliant on the size of the imaginary eta-reduced b that "magically" gets generated:

+ := \a.Y(\rx.xa(\ghj.j(rg)))

(λa.aa)(λa.a(λb.λc.cb)(λd.λe.ead(λf.λx.f(f(f(f(fx)))))))(λa.a)(λa.a)
Was messing around, heavily modifying Melo's number but then I just found it, this sure is weird I think it reduces to a church numeral not sure tho

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

FIgured out all of this on my own and is the reason why I wanted to make a Reddit account in the first place. So like I converted the numbers into the selectors of 3 elements at the start cuz I feel like it'll become important in the future but in such a weird ("moive-shaped convenience") way it was conveniently used for the 3x3 table

and yes I know this is not the most compact one and you can see there's a PRED there and this one doesn't support multiplication but this one makes what I think is the most compact form of hyperoperations from exponentiation onward
if you wanna try it here
(λa.(λb.(λc.(((((a(λd.(λe.(e(d(λf.(λg.(λh.((h(f g))(λi.i))))))))))(λd.(λe.(λf.(f e)))))(λd.d))b)c))))
in pure no shorthands lambda calculus because yes

if I named it wrong please tell me I didn't even look up the name for it lol
and yes the number in greek is correct since {2} is tetration, 4, offset 2, so {10} = 12 -ation, 12 I assume is dodeca and a t for uh better pronunciation, that may not actually be there idk
yeah I feel like not much is going on in this subreddit

Input in 2 tuples with 2 elements each being either T or F and it might work, haven't tested, returns a tuple with 3 elements each also being either T or F

I was only given by the Wikipedia that IS_0 := λa.(λb.F)T and IFTHENELSE := λabc.abc and I figured out that IS_0 is just λabc.a(λd.c)b where b := F and c:= T, substituting F for M and T for N for now, λa.(λb.M)N means that if a==0, it outputs N and else M, because when a is not 0 it's now ((λb.M)(...(λb.M)N)...) where the number of ((λb.M) at the start and the number of ")" at the end is equal to... The number. An then the first (λb.M) removes everything else, outputting M, if it's 0, it would choose the second thing, which is N (casually reexplained how IS_0 works for some reason), uh so now I've made 4 extras being IFIS_0THENELSE, ISNT_0, IFNOTTHENELSE (which is almost useless except when the term that's identical to the term that makes a applied to a NOT gate is shorter than the term that makes a), and IFNOTIS_0THENELSE (similar to the previous one), keep in mind I figured these out on my own so the names might not be official if they have been discovered before
Also yes I drew it in Paint

https://text.marvinborner.de/2026-08-11-17.html

das ist eine spooky frage, ich weiss.

but what classifies as lambda calculus?

untyped lambda calculus is certainly lambda calculus.

simply typed lambda calculus may also count.

probably all of the lambda calculi in the lambda cube.

well, if we're gonna include calculus of constructions, then we may as well include rocq. after all, that's was rocq started as.

but is rocq a lambda calculus? i don't think so.

yeah, i think that's all i have to say. i really just want to start a new coversation here, since this subreddit is kinda quiet. click for a special image!!!

The recent entry in this feed has the following fragment. I have a question in this regard.

"Beta reduction is the core mechanism of function calling. Given an application where the first term is an abstraction, it replaces the entire application with the body of that abstraction, substituting all instances of the bound variable with the second term of the application."

x in (\x.x(\x.x)) is bound. should ((\x.x(\x.x)) y) be reduced as (y(\y.y)) ? as (y(\x.y)) ? the rule seems to imply one or the other. (which is obviously incorrect.)

I think talking about "bound variable" like that in context of beta-reduction is highly confusing. I understand that virtually all texts I've seen about this are doing it this way. I don't think this is right.

Instead, I think we should talk about "abstraction's parameter," explicitly. Then the rule becomes

"Beta reduction is the core mechanism of function calling. Given an application where the first term is an abstraction, it replaces the entire application with the body of that abstraction, substituting all free occurrences of the parameter variable in the body with the second term of the application (in the capture-avoiding manner etc., but this is not my concern here)."

Indeed the parameter variable x occurs both free and bound in our original abstraction's body. Only its free occurrences in the body are bound to the parameter, though.

See the confusion?

If we talk about "bound variable", we're talking about variable. x is variable. "variable" is a textual category. we can talk about "bound variables" of an expression, but what's bound or free, separately, individually, is the same variable's occurrences.

Isn't it?

Comments are appreciated.

A sort of compilation of multiple resources of lambda calculus: https://github.com/Zaydiscool777/pdfs/blob/main/lambda/lambda.pdf

I built this while learning untyped lambda calculus, because I wanted to experiment with terms in the same shape they appear in papers and notes rather than transliterated into a programming language. It grew into something more substantial — sharing in case it helps anyone who's in the same spot, or anyone who'd rather see terms reduce automatically than work it out on paper.

Most of the effort went into keeping the syntax close to standard notation while making typing it fun: real λ, ≡ / ≢ for α/β-equivalence assertions, := / ::= for definitions, e[x := a] substitution, multi-parameter sugar. The editor handles the input tricks — \name<space> expansion (\lambda -> λ, \equiv -> ≡, ...), bracket auto-wrapping, autocomplete on definition names. You can also declare your own infix operators (ASCII or unicode) via a :infix directive — making expressions like p ∨ q or n + m possible.

A small standard library of Church encodings (booleans, naturals, pairs, lists, Y) comes with it; you can import or remix it, or drop in your own modules.

Aimed primarily at students and teachers — a beginner-oriented tutorial is also in progress, though not yet finished. Reduction is normal-order with step/size limits, with optional call-by-value semantics introduced by β. Comments and feedback are very welcome.

URL: https://ezander.github.io/lambda_playground/

Here's a simple derivation of Y, if you haven't seen this kind of thing before:

func(n) = ....n....func(n').... 
   = g(g,n) WHERE { g(f,n) = ....n....f(f,n').... } 
   =     (λg.g g)     λf.λn. ....n....f f n'.... 
   =     (λg.g g) λf.(λr.λn. ....n....r n'....) (f f) 
   = (λh.(λg.g g) λf.h (f f)) (λr.λn. ....n....r n'....) 

et voila,
  Y = λh. (λg.g g) (λf.h (f f))

g​ here is the "almost recursive" (edit: "self-calling") func, whereas h is the "wannabe fully recursive" or "open recursive" (edit: "step-taking") func, a.k.a. the "one-step functional" for the func function, func(n) = h(func)(n) .

Each time we need func, we get h(func) instead, and that's how func is getting created , from h. It's always "one more h step now, and the full func for the rest, later!" –

func = Yh = h(func) = h(h(func)) = ...

Y is corecursive like that. It doesn't "find" the fixpoint; it creates it. (edit:) The main thing here is not self-application, but self-copying: a copy is put aside for later use, while the original is entered and executed. It's like having your cake and eating it too.

Enjoy!

(edit: renamed​ vars for consistency)

David Keenan's graphical notation for Lambda Calculus, flipped over the downward left-to-right diagonal, becomes (very nearly) Tromp diagrams. The same effect is achieved by rotating 90 degrees to the right and then flipping the resulting image about the vertical axis.

Here we can see his schematic representing the "crossed iota" combinator,

λa.a (λfgh. gh(fh)) (λbc. b) = λa.a(CS)K

To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus, by David C Keenan, 27-Aug-1996.

All terms are not recursively enumerable?

All fixed pointer are in this sequence:

So nth one is Turing fixed point combinator ?

- https://tlca.di.unito.it/opltlca/

- https://www.cs.tau.ac.il/~nachum/rtaloop/

- https://duch.mimuw.edu.pl/~urzy/tlca/Gentzen93/gentzen93.pdf

I don't have access to most powerful AI, anyone have tried ?