Typing in pure type systems

L.S. Benthem Jutting, van

Research output: Contribution to journalArticleAcademicpeer-review

33 Citations (Scopus)

Abstract

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.
Original languageEnglish
Pages (from-to)30-41
JournalInformation and Computation
Volume105
Issue number1
DOIs
Publication statusPublished - 1993

Fingerprint Dive into the research topics of 'Typing in pure type systems'. Together they form a unique fingerprint.

  • Cite this