On the unification problem for Cartesian closed categories
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 32, 57-63
- https://doi.org/10.1109/lics.1993.287600
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.Keywords
This publication has 13 references indexed in Scilit:
- A complete axiom system for isomorphism of types in closed categoriesPublished by Springer Nature ,1993
- Complexity of unification problems with associative-commutative operatorsJournal of Automated Reasoning, 1992
- Provable isomorphisms of typesMathematical Structures in Computer Science, 1992
- Retrieving library identifiers via equational matching of typesPublished by Springer Nature ,1990
- Associative-commutative unificationJournal of Symbolic Computation, 1987
- Completion of a Set of Rules Modulo a Set of EquationsSIAM Journal on Computing, 1986
- The category of finite sets and Cartesian closed categoriesJournal of Mathematical Sciences, 1983
- A Unification Algorithm for Associative-Commutative FunctionsJournal of the ACM, 1981
- Complete Sets of Reductions for Some Equational TheoriesJournal of the ACM, 1981
- Equations and Rewrite Rules: A SurveyPublished by Elsevier ,1980