Abstract

Tree automata have good closure properties and therefore a commonly used to prove/disprove properties. This formalization contains among other things the proofs of many closure properties of tree automata (anchored) ground tree transducers and regular relations. Additionally it includes the well known pumping lemma and a lifting of the Myhill Nerode theorem for regular languages to tree languages. We want to mention the existence of a tree automata APF-entry developed by Peter Lammich. His work is based on epsilon free top-down tree automata, while this entry builds on bottom-up tree auotamta with epsilon transitions. Moreover our formalization relies on the Collections Framework, also by Peter Lammich, to obtain efficient code. All proven constructions of the closure properties are exportable using the Isabelle/HOL code generation facilities.

BibTeX

@article{Regular_Tree_Relations-AFP,
  author  = {Alexander Lochmann and Bertram Felgenhauer and Christian Sternagel and René Thiemann and Thomas Sternagel},
  title   = {Regular Tree Relations},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/Regular_Tree_Relations.html},
            Formal proof development},
  ISSN    = {2150-914x},
}