TY - GEN
T1 - Higher-order critical pairs
AU - Nipkow, Tobias
PY - 1991/7
Y1 - 1991/7
N2 - A subclass of λ-terms, called patterns, which have unification properties resembling those of first-order terms, is introduced. Higher-order rewrite systems are defined to be rewrite systems over λ-terms whose left-hand sides are patterns: this guarantees that the rewrite relation is easily computable. The notion of critical pair is generalized to higher-order rewrite systems, and the analog of the critical pair lemma is proved. The restricted nature of patterns is instrumental in obtaining these results. The critical pair lemma is applied to a number of λ-calculi and some first-order logic formalized by higher-order rewrite systems.
AB - A subclass of λ-terms, called patterns, which have unification properties resembling those of first-order terms, is introduced. Higher-order rewrite systems are defined to be rewrite systems over λ-terms whose left-hand sides are patterns: this guarantees that the rewrite relation is easily computable. The notion of critical pair is generalized to higher-order rewrite systems, and the analog of the critical pair lemma is proved. The restricted nature of patterns is instrumental in obtaining these results. The critical pair lemma is applied to a number of λ-calculi and some first-order logic formalized by higher-order rewrite systems.
UR - https://www.scopus.com/pages/publications/0026191418
M3 - Conference contribution
AN - SCOPUS:0026191418
SN - 081862230X
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 342
EP - 349
BT - Proceedings - Symposium on Logic in Computer Science
PB - Publ by IEEE
T2 - Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science
Y2 - 15 July 1991 through 18 July 1991
ER -