Abstract
The framework of action calculi accommodates a variety of disciplines of interaction and computation. A general theory of action calculi is under development; each particular action calculus — such as the π-calculus — will possess also a specific theory. It has previously been shown that any action calculus can be extended in a conservative manner to higher-order, thus allowing its actions to be encapsulated and treated as data. The dynamics of each higher-order calculus includes β-reduction, analogous to the λ-calculus. This paper demonstrates that under an assumption on the arities of a higher-order calculus (analogous to the assumption of simple types in the λ-calculus), β-reduction in higher-order action calculi is strongly normalising.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Cardelli, L, Curien, P.-L. and Lévy J.-J., Explicit Substitutions. ACM POPL Conference, San Francisco (1990).
Barendregt, H., The Lambda Calculus. North Holland (1981).
Hasegawa, M., Private communication.
Kahrs, S., Towards a domain theory for termination proofs. Proc. RTA'95, Lecture Notes in Computer Science 914, Springer-Verlag, Berlin (1995), 241–255.
Lescanne, P., From λδ to λβ, a journey through calculi of explicit substitutions. In: Proc. 21st Annual ACM Symposium on Principles of Programming Languages (1994), 60–69.
Melliès, P.-A., Typed lambda-calculi with explicit substitutions may not terminate. In: M Dezani-Ciancaglini and G Plotkin (Eds), Typed Lambda Calculus and Applications, TLCA'95, Proc. 2nd Int. Conf., Lecture Notes in Computer Science 902, Springer-Verlag, Berlin (1995), 328–334.
Milner, R., Action structures and the π-calculus. In: H. Schwichtenberg (Ed), Proof and Computation, Series F: Computer and Systems Sciences, NATO Advanced Study Institute, Springer Verlag (1994), 219–280.
Milner, R., Calculi for interaction. Acta Informatica 33 (1996), 707–737.
Milner, R., Higher-order action calculi. Proc. CSL conference, Swansea, Lecture Notes in Computer Science 832 (1993), 238–260.
Ritter, E., Normalization for Typed Lambda Calculi with Explicit Substitution. Proc. CSL conference, Swansea, Lecture Notes in Computer Science 832 (1993), 295–304.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Milner, R. (1997). Strong normalisation in higher-order action calculi. In: Abadi, M., Ito, T. (eds) Theoretical Aspects of Computer Software. TACS 1997. Lecture Notes in Computer Science, vol 1281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014545
Download citation
DOI: https://doi.org/10.1007/BFb0014545
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63388-4
Online ISBN: 978-3-540-69530-1
eBook Packages: Springer Book Archive