Analytic proof systems for λ-calculus: the elimination of transitivity, and why it matters |
| |
Authors: | Pierluigi Minari |
| |
Institution: | (1) Department of Philosophy, University of Florence, Via Bolognese 52, 50139 Firenze, Italy |
| |
Abstract: | We introduce new proof systems Gβ] and G
extβ], which are equivalent to the standard equational calculi of λβ- and λβη- conversion, and which may be qualified as ‘analytic’ because it is possible to establish, by purely proof-theoretical methods,
that in both of them the transitivity rule admits effective elimination. This key feature, besides its intrinsic conceptual
significance, turns out to provide a common logical background to new and comparatively simple demonstrations—rooted in nice
proof-theoretical properties of transitivity-free derivations—of a number of well-known and central results concerning β- and βη-reduction. The latter include the Church–Rosser theorem for both reductions, the Standardization theorem for β- reduction, as well as the Normalization (Leftmost reduction) theorem and the Postponement of η-reduction theorem for βη-reduction
|
| |
Keywords: | Lambda-calculus Extensionality Elimination of transitivity Equational proof systems Lambda reduction |
本文献已被 SpringerLink 等数据库收录! |
|