Clemens Grabmayer: Relating Proof Systems for Recursive Types (pdf (locally), thesis page/pdf (on VU-Amsterdam Research Portal)). PhD thesis, Vrije Universiteit Amsterdam, 2005.
For two process graphs on the slides of this talk (see slides 8 and 20) that are indicated as 2-exit-iterations it was claimed there that they are not in the image of the process interpretation. While these statements are irrelevant to the results reported in this talk, they are incorrect for a definition of the process interpretations by means of a TSS (transition system specification): Each of these graphs satisfies the Loop Existence and Elimination Condition LEE (see LICS 2020 article above), and each of them is the process interpretations of a (under-star-1-free) regular expression. Hereby expressibility by (1-free) regular expressions is implied by the result reported at TERMGRAPH 2024 (see above) which states that the image of (under-star-1-free) regular expressions of a compact form of the process interpretation is closed under bisimulation collapse. From the proof of that more recent result it namely follows that all collapsed process graphs with the property LEE that consist of only a single connected component are not only compact process interpretations, but indeed process interpretations of (under-star-1-free) regular expressions. This fact entails that the process graph on slide 8 is the process interpretation of a regular expression, and it can be used to show that also the process graph on slide 20 is the process interpretation of a regular expression.
This tool is a prototype implementation of the maximal-sharing operation for functional programs in the λ-calculus with letrec as defined in our ICFP 2014 paper. Following the definition of maximally shared representations of such functional programs via a ‘representation pipeline’, the tool transforms a given functional program in the Core language of the λ-calculus with letrec into a term graph, and subsequently into a deterministic finite-state automaton (DFA). It prints intermediate representations, and graphically displays the obtained DFA. This DFA is then minimized, and finally a maximally shared representation of the original program is computed as the result.
This is an animation tool for displaying and transforming port graphs (a general framework for graph transformations), and for carrying out rewrite-rule based transformations on these graphs per mouse-click. It produces beautifully rendered graphs that slowly float over the screen like bacteria in a liquid under a microscope.