Tarski's fixed-point theorem and lambda calculi with monotone inductive types
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) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,653 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesSergei 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.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads3 ( #201,730 of 548,984 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
