Tree Set Automata for Prolog Mode Analysis (2016)
=================================================

This was a rejected submission to TTATT 2016, but was part of the work that
became chapters 4 and 5 of my :doc:`thesis <2017-thesis>`.  The
:download:`paper <2016-tsa.pdf>` is available locally. :doc:`2016-ttatt` 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:

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