{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T17:45:49Z","timestamp":1743011149520,"version":"3.40.3"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572302"},{"type":"electronic","value":"9783031572319"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We explain how to recast the semantics of the simply-typed <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\uplambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bb<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus, and its linear and ordered variants, using multi-ary structures. We define universal properties for multicategories, and use these to derive familiar rules for products, tensors, and exponentials. Finally we outline how to recover both the category-theoretic syntactic model and its semantic interpretation from the multi-ary framework. We then use these ideas to study the semantic interpretation of combinatory logic and the simply-typed <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\uplambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bb<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus without products. We introduce <jats:italic>extensional SK-clones<\/jats:italic> and show these are sound and complete for both combinatory logic with extensional weak equality and the simply-typed <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\uplambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bb<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus without products. We then show such SK-clones are equivalent to a variant of closed categories called <jats:italic>SK-categories<\/jats:italic>, so the simply-typed <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\uplambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03bb<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus without products is the internal language of SK-categories.<\/jats:p>","DOI":"10.1007\/978-3-031-57231-9_8","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T18:01:54Z","timestamp":1712340114000},"page":"160-181","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Clones, closed categories, and combinatory logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8320-0280","authenticated-orcid":false,"given":"Philip","family":"Saville","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Abramsky, S.: Computational interpretations of linear logic. Theoretical Computer Science 111(1-2), 3\u201357 (1993). https:\/\/doi.org\/10.1016\/0304-3975(93)90181-r","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Abramsky, S.: Temperley-Lieb algebra: From knot theory to logic and computation via quantum mechanics. In: Mathematics of Quantum Computation and Quantum Technology. Chapman and Hall\/CRC (2007)","DOI":"10.1201\/9781584889007.ch15"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Arkor, N., Fiore, M.: Algebraic models of simple type theories. In: Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science. ACM (2020). https:\/\/doi.org\/10.1145\/3373718.3394771","DOI":"10.1145\/3373718.3394771"},{"key":"8_CR4","unstructured":"Arkor, N., McDermott, D.: Abstract clones for abstract syntax. In: Kobayashi, N. (ed.) 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference). LIPIcs, vol.\u00a0195, pp. 30:1\u201330:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2021.30"},{"key":"8_CR5","unstructured":"Barendregt, H.P.: The lambda calculus: its syntax and semantics, Studies in Logic and the Foundations of Mathematics), vol.\u00a0103. North-Holland (1985), revised edition"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Bimb\u00f3, K.: Combinatory logic pure, applied, and typed. Taylor & Francis (2012)","DOI":"10.1201\/b11046"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Blanco, N., Zeilberger, N.: Bifibrations of polycategories and classical linear logic. Electronic Notes in Theoretical Computer Science 352, 29\u201352 (Oct 2020). https:\/\/doi.org\/10.1016\/j.entcs.2020.09.003","DOI":"10.1016\/j.entcs.2020.09.003"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Church, A.: A formulation of the simple theory of types. The Journal of Symbolic Logic 5(2), 56\u201368 (1940), http:\/\/www.jstor.org\/stable\/2266170","DOI":"10.2307\/2266170"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Crole, R.L.: Categories for Types. Cambridge University Press (1994). https:\/\/doi.org\/10.1017\/CBO9781139172707","DOI":"10.1017\/CBO9781139172707"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Day, B.J., Laplaza, M.L.: On embedding closed categories. Bulletin of the Australian Mathematical Society 18(3), 357\u2013371 (1978). https:\/\/doi.org\/10.1017\/s0004972700008236","DOI":"10.1017\/S0004972700008236"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Eilenberg, S., Kelly, G.M.: Closed categories. In: Proceedings of the Conference on Categorical Algebra, pp. 421\u2013562. Springer Berlin Heidelberg (1966). https:\/\/doi.org\/10.1007\/978-3-642-99902-4_22","DOI":"10.1007\/978-3-642-99902-4_22"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Fiore, M., Mahmoud, O.: Second-order algebraic theories. In: Mathematical Foundations of Computer Science 2010, pp. 368\u2013380. Springer Berlin Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15155-2_33","DOI":"10.1007\/978-3-642-15155-2_33"},{"key":"8_CR13","unstructured":"Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science. pp. 193\u2013. LICS \u201999, IEEE Computer Society, Washington, DC, USA (1999), http:\/\/dl.acm.org\/citation.cfm?id=788021.788948"},{"key":"8_CR14","unstructured":"Fox, T.: Combinatory logic and cartesian closed categories. Master\u2019s thesis, McGill University (1971), https:\/\/escholarship.mcgill.ca\/concern\/theses\/6h440t871"},{"key":"8_CR15","unstructured":"Gilezan, S.: A note on typed combinators and typed lambda terms. Novi Sad Journal of Mathematics 23(1), 319\u2013329 (1993), https:\/\/sites.dmi.uns.ac.rs\/nsjom\/Papers\/23_1\/NSJOM_23_1_319_329.pdf"},{"key":"8_CR16","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York, NY, USA (1989), http:\/\/www.paultaylor.eu\/stable\/Proofs+Types.html"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Hermida, C.: Representable multicategories. Advances in Mathematics 151(2), 164\u2013225 (2000). https:\/\/doi.org\/10.1006\/aima.1999.1877","DOI":"10.1006\/aima.1999.1877"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Hyland, M.: Towards a notion of lambda monoid. Electronic Notes in Theoretical Computer Science 303, 59\u201377 (2014). https:\/\/doi.org\/10.1016\/j.entcs.2014.02.004","DOI":"10.1016\/j.entcs.2014.02.004"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Hyland, M.: Classical lambda calculus in modern dress. Mathematical Structures in Computer Science 27(5), 762\u2013781 (2015). https:\/\/doi.org\/10.1017\/s0960129515000377","DOI":"10.1017\/S0960129515000377"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Hyland, M., de\u00a0Paiva, V.: Full intuitionistic linear logic (extended abstract). presented at the 9th International Congress of Logic, Methodology and Philosophy of Science held in Uppsala, Sweden, August 7-14, 1991. Annals of Pure and Applied Logic 64(3), 273\u2013291 (1993). https:\/\/doi.org\/10.1016\/0168-0072(93)90146-5","DOI":"10.1016\/0168-0072(93)90146-5"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Jacobs, B.: Simply typed and untyped lambda calculus revisited. In: Applications of Categories in Computer Science, pp. 119\u2013142. Cambridge University Press (1992). https:\/\/doi.org\/10.1017\/cbo9780511525902.008","DOI":"10.1017\/CBO9780511525902.008"},{"key":"8_CR22","unstructured":"Jacobs, B.: Categorical logic and type theory. Elsevier Science (1999)"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium Volume 2 (Oxford Logic Guides). Clarendon Press (2002)","DOI":"10.1093\/oso\/9780198515982.001.0001"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Lambek, J.: The mathematics of sentence structure. The American Mathematical Monthly 65(3), \u00a0154 (1958). https:\/\/doi.org\/10.2307\/2310058","DOI":"10.2307\/2310058"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Lambek, J.: Deductive systems and categories II: Standard constructions and closed categories. In: Category theory, homology theory and their applications I, pp. 76\u2013122. Springer (1969). https:\/\/doi.org\/10.1007\/BFb0079385","DOI":"10.1007\/BFb0079385"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Lambek, J.: Multicategories revisited. In: Gray, J.W., Scedrov, A. (eds.) Categories in Computer Science and Logic: Proceedings of the AMS-IMS-SIAM Joint Summer Research Conference Held June 14-20, 1987 with Support from the National Science Foundation, vol.\u00a092, pp. 217\u2013240. American Mathematical Society (1989). https:\/\/doi.org\/10.1090\/conm\/092","DOI":"10.1090\/conm\/092\/1003201"},{"key":"8_CR27","unstructured":"Lambek, J., Scott, P.J.: Introduction to Higher Order Categorical Logic. Cambridge University Press, New York, NY, USA (1986)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Leinster, T.: Higher operads, higher categories. No.\u00a0298 in London Mathematical Society Lecture Note Series, Cambridge University Press (2004). https:\/\/doi.org\/10.1017\/CBO9780511525896","DOI":"10.1017\/CBO9780511525896"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Linton, F.E.J.: Some aspects of equational categories. In: Proceedings of the Conference on Categorical Algebra, pp. 84\u201394. Springer Berlin Heidelberg (1966). https:\/\/doi.org\/10.1007\/978-3-642-99902-4_3","DOI":"10.1007\/978-3-642-99902-4_3"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Mac Lane, S.: Categories for the Working Mathematician, Graduate Texts in Mathematics, vol.\u00a05. Springer-Verlag New York, second edn. (1998). https:\/\/doi.org\/10.1007\/978-1-4757-4721-8","DOI":"10.1007\/978-1-4757-4721-8"},{"key":"8_CR31","unstructured":"Manzyuk, O.: Closed categories vs. closed multicategories. Theory and Applications of Categories 26(5), 132\u2013175 (2012), http:\/\/www.tac.mta.ca\/tac\/volumes\/26\/5\/26-05.pdf"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"May, J.P.: The Geometry of Iterated Loop Spaces. Springer Berlin Heidelberg (1972). https:\/\/doi.org\/10.1007\/bfb0067491","DOI":"10.1007\/BFb0067491"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Melli\u00e8s, P.A.: Ribbon tensorial logic. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science. LICS \u201918, ACM (Jul 2018). https:\/\/doi.org\/10.1145\/3209108.3209129","DOI":"10.1145\/3209108.3209129"},{"key":"8_CR34","unstructured":"Pisani, C.: Sequential multicategories. Theory and Applications of Categories 29(19), 496\u2014541 (2014). https:\/\/doi.org\/http:\/\/www.tac.mta.ca\/tac\/volumes\/29\/19\/29-19.pdf"},{"key":"8_CR35","unstructured":"Pitts, A.M.: Categorical logic. In: Handbook of Logic in Computer Science, chap.\u00a02, pp. 39\u2013123. Oxford University Press, Oxford, UK (2000)"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Polakow, J., Pfenning, F.: Natural deduction for intuitionistic non-commutative linear logic. In: Lecture Notes in Computer Science, pp. 295\u2013309. Springer Berlin Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48959-2_21","DOI":"10.1007\/3-540-48959-2_21"},{"key":"8_CR37","unstructured":"Riehl, E.: Category Theory in Context. Dover Publications, Incorporated (2016), https:\/\/math.jhu.edu\/~eriehl\/context.pdf"},{"key":"8_CR38","unstructured":"Saville, P.: Cartesian closed bicategories: type theory and coherence. Ph.D. thesis, University of Cambridge (2020). https:\/\/doi.org\/10.17863\/CAM.55080"},{"key":"8_CR39","unstructured":"Shulman, M.: Closed category, https:\/\/ncatlab.org\/nlab\/show\/closed+category, revision 49 (May 2018)"},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"Shulman, M.: LNL polycategories and doctrines of linear logic. Logical Methods in Computer Science 19(2) (2023). https:\/\/doi.org\/10.46298\/lmcs-19(2:1)2023","DOI":"10.46298\/lmcs-19(2:1)2023"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Taylor, W.: Characterizing Mal\u2019cev conditions. Algebra Universalis 3(1), \u00a0351 (Dec 1973). https:\/\/doi.org\/10.1007\/BF02945141","DOI":"10.1007\/BF02945141"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic proof theory. No.\u00a043 in Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, second edn. (2000)","DOI":"10.1017\/CBO9781139168717"},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"Uustalu, T., Veltri, N., Zeilberger, N.: Eilenberg-Kelly reloaded. Electronic Notes in Theoretical Computer Science 352, 233\u2013256 (Oct 2020). https:\/\/doi.org\/10.1016\/j.entcs.2020.09.012","DOI":"10.1016\/j.entcs.2020.09.012"},{"key":"8_CR44","doi-asserted-by":"crossref","unstructured":"Uustalu, T., Veltri, N., Zeilberger, N.: Deductive systems and coherence for skew prounital closed categories. In: Sacerdoti\u00a0Coen, C., Tiu, A. (eds.) Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Paris, France, 29th June 2020. Electronic Proceedings in Theoretical Computer Science, vol.\u00a0332, pp. 35\u201353. Open Publishing Association (2021). https:\/\/doi.org\/10.4204\/EPTCS.332.3","DOI":"10.4204\/EPTCS.332.3"},{"key":"8_CR45","unstructured":"Weber, M.: Free products of higher operad algebras. Theory and Applications of Categories 28(2), 24\u201365 (2013), http:\/\/www.tac.mta.ca\/tac\/volumes\/28\/2\/28-02.pdf"},{"key":"8_CR46","doi-asserted-by":"crossref","unstructured":"Zeilberger, N., Giorgetti, A.: A correspondence between rooted planar maps and normal planar lambda terms. Logical Methods in Computer Science 11 (2015). https:\/\/doi.org\/10.2168\/lmcs-11(3:22)2015","DOI":"10.2168\/LMCS-11(3:22)2015"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57231-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T16:03:38Z","timestamp":1714752218000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57231-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572302","9783031572319"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57231-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"6 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}