Highlighting the usefulness of graph techniques for problems that have been approached predominantly as questions about terms, I want to explain two examples from my past and current work: increasing sharing in functional programs, and tackling problems about Milner's process interpretation of regular expressions. The unifying element consists in modeling terms by term graphs or transition graphs with structure constraints (higher-order features or labelings with added conditions), and in being able to go back and forth between terms and graphs.
The first example concerns the definition, and efficient implementation of maximal sharing for the higher-order terms in the lambda calculus with letrec. Jan Rochel and I showed that higher-order terms can be represented by, appropriately defined, higher-order term graphs, that those can be encoded as first-order term graphs, and that these can in turn be represented as deterministic finite-state automata (DFAs). Via these correspondences and DFA minimization, maximal shared forms of higher-order terms can be computed.
The setting for the second illustration is the process interpretation of regular expressions, which yields nondeterministic finite-state automata (NFAs) whose equality is studied under bisimulation. Unlike for the standard language interpretation, not every NFA can be expressed by a regular expression. I will explain Milner's recognizability and axiomatization problems, and some of the results/ partial results that have been obtained. Finally I will explain my current approach in work together with Wan Fokkink: inspired by Milner's notion of `loop' we use labelings of process graphs that witness direct expressibility by a regular expression.