Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars

Authors Jonathan Kochems, C.H. Luke Ong

Thumbnail PDF


  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Jonathan Kochems
C.H. Luke Ong

Cite AsGet BibTex

Jonathan Kochems and C.H. Luke Ong. Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 187-202, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)


The collecting semantics of a program defines the strongest static property of interest. We study the analysis of the collecting semantics of higher-order functional programs, cast as left-linear term rewriting systems. The analysis generalises functional flow analysis and the reachability problem for term rewriting systems, which are both undecidable. We present an algorithm that uses indexed linear tree grammars (ILTGs) both to describe the input set and compute the set that approximates the collecting semantics. ILTGs are equi-expressive with pushdown tree automata, and so, strictly more expressive than regular tree grammars. Our result can be seen as a refinement of Jones and Andersen's procedure, which uses regular tree grammars. The main technical innovation of our algorithm is the use of indices to capture (sets of) substitutions, thus enabling a more precise binding analysis than afforded by regular grammars. We give a simple proof of termination and soundness, and demonstrate that our method is more accurate than other approaches to functional flow and reachability analyses in the literature.
  • Flow analysis
  • reachability
  • collecting semantics
  • higher-order program
  • term rewriting
  • indexed linear tree grammar


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads