کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
433718 | 689615 | 2016 | 37 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Termination of rewrite relations on λ-terms based on Girard's notion of reducibility
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: Termination of rewrite relations on λ-terms based on Girard's notion of reducibility Termination of rewrite relations on λ-terms based on Girard's notion of reducibility](/preview/png/433718.png)
چکیده انگلیسی
In this paper, we show how to extend the notion of reducibility introduced by Girard for proving the termination of β-reduction in the polymorphic λ-calculus, to prove the termination of various kinds of rewrite relations on λ-terms, including rewriting modulo some equational theory and rewriting with matching modulo βη, by using the notion of computability closure. This provides a powerful termination criterion for various higher-order rewriting frameworks, including Klop's Combinatory Reductions Systems with simple types and Nipkow's Higher-order Rewrite Systems.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 611, 18 January 2016, Pages 50–86
Journal: Theoretical Computer Science - Volume 611, 18 January 2016, Pages 50–86
نویسندگان
Frédéric Blanqui,