| Playlist | schedule page slides as PDF |
Encoding 1 — let and arguments (2:54)
Local bindings via let and multi-argument functions both can be considered syntactic sugar over functions. We’ll use this idea from now on.
Encoding 2 — booleans and pairs (4:35)
Instead of adding booleans and pairs to our language, they can be encoded using functions. We won’t use these encodings much, but you should understand them.
Encoding 3 — λ-calculus (1:08)
The λ-calculus is an even simpler language than the one that we’ve been implementing. It’s a Turing-complete language that was invented by Alonzo Church in the 1930s.
Encoding 4 — numbers (8:10)
Numbers can be encoded as functions. We look at a particular encoding known as Church numerals. It’s ok if you don’t get all the details, as long as you get the general idea that numbers can be encoded in functions just as well as they can be encoded in bit patterns.
Encoding 5 — recursion (4:05)
Recursive functions can be encoded using non-recursive binding forms.
Encoding 6 — Y combinator (4:20)
Abstracting the recursive-function pattern into a form that could be implemented as syntactic sugar. It’s ok if you don’t get every detail of the derivation, as long as you understand that mk-rec can be used to construct a recursive functions. The mk-rec function is a variant of the Y combinator. For other presentations of the derivation, search the web for “the why of Y.”