Well-definedness of Streams by Transformation and Termination
From MaRDI portal
Publication:2786138
DOI10.2168/LMCS-6(3:21)2010zbMATH Open1208.68110arXiv1008.2590OpenAlexW3106344214MaRDI QIDQ2786138
Publication date: 21 September 2010
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Abstract: Streams are infinite sequences over a given data type. A stream specification is a set of equations intended to define a stream. We propose a transformation from such a stream specification to a term rewriting system (TRS) in such a way that termination of the resulting TRS implies that the stream specification is well-defined, that is, admits a unique solution. As a consequence, proving well-definedness of several interesting stream specifications can be done fully automatically using present powerful tools for proving TRS termination. In order to increase the power of this approach, we investigate transformations that preserve semantics and well-definedness. We give examples for which the above mentioned technique applies for the ransformed specification while it fails for the original one.
Full work available at URL: https://arxiv.org/abs/1008.2590
Related Items (2)
Uses Software
This page was built for publication: Well-definedness of Streams by Transformation and Termination
