We are concerned with demonstrating productivity of specifications of infinite streams of data, based on orthogonal rewrite rules.
In general, this property is undecidable, but for restricted formats computable sufficient conditions can be obtained.
The usual analysis, also adopted here, disregards the identity of data, thus leading to approaches that we call data-oblivious.
We present a method that is provably optimal among all such data-oblivious approaches.
This means that in order to improve on our algorithm one has to proceed in a data-aware fashion.

See research for an overview of my research on productivity.

Bibtex

@inproceedings{productivity:data:oblivious:2008,
author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri},
title = {{Data-Oblivious Stream Productivity}},
booktitle = {Proc.\ Conf.\ on Logic for Programming Artificial Intelligence and Reasoning (LPAR~2008)},
number = {5330},
pages = {79--96},
publisher = {Springer},
series = {LNCS},
year = {2008},
doi = {10.1007/978-3-540-89439-1\_6},
keywords = {rewriting, infinitary rewriting, productivity},
type = {conference}
}

We present a new method for automatically proving termination of term rewriting using matrix interpretation (weighted automata with natural numbers as weights).
It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease,
but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular nontotal well-founded ordering.
Function symbols are interpreted by linear mappings represented by matrices.
This method allows us to prove termination and relative termination.

A modification of the latter, in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation.
By bounding the dimension and the matrix coefficients, the search problem becomes finite.
Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver.

See research for an overview of my research on termination.

Bibtex

@article{termination:matrix:2008,
author = {Endrullis, J\"{o}rg and Waldmann, Johannes and Zantema, Hans},
title = {{Matrix Interpretations for Proving Termination of Term Rewriting}},
journal = {Journal of Automated Reasoning},
volume = {40},
number = {2-3},
pages = {195--220},
year = {2008},
doi = {10.1007/s10817-007-9087-9},
keywords = {rewriting, termination},
type = {journal}
}

@inproceedings{infinitary:normalization:2009,
author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and de~Vrijer, Roel C.},
title = {{Proving Infinitary Normalization}},
booktitle = {Proc.\ Conf.\ on Types for Proofs and Programs (TYPES~2008)},
volume = {5497},
pages = {64--82},
publisher = {Springer},
series = {LNCS},
year = {2008},
doi = {10.1007/978-3-642-02444-3\_5},
keywords = {rewriting, infinitary rewriting, automata},
type = {conference}
}