Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
423390 | Electronic Notes in Theoretical Computer Science | 2006 | 15 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics