=========================================================================
From Compactifying Lambda-Letrec Terms
  to Recognizing Regular-Expression Processes
=========================================================================

I want to explain a transferal of ideas from finding graph
representations for terms in the Lambda Calculus with letrec, a universal
model of computation, to understanding process graphs that can be
expressed by regular expressions (via Milner's process interpretation),
a proper subclass of finite-state processes. In both cases structure-
constrained (term-/process-)graphs are expedient that permit to go back
and forth easily between terms/expressions and term-graphs/process-graphs.
They respect the appertaining operational semantics, but were conceived
with specific purposes in mind: to optimize functional programs in the
Lambda Calculus with letrec; and to reason with process graphs denoted
by regular expressions, and to decide recognizability of these graphs.

For the definition, and efficient implementation of maximal sharing for
the higher-order terms in the lambda calculus with letrec, Jan Rochel
and I formulated a representation-pipeline, as follows. Higher-order
terms can be represented by, appropriately defined, higher-order term
graphs, those can be encoded as first-order term graphs, and 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.

In Milner's process semantics, regular expressions are interpreted as
nondeterministic finite-state automata (NFAs) whose equality is studied
modulo bisimulation. Unlike for the standard language interpretation,
not every NFA can be expressed by a regular expression. This raised a
non-trivial recognition (or expression) problem, which was formulated
by Milner (1984) next to a completeness problem for an equational
proof system. I want to explain a crucial tool for tackling these
problems that I have developed in work with Wan Fokkink: process graphs
that are structurally constrained by the Loop Existence and Elimination
Property LEE. 
=========================================================================