Abstract
We introduce a coinductive logical system à la Gentzen for establishing bisimulation equivalences on circular non-wellfounded regular objects, inspired by work of Coquand, and of Brandt and Henglein. In order to describe circular objects, we utilize a typed language, whose coinductive types involve disjoint sum, cartesian product, and finite powerset constructors. Our system is shown to be complete with respect to a maximal fixed point semantics. It is shown to be complete also with respect to an equivalent final semantics. In this latter semantics, terms are viewed as points of a coalgebra for a suitable endofunctor on the category Set* of non-wellfounded sets. Our system subsumes an axiomatization of regular processes, alternative to the classical one given by Milner.
Work supported by Esprit Working Group “Types”, MURST’97 Cofin. “Sistemi Formali...” grant, TMR Linear FMRX-CT98-0170.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
P. Aczel. Non-well-founded sets, CSLI Lecture Notes 14, Stanford 1988.
J. de Bakker, E. de Vink. Control Flow Semantics, Foundations of Computing Series, The MIT Press, Cambridge, 1996.
J. Barwise, L. Moss. Vicious circles: On the mathematics of non-wellfounded phenomena, CSLI Publications, Stanford, 1996.
M. Brandt, F. Henglein. Coinductive axiomatization of recursive type equality and subtyping, TLCA’97 Conf. Proc., P. de Groote, R. Hindley, eds., Springer LNCS 1210, 1997, 63–81.
T. Coquand. Infinite Objects in Type Theory, Types for Proofs and Programs TYPES-93, Springer LNCS 806, 1994, 62–78.
M. Fiore. A Coinduction Principle for Recursive Data Types Based on Bisimulation, Inf. & Comp. 127, 1996, 186–198.
M. Forti, F. Honsell. Set theory with free construction principles, Ann. Scuola Norm. Sup. Pisa, Cl. Sci. (4) 10, 1983, 493–522.
E. Giménez. Codifying guarded definitions with recursive schemes, Workshop on Types for Proofs and Programs, P. Dybjer et al. eds., Springer LNCS 996, 1994, 39–59.
E. Giménez. An application of co-Inductive types in Coq: verification of the Alternating Bit Protocol, Workshop Types Proofs and Programs, 1995.
E. Giménez. Un calcul de constructions infinies et son application a la verfication de systemes communicants, PhD Thesis, École normale supérieure de Lyon, December 1996.
F. Honsell, M. Lenisa. Final Semantics for Untyped Lambda Calculus, TLCA’95 Conf. Proc., M. Dezani et al eds., Springer LNCS 902, 1995, 249–265.
M. Lenisa. Final Semantics for a Higher Order Concurrent Language, CAAP’96, H. Kirchner et. al. eds., Springer LNCS 1059, 1996, 102–118.
M. Lenisa. Themes in Final Semantics, Ph.D. Thesis TD-6/98, Dipartimento di Informatica, Università di Pisa, March 1998.
N. P. Mendler, P. Panangaden, R. L. Constable. Infinite Objects in Type Theory, 1th LICS Conf. Proc., IEEE Computer Society Press, 1986, 249–255.
R. Milner. Calculi for synchrony and asynchrony, TCS 25, 1983, 267–310.
R. Milner. A complete inference system for a class of regular behaviours, J. of Computer and System Sciences 28, 1984, 39–466.
L. Moss. Coalgebraic Logic, to appear in the Annals of Pure and Applied Logic.
A. M. Pitts. Relational Properties of Domains, Inf. & Comp. 127, 1996.
G. Plotkin. Types and Partial Functions, Post-Graduate Lecture Notes, Department of Computer Science, University of Edinburgh, 1985.
J. J. M. M. Rutten. Universal coalgebra: a theory of systems, Report CS-R9652, CWI, Amsterdam, 1996.
J. J. M. M. Rutten, D. Turi. On the Foundations of Final Semantics: Non-Standard Sets, Metric Spaces, Partial Orders, REX Conf. Proc., J. de Bakker et al. eds., Springer LNCS 666, 1993, 477–530.
C. Talcott. A Theory for Program and Data type Specification, TCS, Disco90 Special Issue, 1990.
D. Turi. Functorial Operational Semantics and its Denotational Dual, PhD thesis, CWI, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lenisa, M. (1999). A Complete Coinductive Logical System for Bisimulation Equivalence on Circular Objects. In: Thomas, W. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 1999. Lecture Notes in Computer Science, vol 1578. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49019-1_17
Download citation
DOI: https://doi.org/10.1007/3-540-49019-1_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65719-4
Online ISBN: 978-3-540-49019-7
eBook Packages: Springer Book Archive