Higher-Order Critical Pairs
Tobias Nipkow
We consider rewrite systems over simply typed lambda-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 the paper is a decidable confluence criterion which extends
the well-known critical pairs to a higher-order setting. Several
applications to typed lambda-calculi and proof theory are shown.
BibTeX:
@inproceedings{Nipkow-LICS-91,
author={Tobias Nipkow},
title={Higher-Order Critical Pairs},
booktitle={Proc.\ 6th IEEE Symp.\ Logic in Computer Science},
publisher={IEEE Press},year=1991,pages={342--349}}
A much extended journal article
appeared in Theoretical Computer Science.