A logic you can count on

We prove the decidability of the quantifier-free, 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 of 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 on formulas that improves the effectiveness of our algorithms on large examples. Categories and Subject Descriptors: E.1 [Data Structures]: Trees; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic--modal logic; F.4.3 [Mathematical Logic and Formal Languages]: Formal...

• Type: Conference
• Year: 2004
• Where: POPL
• Authors: Silvano Dal-Zilio, Denis Lugiez, Charles Meyssonnier
• Keywords: Design General Terms, POPL 2004, Programming Languages, Regular Expression Language, Simple Syntactic Restriction