Well-definedness of streams by transformation and termination

Research output: Contribution to journalArticleAcademicpeer-review

5 Citations (Scopus)
85 Downloads (Pure)

Abstract

Steams are innite sequences over a given data type. A stream specication is a set of equations intended to dene a stream. We propose a transformation from such a stream specication to a term rewriting system (TRS) in such a way that termination of the resulting TRS implies that the stream specication is well-dened, that is, admits a unique solution. As a consequence, proving well-denedness of several interesting stream specications 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-denedness. We give examples for which the above mentioned technique applies for the transformed specication while it fails for the original one.
Original languageEnglish
Pages (from-to)21-1/27
JournalLogical Methods in Computer Science
Volume6
Issue number3
DOIs
Publication statusPublished - 2010

Fingerprint

Dive into the research topics of 'Well-definedness of streams by transformation and termination'. Together they form a unique fingerprint.

Cite this