Paper: Higher-order critical pairs (at LICS 1991)

Authors: Tobias Nipkow

Abstract

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

BibTeX

  @InProceedings{Nipkow-Higherordercritical,
    author = 	 {Tobias Nipkow},
    title = 	 {Higher-order critical pairs},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science (LICS 1991)},
    year =	 {1991},
    month =	 {July}, 
    pages =      {342--349},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }