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

lmcs:1107 - Logical Methods in Computer Science, September 7, 2010, Volume 6, Issue 3 - https://doi.org/10.2168/LMCS-6(3:21)2010
Well-definedness of Streams by Transformation and TerminationArticle

Authors: Hans H Zantema

    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.


    Volume: Volume 6, Issue 3
    Published on: September 7, 2010
    Imported on: October 29, 2009
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.4.2, E.1

    3 Documents citing this article

    Consultation statistics

    This page has been seen 1222 times.
    This article's PDF has been downloaded 383 times.