Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-24T23:41:10.788Z Has data issue: false hasContentIssue false
  • English
  • Français

On the unification problem for Cartesian closed categories

Published online by Cambridge University Press:  12 March 2014

Paliath Narendran ,
Frank Pfenning  and
Richard Statman
Paliath Narendran
Affiliation:
Institute of Programming and Logics, Department of Computer Science, State University of NY at Albany, Albany, NY 12222, USA, E-mail: [email protected]
Frank Pfenning
Affiliation:
Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, USA, E-mail: [email protected]
Richard Statman
Affiliation:
Department of Mathematics, Carnegie Mellon University, Pittsburgh, Pa 15213, USA, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Cartesian closed categories (CCCs) have played and continue to play an important role in the study of the semantics of programming languages. An axiomatization of the isomorphisms which hold in all Cartesian closed categories discovered independently by Soloviev and Bruce, Di Cosmo and Longo leads to seven equalities. We show that the unification problem for this theory is undecidable, thus settling an open question. We also show 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 Rittri. It also has potential applications to the problem of polymorphic type inference and polymorphic higher-order unification, which in turn is relevant to theorem proving and logic programming.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 62 , Issue 2 , June 1997 , pp. 636 - 647
Copyright
Copyright © Association for Symbolic Logic 1997

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Bruce, K. B., di Cosmo, R., and Longo, G., Provable isomorphisms of types, Mathematical Structures in Computer Science, vol. 2 (1992), no. 2, pp. 231–247.CrossRefGoogle Scholar
[2]Caires, Luis and Monteiro, Luis, Higher-order polymorphic unification for logic programming, Proceedings of the eleventh international conference on logic programming (Van Hentenryck, Pascal, editor), MIT Press, 1994, pp. 419–433.Google Scholar
[3]Dershowitz, N. and Jouannaud, Jean-Pierre, Rewrite systems, Handbook of theoretical computer science (van Leeuwen, J., editor), vol. B: Formal Models and Semantics, Elsevier, Amsterdam, 1990, pp. 243–320.Google Scholar
[4]di Cosmo, R., Type isomorphisms in a type assignment framework, Annual ACM symposium on the principles of programming languages, ACM, 1992, pp. 200–210.Google Scholar
[5]di Cosmo, R., Isomorphisms of types, Ph.D. thesis, Dipartimento di Informatica, Universita di Pisa, 1993.Google Scholar
[6]Fages, François, Associative-commutative unification, Journal of Symbolic Computation, vol. 3 (1987), pp. 257–275.CrossRefGoogle Scholar
[7]Hustadt, Ullrich, A complete transformation system for polymorphic higher-order unification, Technical Report MPI-I-91-228, Max-Planck-Institut für Informatik, Saarbrücken, Germany, 12 1991.Google Scholar
[8]Jouannaud, Jean-Pierre and Kirchner, Helene, Completion of a set of rules modulo a set of equations, SIAM Journal of Computing, vol. 15 (1986), no. 4, pp. 1155–1194.CrossRefGoogle Scholar
[9]Kapur, Deepak and Narendran, Paliath, Complexity of unification problems with associative-commutative operators, Journal of Automated Reasoning, vol. 9 (1992), no. 2, pp. 261–288.CrossRefGoogle Scholar
[10]Klop, J. W., Term rewriting systems: a tutorial, Bulletin of the EATCS, vol. 32 (1987), pp. 143–182.Google Scholar
[11]Lambek, J. and Scott, P. J., Introduction to higher order categorical logic, Cambridge University Press, Cambridge, England, 1986.Google Scholar
[12]Narendran, Paliath, Pfenning, Frank, and Statman, Richard, On the unification problem for Cartesian closed categories, talk presented at the workshop on higher-order logic in Banff, Alberta, 09 1989.Google Scholar
[13]Narendran, Paliath, On the unification problem for Cartesian closed categories, Proceedings of the eighth annual symposium on logic in computer science (Vardi, Moshe, editor), IEEE Press, 1993.Google Scholar
[14]Nipkow, Tobias, Higher-order unification, polymorphism and subsorts, Proceedings of the second international workshop on conditional and typed rewriting systems (Kaplan, S. and Okada, M., editors), Lecture Notes in Computer Science, no. 516, Springer-Verlag, 1990.Google Scholar
[15]Peterson, G. E. and Stickel, M. E., Complete sets of reductions for some equational theories, Journal of the ACM, vol. 28 (1981), no. 3, pp. 233–264.CrossRefGoogle Scholar
[16]Rittri, Mikael, Retrieving library identifiers via equational matching of types, Proceedings of the tenth international conference on automated deduction (Stickel, M. E., editor), Lecture Notes in Artificial Intelligence, no. 449, Springer-Verlag, 1990, pp. 603–617.CrossRefGoogle Scholar
[17]Rittri, Mikael, Using types as search keys in function libraries, Journal of Functional Programming, vol. 1 (1991), no. 1, pp. 71–89, A preliminary version appeared in the proceedings of FPCA '89, pages 174–183.CrossRefGoogle Scholar
[18]Rittri, Mikael, Retrieving library functions by unifying types modulo linear isomorphism, Programming Methodology Group Report 66, Chalmers University of Technology and University of Göteborg, Göteborg, Sweden, 05 1992.Google Scholar
[19]Rittri, Mikael, Retrieving library functions by unifying types modulo linear isomorphism, RAIRO Theoretical Informatics and Applications, vol. 27 (1993), no. 6, pp. 523–540.CrossRefGoogle Scholar
[20]Runciman, Colin and Toyn, Ian, Retrieving re-usable software components by polymorphic type, Journal of Functional Programming, vol. 1 (1991), no. 2, pp. 191–211, A preliminary version appeared in the proceedings of FPCA '89, pages 166–173.CrossRefGoogle Scholar
[21]Soloviev, Sergei V., The category of finite sets and Cartesian closed categories, Soviet Mathematics, vol. 22 (1983), no. 3, pp. 1387–1400.CrossRefGoogle Scholar
[22]Soloviev, Sergei V., The ordinary identities form a complete axiom system for isomorphism of types in closed categories, Proceedings of the international conference on logic programming and automated reasoning (Voronkov, A., editor), Lecture Notes in Artificial Intelligence, no. 698, Springer-Verlag, 1993, pp. 360–371.CrossRefGoogle Scholar
[23]Stickel, Mark, A unification algorithm for associative-commutative functions, Journal of the ACM, vol. 28 (1981), no. 3, pp. 423–434.CrossRefGoogle Scholar