Pure Type System
   HOME

TheInfoList



OR:

__NOTOC__ In the branches of
mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
known as proof theory and
type theory In mathematics, logic, and computer science, a type theory is the formal system, formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theor ...
, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of
typed lambda calculus A typed lambda calculus is a typed formalism (mathematics), formalism that uses the lambda-symbol (\lambda) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda term ...
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 mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ ...
, in the sense that all corners of the cube can be represented as instances of a PTS with just two sorts. In fact, Barendregt (1991) framed his cube in this setting. 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 In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason ...
, but this is not generally the case, e.g. the
simply typed lambda calculus The simply typed lambda calculus (\lambda^\to), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda ...
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. In his PhD thesis, 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 Geuvers, who in his PhD thesis extended the
Curry–Howard correspondence In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relat ...
to this setting. Based on these ideas, Barthe and others defined classical pure type systems (CPTS) by adding a double negation operator. Similarly, in 1998, Tijn Borghuis introduced modal pure type systems (MPTS). Roorda has discussed the application of pure type systems to
functional programming In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that ...
; and Roorda and Jeuring have proposed a programming language based on 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. 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 Hendrik Pieter (Henk) Barendregt (born 18 December 1947, Amsterdam) is a Dutch logician, known for his work in lambda calculus and type theory. Life and work Barendregt studied mathematical logic at Utrecht University, obtaining his master's de ...
, Herman Geuvers, and Jan Willem Klop).


Definition

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


Implementations

The following programming languages have pure type systems: *SAGE SAGE
/ref> *Yarrow Yarrow
/ref> *Henk 2000 Henk 2000
/ref>


See also

* System U – an example of an inconsistent PTS * λμ-calculus uses a different approach to control than CPTS


Notes


References

* *


Further reading

*


External links

* * {{DEFAULTSORT:Pure Type System Proof theory Type theory Lambda calculus