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

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