Projekt A6 - Testmengen für den universellen und existentiellen Abschluß regulärer Baumsprachen (Test sets for the universal and existential closure of regular tree languages)

(until 2001)

Finite test sets are a useful tool for deciding the membership problem for the universal closure of a given tree language, that is, for deciding whether a term has all its ground instances in the given language. A uniform test set for the universal closure must serve the following purpose: In order to decide membership of a term, it is sufficient to check whether all its test set instances belong to the underlying language.

A possible application, and our main motivation, is ground reducibility, an essential concept for many approaches to inductive reasoning. Ground reducibility modulo some rewrite system is membership in the universal closure of the set of reducible ground terms. Here, test sets always exist, and several algorithmic approaches are known. The resulting sets, however, are often unnecessarily large.

We consider regular languages and linear closure operators and prove that universal as well as existential closure, defined analogously, preserve regularity. By relating test sets to tree automata and to appropriate congruence relations, we show how to characterize, how to compute, and how to minimize ground and non-ground test sets. In particular, optimal solutions now replace previous ad hoc approximations for the ground reducibility problem.

Members:

Dieter Hofbauer

Maria Huber

Technical Reports:

Hofbauer, D. and Huber, M.:
Test Sets for the Universal and Existential Closure of Regular Tree Languages.
Mathematische Schriften Kassel 7/99, Universität-GH Kassel (42 pages), October 1999. (To appear in Information and Computation.)

Publications:

Hofbauer, D. and Huber, M.:
Test Sets for the Universal and Existential Closure of Regular Tree Languages.
Proc. of the 10th International Conference on Rewriting Techniques and Applications, RTA 99, Trento (Italy), Lecture Notes in Computer Science 1631, pages 205-219, 1999.