Combinatory representation of mobile processes

ABSTRACT

A theory of combinators in the setting of concurrent processes is formulated. The new combinators are derived from an analysis of the operation called asynchronous name passing, just as an analysis of logical substitution gave rise to the sequential combinators. A system with seven atoms and fixed interaction rules, but with no notion of prefixing, is introduced, and is shown to be capable of representing input and output prefixes over arbitrary terms in a behaviourally correct way, just as SK-combinators are closed under functional abstraction without having it as a proper syntactic construct. The basic equational correspondence between concurrent combinators and a system of asynchronous mobile processes, as well as the embedding of the finite part of &pgr;-calculus in concurrent combinators, is proved. These results will hopefully serve as a cornerstone for further investigation of the theoretical as well as pragmatic possibilities of the presented construction.

REFERENCES

• 1: Samson Abramsky, The lazy lambda calculus, Research topics in functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 2: Barendregt, H., The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984.
• 3: Gérard Berry , Gérard Boudol, The chemical abstract machine, Theoretical Computer Science, v.96 n.1, p.217-248, 6 April 1992
• 4: Boudol, G., Asynchrony and 7r-calculus. INRIA Report 1702, INRIA, Sophia Antipolis, 1991.
• 5: Curry, H. B. and Feys, R., Combinatory Logic, Vol. L North Holland, 1958.
• 6: Engberg, U. and Nielsen, M., A Calculus of Communicating Systems with Label Passing. Research Report DAIMI PB-208, Computer Science Department, University of Aarhus, 1986.
• 7: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 8: Hewitt, C., Bishop, P., and Steiger, R., A Universal Modular ACTOR Formalism for Artificial Intelligence. Proc. o/the 3rd International Joint Conference on Artificial Intelligence, pp.235-245, 1973.
• 9: J. Roger Hindley , Jonathan P. Seldin, Introduction to combinators and &lgr;-calculus, Cambridge University Press, New York, NY, 1986
• 10: Kohei Honda , Mario Tokoro, An Object Calculus for Asynchronous Communication, Proceedings of the European Conference on Object-Oriented Programming, p.133-147, July 15-19, 1991
• 11: Honda, K., Two bisimilarities in v-calculus. Keio CS report 92-002, Department of Computer Science, Keio University, 1992.
• 12: Kohei Honda, Types for Dynamic Interaction, Proceedings of the 4th International Conference on Concurrency Theory, p.509-523, August 23-26, 1993
• 13: Kohei Honda , Nobuko Yoshida, On reduction-based process semantics, Selected papers of the thirteenth conference on Foundations of software technology and theoretical computer science, p.437-486, November 1995, Bombay, India
• 14: Kohei Honda , Nobuko Yoshida, Replication in Concurrent Combinators, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.786-805, April 19-22, 1994
• 15: Honda, K., Kubo, M., and Yoshida, N., Combinatory Representation of Mobile Processes: Part I. To appear as a Keio CS report.
• 16: Cliff B. Jones, Constraining Inference in an Object-Based Design Model, Proceedings of the International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.136-150, April 13-17, 1993
• 17: Jones, C.B., Process-Algebraic Foundations for an Object.Based Design Notation. UMCS-93-10-1, Computer Science Department, Manchester University, 1993.
• 18: Yves Lafont, Interaction nets, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.95-108, December 1989, San Francisco, California, United States [doi>10.1145/96709.96718]
• 19: Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, I, Information and Computation, v.100 n.1, p.1-40, Sept. 1992 [doi>10.1016/0890-5401(92)90008-4]
• 20: Milner, R., Functions as Processes. Mathematical Structure in Computer Science, 2(2), pp.119-146, 1992.
• 21: Milner, R., Polyadic 7r-Calculus: a tutorial. Logic and Algebra of Specification, Springer-Verlag, 1992.
• 22: Robin Milner , Davide Sangiorgi, Barbed Bisimulation, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.685-695, July 13-17, 1992
• 23: SchSnfinkel, M., Uber die Bausteine der mathematischen Logik. Math. Annalen 92, pp.305-316, 1924. Engl. trans, in J. van Heijenoort, editor, From Frege to GSdel, pp.355-366, Harvard Univ. Press, 1967.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

General Terms:
Languages, Theory, Verification