{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T04:13:00Z","timestamp":1744171980386,"version":"3.40.3"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T00:00:00Z","timestamp":1744070400000},"content-version":"unspecified","delay-in-days":97,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n\t  <jats:p>We show that the <jats:italic>principal types<\/jats:italic> of the closed terms of the affine fragment of \u03bb-calculus, with respect to a simple type discipline, are structurally isomorphic to their interpretations, as <jats:italic>partial involutions<\/jats:italic>, in a natural <jats:italic>Geometry of Interaction<\/jats:italic> model \u00e0 la Abramsky. This permits to explain in elementary terms the somewhat awkward notion of <jats:italic>linear application<\/jats:italic> arising in <jats:italic>Geometry of Interaction<\/jats:italic>, simply as the <jats:italic>resolution<\/jats:italic> between principal types using an alternate unification algorithm. As a consequence, we provide an answer, for the purely affine fragment, to the open problem raised by Abramsky of characterizing those partial involutions which are denotations of combinatory terms.<\/jats:p>","DOI":"10.1017\/s0960129524000380","type":"journal-article","created":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T06:16:18Z","timestamp":1744092978000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Principal types as partial involutions"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8937-1892","authenticated-orcid":false,"given":"Furio","family":"Honsell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marina","family":"Lenisa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ivan","family":"Scagnetto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2025,4,8]]},"reference":[{"key":"S0960129524000380_ref2","volume-title":"Lecture Notes","author":"Abramsky","year":"1997"},{"key":"S0960129524000380_ref9","unstructured":"Abramsky, S. and Longley, J. (2000). Realizability models based on history-free strategies. Draft manuscript"},{"key":"S0960129524000380_ref14","doi-asserted-by":"crossref","unstructured":"Ciaffaglione, A. , Honsell, F. , Lenisa, M. and Scagnetto, I. (2018). The Involutions-as-principal type\/application-as-unification Analogy. In: Barthe, G., Sutcliffe, G., and Veanes, M. (eds.) 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2018), EasyChair, 254\u2013270.","DOI":"10.29007\/ntwg"},{"key":"S0960129524000380_ref30","unstructured":"Levy, J.-J. (1978). R\u00e9ductions correctes et optimales dans le lambda-calcul. Th\u00e8se de doctorat d\u2019\u00e9tat, Universit e Paris VII."},{"key":"S0960129524000380_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.08.003"},{"key":"S0960129524000380_ref13","unstructured":"Ciaffaglione, A. , Di Gianantonio, P. , Honsell, F. , Lenisa, M. and Scagnetto, I. (2019a). \u03bb!-calculus, intersection types, and involutions. In: Geuvers, H. (ed.) Formal Structures for Computation and Deduction (FSCD 2019), vol.131, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 1\u201316."},{"key":"S0960129524000380_ref15","doi-asserted-by":"crossref","unstructured":"Coppo, M. , Dezani-Ciancaglini, M. , Honsell, F. and Longo, G. (1984).Extended type structures and filter lambda models. Logic Colloquium 112 241\u2013262.","DOI":"10.1016\/S0049-237X(08)71819-6"},{"key":"S0960129524000380_ref11","volume-title":"Studies in Logic","volume":"103","author":"Barendregt","year":"1984"},{"key":"S0960129524000380_ref6","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1006\/inco.1994.1041","article-title":"New foundations for the geometry of interaction","volume":"111","author":"Abramsky","year":"1994","journal-title":"Information and Computation"},{"key":"S0960129524000380_ref12","first-page":"931","article-title":"Reversible computation and principal types in \u03bb!-calculus","volume":"25","author":"Ciaffaglione","year":"2019","journal-title":"The Bulletin of Symbolic Logic"},{"key":"S0960129524000380_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003730"},{"key":"S0960129524000380_ref18","unstructured":"Di Gianantonio, P. and Lenisa, M. (2022) Principal Types as Lambda Nets. In: Basold, H., Cockx, J., and Ghilezan, S. (eds.) Types for Proofs and Programs (TYPES 2021), vol. 239. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 1\u201323."},{"key":"S0960129524000380_ref10","first-page":"1","article-title":"Elementary complexity and geometry of interaction","volume":"45","author":"Baillot","year":"2001","journal-title":"Fundamenta Informaticae"},{"key":"S0960129524000380_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"key":"S0960129524000380_ref5","doi-asserted-by":"publisher","DOI":"10.2307\/2275407"},{"key":"S0960129524000380_ref17","unstructured":"Danos, V. and Regnier, L. (1993). Local and asynchronous beta-reduction. In: Proceedings of the Eighth International Symposium on Logic in Computer Science (LICS 1993), New York: IEEE Press, 296\u2013306"},{"key":"S0960129524000380_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.002"},{"key":"S0960129524000380_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199483"},{"key":"S0960129524000380_ref7","doi-asserted-by":"crossref","unstructured":"Abramsky, S. and Lenisa, M. (2001). Fully Complete Minimal PER Models for the Simply Typed Lambda-calculus. In: Fribourg, L. (ed.) CSL\u20192001 Conference Proceedings, Springer. Lecture Notes in Computer Science 2142 443\u2013457.","DOI":"10.1007\/3-540-44802-0_31"},{"key":"S0960129524000380_ref19","first-page":"221","volume-title":"Logic Colloquium \u201988","author":"Girard","year":"1989"},{"key":"S0960129524000380_ref26","volume-title":"Introduction to Combinators and the \u03bb-Calculus","author":"Hindley","year":"1986"},{"key":"S0960129524000380_ref29","volume-title":"44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs)","author":"Honsell","year":"2024"},{"key":"S0960129524000380_ref32","doi-asserted-by":"crossref","first-page":"623","DOI":"10.1017\/S0956796804005131","article-title":"Linear lambda calculus and PTIME-completeness","volume":"14","author":"Mairson","year":"2004","journal-title":"Journal of Functional Programming"},{"key":"S0960129524000380_ref1","first-page":"1","volume-title":"CONCUR\u201996 Conference Proceedings","author":"Abramsky","year":"1996"},{"key":"S0960129524000380_ref16","doi-asserted-by":"crossref","unstructured":"Danos, V. , Herbelin, H. and Regnier, L. (1996). Game Semantics & Abstract Machines. In: Proceedings of the Eleventh International Symposium on Logic in Computer Science (LICS 1996), New York: IEEE Press, 394\u2013405","DOI":"10.1109\/LICS.1996.561456"},{"key":"S0960129524000380_ref27","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(93)90171-O","article-title":"Principal types of BCK-lambda-terms","volume":"107","author":"Hirokawa","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"S0960129524000380_ref22","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1006\/inco.1998.2700","article-title":"Light linear logic","volume":"143","author":"Girard","year":"1998","journal-title":"Information and Computation"},{"key":"S0960129524000380_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143172"},{"key":"S0960129524000380_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90100-X"},{"key":"S0960129524000380_ref34","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"Journal of the ACM"},{"key":"S0960129524000380_ref20","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/3-540-52335-9_49","volume-title":"COLOG-88: International Conference on Computer Logic","author":"Girard","year":"1990"},{"key":"S0960129524000380_ref28","unstructured":"Honsell, F. , Lenisa, M. and Scagnetto, I. (2020). \u039b -Symsym: An Interactive Tool for Playing with Involutions and Types. In: de\u2019Liguoro, U., Berardi, S., and Altenkirch, T. 26th International Conference on Types for Proofs and Programs, TYPES, vol. 7, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik,1\u201318."},{"key":"S0960129524000380_ref21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129524000380","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T06:17:20Z","timestamp":1744093040000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129524000380\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":33,"alternative-id":["S0960129524000380"],"URL":"https:\/\/doi.org\/10.1017\/s0960129524000380","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}],"article-number":"e8"}}