{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:40Z","timestamp":1714413220230},"reference-count":22,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5207,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1994,12]]},"abstract":"<jats:p>We introduce a new class of higher order rewriting systems, called Interaction Systems (IS's). IS's are derived from Lafont's (Intuitionistic) Interaction Nets (Lafont 1990) by dropping the linearity constraint. In particular, we borrow from Interaction Nets the syntactical bipartitions of operators into constructors and destructors and the principle of <jats:italic>binary interaction<\/jats:italic>. As a consequence, IS's are a subclass of Klop's Combinatory Reduction Systems (Klop 1980), where the Curry-Howard analogy still \u2018makes sense\u2019. Destructors and constructors, respectively, correspond to left and right logical introduction rules: interaction is cut and reduction is cut-elimination.<\/jats:p><jats:p>Interaction Systems have been primarily motivated by the necessity of extending the practice of optimal evaluators for \u03bb-calculus (Lamping 1990; Gonthier <jats:italic>et al.<\/jats:italic> 1992a) to other computational constructs such as conditionals and recursion. In this paper we focus on the theoretical aspects of optimal reductions. In particular, we generalize the <jats:italic>family relation<\/jats:italic> in L\u00e9vy (1978; 1980), thus defining the <jats:italic>amount of sharing<\/jats:italic> an optimal evaluator is required to perform. We reinforce our notion of family by approaching it in two different ways (generalizing labelling and extraction in Levy (1980)) and proving their coincidence. The reader is referred to Asperti and Laneve (1993c) for the paradigmatic description of optimal evaluators of IS's.<\/jats:p>","DOI":"10.1017\/s0960129500000566","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:00:57Z","timestamp":1236157257000},"page":"457-504","source":"Crossref","is-referenced-by-count":20,"title":["Interaction Systems I: The theory of optimal reductions"],"prefix":"10.1017","volume":"4","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cosimo","family":"Laneve","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000566_ref022","unstructured":"Regnier L. (1992) Lambda Calcul et Reseaux, Ph.D. thesis, Universit\u00e9 Paris VII."},{"key":"S0960129500000566_ref021","doi-asserted-by":"crossref","unstructured":"Maranget L. (1991) Optimal Derivations in Weak lambda-calculi and in Orthogonal Terms Rewriting Systems. In Proceedings 17th ACM Symposium on Principles of Programmining Languages 255\u2013269.","DOI":"10.1145\/99583.99618"},{"key":"S0960129500000566_ref020","first-page":"63","volume-title":"Proceedings 6th Annual Symposium on Logic in Computer Science","author":"Malacaria","year":"1991"},{"key":"S0960129500000566_ref008","doi-asserted-by":"crossref","unstructured":"Field J. (1990) On laziness and optimality in lambda interpreters: tools for specification and analysis. In Proceedings 17th ACM Symposium on Principles of Programmining Languages 1\u201315.","DOI":"10.1145\/96709.96710"},{"key":"S0960129500000566_ref014","unstructured":"Klop J. W. (1980) Combinatory Reduction System, Ph.D. thesis, Mathematisch Centrum, Amsterdam."},{"key":"S0960129500000566_ref019","first-page":"159","volume-title":"To H. B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Levy","year":"1980"},{"key":"S0960129500000566_ref018","unstructured":"L\u00e9vy J. J. (1978) R\u00e9ductions correctes et optimales dans le lambda calcul, Ph.D. thesis, Universit\u00e9 Paris VII."},{"key":"S0960129500000566_ref002","unstructured":"Asperti A. and Laneve C. (1992) Interaction Systems I: the theory of optimal reductions. Technical Report 1748, INRIA-Rocquencourt."},{"key":"S0960129500000566_ref013","unstructured":"Kathail V. (1990) Optimal Interpreters for lambda-calculus based functional languages, Ph.D. thesis, MIT."},{"key":"S0960129500000566_ref001","unstructured":"Aczel P. (1978) A general Church-Rosser theorem. Draft, Manchester."},{"key":"S0960129500000566_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56610-4_84"},{"key":"S0960129500000566_ref005","unstructured":"Asperti A. and Laneve C. (1993c) Interaction Systems II: the practice of optimal reductions. Technical Report UBLCS\u201393\u201312, Laboratory for Computer Science, Universit\u00e1 di Bologna, May 1993. Also Research Report n. 2001, INRIA-Sophia Antipolis. (Also available via anonymous ftp on ftp.cs.unibo.it in the directory \/pub\/TR\/UBLCS under the name 93\u201312.ps.Z.)"},{"key":"S0960129500000566_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56868-9_13"},{"key":"S0960129500000566_ref006","first-page":"23","volume-title":"Springer-Verlag Lecture Notes in Computer Science","author":"Asperti","year":"1994"},{"key":"S0960129500000566_ref007","unstructured":"Danos V. (1990) La Logique Lin\u00e9are appliqu\u00e9e \u00e1 l'\u00e9tude de divers processus de normalisation (prin-cipalement du \u03bb-calcul), Ph.D. thesis, Universit\u00e9 Paris VII."},{"key":"S0960129500000566_ref009","first-page":"50","article-title":"Linear Logic","author":"Girard","year":"1986","journal-title":"Theoretical Computer Science"},{"key":"S0960129500000566_ref010","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0960129500000566_ref011","doi-asserted-by":"crossref","unstructured":"Gonthier G. , Abadi M. and L\u00e9vy J. J. (1992a) The geometry of optimal lambda reduction. In Proceedings 19th ACM Symposium on Principles of Programmining Languages 15\u201326.","DOI":"10.1145\/143165.143172"},{"key":"S0960129500000566_ref012","unstructured":"Gonthier G. , Abadi M. and L\u00e9evy J. J. (1992b) Linear logic without boxes. In Proceedings 7th Annual Symposium on Logic in Computer Science"},{"key":"S0960129500000566_ref015","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96718"},{"key":"S0960129500000566_ref016","doi-asserted-by":"crossref","unstructured":"Lamping J. (1990) An algorithm for optimal lambda calculus reductions. In Proceedings 17th ACM Symposium on Principles of Programmining Languages 16\u201330.","DOI":"10.1145\/96709.96711"},{"key":"S0960129500000566_ref017","unstructured":"Laneve C. (1993) Optimality and Concurrency in Interaction Systems, Ph.D. thesis, Dip. Informatica, Universit\u00e0 di Pisa. Technical Report TD-8\/93."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000566","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T21:55:09Z","timestamp":1557870909000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000566\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,12]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1994,12]]}},"alternative-id":["S0960129500000566"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000566","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,12]]}}}