Lambda-Calculus and Combinators, an Introduction
2nd Edition
J. Roger Hindley and Jonathan P. Seldin
Cambridge University Press, 2008
Hardback, ISBN-13: 9780521898850, $ 70.00
What is new compared to the first edition?
The title, a little bit.
The much more modern type setting.
The order of what I call the three parts of the book:
in the new version first the untyped systems,
then the typed systems, and finally the model theory.
In the old version it was untyped systems,
model theory, typed systems.
An inspection of both tables of contents further reveals
that most chapters have the same structure as in the
first edition; in a few cases a section is added.
Two chapters have been removed from the first edition:
Logic based on combinators, and
Gödel's consistency-proof for arithmetic.
The part concerned with typed systems
has been rewritten considerably.
Moreover, the formal details concerning renaming of
bound variables are moved from the introduction
to -calculus to a new separate appendix.
So the second edition differs quite significantly from the first.
The book consists of 16 chapters and 5 appendices.
I see the chapters as divided into three parts.
The first part, Chapters 1-9, is concerned with the syntax,
expressivity, theories, and extensionality of
untyped -calculus and Combinatory Logic (CL).
Then we switch to the typed setting in
the second part, Chapters 10-13.
This part treats simple typing à la Curry and à la Church
quite extensively, and general typing systems more shortly.
The third part, Chapters 14-16, turns back to the untyped world
by presenting models for
-calculus and CL.
Chapter 1 introduces untyped -terms, substitution,
-reduction and
-equality.
The section concerning substitution cites mainly the
book by Curry and Feys from 1958 as source,
and refers to Appendix A1 for details of proofs.
The sections concerning
-reduction and
-equality treat the Church-Rosser property
and confluence, and refer for proofs to Appendix A2.
The chapter contains some nice exercises.
I liked in particular the exercises concerning normal
forms and substitutions:
find terms
and
such that
has a normal form but M does not,
and, a harder one: find
and
such that
neither of
and
has a normal form, but
has one.
What I missed in this chapter is the representation
of a
-term as a tree; something I find often
helpful for myself and in teaching.
Chapter 2 introduces untyped Combinatory Logic
(CL) terms, weak reduction induced by the rules for
the combinators ,
, and
,
and weak equality.
There are no issues concerning bound variables now.
For proofs of confluence the reader is again referred to
Appendix A2.
Abstraction in CL is defined, but combinatory completeness
is not yet shown.
Chapter 3 is concerned with both -calculus and CL,
and starts by giving a fixed point combinator for both systems.
Here abstraction in CL, defined in Chapter 2, is used, and
combinatorical completeness of CL is given as a corollary
of the fixed-point theorem.
The next topic concerning expressivity is
Böhm's Theorem, stating that syntactically different
-normal forms can be distinguished by their behaviour.
The statement makes use of the notion of
-reduction
for
-terms, and strong normal forms for CL.
Both are defined in this chapter (one can imagine looking
for them in Chapters 1 and 2).
Then the quasi-leftmost reduction theorem is given,
stating that by contracting repeatedly the leftmost redex
the normal form of a term, if it exists, will be reached.
The `quasi' means that such a rewrite sequence may even
be `polluted' by steps that are not leftmost.
This section contains a definition that I found rather
puzzling: it states that a reduction has maximal length
if it is either infinite or ends in a normal form.
Now the reduction
is clearly not the longest possible,
however, it has maximal length according to the
definition.
The word length in the definition is the thing that
confuses me.
The chapter concludes with an interesting and quite lengthy
discussion,
first on the history of
-calculus and CL, and their
role in logic and computer science,
and then more in particular on the interpretation of
their (untyped) terms as operators.
Chapter 4 continues the study of expressivity
by showing that all
partial recursive functions can be represented
in -calculus with
-equality
and in CL with weak equality.
The presentation is careful and detailed and
hence very suitable for teaching.
The chapter also shortly discusses
representing arithmetic using an iteration operator.
Chapter 5 is a rather short chapter in which a general
undecidability theorem is proved.
This theorem states that no pair of non-empty sets
of terms closed under conversion is recursively separable,
both for the -calculus with
-conversion
and for CL with weak conversion.
Two important corollaries are:
first,
given a term there is no recursive way of deciding
whether it has a normal form,
and second,
given two terms there is no recursive way of deciding
whether they are convertible or not.
These results, here stated as corollaries of a more
general theorem, led Church to proving
the undecidability of first-order predicate logic.
Chapter 6 is a proof-theoretic account of the
formal theories of -calculus with
-equality and CL with weak equality.
The word `formal' means that now these theories
are presented using axioms,
as for instance
,
and rules of inference.
So now one can derive statement such as
,
and one can talk about issues like
admissible and derivable rules, and equivalence of theories.
Equivalence of theories is used later in the book
for instance to talk about equivalent formalizations
of extensionality.
So I understand the use of the material presented in
this chapter, but for me, it would not get top-priority
in teaching untyped
-calculus.
Chapter 7 is concerned with extensionality in -calculus.
It starts by presenting two rules and one axiom that
have been proposed as a formalization of extensionality
in
-calculus.
The rule
roughly states that if
applied to
equals
applied to
, for a fresh variable
,
then
equals
.
The rule
states that if
for all
,
then
.
Finally, the axiom
states
with the side-condition that
is not free in
.
Now the terminology of Chapter 6 concerning rule-equivalence
of formal theories is used to state and prove
that
is as strong as
and
.
The chapter then continues with a short study of
-calculus with
-reduction, showing
confluence, hence uniqueness of normal forms,
and
-postponement.
The proofs of confluence are given in Appendix A2.
Chapter 8 treats the rather subtle subject of extensionality in CL.
The theory of weak equality is extended to an extensional
theory in two different ways: by adding an axiom
, similar to
for
-calculus,
and by adding
, also similar to the
-rule for
-calculus, with the difference that abstraction
in CL is no syntax but a meta-notation.
One can instead add a rule
, similar to the
-axiom
for
-calculus, but this axiom holds in CL as
an identity.
Equivalence of adding
or adding
is proved,
which is not hard.
Then the issue whether there is a reduction theory for
extensionality, like
-reduction in
-calculus,
is tackled.
This leads to the notion of strong reduction,
for which confluence is proved, but,
as the authors remark,
it is a bit worrying that this proof uses the
translation between
-calculus and CL.
Chapter 9 is the last chapter of what I consider
the first part of the book, concerned with untyped
-calculus and CL.
It treats
the correspondence between
-calculus and CL.
This correspondence is stressed in the majority of
the material treated so far,
so the reader gets to know them as strongly related systems,
but now the correspondence is studied in a formal way.
Weak reduction,
-reduction,
and different extensional equalities are discussed.
Now what I call part 2 of the book starts.
It is concerned with typed -calculus and CL.
This part contains the main differences compared
to the first edition.
Chapter 10 introduces simple types and continues with
defining simply typed -calculus à la Church.
That means that we work with typed variables,
and in an abstraction the type
of the abstracted
variable is part of the syntax:
.
Every subterm may be annotated with its type.
One of the differences with the first edition of the book is that
now simple types are written as
,
which I think is much nicer than using
,
because why using
for writing a type in a system with
-reduction?
Some elementary results concerning substitution, and subject reduction are presented, before moving on to weak and strong normalization. For the proofs the reader is referred to Appendix A3 where a proof using computability is presented.
Chapter 11 is concerned with simply typed CL
à la Curry.
The authors are experts on Curry typing
and indeed:
typing à la Curry for both -calculus
and CL in Chapter 10 takes around 10 pages,
whereas the Chapters 11 and 12, dealing with
typing à la Church for
-calculus
and CL take together around 60 pages.
So a wealth of material is presented.
In Curry-style systems types are parametric, leading
to a form of polymorphism à la ML.
Then after some elementary results,
subject reduction, and decidability of typing.
The theorems of
strong normalization of weak reduction,
and weak normalization of strong reduction
are given.
For the latter the reader is referred to
the Italian edition of the predecessor of
the first edition (where also Lercher is a coauthor),
together with a footnote concerning a typo.
In a next incarnation of the book, it would
be nice to give this proof explicitly.
The chapter is rather long and contains more
interesting issues: principal types, propositions as
types, and equality.
Chapter 12, then, is concerned with simply typed -calculus
à la Curry.
The ideas and results are essentially equal to those
of the previous chapter, concerning CL,
but now there is the complication of bound variables.
The complication is mainly in the introduction rule
for
, that is, the rule that tells us
how to derive a term of type
.
It corresponds to the rule for implication introduction
in a Gentzen system for natural deduction.
Abstraction of a variable in
-calculus
corresponds to discharging a hypothesis in the
natural deduction proof system, and in both cases
there is some administration to deal with.
Some elementary properties leading to for instance
subject reduction are discussed.
Then the discussion moves on to principal types
(the most general type that can be assigned to
a term) and decidability of typability.
The next topics are
the correspondence between propositions and types,
and weak and strong normalization.
Again, the normalization proofs are mainly sketched,
with a reference to the literature.
Finally a system with equality is discussed.
Chapter 13 deals with more general typing systems.
It starts with discussing a -calculus with
dependent types à la Curry.
It is very interesting to read because most presentations
of dependent types use the Church-style of typing.
Then the focus switches to Church-style typing indeed,
to end eventually with a discussion of PTSs.
One section is devoted to strong normalization of PTSs,
presenting the skeleton of the proof
due to Geuvers and Nederhof given in
the chapter by Barendregt in the Handbook of Logic in Computer Science.
While it is of course useful to mention the result I
doubt the use of presenting only the schedule of such
a technical result; maybe here a reference to the
literature would have been enough.
Now starts what I call part 3 of the book concerning model theory: Chapters 14, 15, and 16.
Chapter 14 is a nice and clear presentation of applicative structures and combinatory algebras as models of CL. It seems to me very suitable for teaching. At p227 an implication is given that is refuted by a counterexample due to Plotkin. The reader is referred to Remark 7.3 for this counterexample, but neither there his curiosity is satisfied: the counterexample is mentioned but unfortunately not explicitly given.
Chapter 15 treats the by nature more complex issue
of models for the -calculus.
Three kinds of models are presented:
-models using an applicative structure,
syntax-free
-models,
and Scott-Meyer
-models.
Chapter 16 is more concrete and
gives an extensive presentation of the model
due to Scott.
Then some other models are discussed more shortly:
the model
,
the model
, and filter models.
But the main point of my conclusion is that
the book contains very interesting material,
partly classical, and partly not easily found elsewhere.
The presentation is very careful and clear.
I appreciate very much the many exercises with solutions.
The position of the book among other books on
-calculi seems very good to me.
The presentation is mathematically more advanced
than for instance in the book
An Introduction to Lambda Calculi for Computer Scientists
by Hankin.
On the other hand, it is shorter and more suitable
for teaching than the encyclopedic book by Barendregt.
Because of the focus on Curry-style typing systems
it contains a lot of material which is not covered in
Barendregt's chapter in the Handbook
of Logic in Computer Science.
So both for teaching and for research or self-study
the book is an outstanding source with its own clear merits.
I think this second edition of this classical book
is a beautiful asset for the literature on
-calculus and Combinatory Logic.