2008

  1. Data-Oblivious Stream Productivity
    Jörg Endrullis, Clemens Grabmayer, and Dimitri Hendriks
    In: Proc. Conf. on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2008) , pp. 79–96 , Springer (2008)
    paper

    Summary

    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}
}

    Digital Object Identifier

    10.1007/978-3-540-89439-1_6
  2. Matrix Interpretations for Proving Termination of Term Rewriting
    Jörg Endrullis, Johannes Waldmann, and Hans Zantema
    Journal of Automated Reasoning , 40 (2-3) , pp. 195–220 (2008)
    paper

    Summary

    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.

    This is an extended version of the paper Matrix Interpretations for Proving Termination of Term Rewriting (IJCAR 2006).

    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}
}

    Digital Object Identifier

    10.1007/s10817-007-9087-9
  3. Reduction under Substitution
    Jörg Endrullis, and Roel C. de Vrijer
    In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2008) , pp. 425–440 , Springer (2008)
    paper

    Bibtex

    @inproceedings{lambda:reduction:under:substitution:2008,
  author = {Endrullis, J\"{o}rg and de~Vrijer, Roel C.},
  title = {{Reduction under Substitution}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2008)},
  volume = {5117},
  pages = {425--440},
  publisher = {Springer},
  series = {LNCS},
  year = {2008},
  doi = {10.1007/978-3-540-70590-1\_29},
  keywords = {rewriting, lambda calculus},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-540-70590-1_29
  4. Proving Infinitary Normalization
    Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Roel C. de Vrijer
    In: Proc. Conf. on Types for Proofs and Programs (TYPES 2008) , pp. 64–82 , Springer (2008)
    paper

    Bibtex

    @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}
}

    Digital Object Identifier

    10.1007/978-3-642-02444-3_5