2017

  1. Undecidability and Finite Automata
    Jörg Endrullis, Jeffrey Shallit, and Tim Smith
    In: Proc. Conf. Developments in Language Theory (DLT 2017), pp. 160–172, Springer (2017)
    paper

    Summary

    Using a novel rewriting problem, we show that several natural decision problems about finite automata are undecidable. In contrast, we also prove three related problems are decidable.

    We apply one result to prove the undecidability of a related problem about k-automatic sets of rational numbers.

    Bibtex

    @inproceedings{automata:undecidability:2017,
  author = {Endrullis, J\"{o}rg and Shallit, Jeffrey and Smith, Tim},
  title = {{Undecidability and Finite Automata}},
  booktitle = {Proc.\ Conf.\ Developments in Language Theory (DLT~2017)},
  volume = {10396},
  pages = {160--172},
  publisher = {Springer},
  series = {LNCS},
  year = {2017},
  doi = {10.1007/978-3-319-62809-7\_11},
  keywords = {automata, undecidability},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-319-62809-7_11

2014

  1. On the Complexity of Stream Equality
    Jörg Endrullis, Dimitri Hendriks, Rena Bakhshi, and Grigore Rosu
    Journal of Functional Programming , 24 (2-3) , pp. 166–217 (2014)
    paper

    Bibtex

    @article{complexity:stream:equality:2014,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Bakhshi, Rena and Rosu, Grigore},
  title = {{On the Complexity of Stream Equality}},
  journal = {Journal of Functional Programming},
  volume = {24},
  number = {2-3},
  pages = {166--217},
  year = {2014},
  doi = {10.1017/S0956796813000324},
  keywords = {rewriting, undecidability, streams},
  type = {journal}
}

    Digital Object Identifier

    10.1017/S0956796813000324

2012

  1. On the Complexity of Equivalence of Specifications of Infinite Objects
    Jörg Endrullis, Dimitri Hendriks, and Rena Bakhshi
    In: Proc. Int. Conf. on Functional Programming (ICFP 2012), pp. 153–164, ACM (2012)
    paper

    Bibtex

    @inproceedings{complexity:stream:equality:2012,
  author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Bakhshi, Rena},
  title = {{On the Complexity of Equivalence of Specifications of Infinite Objects}},
  booktitle = {Proc.\ Int.\ Conf.\ on Functional Programming (ICFP~2012)},
  pages = {153--164},
  publisher = {{ACM}},
  year = {2012},
  doi = {10.1145/2364527.2364551},
  keywords = {rewriting, undecidability, streams},
  type = {conference}
}

    Digital Object Identifier

    10.1145/2364527.2364551

2011

  1. Levels of Undecidability in Rewriting
    Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, and Hans Zantema
    Information 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

2009

  1. Complexity of Fractran and Productivity
    Jörg Endrullis, Clemens Grabmayer, and Dimitri Hendriks
    In: Proc. Conf. on Automated Deduction (CADE 2009), pp. 371–387, Springer (2009)
    paper

    Bibtex

    @inproceedings{complexity:productivity:2009,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri},
  title = {{Complexity of Fractran and Productivity}},
  booktitle = {Proc.\ Conf.\ on Automated Deduction (CADE~2009)},
  volume = {5663},
  pages = {371--387},
  publisher = {Springer},
  series = {LNCS},
  year = {2009},
  doi = {10.1007/978-3-642-02959-2\_28},
  keywords = {rewriting, undecidability, productivity},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-642-02959-2_28
  2. Degrees of Undecidability in Term Rewriting
    Jörg Endrullis, Herman Geuvers, and Hans Zantema
    In: Proc. Conf. on Computer Science Logic (CSL 2009), pp. 255–270, Springer (2009)
    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.

    We refer to Levels of Undecidability in Rewriting (Information and Computation 2011) for an extended journal version of this paper.

    Bibtex

    @inproceedings{rewriting:undecidability:degrees:2009,
  author = {Endrullis, J\"{o}rg and Geuvers, Herman and Zantema, Hans},
  title = {{Degrees of Undecidability in Term Rewriting}},
  booktitle = {Proc.\ Conf.\ on Computer Science Logic (CSL~2009)},
  volume = {5771},
  pages = {255--270},
  publisher = {Springer},
  series = {LNCS},
  year = {2009},
  doi = {10.1007/978-3-642-04027-6\_20},
  keywords = {rewriting, undecidability, termination, confluence},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-642-04027-6_20