Towards a proof theory of rewriting: the simply typed 2λ-calculus |
| |
Authors: | Barnaby P Hilken |
| |
Affiliation: | Department of Computer Science, University of Manchester, Oxford Road, Manchester, M139PL, UK |
| |
Abstract: | This paper describes the simply typed 2λ-calculus, a language with three levels: types, terms and rewrites. The types and terms are those of the simply typed λ-calculus, and the rewrites are expressions denoting sequences of β-reductions and η-expansions. An equational theory is imposed on the rewrites, based on 2-categorical justifications, and the word problem for this theory is solved by finding a canonical expression in each equivalence class. The canonical form of rewrites allows us to prove several properties of the calculus, including a strong form of confluence and a classification of the long-βη-normal forms in terms of their rewrites. Finally we use these properties as the basic definitions of a theory of categorical rewriting, and find that the expected relationships between confluence, strong normalisation and normal forms hold. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|