Dulma Rodriguez, An algorithm for solving constraints over regular infinite trees

An algorithm for solving constraints over regular infinite trees

In this talk we present an algorithm for solving constraints over infinite trees labelled with real numbers. The idea of the algorithm is to unfold the definition of inequality of trees in the constraints in order to obtain a set of linear arithmetic constraints equivalent to the original set of constraints. While this set is in general infinite, if we know that the tree variables in the constraints have a regular structure, we can use this fact to obtain a finite set of arithmetic constraints that we can then solve using an LP-Solver. Thus, we first try to find a regular structure for the tree variables (if this is possible) and then obtain the set of arithmetic constraints by iteratively unfolding the definition of inequality.

This work is motivated by the study of type inference for type systems for resource analysis, since the refined types we need for the analysis can be represented as infinite trees.