Lazy Productivity via Termination

J. Endrullis, R.D.A. Hendriks

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

We present a procedure for transforming strongly sequential constructor-based term rewriting systems (TRSs) into context-sensitive TRSs in such a way that productivity of the input system is equivalent to termination of the output system. Thereby automated termination provers become available for proving productivity. A TRS is called productive if all its finite ground terms are constructor normalizing, and all 'inductive constructor paths' through the resulting (possibly non-wellfounded) constructor normal form are finite. To our knowledge, this is the first complete transformation from productivity to termination. The transformation proceeds in two steps: (i) The strongly sequential TRS is converted into a shallow TRS, where patterns do not have nested constructors. (ii) The shallow TRS is transformed into a context-sensitive TRS, where rewriting below constructors and in arguments not 'consumed from' is disallowed. Furthermore, we show how lazy evaluation can be encoded by strong sequentiality, thus extending our transformation to, e.g., Haskell programs. Finally, we present a simple, but fruitful extension of matrix interpretations to make them applicable for proving termination of context-sensitive TRSs. © 2011 Elsevier B.V. All rights reserved.
Original languageEnglish
Pages (from-to)3203-3225
JournalTheoretical Computer Science
Volume412
Issue number28
DOIs
Publication statusPublished - 2011

Fingerprint Dive into the research topics of 'Lazy Productivity via Termination'. Together they form a unique fingerprint.

Cite this