Home >

news Help

Publication Information


Title
Japanese: 
English:Formalizing Reversible Computations for Synchronous Dataflow Languages with Infinite Lists 
Author
Japanese: 森口 草介, 瀧本 哲史, 白井 瑞貴, 渡部 卓雄.  
English: Sosuke Moriguchi, Satoshi Takimoto, Mizuki Shirai, Takuo Watanabe.  
Language English 
Journal/Book name
Japanese: 
English:Proceedings of 13th Workshop on Computation: Theory and Practice (WCTP 2024) 
Volume, Number, Page         pp. 7-19
Published date Apr. 30, 2025 
Publisher
Japanese: 
English:Atlantis Press 
Conference name
Japanese: 
English:13th Workshop on Computation: Theory and Practice (WCTP 2024) 
Conference site
Japanese: 
English:Manila 
DOI https://doi.org/10.2991/978-94-6463-684-0_2
Abstract Computational systems that deal with discrete time, such as stream computations and synchronous data flow languages, can be modeled using lists. However, most list operations are on finite lists, and it is not easy to define them for infinite lists to express persistent behavior. In particular, when using theorem provers, intuitive definitions are unacceptable due to restrictions on the handling of infinities. When integrating computational failures into the system, existing research either directly expresses failures or utilizes a mechanism that continues to send invalid values indefinitely. Still, the latter cannot determine failures in terms of computation. In this study, we formalize a model of a reversible synchronous dataflow language using finite and infinite lists and show that the semantics of each correspond to each other using the Coq theorem prover. For infinite lists, the inconsistency that arises as a result of incorporating failures into the list is resolved using finite lookahead.

©2007 Institute of Science Tokyo All rights reserved.