Bisimilarity via unique-solution techniques Davide Sangiorgi University of Bologna and INRIA 1 Introduction Bisimilarity is employed to de ne behavioural equivalences and reason about them. Finding its origins in concurrency theory, bisimilarity is now widely used also in other areas, as well as outside Computer Science. In proofs of bisimilarity results, the bisimulation proof method has become predominant, particularly with the enhancements of the method provided by the so called `up-to techniques' [13]. Among these, one of the most powerful ones is `up-to context', whereby, during the bisimulation game, a common context in the derivatives of two terms can be erased. Forms of `bisimulations up-to context' have been shown to be e ective in various elds, including process calculi [13, 18, 11], -calculi [7, 6, 5, 22], and automata [1, 16]. A lot of work has been carried out recently on 'up-to context' and other up-to techniques, as well as on trying to give a systematic treatment of the set of all such techniques (e.g., the tutorial [13]). In this paper we summarise a di erent, ongoing, strand of work about tech- niques for proving bisimilarity results. This strand is inspired by Milner's theorem about unique solution of equations in his landmark book on CCS [8]. This theorem roughly says that two tuples of processes are componentwise bisimilar if they are solutions of the same system of equations. Milner's theorem has however syntactic constraints, on the shape of the equations. For instance, the theorem heavily relies on the sum operator { any other operator but pre x and sum is essentially for- bidden. This limits the expressiveness of the technique (since occurrences of other operators above the variables, such as parallel composition and restriction, in gen- eral cannot be removed), and its transport onto other languages (e.g., languages for distributed systems or higher-order languages, which usually do not include the sum operator). An important remark has to be made before providing more technical details. In this paper, behavioural equivalences, hence also bisimilarity, are meant to be weak because they abstract from internal moves of terms, as opposed to the strong ones, which make no distinctions between the internal moves and the external ones (i.e., the interactions with the environment). Weak equivalences are, practically, the most relevant ones: e.g., two equal programs may produce the same result with di erent numbers of evaluation steps. The problems mentioned above concerning Milner's theorem do not exist in the case of strong bisimilarity. We outline two directions for improving Milner's unique-solution technique. The rst consists in replacing equations with special inequations called contrac- tions [21]. The second consists in replacing the most severe syntactic constraint in Milner's theorem with a semantic condition that has to do with divergence [3, 4]. Other motivations for the work on unique solutions are the following. First, the unique-solution techniques convey the avour of 'bisimilarity up-to context' techinques, as the equations (or contractions) intuitively bring out those contexts that would be erased in an 'up-to context' proof (indeed there are completeness results with respect to certain forms of up-to context, in CCS-like languages [21]). Thus here the goal is to bring light into the up-to-context techniques. For instance, in higher-order languages, while there are well-developed techniques for proving congruence [12], up-to context is still poorly understood [7, 6, 5, 22, 11]. Another possible interest for the unique-solution techniques is that they can be transported onto other equivalences, including contextually-de ned equivalences such as barbed congruence, and non-coinductive equivalences such as contextual equivalence (i.e., may testing) and trace equivalence. 2 Equations and Milner's theorem We recall equations and Milner's theorem, in the setting of CCS. We omit the standard de nitions of syntax and operational semantics of the calculus, as well of weak bisimulation, written , [8]. Uniqueness of solutions of equations [8] intuitively says that if a context C obeys certain conditions, then all processes P that satisfy the equation P  C[P ] are bisimilar with each other. We use capital letters X; Y; Z for variable of equations. The body of an equation is a CCS expression possibly containing variables. De nition 1. Given, for each i of a countable indexing set I , variables Xi , and expressions Ei possibly containing such variables, fXi = Ei gi2I is a system of equations. (There is one equation for each variable Xi .) We write E[Pe] for the expression resulting from E by replacing each variable Xi with the process Pi De nition 2. Suppose fXi = Ei gi2I is a system of equations: { Pe is a solution of the system of equations for  if for each i it holds that Pi  Ei [Pe]. { the system has a unique solution for  if whenever Pe and Qe are both solutions for , then Pe  Q e. De nition 3. A system of equations fXi = Ei gi2I is { guarded if, in each Ei , each occurrence of an equation variable is underneath a visible pre x (i.e., a pre x that is not  ); { sequential if, in each Ei , each occurrence of an equation variable only appears underneath pre xes and sums. In other words, if the system is sequential, then for every expression Ei , any subexpression of Ei in which Xj appears, apart from Xj itself, is a sum (of pre xed terms). For instance, X = . X + . 0 is sequential but not guarded; using ` for a visible pre x, X = `. X j P is guarded but not sequential, whereas X = `. X + .  a (a. b j a. 0), as well as X = . (a. X + . b. X + ) are both guarded and sequential. Theorem 1 (unique solution of equations, [8]). A system of guarded and sequential equations has a unique solution for .  3 Contractions Intuitively, for a behavioural equivalence , its contraction  is a preorder in which P  Q holds if P  Q and, in addition, Q has the possibility of being at least as ecient as P . That is, if P can do some work (i.e., some interactions with its environment), then Q should be able to do the same work at least as quickly as P (i.e., performing no more -steps then those performed by P ). Process Q, however, may be nondeterministic and may have other ways of doing the same work, and these could be slow (i.e., involving more -steps than those performed by P ). The bisimilarity contraction is written bis and is a precongruence in CCS; see [20, 21] for the formal de nition. A system of contractions is de ned as a system of equations, except that the contraction symbol  is used in the place of the equality symbol =. Thus a system of contractions is a set fXi  Ei gi2I where I is an indexing set and expressions Ei may contain the contraction variables fXi gi2I . De nition 4. Given a behavioural equivalence  and its contraction  , and a system of contractions fXi  Ei gi2I , we say that: { Pe is a solution for  of the system of contractions if Pe  E[ e Pe]; { the system has a unique solution for  if whenever P and Q are both solutions e e for  then Pe  Q e. When we reason about bisimilarity, the contraction symbol  is interpreted as the bisimilarity contraction bis , and the equivalence  as the bisimilarity . Thus Pe being a solution for bis of the system of contractions fXi  Ei gi2I means that Pe bis E[ e Pe]; and the system having a unique solution for  means that whenever P and Q are both solutions for bis then Pe  Q. e e e Lemma 1. If a system of equations fXi = Ei gi2I has a unique solution for , then also the corresponding system of contractions fXi  Ei gi2I has a unique solution for . The converse of the lemma, in contrast, is false: systems of contractions more easily have a unique solution. De nition 5. A system of contractions fXi  Ei gi2I is weakly guarded if, in each Ei , each occurrence of a contraction variable is underneath a pre x. Theorem 2 (unique solution of contractions for ). A system of weakly- guarded contractions has a unique solution for . We refer to [20, 21] for discussions on completeness (the method is complete, in the sense that any process bisimilarity can be proved with the method), examples of application, abstract formulation of the method, and generalisation to other languages and to other equivalences, including non-coinductive equivalences. 4 Divergence in equations In this section we highlight a di erent approach, whereby one goes back to equa- tions, but adds a condition based in divergence. In its basic form, the method (in- spired by results by Roscoe in CSP [15, 14] essentially says that a guarded equation (or system of equations) whose in nite unfolding never produces a divergence has the unique-solution property. We discuss the approach in CCS, as before, and assuming for simplicity a single equation X = E (the results can be generalised to systems of equations). We need to reason with the unfoldings of the given equation X = E: we de ne the n-th unfolding of E to be E n ; thus E 1 is de ned as E, E 2 as E[E], and E n+1 as E n [E]. The in nite unfolding represents the simplest and most intuitive solution to the equation. In the CCS grammar, such a solution is obtained by turning the 4 equation into a recursive de nition, namely the process KE with KE = E[KE ]. Process KE is the syntactic solution of the equation. Theorem 3 (Unique solution). A guarded system of equations whose syntactic solutions do not diverge has a unique solution for . The theorem can be strengthened by distinguishing between di erent forms of divergence; in particular, ignoring divergences that already show up in partial unfoldings of the equations, i.e., E n for some n  0, called innocuous divergences. We refer to [3] for abstract formulations of the method, application to other languages, equivalences, as well as preorders. In [4] the method is applied to show- ing what is the equivalence induced on -terms by Milner's encoding into the -calculus (for call-by-value), a problem that had remained open since Milner's work on functions as processes [10, 9]. Such proofs seem hard to carry out with the ordinary bisimulation proof method, even when enhanced by means of `up-to techniques'. 4.1 Comparison In comparison with the method based on contractions, the main drawback for the method based on equations is the presence of a semantic condition, involving divergence: the unfoldings of the equations should not produce divergences, or only produce innocuous divergences. Various techniques for checking divergence exist in the literature, including type-based techniques [23, 19, 2]; a syntactic condition is proposed in [3]. However, in general divergence is undecidable, and therefore, the check may sometimes be unfeasible. Nevertheless, the equations that one writes for proofs usually involve forms of `normalised' processes, and as such they are divergence free (or at most, contain only innocuous divergences). More experiments are needed to validate this claim or to understand how limiting this problem is. On the other hand, using contractions for proving an equivalence, one needs also the theory of the associated contraction preorder; moreover there may be processes for which the contraction technique is not applicable simply because the contraction preorder is strictly ner than the equivalence, and therefore one of the processes fails to be a solution. References 1. Bonchi, F., Pous, D.: Checking nfa equivalence with bisimulations up to congruence. In: Giacobazzi, R., Cousot, R. (eds.) Proc. POPL'13. pp. 457{468. ACM (2013) 2. Demangeon, R., Hirschko , D., Sangiorgi, D.: Termination in impure concurrent languages. In: Proc. 21th CONCUR. LNCS 6269, pp. 328{342. Springer (2010) 3. Durier, A., Hirschko , D., Sangiorgi, D.: Divergence and unique solution of equa- tions. In: 28th CONCUR. LIPIcs, vol. 85, pp. 11:1{11:16. Schloss Dagstuhl - Leibniz- Zentrum fuer Informatik (2017) 4. Durier, A., Hirschko , D., Sangiorgi, D.: Eager functions as processes. In: 33nd An- nual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. IEEE Com- puter Society (2018) 5. Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order im- perative programs. In: Proc. 33rd POPL. pp. 141{152 (2006) 6. Lassen, S.: Relational reasoning about contexts. In: Higher-order operational tech- niques in semantics. pp. 91{135. Cambridge University Press (1998) 7. Lassen, S.: Bisimulation in untyped lambda calculus: Bohm trees and bisimulation up to context. Electr. Notes Theor. Comput. Sci. 20, 346{374 (1999) 8. Milner, R.: Communication and Concurrency. Prentice Hall (1989) 9. Milner, R.: Functions as processes. Journal of Mathematical Structures in Computer Science 2(2), 119{141 (1992) 10. Milner, R.: Functions as processes. In: ICALP. LNCS 443, pp. 167{180. Springer (1990) 11. Pierard, A., Sumii, E.: Sound bisimulations for higher-order distributed process cal- culus. In: Proc. FOSSACS. LNCS 6604, pp. 123{137. Springer (2011) 12. Pitts, A.: Howe's method. In: Sangiorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction. Cambridge University Press (2012) 13. Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method. In: San- giorgi, D., Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction. Cam- bridge University Press (2012) 14. Roscoe, A.W.: An alternative order for the failures model. J. Log. Comput. 2(5), 557{577 (1992) 15. Roscoe, A.W.: The theory and practice of concurrency. Prentice Hall (1998). 16. Rot, J., Bonsangue, M.M., Rutten, J.J.M.M.: Coinductive proof techniques for lan- guage equivalence. In: Proc. LATA. LNCS 7810, pp. 480{492. Springer (2013) 17. Sangiorgi, D., Milner, R.: The problem of \Weak Bisimulation up to". In: Proc. CONCUR '92. LNCS 630, pp. 32{46. Springer Verlag (1992) 18. Sangiorgi, D., Walker, D.: The -calculus: a Theory of Mobile Processes. Cambridge University Press (2001) 19. Sangiorgi, D.: Termination of processes. Mathematical Structures in Computer Sci- ence 16(1), 1{39 (2006) 20. Sangiorgi, D.: Equations, contractions, and unique solutions. In: POPL 2015. pp. 421{432. ACM (2015), 21. Sangiorgi, D.: Equations, contractions, and unique solutions. ACM Trans. Comput. Log. 18(1), 4:1{4:30 (2017), 22. Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. 33(1), 5 (2011) 23. Yoshida, N., Berger, M., Honda, K.: Strong Normalisation in the Pi-Calculus. Infor- mation and Computation 191(2), 145{202 (2004)