DocumentCode
2146972
Title
Predictive type universes and primitive recursion
Author
Mendler, Nax Paul
Author_Institution
Dept. of Comput. Sci., Manchester Univ., UK
fYear
1991
fDate
15-18 July 1991
Firstpage
173
Lastpage
184
Abstract
A category-theoretic explanation of predicative type universes and primitive recursion on them is given. Categories with display maps (cdm) (with canonical pullbacks) are used to model families. A slight generalization of an algebra, called an I -algebra, is given. Primitive recursion is defined, and the general definition of primitive recursion on a cdm which can justify the elimination rules for all the usual inductively defined datatypes, including universes, as an instance, is given. It is shown how operations may be reflected, allowing an I -algebra to be closed under type-forming operations. Universe hierarchies are built: an externally constructed one, and then a large type universe, itself closed under universe construction, in which universe hierarchies can be internally constructed. As an example, a hierarchy up to ω is constructed
Keywords
formal logic; I-algebra; canonical pullbacks; category theory; display maps; elimination rules; explanation; families; inductively defined datatypes; predicative type universes; primitive recursion; type-forming operations; universe hierarchies; Algebra; Chromium; Displays; Equalizers; Predictive models; Writing;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1991. LICS '91., Proceedings of Sixth Annual IEEE Symposium on
Conference_Location
Amsterdam
Print_ISBN
0-8186-2230-X
Type
conf
DOI
10.1109/LICS.1991.151642
Filename
151642
Link To Document