System U

Short description: Special forms of a typed lambda calculus

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). They were both proved inconsistent by Jean-Yves Girard in 1972.[1] This result led to the realization that Martin-Löf's original 1971 type theory was inconsistent as it allowed the same "Type in Type" behaviour that Girard's paradox exploits.

## Contents

* 1 Formal definition
* 2 Girard's paradox
* 3 References
* 4 Further reading

## Formal definition

System U is defined[2]:352 as a pure type system with

* three sorts [math]\displaystyle{ \\{\ast, \square, \triangle\\} }[/math];
* two axioms [math]\displaystyle{ \\{\ast:\square, \square:\triangle\\} }[/math]; and
* five rules [math]\displaystyle{ \\{(\ast,\ast), (\square,\ast), (\square,\square), (\triangle,\ast), (\triangle,\square)\\} }[/math].

System U− is defined the same with the exception of the [math]\displaystyle{ (\triangle, \ast) }[/math] rule.

The sorts [math]\displaystyle{ \ast }[/math] and [math]\displaystyle{ \square }[/math] are conventionally called “Type” and “Kind”, respectively; the sort [math]\displaystyle{ \triangle }[/math] doesn't have a specific name. The two axioms describe the containment of types in kinds ([math]\displaystyle{ \ast:\square }[/math]) and kinds in [math]\displaystyle{ \triangle }[/math] ([math]\displaystyle{ \square:\triangle }[/math]). Intuitively, the sorts describe a hierarchy in the nature of the terms.

1. All values have a type, such as a base type (e.g. [math]\displaystyle{ b : \mathrm{Bool} }[/math] is read as “b is a boolean”) or a (dependent) function type (e.g. [math]\displaystyle{ f : \mathrm{Nat} \to \mathrm{Bool} }[/math] is read as “f is a function from natural numbers to booleans”).
2. [math]\displaystyle{ \ast }[/math] is the sort of all such types ([math]\displaystyle{ t : \ast }[/math] is read as “t is a type”). From [math]\displaystyle{ \ast }[/math] we can build more terms, such as [math]\displaystyle{ \ast \to \ast }[/math] which is the kind of unary type-level operators (e.g. [math]\displaystyle{ \mathrm{List} : \ast \to \ast }[/math] is read as “List is a function from types to types”, that is, a polymorphic type). The rules restrict how we can form new kinds.
3. [math]\displaystyle{ \square }[/math] is the sort of all such kinds ([math]\displaystyle{ k : \square }[/math] is read as “k is a kind”). Similarly we can build related terms, according to what the rules allow.
4. [math]\displaystyle{ \triangle }[/math] is the sort of all such terms.

The rules govern the dependencies between the sorts: [math]\displaystyle{ (\ast,\ast) }[/math] says that values may depend on values (functions), [math]\displaystyle{ (\square,\ast) }[/math] allows values to depend on types (polymorphism), [math]\displaystyle{ (\square,\square) }[/math] allows types to depend on types (type operators), and so on.

## Girard's paradox

The definitions of System U and U− allow the assignment of polymorphic kinds to generic constructors in analogy to polymorphic types of terms in classical polymorphic lambda calculi, such as System F. An example of such a generic constructor might be[2]:353 (where k denotes a kind variable)

[math]\displaystyle{ \lambda k^\square \lambda\alpha^{k \to k} \lambda\beta^k\\!. \alpha (\alpha \beta) \;:\; \Pi k : \square((k \to k) \to k \to k) }[/math].

This mechanism is sufficient to construct a term with the type [math]\displaystyle{ (\forall p:\ast, p) }[/math] (equivalent to the type [math]\displaystyle{ \bot }[/math]), which implies that every type is inhabited. By the Curry–Howard correspondence, this is equivalent to all logical propositions being provable, which makes the system inconsistent.

Girard's paradox is the type-theoretic analogue of Russell's paradox in set theory.

## References

1. ↑ Girard, Jean-Yves (1972). "Interprétation fonctionnelle et Élimination des coupures de l'arithmétique d'ordre supérieur". https://www.cs.cmu.edu/~kw/scans/girard72thesis.pdf.
2. ↑ 2.0 2.1 Sørensen, Morten Heine; Urzyczyn, Paweł (2006). "Pure type systems and the lambda cube". Lectures on the Curry–Howard isomorphism. Elsevier. doi:10.1016/S0049-237X(06)80015-7. ISBN 0-444-52077-5.

## Further reading

* Barendregt, Henk (1992). "Lambda calculi with types". Handbook of Logic in Computer Science. Oxford Science Publications. pp. 117–309. ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps.
* Coquand, Thierry (1986). "An analysis of Girard's paradox". Logic in Computer Science. IEEE Computer Society Press. pp. 227–236.
* Hurkens, Antonius J. C. (1995). "A simplification of Girard's paradox". in Dezani-Ciancaglini, Mariangiola; Plotkin, Gordon. Second International Conference on Typed Lambda Calculi and Applications (TLCA '95). Edinburgh. pp. 266–278. doi:10.1007/BFb0014058. https://link.springer.com/chapter/10.1007/BFb0014058.

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/System U. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=System_U&oldid=3378514"