Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-12-01T08:50:34.927Z Has data issue: false hasContentIssue false
  • English
  • Français

Interaction Systems I: The theory of optimal reductions†

Published online by Cambridge University Press:  04 March 2009

Andrea Asperti  and
Cosimo Laneve
Andrea Asperti
Affiliation:
Dip. di Matematica, Universitá di Bologna, P.za di Porta S.Donato, 40126, Bologna, Italy. Email: [email protected]
Cosimo Laneve
Affiliation:
INRIA Sophia Antipolis, 2004 Route des Lucioles BP 93, 06902, Valbonne, France. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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 binary interaction. As a consequence, IS's are a subclass of Klop's Combinatory Reduction Systems (Klop 1980), where the Curry-Howard analogy still ‘makes sense’. Destructors and constructors, respectively, correspond to left and right logical introduction rules: interaction is cut and reduction is cut-elimination.

Interaction Systems have been primarily motivated by the necessity of extending the practice of optimal evaluators for λ-calculus (Lamping 1990; Gonthier et al. 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 family relation in Lévy (1978; 1980), thus defining the amount of sharing 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.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 4 , Issue 4 , December 1994 , pp. 457 - 504
Copyright
Copyright © Cambridge University Press 1994

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aczel, P. (1978) A general Church-Rosser theorem. Draft, Manchester.Google Scholar
Asperti, A. and Laneve, C. (1992) Interaction Systems I: the theory of optimal reductions. Technical Report 1748, INRIA-Rocquencourt.Google Scholar
Asperti, A. and Laneve, C. (1993a) Optimal Reductions in Interaction Systems. In TapSoft '93. Springer-Verlag Lecture Notes in Computer Science 668 485–500.Google Scholar
Asperti, A. and Laneve, C. (1993b) Paths, Computations and Labels in the λ-calculus. In RTA '93. Springer-Verlag Lecture Notes in Computer Science 690 152–167.Google Scholar
Asperti, A. and Laneve, C. (1993c) Interaction Systems II: the practice of optimal reductions. Technical Report UBLCS–93–12, Laboratory for Computer Science, Universitá 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–12.ps.Z.)Google Scholar
Asperti, A. and Laneve, C. (1994) Interaction Systems. In Proc. of Higher Order Algebras, Logic and Term Rewriting September 1993, Amsterdam23–24. (To appear in Springer-Verlag Lecture Notes in Computer Science.)Google Scholar
Danos, V. (1990) La Logique Linéare appliquée á l'étude de divers processus de normalisation (prin-cipalement du λ-calcul), Ph.D. thesis, Université Paris VII.Google Scholar
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–15.Google Scholar
Girard, J. Y. (1986) Linear Logic. Theoretical Computer Science 50.Google Scholar
Girard, J. Y., Taylor, P. and Lafont, Y. (1989) Proofs and Types, Cambridge University Press.Google Scholar
Gonthier, G., Abadi, M. and Lévy, J. J. (1992a) The geometry of optimal lambda reduction. In Proceedings 19th ACM Symposium on Principles of Programmining Languages 15–26.Google Scholar
Gonthier, G., Abadi, M. and Léevy, J. J. (1992b) Linear logic without boxes. In Proceedings 7th Annual Symposium on Logic in Computer ScienceGoogle Scholar
Kathail, V. (1990) Optimal Interpreters for lambda-calculus based functional languages, Ph.D. thesis, MIT.Google Scholar
Klop, J. W. (1980) Combinatory Reduction System, Ph.D. thesis, Mathematisch Centrum, Amsterdam.Google Scholar
Lafont, Y. (1990) Interaction Nets. In Proceedings 17th ACM Symposium on Principles of Program-mining Languages 95–108.Google Scholar
Lamping, J. (1990) An algorithm for optimal lambda calculus reductions. In Proceedings 17th ACM Symposium on Principles of Programmining Languages 16–30.Google Scholar
Laneve, C. (1993) Optimality and Concurrency in Interaction Systems, Ph.D. thesis, Dip. Informatica, Università di Pisa. Technical Report TD-8/93.Google Scholar
Lévy, J. J. (1978) Réductions correctes et optimales dans le lambda calcul, Ph.D. thesis, Université Paris VII.Google Scholar
Levy, J. J. (1980) Optimal reductions in the lambda-calculus. In: Seldin, J. P. and Hindley, J. R. (eds.) To H. B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 159–191.Google Scholar
Malacaria, P. and Regnier, L. (1991) Some results on the interpretation of λ-calculus in operator algebras. In Proceedings 6th Annual Symposium on Logic in Computer Science, Amsterdam63–72.Google Scholar
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–269.Google Scholar
Regnier, L. (1992) Lambda Calcul et Reseaux, Ph.D. thesis, Université Paris VII.Google Scholar