Technical reports
Higher-order critical pairs
Tobias Nipkow
April 1991, 15 pages
DOI: 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} }