Inductive Definition in Type Theory

Other Titles

Type theories can provide a foundational account of constructive mathematics, and for the computer scientist, they can also serve the dual roles of specification and programming languages. In the search for natural and expressive extensions to the NuPrl type theory, we are lead to consider forms of inductive and co-inductive definition. We realize these notions through the addition of two new type constructors, denoted μandν. This represents a step towards a more expressive theory, without adopting a completely impredicative notion of type. With these constructors we can define all the common inductive data types, from natural numbers to infinite trees. Through the propositions-as-types principle, these type constructors yield inductively defined propositions. The induction principle associated with the μ types lets us define well-founded recursive functions, and dual principle for the ν types lets us inductively define their "infinite" elements. We present another induction principle for the μ types which takes advantage of the information hiding properties of the Missing open brace for subscript\{ __ | __ \}\{ __ | __ \} type, and can be used to define an unbounded search operator, or more generally, to compute not with elements of the μ type, but under the assumption of its inhabitation. After presenting the proof rules for these new type constructors we give a semantic account, from which intuitionistic consistency is a consequence. First, we consider the the question of inductive types in the simpler setting of the second-order lambda calculus, where we prove a strong normalization property. We also consider typing terms in the presence of type constraints, and present a condition on the constraints (of polynomial complexity in the size of the constraints) for determining if the terms will be strongly normalizable or there will be a diverging typed term. Second, we develop a semantic account of the basic type theory, then relativize it to account for the impredicativity inherent in the definition of the new type constructors. We also show how this model can justify other impredicative type constructors, such as an impredicative type abstraction operation.

Journal / Series
Volume & Issue
Date Issued
Cornell University
computer science; technical report
Effective Date
Expiration Date
Union Local
Number of Workers
Committee Chair
Committee Co-Chair
Committee Member
Degree Discipline
Degree Name
Degree Level
Related Version
Related DOI
Related To
Related Part
Based on Related Item
Has Other Format(s)
Part of Related Item
Related To
Related Publication(s)
Link(s) to Related Publication(s)
Link(s) to Reference(s)
Previously Published As
Government Document
Other Identifiers
Rights URI
technical report
Accessibility Feature
Accessibility Hazard
Accessibility Summary
Link(s) to Catalog Record