Strong normalisation in the \(\pi\)-calculus. (English) Zbl 1101.68705
Summary: We introduce a typed \(\pi\)-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed \(\lambda\)-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed \(\lambda\)-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
References:
| [1] | Abramsky, S., Computational interpretation of linear logic, TCS, 111, 3-57 (1993) · Zbl 0791.03003 |
| [2] | Abramsky, S., Proofs as processes, TCS, 135, 5-9 (1994) · Zbl 0850.68297 |
| [3] | Abramsky, S.; Jagadeesan, R., Games and full completeness for multiplicative linear logic, JSL, 59 (1994) · Zbl 0822.03007 |
| [4] | Abramsky, S.; Jagadeesan, R.; Malacaria, P., Full abstraction for PCF, Inform. Comput., 163, 409-470 (2000) · Zbl 1006.68028 |
| [5] | S. Abramsky, Process Realizability, A Tutorial Workshop on Realizability Semantics and Applications, 1999. Available from <web.comlab.ox.ac.uk/oucl/work/samson.abramsky>; S. Abramsky, Process Realizability, A Tutorial Workshop on Realizability Semantics and Applications, 1999. Available from <web.comlab.ox.ac.uk/oucl/work/samson.abramsky> |
| [6] | T. Altenkirch, P. Dybjer, M. Hofmann, P. Scott, Normalisation by evaluation for typed lambda calculus with coproducts, in: Proceedings of the LICS’01, IEEE, London, 2001, pp. 303-310; T. Altenkirch, P. Dybjer, M. Hofmann, P. Scott, Normalisation by evaluation for typed lambda calculus with coproducts, in: Proceedings of the LICS’01, IEEE, London, 2001, pp. 303-310 |
| [7] | Barendregt, H., The Lambda Calculus: Its Syntax and Semantics (1984), North-Holland: North-Holland Amsterdam · Zbl 0551.03007 |
| [8] | Barendregt, H., Lambda calculi with types, (Handbook of Logic in Computer Science, vol. 2 (1992), Clarendon Press: Clarendon Press Oxford), 118-120 · Zbl 0777.68001 |
| [9] | Bellin, G.; Scott, P. J., On the pi-calculus and linear logic, TCS, 135, 11-65 (1994) · Zbl 0817.03001 |
| [10] | Berger, M.; Honda, K.; Yoshida, N., Sequentiality and the \(π\)-calculus, (Proceedings of the TLCA01. Proceedings of the TLCA01, LNCS, vol. 2044 (2001), Springer: Springer Berlin), 29-45 · Zbl 0981.68037 |
| [11] | The full version of 10. Available from <www.dcs.qmw.ac.uk/ kohei>; The full version of 10. Available from <www.dcs.qmw.ac.uk/ kohei> |
| [12] | Berger, M.; Honda, K.; Yoshida, N., Genericity and the \(π\)-calculus, (Proceedings of the FoSSaCs03. Proceedings of the FoSSaCs03, LNCS, vol. 2620 (2003), Springer: Springer Berlin), 103-119 · Zbl 1029.68039 |
| [13] | Boreale, M., On expressiveness in internal mobility of name passing calculi, TCS, 195, 206-226 (1998) · Zbl 0915.68059 |
| [14] | Boreale, M.; Sangiorgi, D., Some congruence properties for \(π\)-calculus bisimilarities, TCS, 198, 159-176 (1998) · Zbl 0902.68117 |
| [15] | G. Boudol, Asynchrony and the pi-calculus, INRIA Research Report 1702, 1992; G. Boudol, Asynchrony and the pi-calculus, INRIA Research Report 1702, 1992 |
| [16] | G. Boudol, The pi-calculus in direct style, in: Proceedings of the POPL’97, ACM, New York, 1997, pp. 228-241; G. Boudol, The pi-calculus in direct style, in: Proceedings of the POPL’97, ACM, New York, 1997, pp. 228-241 |
| [17] | Boudol, G.; Castellani, I., Noninterference for concurrent programs, (Proceedings of the ICALP01. Proceedings of the ICALP01, LNCS, vol. 2076 (2001), Springer: Springer Berlin), 382-395 · Zbl 0986.68012 |
| [18] | S. Chaki, S. Rajamani, J. Rehof, Types as models: model checking message-passing programs, in: Proceedings of the POPL’02, ACM, New York, 2002; S. Chaki, S. Rajamani, J. Rehof, Types as models: model checking message-passing programs, in: Proceedings of the POPL’02, ACM, New York, 2002 · Zbl 1323.68365 |
| [19] | N. Ghani, Adjoint rewriting, Ph.D. Thesis, LFCS, University of Edinburgh, November 1995; N. Ghani, Adjoint rewriting, Ph.D. Thesis, LFCS, University of Edinburgh, November 1995 |
| [20] | Ghani, N., βη-Equality from coproducts, (Proceedings of the TLCA’95. Proceedings of the TLCA’95, LNCS, vol. 902 (1995), Springer: Springer Berlin), 171-185 · Zbl 1063.03513 |
| [21] | J.H. Gallier, On Girard’s “Candidats de Reductibilité,”, Logic and Computer Science, Academic Press, New York, 1990, pp. 123-203; J.H. Gallier, On Girard’s “Candidats de Reductibilité,”, Logic and Computer Science, Academic Press, New York, 1990, pp. 123-203 |
| [22] | Gay, S.; Hole, M., Types and subtypes for client-server interactions, (Proceedings of the ESOP’99. Proceedings of the ESOP’99, LNCS, vol. 1576 (1999), Springer: Springer Berlin), 74-90 |
| [23] | Girard, J.-Y., Linear logic, TCS, 50, 1-102 (1987) · Zbl 0625.03037 |
| [24] | J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and types, vol. 7 of Cambridge Tracts in Theoretical Computer Science, CUP, 1989; J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and types, vol. 7 of Cambridge Tracts in Theoretical Computer Science, CUP, 1989 · Zbl 0671.68002 |
| [25] | Gunter, C. A., Semantics of Programming Languages: Structures and Techniques (1992), MIT Press: MIT Press Cambridge, MA · Zbl 0823.68059 |
| [26] | M. Hicks, P. Kakkar, J.T. Moore, C.A. Gunter, S. Nettles, PLAN: a packet language for active networks, in: Proceedings of the International Conference on Functional Programming (ICFP’98), cf. 58; M. Hicks, P. Kakkar, J.T. Moore, C.A. Gunter, S. Nettles, PLAN: a packet language for active networks, in: Proceedings of the International Conference on Functional Programming (ICFP’98), cf. 58 · Zbl 1369.68075 |
| [27] | K. Honda, Types for dyadic interaction, in: Proceedings of the CONCUR’93, LNCS, vol. 715, 1993, pp. 509-523; K. Honda, Types for dyadic interaction, in: Proceedings of the CONCUR’93, LNCS, vol. 715, 1993, pp. 509-523 · Zbl 0939.68642 |
| [28] | K. Honda, Composing processes, in: Proceedings of the POPL’96, ACM, New York, 1996, pp. 344-357; K. Honda, Composing processes, in: Proceedings of the POPL’96, ACM, New York, 1996, pp. 344-357 |
| [29] | Honda, K.; Kubo, M.; Vasconcelos, V., Language primitives and type discipline for structured communication-based programming, (Proceedings of the ESOP’98. Proceedings of the ESOP’98, LNCS, vol. 1381 (1998), Springer: Springer Berlin), 122-138 |
| [30] | Honda, K.; Tokoro, M., An object calculus for asynchronous communication, (Proceedings of the ECOOP’91. Proceedings of the ECOOP’91, LNCS, vol. 512 (1991), Springer: Springer Berlin), 133-147 |
| [31] | K. Honda, V. Vasconcelos, N. Yoshida, Secure information flow as typed process behaviour, in: Proceedings of the ESOP’99, LNCS, vol. 1782, Springer, Berlin, 2000, pp. 180-199. Full version available as MCS Technical Report 01/2000, University of Leicester, 2000; K. Honda, V. Vasconcelos, N. Yoshida, Secure information flow as typed process behaviour, in: Proceedings of the ESOP’99, LNCS, vol. 1782, Springer, Berlin, 2000, pp. 180-199. Full version available as MCS Technical Report 01/2000, University of Leicester, 2000 · Zbl 0960.68126 |
| [32] | Honda, K.; Yoshida, N., On reduction-based process semantics, (TCS, 151 (1995), North-Holland: North-Holland Amsterdam), 437-486 · Zbl 0871.68122 |
| [33] | Honda, K.; Yoshida, N., Game-theoretic analysis of call-by-value computation, (TCS, 221 (1999), North-Holland: North-Holland Amsterdam), 393-456 · Zbl 0930.68061 |
| [34] | K. Honda, N. Yoshida, A uniform type structure for secure information flow, in: Proceedings of the POPL’02, ACM, New York, 2002, pp. 81-92, Full version as a DOC Technical Report, Department of Computing, Imperial College London, 2002/13, August, 2002. Revised in August, 2003. Available from <www.doc.ic.ac.uk/ yoshida>; K. Honda, N. Yoshida, A uniform type structure for secure information flow, in: Proceedings of the POPL’02, ACM, New York, 2002, pp. 81-92, Full version as a DOC Technical Report, Department of Computing, Imperial College London, 2002/13, August, 2002. Revised in August, 2003. Available from <www.doc.ic.ac.uk/ yoshida> · Zbl 1323.68375 |
| [35] | K. Honda, N. Yoshida, Noninterference through Flow Analysis, a DOC Technical Report 2002/14, Imperial College London, revised September 2003, 40 pp. Available from <www.doc.ic.ac.uk/ yoshdia>; K. Honda, N. Yoshida, Noninterference through Flow Analysis, a DOC Technical Report 2002/14, Imperial College London, revised September 2003, 40 pp. Available from <www.doc.ic.ac.uk/ yoshdia> |
| [36] | Honda, K.; Yoshida, N.; Berger, M., Control in the \(π\)-calculus, (Proceedings of the CW’04 (2004), ACM: ACM New York) |
| [37] | Huet, G., Confluent reductions: Abstract properties and applications to term rewriting systems, J. Assoc. Comput., 23, 1, 11-21 (1981) · Zbl 0465.68014 |
| [38] | Hyland, M.; Ong, L., On full abstraction for PCF: I, II and III, Inform. Comput., 163, 285-408 (2000) · Zbl 1006.68027 |
| [39] | A. Igarashi, N. Kobayashi, A generic type system for the pi-calculus, in: Proceedings of the POPL’01, ACM, New York, 2001; A. Igarashi, N. Kobayashi, A generic type system for the pi-calculus, in: Proceedings of the POPL’01, ACM, New York, 2001 · Zbl 1323.68410 |
| [40] | Klop, J. W., Term rewriting systems, (Handbook of Logic in Computer Science, vol. 2 (1992), Clarendon Press: Clarendon Press Oxford), 2-117 · Zbl 0806.68003 |
| [41] | Kobayashi, N., A partially deadlock-free typed process calculus, ACM TOPLAS, 20, 2, 436-482 (1998) |
| [42] | Kobayashi, N., Type systems for concurrent processes: from deadlock-freedom to livelock-freedom, time-boundedness, (Proceedings of the TCS2000. Proceedings of the TCS2000, LNCS, vol. 1872 (2000), Springer: Springer Berlin), 365-389 · Zbl 0998.68085 |
| [43] | Kobayashi, N.; Pierce, B.; Turner, D., Linear types and \(π\)-calculus, (Proceedings of the POPL’96 (1996), ACM: ACM New York), 358-371 |
| [44] | Laird, J., A deconstruction of non-deterministic classical cut elimination, (Proceedings of the TLCA’01. Proceedings of the TLCA’01, LNCS, vol. 2044 (2001), Springer: Springer Berlin), 268-282 · Zbl 0981.03057 |
| [45] | O. Laurent, Polarized games, in: Proceedings of the LICS 2002, IEEE, London, 2002, pp. 265-274; O. Laurent, Polarized games, in: Proceedings of the LICS 2002, IEEE, London, 2002, pp. 265-274 |
| [46] | O. Laurent, Invited lecture: polarities in linear logic, Linear Logic Workshop, 2002; O. Laurent, Invited lecture: polarities in linear logic, Linear Logic Workshop, 2002 |
| [47] | Lafont, Y., Interaction nets, (Proceedings of the POPL’90 (1990), ACM: ACM New York), 95-108 |
| [48] | Lévy, J.-J., An algebraic interpretation of the \(λ-β-K\)-calculus and a labelled \(λ\)-calculus, (Proceedings of the \(λ\)-calculus and Computer Science Theory. Proceedings of the \(λ\)-calculus and Computer Science Theory, LNCS, vol. 37 (1975), Springer: Springer Berlin), 147-165 · Zbl 0335.02015 |
| [49] | Merro, M.; Sangiorgi, D., On asynchrony in name-passing calculi, (Proceedings of the ICALP’98. Proceedings of the ICALP’98, LNCS, vol. 1443 (1998), Springer: Springer Berlin), 856-867 · Zbl 0910.03019 |
| [50] | R. Milner, A Calculus of Communicating Systems, LNCS, vol. 76, Springer, Berlin, 1980; R. Milner, A Calculus of Communicating Systems, LNCS, vol. 76, Springer, Berlin, 1980 · Zbl 0452.68027 |
| [51] | R. Milner, Functions as Processes, MSCS, vol. 2(2), CUP, 1992, pp. 119-146; R. Milner, Functions as Processes, MSCS, vol. 2(2), CUP, 1992, pp. 119-146 · Zbl 0773.03012 |
| [52] | Milner, R., Polyadic \(π\)-calculus: a tutorial, (Proceedings of the International Summer School on Logic Algebra of Specification (1992), Marktoberdorf) |
| [53] | Milner, R.; Parrow, J. G.; Walker, D. J., A calculus of mobile processes, Inform. Comput., 100, 1, 1-77 (1992) · Zbl 0752.68037 |
| [54] | Mitchell, J., Foundations for Programming Languages (1996), MIT Press: MIT Press Cambridge, MA |
| [55] | L. Ong, C. Stewart, A Curry-Howard foundation for functional computation with control, in: Proceedings of the POPL’97, ACM, New York, 1997; L. Ong, C. Stewart, A Curry-Howard foundation for functional computation with control, in: Proceedings of the POPL’97, ACM, New York, 1997 |
| [56] | Parigot, M., λμ-Calculus: an algorithmic interpretation of classical natural deduction, (Proceedings of the Logic Programming and Automated Reasoning. Proceedings of the Logic Programming and Automated Reasoning, LNCS, vol. 624 (1992), Springer: Springer Berlin), 190-201 · Zbl 0925.03092 |
| [57] | B.C. Pierce, D. Sangiorgi, Typing and subtyping for mobile processes, in: Proceedings of the LICS’93, IEEE, London, 1993, pp. 187-215; B.C. Pierce, D. Sangiorgi, Typing and subtyping for mobile processes, in: Proceedings of the LICS’93, IEEE, London, 1993, pp. 187-215 · Zbl 0861.68030 |
| [58] | PLAN: A Packet Language for Active Networks, SwitchWare Project, University of Pennsylvania. Available from <http://www.cis.upenn.edu/ switchware/>; PLAN: A Packet Language for Active Networks, SwitchWare Project, University of Pennsylvania. Available from <http://www.cis.upenn.edu/ switchware/> |
| [59] | Quaglia, P.; Walker, D., On synchronous and asynchronous mobile processes, (Proceedings of the FoSSaCS 00. Proceedings of the FoSSaCS 00, LNCS, vol. 1784 (2000), Springer: Springer Berlin), 283-296 · Zbl 0961.68092 |
| [60] | D. Sangiorgi, \(π\)-Calculus, internal mobility, and agent-passing calculi,TCS 167(2) (1996) 235-271, North-Holland, Amsterdam; D. Sangiorgi, \(π\)-Calculus, internal mobility, and agent-passing calculi,TCS 167(2) (1996) 235-271, North-Holland, Amsterdam · Zbl 0874.68103 |
| [61] | Sangiorgi, D., The name discipline of uniform receptiveness, (Proceedings of the ICALP’97. Proceedings of the ICALP’97, LNCS, vol. 1256 (1997), Springer: Springer Berlin), 303-313 · Zbl 0930.68035 |
| [62] | Sangiorgi, D., Types, or: where’s the difference between CCS and \(π\)?, (Proceedings of the CONCUR 2002. Proceedings of the CONCUR 2002, LNCS, vol. 2421 (2002), Springer: Springer Berlin), 76-97 · Zbl 1012.68137 |
| [63] | G. Smith, A new type system for secure information flow, in: Proceedings of the CSFW’01, IEEE, London, 2001; G. Smith, A new type system for secure information flow, in: Proceedings of the CSFW’01, IEEE, London, 2001 |
| [64] | G. Smith, D. Volpano, Secure information flow in a multi-threaded imperative language, in: Proceedings of the POPL’98, ACM, New York, 1998, pp. 355-364; G. Smith, D. Volpano, Secure information flow in a multi-threaded imperative language, in: Proceedings of the POPL’98, ACM, New York, 1998, pp. 355-364 |
| [65] | Tait, W., Intensional interpretation of functionals of finite type, I, J. Symb. Log, 32, 198-212 (1967) · Zbl 0174.01202 |
| [66] | Urban, C.; Bierman, G. M., Strong normalisation of cut-elimination in classical logic, Fundam. Inform., 45, 1-2, 123-155 (2001) · Zbl 0982.03032 |
| [67] | Vasconcelos, V., Typed concurrent objects, (Proceedings of the ECOOP’94. Proceedings of the ECOOP’94, LNCS, vol. 821 (1994), Springer: Springer Berlin), 100-117 |
| [68] | Vasconcelos, V.; Honda, K., Principal typing scheme for polyadic \(π\)-calculus, (Proceedings of the CONCUR’93. Proceedings of the CONCUR’93, LNCS, vol. 715 (1993), Springer: Springer Berlin), 524-538 |
| [69] | N. Yoshida, Graph types for monadic mobile processes, in: FST/TCS’16, LNCS vol. 1180, Springer, Berlin, 1996. Full version as LFCS Technical Report, ECS-LFCS-96-350, 1996, pp. 371-387; N. Yoshida, Graph types for monadic mobile processes, in: FST/TCS’16, LNCS vol. 1180, Springer, Berlin, 1996. Full version as LFCS Technical Report, ECS-LFCS-96-350, 1996, pp. 371-387 |
| [70] | N. Yoshida, Type-based liveness guarantee in the presence of nontermination and nondeterminism, April 2002. MCS Technical Report, 2002-20, University of Leicester. Available from <www.doc.ic.ac.uk/ yoshida>; N. Yoshida, Type-based liveness guarantee in the presence of nontermination and nondeterminism, April 2002. MCS Technical Report, 2002-20, University of Leicester. Available from <www.doc.ic.ac.uk/ yoshida> |
| [71] | N. Yoshida, M. Berger, K. Honda, Strong Normalisation in the \(π\)-calculus, in: Proceedings of the LICS’01, IEEE, London, 2001, pp. 311-322. The first full version as MCS Technical Report, 2001-09, University of Leicester, 2001; N. Yoshida, M. Berger, K. Honda, Strong Normalisation in the \(π\)-calculus, in: Proceedings of the LICS’01, IEEE, London, 2001, pp. 311-322. The first full version as MCS Technical Report, 2001-09, University of Leicester, 2001 |
| [72] | N. Yoshida, K. Honda, M. Berger, Linearity and bisimulation, in: Proceedings of the Fifth International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2002), LNCS 2303, pp. 417-433, Springer, Berlin, 2002. A full version as a MCS Technical Report, 2001-48, University of Leicester, 2001. Available from <www.doc.ic.ac.uk/ yoshida>; N. Yoshida, K. Honda, M. Berger, Linearity and bisimulation, in: Proceedings of the Fifth International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2002), LNCS 2303, pp. 417-433, Springer, Berlin, 2002. A full version as a MCS Technical Report, 2001-48, University of Leicester, 2001. Available from <www.doc.ic.ac.uk/ yoshida> · Zbl 1077.68719 |
| [73] | Yoshida, N., Channel dependency types for higher-order mobile processes, Proceedings of the POPL’04 (2004), ACM: ACM New York |
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.
