## (3,5): Church's Language
### Or: What Church was thinking
### Or: Take Me To Church
### Or: Implementing λ lang
### Or: Premathematics of λ
### Or: Be My Church
### Or: BMC
1: Wait. How can do programming in the language if we haven't written the language yet?
0: Y'know. Pseudo-code.
1: Does that count as programming?
0: Of course! If we didn't write code before it existed, how would we know how we wanted it to behave?
1: Makes sense.
0: Where would you like to start?
1: Definitely not with numbers. That definition scared me. If we're gonna start with programming, I'd rather start with simpler stuff, like `if then else` and then maybe some data structures after that.
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. 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 in that code?
0: I mean if `if` is a function, then it takes three things:
1. A boolean called `if`.
2. A code block called `then`
3. A code block called `else`
1: Can we call the boolean something different? This is hurting my head.
0: Sure, refactor however you want.
1: Ok how's this?
```
def if_then_else(condition, then_do_a_thing, else_do_b_thing):
# Ok this is gonna be a problem...
# Ummmmmmmmmmmmmmmmmmmmmmmmmmmm...
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. 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! I was trying to write a normal function call, I just pronounced it with a shell accent.
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 this 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: Well 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
##################
### Your 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.
################
### My 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. 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. 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.
1. `sed s/def //g`
2. 1. `sed s/function_name/function_name = /g` (and then apologize and say "We don't technically have equals but I'm going to do it anyway", which is what everyone does)
3. `sed s/(/λ/g`
4. `sed s/, */λ/g`
5. `sed s/)//g`
6. `sed s/:/./g`
7. `sed s/return//g`
1: Simple enough.
_(Narrator: 1 runs the seds.)_
1: Ok I did everything you said. Here:
```
if_then_else = λcλaλb.
cλaλb
```
1: Is that right?
0: No.
1: Where did I mess up?
0: You didn't. My instructions were wrong, but we're like four backspaces and two spaces away from this being valid Church. Here:
```
if_then_else = λcλaλb.c a b
```
1: What's going on here?
0: It's just Church-lang. 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)
```
but technically in order to be Gramatically Correct Church (or gcc) that compiles correctly (or cc) we have to replace all the multiple argument functions with single argument functions returning functions, like this:
```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?
0: This:
```
if_then_else = λcλaλb.c a b
```
1: Ok...
```
# 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 in
= (λb.true A b)(B) # pass the A in
= (true A B) # pass the B in
= true A B # this is probably allowed, idk...
```
1: Now what?
0: Well we already defined `true`, 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 those steps I did above
= true A B # now let's plug true into true ._.
= (λ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 language.
```python
# This was our `false` in pseudo-code
def false(a, b):
return b
# 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 all three in this time
= (λaλb.b) A B # by our definition of false
= (λb.b) B # plug in the A
= B # now (λb.b) is the identity function, so we get B
```
0: It's false!
1: I messed up?
0: No! I mean 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: Good call.
0: 1st lets implement numbers. But 0th let's recap what we've implemented so far.
```
##############################
### the λ standard library ###
### by 0 and 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 And and Or and Nor.
1: ZERO STOP RECURSING!
0: It's hard in λ lang. Everything's a recurse word.
1: 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))
## 3. Data Structures = (Data, Structures)
## 4. Arithmetic (Succ n' friends)
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
- should we do subtraction maybe?
## 4.5: Arithmetic Succs
### Or: Predecessor turns out to be surprisingly hard
### Or: Kleene at the Dentist
### Or: Kleene'ing Teeth
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.
TODO: 6:50. Church didn't think it would be possible to implement predecessor in lambda calculus. Kleene realizing how to implement predecessor at the dentist.
TODO: 7:15.
> Steve Kleene: So there was no idea at the beginning that this was going to be all effectively calculable functions.
TODO: 7:30.
> Steve Kleene: I kept taking it as a challenge and everything I tried I could work.
TODO:
> Steve Kleene: It was an unexpected fallout that this could represent all effectively calculable functions.
TODO:
> Steve Kleene: The basic work was done between January 1932 and the next 5 or 6 months.
TODO:
> Steve Kleene: Everything I tried, every kind of function I tried to define, every kind of effective operation that I tried to parallel by lambda definability, I probably knocked off within the first 5 months.
TODO:
> Steve Kleene: For us the first concept of lambda definability was after the fact, after having formulated the notion of lambda definable functions as simply the ones for which you could find formulas in this symbolism. And discovering that everything you thought of that you wanted to prove lambda definable you could!... But it was Church, I have to give the credit to Church, I can't take it myself, he said "Y'know, don't you think maybe we've really got ALL the effectively calculable functions?"
## 5. Cursing and Recursing
## 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]]