TERESE: TErm REwriting SEminar, June 27, 2017

This meeting on term rewriting will be held at the Technische Universiteit Eindhoven on Tuesday, June 27, 2017, in
Metaforum, floor 4, lecture room 11 (= room 4.210)
Groene Loper 5, 5612 AZ Eindhoven

How to get there?


Schedule:

time	speaker	title
13.30 - 14.10	Jasmin Blanchette (VU, Amsterdam)	New Orders for Applicative Terms and their Formalization in Isabelle/HOL
14.10 - 14.50	Florian Frohn (RWTH Aachen)	Analyzing Runtime Complexity via Innermost Runtime Complexity
14.50 - 15.30	Vincent van Oostrom (University of Innsbruck)	Critical peaks redefined: Phi union Psi = Top
15.30 - 15.50	break
15.50 - 16.30	Cynthia Kop (Copenhagen University)	Cons-free rewriting: non-determinism in implicit computational complexity
16.30 - 17.10	Hans Zantema (TU Eindhoven and RU Nijmegen)	Partial automata with exponential shortest synchronization length
17.10 - 17.30	TERESE business meeting
17.45 - ???	dinner in Restaurant Surabaya

Abstracts:

Jasmin Blanchette: New Orders for Applicative Terms and their Formalization in Isabelle/HOL
Many successful automatic theorem provers, including E, SPASS, and Vampire, are based on superposition, a first-order calculus that relies on term orders to prune the search space. We are looking into extending superposition to higher-order logic, starting with a lambda-free fragment that amounts to applicative first-order logic. We designed versions of RPO and the transfinite KBO that coincide with their first-order counterparts on curried terms that fully apply all function symbols and do not apply variables. We formalized our results in the Isabelle/HOL proof assistant, and relied on its counterexample generator Nitpick to debug our definitions. We also developed a formal library of ordinals, which we used for the transfinite KBO and in small case studies, notably a proof of Goodstein's theorem.
This is joint work with Heiko Becker, Alexander Bentkamp, Simon Cruanes, Uwe Waldmann, and Daniel Wand.

Florian Frohn: Analyzing Runtime Complexity via Innermost Runtime Complexity
There exist powerful techniques to infer upper bounds on the innermost runtime complexity of term rewrite systems (TRSs), i.e., on the lengths of rewrite sequences that follow an innermost evaluation strategy. However, the techniques to analyze the (full) runtime complexity of TRSs are substantially weaker. In this paper, we present a sufficient criterion to ensure that the runtime complexity of a TRS coincides with its innermost runtime complexity. This criterion can easily be checked automatically and it allows us to use all techniques and tools for innermost runtime complexity in order to analyze (full) runtime complexity. By extensive experiments with an implementation of our results in the tool AProVE, we show that this improves the state of the art of automated complexity analysis significantly.

Vincent van Oostrom: Critical peaks redefined: Phi union Psi = Top
We call a linear non-variable term p a pattern, and say p is a pattern in a term t if t can be written as C[p^sigma] for some context C and substitution sigma, i.e. if t encompasses p. We introduce the notion of a cluster as a term together with a set of non-overlapping patterns in it. We show that the clusters for a given term constitute a finite distributive lattice with respect to the refinement/coarsening order, and use this to give an algebraic single-line characterisation of critical (one-one) peaks: a peak s <- t -> u is critical iff the union of the respective clusters is t. The exact same characterisation applies to parallel-one peaks s <-||- t -> u, and multi-one peaks s <-o- t -> u. We show how distributivity of the lattice allows one to reason about the amount of overlap between (parallel, multi-) steps, and argue that this generalizes to other settings such as graph rewriting and higher-order rewriting.

Cynthia Kop: Cons-free rewriting: non-determinism in implicit computational complexity
The area of implicit computational complexity seeks to provide an alternative way to analyse complexity classes: rather than defining classes such as PTIME or EXPSPACE directly by their resource use, the goal of implicit complexity analysis is to define calculi or logics whose expressivity directly corresponds to some of these classes. One such methodology is cons-free programming: if functional programs are restricted to be read-only -- cons-free -- then further adding limits on data order and recursion style provides a range of characterisations in the EXPTIME and EXPSPACE hierarchies. Considering term rewriting instead of functional programming sheds an entirely new light on these characterisations, both due to its native non-determinism and the lack of a fixed reduction strategy.

Hans Zantema: Partial automata with exponential shortest synchronization length
For a DFA, a synchronizing word is a word in the input alphabet of the DFA which sends any state of the DFA to one and the same state. The length of the shortest synchronizing word for a DFA is polynomial in the DFA size: a quadratic length can be reached and a cubic upper bound has been proved. When switching to partial automata, that is for every state and symbol there is at most one outgoing arrow rather than exactly one, the situation is completely different. Based on a string rewriting system with exponential reduction length, we construct a series of partial automata each having a synchronizing word, but the size of the shortest one is exponential in the size of the automaton.
This is joint work with Michiel de Bondt en Henk Don.