This was a rejected submission to TTATT 2016, but was part of the work that became chapters 4 and 5 of my thesis. The paper is available locally. Rigid Tree Automata With Isolation (2016) was, however, accepted to TTATT and the slides given there include an overview of this work.

Abstract:

We present our work towards a formalism useful for static analysis of pure Prolog programs. Semantically, such programs reason about trees, but the solvers actually manipulate sets of trees. Thus, at compile time we wish to circumscribe the set of possibilities—which trees may arise semantically (“type analysis”), but also which tree sets may arise procedurally (“mode analysis”). Our proposed solution is a class of automata in which each accepting path represents a set of trees. We discuss the automaton operations that arise during static analysis. We build atop rigid tree automata, which we regard as adequate for a simple Prolog type system: they permit disjunction and recursion (for algebraic data types on trees) as well as limited forms of equality constraints (enforced by repeated variables in Prolog). We then “lift” this formalism to handle tree sets. Disjunction and recursion can now capture uncertainty about the tree set, and equality encodes which Prolog variables are identical.

BibTeX:

@TechReport{filardo:treesetautomata,
  author  = {Filardo, Nathaniel Wesley and Eisner, Jason},
  title   = {Tree Set Automata for Prolog Mode Analysis},
  year    = {2016}
}