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.