Abstract
Action calculi are a broad class of algebraic structures, including a formulation of Petri nets as well as a formulation of the π-calculus. Each action calculus HAC(K) is generated by a particular set K of operators called controls. The purpose of this paper is to extend action calculi in a uniform manner to higher-order. A special case is essentially the extension of the π-calculus to higher order by Sangiorgi. To establish a link between the interactive and functional paradigms of computation, a variety of the λ-calculus is obtained as the extension of the smallest action calculus HAC(θ).
The dynamics of higher-order action calculi is presented, blending communication -for example in process calculi- with reduction as in the λ-calculus. Strong normalisation is obtained for reduction. A set of equational axioms is given for higher-order action calculi. Taking the quotient of HAC(θ) by a single extra axiom η, a cartesian-closed category is obtained.
An ultimate goal of the paper is to combine process calculi and functional calculi, both in their formulation and in their semantics.
This work was done with the support of a Senior Fellowship from the Science and Engineering Research Council, UK.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, Explicit Substitutions, ACMPOPL Conference, San Francisco, 1990.
Asperti, A. and Laneve, C., Interaction systems, Proc. International Workshop on Higher-order algebra, Logic and Term rewriting, Amsterdam, September 1993.
Asperti, A. and Longo, G., Categories, Types and Structures, MIT Press, 1991.
Barendregt, H., The Lambda Calculus, North Holland 1981.
Berry, G. and Boudol, G., The chemical abstract machine, Journal of Theoretical Computer Science, Vol 96, pp 217–248, 1992.
Danos, V. and Regnier, L., Local and asynchronous beta-reduction, Proc. LICS, Montreal, 1993.
Giacalone, P., Mishra, P. and Prasad, S., Facile: a symmetric integration of concurrent and functional programming, International Journal of Parallel Programming, Vol 18, pp121–160, 1989.
Gunter, C.A., Semantics of Programming Languages, MIT Press, 1992.
Lambek, J. and Scott, P.J., Introduction to Higher-order Categorical Logic, Cambridge University Press,1986.
Milner, R., The polyadic π-calculus: a tutorial, in Logic and Algebra of Specification, ed. F.L. Bauer, W. Brauer and H. Schwichtenberg, Springer Verlag, 1993.
Milner, R., Action structures and the π-calculus, to appear in Proceedings of NATO Advanced Study Institute on Proof and Computation (held at Marktoberdorf, 1993), about 60pages. (This paper combines of two previous reports: Action structures, Research Report ECS-LFCS-92-249, and Action structures for the π-calculus, Research Report ECS-LFCS-93-264, Laboratory for Foundations of Computer Science, Computer Science Department, Edinburgh University.
Milner, R., Action calculi I: axioms and applications, Computer Science Department, Edinburgh University, 1993. Also appeared as Action calculi, or syntactic action structures, Proceedings of MFCS '93, Lecture Notes in Computer Science Vol 711, Springer-Verlag, pp105–121, 1993.
Milner, R., Action calculi II: π-nets with boxes and replication, Computer Science Department, Edinburgh University, 1993.
Milner, R., Parrow, J. and Walker, D., A calculus of mobile processes, Parts I and II, Journal of Inf. and Comp, Vol 100, pp1–40 and pp41–77, 1992.
Petri, C.A., Fundamentals of a theory of asynchronous information flow, Proc. IFIP Congress '62, North Holland, pp386–390, 1962.
Pierce, B.C., Programming in the π-calculus, Draft, Computer Science Department, University of Edinburgh, 1993.
Pitts, A.M. and Stark, I.D.B., Observable properties of higher-order functions that dynamically create local names, or: What's new?, Proc. MFCS'93, Lecture Notes in Computer Science Vol 711, Springer-Verlag, pp122–141, 1993.
Ritter, E., Normalization for Typed Lambda Calculi with Explicit Substitution, Paper presented at the 1993 Annual Conference of the European Association for Computer Science Logic, Swansea 1993.
Sangiorgi, D., Expressing mobility in process algebras: first-order and higher-order paradigms, PhD Thesis, CST-99-93, Computer Science Department, University of Edinburgh, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Milner, R. (1994). Higher-order action calculi. In: Börger, E., Gurevich, Y., Meinke, K. (eds) Computer Science Logic. CSL 1993. Lecture Notes in Computer Science, vol 832. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0049335
Download citation
DOI: https://doi.org/10.1007/BFb0049335
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58277-9
Online ISBN: 978-3-540-48599-5
eBook Packages: Springer Book Archive