Modeling Terms by Graphs with Structure Constraints (Two Illustrations)

TL;DR

This paper demonstrates how graph techniques with structure constraints can effectively address complex problems in functional programming sharing and process semantics, offering new modeling approaches and initial promising results.

Contribution

It introduces a novel approach of modeling terms by graphs with structure constraints for problems in functional programming and process semantics.

Findings

Graph modeling improves sharing in functional programs

Approach provides insights into Milner's process semantics

Initial results show promising applications

Abstract

In the talk at the workshop my aim was to demonstrate the usefulness of graph techniques for tackling problems that have been studied predominantly as problems on the term level: increasing sharing in functional programs, and addressing questions about Milner's process semantics for regular expressions. For both situations an approach that is based on modeling terms by graphs with structure constraints has turned out to be fruitful. In this extended abstract I describe the underlying problems, give references, provide examples, indicate the chosen approaches, and compare the initial situations as well as the results that have been obtained, and some results that are being developed at present.

Equations

$$\begin{array}{rlrlrlrlrl}& \text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}25.44443pt\text{vbox}\text{vskip}2.0pt\text{nointerlineskip}\text{lower}-0.2ptto18.00003pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}-0.2pt\text{vskip}2.0pt\text{nointerlineskip}1\downarrow \text{ignorespaces}& & \text{ignorespaces}\text{ignorespaces}& & \text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}26.0pt\text{vbox}{e}_i\downarrow \text{vskip}2.0pt\text{nointerlineskip}\text{lower}-0.2ptto45.69032pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}-0.2pt\text{vskip}2.0pt\text{nointerlineskip}(e_1+e_2)\downarrow \text{ignorespaces}& & \text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}26.0pt\text{vbox}{e}_1\downarrow e_2\downarrow \text{vskip}2.0pt\text{nointerlineskip}\text{lower}-0.2ptto55.36633pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}-0.2pt\text{vskip}2.0pt\text{nointerlineskip}(e_1\cdot e_2)\downarrow \text{ignorespaces}& & \text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}26.0pt\text{vbox}\text{vskip}2.0pt\text{nointerlineskip}\text{lower}-0.2ptto28.23409pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}-0.2pt\text{vskip}2.0pt\text{nointerlineskip}(e^{\ast })\downarrow \text{ignorespaces}\end{array}$$

$$\begin{array}{rlrlrlrlrl}& \text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}24.57222pt\text{vbox}\text{vskip}2.0pt\text{nointerlineskip}\text{lower}-0.2ptto33.01614pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}-0.2pt\text{vskip}2.0pt\text{nointerlineskip}a\stackrel{a}{\to }1\text{ignorespaces}& & \text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}25.49554pt\text{vbox}{e}_i\stackrel{a}{\to }{e}_i^{\prime }\text{vskip}2.0pt\text{nointerlineskip}\text{lower}-0.2ptto51.61684pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}-0.2pt\text{vskip}2.0pt\text{nointerlineskip}{e}_1+e_2\stackrel{a}{\to }{e}_i^{\prime }\text{ignorespaces}& & \text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}25.47444pt\text{vbox}{e}_1\stackrel{a}{\to }{e}_1^{\prime }\text{vskip}2.0pt\text{nointerlineskip}\text{lower}-0.2ptto56.85088pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}-0.2pt\text{vskip}2.0pt\text{nointerlineskip}{e}_1\cdot e_2\stackrel{a}{\to }{e}_1^{\prime }\cdot e_2\text{ignorespaces}& & \text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}25.47444pt\text{vbox}{e}_1\downarrow e_2\stackrel{a}{\to }{e}_2^{\prime }\text{vskip}2.0pt\text{nointerlineskip}\text{lower}-0.2ptto71.29282pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}-0.2pt\text{vskip}2.0pt\text{nointerlineskip}{e}_1\cdot e_2\stackrel{a}{\to }{e}_2^{\prime }\text{ignorespaces}& & \text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}24.57222pt\text{vbox}e\stackrel{a}{\to }{e}^{\prime }\text{vskip}2.0pt\text{nointerlineskip}\text{lower}-0.2ptto46.61682pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}-0.2pt\text{vskip}2.0pt\text{nointerlineskip}{e}^{\ast }\stackrel{a}{\to }{e}^{\prime }\cdot e^{\ast }\text{ignorespaces}\end{array}$$

$${\partial }_{\cdot }(\cdot ):A\times RegExp(A)$$

$$⟨a,e⟩$$

$${\partial }_a(e)$$

$$(B_{\_}1)$$

$$(B_{\_}2)$$

$$(B_{\_}3)$$

$$(B_{\_}4)$$

$$\displaystyle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}({B}_{\_}5)}$$

$$(B_{\_}6)$$

$$(\text{Ref/l})$$

$$\begin{array}{r}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{leavevmode}\text{lower}25.44444pt\text{vbox}e=f\text{vskip}-2.18889pt\text{nointerlineskip}\text{lower}-0.2ptto31.96175pt\text{xleaders}\text{hrule}\text{hfill}\text{lower}2.24443ptSymm\text{vskip}-2.18887pt\text{nointerlineskip}f=e\text{ignorespaces}\end{array}$$

Full text

††terms: e††terms: e††terms: e

1 Introduction

For my talk at the workshop I prepared two examples from my past and current work that highlight the usefulness and the potential of graph techniques for problems that have been approached predominantly as questions about terms: increasing sharing in functional programs, and tackling problems about Milner’s process semantics for regular expressions. The unifying element of these two illustrations 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 illustration, which I only touched on in my talk, concerns the definition, and the efficient implementation of maximal sharing for the higher-order terms in the $\lambda$-calculus with letrec. For solving this problem, Jan Rochel and I developed a representation pipeline from terms via higher-order term graphs and first-order term graphs to deterministic finite-state automata.

The setting for the second illustration, on which I focused in my presentation, is Milner’s process semantics of regular expressions, which yields nondeterministic finite-state automata (NFAs) whose equality is studied under bisimilarity. In my current work with Wan Fokkink, I use labelings of process graphs that witness direct expressibility by a regular expression via a condition on the graph topology.

My motivation for explaining these two cases together developed as follows. While working on problems concerning the process semantics of regular expressions I have repeatedly benefited from the previous work on modeling cyclic $\lambda$-terms by structure-constrained term graphs. It turned out that many concepts and methods that Jan Rochel and I had developed could be adapted in order to define structure-constrained process graphs that directly represent regular expressions under the process semantics. It seemed worthwhile to compare the settings and the results so that the flow of ideas from one setting to the other, and probably back, might become clearer. Perhaps this can be of help in similar situations.

In this extended abstract I explain the setting and the background of the underlying problems, provide references, give examples, and informally describe the chosen approaches: in Section 2, for the implementation of maximal sharing of functional programs, and in Section 3, for the problems concerning the process semantics of regular expressions. In order to highlight differences, and to identify similarities that enabled a transferal of ideas between the two illustrations, I compare them in Section 4 with respect to the initial situation, the desired concepts, and the defined structure-constrained graphs.

2 Maximal sharing of functional programs

The first example concerns the definition, and the efficient implementation of maximal sharing for functional programs, and more specifically, for the higher-order terms in the $\lambda$-calculus with letrec [14].

Graph representations of terms in the $\lambda$-calculus with letrec are crucial for the implementation of functional programming languages, in particular for facilitating the efficient execution of compiled programs in sharing-graph form via graph reduction. However, these graph representations were never conceived as term graph representations that keep their intended meaning under bisimilarity. In fact they do not behave well under bisimilarity with respect to the unfolding semantics of terms in the $\lambda$-calculus with letrec. In order to study the compactification of functional programs (in their usual language), Jan Rochel and I therefore looked for term graph representations that support compactification under bisimilarity while preserving the intended meaning, and being easy to compute and to translate back into terms. Our focus on these desiderata (see also Figure 9 later) led us to structure-constrained term graph representations, for which we investigated a number of different options [13]. We eventually defined classes of ‘$\lambda$-higher-order-term-graphs’ and of ‘$\lambda$-term-graphs’ that are closed under functional bisimilarity and have natural correspondences with the terms in the $\lambda$-calculus with letrec (see again in Figure 9).

On this basis Jan Rochel and I developed a ‘representation pipeline’ from higher-order terms to deterministic finite-state automata (DFAs): (1) Terms in the $\lambda$-calculus with letrec can be represented by appropriately defined higher-order term graphs, which are first-order term graphs together with higher-order features such as a scope function, or an abstraction prefix function, that are defined on the set of vertices (see [13]); (2) higher-order term graphs are encoded as first-order term graphs (see also [13]), and (3) first-order term graphs are represented as DFAs (see [14]). In this way unfolding equivalence on terms is represented by bisimulation equivalence on term graphs (higher-order and first-order), and ultimately, by language equivalence of DFAs. In [14] we also define a readback operation from DFAs that arise by the representation pipeline back to terms in the $\lambda$-calculus with letrec. This operation makes it possible to go back and forth between terms and representing DFAs: it has the property that the representation via (1), (2), and (3) is the inverse of the readback operation.

Figure 1 and Figure 2 provide an example for the translation of a term in the $\lambda$-calculus with letrec into higher-order and first-order graph representations, and eventually to a finite-state automaton. Figure 1 covers the part from the syntax tree to $\lambda$-higher-order-term-graphs, and Figure 2 the remaining part via a $\lambda$-term-graph and an ‘incomplete $\lambda$-DFA’ to a ‘$\lambda$-DFA’.

In Figure 1 we start from the syntax tree of the term, model the recursive definition by a recursive backlink, replace variable names by nameless dummies that have binding backlinks to the corresponding abstraction vertices, and draw scopes. In this way we obtain first-order term graphs with scope sets that satisfy the conditions for scope sets in the concept of ‘higher-order term graph’ by Blom [7]. We call the specific version obtained here a $\lambda$-higher-order term graph with scope sets. In doing so we distinguish it from a $\lambda$-higher-order term graph with an abstraction prefix function, where scopes of abstraction vertices are recorded per vertex $v$ via the stack of those abstraction vertices in whose scope $v$ resides. See both versions of $\lambda$-higher-order term graph for the example here at the bottom of Figure 1.

In Figure 2 we start from the $\lambda$-higher-order-term-graph obtained in Figure 1, and crucially encode all scope information (recorded by the scope set, or by the abstraction prefix function) by introducing a scope vertex for the single edge in this example that crosses the boundary of a scope. We call the resulting first-order term graph a $\lambda$-term-graph. By using an intuitive correspondence of term graphs with DFAs, we translate this first-order term graph further to obtain an incomplete $\lambda$-DFA and eventually a $\lambda$-DFA, both of which represent the term $\,\lambda{x}.\,{\lambda{f}.\,{{\text{\sf let}}\;{r={{f}\hskip 1.5pt{r}}\hskip 1.5pt{x}}\;{\text{\sf in}}\;{r}}}\,$ from which we started.

Via the correspondence statements on which the representation pipeline is based, unfolding equivalence of terms in the $\lambda$-calculus with letrec can be computed in pseudo-quadratic time ${O}({n^{2}\cdot{\alpha}({n})})$ where $\alpha$ is the inverse Ackermann function (see [14]). Again via the correspondences described above, via DFA-minimization, and via the readback a maximally shared form of higher-order terms can be computed in ${O}({n^{2}\cdot\log n})$ time (again see [14]).

In order to demonstrate the maximal-sharing method as a manageable optimizing transformation for the compilation of functional programs, we developed the software tool [18] that is available on Haskell’s Hackage platform. Following the definition of maximally shared representations via the representation pipeline in [14] (see also Rochel’s thesis [19] for more context), this tool transforms a given functional program in the $\lambda$-calculus with letrec (the basis of the Core Language of the Glasgow Haskell Compiler) into a $\lambda$-term-graph, and then into a $\lambda$-DFA . It prints intermediate representations textually, and displays the obtained incomplete $\lambda$-DFA graphically. The $\lambda$-DFA is then minimized, and a maximally shared representation of the original program is computed by the readback operation as the result.

Together with Vincent van Oostrom, I have set out to generalize this technique of representing higher-order terms as term graphs with added features that are needed for modeling scopes of binding constructs. But rather than capturing the constraints on the term graph structure by ‘ad hoc’ features, we now used ‘nesting’ as the single added structuring concept. In [15] we defined, and investigated the behavioral semantics of ‘nested term graphs’ that arise as follows: by nesting first-order term graphs into the vertices of, initially, a first-order term graph, and then of nested term graphs that have already been formed.

3 Process semantics of regular expressions

The second illustration concerns the process semantics of regular expressions. Milner developed a complete axiomatization of bisimulation equivalence for finite process graphs represented in $\mu$-term notation [17] (1984). On this basis he turned to descriptions of finite process graphs by regular expressions with a unary star operation.111While regular expressions with a binary star operation were introduced by Kleene in [16] (1951), regular expressions with a unary star operation seem to have been first formulated by Copi, Elgot, and Wright [9] (1958). Also in [17] he defined a semantics $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$ for regular expressions as finite-state processes: [math] is interpreted as the deadlock process, $1$ as the immediately terminating process, letters as actions that lead to termination, and the symbols ‘$+$’, ‘$\cdot$’, and $(\cdot)^{*}$ as operators that enable choice between processes, sequential composition of processes, and iteration of a process, respectively. See Figure 4 for two examples of process interpretations of regular expressions via $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$. Formally, Milner’s definition of $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$ yields finite process graphs by an inductive definition on the structure of regular expressions.

A close variant $\llbracket{\cdot}\rrbracket^{\prime}_{\boldsymbol{P}}$ of Milner’s process semantics $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$ has later been defined via a transition system specification (TSS): the TSS ${\cal{T}}$ in Figure 3 explains the operational behavior of a regular expression (the option to do a labeled step, or to terminate) inductively for each of the constants and letters, and for each of the operators. This TSS is an adaptation for regular expressions with a unary star operation of a TSS that was formulated for regular expressions with a binary star operation by Bergstra, Bethke, and Ponse [6] (1994). By means of the TSS ${\cal{T}}$ the set ${\mathit{RegExp}}({A})$ of regular expressions over a given set $A$ of action labels is endowed with the structure of a labeled transition system (LTS) {\mathcal{L}}({\text{{\cal{T}}}}): there is an $a$-transition from $e_{1}$ to $e_{2}$ in {\mathcal{L}}({\text{{\cal{T}}}}) if and only if $e_{1}\mathrel{{\xrightarrow{a}}}e_{2}$ is provable in ${\cal{T}}$. Then the variant process interpretation $\llbracket{e}\rrbracket^{\prime}_{\boldsymbol{P}}$ of a regular expression $e$ is defined within this encompassing LTS {\mathcal{L}}({\text{{\cal{T}}}}) on ${\mathit{RegExp}}({A})$ as the LTS, or process graph, that consists of the part of {\mathcal{L}}({\text{{\cal{T}}}}) that is reachable from $e$. This process graph $\llbracket{e}\rrbracket^{\prime}_{\boldsymbol{P}}$ can be shown to be finite for every regular expression $e$. It is closely related, and in fact always bisimilar to the interpretation $\llbracket{e}\rrbracket_{\boldsymbol{P}}$ of $e$ according to Milner’s process semantics $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$.

Every labeled transition system with a finite set of vertices can be construed as a non-deterministic finite-state automaton (NFA). Therefore the process semantics $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$ for regular expressions can be viewed as a translation into NFAs whose equality is studied with respect to bisimilarity, rather than with respect to language equivalence. Indeed, Antimirov [3] (1996) arrived at the same automaton-translation for regular expressions, but without process theory and bisimulation equivalence in mind. He pursued the goal of obtaining for a given regular expression $e$, in a natural way, an NFA that accepts the language ${L}({e})$ denoted by $e$, and that is smaller than NFAs accepting ${L}({e})$ that are obtained by classical algorithms for the translation of regular expressions into NFAs. For this purpose he introduced, for regular expressions $e\in{\mathit{RegExp}}({A})$ the set of ‘partial derivatives’ ${\partial_{a}}({e})$ of $e$ with respect to letters $a\in A$, and a termination predicate . More precisely, he gave definitions by induction on the structure of regular expressions for the functions:

[TABLE]

in such a way that the following correspondences hold with respect to the transition system ${\cal{T}}$:

[TABLE]

In this way the NFA that is obtained by repeated applications of Antimirov’s partial derivatives to a regular expression $e$ coincides with the NFA that corresponds to the LTS $\llbracket{e}\rrbracket^{\prime}_{\boldsymbol{P}}$ as obtained by the TSS ${\cal{T}}$. That NFA is in turn bisimilar (as a consequence of bisimilarity of the LTSs involved as mentioned above) to the NFA that corresponds to the interpretation $\llbracket{e}\rrbracket_{\boldsymbol{P}}$ of $e$ in Milner’s process semantics.

Unlike for the standard language semantics $\llbracket{\cdot}\rrbracket_{\boldsymbol{L}}\,$, not every NFA can be expressed by a regular expression under the process interpretation $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}\,$. That is, not every NFA is bisimilar to the process translation NFA of some regular expression. This is witnessed by the two examples in Figure 5, both of which were suggested already by Milner. He showed, in [17], that the three-vertex example without termination in Figure 5 is not $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$-expressible. That the second example with two termination-permitting vertices in Figure 5 is not $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$-expressible was proved by Bosscher [8].

Still in [17], Milner adapted the complete axiomatization by Salomaa [20] for language equivalence of regular expressions. He started from a version of Salomaa’s system in which all product expressions in the axioms and rules are commuted, see Figure 6. The rule Fix is subject to the ‘non-algebraic’ side-condition that the regular expression $e$ does not have the ‘empty word property’, that is, the language interpretation $\llbracket{e}\rrbracket_{\boldsymbol{L}}$ of $e$ does not contain the empty word. This system is close to the complete axiomatization for language equivalence that was presented by Aanderaa [2] independently from Salomaa’s work (Aanderaa’s system was probably not directly known to Milner). Milner dropped the two rules from the system that are unsound under the process semantics (left-distributivity ${B}_{\_}5$, and the axiom ${B}_{\_}8$), but additionally took up the axiom $(A_{\_}{8})$ from Salomaa’s original system, which describes a correct interaction property of [math] as deadlock with process concatenation. The resulting system is sound for the process semantics $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}\,$. It has later been called $\text{\sf BPA}_{\text{\sf 0},\text{\sf 1}}^{*}$ as an adaptation of Basic Process Algebra BPA to regular expressions as terms that describe process behavior with respect to $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$.

Milner noticed that completeness for $\text{\sf BPA}_{\text{\sf 0},\text{\sf 1}}^{*}$ cannot be settled directly by Salomaa’s arguments. This is due to the incompleteness modulo bisimilarity 

$\leftrightarrow$

of the image of the process semantics $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}\,$. That namely implies that not every finite regular system of equations is solvable by a regular expression (for example, specifications that correspond to the process graphs in Figure 5 are not solvable). However, being able to solve arbitrary finite regular systems of equations by regular expressions is a crucial lemma in Salomaa’s and Aanderaa’s completeness proofs. Recognizing this difficulty, Milner formulated the question as to whether $\text{\sf BPA}_{\text{\sf 0},\text{\sf 1}}^{*}$ is indeed a complete axiomatization for bisimilarity of interpretations of regular expressions in the process semantics $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$. In addition, he also formulated the problem of characterizing those process graphs that are bisimilar to process interpretations of regular expressions, and a star-height problem for regular expressions over a single-letter alphabet.

The known approaches to these questions by Milner fall, broadly speaking, into two groups that are distinguished by how they model processes that are represented by regular expressions: either by working with process terms whose operational semantics is governed by structural operational semantics (SOS) rules, such as TSSs, or by reasoning about regular recursive process specifications of a certain structure. Taking a new approach, I have set out to use structure-constrained process graphs, see below.

Building on work from the process term tradition, Fokkink (1996-97) showed that the restriction of Milner’s system to exit-less iteration, which he called ‘perpetual-loop’ and ‘terminal cycle’, is complete for the general case with ‘empty’ 1-steps [11], and for the easier case without [12]. To achieve this result he completely overturned Salomaa’s and Aanderaa’s proof technique of extension of terms (obtaining a common extension for semantically equal terms) into its contrary, a strategy of term minimization.

Also working with term calculi for process terms, Corradini, De Nicola, and Labella [10] define a subclass of regular expressions, those without occurrences of [math] that satisfy the ‘hereditary non-empty word property (hnewp)’, and give a ‘(purely) equational’ axiomatization for $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$ on regular expressions with these restrictions. Indeed their result shows that Milner’s axiomatization without the axioms involving [math] is complete for regular expressions from that class. This is because for regular expressions with hnewp the non-equational side-condition on the fixed-point rule Fix is irrelevant, and therefore can be dropped, which turns the axiomatization into a purely equational one.

Regular expressions that may contain [math], but satisfy the property hnwep of Corradini, De Nicola, and Labella can be characterized as follows: for no iteration subexpression ${f^{*}}$ of $e$ does $\llbracket{f}\rrbracket_{\boldsymbol{P}}$ proceed to a process $p$ such that: $p$ has the option to immediately terminate, and $p$ has the option to do a proper step, and terminate later. Motivated by this, I call these expressions ‘$1$-return-less(-under-$*$)’. They turned out to be relevant in my current work on structure-constrained process graphs, see below.

Using recursive specifications to formalize processes that are induced by regular expressions, Baeten and Corradini (2005) introduced ‘well-behaved specifications’ [4]. These systems of equations are arranged according to trees with back-bindings (‘palm trees’) with a ‘loop–exit’ structure requirement. This concept enabled Baeten, Corradini, and myself to show that expressibility modulo bisimilarity of a finite process graph by a regular expression is decidable [5], although via a super-exponential procedure.

My current approach to the axiomatization problem (in work with Wan Fokkink) takes the conscious step to reasoning about process graphs for which the palm-tree form is relaxed significantly as constraint. A crucial step is the formulation of a concept of transition graph labeling that is inspired by Milner’s notion of ‘loop’. Transitions (action-labeled edges) are decorated by additional marker labels that witness that the syntax tree of a regular expression can be inscribed on to a (typically cyclic) process graph. In this way a labeling witnesses that the process graph can be expressed directly by a regular expression. This opens the way to develop bisimilarity-preserving transformations of directly expressible process graphs, in order to constructively connect any two given directly expressible process graphs that are bisimilar.

Figure 10 in Section 4 gathers the initial motivation for defining structure-constrained process graphs, and puts the desiderata here in the context of the properties of Milner’s process semantics $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$. It also gives a preliminary overview on results that are being developed at the moment.

By modifying a concept introduced by Milner in [17], we call a process graph a ‘loop’ if all paths from the start vertex return to it, and termination is only permitted at the start vertex. A ‘loop subgraph’ in a process graph $G$ is a loop that is generated from a vertex $v$ of $G$ by a set $T$ of ‘loop-entry transitions’ from $v$ as follows: the subgraph of $G$ that consists of all vertices and edges that are reachable on paths departing from $v$ via an edge in $T$ until $v$ is reached again. Furthermore we call ‘loop elimination’ a procedure that, starting from a given process graph repeatedly identifies a loop subgraph, drops its loop-entry transitions, and performs garbage collection (removing vertices and edges that have become unreachable from the start vertex). We say that a process graph $G$ satisfies the loop existence and elimination condition (LEE) if by loop elimination from $G$ a process graph without an infinite behavior (that is, without an infinite trace) can be reached.

Figure 7 in its upper row shows two loop elimination steps that are performed starting from the process graph in the middle of Figure 4. These steps lead to a process graph without any transitions, and hence without an infinite trace. Thus they witness that the original process graph has the property LEE. By contrast, none of the two process graphs in Figure 5 contains a loop subgraph: the two-vertex graph does not because the termination condition of a loop would be violated; and the three-vertex graph does not because no transition from a vertex $v$ generates a subchart in which all infinite paths return to $v$. Hence these process graphs, which are not $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$-expressible modulo 

$\leftrightarrow$

, do not satisfy the property LEE.

In its lower row, Figure 7 records a procedure of reassembly of the process graph in the upper left corner from the results that have been obtained during loop elimination. Thereby an approximation of the original process graph is assembled that is structured by $1$-transitions. We call it a structured LEE-witness. Figure 8 indicates that a LEE-witness is obtained from the structured version by overlaying the separately recorded loop subgraphs on to the original process graph, and by labeling the identified loop-entry  transitions according to the order in which they have been removed during loop elimination.

A LEE-witness records the loop elimination procedure in a process graph by marking transitions that have been recognized as loop-entry  transitions with a label that indicates its number (or nesting depth) in the procedure. It is subject to conditions that follow from this intuition, and the requirement that loop elimination leads to a process graph without an infinite trace. Thus a LEE-witness is a labeling of a process graph that is subject to appropriate conditions that witnesses that the graph satisfies LEE. In this way we obtain a class of structure-constrained process graphs that consists of all graphs that have a LEE-witness, and hence satisfy LEE. The arising class properly extends the class of process graphs that are the process semantics of some regular expression: the process graph in the middle of Figure 4 has a LEE-witness, and satisfies LEE (see Figure 7 and Figure 8), but it is not $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$-expressible.

The concept of LEE-witness is an important technical tool for investigating transformations between process graphs that satisfy the graph-topological property LEE, and for extracting regular expressions from such process graphs. It facilitates a number of results such as the following: (1) LEE is preserved under functional bisimilarity 

$\rightarrow$

for process graphs without empty steps. The proof of this statement relies on the fact that LEE -witnesses can be transferred along functional bisimulations. (2) From every process graph $G$ without $1$-transitions that satisfies LEE a 1-return-less regular expression $e$ can be extracted for which \llbracket{e}\rrbracket_{\boldsymbol{P}}\mathrel{\hbox{\kern 0.43057pt\vbox{\hbox{\raise 0.43057pt\hbox{\kern-0.43057pt{\leftrightarrow}\kern-0.43057pt}}\hrule}\kern 0.43057pt}\hskip 1.0pt}G holds, that is, such that $e$ expresses $G$ under $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$ modulo bisimilarity. This statement can be proved by using the number labels of the loop-entry transitions in a LEE-witness to define a bottom-up extraction procedure of a regular expression.

These statements lead to a new partial answer to Milner’s question about how $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$-expressibility of finite process graphs can be characterized: A finite process graph $G$ is $\llbracket{\cdot}\rrbracket_{\boldsymbol{P}}$-expressible by a 1-return-less regular expression if and only if the bisimulation collapse of $G$ satisfies the property LEE.

4 Comparison desiderata and results

Apart from demonstrating the usefulness of working with structure-constrained graphs, another motivating aim for my talk was to obtain a clearer view of the similarity and the difference of the two situations. In particular I wanted to understand why I was able to benefit from a flow of ideas from the first to the second illustration. As a first step towards a better understanding I assembled, for each of the two settings, a list of the motivations and desiderata for graph representations arising from the initial problems, and of the results that have been obtained, or that are being developed. These overviews are gathered in Figure 9 and in Figure 10.

The initial situations are markedly different: a graph semantics that is studied under bisimilarity is provided by Milner’s process semantics of regular expressions, whereas graph representations for cyclic $\lambda$-terms that are used in compilers do not behave well under bisimilarity. For representing cyclic $\lambda$-terms an appropriate class of term graph representations needed to be defined, for example one based on Blom’s higher-order term graphs [7]. Yet also the incompleteness under functional bisimilarity of the image of the process semantics stimulated extending this class of graphs to one with more satisfying properties.

The joining element of the results obtained in the two settings consists in the definition of classes of structure-constrained graphs that, on the one hand, are closed under functional bisimilarity (and hence are closed under the operation of taking the bisimulation collapse), and that, on the other hand, enable a natural, and efficiently computable correspondence with the class of terms that is relevant for the setting. This observation is highlighted in Figure 9 and Figure 10 by the items with boldface numbers: (ii) for closedness under functional bisimilarity

$\rightarrow$

, and (iii) for the natural correspondence with terms.

In conclusion I want to repeat a request that I have put to the participants of the workshop: I am interested in, and would like to hear about, other situations and settings in which structure-constrained graph representations might be useful, or have already been developed and used successfully.

Acknowledgment.

I want to thank Luca Aceto for his detailed comments and for valuable hints at substantial issues, Ruben Becker for spotting several errors and inconsistencies, Omar Inverso for a good number of concise, acute, and helpful suggestions, and Maribel Fernandez for pointing me to some structural improvements.