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
  2. Clocked Lambda Calculus
    Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky
    Mathematical Structures in Computer Science , 27 (5) , pp. 782–806 (2017)
    paper

    Summary

    We introduce the clocked lambda calculus, an extension of the classical lambda calculus with a unary symbol \( \tau \) that serves as a witness of \( \beta \)-steps. This calculus consists of the following two rules: \[ \begin{aligned} (\lambda x.M) N &\to \tau( M[x = N] ) \\ \tau(M)N &\to \tau(MN) \end{aligned} \] The clocked lambda-calculus is infinitary strongly normalizing, infinitary confluent, and the unique infinitary normal forms constitute enriched Böhm trees (more precisely, Lévy-Longo trees), which we call clocked Böhm trees. We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms having the same Böhm trees.

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

    Bibtex

    @article{clocked:lambda:calculus:2017,
      author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew},
      title = {{Clocked Lambda Calculus}},
      journal = {Mathematical Structures in Computer Science},
      volume = {27},
      number = {5},
      pages = {782--806},
      year = {2017},
      doi = {10.1017/S0960129515000389},
      keywords = {rewriting, infinitary rewriting, lambda calculus},
      type = {journal}
    }
    

    Digital Object Identifier

    10.1017/S0960129515000389