文章基本信息
- 标题：Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction
- 本地全文：下载
- 作者：Keiko Nakata ; Tarmo Uustalu
- 期刊名称：Electronic Proceedings in Theoretical Computer Science
- 电子版ISSN：2075-2180
- 出版年度：2010
- 卷号：32
- 页码：57-75
- DOI：10.4204/EPTCS.32.5
- 出版社：Open Publishing Association
- 摘要：We look at the operational semantics of languages with interactive I/O through the glasses of constructive type theory. Following on from our earlier work on coinductive trace-based semantics for While, we define several big-step semantics for While with interactive I/O, based on resumptions and termination-sensitive weak bisimilarity. These require nesting inductive definitions in coinductive definitions, which is interesting both mathematically and from the point-of-view of implementation in a proof assistant.
After first defining a basic semantics of statements in terms of resumptions with explicit internal actions (delays), we introduce a semantics in terms of delay-free resumptions that essentially removes finite sequences of delays on the fly from those resumptions that are responsive. Finally, we also look at a semantics in terms of delay-free resumptions supplemented with a silent divergence option. This semantics hinges on decisions between convergence and divergence and is only equivalent to the basic one classically.
We have fully formalized our development in Coq.
