Synthese 133 (1-2):107 - 129 (2002)
|Abstract||The new concept of lambda calculi with monotone inductive types is introduced byhelp of motivations drawn from Tarski's fixed-point theorem (in preorder theory) andinitial algebras and initial recursive algebras from category theory. They are intendedto serve as formalisms for studying iteration and primitive recursion ongeneral inductively given structures. Special accent is put on the behaviour ofthe rewrite rules motivated by the categorical approach, most notably on thequestion of strong normalization (i.e., the impossibility of an infinitesequence of successive rewrite steps). It is shown that this key propertyhinges on the concrete formulation. The canonical system of monotone inductivetypes, where monotonicity is expressed by a monotonicity witness beinga term expressing monotonicity through its type, enjoys strong normalizationshown by an embedding into the traditional system of non-interleavingpositive inductive types which, however, has to be enriched by the parametricpolymorphism of system F. Restrictions to iteration on monotone inductive typesalready embed into system F alone, hence clearly displaying the differencebetween iteration and primitive recursion with respect to algorithms despitethe fact that, classically, recursion is only a concept derived from iteration.|
|Keywords||No keywords specified (fix it)|
|Through your library||Configure|
Similar books and articles
Sergei Tupailo (2004). On the Intuitionistic Strength of Monotone Inductive Definitions. Journal of Symbolic Logic 69 (3):790-798.
Motohiko Mouri & Norihiro Kamide (forthcoming). Strong Normalizability of Typed Lambda-Calculi for Substructural Logics. Logica Universalis.
William J. Mitchell (2003). A Gitik Iteration with Nearly Easton Factoring. Journal of Symbolic Logic 68 (2):481-502.
Jouko Väänänen & Dag Westerståhl (2002). On the Expressive Power of Monotone Natural Language Quantifiers Over Finite Models. Journal of Philosophical Logic 31 (4):327-358.
Paul Taylor (1996). Intuitionistic Sets and Ordinals. Journal of Symbolic Logic 61 (3):705-744.
Peter Dybjer (2000). A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. Journal of Symbolic Logic 65 (2):525-549.
Michael Rathjen (1999). Explicit Mathematics with the Monotone Fixed Point Principle. II: Models. Journal of Symbolic Logic 64 (2):517-550.
Michael Rathjen (1998). Explicit Mathematics with the Monotone Fixed Point Principle. Journal of Symbolic Logic 63 (2):509-542.
Helmut Schwichtenberg (1999). Monotone Majorizable Functionals. Studia Logica 62 (2):283-289.
Michael Rathjen (1996). Monotone Inductive Definitions in Explicit Mathematics. Journal of Symbolic Logic 61 (1):125-146.
Added to index2009-01-28
Total downloads3 ( #201,730 of 548,984 )
Recent downloads (6 months)0
How can I increase my downloads?