dc.contributor.author Mendler, Paul Francis en_US dc.date.accessioned 2007-04-23T17:22:19Z dc.date.available 2007-04-23T17:22:19Z dc.date.issued 1987-09 en_US dc.identifier.citation http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-870 en_US dc.identifier.uri https://hdl.handle.net/1813/6710 dc.description.abstract 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 $\mu and \nu$. 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 $\mu$ types lets us define well-founded recursive functions, and dual principle for the $\nu$ types lets us inductively define their "infinite" elements. We present another induction principle for the $\mu$ types which takes advantage of the information hiding properties of the $\{ __ | __ \}$ type, and can be used to define an unbounded search operator, or more generally, to compute not with elements of the $\mu$ 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. en_US dc.format.extent 6773607 bytes dc.format.extent 1433210 bytes dc.format.mimetype application/pdf dc.format.mimetype application/postscript dc.language.iso en_US en_US dc.publisher Cornell University en_US dc.subject computer science en_US dc.subject technical report en_US dc.title Inductive Definition in Type Theory en_US dc.type technical report en_US
﻿