Department of Computer Science and Technology

Technical reports

Higher-order critical pairs

Tobias Nipkow

April 1991, 15 pages

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

Abstract

We consider rewrite systems over simply typed λ-terms with restricted left-hand sides. This gives rise to a one-step reduction relation whose transitive, reflexive and symmetric closure coincides with equality. The main result of this paper is a decidable confluence criterion which extends the well-known critical pairs to a higher-order setting. Several applications to typed λ-calculi and proof theory are shown.

Full text

PDF (1.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-218,
  author =	 {Nipkow, Tobias},
  title = 	 {{Higher-order critical pairs}},
  year = 	 1991,
  month = 	 apr,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-218.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-218},
  number = 	 {UCAM-CL-TR-218}
}