Linear tree constraints were introduced by Hofmann and Rodriguez in the context of amortized resource analysis for object oriented programs. More precisely, they gave a reduction from inference of resource types to constraint solving. Thus, once we have found an algorithm to solve the constraints generated from a program, we can read off the resource consumption from their solutions.
These constraints have the form of pointwise linear inequalities between infinite trees labeled with nonnegative rational numbers. I am interested in the question if a system of such constraints is simultaneously satisfiable. Martin Hofmann and me have recently proven that the famous Skolem-Mahler-Lech problem can be reduced to this satisfiability question and identified a fragment of the tree constraint problem (UTC) that is still sufficient for program analysis. We then proved that UTC is decidable. We give a decision procedure that covers the entire range of constraints needed for resource analysis.
In my talk, I will present the decidability proof, starting with the list case, and then generalizing it to trees of arbitrary degree. If there is time, I will also focus on the estimation of asymptotic growth rates for solutions of satisfiable constraint systems.
Sabine Bauer is a Ph.D. student at the chair for theoretical computer science at LMU Munich and work on object oriented resource analysis. Before that, I was a member of the research training group ”program and model analysis” (PUMA), formerly supervised by Martin Hofmann. And before PUMA, I studied mathematics at LMU, with focus on algebra and with minor subject computer science.