- [[#(3,5): The Zeroth Law|(3,5): The Zeroth Law]]
- [[#1. Control Flow: if `if` then `then` else `else`|1. Control Flow: if `if` then `then` else `else`]]
- [[#2. Logic and (Logic or (Logic and not not Logic))|2. Logic and (Logic or (Logic and not not Logic))]]
- [[#3. Data Structures = (Data, Structures)|3. Data Structures = (Data, Structures)]]
- [[#4. Plus One|4. Plus One]]
- [[#4. Plus One (One More Time)|4. Plus One (One More Time)]]
- [[#5. Arithmetic Succs|5. Arithmetic Succs]]
- [[#6. Arithmetic Succs (Hard)|6. Arithmetic Succs (Hard)]]
- [[#Reminiscences of Logicians: What Church was Thinking|Reminiscences of Logicians: What Church was Thinking]]
- [[#6. Lambda the Ultimate|6. Lambda the Ultimate]]
- [[#Reminiscences of Logicians: Church's Thesis|Reminiscences of Logicians: Church's Thesis]]
- [[#Reminiscences of Logicians: Post Haste|Reminiscences of Logicians: Post Haste]]
- [[#Reminiscences of Logicians: Post Script|Reminiscences of Logicians: Post Script]]
- [[#Reminiscences of Logicians: Post Mortem|Reminiscences of Logicians: Post Mortem]]
- [[#Gödel arrives on the Scene|Gödel arrives on the Scene]]
## (3,5): The Zeroth Law
### Or: Premathematics
> _We have a habit in writing articles published in scientific journals to make the work as finished as possible, to cover all the tracks, to not worry about the blind alleys or to describe how you had the wrong idea first, and so on. So there isn't any place to publish, in a dignified manner, what you actually did in order to get to do the work._
> `~ $ echo "Richard Feynman, Nobel Prize Lecture (1965)"`
> _Science is the belief in the ignorance of experts._
> `~ # Ibid | sed -e 's/,[^(]*/, What is Science? /' -e 's/5/9/g'`
---
0: Where would you like to start?
1: Definitely not with numbers. That definition scared me.
0: So where should we start?
1: I'd rather start with like, programming.
0: Which part?
1: I dunno. Maybe if we start with `if`, then `else`, then maybe some data structures or something then I'll have a better idea of what Church was thinking, because so far I don't really get why he'd want to do all this.
0: I'll follow your lead.
---
## 1. Control Flow: if `if` then `then` else `else`
1: How do I start?
0: You said you want to start by implementing `if`.
1: In what?
0: In functions!
1: How is `if` a function?
0: It's not. But we need to make it be one.
1: Why?
0: Cuz all we have is functions.
1: Ok, um...
```
def if(???):
return what?
```
1: I'm definitely stuck.
0: No you're not! That was a great start.
1: How was that a great start?
0: Because now the rest is obvious. Here watch:
```
def if(if, then, else):
if if
then then
else else
```
1: What the hell is going on zero?
0: I mean if `if` is a function, then it takes three things:
1. A boolean called `if`.
2. A stuff called `then`
3. A stuff called `else`
1: What's a stuff?
0: Whatever stuff you want to do. Like a code block. Any code.
1: Can we call the boolean something different? This is hurting my head.
0: Sure, refactor however you want.
1: Ok how's this?
```python
def if_then_else(condition, then_do_a_thing, else_do_b_thing):
# Ok this is gonna be a problem...
# Umm...
if condition: # TODO: Implement if
return then_do_a_thing
else: # TODO: See above
return else_do_b_thing
```
0: Great!
1: Zero that was a joke.
0: Seemed totally reasonable to me.
1: ZERO COME ON. Obviously I can't use `if` to implement `if`. I just got stuck and gave up.
0: I don't think you got stuck at all! Here let's re-write it in Church.
1: What?
0: I mean that pseudo-code looks like python. If we re-write your pseudo-code in Church, it sort of makes sense. Watch:
```
if_then_else = λc λa λb: c a b
```
1: What the hell's going on there?
0: It's just an abbreviation for your code. It means this:
```python
def if_then_else(c, # ondition
a, # a thing to do if c is true
b, # b thing to do if c is false
) # that's it.
```
0: See?
1: But you didn't write the function body. That's just the signature.
0: The body is the same.
1: Same as what?
0: The signature! Look:
```python
def if_then_else(c,
a,
b,
):
return (c
a
b
)
```
1: Is this actually an idea or are you just stalling for time?
0: It's your idea! I'm just rewriting your implementation by making the variable names shorter.
1: But my implementation was a joke. I used `if` inside of `if`. That was cheating.
0: Well obviously we need to use `if` inside of `if` or else it won't act like `if`.
1: Come again?
0: I mean unless we do something iffy in the implementation then it won't be iffy enough to act like if!
1: I agree that this is iffy.
0: Here look. It's already there in the code. I'll reformat it so it's clearer.
```python
def if_then_else(c, a, b):
return c a b
```
1: What does that `return c a b` mean?
0: Oh sorry, in the top line I was writing python-y but then on line two I accidentally slipped back into my native language.
1: What?
0: The shell!
1: Oh right.
0: I was trying to write a normal function call, I just pronounced it with a shlaccent.
1: I still don't see how this is `if`.
0: It's obviously `if`! Here look:
```python
def if_then_else(c, a, b):
return c(a, b)
```
1: I'm even more confused now.
0: Look back at your definition.
_(Narrator: 1 looks back at 1's definition.)_
1: I don't see how that helps.
0: Here I'll rewrite it.
```python
def if_then_else(c, a, b):
if c:
return a
else:
return b
```
1: It's still iffy.
0: It better be. If it's not iffy it's not if!
1: Can you stop with the puns and explain how your thing is my thing?
0: Pass a bool into both.
1: We didn't implement bools yet.
0: So pass one in.
1: How can we pass bools into `if` if we haven't implemented bools yet?
0: Y'know. Pseudo-code.
1: But pseudo-code isn't REAL zero.
0: In situations like this, it's best not to worry about whether or not a thing is real. Worrying about if its real just prevents you from using it.
1: How can I use it if it doesn't exist?
0: Pass a bool in.
1: How can I pass a bool in if it doesn't exist?
0: Well if the pragmatic benefits aren't your thing and you'd prefer a more rigorous and ontologically grounded argument, I'd say we also didn't implement errors so it's guaranteed to work.
1: You're the weirdest programming teacher.
0: Just do it.
1: Ok...
```python
#################
### 0's thing ###
#################
def if_then_else(c, a, b):
return c(a, b)
# Now let's pass in `true`,
# even though we didn't
# implement it yet...
if_then_else(true, a, b)
# the true goes into the
# function and becomes
return true(a, b)
# which is just
true(a, b)
# Um...
# Ok I'm stuck. Let's go do mine.
#################
### 1's thing ###
#################
def if_then_else(c, a, b):
if c:
return a
else:
return b
# Pass in a true
if_then_else(true, a, b)
# the true goes into the function body
if true:
return a
else:
return b
# this one's easier to reason about.
# obviously this is just
return a
# which is just
a
```
1: Did I do it right?
0: Did you get any errors?
1: We didn't implement errors.
0: Well we didn't implement `if` either but you just used it twice.
1: That's true. Was that allowed?
0: Any errors?
1: No.
0: Great! I'd say we're on the right track.
1: I still don't understand your implementation.
0: Do you understand yours?
1: Yes, but mine was cheating.
0: Well mine's the same as yours, but mine isn't cheating.
_(Narrator: 1 looks back at 0's `if`.)_
```python
def if_then_else(c, a, b):
return c(a, b)
>>> if_then_else(true, a, b)
true(a, b)
```
1: How is yours the same as mine?
0: Well it better return `a` like yours did or else it's not `if`. Because yours is definitely `if`. And yours returned `a`.
1: So yours behaves like this?
```python
>>> true(a, b)
a
```
0: I think it has to.
1: But we didn't define `true` yet.
0: I think we just did.
1: How?
0: Well `true` had better take two variables and return the first one.
1: What do you mean "had better"?
0: Well if it doesn't act like that, then my `if` doesn't act like `if` and I'm gonna have to start over. But if it does act like that, then I already implemented `if` and `true`, so the number of things I've implemented is either zero or two, and I'd prefer the latter, because in that case I'm ahead of you.
1: _(Skeptical)_ I feel like you're getting ahead of yourself.
0: Good point, we haven't done `false` yet. And until we have `false`, we can't say we're done with `if`.
1: How do we implement `false`?
0: I dunno. Pass it in.
1: I would remind you that we didn't implement it yet, but your weird backwards reasoning seemed to work last time, so what the hell...
```python
# Mine obviously does this:
>>> if_then_else(false, a, b)
b
# And yours is weird, same as before
def if_then_else(c, a, b):
return c(a, b)
>>> if_then_else(false, a, b)
false(a, b)
```
1: What's `false(a, b)`?
0: Well it had better be `b` or I'm gonna have to start over.
1: Who decides if it gets to be `b`?
0: I think `false` gets to decide.
1: Who gets to decide how to implement `false`?
0: I think we do.
1: This feels illegal.
0: It's totally fine. Here look.
```python
def false(a, b):
return b
```
0: And now we've implemented `false` too!
1: I'm kind of mad that this keeps working for you.
0: You're mad that it keeps working for _us._
1: How do we know if we cheated?
0: What do you mean?
1: I mean we're supposed to be implementing Church's λ language, but so far we've been speaking slang and pseudo-code and it all feels a bit iffy.
0: It had be---
1: Yes yes. How do we check if this all works in Church?
0: Well, let's write the same thing in Church and see if it works.
1: How will we know if it works?
0: I guess we'll have to use the language.
1: Again, I would complain, but this seems to be working.
0: I'll follow your lead.
1: What do you want me to do?
0: Take the iffy stuff we just did and say it in Church.
1: This?
```python
def if_then_else(c, a, b):
return c(a, b)
```
0: Yeah.
1: How do I say it in Church?
0: Easy. You just go:
```sh
# And the L||D sed...
sed -E \
-e '1s@[(]@ = @' \
-e '1s@(.)(, |[)])@λ\1@g' \
-e 'N;s@(def |\s+return )@@g' \
-e 's@(, |[()])@ @g' \
-e 's@:@.@'
```
1: Simple enough.
_(Narrator: 1 runs the sed.)_
1: Ok it looks like this now:
```
if_then_else = λcλaλb.c a b
```
1: Is that right?
0: Has to be.
1: What's going on here?
0: It's just Church-lang.
1: What's the dot?
0: Think of it as a colon and it'll feel more familiar. The Church-lang code above is the same idea as this:
```python
def if_then_else(a,b,c): return c(a,b)
```
or equivalently:
```python
if_then_else = lambda c,a,b: c(a,b)
```
Now technically, in order to be Gramatically Correct Church[^1] that compiles correctly[^2] we have to replace all the multiple argument functions with single argument functions returning functions, like this:
[^1]: Or: gcc.
[^2]: Or: cc.
```python
if_then_else = lambda c: lambda a: lambda b: c(a)(b)
```
1: _(Looking back at the iffy stuff)_ How do we know if it worked?
0: I think we have to use it.
1: How do we use it?
0: I dunno, pass in a `true`.
1: Into what?[^3]
[^3]:
1: Into what?
0: Into the function `if_then_else = λcλaλb.c a b`.
1: No, I mean: When I pass something in to that function , does it go into the slot on the left (where the `c` is) or the slot on the right (where the `b` is)?
0: Why are you asking me? We're inventing this language after all.
1: So I can pass in the `true` to any slot?
0: No. I was saying, we _could_ design the language either way, but in this case we already decided which slot stuff goes in. If you need a hint, look at two code blocks above this one, in the python example with the three `lambdas`.
1: Oh, I feel dumb.
0: No worries, I have to remind myself about this stuff too.
0: This:
```
if_then_else = λcλaλb.c a b
```
1: Ok so...
```
# if we take the code here:
if_then_else = λcλaλb.c a b
# and pass in a true, we get
if_then_else(true) = λaλb.true a b = ?...
```
1: I'm confused. Why are there still λs in there?
0: You forgot to pass in two code blocks that tell the `if` what to do.
1: We didn't implemen--- Nevermind. I'm seeing a pattern here.
0: Pick up where you left off.
1: Ok, so let's pass in two imaginary code blocks `A` and `B` that say what to do when the condition's true or false.
```
if_then_else(true)(A)(B)
= (λcλaλb.c a b)(true)(A)(B) # by definition
= (λaλb.true a b)(A)(B) # pass the true into the c slot
= (λb.true A b)(B) # pass the A into the b slot
= (true A B) # pass the B into the a slot
= true A B # ok i'm stuck
```
1: Now what?
0: Well we already defined `true`.
1: Oh right.
0: So now we just say it in Church, like this:
```python
# In the pseudo-code from earlier (non Church lang)
>>> true(a, b)
a
```
0: In Church lang, we pronounce it like this:
```
true = λaλb.a
```
1: How do I use that?
0: Plug it into true.
1: Plug true into true?
0: By definition!
1: All your worst nonsense somehow makes more sense than your best non-nonsense.
0: That's how truth works! Now show me how true works.
```
if_then_else(true)(A)(B)
... # all the steps I did above
= true A B # now let's plug true into true (O_o)
= (λaλb.a) A B # plug in the `then` code path
= (λb.A) B # plug in the `else` code path
A # I think this means it worked?
```
0: Of course that means it worked!
1: "Of course" how?
0: We plugged a `true` into `if` and the `then` branch popped out!
1: So if we pass `false` in we get `B`?
0: We better! If not, that wouldn't be very iffy.
1: Here I'll check, I think I'm getting the hang of Church lang.
```python
# This was our `false` in pseudo-code
def false(a, b):
return b
```
1: So if we pronounce that in Church, we say
```
false = λaλb.b
```
1: Now let's plug `false` into the `false` slot of `if` and toss two pretend code blocks in too, same as before:
```
if_then_else(false)(A)(B)
= (λcλaλb.c a b)(false)(A)(B) # by definition of if_then_else
= false A B # i'll just plug in all three this time
= (λaλb.b) A B # by our definition of false
= (λb.b) B # plug in the A
= B # (λb.b) is the identity, so we get B
```
0: It's false!
1: I messed up?
0: No! I mean hooray, our false worked like false. It's a true false!
1: I'm kinda surprised but this is actually making sense.
0: 1derful! Onward!
1: What should we do now?
0: I dunno, maybe we're ready for numbers?
1: How were zero and one defined again?
0: I think that's up to us.
1: Sure sure, but I mean how did Church define numbers again? I forgot.
0: I think it was:
```
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: Yeah I don't think I'm ready for numbers yet.
0: Why not?
1: Because I have no idea how to justify that definition with the stuff we've built so far.
0: So what should we do next?
1: Dunno.
0: Ok 1st lets decide what to do next. But 0th let's recap what we've implemented so far.
```
##############################
### the λ standard library ###
### by 0 & 1 ###
##############################
if := λa. λb. λc. a b c
true := λa. λb. a
false := λa. λb. b
```
1: Wild.
0: What?
1: Until you renamed the variables, I didn't realize `if` was `λa. λb. λc. a b c`.
0: What's wrong with that?
1: It's like... nothing.
0: Not true. Zero is nothing. We didn't define zero yet.
1: I mean it's so minimal. It's like essentially "not defined."
0: Not true! Not's not defined yet, nor are Nor and And or Or.
1: ZERO STOP RECURSING!
0: It's hard in λ lang. Everything's a recurse word.
1: _(Smiling and frowning at the same time, somehow)_ ... I hate you.
0: What next?
1: Well now that we've got booleans, I guess we could do `and` and `or` and `not` and stuff.
0: Perfect! Let's go.
## 2. Logic and (Logic or (Logic and not not Logic))
> [!Editor's Note]
> The following section uses a somewhat different notation for the λ calculus than the section above, with the section below using `:` and preferring spaces in places where the above section used `.` and no spaces, respectively. Further, while the section above uses `true` and `false`, the § below uses `T` and `F`. Based on these and similar inconsistencies, it has often been suggested that the section below was written by a different Author or Authors than the section above. Were this to be the case, of course, we are consequently forced rather forcefully to the corollary assumption that the Author (or Authors) of whichever-of-these-two-sections-came-after[^4] was (or were) sufficiently familiar with the work of the Author (or Authors) of whichever-of-these-two-sections-came-before[^5] that he (or she (or they)) was (or was (or were))[^6] able to emulate his (or her (or their))[^7] writing style(s) with sufficiently high fidelity that they sound \\
> damn near identical bc both sound pretty weird so it'd be weird if it was 2 ppl writing the 2 things bc idk not many ppl write like that or whatever ok back to the thing.
[^4]: E.N. F.N. 1: (in the historical chronology of the publication and distribution of the document known as `sudocode`, not the chronoloy of the surrounding narrative within the book)
[^5]: E.N. F.N. 2: (same addendum as in supra E.N. F.N. 1.)
[^6]: E.N. F.N. 3: respectively.
[^7]: E.N. F.N. 4: ibid.
1: I'm stuck.
0: Already?
1: I think so. I mean, I don't entirely know how we invented `if` up there.
0: Sure you do! You were there the whole time.
1: I know, but it felt sort of like a shell game.
0: "Shell game" as in `man(6)`? How's it like---
1: No. I mean you're talking as if we're "inventing" or "deriving" all these definitions using some "process."
0: We are!
1: But to be honest I feel like you did some sort of magic trick where you slipped the standard definition into a really long conversation one piece at a time, and then somehow tricked me into thinking that I contributed to some kind of creative process, which I don't really feel like I did, and I don't like that feeling because I _did_ like the feeling I had briefly when I felt like I actually _did_ derive the definition like you said.
0: Can you complain that complaint a bit briefer?
1: I'm not convinced I understand what we just did.
0: Why aren't you convinced?
1: Because I don't know how to repeat it.
0: Repeat what?
1: Like the whole process. We sort of "derived a definition" up there. Seems like an important skill. But I'm not entirely sure what the rules of the game are.
0: There aren't any rules. We're inventing th---
1: Ok but that's not true.
0: Why not?
1: Because if there were really "no rules," then we could just define `and` in λ-lang to be `true` all the time no matter what we pass to it.
0: That's allowed!
1: _Sure but it's a pretty bad definition of `and`!_
0: What counts as a good definition?
1: ONE THAT ACTS LIKE `AND`!
0: Perfect. What does it mean to act like `and`?
1: Obviously, it needs to take two arguments.
0: Well, write that.
1: How?
0: Pseudo-code!
1: But there aren't multiple argument functions in λ-lang zero. And there don't seem to be type signatures or anything at all, at least not anything I can use to write _"this function takes two arguments" _even in pseudo-code.
0: Why not write this?
```
and = λa λb: (?)
```
1: What's the `(?)`
0: I don't know. We haven't decided yet.
1: Ok, now what?
0: What does `and` spit out when we pass two booleans in?
1: Another boolean.
0: Ok, write that for me.
1: Zero I don't know how to write that. This language is insane and it has zero features.
0: Plug in a `T` and `F`.
1: To what?
0: To that `and` we're implementing.
1: Like this?
```
and T F = (??)
```
0: Exactly!
1: What does that prove?
0: You said it yourself up above.
> 0: What does `and` spit out when we pass two booleans in?
>
> 1: Another boolean.
1: So what?
0: Well, that's major progress!
1: How?
0: Because now we know that `(??)` thing you wrote has to be a boolean.
1: How does that help?
0: Well we already implemented booleans right?
1: Yeah.
0: What were they?
1: Weird two argument functions.
0: Mind reminding me how they looked?
1: They were those weird two argument functions remember?
```
T = λa λb: a
F = λa λb: b
```
0: Wonderful progress!
1: How is that progress?
0: You said it yourself. Booleans in λ-lang are two argument functions.
1: HOW IS THAT PROGRESS ZERO?
0: Put two booleans into `and` and `and` returns a boolean right?
1: Yeah.
0: And that boolean it returns is a two argument function, so now we can write this:
```
and T F = λa λb: (???)
```
1: Oh my god I think I'm starting to understand this.
0: Starting to understand `and`?
1: Starting to understand premathematics!
_(Narrator: It's not necessarily mathematics, that's just what it's called for historical re---)_
1: How to derive definitions.
0: What do you feel you understood just then that you didn't befo---
_(Narrator: 1 isn't listening to 0 or to Narrator.)_
1: --can do with this! Like how to get inside Church's head, how to understand what a person would have be _thinking_ to do crazy stuff like defining booleans as two argument functions, why is this not taught? This is the most... I feel like we could do _anything_ with this.
0: You seem excited.
1: Hell yeah!
0: What changed just now?
1: I got it!
0: Explain it to me.
1: Ok, here's how you derive a definition.
You just don't decide on anything about it until you need to.
You do absolutely nothing, then you go ahead and start using it!
The definition I mean.
It's lazy evaluation.
To derive a definition of `and` or `or` or `if_then_else` or `T` and `F` or whatever in an _arbitrarily unfamiliar system,_ you just do nothing -- be lazy -- and start using the def'n _inside the system._
The system will tell you when you need to decide.
Using stuff is the only way to know how it wants to be defined.
_(Narrator: The file falls into a high energy and almost manic (and a bit sweaty) sort of silence.)_
1: I love this! What should we do next?
0: We didn't actually do `and` yet.
1: But I get it now. I totally get it.
0: Want to do the honors?
1: Hell yeah.
Ok so...
```
# 1: Suppose we're Church.
# We're inventing λ-lang.
# We want to define 'and',
# but there's no textbooks
# on λ-lang yet b/c we're
# Church and we're like,
# inventing it ourselves.
#
# Here's how we can derive
# the definition of 'and',
# as if the definition was
# just any old calculation.
#
# 1. Just
# 2. Start
# 3. Using
# 4. It.
#
# For example:
and = ?
# Now suppose we want to
# call it. It takes two
# arguments, because our
# everyday concept of
# 'and' takes two args.
# So now we write:
and = λp λq: (?)
# and it returns a bool,
# and back when we invented
# if_then_else we decided
# that bools are two arg
# functions, like this:
#
# λa λb: (??)
#
# so our choice
# from earlier about how
# to implement bools means
# that now we can write
# this about 'and':
and = λp λq: (some boolean)
# and now we can write
and = λp λq: λa λb: (??)
# and that middle colon
# doesn't actually mean
# anything, we could
# write the same thing
# like this if we wanted:
and = λp λq λa λb: (??)
# now we're done until
# we run into a situation
# where we need more
# things to be true about
# the definition, for
# example, suppose we
# pass in two Ts, like this:
and T T = (λp λq λa λb: (??)) T T
= λa λb: (?? with p and q replaced with T)
# We haven't even written
# the function body yet,
# but it had better be T,
# because if our definition
# of `and` didn't satisfy
# `and T T == T` then it'd
# be a pretty lame definition
# of and. So now we can say:
and T T = λa λb: (?? with p and q replaced with T)
= T # because we insist, right now
= λa λb: a # because of how we defined bools
# So now we know a new thing:
(?? with p and q replaced with T) = a
# where that ?? was the entire
# function body of `and` that
# we didn't even write yet!
# I need some new notation.
# Let's write (stuff) instead
# of (??) and think of it as
# an expression we didn't write
# yet that might have variables
# in it, in places we haven't
# decided on yet.
# So here's what we know so far:
# Fact 1:
#
# and = λp λq λa λb: (stuff)
#
# And we don't know what (stuff) is,
# but we know one thing about it,
# namely:
#
# Fact 2:
#
# stuff(p=T, q=T) = a
#
# Or in other words, whatever stuff
# is, it has to turn into 'a' when we
# pass T into the p slot and
# pass T into the q slot.
#
# To derive more facts, we need to use
# Um...
```
1: Oh no zero I'm stuck again.
0: No you're not.
1: I'm not?
0: Not at all. You know three more things about `and`!
1: Where did they come from?
0: From our intuitive idea of `and`.
1: What are they?
0: Like how `and F T` is `F` and all that.
1: OH! Of course. Wow I really spaced there. Ok back into the code block!...
```
# 1: Right ok...
#
# So now..
#
# Oof, I'm getting kinda tired.
```
1: Zero!
0: I'm here.
1: This is taking forever.
0: That's ok, you're new.
1: But I'm a professional devel---
0: I mean you're new to premathematics.
1: Why do you call it that? "Premathematics"?
0: Just a word I stole from some textbook.
1: Which textboo---
0: There are only like zero textbooks that talk about this whole process -- deriving definitions, I mean -- so I just took the word from the first textbook I ever encountered that actually explained the whole process. Around that time is when I got kinda obsessed with it.
1: I'm kind of loving it too but it's taking forever.
0: That's ok, you're new to it.
1: Is there a quicker way of doing this stuff?
0: Absolutely! Totally changes how you read textbooks, once you get it. It's hard to read a standard mathematics textbook after that without getting mad. The damn things are all half-complete, every one of em.
1: So how would you finish the `and` derivation? I feel like I get it but at this rate it'll take forever to derive the definitions of numbers and data structures and all the other bits of programming.
0: Here, I'll speed us up.
1: Don't skip steps though.
0: Of course. The best thing about premathematics is that once you 'get' it, it feels like every other explanation is skipping steps. But I'll try to skip some of the commentary. If anything's unclear, it's your job to let me know.
1: Deal!...
0: Ok so...
_(Narrator: 0 continues the logic section (of the fifth file (of the lambda calculus section (of the lost+found directory (of the book (or whatever this is))))))_
0: I'd finish up the derivation of `and` like this...
---
![[lambda-premathematics-01.jpg]]
![[lambda-premathematics-02.jpg]]
![[lambda-premathematics-03.jpg]]
![[lambda-premathematics-04.jpg]]
![[lambda-premathematics-05.jpg]]
![[lambda-premathematics-06.jpg]]
---
## 3. Data Structures = (Data, Structures)
![[lambda-premathematics-08.jpg]]
---
## 4. Plus One
### Or: Succ n' friends
### Or: `f`ing one more time
1: Ok this time don't give away the answer. I want to try it myself and see if I get it right.
0: I'm afraid that's not how this works.
1: You're gonna tell me the answer against my will?
0: No, I mean it's not up to me to say what's right. We're implementing the language remember?
1: But how will we know if we get it right?
0: Same as any code. We just have to use it and see if we hate it enough to refactor.
1: Makes sense. Where do we start?
0: Well I think I'll start with zero and one. You can start with whomever you like.
1: You're an idiot.
_(Narrator: 0 and 1 each work independently on their own definitions of zero and one.)_
1: Got one.
0: One sec, I'm not done typing yet.
_(Narrator: The 0 character types a few more characters.)_
0: Ok I'm done.
1: How did you do it?
0: I did this.
```
0 = λaλb.b
1 = λaλb.a(b)
2 = λaλb.a(a(b))
3 = λaλb.a(a(a(b)))
```
0: What did you do?
1: I didn't see the point of having two variables. I just used one. Like this:
```
0 = λa.a
1 = λa.a(a)
2 = λa.a(a(a))
3 = λa.a(a(a(a)))
```
0: Hmm.
1: Which definition is better?
0: I dunno.
1: How do we find out?
0: I think we just have to use both and see which one we like better.
1: How do we "use" them?
0: I dunno, let's try to add one.
1: Add me?
0: No, I mean let's try succ.
1: Do what now?
0: This. Successor. Like the function f(n) = n+1.
1: Oh ok, I misheard. Isn't `succ n` just
```
succ n = a(n)
```
So like
```
4 = a(3)
```
Or for your definition, since
```
3 = λfλx.f(f(f(x)))
```
Wouldn't we just have
```
4 = f(3)
```
Like wrap one more copy of the function around it?
0: I dunno, substitute in the definitions of 3.
1: Ok.
```
4 = a(λa.a(a(a(a))))
```
Wait, I'm confused. Is having the lambda inside like that is allowed? This feels wrong.
0: Hey 1, I made progress! Come look!
_(Narrator: 1 goes over to see what 0 accomplished.)_
1: Zero, you just wrote
```
succ n = ?
```
1: That's not progress.
0: I think it is.
1: Ok then.
_(Narrator: 1 quickly writes a few characters.)_
1: _(Sarcastically)_ "Hey 0 I made progress."
0: Great! Let me see.
_(Narrator: 0 goes over to see what 1 accomplished.)_
0: Beautiful!
1: _(Confused)_ I was being sarcastic. I didn't do anything.
0: Sure you did!
1: Zero, I literally just wrote
```
succ n = m
```
1: I was making fun of you. This isn't progress.
0: I think it's wonderful progress.
1: You're acting weird again. Why is this 1derful?
0: Well we haven't agreed on which definition of numbers to use yet, but we each have our own definition, so I can do this:
```
succ = λn λ? λ? (stuff)
```
1: Explain?
0: Well whatever succ is, we know it takes an number n and spits out a number m. So I turned
```
# this
succ n = m
# into this
succ = λn (stuff)
# and since it spits out a number m,
# that (stuff) bit has to be a number,
# and since numbers in my definition
# are two argument functions, I wrote
succ = λn λ? λ? (stuff)
```
1: Are those question marks the same question mark or different question marks?
0: Different. I guess that wasn't clear. Here:
```
succ = λn λf λx. (stuff)
```
0: This isn't really saying anything new. It's just the idea that succ returns a number too, and my numbers are functions of two arguments. Now we just have to implement the `(stuff)`!
1: Isn't that the entire problem? How is this progress?
0: Or course it's progress! Now we know how to undress the numbers!
1: Un-what the who now?
0: You had a good idea about wrapping the function around one more time, but you were wrapping it around the outside. Now that the numbers are naked, no more lambdas wrapped around them, maybe we can add the extra copy of `f` down here.
1: Like how?
0: Watch.
```
succ = λn λf λx. f(n)
```
1: Wait I think this has the same problem as mine. That `n` has lambdas on it.
0: Show me?
1: Here look.
```
3 = λf λx. f(f(f(x))
```
So
```
3 g y = g(g(g(y)))
```
0: What are `g` and `y`?
1: I used different letters because I wasn't sure if I'm allowed to plug `f` and `x` into a thing that already has those.
0: I think it should be ok.
1: Ok then I just meant this:
```
3 f x = f(f(f(x)))
```
0: Great! Or in general:
```
n f x = naked n
```
0: So now
```
succ = λn λf λx. f(naked n)
```
Or
```
succ = λn λf λx. f(n f x)
```
1: Ok wait, in my definition of numbers, I'd have:
```
succ = λn λa. a(naked n)
```
Or:
```
succ = λn λa. a(n a)
```
0: Wonderful! We're done!
1: With what?
0: We both know how to `succ` any number.
1: But we didn't even agree on how to define numbers yet.
0: That ok! Even if we're succ'ing different things, at least we're both succ'ing something.
1: Now what?
0: Well what else can we do with two numbers?
1: The usual stuff I guess. There's:
- addition
- multiplication
- exponentiation
- subtraction
1: Shouldn't be too hard.
---
## 4. Plus One (One More Time)
### Or: How to Undress a Number
### Or: One more `f`ing time
```
1: Why not this?
succ := λn. λf. f n
0: What's the motivation?
1: I mean based on how we defined numbers, "+1" should just be "wrap another f around it."
0: I'm not sure that's what you did there.
1: How is that not what I did?
0: You're trying to define something like this right?
0 ≈ x
1 ≈ f(x)
2 ≈ f(f(x))
3 ≈ f(f(f(x)))
1: Why the squiggly equals signs?
0: I just meant "You're trying to do that, but without the f and x being free variables" right?
1: Yeah exactly.
0: So let's just toss some lambdas outside.
1: What's the point of that?
0: I dunno. It'll get rid of the free variables.
1: Ok, here:
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)))
0: I'm still not sure how to define "+1".
1: Just wrap another f around it.
0: Around the outside?
1: Sure.
0: Like this?
5 := f( λf. λx. f( f (f (f x))))
1: Oh yeah, I guess that's wrong.
0: It's not too wrong though, we just need to wrap the f around the inside.
1: How do we do that if we only have 3 system calls?
0: System calls?
1: Yeah. So far it seems like we only have three.
0: What do you mean?
1: Like this:
System Calls
============
1: mkvar: takes a str, makes a var
2: mkfun: takes a var x and an expr e, makes λ x: e
3: rmvar: takes a fun f and an expr e
0: Hadn't thought of it like that. What do you mean by "str" and "var" and "expr" and "fun"?
1: Obviously, that's "string" and "variable" and "expression" and "function".
0: No no, I mean we only have functions.
1: Sure fine, I mean know there's only one type, but I figured we could just pull an Alonzo Church and give the one type 3 or 4 different names, depending on how we're thinking about it. It's really all the same type though. Everything's Alonzo Church. I mean functions.
0: Ok, as long as it's just following the laws of Alonzo Church.
1: So then how do we define "+1"?
0: Well I think your system calls idea solved it.
1: How so?
0: Here look. We tried this, but it was clearly wrong.
5 := f( λf. λx. f( f (f (f x))))
0: So to make it right, we just need to get that f inside somehow.
1: How do we do that?
0: With your system calls! Look:
Supposing we start with, say, the number four, namely:
4 := λf. λx. f( f (f (f x)))
Then we can get to five like this:
4 = λf. λx. f( f (f (f x)))
rmvar 4 = λx. f( f (f (f x)))
rmvar (rmvar 4) = f( f (f (f x)))
f(rmvar (rmvar 4)) = f( f( f (f (f x))))
mkfun( f(rmvar (rmvar 4))) = λx. f( f( f (f (f x))))
mkfun( mkfun( f(rmvar (rmvar 4)))) = λf. λx. f( f( f (f (f x))))
1: I don't think you used my syscalls right.
0: (Zero checks the syscall signatures) Oh, oops.
1: But I think I get your idea. Can I define some terms?
0: Always!
1: Ok so:
undress(4) = f( f (f (f x)))
f(undress(4)) = f( f( f (f (f x))))
redress(f(undress(4))) = λf. λx. f( f( f (f (f x))))
And that's 5.
0: I don't think that's what redress means.
1: What?
0: Here look.
re·dress /rəˈdres/
1. (verb) To remedy or set right (an undesirable or unfair situation).
2. (noun) A remedy or compensation for a wrong or grievance.
1: Yeah exactly. That's what I meant.
0: How is that what you meant?
1: Well we didn't ask permission to undress these numbers, so naturally thr redress step is how we make amends.
0: You're the weirdest student I've ever ha---
1: Whatever. Look, we did it!
succ(n) = redress(f(undress(n)))
0: And now we can remedy or set right the crime we just committed against terminology by rewriting it like this:
succ := λn. λf. λx. f (n f x)
1: How is that the same?
0: It's clearly the same.
- The succ function takes a number n.
That's the λn bit.
- Then it returns a number,
which is a two argument function.
That's the λf. λx. bit.
- That accounts for the function signature.
- Now the internals of the function are just:
f (n f x)
- And f (n f x) is the same as f(undress(n))
1: How is f (n f x) the same as f(undress(n))?
0: I'm just plugging in values that happen to have the same names as the function's parameters. That's how we undress any number n. Just feed it an unspecified thing named f, and another unspecified thing named x.
1: Got it! What about the redress step?
0: I already took care of that in the lambdas. I just reasoned in reverse, compared to what you did. The redress is the bit where I explained where the
λn. λf. λx.
bits come from.
1: Great! Now how do we add numbers?
0: We just did that.
1: No no, I mean how do we add numbers other than 1?
```
---
## 5. Arithmetic Succs
### Or: Taking bits out
### Or: Whine and Din
### Or: pow n m = m n
![[lambda-premathematics-09.jpg]]
![[lambda-premathematics-10.jpg]]
![[lambda-premathematics-11.jpg]]
![[lambda-premathematics-12.jpg]]
![[lambda-premathematics-13.jpg]]
![[lambda-premathematics-14.jpg]]
![[lambda-premathematics-16.jpg]]
![[lambda-premathematics-17.jpg]]
![[lambda-premathematics-18.jpg]]
![[lambda-premathematics-19.jpg]]
![[lambda-premathematics-20.jpg]]
![[lambda-premathematics-21.jpg]]
---
## 6. Arithmetic Succs (Hard)
### Or: How to Un-succ
### Or: Taking off ones
### Or: Taking an `f`
### Or: Not giving an `f`
### Or: `f`ing one less time
### Or: Harder than it looks
### Or: Too much for Church
### Or: Don't be so positive
0: Well Church himself didn't actually think this was enough to capture ALL of computation!
1: He didn't?
0: Hell no! You'd have to be insane to think that this was ALL of computation the first time you see it. I mean Church _came up_ with this idea and even HE didn't think that.
1: How do you know?
0: From Steve.
![[reminiscences-of-logicians-009-1.jpg]]
1: What does it mean "convinced himself there wasn't"?
0: Church didn't think it was possible to implement the function `x-1` in lambda calculus.
1: What?!
---
## Reminiscences of Logicians: What Church was Thinking
### Or: Predecessor ~~might be impossible~~ is hard
### Or: Kleene at the Dentist
### Or: Kleene of Teeth
![[reminiscences-of-logicians-004.jpg]]
![[reminiscences-of-logicians-005.jpg]]
![[reminiscences-of-logicians-006.jpg]]
![[reminiscences-of-logicians-007.jpg]]
![[reminiscences-of-logicians-008.jpg]]
---
![[lambda-premathematics-24.jpg]]
![[lambda-premathematics-25.jpg]]
---
![[reminiscences-of-logicians-009-1.jpg]]
![[reminiscences-of-logicians-009-2.jpg]]
![[reminiscences-of-logicians-009-3.jpg]]
![[reminiscences-of-logicians-010.jpg]]
---
## 6. Lambda the Ultimate
### Or: The L||D's Programming Language
### Or: In the beginning was the W||D
### Or: W||d implies W|ld
### Or: λολγοes the λογος
![[lambda-premathematics-07.jpg]]
![[lambda-premathematics-22.jpg]]
![[lambda-premathematics-23.jpg]]
---
## Reminiscences of Logicians: Church's Thesis
![[reminiscences-of-logicians-015.jpg]]
## Reminiscences of Logicians: Post Script
### Or: Post Haste
### Or: Post Mortem
### Or: Publish or Perish
### Or: Protest against this habit of Not Publishing
### Or: Missing bits
> _Emil Leon Post (/poʊst/; February 11, 1897 – April 21, 1954) was an American mathematician and logician. He is best known for his work in the field that eventually became known as computability theory._
>
> -The Dynamic Read-Writable Free Encyclopedic Repository of the Modern State of Human Knowledge
![[reminiscences-of-logicians-029.jpg]]
> _While at Princeton, Post came very close to discovering the incompleteness of Principia Mathematica, which Kurt Gödel proved in 1931. Post initially failed to publish his ideas as he believed he needed a 'complete analysis' for them to be accepted._
>
> -The Dynamic Read-Writable Free Encyclopedic Repository of the Modern State of Human Knowledge
![[reminiscences-of-logicians-030.jpg]]
> _Post had been interested in astronomy, but at the age of twelve lost his left arm in a car accident. This loss was a significant obstacle to being a professional astronomer, leading to his decision to pursue mathematics rather than astronomy._
>
> -The Dynamic Read-Writable Free Encyclopedic Repository of the Modern State of Human Knowledge
![[reminiscences-of-logicians-031.jpg]]
> _In \[the logic of inductive inference\], censoring is a condition in which the value of a measurement or observation is only partially known._
>
> -The Dynamic Read-Writable Free Encyclopedic Repository of the Modern State of Human Knowledge
![[reminiscences-of-logicians-030.jpg]]
> _Post spent at most three hours a day on research on the advice of his doctor in order to avoid manic attacks, which he had been experiencing since his year at Princeton._
>
> -The Dynamic Read-Writable Free Encyclopedic Repository of the Modern State of Human Knowledge
![[emil-post.jpg]]
> _He died in April 1954 of a heart attack following electroshock treatment for depression._
>
> -The Dynamic Read-Writable Free Encyclopedic Repository of the Modern State of Human Knowledge
![[reminiscences-of-logicians-026-1.jpg]]
---
## Gödel arrives on the Scene
> Steve Kleene: The first thing we knew of Gödel's paper was one time the mathematics colloquium speaker was gonna be von Neumann. And of course von Neumann had lots of things of his own to talk about but instead of that we got him there and found out he was telling us about Gödel's 1931 results.
>
> Someone: This was at Princeton?
>
> Steve Kleene: This was at Princeton and it was in the Fall of 1931. And whether he had the paper itself or not I don't know...
>
> C. C. Chang: Was this the first you'd heard of Gödel?
>
> Steve Kleene: When we went into this meeting was the first that any of us heard of Gödel. Church was teaching a logic course, Rosser and I were among the students, it was the first that any of us had heard of Gödel. I don't know whether Church was aware of Gödel's 1928 paper on completeness, he never gave it in class, because I... I never had the classical form of the propositional or predicate calculi in my coursework, I learned them for myself afterwards.
>
> Steve Kleene: So as soon as we heard the lecture, the paper was available. We hadn't noticed it, y'know, we didn't go looking at every journal that came into the library to search it through for papers that would interest us, maybe we should've but we didn't, so of course we went and we read the paper right off.
goto: [[lost+found/4/1]]