HOME

TheInfoList



OR:

In the branches of
mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
known as
proof theory Proof theory is a major branchAccording to , proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. consists of four corresponding parts, with part D being about "Proof The ...
and
type theory In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of ...
, 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 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 terms; the exact nature of a ...
that allows an arbitrary number of sorts and dependencies between any of these. The framework can be seen as a generalisation of
Barendregt Barendregt is a Dutch surname Dutch or Nederlands commonly refers to: * Something of, from, or related to the Netherlands ** Dutch people as an ethnic group () ** Dutch nationality law, history and regulations of Dutch citizenship () ** Dutch lang ...
'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 λ-c ...
, 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 A class hierarchy or inheritance tree in computer science is a classification of Object (computer science), object types, denoting objects as the instantiations of Class (computer programming), classes (class is like a blueprint, the object is wh ...
, 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 reaso ...
, but this is not generally the case, e.g. the
simply typed lambda calculus The simply typed lambda calculus (), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor () that builds function types. It is the canonical and simplest example of a typed lambda calculus. The ...
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 logic Constructive logic is a family of logics where proofs must be constructive (i.e., proving something means one must build or exhibit it, not just argue it “must exist” abstractly). No “non-constructive” proofs are allowed (like the classic p ...
s 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 In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs. It is also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-p ...
to this setting. Based on these ideas, G. Barthe and others defined ''classical pure type systems'' (CPTS) by adding a
double negation In propositional logic, the double negation of a statement states that "it is not the case that the statement is not true". In classical logic, every statement is logically equivalent to its double negation, but this is not true in intuitionis ...
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 Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declarat ...
; and Roorda and Jeuring have proposed a
programming language A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...
based on pure type systems. The systems from the lambda cube are all known to be
strongly normalizing In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems ...
. Pure type systems in general need not be, for example
System U In mathematical logic, System U and System U− are pure type systems, i.e. special forms of a typed lambda calculus with an arbitrary number of sorts, axioms and rules (or dependencies between the sorts). System U was proved inconsistent by Je ...
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 In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computation based on function abstraction and application using variable binding and substitution. Untyped lambda calculus, the topic ...
. 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 Mathematical logic, logician, known for his work in lambda calculus and type theory. Life and work Barendregt studied mathematical logic at Utrecht University, obtai ...
, Herman Geuvers, and Jan Willem Klop).


Definition

A pure type system is defined by a triple (\mathcal, \mathcal, \mathcal) where \mathcal is the
set Set, The Set, SET or SETS may refer to: Science, technology, and mathematics Mathematics *Set (mathematics), a collection of elements *Category of sets, the category whose objects and morphisms are sets and total functions, respectively Electro ...
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: *SAGESAGE
/ref> *YarrowYarrow
/ref> *Henk 2000Henk 2000
/ref>


See also

*
System U In mathematical logic, System U and System U− are pure type systems, i.e. special forms of a typed lambda calculus with an arbitrary number of sorts, axioms and rules (or dependencies between the sorts). System U was proved inconsistent by Je ...
– 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