###
Modeling terms by graphs with structure constraints (two illustrations)

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.