2015

  1. Syllogistic Logic with "Most"
    Jörg Endrullis, and Lawrence S. Moss
    In: Proc. Int. Workshop on Logic, Language, Information, and Computation (WoLLIC 2015), pp. 124–139, Springer (2015)
    paper

    Summary

    This paper presents a sound and complete proof system for the logical system whose sentences are of the form

    • All X are Y,
    • Some X are Y, and
    • Most X are Y
    where we interpret these sentences on finite models, with the meaning of `most' being `strictly more than half'. Our proof system is syllogistic; there are no individual variables.

    We have published an extended journal version of this paper in Mathematical Structures in Computer Science, 2019.

    Bibtex

    @inproceedings{logic:most:2015,
  author = {Endrullis, J\"{o}rg and Moss, Lawrence S.},
  title = {{Syllogistic Logic with "Most"}},
  booktitle = {Proc.\ Int.\ Workshop on Logic, Language, Information, and Computation (WoLLIC~2015)},
  volume = {9160},
  pages = {124--139},
  publisher = {Springer},
  series = {LNCS},
  year = {2015},
  doi = {10.1007/978-3-662-47709-0\_10},
  keywords = {logic},
  type = {rewriting,conference}
}

    Digital Object Identifier

    10.1007/978-3-662-47709-0_10
  2. Regularity Preserving but Not Reflecting Encodings
    Jörg Endrullis, Clemens Grabmayer, and Dimitri Hendriks
    In: Proc. Symp. on Logic in Computer Science (LICS 2015), pp. 535–546, IEEE Computer Society (2015)
    paper

    Summary

    Encodings, that is, injective functions from words to words, have been studied extensively in several settings. In computability theory the notion of encoding is crucial for defining computability on arbitrary domains, as well as for comparing the power of models of computation. In language theory much attention has been devoted to regularity preserving functions.

    A natural question arising in these contexts is: Is there a bijective encoding such that its image function preserves regularity of languages, but its pre-image function does not? Our main result answers this question in the affirmative: For every countable class \( C \) of languages there exists a bijective encoding \( f \) such that for every language \( L \in C \) its image \( f[L] \) is regular.

    Our construction of such encodings has several noteworthy consequences. Firstly, anomalies arise when models of computation are compared with respect to a known concept of implementation that is based on encodings which are not required to be computable: Every countable decision model can be implemented, in this sense, by finite-state automata, even via bijective encodings. Hence deterministic finite-state automata would be equally powerful as Turing machine deciders. A second consequence concerns the recognizability of sets of natural numbers via number representations and finite automata. A set of numbers is said to be recognizable with respect to a representation if an automaton accepts the language of representations. Our result entails that there is one number representation with respect to which every recursive set is recognizable.

    Bibtex

    @inproceedings{regularity:reflecting:2015,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri},
  title = {{Regularity Preserving but Not Reflecting Encodings}},
  booktitle = {Proc.\ Symp.\ on Logic in Computer Science (LICS~2015)},
  pages = {535--546},
  publisher = {{IEEE} Computer Society},
  year = {2015},
  doi = {10.1109/LICS.2015.56},
  keywords = {automata},
  type = {conference}
}

    Digital Object Identifier

    10.1109/LICS.2015.56
  3. Proving Non-Termination by Finite Automata
    Jörg Endrullis, and Hans Zantema
    In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2015), pp. 160–176, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)
    paper

    Summary

    We present a new technique to prove non-termination of term rewriting. The basic idea is tofind a non-empty regular language of terms that is weakly closed under rewriting and does not containnormal forms. It is automated by representing the language by a tree automaton with a fixednumber of states, and expressing the mentioned requirements in a SAT formula. Satisfiabilityof this formula implies non-termination. Our approach succeeds for many examples where allearlier techniques fail, for instance for the S-rule from combinatory logic.

    See research for an overview of my research on termination.

    Bibtex

    @inproceedings{termination:automata:2015,
  author = {Endrullis, J\"{o}rg and Zantema, Hans},
  title = {{Proving Non-termination by Finite Automata}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2015)},
  volume = {36},
  pages = {160--176},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  series = {LIPIcs},
  year = {2015},
  doi = {10.4230/LIPIcs.RTA.2015.160},
  keywords = {rewriting, termination, automata},
  type = {conference}
}

    Digital Object Identifier

    10.4230/LIPIcs.RTA.2015.160
  4. Degrees of Transducibility
    Jörg Endrullis, Jan Willem Klop, Aleksi Saarela, and Markus A. Whiteland
    In: Proc. Conf. on Combinatorics on Words (WORDS 2015), pp. 1–13, Springer (2015)
    paper

    Summary

    In this survey paper we compare different hierarchies of degrees of infinite words (streams) arising from transformation (transduction) of these words. As transformational devices we consider

    • Turing machines,
    • finite state transducers, and
    • Mealy machines.
    The stream transformation realised by these machine models induces equivalence classes of streams, called degrees, and a partial order on these degrees. We refer to these hierarchies as Turing degrees, Transducer degrees and Mealy degrees, respectively.

    While Turing degrees have been extensively studied in the 60th and 70th, hardly anything is known about Transducer and Mealy degrees. In this paper, we compare central properties of these hierarchies and mention many open problems.

    See research for an introduction to finite state transducers, an overview of my research and many open questions.

    Bibtex

    @inproceedings{streams:degrees:transducibility:2015,
  author = {Endrullis, J\"{o}rg and Klop, Jan Willem and Saarela, Aleksi and Whiteland, Markus A.},
  title = {{Degrees of Transducibility}},
  booktitle = {Proc.\ Conf.\ on Combinatorics on Words (WORDS~2015)},
  volume = {9304},
  pages = {1--13},
  publisher = {Springer},
  series = {LNCS},
  year = {2015},
  doi = {10.1007/978-3-319-23660-5\_1},
  keywords = {streams, degrees, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-319-23660-5_1
  5. The Degree of Squares Is an Atom
    Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, and Hans Zantema
    In: Proc. Conf. on Combinatorics on Words (WORDS 2015), pp. 109–121, Springer (2015)
    paper

    Summary

    A finite state transducer is a finite automaton that transforms input words into output words. The transducer reads the input letter by letter, in each step producing an output word and changing its state.

    While finite state transducers are very simple and elegant devices, their power in transforming infinite words is hardly understood.

    In this paper we show that the degree of the stream \[ \prod_{i = 0}^\infty 1\, 0^{i^2} = 1 \, 0^0 \, 1 \, 0^1 \, 1 \, 0^4 \, 1 \, 0^9 \, 1 \, 0^{16} \, \cdots = 1101000010000000001 \cdots \] is an atom in the hierarchy of streams arising from finite state transduction.

    In the paper Degrees of Infinite Words, Polynomials and Atoms we vastly generalise this result by showing that there is precisely one atom for each polynomial degree. See research for an introduction to finite state transducers, an overview of my research and many open questions.

    Bibtex

    @inproceedings{streams:degrees:squares:2015,
  author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Zantema, Hans},
  title = {{The Degree of Squares is an Atom}},
  booktitle = {Proc.\ Conf.\ on Combinatorics on Words (WORDS~2015)},
  volume = {9304},
  pages = {109--121},
  publisher = {Springer},
  series = {LNCS},
  year = {2015},
  doi = {10.1007/978-3-319-23660-5\_10},
  keywords = {streams, degrees, automata},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-319-23660-5_10
  6. A Coinductive Framework for Infinitary Rewriting and Equational Reasoning
    Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva
    In: Proc. Conf. on Rewriting Techniques and Applications (RTA 2015), pp. 143–159, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)
    paper

    Summary

    We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way.

    The framework lends itself to an elegant and concise definition of the infinitary rewrite relation \( \to^\infty \) in terms of the single step relation \( \to \): \[ {\to^\infty} \,=\, \mu R. \nu S. ( \to \cup \mathrel{\overline{R}} )^* \mathrel{;} \overline{S} \] Here \( \mu \) and \( \nu \) are the least and greatest fixed-point operators, respectively, and \[ \overline{R} \,=\, \{\, (\, f(s_1,\ldots,s_n),\, \,f(t_1,\ldots,t_n) \,) \mid f \in \Sigma,\, s_1\! \mathrel{R} t_1,\ldots,s_n\! \mathrel{R} t_n \,\} \cup \text{Id} \] The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework suitable for formalizations in theorem provers.

    We refer to Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic (LMCS 2018) for an extended journal version of this paper.

    We build on ideas in Infinitary Rewriting Coinductively (TYPES 2012) giving a coinductive perspective on infinitary lambda calculus. We extend these ideas to rewrite sequences beyond length omega by mixing induction and coinduction (least and greatest fixed-points).

    Bibtex

    @inproceedings{infintary:rewriting:coinductive:2015,
  author = {Endrullis, J\"{o}rg and Hansen, Helle Hvid and Hendriks, Dimitri and Polonsky, Andrew and Silva, Alexandra},
  title = {{A Coinductive Framework for Infinitary Rewriting and Equational Reasoning}},
  booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA 2015)},
  volume = {36},
  pages = {143--159},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  series = {LIPIcs},
  year = {2015},
  doi = {10.4230/LIPIcs.RTA.2015.143},
  keywords = {rewriting, infinitary rewriting, coinduction},
  type = {conference}
}

    Digital Object Identifier

    10.4230/LIPIcs.RTA.2015.143