Zantema, Hans H - Well-definedness of Streams by Transformation and Termination

lmcs:1107 - Logical Methods in Computer Science, September 7, 2010, Volume 6, Issue 3
Well-definedness of Streams by Transformation and Termination

Authors: Zantema, Hans H

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.


Source : oai:arXiv.org:1008.2590
DOI : 10.2168/LMCS-6(3:21)2010
Volume: Volume 6, Issue 3
Published on: September 7, 2010
Submitted on: October 29, 2009
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.4.2, E.1


Share

Consultation statistics

This page has been seen 60 times.
This article's PDF has been downloaded 15 times.