2020

  1. Decreasing Diagrams for Confluence and Commutation
    Jörg Endrullis, Jan Willem Klop, and Roy Overbeek
    Logical Methods in Computer Science , Volume 16, Issue 1 (2020)
    paper

    Summary

    Like termination, confluence is a central property of rewrite systems. Unlike for termination, however, there exists no known complexity hierarchy for confluence. In this paper we investigate whether the decreasing diagrams technique can be used to obtain such a hierarchy.

    The decreasing diagrams technique is one of the strongest and most versatile methods for proving confluence of abstract rewrite systems. It is complete for countable systems, and it has many well-known confluence criteria as corollaries. So what makes decreasing diagrams so powerful? In contrast to other confluence techniques, decreasing diagrams employ a labelling of the steps with labels from a well-founded order in order to conclude confluence of the underlying unlabelled relation. Hence it is natural to ask how the size of the label set influences the strength of the technique. In particular, what class of abstract rewrite systems can be proven confluent using decreasing diagrams restricted to 1 label, 2 labels, 3 labels, and so on?

    Surprisingly, we find that two labels suffice for proving confluence for every abstract rewrite system having the cofinality property, thus in particular for every confluent, countable system. Secondly, we show that this result stands in sharp contrast to the situation for commutation of rewrite relations, where the hierarchy does not collapse.

    Thirdly, investigating the possibility of a confluence hierarchy, we determine the first-order (non-)definability of the notion of confluence and related properties, using techniques from finite model theory. We find that in particular Hanf's theorem is fruitful for elegant proofs of undefinability of properties of abstract rewrite systems.

    This paper is an extended version of Decreasing Diagrams with Two Labels Are Complete for Confluence of Countable Systems (FSCD 2018).

    See research for an overview of my research on confluence.

    Bibtex

    @article{confluence:decreasing:diagrams:2020,
  title = {{Decreasing Diagrams for Confluence and Commutation}},
  author = {Endrullis, J{\"{o}}rg and Klop, Jan Willem and Overbeek, Roy},
  doi = {10.23638/LMCS-16(1:23)2020},
  journal = {{Logical Methods in Computer Science}},
  volume = {{Volume 16, Issue 1}},
  year = {2020},
  keywords = {rewriting, confluence},
  type = {journal}
}

    Digital Object Identifier

    10.23638/LMCS-16(1:23)2020
  2. Patch Graph Rewriting
    Roy Overbeek, and Jörg Endrullis
    In: Proc. Conf. on Graph Transformation (ICGT 2020), pp. 128–145, Springer (2020)
    paper

    Summary

    The basic principle of graph rewriting is the stepwise replacement of subgraphs inside a host graph. A challenge in such replacement steps is the treatment of the patch graph, consisting of those edges of the host graph that touch the subgraph, but are not part of it.

    We introduce patch graph rewriting, a visual graph rewriting language with precise formal semantics. The language has rich expressive power in two ways. First, rewrite rules can flexibly constrain the permitted shapes of patches touching matching subgraphs. Second, rules can freely transform patches. We highlight the framework’s distinguishing features by comparing it against existing approaches.

    Bibtex

    @inproceedings{graph:rewriting:patch:2020,
  author = {Overbeek, Roy and Endrullis, J{\"{o}}rg},
  title = {Patch Graph Rewriting},
  booktitle = {Proc.\ Conf.\ on Graph Transformation (ICGT~2020)},
  series = {LNCS},
  volume = {12150},
  pages = {128--145},
  publisher = {Springer},
  year = {2020},
  doi = {10.1007/978-3-030-51372-6\_8},
  keywords = {rewriting},
  type = {conference}
}

    Digital Object Identifier

    10.1007/978-3-030-51372-6_8
  3. Transducer Degrees: Atoms, Infima and Suprema
    Jörg Endrullis, Jan Willem Klop, and Rena Bakhshi
    Acta Informatica , 57 (3-5) , pp. 727–758 (2020)
    paper

    Summary

    Although finite state transducers are very natural and simple devices, surprisingly little is known about the transducibility relation they induce on streams (infinite words). We collect some intriguing problems that have been unsolved since several years. The transducibility relation arising from finite state transduction induces a partial order of stream degrees, which we call Transducer degrees, analogous to the well-known Turing degrees or degrees of unsolvability.

    We show that there are pairs of degrees without supremum and without infimum. The former result is somewhat surprising since every finite set of degrees has a supremum if we strengthen the machine model to Turing machines, but also if we weaken it to Mealy machines.

    Bibtex

    @article{streams:degrees:suprema:2020,
  author = {Endrullis, J{\"{o}}rg and Klop, Jan Willem and Bakhshi, Rena},
  title = {{Transducer Degrees: Atoms, Infima and Suprema}},
  journal = {Acta Informatica},
  volume = {57},
  number = {3-5},
  pages = {727--758},
  year = {2020},
  doi = {10.1007/s00236-019-00353-7},
  keywords = {streams, degrees, automata},
  type = {journal}
}

    Digital Object Identifier

    10.1007/s00236-019-00353-7