# Rewriting Higher-order Stack Trees

- 11:00 18th May 2016 ( week 4th Week, Trinity Term 2016 )Lecture Theatre B, Wolfson Building, Parks Road

Higher-order pushdown systems and ground tree rewriting systems can be

seen as extensions of suffix word rewriting systems. Both classes

generate infinite graphs with interesting logical properties. Indeed,

the satisfaction of any formula written in monadic second order logic

(respectively first order logic with reachability predicates) can be

decided on such a graph.

The purpose of this talk is to propose a common extension to both

higher-order stack operations and ground tree rewriting. We introduce a model

of higher-order ground tree rewriting over trees labelled by

higher-order stacks (henceforth called stack trees), which syntactically

coincides with ordinary ground tree rewriting at order 1 and with the dynamics

of higher-order pushdown automata over unary trees. The infinite

graphs generated by this class have a decidable first order logic with

reachability.

Formally, an order n stack tree is a tree labelled by order n-1 stacks.

Operations of ground stack tree rewriting are represented by a certain class

of connected DAGs labelled by a set of basic operations over stack trees

describing of the relative application positions of the basic

operations appearing on it. Applying a DAG to a stack tree t intuitively

amounts to paste its input vertices to some leaves of t and to simplify

the obtained structure, applying the basic operations labelling the edges of the

DAG to the leaves they are appended to, until either a new stack tree is

obtained or the process fails, in which case the application of the DAG to t

at the chosen position is deemed impossible. This model is a common extension

to those of higher-order stack operations presented by Carayol and of

ground tree

transducers presented by Dauchet and Tison.

As further results we can define a notion of recognisable sets of

operations through a generalisation. The proof that the graphs generated

by a ground stack tree rewriting system have a decidable first order theory

with reachability is inspired by the technique of finite set interpretations

presented by Colcombet and Loding.