pure type system

{{unsolved|computer science|Is every weakly normalizing pure type system also strongly normalizing?}}

In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and dependencies between any of these. The framework can be seen as a generalisation of Barendregt's lambda cube, in the sense that all corners of the cube can be represented as instances of a PTS with just two sorts.{{cite book|last=Pierce|first=Benjamin|title=Types and Programming Languages|url=https://archive.org/details/typesprogramming00pier_639|url-access=limited|publisher=MIT Press|year=2002|isbn=0-262-16209-1|page= [https://archive.org/details/typesprogramming00pier_639/page/n487 466]}}{{cite book | first1 = Fairouz D. | last1 = Kamareddine | first2 = Twan | last2 = Laan | first3 = Rob P. | last3 = Nederpelt | title = A modern perspective on type theory: from its origins until today | publisher = Springer | year = 2004 | isbn = 1-4020-2334-0 | chapter = Section 4c: Pure type systems | page = 116 }} In fact, Barendregt (1991) framed his cube in this setting.{{cite journal |author-link=H.P. Barendregt |first=H. P. |last=Barendregt |url= https://www.researchgate.net/publication/216300104 |title=Introduction to generalized type systems |journal=Journal of Functional Programming |volume=1 |issue=2 |pages=125–154 |year=1991 |doi=10.1017/s0956796800020025 |hdl=2066/17240 |s2cid=44757552 |hdl-access=free }} Pure type systems may obscure the distinction between types and terms and collapse the type hierarchy, as is the case with the calculus of constructions, but this is not generally the case, e.g. the simply typed lambda calculus allows only terms to depend on terms.

Pure type systems were independently introduced by Stefano Berardi (1988) and Jan Terlouw (1989). Barendregt discussed them at length in his subsequent papers.{{cite book |editor-first=S. |editor-last=Abramsky |editor2-first=D. |editor2-last=Gabbay |editor3-first=T. |editor3-last=Maibaum |first=H. |last=Barendregt|chapter=Lambda calculi with types|chapter-url=ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps|title=Handbook of Logic in Computer Science|publisher=Oxford Science Publications|year=1992}} In his PhD thesis,{{cite thesis | first = S. | last = Berardi | title = Type dependence and Constructive Mathematics | degree = PhD | publisher = University of Torino | year = 1990 }} Berardi defined a cube of constructive logics akin to the lambda cube (these specifications are non-dependent). A modification of this cube was later called the L-cube by Herman Geuvers, who in his PhD thesis extended the Curry–Howard correspondence to this setting.{{cite thesis | first = H. | last = Geuvers | title = Logics and Type Systems | citeseerx = 10.1.1.56.7045 | degree = PhD | publisher = University of Nijmegen | year = 1993 }} Based on these ideas, G. Barthe and others defined classical pure type systems (CPTS) by adding a double negation operator.{{cite journal |first1=G. |last1=Barthe |first2=J. |last2=Hatcliff |first3=M. H. |last3=Sørensen |title=A Notion of Classical Pure Type System|citeseerx = 10.1.1.32.1371|journal=Electronic Notes in Theoretical Computer Science|volume=6|year=1997|pages=4–59|doi=10.1016/S1571-0661(05)80170-7}}

Similarly, in 1998, Tijn Borghuis introduced modal pure type systems (MPTS).{{cite journal |first=Tijn |last=Borghuis |title=Modal Pure Type Systems |journal=Journal of Logic, Language and Information |volume=7 |issue=3 |year=1998 |pages=265–296 |doi=10.1023/A:1008254612284 |s2cid=5067584 }} Roorda has discussed the application of pure type systems to functional programming; and Roorda and Jeuring have proposed a programming language based on pure type systems.{{cite web|url=http://people.cs.uu.nl/johanj/MSc/jwroorda/|author=Jan-Willem Roorda|author2=Johan Jeuring|title=Pure Type Systems for Functional Programming|access-date=2010-08-29|archive-url=https://web.archive.org/web/20111002055103/http://people.cs.uu.nl/johanj/MSc/jwroorda/|archive-date=2011-10-02|url-status=dead}} Roorda's masters' thesis (linked from the cited page) also contains a general introduction to pure type systems.

The systems from the lambda cube are all known to be strongly normalizing. Pure type systems in general need not be, for example System U from Girard's paradox is not. (Roughly speaking, Girard found pure systems in which one can express the sentence "the types form a type".) Furthermore, all known examples of pure type systems that are not strongly normalizing are not even (weakly) normalizing: they contain expressions that do not have normal forms, just like the untyped lambda calculus{{Citation needed|date=April 2013}}. It is a major open problem in the field whether this is always the case, i.e. whether a (weakly) normalizing PTS always has the strong normalization property. This is known as the Barendregt–Geuvers–Klop conjecture (named after Henk Barendregt, Herman Geuvers, and Jan Willem Klop).{{cite book |first1=Morten Heine |last1=Sørensen |first2=Paweł |last2=Urzyczyn |title=Lectures on the Curry–Howard isomorphism |publisher=Elsevier |year=2006 |isbn=0-444-52077-5 |chapter=Pure type systems and the lambda cube § 14.7 |chapter-url=https://books.google.com/books?id=_mtnm-9KtbEC&pg=PA358 |page=358}}

Definition

A pure type system is defined by a triple $(\mathcal{S}, \mathcal{A}, \mathcal{R})$ where $\mathcal{S}$ is the set of sorts, $\mathcal{A} \subseteq \mathcal{S}^2$ is the set of axioms, and $\mathcal{R} \subseteq \mathcal{S}^3$ is the set of rules. Typing in pure type systems is determined by the following rules, where $s$ is any sort:

$\frac{(s_1, s_2) \in \mathcal{A}}{\vdash s_1 : s_2}\quad \text{(axiom)}$

$\frac{\Gamma \vdash A : s \quad x \notin \text{dom}(\Gamma)}{\Gamma, x : A \vdash x : A }\quad \text{(start)}$

$\frac{\Gamma \vdash A : B \quad \Gamma \vdash C : s \quad x \notin \text{dom}(\Gamma)}{\Gamma, x : C \vdash A : B}\quad \text{(weakening)}$

$\frac{\Gamma \vdash A : s_1 \quad \Gamma, x : A \vdash B : s_2 \quad (s_1, s_2, s_3) \in \mathcal{R}}{\Gamma \vdash \Pi x : A. B : s_3}\quad\text{(product)}$

$\frac{\Gamma \vdash C : \Pi x : A. B \quad \Gamma \vdash a : A}{\Gamma \vdash Ca : B[x := a]}\quad\text{(application)}$

$\frac{\Gamma, x : A \vdash b : B \quad \Gamma \vdash \Pi x : A. B : s}{\Gamma \vdash \lambda x : A. b : \Pi x : A. B}\quad\text{(abstraction)}$

$\frac{\Gamma \vdash A : B \quad B =_{\beta} B' \quad \Gamma \vdash B' : s}{\Gamma \vdash A : B'}\quad\text{(conversion)}$

Implementations

The following programming languages have pure type systems:{{citation needed|date=May 2013}}

SAGE[http://sage.soe.ucsc.edu/ SAGE]
Yarrow[https://www.cs.ru.nl/~janz/yarrow/ Yarrow]
Henk 2000[https://web.archive.org/web/20111002055103/http://people.cs.uu.nl/johanj/MSc/jwroorda/ Henk 2000]

Notes

References

{{cite tech report |last=Berardi |first=Stefano |title=Towards a mathematical analysis of the Coquand–Huet calculus of constructions and the other systems in Barendregt's cube |publisher=Department of Computer Science, CMU, and Dipartimento Matematica, Universita di Torino |year=1988 |id=CMU-CS-88-131}}
{{cite document |last=Terlouw |first=J. |language=nl |title=Een nadere bewijstheoretische analyse van GSTTs |publisher=University of Nijmegen |location=Netherlands |year=1989}}

External links

{{nlab|id=pure+type+system|title=Pure type system}}
{{cite web |url=http://www.rbjones.com/rbjpub/logic/cl/tlc004.htm |title=Pure Type Systems overview |first=Roger Bishop |last=Jones |year=1999}}

Category:Proof theory

Category:Type theory

Category:Lambda calculus