A calculus of higher order communicating systems

ABSTRACT

In this paper we present A Calculus of Higher Order Communicating Systems. This calculus considers sending and receiving processes to be as fundamental as nondeterminism and parallel composition. The calculus is an extension of CCS [Mil80] in the sense that all the constructions of CCS are included or may be derived from more fundamental constructs and most of the mathematical framework of CCS carries over almost unchanged. Clearly CCS with processes as first class objects is a powerful metalanguage and we show that it is possible to simulate the untyped &lgr;-calculus in CHOCS. The relationship between CHOCS and the untyped &lgr;-calculus is further strengthened by a result showing that the recursion operator is unnecessary in the sense that recursion can be simulated by means of process passing and communication. As pointed out by R. Milner in [Mil80], CCS has its limitations when one wants to describe unboundedly expanding systems as e.g. an unbounded number of procedure invocations in an imperative concurrent programming language. We show how neatly CHOCS may describe both call by value and call by reference parameter mechanisms for the toy language of chapter 6 in [Mil80].

REFERENCES

• Abr87a: S. Abramsky: Domain Theory in Logical Form, Proceedings of LICS 87. Full version submitted to AnnMs of Pure and Applied Logic, 1987.
• Abr87b: S. Abr~msky: A Domain Equation For Bisimulation, Unpublished manuscript, Dept. Computing, Imperial College, London 1987.
• Abr88: S. Abr~msky: The Lazy Lambda Calculus, to appear in Declarative Prg. ed. D. Turner, Addison Wesley, 1988.
• AusBou84: D. Austry & G. Boudol: Alg~bre de Processus et Synchronisatiou, Theoretical Computer Science 30(1) pp. 91-131, 1984.
• AstReg87: E. Astesiano , G. Reggio, SMoLCS-driven concurrent calculi, The International Joint Conference on theory and practice of software development on TAPSOFT '87, p.169-201, January 1987, Pisa, Italy
• Bar85: H.P. Barendreght: The Lambda Calculus -- Its Syntaz and Semantics, North-Holland 1985.
• BerKlo84: j. Bergstra & J. W. Klop: Process Algebra for Synchronous Communication, Information and Control 60, pp. 109-137, 1984.
• Bou88: G. Boudol: Towards a Lambda-Calculus for Concurrent and Communicating Systems~ Research Report hr. 885, INRIA Sophia Antipolis, Autumn 1988.
• Chr88: P. Christen~en: The Domain of CSP Proce~se~, incomplete draft, The Technical University of Denmark, 1988.
• CouCou79: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• dNiHen87: R. De Nicola , M. Hannessy, CCS without &tgr;'s, The International Joint Conference on theory and practice of software development on TAPSOFT '87, p.138-152, January 1987, Pisa, Italy
• EngNie86: U. Engberg & M. Nielsen: A Calculus of Communicating Systems with Label Passing, DAIMI PB-208 Aarhus University Computer Science Department, 1986.
• HenMil85: Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
• KenSle83: Richard Kennaway , M. Ronan Sleep, Syntax and informal semantics of DyNe, a parallel language, The Analysis of Concurrent Systems, p.222-230, September 12-16, 1983
• KenSle88: J. R. Kennaway & M. R. Sleep: A Denotational Semantics for First Class Processes, Draft, School of Information Systems, University of East Anglia, Norwich, U.K., August 1988.
• Mil80: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• Mil81: R. Milner: A Complete Inference System for a Class of Regular Behaviours, University of Edinburgh 1981.
• Mil83: R. Milner: Calculi for Synchrony and Asynchrony, Theoretical Computer Science 25 (1983), pp 269-310, North Holland.
• Mil83b: K. Mihter: Parallel Combinator Reduction Machine, LNCS 207, Springer Verlag, 1983.
• Nie88: F. Nielson: The Typed .~-Calculus with First- Class Processe,~, Technical Report ID-TR: 1988- 43 ISSN 0902-2821, Department of Computer Science, Technical University of Denmark, August 1988.
• Par81: David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the 5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981
• Plo81: G. Plotkin: A Structural Approach to Operational Semantics, DAIMI FN-19 Aarhus University Computer Science Department 1981.
• Pra88: K. V. S. Prasad, Combinators and bisimulation proofs for restartable systems, 1987
• Tar55: A. Tarski: A Lattice-Theoretical Fixpoint Theorem and Its Applications, Pacific Journal of Math. 5, 1955.
• Wal88: D. Walker: Bi~simulation and Divergence, Proc. of LICS 88, ISBN 0-8186-0853-6.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages

          Nouns: CCS

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax; Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Design, Languages, Theory