λ-Calculus (Lambda)

---

---

Section 0: Introduction

As Wikipedia puts it “In mathematical logic, the lambda calculus (also written as λ-calculus) is a formal system for expressing computation based on function abstraction and application using variable binding and substitution. Untyped lambda calculus, the topic of this article, is a universal machine, i.e. a model of computation that can be used to simulate any Turing machine (and vice versa). It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics. In 1936, Church found a formulation which was logically consistent, and documented it in 1940.” (https://en.wikipedia.org/wiki/Lambda_calculus)

Blah blah blah. Alonzo Church created a Turing-complete computational system (before Alan Turing btw; also way cooler than TMs btw). This page should hopefully explain λ-Calculus in a simple, understandable way–using my own notation.

Before anything, I should mention that I got introduced to λ-Calculus from this video https://www.youtube.com/watch?v=RcVA8Nj6HEo&t by 2Swap. (2Swap if you ever read this, I love you bro.) I have had no formal teaching on λ-Calculus and most of my knowledge comes from various sources on the internet.

My notation differs slightly from the standard, but I believe mine’s much clearer than the current standard (especially for beginners) so the entire article is written in it. Don’t worry though! I cover how to read and write current standard notation at the end. My notation–the Jimmanual Standard Notation (JSN)–was developed entirely by me sometime around October of 2025.

---

Section 1: Fundamental Building Blocks

First, we learn the three fundamental building blocks of λ-Calculus,

1. Variables – x, y, z, a, b, c, α, β, θ, etc. Just a symbol that represents something. Don’t want to go too far in depth on these, most people know what a variable is. These are read just as the name of the variable. (eg. “x” is read “x”).
2. Functions – (λ_._) A function is made up of parenthesis, Lambda (λ) to notate the start of the function, the first blank (_), a separator–a period or “dot”–(.), and the second blank (_). It is important to note that the first blank of a function is the only special blank in λ, as it can ONLY be filled with a variable, whereas all other blanks can be filled with any fundamental building block. Thus, the second blank can take in any building block, including other functions. It is extremely important to note that these are not functions in the algebraic sense (like x²), they are much more akin to programming functions. Functions are read “[the] function of _ do _” (eg. (λa.b) is read “[the] function of a do b”). Also, the first blank of the function is called the parameter, and the second blank is called the body. For example, in the earlier function (λa.b), a is the parameter and b is the body.
3. Applications – [_ _] An application is made up of square brackets and two blanks. Each blank can be filled with any fundamental building blocks, including other applications. These are read “apply _ to _” or “[the] application onto _ of/with _” (eg. [a b] is read “apply a to b” or “[the] application onto b of/with a]”).

Now, before we get into what any of this actually means or how to use it, let’s just do some practice writing lambda terms.

Try to guess which of the following is NOT a proper lambda term: 1. (λa.[a a]) 2. [a (λa.(λb.a))] 3. (λ(λa.a).a) 4. [(λb.a) (λa.b)]

If you guessed 3. ((λ(λa.a).a)), you would be right! A function’s first blank can only hold a variable, not a function or an application! All of the other terms are valid expressions and some might even show up later in the article 😉

Now, see if you can see what’s wrong with this term: [(λa.(λ.a)) c]

If you said that the second (inner) function is missing a variable in its first blank, you’d be right again! Each blank MUST be filled for a lambda expression to be valid. (eg. we can’t have like “[ b ]” or “(λa.)”).

I hope that’s enough practice cause I can’t think of anything else. Perhaps you could try just creating some terms of your own–on paper I would recommend.

---

Section 2: Jimmanual Large Diagrams (JLDs)

Now we still have one more (completely optional) thing to discuss before we start actually learning λ-Calculus: Jimmanual’s Large Diagrams (JLDs)! Yay! (These were created for and serve as simply a visual learning tool; the useful diagrams–JSDs–will come closer to the end of the article.)

JLDs are an extension of the JSN: an application is represented by a rectangle (like the square bracket), a function is represented by a circle/oval (like the parenthesis), and variables are just dots with lines connecting them to the function they originate from. Below are some “random” examples of JLDs with the JSN above.

I hope these gave a pretty good view of how JLDs work and how to construct them from JSN. These will not see much use in this article as they’re really just used for a visual explanation of λ-calc. I couldn’t find a way to make these work in this non-video format, so if you wish to see more on JLDs, just check out the videos… Now, we can finally explain what functions are/do and what applications are/do!!

---

Applications apply functions to things. Applications can apply functions to anything–variables, applications, or other functions–but applications can only apply functions. In other words, applications apply if and only if there is a function in the left part of the application. Or in other other words: for an application [a b], the application can only be applied if a is a function (whereas b can be any term). [(λa.a) b], [(λa.a) [b c]], and [(λa.a) (λx.x)] are all applications that can be applied while [a b] and [[a b] c] are not (but are still valid terms). I should also mention at this point “applying” is formally called β-Reduction (Beta-reduction) and when you have applied something you have β-reduced it. Also, when there is nothing left to apply–to β-reduce–then it is said to be completely β-reduced.

But what actually is applying? What does an application do? Well, when applying to a function, we take the body of the function, and replace every instance of the variable in the definition of the body with what we are applying to the function. Hmm. Not sure how to write that more comprehensibly. Basically, for some application [a b] we first check if a is a function. In this case, let’s say a is (λc.d) so the application is [(λc.d) b]. Since a is a function, we can apply this application. For our case, let’s say d is c, so the function is (λc.c) and the application is [(λc.c) b]. Then, we isolate the body of the function–c–save this elsewhere; this will replace the application term. Then, we look at the parameter of the function–c–and take the right term of the application and replace all instances of the definition (c) within the body of the function (c) with this term. So the body is entirely replaced with b. So, in conclusion [(λc.c) b] β-Reduces to b. Make sense yet? No? Sorry. Hopefully some practice will help. Also the video probably helps a lot more, so maybe check that out.

β-Reduce [b (λa.a)]

Did you say “b”? If so.. WRONG!! This term is the application of b onto the function of a do a. In other words, you are not applying a function to something else, so it can not be applied. In other other words: [b (λa.a)] does not β-reduce; The term is already completely β-reduced.

β-Reduce [(λa.c) b]

Did you say “b” again? Wrong again… The body is c and the parameter is a, so when replacing all instances of a within the body, there is nothing to replace with the right application term–b–and therefore all instances of the parameter have been replaced, so the term β-reduces to “c”.

β-Reduce [(λa.[a a]) b]

There is a function on the left of the application, so we can apply it. The parameter of the function is a, the body is [a a], and the term we’re applying this function to is b, so we replace all of the instances of the parameter–a–in the body–[a a]–with the term we’re applying to–b–to get [b b]. So [(λa.[a a]) b] β-Reduces to [b b].

β-Reduce (λa.[(λb.b) a])

Well, the outside term isn’t an application, so perhaps we can’t β-Reduce? However, there is still an application with a function being applied, so this term can be β-Reduced. In this term–[(λb.b) a]–the parameter is b, the body is b, and the term applied to is a. We take the body–b–and replace all instances of the parameter–b–in the body with the term applied to–a. So b is replaced with a so the term β-Reduces to b. However, this is a term inside a term, so we reintroduce the context to get (λa.[(λb.b) a]) β-Reduces to (λa.a).

β-Reduce [(λa.[b a]) [c c]]

Application of function: ✓. Parameter: a, Body: [b a], Term-Being-Applied to: [c c]. Replace all parameters–a–in body–[b a]–with term being applied to–[c c]–to get [b [c c]]. So in conclusion, [(λa.[b a]) [c c]] β-reduces to [b [c c]].

β-Reduce [[(λa.(λb.b)) c] d]

Look here! This application has an application on the left! We can’t apply an application, we can only apply functions! So this can’t be β-reduced, right? Well… look closer. That inner application–[(λa.(λb.b)) c]–has a function on the left, meaning it can be applied. Let’s apply it. Parameter: a, Body: (λb.b), Term-Being-Applied-To: c. So, we replace all the a’s in the body–(λb.b)–with c to get (λb.b) because there are no a’s to replace. Then, we sub this back into the larger term to get [(λb.b) d]. So, [[(λa.(λb.b)) c] d] β-reduces to [(λb.b) d]. But look! We can β-reduce again now! Let’s do this. Parameter: b, body: b, other term: d, fully β-reduced: d. So, [[(λa.(λb.b)) c] d] β-reduces to [(λb.b) d] which in turn β-reduces to d. In other words, [[(λa.(λb.b)) c] d] completely β-reduces to d.

Those should give a pretty good understanding of functions, applications, and applying/β-reduction. If you’re still struggling, consider watching Lecture 1 Part 1. The ones below are just fun bonus and explanations are not given.

β-Reduce [[(λa.(λb.a)) c] d]

c.

β-Reduce [(λa.[[a a] [a a]]) (λa.a)]

(λa.a) — I hope this one made you giggle like it did for me.

β-Reduce [(λa.[[a (λb.(λc.c))] (λb.(λc.b))]) (λa.(λb.a))]

(λb.(λc.c)) — This one is kinda a doozy. Later you’ll learn easier ways to write and β-reduce these.

---

Now we move on to currying. Currying is just a simpler way to write expressions. Basically, for a function (λa.(λb.c)), we combine the definitions into a single definition, making a multi-variable function (λab.c). So, to curry a function with another function as its body, you just combine the definitions into one. So for something like (λa.(λb.(λc.[a [b c]]))) curries as (λabc.[a [b c]]). However, something like (λa.[b (λc.d)]) is not curry-able, because there is no function in the body of a function.

Applications can also be curried. These are rather simple as it’s just [[a b] c] curries to [a b c]. Try some practice, now.

Curry (λa.(λb.[a [(λc.(λd.d)) b]]))

First, the outer functions curry to (λab.[a [(λc.(λd.d)) b]]). Then, the inner functions curry to (λab.[a [(λcd.d) b]]). This is now completely curried. Note here, we can not curry the applications into a single [a (λcd.d) b] because that implies (λcd.d) is applied to a and then b is applied to that. Or in other words, [a (λcd.d) b] un-curries to [[a (λcd.d)] b], not [a [(λcd.d) b]].

Curry (λa.[[a a] [a a]])

This curries to (λa.[a a [a a]])

UN-curry (λab.[a b [b a b]])

This un-curries to (λa.(λb.[[a b] [[b a] b]]))

UN-curry [(λa.[a (λbc.c) (λbc.b)]) (λab.a)]

[(λa.[[a (λb.(λc.c))] (λb.(λc.b))]) (λa.(λb.a))]. Do you recognize it? I used it as a bonus question just a moment ago. You could also just say this un-curries into (λb.(λc.c)) as this is it what it β-Reduces to. Fun.

I’m having trouble thinking of more practice for basic currying, so instead let’s try β-reducing some curried terms. For some curried application [(λab.c) d e], β-reduction is done by matching the first term being applied to (so the middle application term; d in our case) with the first parameter–a–and the right term being applied to (so the rightmost application term; e in our case) with the second parameter–b–and replacing each instance of each parameter in the body–c–with the term it’s connected to.

However, there are times when the number of terms being applied to does not match the number of parameters of the applying function. For example take [(λa.b) c d]. In this case, you just match as many terms that are being applied to with their parameters as possibly and β-reduce it as if it was one curried application. Also, only remove the application when there are no terms left to apply to. So for [(λa.b) c d] we would mentally (or maybe physically) rewrite it as [[(λa.b) c] d] and β-reduce to [b d]. These β-reductions usually take more than one step. For example, consider [(λa.[a a]) (λb.b) c]. The first β-reduction brings it to [[(λb.b) (λb.b)] c] (which can be curried to [(λb.b ) (λb.b) c], if you wish) which β-reduces again to [(λb.b) c] which finally completely β-reduces to c. Practice time!

β-Reduce [(λab.a) c d]

c

β-Reduce [(λab.b) c d]

d

β-Reduce (λab.[(λcd.[a d]) b])

(λabd.[a d]). Is this one confusing? It’s (λab.[(λcd.[a d]) b]) -> (λab.(λd.[a d])) and then you just curry it to the (λabd.[a d]).

β-Reduce [(λab.[b a [a b]]) (λa.a) (λab.a)]

(λa.a)

β-Reduce [(λabcd.[a b c [b d a]]) (λabc.c) (λab.a) (λa.[a a])]

(λd.d)

If someone reminds me, I might put more examples and also add explanations for the examples already there.

---

---

Read that word up there… booleans! Yay! If you don’t know what boolean logic is it’s just logic in terms of binary: true and false; it’s like how computers operate. In λ-Calculus, these booleans are called Church Booleans. Here they are:

1. (λab.a) — TRUE (T) (S_f)
2. (λab.b) — FALSE (F) (S_s)

I think I’ll explain this section with my story of when I was learning λ. See, when I was doing my self studying I came across these definitions for the church booleans and I was quite confused. (I mean I was also confused on most of the language, because I couldn’t find any good resources.) In fact, I wasn’t just confused–I was angry! I said that “these are not the proper names for these functions! All they do is take in two variables and either return [β-reduce to] the first or second input!” And so I renamed them, “(λab.a) just selects the first input! It’s the first selector–S_f! And this other one, (λab.b) just selects the second input! It’s the second selector–S_s!”

Well yes, Jim, this is true; those are what the functions do. However, there is certainly merit in labeling these functions as booleans. My favorite thing to show is how they interact when you apply them TO the church booleans. So for True it would be [(λab.a) (λab.a) (λab.b)] which β-reduces to (λab.a) which is True. Hmm interesting. What about false. [(λab.b) (λab.a) (λab.b)] -> (λab.b) which is False… Interesting. So when applying the two bools to one of the bools, it returns the bool that was applied. Now past Jim would probably say, here, something like “Okay but you’re just manipulating the fact that they select the first or second input; if the order was different then they’d select the opposite bool!” And, well, he would be right. These are sort-of arbitrary definitions and other definitions can be explored. This is why I have kept–and still use–the S_f and S_s names for (λab.a) and (λab.b). However, choosing these as our TRUE and FALSE makes a lot of emergent logic simple and easy.

Speaking of, let’s get into Boolean Operators: Logic Gates! Supposedly, you only need a NOR (or NAND) gate to build an entire computer and (spoiler alert) we can construct that in λ. Oh and btw what are logic gates? They’re just a device that performs a logical operation on booleans–things like NOT which would take in True and return False or take in False and return True. Speaking of, let’s try to construct that.

So we need a function that takes in one input (either T or F) and returns T or F based on its input. so the function will be in the simple form (λa.b). What will this b term be though? If the input (a) is T, then the function should β-reduce to F and if the input is F, then vice-versa. Well, if we look at Jim’s definition of the boolean functions, we might get some insight. TRUE selects the first input applied to it and FALSE selects the second. We have to remember that these are functions–we can apply them to things! So our NOT function should probably be in the form (λa.[a b c]). Well what are b and c? Hmm… if a is True, then it will select the first input–b–so b has to be False! and if a is False, then it will select the second input–c–so c has to be True! So our NOT operator is (λa.[a F T])! Let’s try this out [(λa.[a F T]) T] -> [T F T] -> [(λab.a) F T] -> F & [(λa.[a F T]) F] -> [F F T] -> [(λab.b) F T] -> T. It works! You have successfully constructed your first λ-calculus boolean operator!

Now, you are going to construct the AND logic gate. This function should beta reduce to true only when taking the inputs TRUE and TRUE, all other boolean combination inputs should return false.

Hint 1

Here is the truth table for the AND gate, this may help.

Hint 2

The function should take a similar form to the NOT gate: (λab.[a c d]). Note: Technically that first term could be either a or b, but for simplest case we just say a.

Hint 3

Let’s just say this first term is a. Looking at the truth table, we can see whenever this a term is false, the output is also false. Considering that false always selects the second of its inputs, if a was false, it would select d, so we need d to be FALSE.

Hint 4

Then, we notice that when a is true, the output is b–whatever the second input is. So, since TRUE selects the first input–c for our case–c must be whatever the second variable is–b.

Answer

AND is (λab.[a b F]).

There is one thing to note here: since we want F when a is false, we could have also made d be a for the function (λab.[a b a]).
Test one of these with all 4 2-digit binary inputs yourself if you want some β-reduction practice. (FF, FT, TF, TT)

Don’t worry if you didn’t get that one, I know how confusing λ-calculus can be. Try to see how far you can get in constructing OR now. Follow the steps we took to construct AND.

Hint 1

Here’s the truth table:

Hint 2

This should be the same form as AND: (λab.[a c d])

Hint 3

We can see that if a is true, then the function will return true. Considering that a chooses the first input–in our case c–so c must be TRUE

Hint 4

Then, we see that if a is false, the output is whatever the second variable–b–is so d should be b.

Answer

(λab.[a T b])

Similar to AND, we could’ve also concluded the c term to be a for the function (λab.[a a b])

From just those (technically didn’t even need all three), you can already construct all of the other logic gates and therefore… anything! In fact let’s see how. Construct NOR using these three logic gates (AND, NOT, and OR)

NOR

(λab.[NOT [OR a b]]) — Can you see how we’re applying NOT to the application of OR to the inputs? It’s literally NOT OR -> NOR.

Similarly, construct NAND.

NAND

(λab.[NOT [AND a b]])

The astute among you may have realized that if we expand the inner logic gates, we can β-reduce the function. However, doing so makes it less readable, so I refrain. If you want some practice, try writing them in their completely β-reduced forms. If you want even more practice, try writing their β-reduced forms in completely un-curried, raw λ-calculus versions. You can do that for the earlier three logic gates too. Oh also construct XOR; I almost forgot about that one.

NOR

(λab.[NOT [OR a b]]) -> (λab.[(λc.[c F T]) [(λcd.[c T d]) a b]]) -> (λab.[(λc.[c F T]) [a T b]]) -> (λab.[[a T b] F T]) -> (λab.[a T b F T]) which then can be turned into the raw form of (λa.(λb.[[[[a (λc.(λd.c))] b] (λc.(λd.d))] (λc.(λd.c))]))

NAND

(λab.[NOT [AND a b]]) -> (λab.[(λc.[c F T]) [(λcd.[c d F]) a b]]) -> (λab.[(λc.[c F T]) [a b F]]) -> (λab.[[a b F] F T]) -> (λab.[a b F F T]) which is (λa.(λb.[[[[a b] (λc.(λd.d))] (λc.(λd.d))] (λc.(λd.c))]))

NOT

(λa.[a F T]) doesn’t β-reduce. Raw: (λa.[[a (λa.(λb.b))] (λa.(λb.a))])

OR

(λab.[a T b]) Raw: (λa.(λb.[[a (λc.(λd.c))] b]))

AND

(λab.[a b F]) Raw: (λa.(λb.[[a b] (λc.(λd.d))]))

XOR

(λab.[a [NOT b] b]) -> (λab.[a [b F T] b]) -> (λa.(λb.[[a [[b (λc.(λd.d))] (λc.(λd.c))]] b]))

XOR Hint 1

Truth Table:

XOR Hint 2

Should be the same form as AND and OR: (λab.[a c d]). Here’s the actual hint though: c or d or maybe both will be special; they wont just be the basic T or F or b.

XOR Hint 3

Notice, when a is False, the output is the second input–b–so d should be b.

XOR Hint 4

The c term is a bit more complicated. Notice, when a is true, the output is the opposite of b. Consider how we could do that… if only there was some function that returned the opposite of its boolean input…

XOR Hint 5

This function is NOT. The c term should be [NOT b]

For fear of making this section too long, I’m just going to stop here. If you’re really interested in boolean logic like this, go learn 𝜏-Calculus. But, even with just these logic gates, you can create almost anything you can imagine. Here, one more thing. Let’s create a function that takes in three bools and returns true if all three inputs are true.

All Three True Checker

There’s a couple ways to write this function already. Here’s what I came up with: (λabc.[AND a b c F]). Here’s another: (λabc.[AND [AND a b] c]) or similarly: (λabc.[AND a [AND b c]]). Another: (λabc.[a [b c F] F]) There are probably others, so if you don’t see yours here, don’t worry.

If you couldn’t before, hopefully you can now see how we can create anything with these. Again, check out 𝜏-Calculus for cooler booleans.

---

Now we get to look at another visual of λ-Calculus! JSDs are heavily inspired by Tromp Diagrams, but I found those unreadable, so I remade them–just like the λ-Calculus written notation, woah!

JSDs are drawn from the top-down. Functions are thin horizontal lines, applications are thick horizontal lines, and variables are thin vertical lines extending from the function they’re defined from. I think the best way to understand these is to just see them and draw your own.

See, first, the Identity function ɪ (λa.a),

Then, see FALSE (λab.b),

Notice: The function needs to have a new “function line” for every parameter as if its un-curried.

Construct TRUE (λab.a),

Now let’s show some applications.

Let’s do a random function, (λab.[b b a]),

Notice: Applications can stay curried.

Now, try to construct AND (λab.[a b F])

Notice: You can see FALSE nestled within; Interesting!

Let’s look at some β-reductions with JSDs now. Sadly, I don’t currently have a way to animate these (@2swap 👀), so you’re just gonna have to imagine how things move.

Let’s look at [M ɪ] or [(λa.[a a]) (λa.a)] — Click the arrows on the sides

Got it? You just replace the ends of the vertical lines with the right term and remove the horizontal function & application lines.

Let’s look at another. [AND T F] which is [(λab.[a b F]) (λab.a) (λab.b)]

Notice in this one, I applied parameter by parameter instead of all at once. This was not needed; This “animation” (slideshow) works perfectly well if you just look at every other “frame” (picture).

My ability to show the actual application is rather limited, so most of the work falls on your imagination at the moment. I think that’s all for now… I don’t really know what else to do. I might post some things with JSDs on my YouTube eventually, so keep a look out.

---

Another well-explored function definition/s involves representing numbers. In this system–Church Numerals–numbers are represented by how many times the first variable of a function is applied to the second variable in a two-variable function. Also, these variables are usually f and x. Hopefully this will make it more clear:

• 0 – (λfx.x)
• 1 – (λfx.[f x])
• 2 – (λfx.[f [f x]])
• 3 – (λfx.[f [f [f x]]])

Notice this fun thing, 0 is FALSE! Sadly though, TRUE does not similarly match 1.

Take a look at the JSDs for the first few integers,

They look sort of like tally marks–and if you think about it… that’s kinda what Church Numerals are.

Now just like with the bools, we can perform operators on these base functions. For numbers, these are things like the successor (SUCC) operator which just increases the number by one. There’s also all the obvious ones like addition, multiplication, subtraction, etc. Also, these operators usually use m and n for their variables.

Here’s a couple of the mathematical operators on Church Functions:

• (λnfx.[n f [f x]]) — Successor; SUCC — This one’s kinda weird to explain; the best way to see how it works is just applying it to some Church Numeral and watching how it works–so go try that. Basically, it takes in some church numeral and replaces the f input with f, so that stays the same, but is now defined from the function. Then it replaces x with [f x], so it adds another application to the numeral–therefore increasing it by one.
• (λmnfx.[m f [n f x]]) — Addition; ADD; + — Notice how for the second number–n–it feeds f into f and x into x, keeping it the same number, but changing the variables so they’re from the outer function. Then, with the first number–m–it feeds f in for f but then feeds in the second number as the x, sort of appending it to the end of the numeral. This increases the amount of times f is applied to x in m by n, therefore adding the two numbers. Again, maybe try just adding two numbers using this to see how it works.
• Addition Pt. 2… There’s another way! Now, before I show you this other function, I want to show you the pathway and reasoning to it, since it reveals an interesting, unique property of Church Numerals! First, let’s consider addition. Think of Kurt Gödel’s system (I’m not too familiar with it; I may misquote heavily.) In here, addition is defined by repeated addition. Like 2 + 3 would just be 2 + 1 + 1 + 1. This is also probably how you originally learned addition all the way back as a kid. “Start at one number and count up [successor] the number of times of the other number.” If only we had some function that applied a function to another function a certain number of times… hmm… wait a second… Yes! That’s it! That’s exactly what a Church Numeral is! If we just plug in the successor function for f then it applies SUCC the same number of times as the number’s value! And then if we plug in another number for x, SUCC gets applied to that plugged in number the number of times of the original number, therefore adding the two numbers together! See if you can come up with this addition function, defined by repeated succession. Here it is… (λmn.[m SUCC n])
• (λmnf.[m [n f]]) — Multiplication; MUL; *; × — This one is also not so easily explained and β-reducing some multiplication yourself would probably give the best understanding. In this function, we replace the second number’s–n’s–f variable with the outer function’s f. Then, we simply apply the first number–m–to the changed second number. This replaces all the f’s of the first number with the second number (that is now just a single variable function because it already has its f’s defined from outermost function). The result of this is some number–the value of m–of the second number applied to x and to each-other, such that in cascading pattern, they replace the x variable of the preceding number such that it combines the applications into one. In other words, this function duplicates n m times and then combines the n’s into a single application.
• (λmn.[m [ADD n] (λfx.x)]) — This is the repeated addition definition of multiplication. This function adds n–[ADD n]–to zero–(λfx.x)–m number of times.
• (λbn.[n b]) — Exponentiation; EXP; ^ — Notice that this is our first asymmetrical operator, as in b^n (bⁿ) is not the same as n^b (n^b). I think I’m done with the long explanations for now, as the best way to see how they work–and possibly how they were derived–is to try an example or two yourself (like I said twice already).
• (λbn.[n [MUL b] (λfx.[f x])]) — Exponentiation in repeated multiplication form. This function multiples one–(λfx.[f x])–by b–[MUL b]–n times.
• (λnfx.[n (λri.[i [r f]]) (λf.x) (λu.u)]) — Predecessor; PRED — There is no point offering an explanation for this one with the knowledge you have; it uses a pair trick and well I’m pretty sure I didn’t cover those? I can’t remember.
• (λmn.[n PRED m]) — Subtraction; -; SUBT(…? SUB? No… MINUS? Can’t be MIN…) — Notice how we just use repeated predecessor for subtraction? That is because without the predecessor, subtraction is quite complicated… too complicated. Also note that this is another asymmetrical function, in this form it is m – n.

This concludes the Church Numeral section. There’s a couple more things, but this is really all you need to know. Here’s some fun practice if you want:

Make a function that returns 5 times the number put in; 5a

(λa.[* 5 a]) or (λa.[MUL (λfx.[f [f [f [f [f x]]]]]) a])

Make a³ + b²

(λab.[+ [^ a 3] [^ b 2]]) or (λab.[ADD [EXP a (λfx.[f [f [f x]]])] [EXP b (λfx.[f [f x]])]])

Make (a + b)^2 – 3a + 2c

(λabc.[+ [- [^ [+ a b] 2] [* 3 a]] [* 2 c]]) or (λabc.[ADD [SUBT [EXP [ADD a b] (λfx.[f [f x]])] [MUL (λfx.[f [f [f x]]]) a]] [MUL (λfx.[f [f x]]) c]])

---

If you understood all of this… congratulations! λ-Calculus is confusing and you should genuinely be proud of yourself for getting this far. Now, don’t go and be a victim of the Dunning-Kruger Effect just yet though. There’s a whole other load of things within λ-Calculus that weren’t covered here. I mean, I didn’t even mention recursive functions or even pairs (although τ-Calculus is just better and cooler than pairs). This is all to say I hope walking through this article inspires you to learn more about λ-Calculus–to learn about every little thing within it!

That is sort-of in bad taste to say, though, because if you’ve strictly learned from me, you won’t be able to read or write the current standard notation… and therefore can’t learn from any other online resource… hmm. Perhaps I will give you a short lesson on the current standard notation real quick, then:

1. Variables: The same, don’t worry lol.
2. Functions (Abstractions): λa.b — sometimes written in parenthesis, like mine: (λa.b)
3. Applications: (a b) — See, isn’t this already dumb? Why would you use the same symbol? Whatever.
4. Here’s the main annoying part: When an application is the first thing in a function body, it is often omitted. Like (λa.[c d]) would be written as λa.c d. Annoying, no? So, for the number 2, one would write λfx.f (f x). Is that not just so, horribly, incredibly ugly? Here it is in JSN to wash your eyes: (λfx.[f [f x]]).
5. Now take the ISZERO function (something you can research!) in standard notation: λn.n (λx.FALSE) TRUE. And here it is in JSN: (λn.[n [(λx.FALSE)] TRUE]).

Maybe you’re seeing this now and you’re thinking that standard notation is better. I definitely don’t blame you, and I won’t tell you I hate you. I think at this point I should make it clear my distaste for current standard notation is mostly a joke–I do not actually mind it that much. However, the spaces and lack of encapsulating terms was annoying enough to me to use (make) a new notation. If you are on my side, maybe consider spreading my notation around ¯\_(ツ)_/¯.

Welp. That’s it from me. τ-Calculus is pretty cool; consider checking that out if you enjoyed this.

P.S. (Are we finally done? In review mode now!)