Proceedings of the Workshop on Computation: Theory and Practice (WCTP 2024)

<Previous Article In Volume
Next Article In Volume>

Formalizing Reversible Computations for Synchronous Dataflow Languages with Infinite Lists

Authors
Sosuke Moriguchi1, *, Satoshi Takimoto1, Mizuki Shirai1, Takuo Watanabe1
1Department of Computer Science, Institute of Science Tokyo, Tokyo, Japan
*Corresponding author. Email: chiguri@acm.org
Corresponding Author
Sosuke Moriguchi
Available Online 30 April 2025.
DOI
10.2991/978-94-6463-684-0_2How to use a DOI?
Keywords
synchronous dataflow language; theorem proving; reversible computation; coinductive definition
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.

Copyright
© 2025 The Author(s)
Open Access
Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International License (http://creativecommons.org/licenses/by-nc/4.0/), which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

Download article (PDF)

<Previous Article In Volume
Next Article In Volume>
Volume Title
Proceedings of the Workshop on Computation: Theory and Practice (WCTP 2024)
Series
Atlantis Highlights in Computer Sciences
Publication Date
30 April 2025
ISBN
978-94-6463-684-0
ISSN
2589-4900
DOI
10.2991/978-94-6463-684-0_2How to use a DOI?
Copyright
© 2025 The Author(s)
Open Access
Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International License (http://creativecommons.org/licenses/by-nc/4.0/), which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

Cite this article

risenwbib
TY  - CONF
AU  - Sosuke Moriguchi
AU  - Satoshi Takimoto
AU  - Mizuki Shirai
AU  - Takuo Watanabe
PY  - 2025
DA  - 2025/04/30
TI  - Formalizing Reversible Computations for Synchronous Dataflow Languages with Infinite Lists
BT  - Proceedings of the  Workshop on Computation: Theory and Practice (WCTP 2024)
PB  - Atlantis Press
SP  - 7
EP  - 19
SN  - 2589-4900
UR  - https://doi.org/10.2991/978-94-6463-684-0_2
DO  - 10.2991/978-94-6463-684-0_2
ID  - Moriguchi2025
ER  -