On the origins of bisimulation and coinduction

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

On the origins of bisimulation and coinduction

Full text

Pdf (285 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 31 , Issue 4 (May 2009) table of contents

Article No. 15

Year of Publication: 2009

ISSN:0164-0925

Author

Davide Sangiorgi

University of Bologna, Bologna, Italy

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 41, Downloads (12 Months): 208, Citation Count: 1

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1516507.1516510 What is a DOI?

ABSTRACT

The origins of bisimulation and bisimilarity are examined, in the three fields where they have been independently discovered: Computer Science, Philosophical Logic (precisely, Modal Logic), Set Theory.

Bisimulation and bisimilarity are coinductive notions, and as such are intimately related to fixed points, in particular greatest fixed points. Therefore also the appearance of coinduction and fixed points is discussed, though in this case only within Computer Science. The paper ends with some historical remarks on the main fixed-point theorems (such as Knaster-Tarski) that underpin the fixed-point theory presented.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Luca Aceto , Anna Ingólfsdóttir , Kim Guldstrand Larsen , Jiri Srba, Reactive Systems: Modelling, Specification and Verification, Cambridge University Press, New York, NY, 2007
	2	Aczel, P. 1988. Non-Well-Founded Sets. CSLI lecture notes, no. 14.
	3	Peter Aczel, Final Universes of Processes, Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, p.1-28, April 07-10, 1993
	4	Carme Álvarez , José L. Balcázar , Joaquim Gabarró , Miklós Sántha, Parallel complexity in the design and analysis of concurrent systems, Proceedings on Parallel architectures and languages Europe : volume I: parallel architectures and algorithms: volume I: parallel architectures and algorithms, p.288-303, June 1991, Eindhoven, The Netherlands
	5	Roberto M. Amadio , Luca Cardelli, Subtyping recursive types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.4, p.575-631, Sept. 1993 [doi>10.1145/155183.155231]
	6	Arden, D. N. 1960. Delayed logic and finite state machines. In Theory of Computing Machine Design. University of Michigan Press, 1--35.
	7	Bakker, J. W. D. 1971. Recursive Procedures. Mathematical Centre Tracts 24, Mathematisch Centrum, Amsterdam.
	8	Bakker, J. W. D. 1975. The fixed-point approach in semantics: Theory and applications. In Foundations of Computer Science, J. de Bakker, Ed. Mathematical Centre Tracts 63, Mathematisch Centrum, Amsterdam, 3--53.
	9	Bakker, J. W. D. and Roever, W. P. D. 1973. A calculus for recursive program schemes. In Proceedings of the IRIA Symposium on on Automata, Languages and Programming 1972, M. Nivat, Ed. North-Holland, 167--196.
	10	Balcázar, J. L., Gabarró, J., and Santha, M. 1992. Deciding bisimilarity is P-complete. Formal Asp. Comput. 4, 6A, 638--648.
	11	Jon Barwise , John Etchemendy, The liar; an essay in truth and circularity, Oxford University Press, Inc., New York, NY, 1987
	12	Barwise, J., Gandy, R. O., and Moschovakis, Y. N. 1971. The next admissible set. J. Symb. Log. 36, 108--120.
	13	Jon Barwise , Lawrence Moss, Vicious circles: on the mathematics of non-wellfounded phenomena, Center for the Study of Language and Information, Stanford, CA, 1996
	14	Bekič, H. 1969. Definable operations in general algebras and the theory of automata and flowcharts. Unpublished manuscript, IBM Lab. Vienna 1969. Also appeared in Jones {1984}.
	15	Benthem, J. V. 1976. Modal correspondence theory. Ph.D. thesis, Mathematish Instituut and Instituut voor Grondslagenonderzoek, University of Amsterdam.
	16	Benthem, J. V. 1983. Modal Logic and Classical Logic. Bibliopolis.
	17	Benthem, J. V. 1984. Correspondence theory. In Handbook of Philosophical Logic, D. Gabbay and F. Guenthner, Eds. Vol. 2. Reidel, 167--247.
	18	Bernays, P. 1954. A system of axiomatic set theory--Part VII. J. Symb. Log. 19, 2, 81--96.
	19	Birkhoff, G. 1948. Lattice Theory (revised edition). Vol. 25 of American Mathematical Society Colloquium Publications. American Mathematical Society.
	20	Patrick Blackburn , Maarten de Rijke , Yde Venema, Modal logic, Cambridge University Press, New York, NY, 2001
	21	Blikle, A. 1977. A comparative review of some program verification methods. In 6th Symposium on Mathematical Foundations of Computer Science (MFCS'77), J. Gruska, Ed. Lecture Notes in Computer Science, vol. 53. Springer, 17--33.
	22	Boffa, M. 1968. Les ensembles extraordinaires. Bull. Société Math. Belgique XX, 3--15.
	23	Boffa, M. 1969. Sur la théorie des ensembles sans axiome de fondement. Bull. Société Math. Belgique XXXI, 16--56.
	24	Boffa, M. 1972. Forcing et negation de l'axiome de fondement. Académie Royale de Belgique, Mémoires de la classe des sciences, 2e série XL, 7, 1--53.
	25	Bourbaki, N. 1950. Sur le théorème de Zorn. Arch. Math.. 2, 434--437.
	26	Brand, D. June 1978. Algebraic simulation between parallel programs. Res. rep. RC 7206, Yorktown Heights, New Yok, 39 pp.
	27	Michael Brandt , Fritz Henglein, Coinductive Axiomatization of Recursive Type Equality and Subtyping, Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, p.63-81, April 02-04, 1997
	28	Burge, W. H. 1975. Stream processing functions. IBM J. Res. Development 19, 1, 12--25.
	29	Jean-Marie Cadiou, Recursive definitions of partial functions and their computations, Stanford University, Stanford, CA, 1972
	30	Edmund Melson Clarke, Jr., Completeness and incompleteness theorems for hoare-like axiom systems., Cornell University, Ithaca, NY, 1976
	31	Thierry Coquand, Infinite objects in type theory, Proceedings of the international workshop on Types for proofs and programs, p.62-78, January 1994, Nijmegen, The Netherlands
	32	Cousot, P. and Cousot, R. 1979. Constructive versions of Tarski's fixed point theorems. Pacific J. Math. 81, 1, 43--57.
	33	Willem P. de Roever, On Backtracking and Greatest Fixpoints, Proceedings of the Fourth Colloquium on Automata, Languages and Programming, p.412-429, July 18-22, 1977
	34	Devidé, V. 1963. On monotonous mappings of complete lattices. Fundam. Math. LIII, 147--154.
	35	Ehrenfeucht, A. 1961. An application of games to the completeness problem for formalized theories. Fundam. Math. 49, 129--141.
	36	Finsler, P. 1926. Über die Grundlagen der Mengenlehre. I. Math. Zeitschrift 25, 683--713.
	37	Floyd, R. W. 1967. Assigning meaning to programs. In Proceedings of the Symposia in Applied Mathematics. Vol. 19. American Mathematical Society, 19--32.
	38	Forti, M. and Honsell, F. 1983. Set theory with free construction principles. Annali Scuola Normale Superiore, Pisa, Serie IV X, 3, 493--522.
	39	Fraenkel, A. 1922. Zu den Grundlagen der Cantor-Zermeloschen Mengenlehre. Math. Annalen 86, 230--237.
	40	Fraïssé, R. 1953. Sur quelques classifications des syst&mgrave;es de relations. Ph.D. thesis, University of Paris. Also in Publications Scientifiques de l'Universite d'Alger, series A 1, 35--182, 1954.
	41	Friedman, H. 1973. The consistency of classical set theory relative to a set theory with intuitionistic logic. J. Symb. Log. 38, 315--319.
	42	Giarratana, V. Gimona, F. and Montanari, U. 1976. Observability concepts in abstract data type specification. In 5th Symposium on Mathematical Foundations of Computer Science, A. Mazurkievicz, Ed. Lecture Notes in Computer Science, vol. 45. Springer, 576--587.
	43	Giménez, E. 1996. Un calcul de constructions infinies et son application a la verification des systemes communicants. Ph.D. thesis, Laboratoire de l'Informatique du Parallélisme, Ecole Normale Supérieure de Lyon.
	44	Seymour Ginsburg , H. Gordon Rice, Two Families of Languages Related to ALGOL, Journal of the ACM (JACM), v.9 n.3, p.350-371, July 1962 [doi>10.1145/321127.321132]
	45	Ginzburg, A. 1968. Algebraic Theory of Automata. Academic Press.
	46	Rob J. van Glabbeek, The Linear Time-Branching Time Spectrum (Extended Abstract), Proceedings of the Theories of Concurrency: Unification and Extension, p.278-297, August 27-30, 1990
	47	Rob J. van Glabbeek, The Linear Time - Branching Time Spectrum II, Proceedings of the 4th International Conference on Concurrency Theory, p.66-81, August 23-26, 1993
	48	Goldblatt, R. 1989. Varieties of complex algebras. Ann. Pure Applied Logic 44, 173--242.
	49	Gordeev, L. 1982. Constructive models for set theory with extensionality. In The L.E.J. Brouwer Centenary Symposium, A. Troelstra and D. van Dalen, Eds. 123--147.
	50	John S. Gourlay , William C. Rounds , Richard Statman, On Properties Preserved by Contraction of Concurrent Systems, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.51-65, July 02-04, 1979
	51	Heijenoort (Ed.), J. V. 1967. From Frege to Gödel: A Source Book in Mathematical Logic 1879-1931. Harvard University Press.
	52	Matthew Hennessy , Robin Milner, On Observing Nondeterminism and Concurrency, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.299-309, July 14-18, 1980
	53	Matthew Hennessy , Robin Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM (JACM), v.32 n.1, p.137-161, Jan. 1985 [doi>10.1145/2455.2460]
	54	Hinnion, R. 1980. Contraction de structures et application à NFU. Comptes Rendus Acad. des Sciences de Paris 290, Sér. A, 677--680.
	55	Hinnion, R. 1981. Extensional quotients of structures and applications to the study of the axiom of extensionality. Bull. Société Math. Belgique XXXIII (Fas. II, Sér. B), 173--206.
	56	Hinnion, R. 1986. Extensionality in Zermelo-Fraenkel set theory. Zeitschr. Math. Logik und Grundlagen Math. 32, 51--60.
	57	Hitchcock, P. and Park, D. 1973. Induction rules and termination proofs. In Proceedings of the IRIA symposium on on Automata, Languages and Programming 1972, M. Nivat, Ed. North-Holland, 225--251.
	58	Hoare, T. 1972. Proof of correctness of data representations. Acta Inf. 1, 271--281.
	59	Honsell, F. 1981. Modelli della teoria degli insiemi, principi di regolarità e di libera costruzione. Tesi di Laurea, Universita' di Pisa.
	60	Huffman, D. 1954. The synthesis of sequential switching circuits. J. Franklin Institute 257, 3--4, 161--190 and 275--303.
	61	Immerman, N. 1982. Upper and lower bounds for first order expressibility. J. Comput. Syst. Sci. 25, 1, 76--98.
	62	Jacobs, B. and Rutten, J. 1996. A tutorial on (co)algebras and (co)induction. Bull. EATCS 62, 222--259.
	63	Kurt Jensen, A Method to Compare the Descriptive Power of Different Types of Petri Nets, Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, p.348-361, September 01-05, 1980
	64	Jones, C. B., Ed. 1984. Programming Languages and Their Definition -- Hans Bekic (1936-1982). Lecture Notes in Computer Science, vol. 177. Springer.
	65	Jongh, D. D. and Troelstra, A. 1966. On the connection of partially ordered sets with some pseudo-boolean algebras. Indagationes Math. 28, 317--329.
	66	Kahn, G. 1974. The semantics of simple language for parallel programming. In IFIP Congress. North-Holland, 471--475.
	67	Paris C. Kanellakis , Scott A. Smolka, CCS expressions finite state processes, and three problems of equivalence, Information and Computation, v.86 n.1, p.43-68, May 1990 [doi>10.1016/0890-5401(90)90025-D]
	68	Kantorovich, L. V. 1939. The method of successive approximations for functional equations. Acta Math. 71, 63--97.
	69	Kleene, S. C. 1952. Introduction to Metamathematics. Van Nostrand.
	70	Stephen C. Kleene, Origins of recursive function theory, Proceedings of the 20th Annual Symposium on Foundations of Computer Science, p.371-382, October 29-31, 1979
	71	Knaster, B. 1928. Un théorèm sur les fonctions d'ensembles. Annals Soc. Pol. Math 6, 133--134.
	72	Kwong, Y. S. 1977. On reduction of asynchronous systems. Theor. Comput. Sci. 5, 1, 25--50.
	73	Landin, P. 1969. A program-machine symmetric automata theory. Mach. Intell. 5, 99--120.
	74	Landin, P. J. 1964. The mechanical evaluation of expressions. The Comput. J. 6, 4, 308--320.
	75	P. J. Landin, Correspondence between ALGOL 60 and Church's Lambda-notation: part I, Communications of the ACM, v.8 n.2, p.89-101, Feb. 1965 [doi>10.1145/363744.363749]
	76	P. J. Landin, A correspondence between ALGOL 60 and Church's Lambda-notations: Part II, Communications of the ACM, v.8 n.3, p.158-167, March 1965 [doi>10.1145/363791.363804]
	77	Lassez, J.-L., Nguyen, V. L., and Sonenberg, L. 1982. Fixed point theorems and semantics: A folk tale. Inf. Process. Lett. 14, 3, 112--116.
	78	Manna, Z. 1969. The correctness of programs. J. Comput. Syst. Sci. 3, 2, 119--127.
	79	Zohar Manna, Introduction to Mathematical Theory of Computation, McGraw-Hill, Inc., New York, NY, 1974
	80	Mazurkiewicz, A. 1973. Proving properties of processes. Tech. rep. 134, Computation Center ol Polish Academy of Sciences, Warsaw. Also in Algorytmy 11, 5--22, 1974.
	81	Mazurkiewicz, A. W. 1971. Proving algorithms by tail functions. Inf. Control 18, 3, 220--226.
	82	McCarthy, J. 1961. A basis for a mathematical theory of computation. In Proceedings of the Western Joint Computer Conference, Vol. 19. Spartan Books, 225--238. Reprinted, with corrections and an added tenth section, in Computer Programming and Formal Systems, P. Braffort and D. Hirschberg, eds., North-Holland, 1963, pp. 33--70.
	83	McCarthy, J. 1963. Towards a mathematical science of computation. In Proceedings of the IFIP Congress 62. North-Holland, 21--28.
	84	A. R. Meyer , L. J. Stockmeyer, The equivalence problem for regular expressions with squaring requires exponential space, Proceedings of the 13th Annual Symposium on Switching and Automata Theory (swat 1972), p.125-129, October 25-27, 1972 [doi>10.1109/SWAT.1972.29]
	85	Milner, R. 1970. A formal notion of simulation between programs. Memo 14, Computers and Logic Resarch Group, University College of Swansea, U.K.
	86	Milner, R. 1971b. Program simulation: An extended formal notion. Memo 17, Computers and Logic Resarch Group, University College of Swansea, U.K.
	87	R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	88	R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
	89	Milner, R. London, 1971a. An algebraic definition of simulation between programs. In Proceedings of the 2nd International Joint Conferences on Artificial Intelligence. British Computer Society.
	90	Milner, R. and Tofte, M. 1991. Co-Induction in relational semantics. Theor. Comput. Sci. 87, 209--220. Also Tech. rep. ECS-LFCS-88-65, University of Edinburgh, 1988.
	91	Mirimanoff, D. 1917a. Les antinomies de Russell et de Burali-Forti et le problème fondamental de la théorie des ensembles. L'Enseignement Math. 19, 37--52.
	92	Mirimanoff, D. 1917b. Remarques sur la théorie des ensembles et les antinomies cantoriennes I. L'Enseignement Math. 19, 209--217.
	93	Mirimanoff, D. 1920. Remarques sur la théorie des ensembles et les antinomies cantoriennes II. L'Enseignement Math. 21, 29--52.
	94	Moore, E. 1956. Gedanken experiments on sequential machines. Automata Studies, Ann. Math. Series 34, 129--153.
	95	Morris, J. H. Dec. 1968. Lambda-Calculus models of programming languages. Ph.D. thesis, M.I.T., project MAC.
	96	Yiannis N Moschovakis, Elementary induction on abstract structures (Studies in logic and the foundations of mathematics), American Elsevier Pub. Co, 1974
	97	Nerode, A. 1958. Linear automaton transformations. In Proceedings of the American Mathematical Society. Vol. 9. 541--544.
	98	Robert Paige , Robert E. Tarjan, Three partition refinement algorithms, SIAM Journal on Computing, v.16 n.6, p.973-989, December 1, 1987 [doi>10.1137/0216062]
	99	Park, D. 1969. Fixpoint induction and proofs of program properties. In Machine Intelligence 5, B. Meltzer and D. Michie, Eds. Edinburgh University Press, 59--78.
	100	D. M.R. Park, The Y-combinator in Scott''s Lambda-calculus Models, University of Warwick, Coventry, UK, 1976
	101	David Park, On the Semantics of Fair Parallelism, Proceedings of the Abstract Software Specifications, 1979 Copenhagen Winter School, p.504-526, January 22-February 02, 1979
	102	David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the 5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981
	103	Park, D. 1981b. A new equivalence notion for communicating systems. In Bull. EATCS, G. Maurer, Ed. Vol. 14. 78--80. Abstract of the talk presented at the 2nd Workshop on the Semantics of Programming Languages. Abstracts collected in the Bulletin by B. Mayoh.
	104	Pasini, A. 1974. Some fixed point theorems of the mappings of partially ordered sets. Rendiconti del Seminario Matematico della Università di Padova 51, 167--177.
	105	Pous, D. 2007. Complete lattices and up-to techniques. In 5th Asian Symposium on Programming Languages and Systems (APLAS). Lecture Notes in Computer Science, vol. 4807. Springer, 351--366.
	106	John C. Reynolds, The discoveries of continuations, Lisp and Symbolic Computation, v.6 n.3-4, p.233-248, Nov. 1993 [doi>10.1007/BF01019459]
	107	Hartley Rogers, Jr., Theory of recursive functions and effective computability, MIT Press, Cambridge, MA, 1987
	108	Russell, B. 1903. Principles of Mathematics. Cambridge University Press.
	109	Russell, B. 1908. Mathematical logic as based on the theory of types. Amer. J. Math. 30, 222--262.
	110	Russell, B. and Whitehead, A. N. 1910, 1912, 1913. Principia Mathematica, 3 vols. Cambridge University Press.
	111	Jan J. M. M. Rutten , Daniele Turi, On the Foundation of Final Semantics: Non-Standard Sets, Metric Spaces, Partial Orders, Proceedings of the REX Workshop on Sematics: Foundations and Applications, p.477-530, June 01-04, 1992
	112	Davide Sangiorgi, On the bisimulation proof method, Mathematical Structures in Computer Science, v.8 n.5, p.447-479, October 1998 [doi>10.1017/S0960129598002527]
	113	Davide Sangiorgi , Naoki Kobayashi , Eijiro Sumii, Environmental Bisimulations for Higher-Order Languages, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.293-302, July 10-14, 2007 [doi>10.1109/LICS.2007.17]
	114	Davide Sangiorgi , David Walker, PI-Calculus: A Theory of Mobile Processes, Cambridge University Press, New York, NY, 2001
	115	Scott, D. 1960. A different kind of model for set theory. Unpublished paper, given at the 1960 Stanford Congress of Logic, Methodology and Philosophy of Science.
	116	Scott, D. 1972a. Continuous lattices. In Toposes, Algebraic Geometry and Logic, E. Lawvere, Ed. Lecture Notes in Mathematics, vol. 274. Springer, 97--136.
	117	Scott, D. 1972b. The lattice of flow diagrams. In Symposium of Semantics of Algorithmic Languages, E. Engeler, Ed. Lecture Notes in Mathematics, vol. 188. Springer, 311--366.
	118	Scott, D. 1976. Data types as lattices. SIAM J. Comput. 5, 522--587.
	119	Scott, D. December 1969b. Models for the λ-calculus. Manuscript, raft, Oxford.
	120	Scott, D. November 1969a. A construction of a model for the λ-calculus. Manuscript, Oxford.
	121	Scott, D. October 1969c. A type-theoretical alternative to CUCH, ISWIM, OWHY. Typed script, Oxford. Also appeared as Scott {1993}.
	122	Scott, D. and de Bakker, J. 1969. A theory of programs. Handwritten notes. IBM Lab., Vienna, Austria.
	123	Dana S. Scott, A type-theoretical alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science, v.121 n.1-2, p.411-440, Dec. 6, 1993 [doi>10.1016/0304-3975(93)90095-B]
	124	Segerberg, K. 1968. Decidability of S4.1. Theoria 34, 7--20.
	125	Segerberg, K. 1970. Modal logics with linear alternative relations. Theoria 36, 301--322.
	126	Segerberg, K. 1971. An essay in classical modal logic. Filosofiska Studier, Uppsala.
	127	Skolem, T. 1923. Einige Bemerkungen zur Axiomatischen Begründung der Mengenlehre. In Proceedings of the 5th Scandinavian Mathematics Congress, 1922. Akademiska Bokhandeln, Helsinki, 217--232. English translation, “Some remarks on axiomatized set theory”, in Heijenoort (Ed.) {1967}, pages 290--301.
	128	Specker, E. 1957. Zur axiomatik der Mengenlehre. Z. Math. Logik 3, 3, 173--210.
	129	Tarski, A. 1949. A fixpoint theorem for lattices and its applications (preliminary report). Bull. Amer. Math. Soc. 55, 1051--1052 and 1192.
	130	Tarski, A. 1955. A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5, 285--309.
	131	Wolfgang Thomas, On the Ehrenfeucht-Fraïssé Game in Theoretical Computer Science, Proceedings of the International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.559-568, April 13-17, 1993
	132	Thomason, S. K. 1972. Semantic analysis of tense logics. J. Symb. Log. 37, 1, 150--158.
	133	Daniele Turi , Gordon Plotkin, Towards a Mathematical Operational Semantics, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.280, June 29-July 02, 1997
	134	Zermelo, E. 1908. Untersuchungen über die Grundlagen der Mengenlehre I. Mathematische Annalen 65, 261--281. English translation, “Investigations in the foundations of set theory”, in Heijenoort (Ed.) {1967}, 199--215.