On the Origins of Bisimulation and Coinduction

被引:97
作者
Sangiorgi, Davide [1 ]
机构
[1] Univ Bologna, Dipartimento Sci Informaz, I-40126 Bologna, Italy
来源
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 2009年 / 31卷 / 04期
关键词
Theory; Verification; Bisimulation; coinduction; fixed points; greatest fixed points; history; SET-THEORY; ALGOL; 60;
D O I
10.1145/1516507.1516510
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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.
引用
收藏
页数:41
相关论文
共 137 条
[1]  
Aczel P., 1988, CSLI Lecture Notes, V14
[2]  
ACZEL P, 1993, LECT NOTES COMPUTER, V802, P1
[3]  
ALVAREZ C, 1991, LECT NOTES COMPUT SC, V505, P288
[4]   SUBTYPING RECURSIVE TYPES [J].
AMADIO, RM ;
CARDELLI, L .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1993, 15 (04) :575-631
[5]  
[Anonymous], 1971, FILOSOFSKA STUDIER
[6]  
[Anonymous], 1971, IJCAI
[7]  
[Anonymous], THEORY COMPUTING MAC
[8]  
[Anonymous], 2007, Reactive Systems: Modelling, Specification and Verification
[9]  
[Anonymous], 1928, Annales Soc. Polon. Math.
[10]  
[Anonymous], 2002, Cambridge Tracts in Theoretical Computer Science