• 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