{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T21:21:57Z","timestamp":1649020917360},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"In 2005, S. Abramsky introduced various universal models of computation based on Affine Combinatory Logic, consisting of partial involutions over a suitable formal language of moves, in order to discuss reversible computation in a game-theoretic setting. We investigate Abramsky\u2019s models from the point of view of the model theory of \u03bb-calculus, focusing on the purely linear and affine fragments of Abramsky\u2019s Combinatory Algebras.<\/jats:p>Our approach stems from realizing a structural analogy, which had not been hitherto pointed out in the literature, between the partial involution interpreting a combinator and the principal type of that term, with respect to a simple types discipline for \u03bb-calculus. This analogy allows for explaining as unification between principal types the somewhat awkward linear application of involutions arising from Geometry of Interaction (GoI).<\/jats:p>Our approach provides immediately an answer to the open problem, raised by Abram- sky, of characterising those finitely describable partial involutions which are denotations of combinators, in the purely affine fragment. We prove also that the (purely) linear combinatory algebra of partial involutions is a (purely) linear \u03bb-algebra, albeit not a combinatory model, while the (purely) affine combinatory algebra is not. In order to check the complex equations involved in the definition of affine \u03bb-algebra, we implement in Erlang the compilation of \u03bb-terms as involutions, and their execution.<\/jats:p>","DOI":"10.29007\/ntwg","type":"proceedings-article","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T20:06:42Z","timestamp":1540325202000},"source":"Crossref","is-referenced-by-count":0,"title":["The involutions-as-principal types\/application-as-unification Analogy"],"prefix":"10.29007","author":[{"given":"Alberto","family":"Ciaffaglione","sequence":"first","affiliation":[]},{"given":"Furio","family":"Honsell","sequence":"additional","affiliation":[]},{"given":"Marina","family":"Lenisa","sequence":"additional","affiliation":[]},{"given":"Ivan","family":"Scagnetto","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T20:06:58Z","timestamp":1540325218000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/GRzV"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"http:\/\/dx.doi.org\/10.29007\/ntwg","relation":{},"ISSN":["2398-7340"],"issn-type":[{"value":"2398-7340","type":"print"}]}}