skip to main content
research-article

Equations, Contractions, and Unique Solutions

Published: 14 January 2015 Publication History

Abstract

One of the most studied behavioural equivalences is bisimilarity. Its success is much due to the associated bisimulation proof method, which can be further enhanced by means of "up-to bisimulation" techniques such as "up-to context".
A different proof method is discussed, based on unique solution of special forms of inequations called contractions, and inspired by Milner's theorem on unique solution of equations. The method is as powerful as the bisimulation proof method and its "up-to context" enhancements. The definition of contraction can be transferred onto other behavioural equivalences, possibly contextual and noncoinductive.
This enables a coinductive reasoning style on such equivalences, either by applying the method based on unique solution of contractions, or by injecting appropriate contraction preorders into the bisimulation game. The techniques are illustrated on CCS-like languages; an example dealing with higher-order languages is also shown.

Supplementary Material

MPG File (p421-sidebyside.mpg)

References

[1]
S. Arun-Kumar and M. Hennessy. An efficiency preorder for processes. Acta Informatica, 29:737--760, 1992.
[2]
J.C.M. Baeten, T. Basten, and M.A. Reniers. Process Algebra: Equational Theories of Communicating Processes. Cambridge University Press, 2010.
[3]
Jos C. M. Baeten, Jan A. Bergstra, and Jan Willem Klop. Readytrace semantics for concrete process algebra with the priority operator. Comput. J., 30(6):498--506, 1987.
[4]
Jos C. M. Baeten and Bas Luttik. Unguardedness mostly means many solutions. Theor. Comput. Sci., 412(28):3090--3100, 2011.
[5]
B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can't be traced. Journal of the ACM, 42(1):232--268, 1995.
[6]
F. Bonchi, D. Petrisan, D. Pous, and J. Rot. Coinduction up to in a fibrational setting. Proc. CSL-LICS'14, ACM, 2014.
[7]
Filippo Bonchi and Damien Pous. Checking nfa equivalence with bisimulations up to congruence. In Proc. POPL'13, pages 457--468. ACM, 2013.
[8]
Rance Cleaveland and Matthew Hennessy. Testing equivalence as a bisimulation equivalence. Formal Asp. Comput., 5(1):1--20, 1993.
[9]
R. De Nicola and R. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83--133, 1984.
[10]
R.J. van Glabbeek. The linear time-branching time spectrum II. In Proc. CONCUR '93, volume 715. Springer, 1993.
[11]
K. Honda and N. Yoshida. On reduction-based process semantics. Theoretical Computer Science, 152(2):437--486, 1995.
[12]
John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison- Wesley, Boston, MA, USA, 2006.
[13]
G. Hutton and M. Jaskelioff. Representing Contractive Functions on Streams. Submitted, 2011.
[14]
V. Koutavas and M. Wand. Small bisimulations for reasoning about higher-order imperative programs. In Proc. POPL'06, pages 141--152. ACM, 2006.
[15]
Michal Kunc. Simple language equations. Bulletin of the EATCS, 85:81--102, 2005.
[16]
S.B. Lassen. Relational reasoning about contexts. In Higher-order operational techniques in semantics, pages 91--135. Cambridge University Press, 1998.
[17]
S.B. Lassen. Bisimulation in untyped lambda calculus: Bohm trees and bisimulation up to context. Electr. Notes Theor. Comput. Sci., 20:346--374, 1999.
[18]
S. Milius, L. S. Moss, and D. Schwencke. Abstract GSOS rules and a modular treatment of recursive definitions. Logical Methods in Computer Science, 9(3), 2013.
[19]
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[20]
R. Milner and D. Sangiorgi. Barbed bisimulation. In Proc. 19th ICALP, volume 623 of LNCS, Springer Verlag, 1992.
[21]
Robin Milner. A complete axiomatisation for observational congruence of finite-state behaviors. Inf. Comput., 81(2):227--247, 1989.
[22]
James H. Morris. Lambda-Calculus Models of Programming Languages. Phd thesis MAC-TR-57, M.I.T., project MAC, Dec. 1968.
[23]
Ion Petre and Arto Salomaa. Algebraic systems and pushdown automata. In Handbook of Weighted Automata, EATCS Series, pages 257--289. Springer, 2009.
[24]
Adrien Piérard and Eijiro Sumii. Sound bisimulations for higherorder distributed process calculus. In Proc. FOSSACS, volume 6604 of LNCS, pages 123--137. Springer, 2011.
[25]
Andrew Pitts. Howe's method. In Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, 2012.
[26]
Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, 2012.
[27]
Alexander Moshe Rabinovich. A complete axiomatisation for trace congruence of finite state behaviors. In Proc. 9th MFPS, volume 802 of LNCS, pages 530--543. Springer, 1993.
[28]
A. W. Roscoe. The theory and practice of concurrency. Prentice Hall, 1998.
[29]
A. W. Roscoe. Understanding Concurrent Systems. Springer, 2010.
[30]
Jurriaan Rot, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Coinductive proof techniques for language equivalence. In Proc. LATA, volume 7810 of LNCS, pages 480--492. Springer, 2013.
[31]
David Sands. Computing with Contexts: A simple approach. ENTCS, volume 10, Elsevier, 1998.
[32]
Sangiorgi, D. and Milner, R. The problem of "Weak Bisimulation up to". In Proc. CONCUR '92, volume 630 of LNCS, Springer, 1992.
[33]
D. Sangiorgi. Locality and True-concurrency in Calculi for Mobile Processes. In Proc. TACS '94, volume 789 of LNCS, Springer, 1994.
[34]
D. Sangiorgi and D. Walker. The *PIE*-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001.
[35]
Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst., 33(1):5, 2011.

Cited By

View all
  • (2020)Unique solutions of contractions, CCS, and their HOL formalisationInformation and Computation10.1016/j.ic.2020.104606275(104606)Online publication date: Dec-2020
  • (2019)Bisimulation and Coinduction Enhancements: A Historical PerspectiveFormal Aspects of Computing10.1007/s00165-019-00497-w31:6(733-749)Online publication date: 1-Dec-2019
  • (2015)The Proof Technique of Unique Solutions of ContractionsProceedings of the 12th International Colloquium on Theoretical Aspects of Computing - ICTAC 2015 - Volume 939910.1007/978-3-319-25150-9_5(63-68)Online publication date: 29-Oct-2015
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 50, Issue 1
POPL '15
January 2015
682 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2775051
  • Editor:
  • Andy Gill
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
    January 2015
    716 pages
    ISBN:9781450333009
    DOI:10.1145/2676726
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

  1. bisimulation
  2. coinduction
  3. contraction
  4. equations
  5. unique solution

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)10
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2020)Unique solutions of contractions, CCS, and their HOL formalisationInformation and Computation10.1016/j.ic.2020.104606275(104606)Online publication date: Dec-2020
  • (2019)Bisimulation and Coinduction Enhancements: A Historical PerspectiveFormal Aspects of Computing10.1007/s00165-019-00497-w31:6(733-749)Online publication date: 1-Dec-2019
  • (2015)The Proof Technique of Unique Solutions of ContractionsProceedings of the 12th International Colloquium on Theoretical Aspects of Computing - ICTAC 2015 - Volume 939910.1007/978-3-319-25150-9_5(63-68)Online publication date: 29-Oct-2015
  • (2018)Unique Solutions of Contractions, CCS, and their HOL FormalisationElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.276.10276(122-139)Online publication date: 24-Aug-2018

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media