The true concurrency of differential interaction nets. (English) Zbl 1398.68370
Summary: We analyse the reduction of differential interaction nets from the point of view of so-called ‘true concurrency,’ that is, employing a non-interleaving model of parallelism. More precisely, we associate with each differential interaction net an event structure describing its reduction. We show how differential interaction nets are only able to generate confusion-free event structures, and we argue that this is a serious limitation in terms of the concurrent behaviours they may express. In fact, confusion is an extremely elementary phenomenon in concurrency (for example, it already appears in CCS with just prefixing and parallel composition) and we show how its presence is preserved by any encoding respecting the degree of distribution and the reduction semantics. We thus infer that no reasonably expressive process calculus may be satisfactorily encoded in differential interaction nets. We conclude with an analysis of one such encoding proposed by Ehrhard and Laurent, and argue that it does not contradict our claims, but rather supports them.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
References:
| [1] | Abramsky, S., Computational interpretations of linear logic, Theoretical Computer Science, 111, 3-57, (1993) · Zbl 0791.03003 · doi:10.1016/0304-3975(93)90181-R |
| [2] | Abramsky, S., Proofs as processes, Theoretical Computer Science, 135, 5-9, (1994) · Zbl 0850.68297 · doi:10.1016/0304-3975(94)00103-0 |
| [3] | Alexiev, V. (1999). Non-deterministic Interaction Nets. Ph.D. Thesis, University of Alberta. |
| [4] | Baldan, P., Corradini, A., Montanari, U. and Ribeiro, L. (2007). Unfolding semantics of graph transformation. Information Computation205(5)733-782. doi:10.1016/j.ic.2006.11.004 · Zbl 1115.68093 |
| [5] | Bellin, G. and Scott, P.J. (1994). On the pi-calculus and linear logic. Theoretical Computer Science135(1)11-65. doi:10.1016/0304-3975(94)00104-9 · Zbl 0817.03001 |
| [6] | Boldi, P., Cardone, F. and Sabadini, N. (1993). Concurrent automata, prime event structures and universal domains. In: Droste, M. and Gurevich, Y. (eds.) Semantics of Programming Languages and Model Theory, Algebra, Logic and Applications, vol. 5, Gordon and Breach, 89-108. · Zbl 0803.68035 |
| [7] | Caires, L. and Pfenning, F. (2010). Session types as intuitionistic linear propositions. In: Gastin, P. and Laroussinie, F. (eds.) Proceedings of CONCUR 2010, Lecture Notes in Computer Science, vol. 6269, Springer, 222-236. · Zbl 1287.68125 |
| [8] | Clark, D. and Kennaway, R. (1996). Event structures and non-orthogonal term graph rewriting. Mathematical Structures in Computer Science6(6)545-578. S0960129500070092 · Zbl 0863.68080 |
| [9] | Crafa, S., Varacca, D. and Yoshida, N. (2012). Event structure semantics of parallel extrusion in the pi-calculus. In: Birkedal, L. (ed.) Proceedings of FoSSaCS 2012, Lecture Notes in Computer Science, vol. 7213, Springer, 225-239. · Zbl 1352.68179 |
| [10] | Dorman, A. (2013). Concurrency in Interaction Nets and Graph Rewriting. Ph.D. Thesis, Università degli Studi Roma Tre / Université Paris Nord-Sorbonne Paris Cité. |
| [11] | Ehrhard, T., Finiteness spaces, Mathematical Structures in Computer Science, 15, 615-646, (2005) · Zbl 1084.03048 · doi:10.1017/S0960129504004645 |
| [12] | Ehrhard, T. and Laurent, O. (2010a). Acyclic solos and differential interaction nets. Logical Methods in Computer Science6(3). · Zbl 1214.68246 |
| [13] | Ehrhard, T. and Laurent, O. (2010b). Interpreting a finitary Pi-calculus in differential interaction nets. Information and Computation208(6)606-633. doi:10.1016/j.ic.2009.06.005 · Zbl 1205.68242 |
| [14] | Ehrhard, T. and Regnier, L. (2006). Differential interaction nets. Theoretical Computer Science364(2)166-195. doi:10.1016/j.tcs.2006.08.003 · Zbl 1113.03054 |
| [15] | Girard, J.-Y., Linear logic, Theoretical Computer Science, 50, 1-102, (1987) · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4 |
| [16] | Girard, J.-Y. (1996). Proof-nets: The parallel syntax for proof-theory. In: Ursini and Agliano (eds.), Logic and Algebra. Marcel Dekker, Inc. · Zbl 0868.03025 |
| [17] | Gorla, D., Towards a unified approach to encodability and separation results for process calculi, Information and Computation, 208, 1031-1053, (2010) · Zbl 1209.68336 · doi:10.1016/j.ic.2010.05.002 |
| [18] | Honda, K. and Laurent, O. (2010). An exact correspondence between a typed pi-calculus and polarised proof-nets. Theoretical Computer Science411(22-24)2223-2238. doi:10.1016/j.tcs.2010.01.028 · Zbl 1203.68114 |
| [19] | Khasidashvili, Z. and Glauert, J.R.W. (2005). The conflict-free reduction geometry. Theoretical Computer Science347(3)465-497. doi:10.1016/j.tcs.2004.07.037 · Zbl 1081.68039 |
| [20] | Kobayashi, N., Pierce, B.C. and Turner, D.N. (1999). Linearity and the Pi-Calculus. ACM Transactions on Programming Languages and Systems21(5)914-947. doi:10.1145/330249.330251 |
| [21] | Lafont, Y. (1990). Interaction nets. In: Conference Record of POPL’90, ACM Press, 95-108. |
| [22] | Lafont, Y., Interaction combinators, Information and Computation, 137, 69-101, (1997) · Zbl 0882.68058 · doi:10.1006/inco.1997.2643 |
| [23] | Laneve, C., Parrow, J. and Victor, B. (2001). Solo diagrams. In: Kobayashi, N. and Pierce, B.C. (eds.) Proceedings of TACS 2001, Lecture Notes in Computer Science, vol. 2215, Springer, 127-144. · Zbl 1087.68607 |
| [24] | Laneve, C. and Victor, B. (2003). Solos in concert. Mathematical Structures in Computer Science13(5)657-683. doi:10.1017/S0960129503004055 S0960129503004055 |
| [25] | Mazurkiewicz, A.W. (1986). Trace theory. In: Brauer, W., Reisig, W. and Rozenberg, G. (eds.) Advances in Petri Nets, Lecture Notes in Computer Science, vol. 255, Springer, 279-324. · Zbl 0633.68051 |
| [26] | Mazza, D. (2005). Multiport interaction nets and concurrency. In: Abadi, M. and De Alfaro, L. (eds.) In: Proceedings of CONCUR 2005, Lecture Notes in Computer Science, Springer, 21-35. · Zbl 1134.68449 |
| [27] | Mazza, D. (2006). Interaction nets: Semantics and concurrent extensions. Ph.D. Thesis, Université de la Méditerranée / Università degli Studi Roma Tre. |
| [28] | Melliès, P.-A., Asynchronous games 2: The true concurrency of innocence, Theoretical Computer Science, 358, 200-228, (2004) · Zbl 1099.68072 |
| [29] | Mimram, S. (2008). Sémantique des jeux asynchrone et réécriture 2-dimensionelle. Ph.D. Thesis, Université Paris-Diderot (Paris 7). |
| [30] | Nielsen, M., Plotkin, G.D. and Winskel, G. (1981). Petri nets, event structures and domains, part I. Theoretical Computer Science13(1)85-108. doi:10.1016/0304-3975(81)90112-2 · Zbl 0452.68067 |
| [31] | Parrow, J., Expressiveness of process algebras, Electronic Notes in Theoretical Computer Science, 209, 173-186, (2008) · Zbl 1279.68264 · doi:10.1016/j.entcs.2008.04.011 |
| [32] | Parrow, J. and Sjodin, P. (1992). Multiway synchrinizaton verified with coupled simulation. In: Cleaveland, R. (ed.) Proceedings of CONCUR’92, Lecture Notes in Computer Science (LNCS), vol. 630, Springer, 518-533. |
| [33] | Parrow, J. and Victor, B. (1998). The fusion calculus: Expressiveness and symmetry in mobile processes. In: Proceedings of LICS, IEEE Computer Society, 176-185. |
| [34] | Rabinovitch, A. and Traktenbrot, B. (1988). Behaviour structures and nets. Fundamenta Informatica11(4)357-404. · Zbl 0657.68068 |
| [35] | Rozenberg, G. and Engelfriet, J. (1996). Elementary net systems. In: Dagstuhl Lectures on Petri Nets, Lecture Notes in Computer Science, vol. 1491, Springer, 12-121. · Zbl 0926.68082 |
| [36] | Stark, E. W., Concurrent transition systems, Theoretical Computer Science, 64, 221-269, (1989) · Zbl 0671.68027 · doi:10.1016/0304-3975(89)90050-9 |
| [37] | Van Glabeek, R.J. and Goltz, U. (1989). Equivalence notions for concurrent systems and refinement of actions. In: Proceedings of MFCS 1989, Lecture Notes in Computer Science (LNCS), vol. 379, Springer-Verlag. · Zbl 0755.68095 |
| [38] | Varacca, D., Völzer, H. and Winskel, G. (2006). Probabilistic event structures and domains. Theoretical Computer Science358(2-3)173-199. doi:10.1016/j.tcs.2006.01.015 · Zbl 1099.68054 |
| [39] | Winskel, G. (1982). Event structure semantics of CCS and related languages. In: Nielsen, M. and Schmidt, E.M. (eds.), Proceedings of ICALP 1982, Lecture Notes in Computer Science vol. 140, Springer, 561-576. · Zbl 0518.68045 |
| [40] | Winskel, G. and Nielsen, M. (1995). Models for concurrency. In: Handbook of Logic in Computer Science, vol. 4, Oxford University Press. · Zbl 0874.68120 |
| [41] | Wischik, L. and Gardner, P. (2005). Explicit fusions. Theoretical Computer Science340(3)606-630. doi:10.1016/j.tcs.2005.03.017 · Zbl 1077.68066 |
| [42] | Yoshida, N., Berger, M. and Honda, K. (2004). Strong normalisation in the pi-calculus. Information and Computation191(2)145-202. doi:10.1016/j.ic.2003.08.004 · Zbl 1101.68705 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
