Department of Computer Science and Technology

Technical reports

Towards a proof theory of rewriting: the simply-typed 2-λ calculus

Barnaby P. Hilken

May 1994, 28 pages

DOIhttps://doi.org/10.48456/tr-336

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.

Full text

PDF (1.7 MB)

BibTeX record

@TechReport{UCAM-CL-TR-336,
  author =	 {Hilken, Barnaby P.},
  title = 	 {{Towards a proof theory of rewriting: the simply-typed
         	   2-$\lambda$ calculus}},
  year = 	 1994,
  month = 	 may,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-336.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-336},
  number = 	 {UCAM-CL-TR-336}
}