On the unification problem for Cartesian closed categories. (English) Zbl 0882.03044

Summary: 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.


03D35 Undecidability and degrees of sets of sentences
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
68Q55 Semantics in the theory of computing
68Q25 Analysis of algorithms and problem complexity
Full Text: DOI


[1] Proceedings of the international conference on logic programming and automated reasoning pp 360– (1993)
[2] DOI: 10.1145/322261.322262 · Zbl 0462.68075 · doi:10.1145/322261.322262
[3] Journal of Functional Programming 1 pp 191– (1991)
[4] DOI: 10.1007/BF00245463 · Zbl 0781.68076 · doi:10.1007/BF00245463
[5] DOI: 10.1137/0215084 · Zbl 0665.03005 · doi:10.1137/0215084
[6] Technical Report MPI-I-91-228 (1991)
[7] DOI: 10.1016/S0747-7171(87)80004-4 · Zbl 0638.68103 · doi:10.1016/S0747-7171(87)80004-4
[8] Annual ACM symposium on the principles of programming languages pp 200– (1992)
[9] Handbook of theoretical computer science B pp 243– (1990)
[10] Proceedings of the eleventh international conference on logic programming pp 419– (1994)
[11] DOI: 10.1017/S0960129500001444 · Zbl 0763.03011 · doi:10.1017/S0960129500001444
[12] RAIRO Theoretical Informatics and Applications 27 pp 523– (1993) · Zbl 0809.68063 · doi:10.1051/ita/1993270605231
[13] Programming Methodology Group Report 66 (1992)
[14] DOI: 10.1017/S095679680000006X · Zbl 1155.68452 · doi:10.1017/S095679680000006X
[15] Proceedings of the tenth international conference on automated deduction pp 603– (1990)
[16] DOI: 10.1145/322248.322251 · Zbl 0479.68092 · doi:10.1145/322248.322251
[17] Proceedings of the second international workshop on conditional and typed rewriting systems (1990)
[18] Proceedings of the eighth annual symposium on logic in computer science (1993)
[19] On the unification problem for Cartesian closed categories (1989)
[20] Introduction to higher order categorical logic (1986) · Zbl 0596.03002
[21] Bulletin of the EATCS 32 pp 143– (1987)
[22] DOI: 10.1007/BF01084396 · Zbl 0509.18002 · doi:10.1007/BF01084396
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.