[Prev][Next][Index][Thread]
Church-Rosser for typed systems
In what you call the alternate (actually, historically first)
presentation of the simply typed lambda calculus (Barendregt, Appendix
A), you have a different way of defining terms, and
A B
\x . (\y . y) x
is not a term at all. For this presentation, it seems to me that typed
CR follows from
1) CR for the untyped calculus built on typed variables (assume that
the sets of variables of distinct types are disjoint and take the set
of variables of the untyped calculus to be the union of all the sets
of typed variables; the (well-)typed terms will be a subset of these
untyped terms
2) well-typedness is preserved by beta and eta reduction.
--- * ---
For the other presentation, one defines "raw" terms, such as
\x:A. (\ y:B. y) x
and then gives rules for deriving typing judgements about raw terms
under type assignments to variables.
As you point out, CR fails for raw terms, otherwise we would invoke a
subject-reduction-theorem-like result (which holds) and obtain CR for
reductions on derivable typing judgements.
However, one can at least preserve the IDEAS of the proof of CR for
the untyped calculus. First prove that beta, by itself, is
Church-Rosser on raw terms, say, using the method of Martin-Lof and
Tait (Barendregt, pp. 59-62). In fact, this would be a simplified
version of Martin-Lof's proof of CR for his Type:Type calculus (it's
in the 1971 unpublished manuscript). Then, check that eta is also, by
itself, Church-Rosser on raw terms (trivial). Finally, show that beta
and eta commute ON THE RAW TERMS THAT OCCUR IN DERIVABLE TYPING
JUDGEMENTS. CR then follows by the Hindley-Rosen Lemma (Barendregt,
pp. 64-66) and the subject-reduction-theorem-like result.
This technique extends immediately to the Girard-Reynolds polymorphic
lambda calculus, the Calculus of Constructions, etc.