SToUT: Symbolic Computation Techniques for Unranked Terms

Languages over unranked alphabets attracted considerable attention in recent years because of their wide range of applications. They naturally model XML documents, program schemata, ambients, multithreaded recursive program configurations where the number of parallel processes is unbounded, variadic functions in various programming languages, etc. They appear also in the areas like rewriting, knowledge representation, program analysis and transformation, just to name a few. The unranked terms we are interested in may contain context and hedge variables, the order of arguments of some function symbols may be irrelevant, regular languages may appear in sorts or in constraints for some variables. Such a framework is rich enough to model interesting applications. Research on symbolic computation techniques (solving, proving, computing) for unranked terms does not have a long history. In this project we are concerned with the solving aspect because of its fundamental importance. In particular, we focus on two dual techniques: Unification and anti-unification. They will be studied for first-order and second-order expressions, with and without sorts, syntactically and modulo an equational theory. The general goal is to design algorithms and procedures, to analyze them, to study efficient special cases, to implement, and to apply in interesting "real-world" problems.

Unification and anti-unification are two dual symbolic computation techniques. With unification, one solves equations between the given expressions, obtaining their most general common instance. With anti-unification, one keeps similarities and abstracts over differences between the given expressions, obtaining their least general generalization. Both techniques have application areas in different fields such as automated reasoning, software engineering, artificial intelligence, bioinformatics, linguistics, etc.In the project SToUT we studied these techniques for languages with unranked alphabets and in some related formalisms. Unranked languages attracted considerable attention in recent years because of their usability in various modern applications. We developed, analyzed, and implemented algorithms for solving equations (and more general constraints) for first-order and second-order languages, where the sort information is provided either by regular expression sorts, or with the help of regular language membership constraints; anti-unification algorithms for first-order and second-order unranked languages, and in higher-order and nominal languages. A free online algorithm library has been created. Besides, we illustrated interesting applications of these techniques in programming, design theory, and bioinformatics.In summary, the SToUT project made important contributions towards the development of unification, constraint solving, and anti-unification algorithms and methods in various languages and formalisms. It also raised new research problems which we have started to investigate.