Logic in Computer Science (LICS 1994)

Paper: Higher-order narrowing (at LICS 1994)

Authors: Christian Prehofer

Abstract

Introduces several approaches for solving higher-order equational problems by higher-order narrowing, and gives some completeness results. The results apply to higher-order functional-logic programming languages and to higher-order unification modulo a higher-order equational theory. We lift the general notion of first-order narrowing to so-called higher-order patterns and argue that the full higher-order case is problematic. Integrating narrowing into unification (called `lazy narrowing') can avoid these problems and can be adapted to the full higher-order case. For the second-order case, we develop a version where the needed second-order unification remains decidable. Finally, we discuss a method that combines both approaches by using narrowing on higher-order patterns with full higher-order constraints

BibTeX

  @InProceedings{Prehofer-Higherordernarrowin,
    author = 	 {Christian Prehofer},
    title = 	 {Higher-order narrowing},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994},
    year =	 1994,
    editor =	 {Samson Abramsky},
    month =	 {July}, 
    pages =      {507--516},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }