Publications in 2011
2011
- On Equal μ-TermsJörg Endrullis, Clemens Grabmayer, Jan Willem Klop, and Vincent van OostromTheoretical Computer Science , 412 (28) , pp. 3175–3202 (2011)paper
Summary
We consider the rewrite system Rμ with μx.M → μM [x := μx.M ] as its single rewrite rule. This kernel system denoting recursively defined objects occurs in several contexts, e.g. it is the framework of recursive types. For general signatures this rewriting system is widely used to represent and manipulate infinite regular trees.
The main concern of this paper is the convertibility relation for μ-terms as given by the μ-rule, in particular its decidability. This relation is sometimes called weak μ-equality, in contrast with strong μ-equality, which is given by equality of the possibly infinite tree unwinding of μ-terms. While strong equality has received much attention, the opposite is the case for weak μ-equality.
We present three alternative proofs for decidability of weak μ-equality.
Bibtex
@article{equal:mu:terms:2011, author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Klop, Jan Willem and van~Oostrom, Vincent}, title = {{On Equal $\mu$-Terms}}, journal = {Theoretical Computer Science}, volume = {412}, number = {28}, pages = {3175--3202}, year = {2011}, doi = {10.1016/j.tcs.2011.04.011}, keywords = {rewriting,automata}, type = {journal} }Digital Object Identifier
10.1016/j.tcs.2011.04.011
- Lazy Productivity via TerminationJörg Endrullis, and Dimitri HendriksTheoretical Computer Science , 412 (28) , pp. 3203–3225 (2011)paper
Bibtex
@article{productivity:termination:2011, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri}, title = {{Lazy Productivity via Termination}}, journal = {Theoretical Computer Science}, volume = {412}, number = {28}, pages = {3203--3225}, year = {2011}, doi = {10.1016/j.tcs.2011.03.024}, keywords = {rewriting, infinitary rewriting, productivity, termination}, type = {journal} }Digital Object Identifier
10.1016/j.tcs.2011.03.024
- Fast Leader Election in Anonymous Rings with Bounded Expected DelayRena Bakhshi, Jörg Endrullis, Wan Fokkink, and Jun PangInformation Processing Letters , 111 (17) , pp. 864–870 (2011)paper
Bibtex
@article{bounded:expected:delay:2011, author = {Bakhshi, Rena and Endrullis, J\"{o}rg and Fokkink, Wan and Pang, Jun}, title = {{Fast Leader Election in Anonymous Rings with Bounded Expected Delay}}, journal = {Information Processing Letters}, volume = {111}, number = {17}, pages = {864--870}, year = {2011}, doi = {10.1016/j.ipl.2011.06.003}, keywords = {protocols}, type = {journal} }Digital Object Identifier
10.1016/j.ipl.2011.06.003
- Degrees of StreamsJörg Endrullis, Dimitri Hendriks, and Jan Willem KlopJournal of Integers , 11B (A6) , pp. 1–40 (2011)paper
Bibtex
@article{streams:degrees:2011, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem}, title = {{Degrees of Streams}}, journal = {Journal of Integers}, volume = {11B}, number = {A6}, pages = {1--40}, year = {2011}, note = {Proceedings of the Leiden Numeration Conference 2010}, keywords = {streams, degrees, automata}, type = {journal} } - Proving Equality of Streams AutomaticallyHans Zantema, and Jörg EndrullisIn: Proc. Conf. on Rewriting Techniques and Applications (RTA 2011), pp. 393–408, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)paper
Bibtex
@inproceedings{streams:equality:2011, author = {Zantema, Hans and Endrullis, J\"{o}rg}, title = {{Proving Equality of Streams Automatically}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2011)}, volume = {10}, pages = {393--408}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2011}, doi = {10.4230/LIPIcs.RTA.2011.393}, keywords = {rewriting, infinitary rewriting, streams}, type = {conference} }Digital Object Identifier
10.4230/LIPIcs.RTA.2011.393
- Infinitary Rewriting CoinductivelyJörg Endrullis, and Andrew PolonskyIn: Proc. Conf. on Types for Proofs and Programs (TYPES 2012), pp. 16–27, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)paper
Summary
We provide a coinductive definition of strongly convergent reductions between infinite lambda terms. This approach avoids the notions of ordinals and metric convergence which have appeared in the earlier definitions of the concept. As an illustration, we prove the existence part of the infinitary standardization theorem. The proof is fully formalized in Coq using coinductive types.
The paper concludes with a characterization of infinite lambda terms which reduce to themselves in a single beta step.
The papers
extend the idea in this paper to reductions of length beyond omega.The extension to reduction lengths beyond omega requires mixing of induction and coinduction. Therefore the simpler setup presented in the current paper (Infinitary Rewriting Coinductively) is preferrable whenever there is no need for reductions longer than omega. This concerns for instance rewrite systems having the compression property, such as lambda calculus and left-linear term rewriting systems (with finite left-hand sides).
Bibtex
@inproceedings{infintary:lambda:coinductive:2011, author = {Endrullis, J\"{o}rg and Polonsky, Andrew}, title = {{Infinitary Rewriting Coinductively}}, booktitle = {Proc.\ Conf.\ on Types for Proofs and Programs (TYPES~2012)}, volume = {19}, pages = {16--27}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2011}, doi = {10.4230/LIPIcs.TYPES.2011.16}, keywords = {rewriting, infinitary rewriting, coinduction}, type = {conference} }Digital Object Identifier
10.4230/LIPIcs.TYPES.2011.16
- Levels of Undecidability in RewritingJörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, and Hans ZantemaInformation and Computation , 209 (2) , pp. 227–245 (2011)paper
Summary
Undecidability of various properties of first-order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This classification gives rise to a hierarchy of distinct levels of undecidability, starting from the arithmetical hierarchy classifying properties using first order arithmetical formulas, and continuing into the analytic hierarchy, where quantification over function variables is allowed.
In this paper we give an overview of how the main properties of first-order term rewriting systems are classified in these hierarchies. We consider properties related to normalization (strong normalization, weak normalization and dependency problems) and properties related to confluence (confluence, local confluence and the unique normal form property). For all of these we distinguish between the single term version and the uniform version. Where appropriate, we also distinguish between ground and open terms.
Most uniform properties are \( \Pi^0_2 \)-complete. The particular problem of local confluence turns out to be \( \Pi^0_2 \)-complete for ground terms, but only \( \Sigma^0_1 \)-complete (and thereby recursively enumerable) for open terms. The most surprising result concerns dependency pair problems without minimality flag: we prove this problem to be \( \Pi^1_1 \)-complete, hence not in the arithmetical hierarchy, but properly in the analytic hierarchy.
This paper is an extended version of Degrees of Undecidability in Term Rewriting (CSL 2009).
Bibtex
@article{rewriting:undecidability:levels:2011, author = {Endrullis, J\"{o}rg and Geuvers, Herman and Simonsen, Jakob Grue and Zantema, Hans}, title = {{Levels of Undecidability in Rewriting}}, journal = {Information and Computation}, volume = {209}, number = {2}, pages = {227--245}, year = {2011}, doi = {10.1016/j.ic.2010.09.003}, keywords = {rewriting, undecidability, termination, confluence}, type = {journal} }Digital Object Identifier
10.1016/j.ic.2010.09.003