Disproving strong head normalization and general productivity automatically in infinitary term rewriting systems

Munehiro Iwami, Takahito Aoto

Research output: Contribution to journalArticle

Abstract

Infinitary term rewriting has been proposed to model functional programs that deal with virtually infinite data structures such as streams or lazy lists. Strong head normalization is a fundamental property of infinitary term rewriting systems and methods for proving this property have been proposed by Zantema (2008) and Endrullis et al. (2009). Endrullis et al. (2010) have proposed a class of infinitary term rewriting systems-stream term rewriting systems-and they have given a decision procedure of the productivity of streams for a class of stream term rewriting systems. In this paper, we present procedures for disproving these two properties of infinitary term rewriting systems-the strong head normalization and the productivity. The basic idea of our procedure is to construct rational counterexamples which are infinitary terms but have finite representations. The correctness of our procedures is proved and an implementation is reported. Our experiments reveal that our procedures successfully disprove the strong head normalization and the productivity automatically for some examples for which no automated disproving procedure is known.

Original languageEnglish
Pages (from-to)211-239
Number of pages29
JournalComputer Software
Volume29
Issue number1
Publication statusPublished - 2012

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Disproving strong head normalization and general productivity automatically in infinitary term rewriting systems'. Together they form a unique fingerprint.

Cite this