## The λogos calls ### Or: Calls Calls Calls ### Or: Numbers are calls ### Or: Booleans are calls ### Or: No names allowed ### Or: Church of λambda ### Or: On the λamb ### Or: Son of Sam 0: Once upon a time, there was a guy named Sam. 1: Ooh I love story time. 0: Sam had an unusual family tree. As a child, during that earliest stage of life when we're looking around the world for the first time and learning what things are called, Sam learned the following: 1. Your Name: Sam 2. Your Father: Alonzo Church 3. Your Brother: Alonzo Church 4. Your Grandfather: Alonzo Church 1: That's a lot of Alonzo Church. 0: For real. And Sam wasn't Alonzo Church. He was the only one who wasn't. 1: Must be rough to get excluded from being Alonzo Church when everyone you know gets to be that. 0: Exactly. So when it came time for Sam to have a son, he pulled a fast one on his brother -- the first born -- and added an item of his own to own the family's family tree. So now, thanks to Sam, the family tree looked like this. 1. Your Name: Sam 2. Your Father: Alonzo Church 3. Your Brother: Alonzo Church 4. Your Grandfather: Alonzo Church 5. Your Son: Alonzo Church 1: Damn Sam. That's cold. 0: "Take that, Alonzo Church," I imagine him saying to his brother Alonzo Church, when he named his son Alonzo Church. 1: Did he actually say that? 0: No idea. But eventually Sam's son would have a son of his own. And he called--- 1: I wonder what he's gonna call it. 0: Drumroll. 1. Your Name: Sam 2. Your Father: Alonzo Church 3. Your Brother: Alonzo Church 4. Your Grandfather: Alonzo Church 5. Your Son: Alonzo Church 6. Your Grandson: Alonzo Church 1: Why are we talking about this? 0: Because trinities are known to be full of mysteries. And Alonzo Church is the first member of our trinity. 1: All five Alonzo Churches are members of the trinity? 0: No. Just one. 1: Which one? 0: Sam's son. The one who wasn't supposed to be Alonzo Church. 1: I'm glad it was that one. He seemed like the underdog. 0: Alonzo Church would go on to do a lot of things, but he's most well known for one thing. 1: What one thing? 0: For inventing the first programming language. 1: Woah seriously? 0: Before computers. Before the field even had an agreed upon definition of "computation." 1: What did it run on? 0: Paper. 1: Woah. 0: It was a strange programming language with only one type. 1: Only one type? 0: Only one type. In terms of built-in types, the language has no numbers. 1: No numbers?! 0: No booleans. 1: No booleans?!?! 0: No `if` or `for` or `while`. 1: This language sounds insane. 0: There's only one built-in type. 1: Is it Alonzo Church? 0: Nope. But Alonzo Church had a lot of experience with systems where everything is one type. 1: Like his family? 0: Yep. So when he grew up and went into the foundations of mathematics, and even more deep into the foundations of logic itself, he came up with a system where everything is functions. 1: Numbers are functions?! 0: Numbers are functions. 1: Booleans are functions?!?! 0: Booleans are functions. 1: Such an Alonzo Church thing to do. 0: It's not as crazy as it sounds. It's actually an incredibly powerful idea. He just didn't realize that at the time. 1: HE didn't realize that? 0: Nope. No one did. 1: Can I have some more details? 0: Of course. Let's go take a tour. ![[church-01.png]] 1: Woah you weren't just making that up? 0: Of course not. I would never lie to you. ![[church-03.png|400]] 1: Hey there's another one! 0: Told ya. They're all over the place. ![[church-02.png]] 1: Damn look at that handsome guy. 0: For real. Could have gone into Hollywood. 1: Why didn't he? 0: Well he's a foundational person. So naturally, he went into foundations. ![[church-04.png]] 0: Did his dissertation on the Axiom of choice. 1: What's that? 0: Well remember, by this time, it's been about 50 years since Cantor, and almost 30 years since 1900 when Hilbert announced his list of problems. So there's been a reasonable amount of work on the foundations of mathematics since then. 1: Why aren't we including those people in "The foundational people"? 0: Good point. Some of them probably deserve to be included too. But every story has to start somewhere, and for a bible on the history of computing, Church is a pretty good place to start. 1: What was going on in the 30 years before this? 0: Well there had been some work on axiomatic set theory. Mostly on a system called ZFC, or Zermelo Fraenkel (with the Axiom of) Choice. That system is still considered the "official" foundations of mathematics by mathematicians today, but it's never really been _used_ as foundations in any real sense. 1: What do you mean "used as foundations." 0: I mean nobody uses it. 1: What?! 0: Or almost nobody. They usually just talk about it or assert that ZFC proves such-and-such. It's extremely rare to see mathematicians actually working _within_ ZFC as a formal system. 1: That doesn't seem so bad. I mean we programmers don't really write in machine code, like ever. But it's sort of the "foundations" of any language that compiles to it, in a sense. 0: No no, I mean even books about ZFC don't work within ZFC. 1: WHAT?! 0: Here I'll show you.