A Logic You Can Count On

Silvano Dal Zilio, Denis Lugiez and Charles Meyssonnier

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


We prove the decidability of the static fragment of ambient logic, with composition adjunct and iteration, which corresponds to a kind of regular expression language for semistructured data. The essence of this result is a surprising connection between formulas in the ambient logic and counting constraints on (nested) vectors of integers. Our proof method is based on a new class of tree automata for unranked, unordered trees, which may result in practical algorithms for deciding the satisfiability of a formula. A benefit of our approach is to naturally lead to an extension of the logic with recursive definitions, which is also decidable. Finally, we identify a simple syntactic restriction that improves the effectiveness of our algorithms on large examples.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:42
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems