Regular Tree Relations

 

Title: Regular Tree Relations
Authors: Alexander Lochmann (alexander /dot/ lochmann /at/ uibk /dot/ ac /dot/ at), Bertram Felgenhauer, Christian Sternagel, René Thiemann and Thomas Sternagel
Submission date: 2021-12-15
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},
}
License: BSD License
Depends on: Knuth_Bendix_Order
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.