Automating the Diagram Method to Prove Correctness of Program Transformations

TL;DR

This paper presents an automated tool that uses the diagram method, combined with unification, matching, and induction, to verify the correctness of program transformations in higher-order functional languages.

Contribution

It automates the diagram method for correctness proofs, integrating unification, matching, alpha-renaming, and termination analysis in a single tool.

Findings

Successfully automates correctness proofs for program transformations.

Demonstrates the tool's effectiveness through experiments.

Integrates multiple techniques into a unified verification framework.

Abstract

We report on the automation of a technique to prove the correctness of program transformations in higher-order program calculi which may permit recursive let-bindings as they occur in functional programming languages. A program transformation is correct if it preserves the observational semantics of programs. In our LRSX Tool the so-called diagram method is automated by combining unification, matching, and reasoning on alpha-renamings on the higher-order meta-language, and automating induction proofs via an encoding into termination problems of term rewrite systems. We explain the techniques, we illustrate the usage of the tool, and we report on experiments.

Tables

Table 1. Table 1: Statistics of executing the LRSX Tool

	# overlaps		# meta joins		# meta joins with $\alpha$-renaming		diagram computation time
	forking	answer	forking	answer	forking	answer
Calculus $L_{\mathrm{𝑛𝑒𝑒𝑑}}$ (11 SR rules, 16 transformations, 2 answers)
$\to$	2215	27	5398	27	93	0	48 secs.
$\leftarrow$	2963	38	7235	38	1399	3	116 secs.
Calculus $L_{\mathrm{𝑛𝑒𝑒𝑑}}^{+seq}$ (17 SR rules, 18 transformations, 2 answers)
$\to$	4869	29	14700	29	143	0	149 secs.
$\leftarrow$	6394	43	18046	43	2374	3	255 secs.
Calculus $\mathrm{LR}$ (76 SR rules, 43 transformations, 17 answers)
$\to$	85455	1586	389678	1586	73601	0	$\sim$ 19 hours
$\leftarrow$	105053	2280	426664	2440	93075	155	$\sim$ 16 hours

Equations

$$\begin{array}[]{@{}r@{\,}l@{\,}l@{}}x,y,z\in{{\textbf{Var}}}&::=&X\,|\,\mathsf{x}\\ \\[-10.76385pt] s,t\in\textbf{HExp}^{0}&::=&S~{}|~{}D[s]~{}|~{}{\tt letrec}~{}\mathit{env}~{}{\tt in}~{}s\ ~{}|~{}f\,r_{1}\ldots r_{\mathit{ar}(f)}\mbox{ such that }r_{i}\in\tau_{i}\text{ if }f:\tau_{1}\to\ldots\to\tau_{n}\to\textbf{Exp}\\ \\[-10.76385pt] s\in\textbf{HExp}^{n}&::=&x.s_{1}\text{ ~{}~{}if $s_{1}\in\textbf{HExp}^{n-1}$}\text{ and }n\geq 1\\ \\[-10.76385pt] b\in\textbf{Bind}&::=&x{=}s\text{ ~{}~{}where $s\in\textbf{HExp}^{0}$}\quad\hfill\mathit{env}\in\textbf{Env}::=\emptyset\,|\,E;\mathit{env}\,|\,{{\mathit{Ch}}}[x,s];\mathit{env}\,|\,b;\mathit{env}\end{array}$$

$$\begin{gathered} \gamma (\ell {\stackrel{\kappa ,n}{\to }}_{\Delta }r):=\left\{\rho (\ell )\to \rho (r)\mid \rho \text{ is ground for ℓ,r, } \\ \text{the LVC holds for ρ(ℓ),ρ(r), ρ satisfies Δ}\right\}. \end{gathered}$$

$$s_1\text{prescript}\alpha \stackrel{SR,n_2}{\to }\cdots \text{prescript}\alpha \stackrel{SR,n_k}{\to }{s}_k\text{prescript}\alpha \stackrel{\mathsf{T},n_{k+1}}{\to }\cdots \text{prescript}\alpha \stackrel{\mathsf{T},n_m}{\to }{s}_m{\sim }_{\alpha }{t}_l\stackrel{SR,n_l^{\prime }}{\leftarrow }{}_{\alpha }\cdots \stackrel{SR,n_2^{\prime }}{\leftarrow }{}_{\alpha }{t}_1$$

$$A[(\lambda X.S)T[\mathtt{letrec}{E}_1\mathtt{in}{S}^{\prime }]]\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\cdot \text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

Full text

1 Introduction

Program transformations replace program fragments by program fragments. They are applied as optimizations in compilers, in code refactoring to increase maintainability of the source code, and in verification for equational reasoning on programs. In all cases correctness of the transformations is an indispensable requirement. We focus on program calculi with a small-step operational semantics (in form of a reduction semantics with evaluation contexts, see e.g. [24]) and a notion of successfully evaluated programs. Convergence of programs holds, if the program can be evaluated to a successful program. As program equivalence we use contextual equivalence [10, 11], which holds for program fragments $P_{1}$ and $P_{2}$ if interchanging $P_{1}$ by $P_{2}$ in any program (i.e. context) is not observable w.r.t. convergence. We are particularly interested in extended lambda-calculi with call-by-need evaluation modeling the (untyped) core languages of lazy functional programming languages like Haskell (see [3, 2, 21]).

The LRSX Tool111available from http://goethe.link/LRSXTOOL61 supports correctness proofs of program transformations in those calculi by automating the “diagram method” (see e.g. [21, 16] and also [8, 23]) which was used in earlier work in non-automated pen-and-paper proofs. The diagram method is a syntactic approach that can roughly be outlined as follows. First all overlaps between standard reduction steps and transformation steps are computed, then the overlaps have to be joined resulting in a complete set of diagrams. This step is related to computing and joining critical pairs in term rewrite systems (see e.g. [4]), however, with two rewrite relations and where for one rewrite relation a strategy (defined by the standard reduction) has to be respected. Finally, the diagrams are used in an inductive proof to show correctness of the transformation.

The automation of the method is schematically depicted in Fig. 1.

The input consists of a calculus description and a set of program transformations. First the diagram calculator computes the overlaps and then tries to join them. If a complete set of diagrams is obtained, it is translated into a term rewrite system such that termination of the system implies correctness of the program transformations. The automated termination prover AProVE [6] and the certifier CeTA [22] are used to automate these steps.

In previous work, we published results on core algorithms that are used in the tool. In [19] the underlying unification-algorithm was defined and analysed, in [14, 15] a matching algorithm was developed, in [13] a procedure to alpha-rename meta-expressions was presented, and in the work [12] the encoding of the diagrams as term rewrite systems for automating the induction step was developed. However, none of these works presents the full automation of the method. Thus, in this paper, we explain core components of the automated method and illustrate the use of the LRSX Tool. In particular, we provide a formal formulation of the rewrite rules (together with some conditions) which ensure that i) the diagram method is correct and ii) the previously developed algorithms are applicable. We also illustrate how the syntax and rules of a correctness problem are represented in our tool.

Outline. In Sect. 2 we illustrate the diagram method for a simple example and thereafter briefly recall the call-by-need lambda calculus $L_{\mathit{need}}$ which will be our running example throughout the paper. In Sect. 3 we explain the meta language and the representation of the input of the diagram method. In Sect. 4 we describe the automated correctness proof for the standard cases. In Sect. 5 we discuss extensions of the automated correctness proof which are also built in the tool. Also cases which cannot be handled by the tool are discussed. In Sect. 6 we report on some experiments. We conclude in Sect. 7.

2 Illustration of the Diagram Method – Examples

We illustrate the concept of observational semantics, correctness of program transformations, and the diagram method (and its automation) using a quite simple example. In Fig. 2 we define a program calculus $\mathit{Simple}$.

The syntax of $\mathit{Simple}$-expressions consists of two constants, $\bot$ to represent a failing computation, and $\top$ to represent success, a unary operator $\neg$ for negation, and a binary operator $\wedge$ which computes the conjunction of $\top$ and $\bot$, i.e. evaluation of $e_{1}\wedge e_{2}$ results in $\top$ iff $e_{1}$ and $e_{2}$ both evaluate to $\top$ and otherwise the evaluation ends with $\bot$. The reduction strategy which evaluates the $\wedge$-operator from left to right is defined by using evaluation contexts $A$ (defined in Fig. 2 where $[\cdot]$ denotes the context hole). The standard reduction $\xrightarrow{sr}$ is the union of the rules $(sr,bot)$, $(sr,top)$, $(sr,neg1)$, and $(sr,neg2)$.

Evaluation contexts $A$ uniquely determine the position where the next standard reduction has to be applied. Hence, thus standard reduction is deterministic. Let $\xrightarrow{sr,*}$ denote the reflexive-transitive closure of $\xrightarrow{sr}$. A $\mathit{Simple}$-expression $e$ converges (written $e{\downarrow}$) iff it evaluates to $\top$, i.e. $e{\downarrow}$ iff $e\xrightarrow{sr,*}\top$. For instance, $((\neg\bot)\wedge\top)\wedge(\neg(\top\wedge\bot))\xrightarrow{sr}(\top\wedge\top)\wedge(\neg(\top\wedge\bot))\xrightarrow{sr}\top\wedge(\neg(\top\wedge\bot))\xrightarrow{sr}\neg(\top\wedge\bot)\xrightarrow{sr}\neg\bot\xrightarrow{sr}\top$.

With $C$ we denote arbitrary contexts. Expressions $e_{1},e_{2}$ are contextually equivalent, written $e_{1}\sim_{c}e_{2}$ iff $\forall C:C[e_{1}]{\downarrow}\iff C[e_{2}]{\downarrow}$. A program transformation $P$ is a binary relation on $\mathit{Simple}$-expressions and it is correct if for all $(e_{1},e_{2})\in P$, $e_{1}\sim_{c}e_{2}$ holds.

We consider the correctness proof of transformation $(top)$ which is defined in Fig. 2. Since transformation $(top)$ is already closed by all contexts (i.e. $e_{1}\xrightarrow{top}e_{2}$ implies $C[e_{1}]\xrightarrow{top}C[e_{2}]$ for all contexts $C$), it suffices to show “convergence equivalence” of the transformation, i.e.:

(1) for all $e_{1}\xrightarrow{top}e_{2}$: $e_{1}{\downarrow}\implies e_{2}{\downarrow}$ and (2) for all $e_{1}\xrightarrow{top}e_{2}$: $e_{2}{\downarrow}\implies e_{1}{\downarrow}$.

For part (1), we have to find all the cases where $e_{1}{\downarrow}$ and $e_{1}\xrightarrow{top}e_{2}$. A first case distinction is whether (i) $e_{1}$ is already successful (i.e. $e_{1}=\top$) or (ii) $e_{1}$ is reducible by the standard reduction. To systematically compute a finite representation of all cases for $e_{1}$ and $e_{2}$, we use unification and thus unify all left hand sides of rule (top) with $\top$ (for case (i)) and also with all left hand sides of all standard reductions (for case (ii)). Let us consider one of those unifications: we unify the left hand sides of $(top)$ and $(sr,bot)$. The unification problem consists of the equation $C[\top\wedge S_{1}]\doteq A[\bot\wedge S_{2}]$, where $C$ and $A$ are meta-variables for $C$- and $A$-contexts and $S_{1},S_{2}$ are meta-variables for $\mathit{Simple}$-expressions. It has two most general unifiers: either $(\top\wedge S_{1})$ is a subexpression of $S_{2}$, or $(\top\wedge S_{1})$ and $(\bot\wedge S_{2})$ are at parallel positions.

We only illustrate the former case. The unifier is $\sigma=\{S_{2}\mapsto C_{1}[\top\cap S_{1}],C\mapsto A[\bot\cap C_{1}]\}$ and the instantiated expression is $\sigma(C[\top\wedge S_{1}])=A[\bot\cap C_{1}[\top\wedge S_{1}]]=\sigma(A[\bot\wedge S_{2}])$. After instantiating the right hand sides of the rules with the unfier, we get $\sigma(C[S_{1}])=A[\bot\cap C_{1}[S_{1}]]$ and $\sigma(A[\bot])=A[\bot]$. The sequence $A[\bot]\xleftarrow{sr,bot}A[\bot\cap C_{1}[\top\wedge S_{1}]]\xrightarrow{top}A[\bot\cap C_{1}[S_{1}]]$ is called a forking overlap. It has to be joined by applying standard reductions for the right and transformation steps for the left meta-expression to find a common successor of both. If we apply a standard reduction to $A[\bot\cap C_{1}[S_{1}]]$, i.e. $A[\bot\cap C_{1}[S_{1}]]\xrightarrow{sr}A[\bot]$, we have already found a join. Note that this “application” of rules is done on meta-expressions which contain meta-variables for contexts and expressions and thus it can be done by matching the expressions against the left hand side of the transformation or standard reduction, resp.

The fork together with its join is called a forking diagram. Usually, forking diagrams are represented abstractly by removing the concrete expressions. Computing all unifiers and joins leads to the set of (abstract) diagrams shown in Fig. 4. These diagrams can be used in an inductive proof to show that if $e_{1}\xrightarrow{top}e_{2}$ then $e_{1}{\downarrow}\implies e_{2}{\downarrow}$. We use induction on the length of the reduction sequence from $e_{1}$ to $\top$. If $e_{1}$ is successful, then the claim holds. For the induction step, let $e_{1}\xrightarrow{sr}e_{1}^{\prime}$ such that $e_{1}^{\prime}{\downarrow}$. Applying a diagram to the fork $e_{1}^{\prime}\xleftarrow{sr}e_{1}\xrightarrow{top}e_{2}$ either shows that $e_{1}^{\prime}=e_{2}$, or that there exists $e_{2}^{\prime}$ with $e_{2}\xrightarrow{sr}e_{2}^{\prime}$ and either $e_{2}^{\prime}=e_{1}^{\prime}$ or $e_{1}^{\prime}\xrightarrow{top}e_{2}^{\prime}$. The induction hypothesis applied to $e_{1}^{\prime}$ shows that $e_{2}^{\prime}{\downarrow}$ and thus $e_{2}{\downarrow}$.

Part (2) of the correctness proof of transformation (top) is analogous, but we have to overlap (and also unify) the right hand side of (top) of against the successful result $\top$ and against any left hand side of a standard reduction. The obtained set of diagrams is shown in Fig. 4. The last diagram is for the case that $e\xrightarrow{top}\top$. Then also $e\xrightarrow{sr,top}\top$. This is expressed by the diagram where we added the rule $\top\xrightarrow{answer}ans$ for a new constant $ans$ (representing answers, i.e. successful results).

By induction and using the diagrams we can show that $e_{1}\xrightarrow{top}e_{2}$ and $e_{2}{\downarrow}$ also implies $e_{1}{\downarrow}$. This completes the diagram-based correctness proof for (top) and the program calculus $\mathit{Simple}$. As we explain later in Sect. 4, the induction can be automated by interpreting the diagrams as rewrite rules on their sequences of labels (where sequences of solid arrows are replaced by the sequences with dashed arrows). In Appendix B we provide the full input for the LRSX Tool that is necessary to describe the calculus $\mathit{Simple}$, the transformation (top), and to perform the automatized correctness proof of (top).

As illustrated before, the diagram computation can be done by algorithms for unification and matching, where for the $\mathit{Simple}$ calculus we require them for first-order terms extended by meta-variables for contexts. For such a language, all these parts can be implemented by known algorithms and techniques (by using some occurrence restrictions on the context variables, also efficiently, while the general problem is known to be in PSPACE [7]). However, we are interested in languages with more complicated syntactic constructs, i.e. program calculi with expressions with binders (i.e. higher-order constructs, like lambda-abstraction) and with recursive bindings (called letrec-expressions). This means, that we have to use an extended meta-language which, for instance, is capable to represent binders and letrec-expressions. That is why we from now on switch to a more complex running example, the call-by-need lambda calculus with letrec $L_{\mathit{need}}$ (see e.g. [20] for the calculus $L_{\mathit{need}}$ and e.g. [3, 2] for similar calculi). Its syntax, small-step operational semantics (called standard reduction), and the program transformations (gc1) and (gc2) to perform garbage collection, and (cp-in) and (cp-e) to copy abstractions, are shown in Fig. 5. Syntactically, $L_{\mathit{need}}$ extends the untyped lambda calculus by ${\tt letrec}$-expressions ${\tt letrec}~{}w_{1}=e_{1},\ldots,w_{n}=e_{n}~{}{\tt in}~{}e$ where the ${\tt letrec}$-environment $w_{1}=e_{1},\ldots,w_{n}=e_{n}$ represents a set of unordered bindings which have a recursive scope, i.e. the scope of $w_{i}$ are all expressions $e_{1},\ldots,e_{n}$ as well as the ${\tt in}$-expression $e$. Standard reduction implements the lazy evaluation strategy with sharing by applying small-step reduction rules at needed positions which are determined by application contexts $A$, reduction contexts $R$, and chains of ${\tt letrec}$-bindings that occur as variable-to-variable bindings and also as chains $\{w_{i}=A[w_{i+1}]\}_{i=1}^{m}$. The rule (sr,lbeta) implements $\beta$-reduction with sharing, the rules (sr,lapp), (sr,llet-in), and (sr,llet-e) reorder and join letrec-environments , the rules (sr,cp-in) and (sr,cp-e) copy abstractions into needed positions. Reduction is meant modulo (extended) $\alpha$-renaming, i.e. $\alpha$-equivalent expressions where ${\tt letrec}$-bindings are treated like a set are not distinguished.

3 Representation of Program Calculi and Transformations

The input of the diagram technique is a program calculus – with definitions of contexts, standard reduction rules, answers representing successfully evaluated programs – and a set of program transformations.

3.1 Meta-Syntax to Represent Expressions

We represent rules and answers in the meta-language LRSX (see also [19]). To cover several program calculi the representation is parametrized over a set $\mathcal{F}$ of (higher-order) function symbols and a finite set $\overline{K}$ of context classes222In the LRSX Tool the set $\overline{K}$ has to be defined explicitly while the set ${\cal F}$ is extracted from the used symbols in the input.. A context class describes a set of contexts (usually defined by a grammar), like $A$- and $C$-contexts in $\mathit{Simple}$ or in $L_{\mathit{need}}$. We define the syntax of LRSX-expressions Exp, the syntax of variables of a countably-infinite set of variables Var, the syntax of higher-order expressions of order $n$ $\textbf{HExp}^{n}$ (i.e. syntactic constructs that bind / abstract over $n$ variables, in particular $\textbf{HExp}^{0}=\textbf{Exp}$), and the syntax of environments Env and bindings Bind. We we assume that every $f\in{\cal F}$ has a syntactic type of the form $f:\tau_{1}\to\ldots\to\tau_{\mathit{ar}(f)}\to\textbf{Exp}$, where $\tau_{i}$ may be Var or $\textbf{HExp}^{k_{i}}$, i.e. the syntactic type of $f$ defines the arity of $f$, but also the syntactic category of which each argument has to be part of. If not otherwise stated, we always assume $\{{\mathtt{var}},\lambda\}\subseteq{\cal F}$ where function symbol ${\mathtt{var}}$ of type ${{\textbf{Var}}}\to\textbf{Exp}$ lifts variables to expressions, and $\lambda$ has type $\textbf{HExp}^{1}\to\textbf{Exp}$. To distinguish term variables, meta-variables, and meta-symbols, we use different fonts and lower- or upper-case letters: concrete term-variables of type Var are denoted by $\mathsf{x}$, $\mathsf{y}$, and $x,y$ are used as meta-symbols to denote a concrete term variable or a meta-variable. Similarly, $s,t$ denote expressions, $\mathit{env}$ denotes environments, and $b$ denotes bindings. Meta-variables are written in upper-case letters, where $X,Y$ are of type Var, $S$ is of type Exp, $E$ is of type Env, $D$ is a context variable, and ${{\mathit{Ch}}}$ is a two-hole environment-context variable (chain variable, for short). Each context variable $D$ has a class $\mathit{cl}(D)$ and each ${{\mathit{Ch}}}$-variable has a class $\mathit{cl}({{\mathit{Ch}}})$. The grammars for the different syntactic categories are:

[TABLE]

An LRSX-expression $s$ is ground (written as $\mathsf{s}$) iff it does not contain any meta-variable, $\mathsf{d}$ denotes a ground context and $d$ denotes contexts, that may contain meta-variables. Filling the hole of $d$ with $s$ is written as $d[s]$. Multi-contexts with $k>1$ holes are written with several hole symbols $[\cdot_{1}],\ldots,[\cdot_{k}]$.

Example 3.1**.**

The syntax of the calculus $\mathit{Simple}$ can be represented by instantiating $\mathcal{F}$ = $\{\bot,\top,\neg\}$ where $\bot,\top:\textbf{Exp}$, $\wedge:\textbf{Exp}\to\textbf{Exp}\to\textbf{Exp}$, $\neg:\textbf{Exp}\to\textbf{Exp}$ and using the context classes $\overline{K}:=\{A,C\}$ with corresponding descriptions of them (see below). Assuming that $D$ is a context variable of class $A$, the expression $D[S_{1}\wedge S_{2}]$ describes all ground expressions of the form $\mathsf{d}[\mathsf{s}_{1}\wedge\mathsf{s}_{2}]$ where $\mathsf{d}$ is a ground-context of context class $A$ and $S_{1},S_{2}$ are arbitrary ground expressions of the calculus $\mathit{Simp}$.

Example 3.2**.**

The syntax of the $\lambda$-calculus (and also of our running example $L_{\mathit{need}}$, since ${\tt letrec}$ is built-in in LRSX) can be expressed in LRSX, by the function symbols $\mathcal{F}=\{{\mathtt{var}},\lambda,{\tt app}\}$ where ${\tt app}$ is a binary function symbol of type $\textbf{Exp}\to\textbf{Exp}\to\textbf{Exp}$. The application of the identity function to itself can be written as the LRSX-expression ${\tt app}~{}(\lambda(\mathsf{x}.{\mathtt{var}}~{}\mathsf{x}))~{}(\lambda(\mathsf{x}.{\mathtt{var}}~{}\mathsf{x}))$. Lists can be represented by function symbols ${\tt nil}::\textbf{Exp}$ and ${\tt cons}::\textbf{Exp}\to\textbf{Exp}\to\textbf{Exp}$. A case-expression – usually written as ${\tt case}~{}l~{}{\tt of}~{}({\tt Nil}\to e_{1})~{}({\tt Cons}~{}\mathsf{x}~{}\mathsf{xs}\to e_{2})$ – to deconstruct lists can be represented as ${\tt caselist}~{}l~{}e_{1}~{}\mathsf{x}.\mathsf{xs}.e_{2}$ where ${\tt caselist}$ is a function symbol of type $\textbf{Exp}\to\textbf{Exp}\to\textbf{HExp}^{2}\to\textbf{Exp}$. For the context classes, we may use $\overline{K}:=\{A,T,C\}$ where $C$ are general contexts, $T$ are top-contexts (which do not have the hole inside an abstraction). Reduction contexts $R$ are not necessary since they can be expressed by $A$-contexts and several variants of the same reduction rule, for the different kinds of $R$-contexts.

In addition to a description of the syntax (by a grammar that describes a set of contexts), we require for each context class $\mathcal{K}\in\overline{K}$ a prefix and a forking table. These tables are used in the matching and unification algorithms to proceed with equations of the form $D_{1}[s_{1}]\doteq D_{2}[s_{2}]$: the prefix table is a partial function that maps pairs of classes ($\mathcal{K}_{1}$, $\mathcal{K}_{2}$) to a pair of classes ($\mathcal{K}_{3}$, $\mathcal{K}_{4}$) such that for context variables $D_{i}$ with $\mathit{cl}(D_{i})=\mathcal{K}_{i}$ an equation $D_{1}[s]\doteq D_{2}[t]$ where $D_{1}$ is a prefix of context $D_{2}$, can be replaced by the equation $s\doteq D_{4}[t]$ and the substitution $\{D_{1}\mapsto D_{3}$, $D_{2}\mapsto D_{3}[D_{4}]\}$. Undefined cases express that the prefix situation is impossible. The forking table is a partial function that maps pairs of classes ($\mathcal{K}_{1}$, $\mathcal{K}_{2}$) to a set of tuples of the form ($\mathcal{K}_{3}$, $\mathcal{K}_{4}$,$\mathcal{K}_{5}$,$d[\cdot_{1},\cdot_{2}]$) such that for context variables $D_{i}$ of class $\mathcal{K}_{i}$ an equation $D_{1}[s]\doteq D_{2}[t]$ where the paths to the holes of $D_{1}$ and $D_{2}$ fork, the equation can be removed by guessing one tuple in the set and substituting $D_{1}\mapsto D_{3}[d[D_{4}[\cdot],D_{5}[t]]],D_{2}\mapsto D_{3}[d[D_{4}[s],D_{5}[\cdot]]]$.

We do not know whether the prefix and the forking table can be computed from given grammars for the context classes. Thus, in the LRSX Tool, the user has to specify them as part of the input. For calculus $\mathit{Simple}$, the definition of these tables is shown in the Appendix B. For calculus $L_{\mathit{need}}$, we define classes for application contexts A, top contexts T and arbitrary contexts C. The definition of the former two classes as input for the LRSX Tool is shown in Fig. 6. We illustrate some exemplary entries of the prefix and forking table: the prefix table maps $(A,T)$ to $(A,T)$, since for every application context $D_{1}$ that is a prefix of a top-context $D_{2}$, we can substitute $D_{1}\mapsto D_{3}$ and $D_{2}\mapsto D_{3}[D_{4}]$ where $D_{3}$ must be an application context (since $D_{1}$ is one) and $D_{4}$ must be a top context (since $D_{2}$ is one). The prefix table maps $(T,A)$ to $(A,A)$, since for every top-context $D_{1}$ that is a prefix of an application context $D_{2}$, we can substitute $D_{1}\mapsto D_{3}$ and $D_{2}\mapsto D_{3}[D_{4}]$ where $D_{3}$ and $D_{4}$ must be application contexts to ensure that $D_{2}$ is an application context. The forking table for $(A,T)$ has only one entry $(A,A,T,\texttt{app}~{}[\cdot_{1}]~{}[\cdot_{2}])$, since an application context $D_{1}$ and a top context $D_{2}$ can only have different hole pathes, if there is an application where the hole path of $D_{1}$ goes through the first argument, while the hole path of $D_{2}$ goes through the second argument, the expression above this application must belong to application contexts (to ensure that $D_{1}$ is an application context) the context inside the first argument of the application must be an application context (again to ensure that $D_{1}$ is an application context), and the context inside the second argument must be a top context (to ensure that $D_{2}$ is a top context). For $(T,T)$ there are more entries, since the forking of two top-contexts may happen in an application or in a letrec-expression: there are two cases for the application depending on whether the hole path of the first context goes through the first or the second argument, and there are three cases for ${\tt letrec}$: the hole path of the first context may go through the ${\tt in}$-expression while the other goes through the ${\tt letrec}$-environment, or vice versa, or both hole paths go through the environment, but through different bindings. In any case the context above the two parallel holes is a top-context and the contexts below must both be top-contexts.

The semantics of meta-variables is straight-forward except for chain-variables: ${{\mathit{Ch}}}[x,s]$ with $\mathit{cl}({{\mathit{Ch}}})=\mathcal{K}$ stands for $x.\mathsf{d}[s]$ or chains $x.\mathsf{d}_{1}[({\mathtt{var}}~{}\mathsf{x}_{1})];\mathsf{x}_{1}.\mathsf{d}_{2}[({\mathtt{var}}~{}\mathsf{x}_{2})]$;$\ldots;\mathsf{x}_{n}.\mathsf{d}_{n}[s]$ with fresh $\mathsf{x}_{i}$ and contexts $\mathsf{d},\mathsf{d}_{i}$ of class $\mathcal{K}$. For expression $e$, ${\mathit{MV}}(e)$ denotes the meta-variables of $e$, ${\mathit{FV}}(e)$ denotes the free variables, ${\mathit{BV}}(e)$ denotes the bound variables, and ${\mathit{Var}}(e):={\mathit{FV}}(e)\cup{\mathit{BV}}(e)$. For a ground context $\mathsf{d}$, $\mathit{CV}(\mathsf{d})$ (the captured variables) is the set of variables $\mathsf{x}$ which become bound if plugged into the hole of $\mathsf{d}$. For environment $\mathit{env}$, ${\mathit{LV}}(\mathit{env})$ are the let-bound variables in $\mathit{env}$. Let $\sim_{\mathit{let}}$ be the reflexive-transitive closure of permuting bindings in a ${\tt letrec}$-environment, and $\sim_{\alpha}$ be the reflexive-transitive closure of combining $\sim_{\mathit{let}}$ and $\alpha$-equivalence. An LRSX-expression $s$ satisfies the let variable convention (LVC) iff a let-bound variable does not occur twice as a binder in the same ${\tt letrec}$-environment; and $s$ satisfies the distinct variable convention (DVC) iff ${\mathit{BV}}(s)$ and ${\mathit{FV}}(s)$ are disjoint and all binders bind different variables.

3.2 Rewrite Rules

The left and the right hand side of a standard reduction rule or a program transformation can be represented by LRSX-expressions. However, the rules and the transformations come with additional constraints, for instance, for the garbage collection rules, we need to express that a (part of a) letrec-environment is indeed unused and garbage. We thus constrain expressions by so-called constraint tuples:

Definition 3.3**.**

A constrained expression $(s,\Delta)$ consists of an LRSX-expression $s$ and a constraint tuple $\Delta=(\Delta_{1},\Delta_{2},\Delta_{3})$ such that $\Delta_{1}$ is a finite set of context variables, called non-empty context constraints; $\Delta_{2}$ is a finite set of environment variables, called non-empty environment constraints; and $\Delta_{3}$ is a finite set of pairs $(t,d)$ where $t$ is an LRSX-expression and $d$ is an LRSX-context, called non-capture constraints (NCCs). A ground substitution $\rho$ satisfies $\Delta$ iff $\rho(D)\not=[\cdot]$ for all $D\in\Delta_{1}$; $\rho(E)\not=\emptyset$ for all $E\in\Delta_{2}$; and ${\mathit{Var}}(\rho(t))\cap\mathit{CV}(\rho(d))=\emptyset$ for all $(t,d)\in\Delta_{3}$. The concretizations of $(s,\Delta)$ are $\gamma(s,\Delta):=\{\rho(s)\mid\rho$ is a ground substitution, $\rho(s)$ fulfills the LVC, $\rho$ satisfies $\Delta\}$333In the LRSX Tool constrained expressions are written as “$e$ where $\mathit{Constraints}$” such that $\mathit{Constraints}$ is a list of constraints, where non-empty context constraints are written as $D$ /= [.], non-empty environment constraints are written as $E$ /= {}, and non-capture constraints can occur as $(s,d)$, but also as $[\mathit{env},d]$ representing the NCC $({\tt letrec}~{}\mathit{env}~{}{\tt in}~{}c,d)$ for some constant $c$..

Example 3.4**.**

The constrained expression $(\lambda X.S,(\emptyset,\emptyset,\{(S,\lambda X.[\cdot])\}))$ represents all abstractions that do not use their argument, since the NCC $(S,\lambda X.[\cdot])$ ensures that (w.r.t. instances) the variable $X$ does not occur free in $S$. The constrained expression $({\tt letrec}~{}E~{}{\tt in}~{}S,(\emptyset,\{E\},\{(S,{\tt letrec}~{}E~{}{\tt in}~{}[\cdot])\}))$ represents all ${\tt letrec}$-expressions with a non-empty environment which is garbage: the NCC forbids references from $S$ into the environment $E$. The constrained expression $(C[{\mathtt{var}}~{}X],(\{C\},\emptyset,\{({\mathtt{var}}~{}X,C)\}))$ represents ground expressions of the form $d[{\mathtt{var}}~{}\mathsf{x}]$ where $d$ is a non-empty context and the occurrence of $\mathsf{x}$ in the context hole of $d$ is guaranteed to be a free occurrence.

We have introduced the formalisms that are required to define our representation of standard reduction rules and program transformations. We now introduce the notion of letrec rewrite rules which are rewrite rules on LRSX-expressions, constrained by a constraint tuple, and which have restrictions on the occurrences of meta-variables. The restrictions make the corresponding unification and matching problems easier to solve. Usually, the rules of a program calculus fulfill these restrictions.

Definition 3.5**.**

For $\ell,r\in\textbf{Exp}$, a constraint tuple $\Delta$, $\kappa\in\{\mathit{SR},\mathsf{T}\}$, a name $n$, we say that $\ell\xrightarrow{\kappa,n}_{\Delta}r$ is a letrec rewrite rule, if the following conditions hold: (i) ${\mathit{MV}}(\Delta)\subseteq{\mathit{MV}}(\ell)\cup{\mathit{MV}}(r)$; (ii) in each of the expressions $\ell$ and $r$, every variable of type $S$ occurs at most twice, and every variable of kind $E,{{\mathit{Ch}}}$, $D$ occurs at most once; and ${{\mathit{Ch}}}$-variables occurring in $\ell$ must occur in one ${\tt letrec}$-environment only; (iii) for any ground substitution $\rho$ that satisfies $\Delta$, $\rho(\ell)$ fulfills the LVC iff $\rho(r)$ fulfills the LVC. A letrec rewrite rule represents the set of ground rewrite rules

[TABLE]

For a set $\{\ell\xrightarrow{\kappa,n_{i}}_{\Delta}r\mid i=1,\ldots,m\}$ of letrec rewrite rules, we write $\mathsf{s}\xrightarrow{\kappa,n_{i}}\mathsf{t}$ if $(\mathsf{s}\to\mathsf{t})\in\gamma(\ell\xrightarrow{\kappa,n_{i}}_{\Delta}r)$ and $\mathsf{s}\xrightarrow{\kappa}\mathsf{t}$ if $\mathsf{s}\xrightarrow{\kappa,n_{i}}\mathsf{t}$ for some $1\leq i\leq m$. We write $\mathsf{s}\mathrel{{\prescript{}{\alpha}{\!}{\xrightarrow[]{\kappa,n_{i}}}}}\mathsf{s}^{\prime}$ if there exists $\mathsf{s}^{\prime\prime}$ such that $\mathsf{s}\sim_{\alpha}\mathsf{s}^{\prime\prime}\xrightarrow{\kappa,n_{i}}\mathsf{s}^{\prime}$.

Standard reductions are letrec rewrite rules that are always applicable to expressions which fulfill the DVC. Answers are constrained expressions which represent successful programs:

Definition 3.6**.**

A standard reduction is a letrec rewrite rule $\ell\xrightarrow{\kappa,n}_{\Delta}r$ such that the following condition holds: if for ground expressions $\mathsf{s}_{1},\mathsf{s}_{2}$ with $\mathsf{s}_{1}\xrightarrow{\mathit{SR},n}\mathsf{s}_{2}\in\gamma(\ell\xrightarrow{\!\kappa,n\!}_{\Delta}r)$, then for all ground expressions $\mathsf{t}_{1}$, such that $\mathsf{s}_{1}\sim_{\alpha}\mathsf{t}_{1}$ and $\mathsf{t}_{1}$ fulfills the DVC, there exists $\mathsf{t}_{2}\sim_{\alpha}\mathsf{s}_{2}$, such that $\mathsf{t}_{1}\xrightarrow{\!\mathit{SR},n\!}\mathsf{t}_{2}\in\gamma(\ell\xrightarrow{\!\kappa,n\!}_{\Delta}r)$. An answer set $\mathsf{Ans}$ is a finite set of constrained expressions $(t,\Delta)$ such that if $\mathsf{s}\in\gamma(t,\Delta)$, then for all $\mathsf{s^{\prime}}\sim_{\alpha}\mathsf{s}$ such that $\mathsf{s}^{\prime}$ fulfills the DVC we have $\mathsf{s}^{\prime}\in\gamma(t,\Delta)$. If $\mathsf{s}\in\gamma(t,\Delta)$ for some $(t,\Delta)\in\mathsf{Ans}$ and $\mathsf{s}^{\prime}\sim_{\alpha}\mathsf{s}$, then $\mathsf{s}^{\prime}$ is called an answer. A program calculus is a pair $({\mathsf{SR}},\mathsf{Ans})$ of a finite set of standard reductions ${\mathsf{SR}}$ and an answer set $\mathsf{Ans}$, such that whenever $\mathsf{s}\xrightarrow{\mathit{SR},n}\mathsf{s}^{\prime}$ and $\mathsf{s}$ is an answer, then also $\mathsf{s}^{\prime}$ is answer.

Example 3.7**.**

The calculus $\mathit{Simp}$ is a program calculus by instantiation the set $\mathsf{SR}$ with the standard reductions $(sr,bot),(sr,top),(sr,neg1),(sr,neg2)$ and the answer set $\mathsf{Ans}$ by $\{(\top,(\emptyset,\emptyset,\emptyset))\}$. Also the calculus $L_{\mathit{need}}$ is a program calculus where $\mathsf{Ans}:=\{(\lambda X.S,(\emptyset,\emptyset,\emptyset)),({\tt letrec}~{}E~{}{\tt in}~{}S,(\emptyset,\{E\},\emptyset))\}$ and $\mathsf{SR}$ are all standard reduction rules (partly shown in Fig. 7).

In the LRSX Tool, standard reduction $\ell\xrightarrow{\mathit{SR},n}_{\Delta}r$ is written “{SR,$n$,$k$} $\ell$ ==> $r$ where $\mathit{Constraints}$” such that $k$ is a number (the variant of the rule444In short representation of rule names, the LRSX Tool unions all variants of a rule of the same name.) and $\mathit{Constraints}$ are the constraints in $\Delta$ written as in constrained expressions. Answers are defined in the LRSX Tool by “ANSWER $e$ where $\mathit{Constraints}$.”

For the calculus $L_{\mathit{need}}$, the conditions on standard reductions hold. An excerpt of the description of $L_{\mathit{need}}$ as input of the LRSX Tool is in Fig. 7, where rules (sr,lbeta) and (sr,lapp) are expressed by three rules each, since the reduction contexts $R$ are unfolded into three cases: the reduction context is an $A$-context, the reduction context has the hole in the ${\tt in}$-part of the ${\tt letrec}$, or the hole is in the ${\tt letrec}$-environment. Chain-variables are written as Ch^K where K is the context class of the chain. Side conditions of the rules (see Fig. 5) are expressed by constraints. The last two lines define the answers in $L_{\mathit{need}}$, which are the weak head normal forms, i.e. abstractions perhaps with an outer ${\tt letrec}$.

Definition 3.8**.**

For a program calculus $({\mathsf{SR}},\mathsf{Ans})$, a ground expression $\mathsf{s}_{0}$ converges (written $\mathsf{s}_{0}{\downarrow}$) iff there exists a sequence $\mathsf{s}_{0}\mathrel{{\prescript{}{\alpha}{\!}{\xrightarrow[]{\mathit{SR}}}}}\mathsf{s}_{1}\mathrel{{\prescript{}{\alpha}{\!}{\xrightarrow[]{\mathit{SR}}}}}\cdots\mathrel{{\prescript{}{\alpha}{\!}{\xrightarrow[]{\mathit{SR}}}}}\mathsf{s}_{k}$ where $\mathsf{s}_{k}$ is an answer and $k\geq 0$. We write $\mathsf{s}\leq_{\downarrow}\mathsf{t}$ iff $\mathsf{s}{\downarrow}\implies\mathsf{t}{\downarrow}$ ($\leq_{\downarrow}$ is called convergence approximation), and $\mathsf{s}\sim_{{\downarrow}}\mathsf{t}$ iff $\mathsf{s}\leq_{\downarrow}\mathsf{t}$ and $\mathsf{t}\leq_{\downarrow}\mathsf{s}$ ($\sim_{\downarrow}$ is called convergence equivalence). If for all contexts $\mathsf{d}$ we have $\mathsf{d}[\mathsf{s}]\leq_{\downarrow}\mathsf{d}[\mathsf{t}]$, then we write $\mathsf{s}\leq_{c}\mathsf{t}$ and say that $\mathsf{t}$ contextually approximates $\mathsf{s}$. Expressions $\mathsf{s},\mathsf{t}$ are contextually equivalent ($\mathsf{s}\sim_{c}\mathsf{t}$) if $\mathsf{s}\leq_{c}\mathsf{t}$ and $\mathsf{t}\leq_{c}\mathsf{s}$.

Meta transformations are letrec rewrite rules that fulfill some form of stability w.r.t. $\alpha$-renaming. These conditions on meta transformations allow us to inspect overlaps between transformations and standard reductions or answers without considering $\alpha$-renaming steps. I.e., they guarantee that inspecting overlaps of the form $s_{1}\xleftarrow{\mathit{SR}}s_{2}\xrightarrow{T}s_{3}$ is sufficient, and hence inspecting overlaps of the form $s_{1}\mathrel{{\xleftarrow[]{\mathit{SR}}}\!_{\alpha}}s_{2}\mathrel{{\prescript{}{\alpha}{\!}{\xrightarrow[]{T}}}}s_{3}$, where the $\alpha$-renaming part of $s_{1}\mathrel{{\xleftarrow[]{\mathit{SR}}}\!_{\alpha}}s_{2}$ is non-trivial, is not necessary (see Appendix A for a soundness proof of the diagram technique which also formalizes this aspect).

Definition 3.9**.**

A letrec rewrite rule with $\kappa=\mathsf{T}$ is a meta transformation, if the following conditions hold (see also Fig. 9):

for all $\mathsf{s}_{1},\mathsf{s}_{2},\mathsf{t}_{1}$ with $\mathsf{s}_{1}\xrightarrow{\mathsf{T},n}\mathsf{s}_{2}$, $\mathsf{s}_{1}\sim_{\alpha}\mathsf{t}_{1}$, such that $\mathsf{t}_{1}$ fulfills the DVC:

1. If $\mathsf{t}_{1}\in\gamma(t,\Delta)$ for some $(t,\Delta)\in\mathsf{Ans}$, then there exists $\mathsf{s}^{\prime}_{1}\in\gamma(t,\Delta)$ such that $\mathsf{s}^{\prime}_{1}\sim_{\alpha}\mathsf{s}_{1}$ and $\mathsf{s}^{\prime}_{1}\xrightarrow{\mathsf{T},n}\mathsf{s}_{2}^{\prime}$ with $\mathsf{s}_{2}^{\prime}\sim_{\alpha}\mathsf{s}_{2}$.

2. If $\mathsf{t}_{1}\xrightarrow{\mathit{SR},n^{\prime}}\mathsf{t}_{2}$, then there exist $\mathsf{s}_{1}^{\prime}\sim_{\alpha}\mathsf{s}_{1}$, $\mathsf{s}_{2}^{\prime}\sim_{\alpha}\mathsf{s}_{2}$, $\mathsf{t}_{2}^{\prime}\sim_{\alpha}\mathsf{t}_{2}$ such that $\mathsf{s}_{1}^{\prime}\xrightarrow{\mathsf{T},n}\mathsf{s}_{2}^{\prime}$, and $\mathsf{s}_{1}^{\prime}\xrightarrow{\mathit{SR},n^{\prime}}\mathsf{t}_{2}^{\prime}$.

A meta transformation $\ell\xrightarrow{\mathsf{T},n}_{\Delta}r$ is correct iff $\gamma(\ell\xrightarrow{\mathsf{T},n}_{\Delta}r)\subseteq\sim_{c}$. A meta transformation $\ell\xrightarrow{\mathsf{T},n}_{\Delta}r$ is called overlapable if no ${{\mathit{Ch}}}$-variable occurs in $\ell$ and $r$ and the transformation is closed w.r.t. a sufficient context class for $\sim_{c}$, i.e. $\mathsf{s}\xrightarrow{\mathsf{T},n}\mathsf{t}$, $\mathsf{s}\leq_{\downarrow}\mathsf{t}$ imply $\mathsf{s}\leq_{c}\mathsf{t}$.

A sufficient criterion for Conditions (1) and (2) from Definition 3.9 is that applicability of a transformation to an expression $s$ implies applicability of the transformation to all $\alpha$-renamed expressions $s^{\prime}\sim_{\alpha}s$ that fulfill the DVC:

Proposition 3.10**.**

Let $({\mathsf{SR}},\mathsf{Ans})$ be a program calculus and $s\xrightarrow{\mathsf{T},n}_{\Delta}t$ be a letrec rewrite rule such that no ${{\mathit{Ch}}}$-variable occurs in $\ell$ and $r$ and the transformation is closed w.r.t. a sufficient context class for contextual equivalence. Assume that $\mathsf{s}_{1}\xrightarrow{\mathsf{T},n}\mathsf{s}_{2}$ implies that for all $\mathsf{s}_{1}^{\prime}\sim_{\alpha}\mathsf{s}_{1}$ such that $\mathsf{s}_{1}^{\prime}$ fulfills the DVC also $\mathsf{s}_{1}^{\prime}\xrightarrow{\mathsf{T},n}\mathsf{s}_{2}^{\prime}$ for some $\mathsf{s}_{2}^{\prime}\sim_{\alpha}\mathsf{s}_{2}$. Assume also that $\mathsf{s}_{1}\xrightarrow{\mathsf{T},n}\mathsf{s}_{2}$ for $\mathsf{s}_{1}\in\gamma(\mathsf{Ans})$ implies that for all $\mathsf{s}_{1}^{\prime}\sim_{\alpha}\mathsf{s}_{1}$ also $\mathsf{s}_{1}^{\prime}\xrightarrow{\mathsf{T},n}\mathsf{s}_{2}^{\prime}$ holds for some $\mathsf{s}_{2}^{\prime}\sim_{\alpha}\mathsf{s}_{2}$. Then $s\xrightarrow{\mathsf{T},n}_{\Delta}t$ is overlapable.

In $L_{\mathit{need}}$, the criterion holds for most of the considered transformations. An exception is the reversed copy transformation, (e.g. the reversal of $\xrightarrow{\text{cp-in}}$ in Fig. 5). It violates the criterion in Proposition 3.10, since all ground instances of the left hand side violate the DVC. However, Conditions (1) and (2) from Definition 3.9 hold, since two occurrences of $\lambda v.e$ do not forbid the application of a standard reduction.

Meta transformations $\ell\xrightarrow{\mathsf{T},n}_{\Delta}r$ are written in the LRSX Tool as “{$n$,$k$} $\ell$ ==> $r$ where $\mathit{Constraints}$” where $k$ is a non-negative integer representing the variant of the rule. For the calculus $L_{\mathit{need}}$ a context lemma [18] holds, which shows that top contexts are a sufficient class for $\sim_{c}$, thus it suffices to consider the closure of garbage collection w.r.t. top contexts. We can represent the rules for garbage collection as:

{gcT,1} T[letrec E1;E2 in S] ==> T[letrec E1 in S]

where E1 /= {}, E2 /= {}, [E1,letrec E2 in [.]], (S,letrec E2 in [.]) {gcT,2} T[letrec E in S] ==> T[S] where E /= {}, (S,letrec E in [.])

4 Computing Diagrams and Automated Induction

For proving ${\gamma(gcT)}\subseteq{\leq_{\downarrow}}$, we have to compute all overlaps between the left hand side of (gcT) and an answer (called answer overlaps555Internally, answer overlaps are computed as overlaps with rules $\ell\xrightarrow{answer}\mathit{ans}$ for $\ell\in\mathsf{Ans}$ and a new constant $\mathit{ans}$.), and between the left hand sides of (gcT) and a standard reduction (called forking overlaps)666In the LRSX Tool the commands to overlap the left hand sides with all standard reductions are overlap (gcT,1).l all and overlap (gcT,2).l all.. Clearly, computing the overlaps cannot be done using the concretizations w.r.t. $\gamma$, but has to be done on the meta-syntax, i.e. by unifying the left hand sides of the meta-transformation with the left hand sides of the standard reductions and the answers, respecting the constraint tuples corresponding to the rules. An appropriate unification algorithm for LRSX was developed in [19] and implemented in the LRSX Tool. Calling the tool produces 99 (93, resp.) overlaps of (gcT,1) ((gcT,2) resp.) with all standard reductions and answers. For joining the overlaps we have to apply standard reductions and transformation rules to the constrained expressions (again on the meta-syntax) of the overlaps until a common successor is found. For an answer $s$ and an answer overlap ${s}\xrightarrow{\mathsf{T},n^{\prime}}{t}$, a join is a sequence ${t}_{k}\mathrel{{\xleftarrow[]{\mathit{SR},n_{k}}}\!_{\alpha}}\cdots\mathrel{{\xleftarrow[]{\mathit{SR},n_{1}}}\!_{\alpha}}{t}$ where $k\geq 0$ and ${t}_{k}\in\gamma(\mathsf{Ans})$. For a forking overlap ${s}_{1}\xleftarrow{\mathit{SR},n}{t}\xrightarrow{\mathsf{T},n^{\prime}}{t}_{1}$, a join is a sequence

[TABLE]

where $m,k,l\geq 1$ and $k>1$ is only allowed if $({\mathsf{SR}},\mathsf{Ans})$ is deterministic777For each ground expression $\mathsf{s}$, there exists at most one $\mathsf{t}$ such that $\mathsf{s}\xrightarrow{\mathit{SR}}\mathsf{t}\in\gamma({\mathsf{SR}})$.. The forking overlap together with a join builds a forking diagram which can be depicted as shown in Fig. 9 (where steps from the overlap are written with solid arrows, and (existentially quantified) steps of the join are written with dashed arrows). Similarly, for an answer overlap together with its join is called an answer diagram.

Applying letrec rewrite rules uses a matching algorithm for LRSX (see [14]). A peculiarity of the matching problem is, that constrained expressions of the overlap have to be matched against meta-expressions from the rewrite rule which also come with constraint tuples. Thus the algorithm has to guarantee that the given constraints imply the needed constraints before returning a matcher. Additionally, the rewrite mechanism has to guarantee completeness w.r.t. ground instances, i.e. each rewrite step on the meta-level (applying meta rewrite rules to constrained expressions) must also be possible for all ground instances. Our tool uses an iterative and depth-bounded depth-first search to bound the number of applied transformations and reductions. Since sometimes no join is found, since a possible rewriting requires more knowledge on the (non-)emptiness of environment and context variables, the LRSX Tool uses backtracking: if no join is found for an overlap, then first a case distinction for context variables in the problem is done (whether they are empty or non-empty) and then the case distinction is done for environment variables. As a further feature, in the LRSX Tool the search space for joins can be limited: using the ignore-primitive of the tool one can forbid to use some transformations at all for the search for joins, and with the restrict-primitive the number of allowed uses of a transformation can be bounded.

For checking if a join is found, we have to test equivalence of constrained expressions. A simple check is testing $\sim_{\mathit{let}}$, but however, also the constraint tuples have to be checked. We omit the more complicated check, but in [15] a sound and complete check for proving equivalence of constrained expressions can be found. A key technique in the check is to split non-capture constraints $(s,d)$ into atomic non-capture constraints which are pairs $(u,v)$ such that $u,v$ are variables or meta-variables. The split is done by collecting the variables and meta-variables appearing in $s$ and in $d$. A ground substitution $\rho$ satisfies an atomic NCC $(u,v)$ iff ${\mathit{Var}}(\rho(u))\cap\mathit{CV\!\!}_{A}(\rho(v))=\emptyset$ where $\mathit{CV\!\!}_{A}(\mathsf{x})=\{\mathsf{x}\}$ for all variables $\mathsf{x}$ and $\mathit{CV\!\!}_{A}(r)=\mathit{CV}(r)$ for all other constructs $r$. Since $\rho$ satisfies $(s,d)$ iff it satisfies all split NCCs, the computations for checking equivalence of constraints can be done on the sets of atomic NCCs.

The join-command of the LRSX Tool tries to join the found overlaps and to compute forking and answer diagrams: The diagrams are rewrite rules where the left hand side represents the overlap and the right hand represents the join, where on both sides the diagrams are abstracted from the concrete expressions (and thus they represent string rewrite systems where the alphabet are names or reductions and transformations and the abstract symbol <-ANSWER-). For our example, the computed forking diagrams and answer diagrams (in textual representation, and condensed form) are shown in Fig. 12 and a pictorial representation of the forking diagrams is in Fig. 12. Here unions of rules are used (which are also supported in the LRSX Tool): (SR,lbeta) is the union of (SR,lbeta,1), (SR,lbeta,2), and (SR,lbeta,3). (SR,lapp) is the union of (SR,lapp,1), (SR,lapp,2), and (SR,lapp,3), (SR,cp) is the union of the rules representing (sr,cp-in) and (sr,cp-e), (SR,llet) is the union of the rules representing (sr,llet-in) and (sr,llet-e) (see Fig. 5), and (SR,lll) is the union of (SR,llet) and (SR,lapp).

In a pen-and-paper proof of $\gamma(gcT)\subseteq\leq_{\downarrow}$, an induction on the length of a converging reduction sequence $s\xrightarrow{\mathit{SR},*}s^{\prime}$ for $s$ with $s\xrightarrow{gcT}t$ is used to show that $t$ converges. The induction base is covered by the answer diagrams, and for the induction step, let $s\xrightarrow{\mathit{SR}}s_{1}\xrightarrow{\mathit{SR},*}s^{\prime}$. Applying a forking diagram to $s_{1}\xleftarrow{\mathit{SR}}s\xrightarrow{gcT}t$ shows existence of some $t^{\prime}$ with $s_{1}\xrightarrow{gcT}t^{\prime}\xleftarrow{\mathit{SR}}t$ or $s_{1}\xrightarrow{gcT}t^{\prime}=t$ and by the induction hypothesis $t^{\prime}{\downarrow}$ which also implies $t{\downarrow}$. This induction (even with more complex induction measures) can be automatized by interpreting the answer and forking diagrams as term rewrite system and by showing (innermost) termination of them (see [12]). From the obtained answer and forking diagrams for $(gcT)$, the LRSX Tool generates the term rewrite system shown in Fig. 12 which can be proved to be innermost terminating using the prover AProVE and the certifier CeTA.

5 Extended Techniques and Limitations of the Method

Our example to prove ${\gamma(gcT)}\subseteq{\leq_{\downarrow}}$ is quite simple. Unification and matching for LRSX-expressions and usual term rewrite systems for the automated induction are successful. However, the LRSX Tool provides more sophisticated techniques that are for instance required when proving the remaining part, i.e. ${\gamma(gcT)}\subseteq{\geq_{\downarrow}}$, to complete the correctness proof of garbage collection. First observe that the diagram technique works as before with the difference that the reversal of (gcT) is used (i.e. with writing $(gcT)^{-}$ for reversing the transformation $(gcT)$ we have to show $\gamma((gcT)^{-})\subseteq{\leq_{\downarrow}}$). However, this means that we have to overlap left hand sides of standard reductions and answers with right hand sides of (gcT). The obtained overlaps are called answer and commuting diagrams. Computing the overlaps results in 99 overlaps for (gcT,1) and 203 overlaps for (gcT,2). However, using the presented techniques for computing joins fails. An overlap (we omit the constraints) which cannot be joined is

[TABLE]

The automated method cannot apply a (SR,lbeta)-reduction to the upper-right expression, since it cannot infer that variable $X$ does not occur in $E_{2}$. However, this problem can be solved by $\alpha$-renaming the expression such that the DVC holds. That is why symbolic $\alpha$-renaming (see [13]) is built into the LRSX Tool which is quite more complex than usual $\alpha$-renaming, since it has to be performed on the meta syntax, e.g. internally symbolic renamings of the form $\alpha\cdot S$ are required. Even with $\alpha$-renaming, the LRSX Tool cannot join all overlaps. E.g., for the overlap (we omit the constraints)

\textstyle{A[{\tt letrec}~{}{X.S^{\prime}}~{}{\tt in}~{}S]}$$\textstyle{A[(\lambda X.S)~{}S^{\prime}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathit{SR},lbeta,1}$$\textstyle{A[({\tt letrec}~{}{E}~{}{\tt in}~{}(\lambda X.S))~{}S^{\prime}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{gcT,2}

a meta-argument is required to close the overlap stating that the standard reduction moves the environment $E$ to the top of the expression, i.e. a sequence $A[({\tt letrec}~{}{E}~{}{\tt in}~{}(\lambda X.S))~{}S^{\prime}]\xrightarrow{\mathit{SR},lll,+}{\tt letrec}~{}{E}~{}{\tt in}~{}A[(\lambda X.S))~{}S^{\prime}]$ where $\xrightarrow{\mathit{SR},lll,+}$ is the transitive closure of $\xrightarrow{\mathit{SR},lll}$. In the LRSX Tool such transitive closures can be defined and with these rules it is able to compute a complete set of commuting diagrams for the (gcT)-transformation. A pictorial representation of the commuting diagrams for $a\in\{lbeta,cp,lll\}$ is shown in Fig. 14.

The automated induction has to treat the transitive closure in the rules. A naive encoding leads to term rewrite systems with infinitely many rules. The LRSX Tool generates a term rewrite system with free variables on the right hand sides (or alternatively integer term rewrite systems, see [12, 5]) where these variables are interpreted as variables representing constructors. Every transitive closure is encoded as a guessing of the number of steps it represents. E.g., the second diagram is encoded by three term rewrite rules in Fig. 14. The termination prover AProVE and the certifier CeTA support such termination problems with free variables on right-hand sides interpreted as arbitrary constructor term. For (gcT), innermost termination can be proved and certified.

Now consider the transformations (cp-in) and (cp-e) from Fig. 5 closed by top-contexts. Computing commuting diagrams and deriving the corresponding term rewrite system results in the system

   cpT(SRlbeta(x)) -> SRlbeta(cpT(x))        cpT(SRcp(x)) -> SRcp(cpT(cpT(x)))
     cpT(SRlll(x)) -> SRlll(cpT(x))       cpT(SRlbeta(x)) -> SRcp(SRlbeta(x))
      cpT(SRcp(x)) -> SRcp(cpT(x))

which is non-terminating. If we split (cpT) into transformations where the copy target is a top-context (tcpT) and where the target is below an abstraction (dcpT), then the diagram set becomes

[TABLE]

and termination of the corresponding TRS can be proved.

We conclude this section by explaining situations for program calculi and program transformations that cannot be handled by the current version of the LRSX Tool. The underlying meta language has no support for substitutions, i.e. usual $\beta$-reduction $(\lambda x.s)~{}t\to s[t/x]$ can only be represented by encoding explicit substitutions (for instance, by using the ${\tt letrec}$-construct). Languages which use an equational theory to equate programs (for instance, structural congruence in the $\pi$-calculus [9] or in the CHF-calculus[17]) are not supported at the moment, since this would require unification and matching to handle the equational theory. Also program transformations with more complicated side-conditions (for instance, those using strictness information) can not be represented in the tool, since only rules that can be constrained the constraint tuples can be represented. Finally, the occurrence restrictions on meta-variables and the conditions on program transformations clearly forbid some program transformations. For instance, we do not allow program transformations that use chain-variables, for calculi which use chain-variables in the standard reduction rules.

6 Implementation and Experiments

The Haskell-implementation of the automated diagram method to prove correctness of program transformation is available as a Cabal-package from http://goethe.link/LRSXTOOL61. We tested our implementation with three different program calculi and a lot of program transformations. The tested calculi are the calculus $L_{\mathit{need}}$ [20] – a minimal call-by-need lambda calculus with ${\tt letrec}$ – the calculus $L_{\mathit{need}}^{+seq}$ which extends $L_{\mathit{need}}$ by the ${\tt seq}$-operator, where ${\tt seq}~{}e_{1}~{}e_{2}$ first evaluates the first argument $e_{1}$ and after obtaining a successful result it evaluates argument $e_{2}$, and the calculus $\mathrm{LR}$ [21] which extends $L_{\mathit{need}}^{+seq}$ by data constructors for lists, booleans and pairs together with corresponding case-expressions, and can be seen as an untyped core language of Haskell. The tested program transformations include all calculus reductions which can be summarized as “partial evaluation”, several copying transformations and rules for removing garbage and inlining of let-bindings which are referenced only once.

Our experimental results are in Table 1, where we also list the numbers of standard reductions, transformations, and answers in the input. The table shows the numbers of computed overlaps, corresponding joins (which is higher due to the branching in unsuccessful cases), joins which use the $\alpha$-renaming procedure. The row marked with $\to$ represent the forking diagrams, and $\leftarrow$ represent the reversed transformations, i.e. commuting diagrams. In all cases, termination of the termination problems was proved by AProVE and certified by CeTA. The last column lists the execution time888Tests ran on a system with Intel i7-4790 CPU 3.60GHz, 8 GB memory using GHC’s -N option for parallel execution for calculating the overlaps and the joins. With increasing numbers of rules, transformations, and syntactic constructs the computation time increases, due to the combinatorial explosion. The time to compute joins for commuting diagrams in $\mathrm{LR}$ is higher than for computing forking diagrams, since we put more effort in optimizing the commuting diagram computation (by avoiding unusual search paths).

7 Conclusion

We presented a system (the LRSX Tool) to automatically prove correctness of program transformations. We illustrated its use by an example and discussed peculiarities of its design and its implementation. By providing the results of experiments, we demonstrated the success of the method and the tool.

Acknowledgments. We thank René Thiemann for support on AProVE and CeTA. We also thank the anonymous reviewers of WPTE 2018 for their valuable comments.

Appendix A Soundness of the Diagram Method

We show soundness of the diagram method. Since we sometimes use slightly more general formulations of program transformations for computing joins (but not for computing overlaps), we use two sets of meta transformations. Let $({\mathsf{SR}},\mathsf{Ans})$ be a program calculus, $\mathsf{OTR}$ be a set of overlapable meta transformations, and $\mathsf{TR}\supseteq\mathsf{OTR}$ be a set of meta transformations such that for each $(\ell\xrightarrow{\!\mathsf{T},n\!}_{\Delta}r)\in\mathsf{TR}$ there exists $(\ell\xrightarrow{\!\mathsf{T},n^{\prime}\!}_{\Delta}r)\in\mathsf{OTR}$ with $\gamma(\ell\xrightarrow{\!\mathsf{T},n\!}_{\Delta}r){\subseteq}\gamma(\ell\xrightarrow{\!\mathsf{T},n^{\prime}\!}_{\Delta}r)$ (we say that $n^{\prime}$ subsumes $n$ w.r.t. $\gamma$). A set of forking and answer diagrams is complete for a set $\mathsf{OTR}$ iff for all forking overlaps of transformations in $\mathsf{OTR}$ with standard reductions and every answer overlap, an applicable diagram is in the set. Applicabilty means that the concrete overlap is an instance of the overlap described by the diagram and that the existentially quantified expressions, reductions, and transformations can accordingly be instantiated.

A set of forking and answer diagrams can be viewed as a string rewrite system (that replaces the overlap by the join). In [12] it was shown that proving termination of the string rewrite system with infinitely many rules can be automated by using termination provers for term rewrite systems to show termination of the corresponding integer term rewrite system, or term rewrite system with free variables on the right hand side that represent arbitrary constructor terms. We do not repeat this technqiue here, and formulate our soundness result in terms of the string rewrite system which is induced by the diagrams:

Theorem A.1**.**

If a complete set of forking and answer diagrams for $\mathsf{OTR}$ is terminating as a string rewrite system, then all $\ell\xrightarrow{\!\mathsf{T},n\!}_{\Delta}r\in\mathsf{TR}$ are convergence equivalent.

Proof.

Since transformations in $\mathsf{TR}$ are subsumed by the transformations in $\mathsf{OTR}$ it is sufficient to consider $\ell\xrightarrow{\mathsf{T},n}_{\Delta}r\in\mathsf{OTR}$. Assume that $\mathsf{s}\xrightarrow{\mathsf{T},n}\mathsf{t}$ and $\mathsf{s}{\downarrow}$. Then there exists a sequence $\mathsf{s}_{k}^{\prime}\sim_{\alpha}\mathsf{s}_{k}\mathrel{{\xleftarrow[]{\mathit{SR}}}\!_{\alpha}}\cdots\mathrel{{\xleftarrow[]{\mathit{SR}}}\!_{\alpha}}\mathsf{s}\xrightarrow{\mathsf{T},n}\mathsf{t}$ where $\mathsf{s}_{k}^{\prime}\in\gamma(\mathsf{Ans})$. We apply modifications to the sequence and replace overlaps by joins according to the following rules:

If the sequence contains a transformation step $\mathsf{s}_{1}\xrightarrow{\mathsf{T},n^{\prime}}\mathsf{s}_{2}$ where $\xrightarrow{\mathsf{T},n^{\prime}}_{\Delta^{\prime}}\in(\mathsf{TR}\setminus\mathsf{OTR}$), then there exists $\xrightarrow{\mathsf{T},n^{\prime\prime}}_{\Delta^{\prime\prime}}\in\mathsf{OTR}$ with $\mathsf{s}_{1}{\xrightarrow{\mathsf{T},n^{\prime}}}\mathsf{s}_{2}\in\gamma(\xrightarrow{\mathsf{T},n^{\prime\prime}}_{\Delta^{\prime\prime}})$. Replace $\mathsf{s}_{1}\xrightarrow{\mathsf{T},n^{\prime}}\mathsf{s}_{2}$ by $\mathsf{s}_{1}\xrightarrow{\mathsf{T},n^{\prime\prime}}\mathsf{s}_{2}$. 2. 2.

If the sequence contains a step $\mathsf{s}_{1}\mathrel{{\xleftarrow[]{\mathit{SR},n^{\prime}}}\!_{\alpha}}\mathsf{s}_{2}$, i.e. $\mathsf{s}_{1}\xleftarrow{\mathit{SR},n^{\prime}}\mathsf{s}_{2}^{\prime}\sim_{\alpha}\mathsf{s}_{2}$, and $\mathsf{s}_{2}^{\prime}$ does not fulfill the DVC, then replace $\mathsf{s}_{2}^{\prime}$ by an expression $\mathsf{s}_{2}^{\prime\prime}\sim_{\alpha}\mathsf{s}_{2}^{\prime}$ such that $\mathsf{s}_{2}^{\prime\prime}$ fulfills the DVC. By the definition of standard reductions, the standard reduction $\mathsf{s}_{1}^{\prime}\xleftarrow{\mathit{SR},n^{\prime}}\mathsf{s}_{2}^{\prime\prime}$ with $\mathsf{s}_{1}^{\prime}\sim_{\alpha}\mathsf{s}_{1}$ exists. Replace $\mathsf{s}_{1}\xleftarrow{\mathit{SR},n^{\prime}}\mathsf{s}_{2}^{\prime}\sim_{\alpha}\mathsf{s}_{2}$ by $\mathsf{s}_{1}\sim_{\alpha}\mathsf{s}_{1}^{\prime}\xleftarrow{\mathit{SR},n^{\prime}}\mathsf{s}_{2}^{\prime\prime}\sim_{\alpha}\mathsf{s}_{2}$. 3. 3.

If the sequence contains $\mathsf{s}_{1}\mathrel{{\xleftarrow[]{\mathit{SR}}}\!_{\alpha}}\mathsf{s}_{2}\mathrel{{\prescript{}{\alpha}{\!}{\xrightarrow[]{\mathit{SR}}}}}\mathsf{s}_{3}$, then the calculus is deterministic and thus $\mathsf{s}_{1}\sim_{\alpha}\mathsf{s}_{3}$ holds. Replace the $\mathsf{s}_{1}\mathrel{{\xleftarrow[]{\mathit{SR}}}\!_{\alpha}}\mathsf{s}_{2}\mathrel{{\prescript{}{\alpha}{\!}{\xrightarrow[]{\mathit{SR}}}}}\mathsf{s}_{3}$ by $\mathsf{s}_{1}\sim_{\alpha}\mathsf{s}_{3}$. 4. 4.

If the sequence has a prefix $\mathsf{s}_{1}\mathrel{{\prescript{}{\alpha}{\!}{\xrightarrow[]{\mathit{SR}}}}}\mathsf{s}_{3}$ where $\mathsf{s}_{1}$ is an answer, then the calculus is deterministic and $\mathsf{s}_{3}$ is an answer and we replace the prefix $\mathsf{s}_{1}\mathrel{{\prescript{}{\alpha}{\!}{\xrightarrow[]{\mathit{SR}}}}}\mathsf{s}_{3}$ by $\mathsf{s}_{3}$. 5. 5.

Subsequences $\mathsf{s}_{1}\sim_{\alpha}\mathsf{s}_{2}\sim_{\alpha}\mathsf{s}_{3}$ are replaced by $\mathsf{s}_{1}\sim_{\alpha}\mathsf{s}_{3}$. 6. 6.

If the left-most expression of the sequence is $\mathsf{s}_{1}\in\gamma(\mathsf{Ans})$ and does not fulfill the DVC, then replace $\mathsf{s}_{1}$ by $\mathsf{s}_{1}^{\prime}\sim_{\alpha}\mathsf{s}_{1}$ such that $\mathsf{s}_{1}^{\prime}$ fulfills the DVC. Due to our assumption on answers, $\mathsf{s}_{1}^{\prime}\in\gamma(\mathsf{Ans})$. 7. 7.

If the sequence has a prefix $\mathsf{t}_{1}\sim_{\alpha}\mathsf{s}_{1}\xrightarrow{\mathsf{T},n^{\prime}}\mathsf{s}_{2}$, where $\mathsf{t}_{1}$ fulfills the DVC and $\mathsf{t}_{1}\in\gamma(\mathsf{Ans})$, then first apply Condition (1) of Definition 3.9, i.e. replace the prefix by $\mathsf{t}_{1}\sim_{\alpha}\mathsf{s}_{1}^{\prime}\xrightarrow{\mathsf{T},n}\mathsf{s}_{2}^{\prime}\sim_{\alpha}\mathsf{s}_{2}$ where $\mathsf{s}_{1}^{\prime}\in\gamma(\mathsf{Ans})$ and $\mathsf{s}_{1}^{\prime}\sim_{\alpha}\mathsf{t}$. Since the set of answer diagrams is complete, there is an answer diagram that allows us to replace the answer overlap $\mathsf{s}_{1}^{\prime}\xrightarrow{\mathsf{T},n}\mathsf{s}_{2}^{\prime}$ by the corresponding join. 8. 8.

If the sequence contains $\mathsf{t}_{2}\xleftarrow{\mathit{SR},n^{\prime}}\mathsf{t}_{1}\sim_{\alpha}\mathsf{s}_{1}\xrightarrow{\mathsf{T},n^{\prime\prime}}\mathsf{s}_{2}$, then $\mathsf{t}_{1}$ fulfills the DVC (by the modification in item 2) and we can use Condition 2 of Definition 3.9 and replace $\mathsf{t}_{2}\xleftarrow{\mathit{SR},n^{\prime}}\mathsf{t}_{1}\sim_{\alpha}\mathsf{s}_{1}\xrightarrow{\mathsf{T},n^{\prime\prime}}\mathsf{s}_{2}$ by $\mathsf{t}_{2}\sim_{\alpha}\mathsf{t}_{2}^{\prime}\xleftarrow{\mathit{SR},n^{\prime}}\mathsf{s}_{1}^{\prime}\xrightarrow{\mathsf{T},n^{\prime\prime}}\mathsf{s}_{2}^{\prime}\sim_{\alpha}\mathsf{s}_{2}$. Since the set of forking diagrams is complete, we can apply a diagram in the set and replace the forking overlap $\mathsf{t}_{2}^{\prime}\xleftarrow{\mathit{SR},n^{\prime}}\mathsf{s}_{1}^{\prime}\xleftarrow{\mathsf{T},n^{\prime\prime}}\mathsf{s}_{2}^{\prime}$ by its join.

The modifications show that we can replace overlaps by joins until the sequence is of the form $\mathsf{s}_{n}\mathrel{{\xleftarrow[]{\mathit{SR}}}\!_{\alpha}}\cdots\mathrel{{\xleftarrow[]{\mathit{SR}}}\!_{\alpha}}\mathsf{t}$. Termination of the string rewrite system and the observation that $\mathrel{{\prescript{}{\alpha}{\!}{\xrightarrow[]{\mathit{SR}}}}}$-reductions which are introduced by joins can always be removed by the modifications (3) and (4), shows that the replacement together with the modifications terminates. Since, the left end of the sequence is always an expression in $\gamma(\mathsf{Ans})$, this shows $\mathsf{t}{\downarrow}$. ∎

Appendix B The Simple Example

We provide the input for the LRSX Tool for the calculus $\mathit{Simple}$ and the correctness proof of transformation (top). Note that $\bot$ is represented by bot, $\top$ by top, $\neg$ by neg, and $\wedge$ by cap (written prefix).

-- file: simple.inp -- Evaluation contexts A and arbitrary contexts C define A ::= [.] | (cap A S) | (neg A) define C ::= [.] | (cap C S) | (cap S C) | (neg C) -- The prefix table and the forking table declare prefix A A = (A,A) declare prefix A C = (A,C) declare prefix C A = (A,A) declare prefix C C = (C,C) declare fork A C = (A,A,C,(cap [.1] [.2])) declare fork C C = (C,C,C,(cap [.1] [.2])) declare fork C C = (C,C,C,(cap [.2] [.1])) declare fork C A = (A,C,A,(cap [.2] [.1])) -- standard reduction and answers {SR,bot} A[cap bot S] ==> A[bot] {SR,top} A[cap top S] ==> A[S] {SR,neg,1} A[neg top] ==> A[bot] {SR,neg,2} A[neg bot] ==> A[top] ANSWER top -- our example transformation: {top} C[cap top S] ==> C[S] -- control commands to compute the diagrams "forking_diagrams" <- overlap (top).l all "commuting_diagrams" <- overlap (top).r all -- calling -- lrsx join simple.inp -- lrsx induct atp-path=aprove/ forking_diagrams -- lrsx induct atp-path=aprove/ commuting_diagrams -- will generate the diagrams and perform the automated induction -- (it is assumed that aprove.jar and ceta are in the path specified by atp-path)