Edit languages for information trees

Abstract

We consider a simple set of edit operations for unordered, edge-labeled trees, called information trees by Dal Zilio et al in "A Logic You Can Count On". We define tree languages using the sheaves automata from Foster et al's "A Logic Your Typechecker Can Count On" which in turn are based on Dal Zilio et al and provide an algorithm for deciding whether a complex edit preserves membership in a tree language. This allows us to view sheaves automata and subsets of tree edits as edit languages in the sense of Hofmann et al's "Edit Lenses". They can then be used to instantiate the framework of edit lenses between such languages and model concrete examples such as synchronisation between different file systems or address directories.