Email Gateway (Dec 29 2021 at 12:14): Email Gateway (Dec 29 2021 at 12:14):From: Tobias Nipkow <nipkow@in.tum.de>
Regular Tree Relations
Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann and
Thomas Sternagel
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.
https://www.isa-afp.org/entries/Regular_Tree_Relations.html
Enjoy!
smime.p7s
Last updated: Jul 15 2022 at 23:21 UTC