{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:09:03Z","timestamp":1763467743419},"reference-count":23,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":6128,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1997,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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<jats:italic>linear isomorphisms<\/jats:italic>, is NP-complete. Furthermore, the problem of matching in CCCs is NP-complete when the subject term is irreducible.<\/jats:p><jats:p>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.<\/jats:p>","DOI":"10.2307\/2275552","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T23:01:20Z","timestamp":1146956480000},"page":"636-647","source":"Crossref","is-referenced-by-count":7,"title":["On the unification problem for Cartesian closed categories"],"prefix":"10.1017","volume":"62","author":[{"given":"Paliath","family":"Narendran","sequence":"first","affiliation":[]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Statman","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200016418_ref023","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322262"},{"key":"S0022481200016418_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/BF01084396"},{"key":"S0022481200016418_ref020","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1017\/S0956796800020049","article-title":"Retrieving re-usable software components by polymorphic type","volume":"1","author":"Runciman","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"S0022481200016418_ref019","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/1993270605231"},{"key":"S0022481200016418_ref018","volume-title":"Programming Methodology Group Report 66","author":"Rittri","year":"1992"},{"key":"S0022481200016418_ref013","volume-title":"Proceedings of the eighth annual symposium on logic in computer science","author":"Narendran","year":"1993"},{"key":"S0022481200016418_ref010","first-page":"143","article-title":"Term rewriting systems: a tutorial","volume":"32","author":"Klop","year":"1987","journal-title":"Bulletin of the EATCS"},{"key":"S0022481200016418_ref007","volume-title":"Technical Report MPI-I-91-228","author":"Hustadt","year":"1991"},{"key":"S0022481200016418_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80004-4"},{"key":"S0022481200016418_ref004","first-page":"200","volume-title":"Annual ACM symposium on the principles of programming languages","author":"di Cosmo","year":"1992"},{"key":"S0022481200016418_ref003","first-page":"243","volume-title":"Handbook of theoretical computer science","volume":"B","author":"Dershowitz","year":"1990"},{"key":"S0022481200016418_ref001","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001444"},{"key":"S0022481200016418_ref015","doi-asserted-by":"publisher","DOI":"10.1145\/322248.322251"},{"key":"S0022481200016418_ref008","doi-asserted-by":"publisher","DOI":"10.1137\/0215084"},{"key":"S0022481200016418_ref009","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245463"},{"key":"S0022481200016418_ref005","unstructured":"di Cosmo R. , Isomorphisms of types, Ph.D. thesis , Dipartimento di Informatica, Universita di Pisa, 1993."},{"key":"S0022481200016418_ref014","volume-title":"Proceedings of the second international workshop on conditional and typed rewriting systems","author":"Nipkow","year":"1990"},{"key":"S0022481200016418_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56944-8_71"},{"key":"S0022481200016418_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52885-7_117"},{"key":"S0022481200016418_ref012","volume-title":"On the unification problem for Cartesian closed categories","author":"Narendran","year":"1989"},{"key":"S0022481200016418_ref002","first-page":"419","volume-title":"Proceedings of the eleventh international conference on logic programming","author":"Caires","year":"1994"},{"key":"S0022481200016418_ref017","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000006X"},{"key":"S0022481200016418_ref011","volume-title":"Introduction to higher order categorical logic","author":"Lambek","year":"1986"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200016418","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,14]],"date-time":"2020-04-14T14:23:16Z","timestamp":1586874196000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200016418\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,6]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1997,6]]}},"alternative-id":["S0022481200016418"],"URL":"https:\/\/doi.org\/10.2307\/2275552","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,6]]}}}