کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
9657906 | 690371 | 2005 | 64 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Iteration and coiteration schemes for higher-order and nested datatypes
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Iteration and coiteration schemes for higher-order and nested datatypes Iteration and coiteration schemes for higher-order and nested datatypes](/preview/png/9657906.png)
چکیده انگلیسی
This article studies the implementation of inductive and coinductive constructors of higher kinds (higher-order nested datatypes) in typed term rewriting, with emphasis on the choice of the iteration and coiteration constructions to support as primitive. We propose and compare several well-behaved extensions of System FÏ with some form of iteration and coiteration uniform in all kinds. In what we call Mendler-style systems, the iterator and coiterator have a computational behavior similar to the general recursor, but their types guarantee termination. In conventional-style systems, monotonicity witnesses are used for a notion of monotonicity defined uniformly for all kinds. Our most expressive systems GMItÏ and GItÏ of generalized Mendler, resp. conventional (co)iteration encompass Martin, Gibbons and Bailey's efficient folds for rank-2 inductive types. Strong normalization of all systems considered is proved by providing an embedding of the basic Mendler-style system MItÏ into System FÏ.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 333, Issues 1â2, 1 March 2005, Pages 3-66
Journal: Theoretical Computer Science - Volume 333, Issues 1â2, 1 March 2005, Pages 3-66
نویسندگان
Andreas Abel, Ralph Matthes, Tarmo Uustalu,