Regular Tree Relations

Alexander Lochmann 📧, Bertram Felgenhauer, Christian Sternagel 🌐, René Thiemann 🌐 and Thomas Sternagel

December 15, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Regular_Tree_Relations