Session 5A

Chair: Maribel Fernandez

• 14:30: Rick Erkens, Maurice Laveaux. Adaptive Non-linear Pattern Matching Automata.     See abstract ...
  ABSTRACT. Efficient pattern matching is fundamental for practical term rewrite engines. By preprocessing the given patterns into a finite deterministic automaton the matching patterns can be decided in a single traversal of the relevant parts of the input term. Most automaton-based techniques are restricted to linear patterns, where each variable occurs at most once, and require an additional post-processing step to check so-called variable consistency. However, we can show that interleaving the variable consistency and pattern matching phases can reduce the number of required steps to find a match. We take the existing adaptive pattern matching automata as introduced by Sekar et al and extend it with consistency checks. We prove that the resulting deterministic pattern matching automaton is correct, and that its evaluation time is more efficient than two-phase approaches.
• 15:00: Kazuyuki Asada, Naoki Kobayashi. Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars.     See abstract ...
  ABSTRACT. Higher-order grammars have recently been studied actively in the context of automated verification of higher-order programs. Asada and Kobayashi have previously shown that, for any order-(n+1) word grammar, there exists an order-n grammar whose frontier language coincides with the language generated by the word grammar. Their translation, however, blows up the size of the input word grammar, which inhibited complexity-preserving reductions from decision problems on word grammars to those on tree grammars. In this paper, we present a new translation from order-(n+1) word grammars to order-n tree grammars that is size-preserving in the sense that the size of the output tree grammar is polynomial in the size of an input tree grammar. The new translation and its correctness proof are arguably much simpler than the previous translation and proof.
• 15:30: David Cerna, Temur Kutsia. Unital Anti-unification: Type and Algorithms.     See abstract ...
  ABSTRACT. Unital theories are characterized by the property of some function symbols having (left and right) unit elements. We address three problems related to unital anti-unification (AU). First, we prove that when the term signature contains at least two unital functions, anti-unification is of type zero (nullary) by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant (computed generalizations are linear) and one-unital fragment (the problems are formulated over a language with one unital symbol) and design AU algorithms for them. The algorithms are terminating, sound, complete and return tree grammars from which set of generalizations can be constructed. For the linear variant, the language of generalizations generated by the grammar is finite. In the one-unital fragment, the language might be infinite, but it contains a finite minimal complete set of generalizations. It means that both linear and one-unital AU are finitary. We also design an AU algorithm for the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations.
  This nullarity proof can be extended to other equational theories such as associative-unital, commutative-unital, and their combination, when multiple function symbols may have these properties. However, our argument fails for idempotent-unital theories. We end with a list of open questions derived from this as well as earlier work.
• 16:00: Andrej Dudenhefner. Undecidability of Semi-unification on a Napkin *** Best paper by a junior researcher.     See abstract ...
  ABSTRACT. Semi-unification (unification combined with matching) has been proven undecidable by Kfoury, Tiuryn, and Urzyczyn in the 1990s. The original argument reduces Turing machine immortality via Turing machine boundedness to semi-unification. The latter part is technically most challenging, involving several intermediate models of computation.
  This work presents a novel, simpler reduction from Turing machine boundedness to semi-unification. In contrast to the original argument, we directly translate boundedness to solutions of semi-unification and vice versa. In addition, the reduction is mechanized in the Coq proof assistant. Taking advantage of the simpler proof, the mechanization is comparatively short and fully constructive.