### 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.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Session Regular_Tree_Relations

- Term_Context
- Basic_Utils
- Ground_Terms
- FSet_Utils
- Ground_Ctxt
- Ground_Closure
- Horn_Inference
- Horn_List
- Horn_Fset
- Tree_Automata
- Tree_Automata_Det
- Tree_Automata_Complement
- Tree_Automata_Pumping
- Myhill_Nerode
- GTT
- GTT_Compose
- GTT_Transitive_Closure
- Pair_Automaton
- AGTT
- RRn_Automata
- RR2_Infinite
- Tree_Automata_Abstract_Impl
- Tree_Automata_Class_Instances_Impl
- Tree_Automata_Impl
- RR2_Infinite_Q_infinity
- Regular_Relation_Abstract_Impl
- Regular_Relation_Impl

### Depends on

- A Formalization of Knuth–Bendix Orders

### Used by

- Reducing Rewrite Properties to Properties on Ground Terms
- First-Order Theory of Rewriting

### Auto-related entries

- The Myhill-Nerode Theorem Based on Regular Expressions
- Tree Automata

## Cite

×

Regular_Tree_Relations-AFP

    @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   = {December},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Regular_Tree_Relations.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 29, 2021 : Isabelle2021-1