Types and Programming Languages Chapter 5 The Untyped Lambda Calculus
In the previous chapter, when we wanted to enrich our language, we had to add an increasing number of specific evaluation rules. If, instead, we use the Lambda Calculus as our language, we can use only a few evaluation rules and leverage the power of the calculus to express extremely powerful language features on top of this "computational substrate".
t ::=
x // variable
λx.t // abstraction
t t // application
Abstraction is analogous to a function definition:
function (n) { t }
λn. t
Application is analogous to a function call:
(function (n) { t }(x))
(λn. t) x
s t u = (s t) u // application associates to the left
λx. λy. x y x = λx. (λy. ((x y) x) // abstraction bodies extend to the right
x is free when it is not bound by an enclosing abstraction on x, e.g.
x y
λy. x y
x is bound:
λx. x
λz. λx. λy. x (y z)
The first x is bound and the second is free:
(λx.x) x
A term with no free variables is closed (also called a combinator):
id = λx.x
Tom lead us in a discussion of the notion of "free" and "bound" variables in terms of a graph where "bound" variable can be thought of as a pointer to an ancestor that declares an abstraction with that variable. In these cases, the name of a variable (e.g. x or y) is irrelevant as it is only really useful for writing down the terms but they are better modelled as pointers to one another.
"Free" variables on the other hand have no ancestor abstraction in the graph and might be considered as pointers into some unseen global environment.
We discussed beta reduction and several different strategies in some detail by working through the given example term (without the potentially confusing id shorthand given in the chapter):
(λx.x) ((λx.x) (λz. (λx.x) z))
Under the normal order strategy, the leftmost, outermost reducible expression is always reduced first.
(λx.x) ((λx.x) (λz. (λx.x) z))
------------------------------
→ (λx.x) (λz. (λx.x) z)
---------------------
→ λz. (λx.x) z
--------
→ λz.z
The call by name strategy is yet more restrictive, allowing no reductions inside abstractions.
(λx.x) ((λx.x) (λz. (λx.x) z))
------------------------------
→ (λx.x) (λz. (λx.x) z)
---------------------
→ λz. (λx.x) z
Most languages use a call by value strategy, in which only outermost reducible expressions are reduced and where a reducible expression is reduced only when its right-hand side has already been reduced to a value — a closed term that is finished computing and cannot be reduced any further.
(λx.x) ((λx.x) (λz. (λx.x) z))
-----------------------
→ (λx.x) (λz. (λx.x) z)
---------------------
→ λz. (λx.x) z
A subtlety here is the notion of "value" which currently only describes abstractions and no other types of term (that is, neither variables nor applications).
tru = λt. λf. t;
fls = λt. λf. f;
We briefly discussed defining the concept of the booleans true and false as functions that take two arguments and return the first if true and the second if false. This matches how we typically define the conditional if, e.g.
function tru(t, f) { return t; }
function fls(t, f) { return f; }
if true then t else f
if false then t else fWe discussed the lack of some sort of input value into the Lambda Calculus and how that might explain the design of booleans: Tom made the point that the notions of true and false typically only exist in a program to eventually be used in some sort of function application, e.g. in an if statement to choose between two branches of a program.
We walked through the initially confusing substitution notation in the book and touched on how it adds significant power to our evaluation rules.
Taking the following definition:
(λx.t12)t2 ⟶ [x ↦ t2]t12
We applied it to a JavaScript example:
function (x) { x * 2 }(21) λx.
------------
function (x) { x * 2 }(21) t12
---------
function (x) { x * 2 }(21) t2
----
function (x) { x * 2 }(21)This means that:
[x ↦ t2]t12
Is equivalent to the following in our example:
[x ↦ 21]x * 2
Giving us:
21 * 2
We finished the meeting by talking through the inference rules presented in the book that describe the call-by-value strategy for evaluating our programs.
We worked through an example of identifiying the values and terms in an expression:
(λx. x) ((λx. x) (λz. (λx. x) z))
Then applied the inference rules to reduce the expression. We realised that it wasn't obvious on first reading, but the inference rules for call-by-value are mutually exclusive. If you can apply any rule to an expression there is only one rule you can apply.
We then tried the exercise to re-write the inference rules to describe full beta reduction.
Mostly this required us to replace references to values in the rules with references to terms and this showed us that we now had a choice of which rule to apply at any given moment. The final rule we added was E-ABS:
t1 → t1ʹ
----------------
λx. t1 → λx. t1ʹ
There was some confusion in the room about why this was necessary. We explained that this is because the other rules do not apply to an abstraction like λx. x. They only apply to two terms next to each other and λx. x is not two terms next to each other, it is a single term made of λx. (the function signature) and x (the function body). We need E-ABS to explicitly break up this term and let us "go inside" the abstraction to work on the function body x.
- There was concern that a few people dominated the conversation and that others might have been left behind: a quick temperature reading across the room revealed that people were following along but that we must continue our focus on shared understanding over being completionist;
- No one volunteered to be a dedicated notetaker this meeting as it is quite a big commitment and effectively takes that person out of the meeting for its duration;
- We spent a lot of time going through the start of the chapter in detail but had to speed through the main bulk of it due to time constraints: could we better plan ahead of time how we want to spend our time in the meeting? There was an attempt on Slack to do this but there were no responses: perhaps formally voting for different tacks to take would help but requires someone choose multiple options ahead of time?
- After the meeting, there was no agreement who would announce and arrange the next meeting, shall we bring back the role of volunteer organiser to handle creating an Attending.io page, announcing it to the mailing list and Twitter, etc.?
- The next meeting was originally meant to be our first "interstitial", non-TAPL meeting but as we are in the midst of the untyped Lambda Calculus topic, we all agreed to postpone that and spend the next meeting implementing the calculus based on Chapters 6 and 7.
Thanks to Leo and Geckoboard for hosting and lending use of their bread knife. Thanks to all those who provided snacks, especially James for his homemade Lambda Focaccia.