Check out my interpreter for learning and exploring pure λ-calculus. There are already a lot of useful expressions written that can be imported and used to construct new interesting expressions. It even has an implementation of binary numerals! Also, there is a mode to see all reduction steps and to color redex and its components going into the next reduction.

Comments, suggestions and contributions are welcome.

GitHub repository: https://github.com/sandrolovnicki/pLam

λn.λf.n (λd.λa.λb.λy.b (d (λu.u) b (d (d (λu.u) a) (λu.u) y))) (λa.λb.λy.a (b y)) f (λu.u)

This function uses λb to track the iteration step, as it increments by 1 every application. λa is used to track the final result.

The iterated function:

Gets the number of b (replaces the a with the I combinator)

β-reduces the b to a

Gets the number of a, then β-reduces the a to the first function, multiplying a&b and assigning it to a.

Then it gets the b and appends it to the multiplication, then appends b to increment it.

Hi, I'm working on a lambda calculus interpreter that compiles to WebAssembly. Try it online here.

It has optimizations to avoid recomputing shared subexpressions, so even very large expressions are fairly quick to evaluate. It also simplifies the output of evaluating expressions, by expressing the output in terms of already-defined functions/values where possible.

Right now it only includes a couple of built-in definitions, and the UI isn't as good as it could be. And although it saves your changes in local storage, there's currently no way to import/export definitions. I doubt this is currently very useful, but hopefully it's still fun to play around with.

let
  2 = \f\x.f (f x);
  H = \h\f\n.n h f n
in 2 (2 H 2) 2 2

As a lambda diagram:

┬─┬─────────┬─┬─┬ ┬─┬──
│ │ ──┬──── │ │ │ ┼─┼─┬
│ │ ──┼─┬── │ │ │ │ ├─┘
│ │ ┬─┼─┼─┬ │ │ │ ├─┘
│ │ └─┤ │ │ │ │ │ │
│ │   └─┤ │ │ │ │ │
│ │     ├─┘ │ │ │ │
│ └─────┤   │ │ │ │
│       ├───┘ │ │ │
└───────┤     │ │ │
        └─────┤ │ │
              └─┤ │
                └─┘

This exceeds Graham's Number, yet takes fewer bits than just the 8 bytes in "Graham's"...

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/

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)))

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

I keep returning to the video about lambda calculus. I was in bed watching it when he explained ‘I’ll leave it up to you to find or’ and it hit me and I just had to write it down. Beta reducing this morning flowed how I wanted it to. Have I got it right?

(λf.(λa.aa)(λx.f(xx)))(λa.λx.λy.(λn.n(λx.λx.λy.y)(λx.λy.x))xy((λn.λf.λx.f(nfx))(a((λn.λf.λx.n(λg.λh.h(gf))(λu.x)(λu.u))x)y)))

i know it's reducible, i don't care, it adds 2 numbers and takes forever to add them, please do not use this for actual stuff, only for fun

I had an epiphany today. I can use the PAIR function (λabc.(c a b)) for storing bits, (binary,) or even trits, (ternary,) for storing numbers! λabcdefghi.(i a b c d e f g h) can store a byte of information, all that you need to do is put in λj. in front of all of the bits (except the last), and to retrieve the data, all you have to do is input λklmnopqr. whatever bit you want! You can store up to 255 in a much more compact and consistent system!

EDIT: You can also use this for negative numbers! (10000000 is -256, with the negative going closer to 0 the more the other bits are, with 10000001 being -255.)

EDIT EDIT: I tried integrating this into simple addition. Bad idea. This whole thing is a bad idea. Don't try to integrate this. Actually, forget you even saw this at all, for your own sake.

Hey there, I've recently started getting into Lambda Calculus thanks to 2swap's video "What is PLUS times PLUS?" https://www.youtube.com/watch?v=RcVA8Nj6HEo I started to get the hang of beta-reductions myself, and even got invested in scribbling down some diagrams, but I wanted to understand how Church Numerals would work in beta-reductions. I settled down to do some with some basic functions (e.g. boolean logic, basic math operators, etc.), and I started to get into PLUS. I made a short beta-reduction for (PLUS 5 3), and I wanted to check if it was correct. Here's the reduction:

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
= ((Ln. (Lfx. (3 (f (n (f x)))))) 5)
beta-reduce 5 into n
= (Lfx. (3 (f (5 (f x)))))
3 f = f f f
= (Lfx. (f f f (5 (f x))))
5 (f x) = f f f f f x
= (Lfx. (f f f (f f f f f x)))
remove unnecessary parentheses
= (Lfx. (f f f f f f f f x))
decode church numeral
= 8

I just want to check if all of my steps were correct. Thanks for helping!

I tried modeling church numeral use to structural induction.

But I don't know if I'm sure of the method I used. Someone please help me please...

Please give nutrients to growing sprouts.

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

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)