2010

1. Productivity of Stream Definitions

   Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Ariya Isihara, and Jan Willem Klop

   Theoretical Computer Science , 411 (4-5) , pp. 765–782 (2010)

   summary paper bib doi

   Summary

   We give an algorithm for deciding productivity of a large and natural class of recursive stream definitions. A stream definition is called `productive' if it can be evaluated continually in such a way that a uniquely determined stream in constructor normal form is obtained as the limit. Whereas productivity is undecidable for stream definitions in general, we show that it can be decided for `pure' stream definitions. For every pure stream definition the process of its evaluation can be modelled by the dataflow of abstract stream elements, called `pebbles', in a finite `pebbleflow net(work)'. And the production of a pebbleflow net associated with a pure stream definition, that is, the amount of pebbles the net is able to produce at its output port, can be calculated by reducing nets to trivial nets.

   This paper is an extended version of Productivity of Stream Definitions (2007) (FCT 2007).

   See research for an overview of my research on productivity.

   Bibtex

   @article{productivity:streams:2010,
     author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Isihara, Ariya and Klop, Jan Willem},
     title = {{Productivity of Stream Definitions}},
     journal = {Theoretical Computer Science},
     volume = {411},
     number = {4-5},
     pages = {765--782},
     year = {2010},
     doi = {10.1016/j.tcs.2009.10.014},
     keywords = {rewriting, infinitary rewriting, productivity},
     type = {journal}
   }
   

   Digital Object Identifier

   10.1016/j.tcs.2009.10.014

2. Brief Announcement: Asynchronous Bounded Expected Delay Networks

   Rena Bakhshi, Jörg Endrullis, Wan Fokkink, and Jun Pang

   In: Proc. Symp. on Principles of Distributed Computing (PODC 2010), pp. 392–393, ACM (2010)

   paper bib doi

   Bibtex

   @inproceedings{bounded:expected:delay:2010,
     author = {Bakhshi, Rena and Endrullis, J\"{o}rg and Fokkink, Wan and Pang, Jun},
     title = {{Brief Announcement: Asynchronous Bounded Expected Delay Networks}},
     booktitle = {Proc.\ Symp.\ on Principles of Distributed Computing (PODC~2010)},
     pages = {392--393},
     publisher = {{ACM}},
     year = {2010},
     doi = {10.1145/1835698.1835787},
     keywords = {protocols},
     type = {conference}
   }
   

   Digital Object Identifier

   10.1145/1835698.1835787

3. Automating the Mean-Field Method for Large Dynamic Gossip Networks

   Rena Bakhshi, Jörg Endrullis, Stefan Endrullis, Wan Fokkink, and Boudewijn R. Haverkort

   In: Proc. Conf. on Quantitative Evaluation of Systems (QEST 2010), pp. 241–250, IEEE Computer Society (2010)

   paper bib doi

   Bibtex

   @inproceedings{meanfield:2010,
     author = {Bakhshi, Rena and Endrullis, J\"{o}rg and Endrullis, Stefan and Fokkink, Wan and Haverkort, Boudewijn R.},
     title = {{Automating the Mean-Field Method for Large Dynamic Gossip Networks}},
     booktitle = {Proc.\ Conf.\ on Quantitative Evaluation of Systems (QEST~2010)},
     pages = {241--250},
     publisher = {{{IEEE} Computer Society}},
     year = {2010},
     doi = {10.1109/QEST.2010.38},
     keywords = {protocols},
     type = {conference}
   }
   

   Digital Object Identifier

   10.1109/QEST.2010.38

4. Local Termination: Theory and Practice

   Jörg Endrullis, Roel C. de Vrijer, and Johannes Waldmann

   Logical Methods in Computer Science , 6 (3) (2010)

   paper bib doi

   Bibtex

   @article{termination:local:2010,
     author = {Endrullis, J\"{o}rg and de~Vrijer, Roel C. and Waldmann, Johannes},
     title = {{Local Termination: Theory and Practice}},
     journal = {Logical Methods in Computer Science},
     volume = {6},
     number = {3},
     year = {2010},
     doi = {10.2168/LMCS-6(3:20)2010},
     keywords = {rewriting, termination, automata},
     type = {journal}
   }
   

   Digital Object Identifier

   10.2168/LMCS-6(3:20)2010

5. Transforming Outermost into Context-Sensitive Rewriting

   Jörg Endrullis, and Dimitri Hendriks

   Logical Methods in Computer Science , 6 (2) (2010)

   summary paper bib doi

   Summary

   We define two transformations from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. In the transformation based on `context extension', each outermost rewrite step is modeled by exactly one step in the transformed system. This transformation turns out to be complete for the class of left-linear TRSs. The second transformation is called `dynamic labeling' and results in smaller sized context-sensitive TRSs. Here each modeled step is adjoined with a small number of auxiliary steps. As a result state-of-the-art termination methods for context-sensitive rewriting become available for proving termination of outermost rewriting. Both transformations have been implemented in Jambox, making it the most successful tool in the category of outermost rewriting of the annual termination competition.

   This is an extended version of the paper From Outermost to Context-Sensitive Rewriting (RTA 2009).

   See research for an overview of my research on termination.

   Bibtex

   @article{termination:outermost:2010,
     author = {Endrullis, J\"{o}rg and Hendriks, Dimitri},
     title = {{Transforming Outermost into Context-Sensitive Rewriting}},
     journal = {Logical Methods in Computer Science},
     volume = {6},
     number = {2},
     year = {2010},
     doi = {10.2168/LMCS-6(2:5)2010},
     keywords = {rewriting, termination, automata},
     type = {journal}
   }
   

   Digital Object Identifier

   10.2168/LMCS-6(2:5)2010

6. Modular Construction of Fixed Point Combinators and Clocked Böhm Trees

   Jörg Endrullis, Dimitri Hendriks, and Jan Willem Klop

   In: Proc. Symp. on Logic in Computer Science (LICS 2010), pp. 111–119, IEEE Computer Society (2010)

   summary paper bib doi

   Summary

   One of the best-known methods for discriminating lambda terms with respect to \( \beta \)-convertibility is due to Corrado Böhm. Roughly speaking, the Böhm tree of a lambda term is its infinite normal form. If lambda terms have distinct Böhm trees, then they are not \( \beta \)-convertible. But what if their Böhm trees coincide? For example, all fixed-point combinators have the same Böhm tree, namely \[ \lambda x. x(x(x(\ldots))) \]

   We refine Böhm trees with a clock that records how many head reduction steps have been used to rewrite each subterm to head normal form. We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms (in particular many fixed-point combinators) having the same Böhm trees.

   We refer to Discriminating Lambda-Terms Using Clocked Boehm Trees (LMCS 2014) for an extended journal version of this paper. In the extended version we improve the precision of the clocks to atomic clocks and we answer a question of Gordon Plotkin, showing that the method can be used beyond simple terms.

   See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.

   Bibtex

   @inproceedings{lambda:clocks:2010,
     author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem},
     title = {{Modular Construction of Fixed Point Combinators and Clocked B\"{o}hm Trees}},
     booktitle = {Proc.\ Symp.\ on Logic in Computer Science (LICS~2010)},
     pages = {111--119},
     publisher = {{IEEE} Computer Society},
     year = {2010},
     doi = {10.1109/LICS.2010.8},
     keywords = {rewriting, infinitary rewriting, lambda calculus},
     type = {conference}
   }
   

   Digital Object Identifier

   10.1109/LICS.2010.8

7. Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting

   Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van Oostrom

   In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2010), pp. 85–102, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2010)

   paper bib doi

   Bibtex

   @inproceedings{infinitary:weakly:orthogonal:unique:normal:forms:2010,
     author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and van~Oostrom, Vincent},
     title = {{Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting}},
     booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2010)},
     volume = {6},
     pages = {85--102},
     publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
     series = {LIPIcs},
     year = {2010},
     doi = {10.4230/LIPIcs.RTA.2010.85},
     keywords = {rewriting, infinitary rewriting, lambda calculus},
     type = {conference}
   }
   

   Digital Object Identifier

   10.4230/LIPIcs.RTA.2010.85