[Prev][Next][Index][Thread]
teach untyped lambda calculus?
Date: Wed, 5 Oct 88 10:56:35 PDT
In response to the course outline I posted last week,
I have gotten a few votes for teaching UNTYPED lambda
calculus (in spite of the fact that this is the TYPES
mailing list ...). I would like to explain my decision
to start the course with typed lambda calculus by
answering my critics' objections.
The main reasons to teach untyped lambda calculus seem to be:
1. it is computationally universal
2. it "underlies" all of the typed systems
If there are others that seem substantially different,
let me know.
Point 1: While it is possible to represent all partial recursive
functions in untyped lambda calculus, I think this is almost a
red herring, from a programming language point of view. To begin
with, there are many "expressiveness" distinctions in programming
which seem unrelated to partial functions on the integers. Almost
all programming languages is actual use are "Turing universal,"
but this does not mean all are equally useful in practice. So
focusing on partial recursive functions does not help us make the
kind of distinctions we would like. Moreover, I do not see why
the argument that untyped lambda calculus is important because
of the encoding of integer functions does not be apply equally
well to other formalisms. For example, should we teach recursion
equations as a fundamental model of programming languages?
In the course I am teaching, we started with a version of PCF
with integers, booleans, products, function spaces and fixed
points. It is easy to program all partial recursive functions in
this language. In fact, the proof of this is just like any
well-organized proof of the universality of untyped lambda
calculus, once we prove the initial lemmas about the representability
of basic operations (addition, recursion, ...). In addition,
in a course that later covers untyped lambda calculus
(in conjunctionEDIT CHA with recursive types or domain equations),
the students have already gone through a simple proof for PCF,
and are familiar with representing functions inside lambda calculus.
All that remains is to show how basic operations are represented.
Point 2: I think the most compelling side of this argument
is that many technical arguments about reduction appear in
their simplest form in the untyped lambda calculus.
One point in favor, for example, is that many normalization
proofs are much simpler when translated into facts about
sets of untyped terms. Therefore it is technically useful
to have some understanding of untyped lambda calculus.
However, properties such as confluence do not transfer
immediately from untyped to typed systems. So even if we
prove it once for untyped lambda calculus, we still have to
prove it again (or do some extra work) when we come to
any typed system.
One technical argument that I think becomes more pleasant
in the typed setting is the uniqueness and finiteness of
developments, surely one of the most interesting facts about
untyped reduction. In the context of PCF, we can first
prove Church-Rosser and SN for pure typed lambda calculus
(by logical relations, say). Then, with a fixed-point
operator added, the obvious thing to do is label each
occurrence of FIX with an integer bound on the number of
FIX reductions. This lets us prove CR and SN again,
by essentially the same proof, giving uniqueness and
finiteness of developments for PCF. Church-Rosser follows
as usual. By following this route, we see most of the
techniques that are involved in proving the theorem
for untyped lambda calculus, but the proof is broken
down into simpler and (perhaps) more intuitive steps.
John