Helmut Seidl and Andreas Neumann. On Guarding Nested Fixpoints. In Jörg Flum and Mario Rodríguez-Artalejo, editors, Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 484-498, Madrid, Spain, September 1999. Springer.
For every hierarchicalsystem of equations S over some complete and distributive lattice we construct an equivalent system with the same set of variables which additionally is guarded. The price to be paid is that the resulting right-hand sides may grow exponentially. We therefore present methods how the exponentialbl ow-up can be avoided. Especially, the loop structure of the variable dependence graph is taken into account. Also we prove that size O(m· S) suffices whenever S originates from a fixpoint expression where the nesting-depth of fixpoints is at most m. Finally, we sketch an application to regular tree pattern-matching.
Download: PDF Reference: Bibtex The original publication is available at www.springerlink.com