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 :
بازگشت