کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
423390 | 685214 | 2006 | 15 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Development Separation in Lambda-Calculus
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله

چکیده انگلیسی
We present a proof technique in λ-calculus that can facilitate inductive reasoning on λ-terms by separating certain β-developments from other β-reductions. We give proofs based on this technique for several fundamental theorems in λ-calculus such as the Church-Rosser theorem, the standardization theorem, the conservation theorem and the normalization theorem. The appealing features of these proofs lie in their inductive styles and perspicuities.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 143, 6 January 2006, Pages 207-221
Journal: Electronic Notes in Theoretical Computer Science - Volume 143, 6 January 2006, Pages 207-221