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.
各種検索
サポート
ヘルプ