# Reasoning About Recursive Tree Traversals

arXiv: https://arxiv.org/abs/1910.09521 · HTML: https://mlsanity.com/paper/1910.09521/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Oct 2019.

## Built on by (most cited first, 1 of 1)

- [Report of the Workshop on Program Synthesis for Scientific Computing](https://mlsanity.com/paper/2102.01687/) (2021)

## Abstract (arXiv)

Traversals are commonly seen in tree data structures, and performance-enhancing transformations between tree traversals are critical for many applications. Existing approaches to reasoning about tree traversals and their transformations are ad hoc, with various limitations on the class of traversals they can handle, the granularity of dependence analysis, and the types of possible transformations. We propose Retreet, a framework in which one can describe general recursive tree traversals, precisely represent iterations, schedules and dependences, and automatically check data-race-freeness and transformation correctness. The crux of the framework is a stack-based representation for iterations and an encoding to Monadic Second-Order (MSO) logic over trees. Experiments show that our framework can reason about traversals with sophisticated mutual recursion on real-world data structures such as CSS and cycletrees.