Typing in pure type systems

Pure Type Systems (also called Generalized Type Systems) describe the functional structure of typed systems. They were introduced by S. Berardi and J. Terlouw in order to give a uniform and simple approach to the theory of typed lambda calculi underlying these systems. Among the systems which fall under this concept are the systems in Barendregt's cube, various AUTOMATH systems (if the mechanism of definitions is regarded as belonging to a meta-language), and some logical systems. In Pure Type Systems the typing of terms is governed by sets of axioms and rules, different sets of axioms and rules giving rise to different systems. In Geuvers and Nederhof (J. Funct. Programming1(2), 155-189 (1991)) it is shown that in a subclass, the class of functional systems, the type of a term is unique up to ß-equivalence. In functional systems also a "thickening lemma" is proved, which we call "strengthening": If G1, x:A, G2 b:B and xFV(G2)FV(b)FV(B) then G1G2 b:B. Strengthening has been proved for the AUTOMATH systems by van Daalen and for the theory ECC by Luo. We analyse typing in non-functional systems. We show that, although the type of a term in such systems is not unique, the various possible types have a simple common structure. In fact if a term has types A and B which are not ß-equivalent, then A=¿ x1:C1 ... ¿ xm:Cm.s1 and B=¿ x1:C1 ... ¿ xm:Cm.s2 where s1 and s2 and are sorts. As a consequence strengthening holds too, and we have also uniqueness of domains: If G a:¿ x:A1.B1 and G a:¿ x:A2.B2 then A1 = ßA2. Finally we prove decidability: if all terms in a Pure Type System normalize and the set of sorts of that system is finite then the typing relation is decidable.