## (3,4):Church's Numbers
### Or: Formal Function Theory
0: Ok so in Church's system, everything is functions.
1: You've mentioned this already, but I still don't know what you mean.
0: How do you mean?
1: I mean if everything is functions, what do they take as inputs?
0: Functions.
1: What do they return as outputs?
0: Functions.
1: Zero?
0: What?
1: ... That's insane.
0: I know it feels that way at first. But it's not so bad once you implement numbers and booleans.
1: Sure sure, but WHY?
0: Why what?
1: Why do this at all?
0: Why are _we_ doing it?
1: No why was Church doing it? I want to know what was going on inside his head, or at least what might have been. What would make a person say "Yaי know what I'm gonna do today? Make a system where 0 and 1 are actually functions." Like that's not a normal behavior and it's not a natural way to think. So I'm curious what was going on in this guy's head that would make him do something like that.
0: Perfect question! Ok so, by the time Church is writing, formal theories had been a thing for a while.
1: "Formal theories" as in?...
0: Programming languages.
1: Oh?
0: Ones that run on paper.
1: Makes sense.
0: ZFC had already done formal set theory. PA had already done formal number theory. It's not unreasonable to think something like "Look guys, those theories you made are cute and all, but the foundations of mathematics or even reasoning itself shouldn't be just whole numbers or unordered collections. The foundations of mathematics should be something more primitive."
1: What's more primitive than those things?
0: Well there are infinitely many natural numbers. And that's not a problem in itself, but we'd like our foundations to be something inherently finite.
1: Inherently finite?
0: Inherently finite. I mean when a mathematician proves stuff about the natural numbers by induction, they do it with only a finite amount of time and food and paper and pencils and erasers and pants and money and everything. Finite everything.
1: Obviously. What's your point?
0: Foundations should be like that. I mean, it's fine that the natural numbers are infinite, but they're not finite in the same obvious way that the mathematician with the paper is finite and only doing finite stuff. If we truncate the natural numbers at any finite level and say "There are no natural numbers above ten million" or whatever, any mathematician would rightly feel like we'd done a violent ugly hack that made the natural numbers less of what they are. But there's no such feeling when a mathematician uses only finitely many pencils or finitely many sheets of paper. We have no problem with that, and we'd be disturbed if either was infinite. So in that sense natural numbers are way too big to be foundations.
1: What about sets? Sets can be finite.
0: True! But all versions of set theory that have ever been proposed as foundations are way more infinite than the whole numbers are. They tend to all include a sentence that says "ω exists."
1: You mean ω like Cantor's first size of infinity?
0: Well in this case it means "The set of natural numbers," but those are actually the same thing.
1: How are those the same thing?
0: Well no finite number is big enough to be the smallest infinite number. So the set of all natural numbers ends up being the same thing as "the smallest infinite number" in that system.
1: Numbers are sets?
0: Numbers are sets. At least in that system, where everything is sets. Anyways things are even worse in set theory than in number theory, because there tends to be another axiom that says "If a set X exists, then so does P(X), the set of all its subsets." And that P(X) thing turns out to always be a bigger size than X is, even if X is infinite. So any formal theory that had these two things together grows an infinite number of different sizes of infinity, each larger than the next.
1: I remember. So what was Church thinking?
0: Well taking together both the fact that (i) the natural numbers have an inherent inability to be made finite without it feeling like an ugly hack, and (ii) set theory has such a wildly irresponsibly number of infinite things that it's not clear how it got invited to the foundations party... taking those two things together, you might end up thinking what Church was thinking.
1: _(Narrative voice)_ "So what was Church thinking?, 1 asked yet again."
0: That we need a "Formal Theory of X" for some better X than just X = numbers and X = sets.
It should be something fundamentally finite.
Maybe there's infinitely many Xs, whatever this not-yet-mentioned X type thing is, but it should be possible to _make_ the theory only about finitely many objects made of inherently finite stuff, and finitely many operations on those things. We should be able to "finitize" the theory without it feeling like an awful hack in the way it would be if we said 1 million is the largest natural number.
1: "Without it feeling like"?
0: Yeah, what's the problem?
1: You seem to be suggesting that Church wanted something finite, but his foundation for wanting that was "feelings."
0: Of course! I mean I never knew Church personally, but that's a totally normal way to think when you're doing mathematics.
1: The more you talk about math, the less I understand what it really is.
0: Good. That means you're listening. So anyways if you thought all the thoughts above, you might end up doing what Church did, so let's do our best to get inside his head.
We're looking for some type of X where we can build a "Formal Theory of X" that doesn't feel fundamentally broken if we don't have infinitely many of them, or if the guts of each one aren't infinite either.
Sure there might be infinitely many Xs for this sought after value of X, but there shouldn't NEED to be.
We're looking for something like that.
Something fundamentally finite or at least something that we could force to be finite without it feeling like the hack job of truncating $\mathbb{N}$.
Our X should be more general than numbers or sets.
Something that's hiding in plain sight all around us if we could just open our eyes and see what X is.
Something that's painted all over every sentence in every area of mathematics, both the discrete areas like number theory and combinatorics and graph theory, and the continuous areas like calculus and geometry and topology.
Our X should be staring us in the face whenever we open any textbook, and when first hear someone say what it is we should feel a feeling of "Damn. Of course. Why didn't I think of that?"
1: Seems reasonable. What kind of thing is like that?
0: You tell me.
1: Functions?
0: Functions.
## The Church Src
### Or: A defn'ing silence
0: Ok, so now do we understand why a person might do something like this in the first place?
1: Totally.
0: Ok so Church's notation for functions was λx---
1: You don't have to explain lambdas. I'm a professional developer.
0: Great! So with that notation in hand, Church defined the natural numbers like this:
```
0 := λf. λx. x
1 := λf. λx. f x
2 := λf. λx. f (f x)
3 := λf. λx. f (f (f x))
4 := λf. λx. f (f (f (f x)))
succ := λn. λf. λx. f (n f x)
```
1: Woah woah, back up, I'm not ready for that yet.
0: You're not ready for the definition?
1: No.
0: What do you mean?
1: I mean that definition makes no sense to me. Back up to the part where they derive that.
0: Derive what?
1: The definition.
0: Church doesn't do that in this paper.
1: Ok can we find a textbook that does?
0: Sure, let's go look.
---
_(Narrator: 0 and 1 go find some other textbooks on λ calculus.)_
---
0: _(Looking at a large imposing yellow hardcover)_ This one doesn't have it.
1: _(Skimming a small paperback full of cute dialogues and elephants)_ Same with this one.
0: Y'know I've actually never seen the kind of derivation you're asking for before.
1: Well what did Kleene use as a repl?
0: He didn't have a repl.
1: How did he know if something he tried worked or not?
0: I think Church was his repl.
1: Well we can't do that! He's not here. And his paper isn't finished.
### Or: How to write good
0: Don't blame Church, this is just how mathematicians write.
1: I thought he was a foundational person.
0: He is. I just mean if you publish in academic journals you have to write that way. It's basically required. You can write _about_ almost anything. All the journals consistently care about is that you write in an academic sounding way.
1: You're not allowed to write good?
0: You're definitely not allowed to write good in journals. They think that's wrong, and it's only right to write "well."
1: Well that sucks.
0: You can't say sucks either.
1: Ibid![^1]
0: Exactly. So they (the Academic Ibid[^2]) care less about what you say and more about how you say it. And that makes it basically impossible to explain certain things, like what sorts of thoughts you'd have to have, and what sorts of mistakes you'd have to make, before you arrive at the definitions.
1: But the definitions are foundation of f$@king everything!
0: Can't say $@.
1: I mean the definitions are the most important bits to derive! They're like the API calls you use to prove stuff from.
0: Not allowed to say "stuff." And that "from" at the end is a preposition.
1: I'm so glad we're not writing a book.
0: You mean a paper?
1: Oh no I meant I'm glad we're not writing an academic thing.
0: Not allowed to say "thing."
_(Narrator: 1 is now vibrating in silent... um... I'm gonna guess rage.)_
0: You're allowed to explain the things after the definitions, because it's possible to write that stuff well.
_(Narrator: 1's emotion stays Ibid.)_
0: But you're not allowed to explain the bits before the definitions, at least not the bits that can only be explained good. If a thing can only be explained good and not well, you're not allowed to explain that thing.
1: You're not allowed to explain things?
0: You're allowed to explain things, but they have to sound formal.
1: I thought most mathematics wasn't formal.
0: No not "formal" as in formal languages. The journals don't care about formal languages and they certainly don't expect you to write in a formal language. They just want you to write in formal language.
1: I'm gonna scream.
### Or: A voice of one crying
### Or: במדבר[^3]
_(Narrator: 1 does the section heading | sed -e 's/cr/s&/' -e 's/y/eam/' -e 's/דב//')_[^4]
0: They just want it to sound fancy.
1: What's the point of that?
0: I don't know, it's a bug that tends to show up in institutions that are culturally overvalued. Whenever a system or group has more social status than it deserves, it always starts talking fancy and insisting the big words matter and anyone who doesn't use the right words is inherently less sophisticated. It's a defensive position. It's not my cup of tea, but one can see where they're coming from.
1: That's retarded. Be My Repl.
0: How so?
1: I'll write stuff. You tell me if it's a syntax error or not. Then when I plug things into functions, you evaluate them.
0: Let's split the work of evaluating them 50/50 and you've got a deal.
1: Great!
0: Ok I'm ready when you are.
1: How do I start the repl?
0: Type λ.
1: Um... ok.
```
~ $ λ
```
0:
![[welcome-to-lambda-trans.png]]
```
1: x
0: (says nothing)
1: So?
0: What do you want me to say?
1: I dunno, say yes if it's ok, or error if it's an error. Is that ok?
0: yes
1: x
0: yes
1: def f(x):
return x
0: error: invalid syntax falls on 'def' ears
1: What exactly am I allowed to do?
0: error: λ allows exactly everything
1: help()
0: error: λ helps those who help themselves
1: Can you be a repl and not a zen fortune cookie?
0: use :? for help
1:?
0:
=======================================
λ lang
t := x | λx.t | t t
:? help for the confused
:?! help for the confused and angry
=======================================
1:?!
0:
=======================================
λ's lang
There are only three
verbs you can do
in λ lang:
1. mkvar
2. mkfun
3. rmfun
1. how to use mkvar
say any letter,
in any alphabet
except λ.
this is a variable.
any variable is a thing.
2. how to use mkfun
take any thing b
that you've already made,
and any variable a
and write this:
λa.b
this is a function.
any function is a thing.
====================
SIDE NOTE: ON MORALS
AND CREATION AND YOU
AND YOUR RETARDATION
--------------------
now if b already has
a λa somewhere in it,
well, don't do that,
use another letter,
because if you say
λa twice in the same
thing, then that's
λaλa
and that's retarded,
so don't be retarded.
but if you choose to
be it anyway, despite
our kind advice, then
bc all bound variables
can always be renamed
in any part of math or
life where variables
are a thing, your λaλa
thing is equivalent to
λoλo
which means λoλ goes
the λoγος which means
you have to go back to
the beginning of life
and start over b/c in
the beginning was the
λoγολoλoγολoλoλoγος
so game over retard,
so sayeth the L||D.
====================
3. how to use rmfun
take any things a and b
that you've already
made, and write this:
a b
now, to evaluate any
thing of the form
a b
here are the rules:
you know the rules
already...
just do what feels
right. alright?
you know the rules
already...
...all this is
is really all just
functions after ∀.
so remember, don't
be afraid, & don't
try to solve lambda
let
lambda
(λ〇λＯλｏλολ。.ｏＯο〇 。) s o l ve you
(λＯλｏλολ。.ｏＯοs 。) o l ve you
(λｏλολ。.ｏoοs 。) l ve you
(λολ。.loοs 。) ve you
(λ。.loves 。) you
loves you
now type:
:) to confirm that you are
no longer angry
=======================================
1:)
```
1: _(Sarcastic slow clap.)_ Well, that was absurd but I think I get it now.
_(Narrator: 0 is unresponsive.)_
1: Zero?
_(Narrator: Ibid.)_
1: ZERO!
0: ʌ!![^5]
```
bash: !!: event not found
```
1: What was that?
0: You startled me.
1: How? I was here the whole time.
0: I think I blacked out there for a minute.
1: I think I get it now.
0: Get what?
1: Lambda calculus. Here be my repl again.
0: _(Dizzily)_
```
~ # λ
```
![[welcome-to-lambda-trans.png]]
```
1: Ok let me try some stuff to make sure I understand.
0: yes
1: Are you ready?
0: yes
1: x y
0: hmm
1: That's not very repl of you.
0: I'm thinking.
1: About what?
0: About what to say.
1: I thought you knew this system.
0: I mean, you have a free variable, and then you plugged it into another free variable. They're both functions. Cuz everything's functions. But neither of them has any lambdas in it. So it's syntactically ok, but we can't reduce it any further. It just sort of sits there. Which I guess is why I'm just sitting here.
1: Acceptable. What about this?
λx. x
0: That's ok.
1: What about
λx: 3
0: There's no 3 yet.
1: What? Why not?
0: You got intimidated by the definition.
1: Oh right. How about this?
λx. y
0: That's ok.
1: You're supposed to say yes.
0: yes
1: λx. λx. x
0: error
1: Why?
0: Try plugging something into it.
1: What something?
0: Idk, like 3.
1: I thought there was no 3 yet.
0: Treat it like a variable.
1: What?
0: I just mean plug something into that thing you just defined. Something that doesn't feel like a variable, so you don't get confused.
1:
(λx. λx. x) 3
= λ3. 3
0: You can't do lambda of three.
1: Why not?
0: 3 isn't a variable.
1: I thought you said treat it like a variable.
0: Fair point. But the problem was that you had two copies of λx.
1: How's that a problem?
0: Because these λ expressions are supposed to act like functions. You know functions. Like for example, in C
```
```c
/* 0: what would you think if I wrote this? */
int foo(int x, int x) {
return x;
}
// 1: i would think you're a damn foo bc
~ $ cc c.c
c.c:1:20: error: redefinition of parameter ‘x’
1 | int foo(int x, int x) {
| ~~~~^
c.c:1:13: note: previous definition of ‘x’ with type ‘int’
1 | int foo(int x, int x) {
| ~~~~^
/* 0: Exactly! So in λ calculus */
```
```
0: The compiler throws an error for this too
(λx. λx. x)
1: Ah, got it. Wait there's a compiler for λ calculus?
0: Of course.
1: What's it called?
0: (λrλρ.ρerl) p r
1: perl?
0: No.
1: rpperlpr?
0: Nope.
1: What's it called then?
0: (λρ.ρepl) r
1: ppeplr?
0: No.
1: Then what?
0: repl
1: But that's you!
0: You're just brilliant, y'know that?
1: I knew what you were doing dummy, I just enjoy watching you act all smug like you're revealing some secret truth even though you were just plugging stuff into functions like a toddler.
0: Damn, you're spicy in this file.
1: Nah, I just got the idea of how λ lang works a while back in that "lambda loves you" example, and now I'm just waiting until you're ready to move on to something harder.
0: What "lambda loves you" example?
1: During that long :?! help message.
0: I don't remember that at all.
1: Yeah I think you blacked out and had a revelation or something.
0: So you're ready to move on?
1:q
```
1: Yeah.
0: Deal.
1: What should we do next?
0: λ calculus!
1: We already did λ calculus.
0: No, you learned to use the repl. We didn't actually build anything.
1: How do you "build" anything in lambda calculus?
0: By writing code. Same as any language.
1: Zero, this language has zero features. You can make variables, put lambdas around stuff, and plug stuff into lambdas. There's zero interesting stuff left to do. It's like playing with a cardboard box.
0: So you understand Church's definition of numbers from earlier?
1: Oh yeah I forgot about that. What was the definition again?
0:
```
0 := λf. λx. x
1 := λf. λx. f x
2 := λf. λx. f (f x)
3 := λf. λx. f (f (f x))
4 := λf. λx. f (f (f (f x)))
```
1: Jesus Christ Church why?
0: Don't understand it yet?
1: Not entirely. I mean obviously each number is the number of `f`s.
0: Sounds like you understand it.
1: I definitely don't.
0: But "the number of `f`s" is the whole idea.
1: No it isn't.
0: How is that not the idea?
1: What's the `x` for?
0: That's the thing you plug into `f`.
1: Exactly. That's why I'm confused.
0: How is that confusing.
1: What's `x`?
0: A variable.
1: What's `f`?
0: A function.
1: But they're both variables.
0: Right. And they're both functions.
1: And Church knew that?
0: Of course Church knew that, he invented all this.
1: Then if he knew what I just said, why not define numbers like this?
```
0 := λx. x
1 := λx. x x
2 := λx. x (x x)
3 := λx. x (x (x x))
4 := λx. x (x (x (x x)))
```
0: Hmm...
1: Not sure why?
0: Not entirely...
1: See? I was right.
0: Well, let's go solve it.
1: Solve what?
0: The definition!
1: How do you solve a definition?
0: I mean solve _for_ the definition. Derive it. Like you were talking about earlier.
1: How do we do that?
0: Just stop thinking of it as math.
1: Isn't it math?
0: Sure, but it's also programming.
1: So what?
0: Well "definitions" in math seem to come out of nowhere, because math books don't show you were definitions come from, so "solving for definitions" feels like some mysterious dark art.
1: Agreed.
0: But you know where definitions come from in programming.
1: Of course.
0: Where?
1: You just write them.
0: What if you do it wrong?
1: Zero don't be dumb. You change the code. Programming isn't magic. Definitions are just code.
0: Exactly!
_(Narrator: The characters are suddenly transported to the next file, as if by magic.)_
goto [[lost+found/3/5]]
[^1]: T.N. Sic.
[^2]: T.N. Sic?
[^3]: T.N. Hebrew for RBDMB. Sic?
[^4]: T.N. Does anyone know what's going on in this file?
[^5]: T.N. Finally something I can help with. The open-mid back unrounded vowel (i.e., ʌ) in the International Phonetic Alphabet (i.e., IPA) 一 not to be confused with an uppercase lambda (i.e., Λ) from the National Hellenic Alphabet (i.e., Grk) 一 the former of which is not dissimilar to the phoneme /ə/, though given the supra (i.e., above) context in which it was used, one can safely assume Zero was screaming, and the above scream should therefore have been transcribed more like this:
<span style="display: block; text-align: center; font-size: 32pt;">/ˈʌ̋ː/</span>
Thank you for your attention.
Professionally yours,
-The Translator### Or: Formal Function Theory
0: Ok so in Church's system, everything is functions.
1: You've mentioned this already, but I still don't know what you mean.
0: How do you mean?
1: I mean if everything is functions, what do they take as inputs?
0: Functions.
1: What do they return as outputs?
0: Functions.
1: Zero?
0: What?
1: ... That's insane.
0: I know it feels that way at first. But it's not so bad once you implement numbers and booleans.
1: Sure sure, but WHY?
0: Why what?
1: Why do this at all?
0: Why are _we_ doing it?
1: No why was Church doing it? I want to know what was going on inside his head, or at least what might have been. What would make a person say "Yaי know what I'm gonna do today? Make a system where 0 and 1 are actually functions." Like that's not a normal behavior and it's not a natural way to think. So I'm curious what was going on in this guy's head that would make him do something like that.
0: Perfect question! Ok so, by the time Church is writing, formal theories had been a thing for a while.
1: "Formal theories" as in?...
0: Programming languages.
1: Oh?
0: Ones that run on paper.
1: Makes sense.
0: ZFC had already done formal set theory. PA had already done formal number theory. It's not unreasonable to think something like "Look guys, those theories you made are cute and all, but the foundations of mathematics or even reasoning itself shouldn't be just whole numbers or unordered collections. The foundations of mathematics should be something more primitive."
1: What's more primitive than those things?
0: Well there are infinitely many natural numbers. And that's not a problem in itself, but we'd like our foundations to be something inherently finite.
1: Inherently finite?
0: Inherently finite. I mean when a mathematician proves stuff about the natural numbers by induction, they do it with only a finite amount of time and food and paper and pencils and erasers and pants and money and everything. Finite everything.
1: Obviously. What's your point?
0: Foundations should be like that. I mean, it's fine that the natural numbers are infinite, but they're not finite in the same obvious way that the mathematician with the paper is finite and only doing finite stuff. If we truncate the natural numbers at any finite level and say "There are no natural numbers above ten million" or whatever, any mathematician would rightly feel like we'd done a violent ugly hack that made the natural numbers less of what they are. But there's no such feeling when a mathematician uses only finitely many pencils or finitely many sheets of paper. We have no problem with that, and we'd be disturbed if either was infinite. So in that sense natural numbers are way too big to be foundations.
1: What about sets? Sets can be finite.
0: True! But all versions of set theory that have ever been proposed as foundations are way more infinite than the whole numbers are. They tend to all include a sentence that says "ω exists."
1: You mean ω like Cantor's first size of infinity?
0: Well in this case it means "The set of natural numbers," but those are actually the same thing.
1: How are those the same thing?
0: Well no finite number is big enough to be the smallest infinite number. So the set of all natural numbers ends up being the same thing as "the smallest infinite number" in that system.
1: Numbers are sets?
0: Numbers are sets. At least in that system, where everything is sets. Anyways things are even worse in set theory than in number theory, because there tends to be another axiom that says "If a set X exists, then so does P(X), the set of all its subsets." And that P(X) thing turns out to always be a bigger size than X is, even if X is infinite. So any formal theory that had these two things together grows an infinite number of different sizes of infinity, each larger than the next.
1: I remember. So what was Church thinking?
0: Well taking together both the fact that (i) the natural numbers have an inherent inability to be made finite without it feeling like an ugly hack, and (ii) set theory has such a wildly irresponsibly number of infinite things that it's not clear how it got invited to the foundations party... taking those two things together, you might end up thinking what Church was thinking.
1: _(Narrative voice)_ "So what was Church thinking?, 1 asked yet again."
0: That we need a "Formal Theory of X" for some better X than just X = numbers and X = sets.
It should be something fundamentally finite.
Maybe there's infinitely many Xs, whatever this not-yet-mentioned X type thing is, but it should be possible to _make_ the theory only about finitely many objects made of inherently finite stuff, and finitely many operations on those things. We should be able to "finitize" the theory without it feeling like an awful hack in the way it would be if we said 1 million is the largest natural number.
1: "Without it feeling like"?
0: Yeah, what's the problem?
1: You seem to be suggesting that Church wanted something finite, but his foundation for wanting that was "feelings."
0: Of course! I mean I never knew Church personally, but that's a totally normal way to think when you're doing mathematics.
1: The more you talk about math, the less I understand what it really is.
0: Good. That means you're listening. So anyways if you thought all the thoughts above, you might end up doing what Church did, so let's do our best to get inside his head.
We're looking for some type of X where we can build a "Formal Theory of X" that doesn't feel fundamentally broken if we don't have infinitely many of them, or if the guts of each one aren't infinite either.
Sure there might be infinitely many Xs for this sought after value of X, but there shouldn't NEED to be.
We're looking for something like that.
Something fundamentally finite or at least something that we could force to be finite without it feeling like the hack job of truncating $\mathbb{N}$.
Our X should be more general than numbers or sets.
Something that's hiding in plain sight all around us if we could just open our eyes and see what X is.
Something that's painted all over every sentence in every area of mathematics, both the discrete areas like number theory and combinatorics and graph theory, and the continuous areas like calculus and geometry and topology.
Our X should be staring us in the face whenever we open any textbook, and when first hear someone say what it is we should feel a feeling of "Damn. Of course. Why didn't I think of that?"
1: Seems reasonable. What kind of thing is like that?
0: You tell me.
1: Functions?
0: Functions.
## The Church Src
### Or: A defn'ing silence
0: Ok, so now do we understand why a person might do something like this in the first place?
1: Totally.
0: Ok so Church's notation for functions was λx---
1: You don't have to explain lambdas. I'm a professional developer.
0: Great! So with that notation in hand, Church defined the natural numbers like this:
```
0 := λf. λx. x
1 := λf. λx. f x
2 := λf. λx. f (f x)
3 := λf. λx. f (f (f x))
4 := λf. λx. f (f (f (f x)))
succ := λn. λf. λx. f (n f x)
```
1: Woah woah, back up, I'm not ready for that yet.
0: You're not ready for the definition?
1: No.
0: What do you mean?
1: I mean that definition makes no sense to me. Back up to the part where they derive that.
0: Derive what?
1: The definition.
0: Church doesn't do that in this paper.
1: Ok can we find a textbook that does?
0: Sure, let's go look.
---
_(Narrator: 0 and 1 go find some other textbooks on λ calculus.)_
---
0: _(Looking at a large imposing yellow hardcover)_ This one doesn't have it.
1: _(Skimming a small paperback full of cute dialogues and elephants)_ Same with this one.
0: Y'know I've actually never seen the kind of derivation you're asking for before.
1: Well what did Kleene use as a repl?
0: He didn't have a repl.
1: How did he know if something he tried worked or not?
0: I think Church was his repl.
1: Well we can't do that! He's not here. And his paper isn't finished.
### Or: How to write good
0: Don't blame Church, this is just how mathematicians write.
1: I thought he was a foundational person.
0: He is. I just mean if you publish in academic journals you have to write that way. It's basically required. You can write _about_ almost anything. All the journals consistently care about is that you write in an academic sounding way.
1: You're not allowed to write good?
0: You're definitely not allowed to write good in journals. They think that's wrong, and it's only right to write "well."
1: Well that sucks.
0: You can't say sucks either.
1: Ibid![^1]
0: Exactly. So they (the Academic Ibid[^2]) care less about what you say and more about how you say it. And that makes it basically impossible to explain certain things, like what sorts of thoughts you'd have to have, and what sorts of mistakes you'd have to make, before you arrive at the definitions.
1: But the definitions are foundation of f$@king everything!
0: Can't say $@.
1: I mean the definitions are the most important bits to derive! They're like the API calls you use to prove stuff from.
0: Not allowed to say "stuff." And that "from" at the end is a preposition.
1: I'm so glad we're not writing a book.
0: You mean a paper?
1: Oh no I meant I'm glad we're not writing an academic thing.
0: Not allowed to say "thing."
_(Narrator: 1 is now vibrating in silent... um... I'm gonna guess rage.)_
0: You're allowed to explain the things after the definitions, because it's possible to write that stuff well.
_(Narrator: 1's emotion stays Ibid.)_
0: But you're not allowed to explain the bits before the definitions, at least not the bits that can only be explained good. If a thing can only be explained good and not well, you're not allowed to explain that thing.
1: You're not allowed to explain things?
0: You're allowed to explain things, but they have to sound formal.
1: I thought most mathematics wasn't formal.
0: No not "formal" as in formal languages. The journals don't care about formal languages and they certainly don't expect you to write in a formal language. They just want you to write in formal language.
1: I'm gonna scream.
### Or: A voice of one crying
### Or: במדבר[^3]
_(Narrator: 1 does the section heading | sed -e 's/cr/s&/' -e 's/y/eam/' -e 's/דב//')_[^4]
0: They just want it to sound fancy.
1: What's the point of that?
0: I don't know, it's a bug that tends to show up in institutions that are culturally overvalued. Whenever a system or group has more social status than it deserves, it always starts talking fancy and insisting the big words matter and anyone who doesn't use the right words is inherently less sophisticated. It's a defensive position. It's not my cup of tea, but one can see where they're coming from.
1: That's retarded. Be My Repl.
0: How so?
1: I'll write stuff. You tell me if it's a syntax error or not. Then when I plug things into functions, you evaluate them.
0: Let's split the work of evaluating them 50/50 and you've got a deal.
1: Great!
0: Ok I'm ready when you are.
1: How do I start the repl?
0: Type λ.
1: Um... ok.
```
~ $ λ
```
0:
![[welcome-to-lambda-trans.png]]
```
1: x
0: (says nothing)
1: So?
0: What do you want me to say?
1: I dunno, say yes if it's ok, or error if it's an error. Is that ok?
0: yes
1: x
0: yes
1: def f(x):
return x
0: error: invalid syntax falls on 'def' ears
1: What exactly am I allowed to do?
0: error: λ allows exactly everything
1: help()
0: error: λ helps those who help themselves
1: Can you be a repl and not a zen fortune cookie?
0: use :? for help
1:?
0:
=======================================
λ lang
t := x | λx.t | t t
:? help for the confused
:?! help for the confused and angry
=======================================
1:?!
0:
=======================================
λ's lang
There are only three
verbs you can do
in λ lang:
1. mkvar
2. mkfun
3. rmfun
1. how to use mkvar
say any letter,
in any alphabet
except λ.
this is a variable.
any variable is a thing.
2. how to use mkfun
take any thing b
that you've already made,
and any variable a
and write this:
λa.b
this is a function.
any function is a thing.
====================
SIDE NOTE: ON MORALS
AND CREATION AND YOU
AND YOUR RETARDATION
--------------------
now if b already has
a λa somewhere in it,
well, don't do that,
use another letter,
because if you say
λa twice in the same
thing, then that's
λaλa
and that's retarded,
so don't be retarded.
but if you choose to
be it anyway, despite
our kind advice, then
bc all bound variables
can always be renamed
in any part of math or
life where variables
are a thing, your λaλa
thing is equivalent to
λoλo
which means λoλ goes
the λoγος which means
you have to go back to
the beginning of life
and start over b/c in
the beginning was the
λoγολoλoγολoλoλoγος
so game over retard,
so sayeth the L||D.
====================
3. how to use rmfun
take any things a and b
that you've already
made, and write this:
a b
now, to evaluate any
thing of the form
a b
here are the rules:
you know the rules
already...
just do what feels
right. alright?
you know the rules
already...
...all this is
is really all just
functions after ∀.
so remember, don't
be afraid, & don't
try to solve lambda
let
lambda
(λ〇λＯλｏλολ。.ｏＯο〇 。) s o l ve you
(λＯλｏλολ。.ｏＯοs 。) o l ve you
(λｏλολ。.ｏoοs 。) l ve you
(λολ。.loοs 。) ve you
(λ。.loves 。) you
loves you
now type:
:) to confirm that you are
no longer angry
=======================================
1:)
```
1: _(Sarcastic slow clap.)_ Well, that was absurd but I think I get it now.
_(Narrator: 0 is unresponsive.)_
1: Zero?
_(Narrator: Ibid.)_
1: ZERO!
0: ʌ!![^5]
```
bash: !!: event not found
```
1: What was that?
0: You startled me.
1: How? I was here the whole time.
0: I think I blacked out there for a minute.
1: I think I get it now.
0: Get what?
1: Lambda calculus. Here be my repl again.
0: _(Dizzily)_
```
~ # λ
```
![[welcome-to-lambda-trans.png]]
```
1: Ok let me try some stuff to make sure I understand.
0: yes
1: Are you ready?
0: yes
1: x y
0: hmm
1: That's not very repl of you.
0: I'm thinking.
1: About what?
0: About what to say.
1: I thought you knew this system.
0: I mean, you have a free variable, and then you plugged it into another free variable. They're both functions. Cuz everything's functions. But neither of them has any lambdas in it. So it's syntactically ok, but we can't reduce it any further. It just sort of sits there. Which I guess is why I'm just sitting here.
1: Acceptable. What about this?
λx. x
0: That's ok.
1: What about
λx: 3
0: There's no 3 yet.
1: What? Why not?
0: You got intimidated by the definition.
1: Oh right. How about this?
λx. y
0: That's ok.
1: You're supposed to say yes.
0: yes
1: λx. λx. x
0: error
1: Why?
0: Try plugging something into it.
1: What something?
0: Idk, like 3.
1: I thought there was no 3 yet.
0: Treat it like a variable.
1: What?
0: I just mean plug something into that thing you just defined. Something that doesn't feel like a variable, so you don't get confused.
1:
(λx. λx. x) 3
= λ3. 3
0: You can't do lambda of three.
1: Why not?
0: 3 isn't a variable.
1: I thought you said treat it like a variable.
0: Fair point. But the problem was that you had two copies of λx.
1: How's that a problem?
0: Because these λ expressions are supposed to act like functions. You know functions. Like for example, in C
```
```c
/* 0: what would you think if I wrote this? */
int foo(int x, int x) {
return x;
}
// 1: i would think you're a damn foo bc
~ $ cc c.c
c.c:1:20: error: redefinition of parameter ‘x’
1 | int foo(int x, int x) {
| ~~~~^
c.c:1:13: note: previous definition of ‘x’ with type ‘int’
1 | int foo(int x, int x) {
| ~~~~^
/* 0: Exactly! So in λ calculus */
```
```
0: The compiler throws an error for this too
(λx. λx. x)
1: Ah, got it. Wait there's a compiler for λ calculus?
0: Of course.
1: What's it called?
0: (λrλρ.ρerl) p r
1: perl?
0: No.
1: rpperlpr?
0: Nope.
1: What's it called then?
0: (λρ.ρepl) r
1: ppeplr?
0: No.
1: Then what?
0: repl
1: But that's you!
0: You're just brilliant, y'know that?
1: I knew what you were doing dummy, I just enjoy watching you act all smug like you're revealing some secret truth even though you were just plugging stuff into functions like a toddler.
0: Damn, you're spicy in this file.
1: Nah, I just got the idea of how λ lang works a while back in that "lambda loves you" example, and now I'm just waiting until you're ready to move on to something harder.
0: What "lambda loves you" example?
1: During that long :?! help message.
0: I don't remember that at all.
1: Yeah I think you blacked out and had a revelation or something.
0: So you're ready to move on?
1:q
```
1: Yeah.
0: Deal.
1: What should we do next?
0: λ calculus!
1: We already did λ calculus.
0: No, you learned to use the repl. We didn't actually build anything.
1: How do you "build" anything in lambda calculus?
0: By writing code. Same as any language.
1: Zero, this language has zero features. You can make variables, put lambdas around stuff, and plug stuff into lambdas. There's zero interesting stuff left to do. It's like playing with a cardboard box.
0: So you understand Church's definition of numbers from earlier?
1: Oh yeah I forgot about that. What was the definition again?
0:
```
0 := λf. λx. x
1 := λf. λx. f x
2 := λf. λx. f (f x)
3 := λf. λx. f (f (f x))
4 := λf. λx. f (f (f (f x)))
```
1: Jesus Christ Church why?
0: Don't understand it yet?
1: Not entirely. I mean obviously each number is the number of `f`s.
0: Sounds like you understand it.
1: I definitely don't.
0: But "the number of `f`s" is the whole idea.
1: No it isn't.
0: How is that not the idea?
1: What's the `x` for?
0: That's the thing you plug into `f`.
1: Exactly. That's why I'm confused.
0: How is that confusing.
1: What's `x`?
0: A variable.
1: What's `f`?
0: A function.
1: But they're both variables.
0: Right. And they're both functions.
1: And Church knew that?
0: Of course Church knew that, he invented all this.
1: Then if he knew what I just said, why not define numbers like this?
```
0 := λx. x
1 := λx. x x
2 := λx. x (x x)
3 := λx. x (x (x x))
4 := λx. x (x (x (x x)))
```
0: Hmm...
1: Not sure why?
0: Not entirely...
1: See? I was right.
0: Well, let's go solve it.
1: Solve what?
0: The definition!
1: How do you solve a definition?
0: I mean solve _for_ the definition. Derive it. Like you were talking about earlier.
1: How do we do that?
0: Just stop thinking of it as math.
1: Isn't it math?
0: Sure, but it's also programming.
1: So what?
0: Well "definitions" in math seem to come out of nowhere, because math books don't show you were definitions come from, so "solving for definitions" feels like some mysterious dark art.
1: Agreed.
0: But you know where definitions come from in programming.
1: Of course.
0: Where?
1: You just write them.
0: What if you do it wrong?
1: Zero don't be dumb. You change the code. Programming isn't magic. Definitions are just code.
0: Exactly!
_(Narrator: The characters are suddenly transported to the next file, as if by magic.)_
goto [[lost+found/3/5]]
[^1]: T.N. Sic.
[^2]: T.N. Sic?
[^3]: T.N. Hebrew for RBDMB. Sic?
[^4]: T.N. Does anyone know what's going on in this file?
[^5]: T.N. Finally something I can help with. The open-mid back unrounded vowel (i.e., ʌ) in the International Phonetic Alphabet (i.e., IPA) 一 not to be confused with an uppercase lambda (i.e., Λ) from the National Hellenic Alphabet (i.e., Grk) 一 the former of which is not dissimilar to the phoneme /ə/, though given the supra (i.e., above) context in which it was used, one can safely assume Zero was screaming, and the above scream should therefore have been transcribed more like this:
<span style="display: block; text-align: center; font-size: 32pt;">/ˈʌ̋ː/</span>
Thank you for your attention.
Professionally yours,
-The Translator