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

TL;DR

This work connects two domains—the lambda-calculus with letrec and Milner's process semantics for regular expressions—through the lens of structure-constrained graphs. It develops a pipeline of graph representations, including $ ext{λ-ho-term-graphs}$ and their first-order encodings, to achieve maximal sharing and faithful unfoldings, and characterizes expressibility of infinite terms via strong regularity. It analyzes process semantics, identifies incompleteness, and introduces the Loop Existence and Elimination (LEE) and layered LLEE criteria, together with the crystallization approach, to advance axiomatization and completeness results. The future directions target runtime maximal sharing, interaction-net implementations, and formal verification of crystallization to tackle full expressibility problems, with potential polynomial-time decidability results for restricted cases. These contributions offer practical techniques for compact representations and a deeper theoretical understanding of expressibility and bisimilarity in term- and process-graphs.

Abstract

As a supplement to my talk at the workshop, this extended abstract motivates and summarizes my work with co-authors on problems in two separate areas: first, in the lambda-calculus with letrec, a universal model of computation, and second, on Milner's process interpretation of regular expressions, a proper subclass of the finite-state processes. The aim of my talk was to motivate a transferal of ideas for workable concepts of structure-constrained graphs: from the problem of finding compact graph representations for terms in the lambda-calculus with letrec to the problem of recognizing finite process graphs that can be expressed by regular expressions. In both cases the construction of structure-constrained graphs was expedient in order to enable to go back and forth easily between, in the first case, lambda-terms and term graphs, and in the second case, regular expressions and process graphs. The main focus here is on providing pointers to my work with co-authors, in both areas separately. A secondary focus is on explaining directions of my present projects, and describing research questions of possibly general interest that have developed out of my work in these two areas.

Figures (7)

• Figure 5: Transition system specification $\text{${\cal{T}}$}$ for computations enabled by regular expressions.
• Figure 6: Two process graphs $G_{1}$ and $G_{2}$ that are $P$-expressible, and hence $\llbracket{\cdot}\rrbracket_{\space P}$-expressible, because they are the process interpretations of regular expressions as indicated. $G_{1}$ and $G_{2}$ are bisimilar via bisimulations that are drawn as links $\space$ to their joint bisimulation collapse $G_{0}$ (of which $P$-ex-pres-si-bi-lity is at first unclear). It follows that also $G_{0}$ is $\llbracket{\cdot}\rrbracket_{\space P}$-expressible, and that process semantics equality holds between the regular expressions with interpretations $G_{1}$ and $G_{2}$, respectively. In this example $G_{0}$ is actually also in the image of ${P}(\space{\cdot}\space)$, hence $P$-expressible, as witnessed for example by $G_{0} = {P}(\space{((1 \cdot a) \cdot (a \cdot (b + b \cdot a))^*) \cdot 0}\space)$.
• Figure 7: On the left: Two process graphs that are neither ${P}(\space{\cdot}\space)$-expressible (that is, not in the image of the process interpretation $P$) nor $\llbracket{\cdot}\rrbracket_{\space P}$-expressible (that is, not bisimilar to the process interpretation of any regular expression). On the right: two regular expressions with the same language semantics (associated language) but different process semantics, since the process interpretations are not bisimilar; therefore right-distributivity does not hold for $=_{{ \llbracket{\cdot}\rrbracket_{\space P}}}$, which entails that fewer identities hold for $=_{{ \llbracket{\cdot}\rrbracket_{\space P}}}$ than for ${=_{ \llbracket{\cdot}\rrbracket_{L}}}$.
• Figure 8: Milner's equational proof system Mil for process semantics equality $\mathrel{=_{{ \llbracket{\cdot}\rrbracket_{\space P}}}}$ of regular expressions with the fixed-point rule $\textrm{\normalfont RSP}^{*}\space$ in addition to the (not shown) basic rules for reasoning with equations (which guarantee that derivability in Mil is a congruence relation). From Mil the complete proof system for language equivalence ${=_{ \llbracket{\cdot}\rrbracket_{L}}}$ due to Aanderaa arises by adding the axioms $e \mathrel{\cdot} (f + g) = e \mathrel{\cdot} f + e \mathrel{\cdot} g$ and $e \mathrel{\cdot} 0 = 0$ (which are not sound for $\mathrel{=_{{ \llbracket{\cdot}\rrbracket_{\space P}}}}$) and by dropping $\text{\normalfont{(A9)}}$ (which then is derivable).
• Figure 9: Four process graphs (action labels ignored) that violate at least one loop graph condition \ref{['LG:1']}, \ref{['LG:2']}, or \ref{['LG:3']}, and a loop graph $\textit{LG}$ with one of its loop subgraph $\textcolor{darkcyan}{LG_{2}}$.