[Prev][Next][Index][Thread]
Confluence for typed terms
Date: Wed, 22 Feb 89 18:51:29 EST
To: jcm@ra.stanford.edu, types@theory.LCS.MIT.EDU
In order to understand what is going on with confluence in typed
lambda-calculi, I think we need to understand what we are doing
when we stick type labels on lambdas, and I suspect we don't really
understand that. My suspicion is based on an example which is
relevant to the remarks in the last paragraph of John Mitchell's
message about the subject of this note. (In fact, I learned the
example from John a couple of years ago.)
Suppose we build up terms from variables (of a single kind, for the
moment) by means of application and type-labelled lambda abstraction.
If we say that (\ x:Z.X)Y beta-contracts to Sub[Y/x/X] and define
reduction and conversion accordingly, the Church-Rosser holds,
as Martin-Lof proved.
But if we say that \ x:Z.Xx eta-contracts to X, provided x is not free
in X, and try to extend reduction and conversion to include the new
contraction, we get in trouble. To see this consider the term
\ x:y.(\ x:z.x)x. Using the version of eta under discussion, we
can reduce this to \ x:z.x. But, using the version of beta specified
in the preceding paragraph, we can also reduce it to \ x:y.x.
These terms are normal and distinct, so goodbye Church-Rosser.
Of course, we know that, in the customary version of the simple typed
lambda calculus with type-labelled abstraction, we don't get into
this fix, because we would have to work with a term of the form
\ x:A.(\ x:B.x)x, where A and B are distinct, in order to adapt
the example of the preceding paragraph. And, according to the
customary typing rules, no typed term can be like that.
Formally, this is clear enough. But the bare symbol manipulations
give us no insight into what is going on here. In what follows,
I will suggest a diagnosis based on some intuitive semantical ideas.
If the suggestion is attractive, perhaps it can be turned into
formal definitions and theorems.
There are, of course, two ways of assigning simple types to terms ---
we can either use unlabelled abstraction and assign many types to
the same term, as Curry liked to do, or we can use labelled abstraction
and assign unique types, as Church did. (I am aware that Church
really started off by assigning types to variables once and for all,
but I don't really think that matters a lot.) This difference corresponds,
I think, to two different ways of thinking about function spaces.
When we write \ x.X : A -> B, we seem to mean that the domain of the
function \ x.X stands for includes the type represented by A and, for
arguments in that type, yields values in the type represented by B.
On the other hand, when we write \ x:A.X : A -> B, we usually have
in mind the claim that \ x:A.X stands for a function the domain
of which is A and the range of which is contained in B.
On this reading, we are using "A -> B" to stand for quite different
sets of functions in these two assertions, and we need different
notations for them. I will use "A -> B" to refer to the set discussed
in the first sentence of the preceding paragraph. The other set
will be called "A >-> B".
In order to justify the claim that \ x.X : A -> B holds relative to
a type assignment Gamma, we prove Gamma , x : A |- X : B. And,
in order to justify the corresponding claim about \ x:A.X : A >-> B,
we prove exactly the same thing. This makes perfect sense, if
we take it that the value of \ x:A.X is, in some reasonable sense,
the restriction to A of the function denoted by \ x.X. I take this
for granted in what follows.
Using "R" to represent restriction of a function to a given type,
we can rewrite \ x:A.X as R A (\ x.X). Of course, if we are going
to do this formally, we need will typing and computation rules for R.
As far as computation is concerned, at least one rule is obvious ---
if R A X Y is well-typed, it should contract to X Y. And, using
this and honest to goodness beta-contraction (i.e., contracting
(\ x.X)Y to Sub[Y/x/X]), we will have (\ x:A.X)Y = R A (\ x.X) Y
red (\ x.X)Y red Sub[Y/x/X], so the "beta-contraction" specified
in the second paragraph of this message comes out as a reduction.
But the "eta-contraction" by which were puzzled turns out to be
a muddle.
Getting all the way back to the situation in which we had only one
style of variable and were worrying about \ x:y.(\ x:z.x)x, note that
if we explain the type labels via R, we will have \ x:y.(\ x:z.x)x
= R y (\ x.R z (\ x.x) x). Now, there is a REAL eta-redex
inside this term, namely (\ x.R z (\ x.x) x). But contracting it
gives us R y (\ x.x), and so does perfroming the reduction
R z (\ x.x) x red (\ x.x) x red x. So, analyzing the type labelling
via R suggests that we went wrong because our original notation
caused us to think we were doing eta-contraction when we weren't.
Moreover, the intuitive semantical considerations which led to analyzing
labelling in terms of R explains why "eta-conversion" works all right
in the simple typed lambda-calculus with labelled abstraction.
A term of the form \ x:A.X x, x not free in X, will have its value
in a type denoted by something of the form A >-> B. If X x is to
make sense for every value of x in the type denoted by X and yield
values in the type denoted by B, we must have X : A -> B or X : A >-> B.
But if \ x:A.X x and X are to have the same value, then, in fact,
we must have X : A -> B. The usual typing rules insure that this
will be the case, so everything works out all right.
Regards,
Garrel Pottinger