Logic in Computer Science (LICS 1993)

Paper: On the unification problem for Cartesian closed categories (at LICS 1993)

Authors: Paliath Narendran Frank Pfenning Richard Statman

Abstract

An axiomatization of the isomorphisms that hold in all Cartesian closed categories (CCCs), discovered independently by S.V. Soloviev (1983) and by K.B. Bruce and G. Longo (1985), leads to seven equalities. It is shown that the unification problem for this theory is undecidable, thus setting an open question. It is also shown that an important subcase, namely unification modulo the linear isomorphisms, is NP-complete. Furthermore, the problem of matching in CCCs is NP-complete when the subject term is irreducible. CCC-matching and unification form the basis for an elegant and practical solution to the problem of retrieving functions from a library indexed by types investigated by M. Rittri (1990, 1991). It also has potential applications to the problem of polymorphic higher-order unification, which in turn is relevant to theorem proving, logic programming, and type reconstruction in higher-order languages

BibTeX

  @InProceedings{NarendranPfenningSt-Ontheunificationpro,
    author = 	 {Paliath Narendran and Frank Pfenning and Richard Statman},
    title = 	 {On the unification problem for Cartesian closed categories},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {57--63},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }