Document Open Access Logo

Precongruences and Parametrized Coinduction for Logics for Behavioral Equivalence

Authors David Sprunger, Lawrence S. Moss

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2017.23.pdf
  • Filesize: 0.5 MB
  • 15 pages

Document Identifiers

Author Details

David Sprunger
Lawrence S. Moss

Cite As Get BibTex

David Sprunger and Lawrence S. Moss. Precongruences and Parametrized Coinduction for Logics for Behavioral Equivalence. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CALCO.2017.23

Abstract

We present a new proof system for equality of terms which present elements of the final coalgebra of a finitary set functor. This is most important when the functor is finitary, and we improve on logical systems which have already been proposed in several papers. Our contributions here are (1) a new logical rule which makes for proofs which are somewhat easier to find, and (2) a soundness/completeness theorem which works for all finitary functors, in particular removing a weak pullback preservation requirement that had been used previously. Our work is based on properties of precongruence relations and also on a new parametrized coinduction principle.

Subject Classification

Keywords
  • precongruence
  • kernel bisimulation
  • finitary functor
  • coalgebra
  • behavioural equivalence

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Peter Aczel and Nax Mendler. A final coalgebra theorem. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science: Manchester, UK, September 5-8, 1989 Proceedings, pages 357-365. Springer Berlin Heidelberg, Berlin, Heidelberg, 1989. Google Scholar
  2. Jirí Adámek, H Peter Gumm, and Vera Trnková. Presentation of set functors: a coalgebraic perspective. Journal of Logic and Computation, 20(5):991-1015, 2010. Google Scholar
  3. Jiří Adámek and Stefan Milius. Terminal coalgebras and free iterative theories. Information and Computation, 204(7):1139 - 1172, 2006. Google Scholar
  4. Jiří Adámek, Stefan Milius, and Lawrence S Moss. On finitary functors and their presentations. In Coalgebraic Methods in Computer Science, pages 51-70. Springer, 2012. Google Scholar
  5. Jiří Adámek and Hans-Eberhardt Porst. On tree coalgebras and coalgebra presentations. Theoret. Comput. Sci., 311:257-283, 2004. Google Scholar
  6. Adriana Balan and Alexander Kurz. Finitary functors: From set to preord and poset. In Algebra and Coalgebra in Computer Science, volume 6859 of LNCS, pages 85-99. Springer, 2011. Google Scholar
  7. Marcello Bonsangue, Jan Rutten, and Alexandra Silva. An algebra for Kripke polynomial coalgebras. In Logic In Computer Science, 2009. LICS'09. 24th Annual IEEE Symposium on, pages 49-58. IEEE, 2009. Google Scholar
  8. Marcello Bonsangue, Jan Rutten, and Alexandra Silva. A Kleene theorem for polynomial coalgebras. In Foundations of Software Science and Computational Structures, pages 122-136. Springer, 2009. Google Scholar
  9. H Peter Gumm and Tobias Schröder. Coalgebras of bounded type. Mathematical Structures in Computer Science, 12(05):565-578, 2002. Google Scholar
  10. Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The power of parameterization in coinductive proof. ACM SIGPLAN Notices, 48(1):193-206, 2013. Google Scholar
  11. Antonius J. C. Hurkens, Monica McArthur, Yiannis N. Moschovakis, Lawrence S. Moss, and Glen T. Whitney. The logic of recursive equations. The Journal of Symbolic Logic, 63(02):451-478, 1998. Google Scholar
  12. Alexander Kurz. Logics for Coalgebras and Applications to Computer Science. PhD thesis, Ludwig-Maximilians-Universität München, 2000. Google Scholar
  13. Stefan Milius. A sound and complete calculus for finite stream circuits. In Logic in Computer Science (LICS), 2010 25th Annual IEEE Symposium on, pages 421-430. IEEE, 2010. Google Scholar
  14. Lawrence S Moss. Recursion and corecursion have the same equational logic. Theoretical Computer Science, 294(1):233-267, 2003. Google Scholar
  15. Lawrence S Moss, Erik Wennstrom, and Glen T Whitney. A complete logical system for the equality of recursive terms for sets. In Logic and Program Semantics, pages 180-203. Springer, 2012. Google Scholar
  16. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3-80, 2000. Google Scholar
  17. David Sprunger. A complete logic for behavioural equivalence in coalgebras of finitary set functors. In International Workshop on Coalgebraic Methods in Computer Science, pages 156-173. Springer, 2016. Google Scholar
  18. Sam Staton. Relating coalgebraic notions of bisimulation. Logical Methods in Computer Science, 7(1), 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact