{'fraction_non_alphanumeric': 0.03800537662748405, 'fraction_numerical': 0.008881977755521585, 'mean_word_length': 4.224149800357979, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Repeated Recursion Unfolding for Super-Linear Speedup within Bounds

Repeated recursion unfolding is a new approach that repeatedly unfolds a recursion with itself and simplifies it while keeping all unfolded rules. Each unfolding doubles the number of recursive steps covered. This reduces the number of recursive rule applications to its logarithm at the expense of introducing a logarithmic number of unfolded rules to the program. Efficiency crucially depends on the amount of simplification inside the unfolded rules. We prove a super-linear speedup theorem in the best case, i.e. speedup by more than a constant factor. Our optimization can lower the time complexity class of a program. In this paper, the super-linear speedup is within bounds: it holds up to an arbitrary but chosen upper bound on the number of recursive steps. We also report on the first results with a prototype implementation of repeated recursion unfolding. A simple program transformation completely removes recursion up to the chosen bound. The actual runtime improvement quickly reaches several orders of magnitude.


Introduction
In the context of rule-based and logic programming, unfolding is the program transformation that replaces a call (goal) in the body of a rule by the body of a rule whose head is matched by the goal. This saves a rule application at runtime. More importantly, the resulting code can be simplified for efficiency.
Head, guard and body of a rule are separated by ⇔ and |, respectively. The rules can be understood as a procedure definition for sum, each rule covering a case. When a call matches the head of a rule and the guard condition holds, the body of the rule is executed. In CHR code, upper case letters stand for logical variables.
Note that this rule r 1 cannot replace the original recursive rule because it only applies in case N > 2. It behaves like applying the original rule r 0 twice. It saves computation time, because we only need about half as many recursive steps as with the original rule alone. Since the simplification of the unfolded rule results in code of similar size and time complexity as the original rule, we can expect to halve the runtime. If we would now unfold the recursive goal in rule r 1 with rule r 0 we have unfolded thrice overall. We can expect a speedup of roughly three times if we replace r 1 by the new rule. But we can do even better than that if we keep rule r 1 and unfold rule r 1 with itself. The resulting rule after simplification is r 2 : sum(N, S) ⇔ N > 4 | S := 4 * N −6 + S1, sum(N −4, S1).
This rule results in a four-fold speedup.
We can repeat this process: unfolding the newly generated recursive rule with itself until we reach a given upper bound. We never unfold with the base case. It is ignored. This is what we call repeated recursion unfolding. With each unfolding, the number of original recursive steps simplified into one recursive step of the unfolded rule will double.
Given n recursive steps with the original rule and log 2 (n) unfolded rules according to our scheme, it is possible to have at most log 2 (n) recursive rule applications instead of n. If the unfolded rules take not more time than the original recursive rule, the time complexity class can be lowered and superlinear speedup in runtime can be achieved.
For our scheme to work, we always have to apply the best, most unfolded rule. To implement this behavior, we use another program transformation that removes the recursion altogether. We call this recursionless recursion.
Overview of the Paper. Section 2 introduces syntax and semantics of the CHR programming language using a single state transition.
Section 3 defines our program transformation scheme of repeated recursion unfolding with simplification and proves its correctness. We will use summation as our running example.
Section 4 proves that there exists a simple optimal rule application strategy for unfolded recursions with best-case simplification that results in super-linear speedup by lowering the time complexity classes by a factor of up to O(n).
Section 5 introduces recursionless recursion, a transformation that provides a semi-naive implementation of optimal rule applications. We prove that the worst-case overhead of this scheme is linear in the number of unfolded rules.
In Section 6 we conclude our summation example with benchmarks in our prototype implementation. It improves time complexity from linear to constant. Another example, naive list reversal, improves from quadratic to linear complexity. It runs faster than the hand-optimized built-in list reversal in Prolog, the implementation language of CHR.
Finally, we discuss related work and end with conclusions.

Preliminaries
We recall the abstract syntax and the equivalence-based abstract operational semantics of CHR (Constraint Handling Rules) [Frü09] in this section. We also informally describe the refined operational semantics typically realized in sequential implementations of CHR.

Abstract Syntax of CHR
The CHR language is based on the abstract concept of constraints. Constraints are relations, distinguished predicates of first-order predicate logic. There are two kinds of constraints: built-in (pre-defined) constraints and user-defined (CHR) constraints which are defined by the rules in a CHR program. Built-in constraints can be used as tests in the guard as well as for auxiliary computations in the body of a rule. There are at least the built-in constraints true and false, syntactical equality = over finite terms and the usual relations over arithmetic expressions. Upper-case letters stand for (possibly empty) conjunctions of constraints in definitions, lemmas and theorems.
Definition 1 (CHR Program and Rules) A CHR program is a finite set of rules. A (generalized) simplification rule is of the form where r is an optional name (a unique identifier) of a rule. The head H is a conjunction of user-defined constraints, the optional guard C is a conjunction of built-in constraints, and the body B is a goal.
The local variables of a rule are those not occurring in the head of the rule. A renaming (variant, copy) of a goal is obtained by uniformly replacing its variables by other variables.
Conjunctions are understood as multisets of their atomic conjuncts. We often use simple commas to denote logical conjunction to avoid clutter. A goal is a conjunction of built-in and user-defined constraints. A state is a goal.

Abstract Operational Semantics of CHR
Computations in CHR are sequences of rule applications. The operational semantics of CHR is given by the state transition system. It relies on a structural equivalence between states that abstracts away from technical details in a transition [RBF09,Bet14].
State equivalence treats built-in constraints semantically and user-defined constraints syntactically. Basically, two states are equivalent if their built-in constraints are logically equivalent (imply each other) and their user-defined constraints form syntactically equivalent multisets in this context. For example, Let CT be a (decidable) constraint theory for the built-in constraints.
Definition 2 (State Equivalence) [RBF09] Let C i be the built-in constraints, let B i denote user-defined constraints, and let V be a set of variables. Variables of a goal or state that do not occur in V are called local variables of the goal or state. Two states S 1 = (C 1 ∧ B 1 ) and S 2 = (C 2 ∧ B 2 ) with local variablesx and y that have been renamed apart are equivalent, written S 1 ≡ V S 2 , if and only if Note that this definitions implies It also makes sure that there is a one-to-one correspondence between userdefined constraints as enforced by B 1 = B 2 . It allows the renaming of local variables. Local variables can be removed if logical equivalence is maintained. Occurrences of local variables can be substituted by terms if logical equivalence is maintained. These properties have been shown in [RBF09]. An example illustrates these properties of state equivalence and the effect of the global variables V: We may drop V from the equivalence if it is clear from the context. Using this state equivalence, the abstract CHR semantics is defined by a single transition (computation step) between states. It defines the application of a rule. If the source state can be made equivalent to a state that contains the head and the guard of a renaming of a rule, then we can apply the rule by replacing the head by the body in the state. Any state that is equivalent to this target state is also in the transition relation.
Definition 3 (Transition) A CHR transition (computation step) S → r T is defined as follows, where S is called source state and T is called target state: where the rule (r : H ⇔ C | B) is a renaming of a rule from a given program P such that its local variables do not occur in G.
A computation (derivation) of a goal (query) S with variables V in a program P is a connected sequence S i → ri S i+1 beginning with the initial state (query) S 0 that is S and ending in a final state (answer, result) S n or otherwise the sequence is infinite and the computation is non-terminating (diverging). We may drop the reference to the rules. The relation → * denotes the reflexive and transitive closure of →.
The goal G is called context of the rule application. It remains unchanged. It may be empty. Note that CHR is a committed-choice language, i.e. there is no backtracking or undoing of rule applications.

Refined Operational Semantics of CHR
Almost all sequential CHR implementations execute queries and rule body constraints from left to right and apply rules top-down following their textual order of the program. This behavior has been formalized in the so-called refined semantics which is a concretization of the abstract operational semantics [DSGH04].
In this refined semantics, a CHR constraint in a goal can be understood as a procedure call that goes efficiently through the rules of the program. If the current goal matches the head constraints of a rule and if, under this matching, the guard check of the rule holds in the current context, the rule is applicable. Given a query, the rules of the program are applied to exhaustion. When a simplification rule is applied, the matched constraints are replaced by the body of the rule.

Repeated Recursion Unfolding
We recall a definition of rule unfolding in CHR, then define and prove correctness of simplification inside rules in order to introduce repeated recursion unfolding.

Rule Unfolding
For correct unfolding of rules in CHR, we follow the definition of [GMTW15], where also correctness of the unfolding function is shown. This means that we can safely add the unfolded rule to a program while preserving its semantics. In other words, a correctly unfolded rule is always redundant (but, of course, is expected to improve efficiency). In this paper we specialize the definition to the case of CHR simplification rules instead of arbitrary CHR rules. This simplifies the definition and is sufficient for our purposes.
For a goal A, let vars(A) denote the set of variables in A. A substitution is based on a mapping function from variables to terms θ : V → T , written in postfix notation, such that domain of θ, the set dom(θ) = {X | Xθ = X} is finite. When a substitution is applied to a goal, it is applied to all variables in the goal.
In words, C 1 does not contain the constraints from C 2 that are implied by C 3 .
Definition 4 (Unfolding) (Def. 8 [GMTW15]) Let P be a CHR program and let r, v ∈ P be two rules whose variables have been renamed apart where D is the conjunction of the built-in constraints in the body of r. Then we define unfold (r, v) = r ′ as follows. Let θ be a substitution such that dom(θ) ⊆ vars(H ′ ) and CT |= (C ∧ D) → S=H ′ θ, then the unfolded rule r ′ is: If a goal S in the body of rule r matches the head H ′ of a rule v, unfolding replaces S in the body of rule r by the body of rule v together with S=H ′ to obtain a new rule r ′ . In the resulting rule r ′ we also add to its guard C an instance of a part of the guard of rule v. This part C ′′ contains the non-redundant built-in constraints that are not already implied by the built-in constraints in the guard and body of the rule r.
Note that for a correct unfolding according to the above definition, three conditions have to be satisfied. First, means that goal S must match the head H ′ , i.e. be an instance of H ′ , in the context of the built-in constraints of the rule r. This condition reflects the fact that the rule v should be applicable to S.

Second, the non-obvious condition
means that for correctness the variables shared between the instantiated head H ′ θ and instantiated simplified guard C ′′ θ of the rule v must also occur in H. Note that using C ′′ instead of C can make the set of variables smaller that have to occur in H.
Third, the satisfiability of the guard of the unfolded rule r ′ , CT |= ∃(C∧C ′′ θ), ensures that the rule is nontrivial in that it has a satisfiable guard. Otherwise the rule would never be applicable.
Example 2 (Summation, contd.) We unfold the recursive rule for summation with (a copy of ) itself: Then the unfolded rule is Unfolding is correct since its three conditions are satisfied. First, sum(N −1, S1) is an instance of sum(N ′ , S ′ ), i.e.
(N > 1, S := N + S1) → sum(N −1, S1) = sum(N ′ , S ′ )θ, since θ can map N ′ to N −1 and S ′ to S1. Second, Obviously we can simplify the built-in constraints of the guard and the body of this rule, and we will define this kind of simplification next.

Rule Simplification
Speedup crucially depends on the amount of constraint simplification that is possible in the unfolded rules. The goal is to replace constraints by semantically equivalent ones that can be executed more efficiently.
Definition 5 (Simplification) Given a rule r of the form where D are the built-in constraints and B are the user-defined constraints in the body of the rule. We define where D ′ are the built-in constraints and B ′ are the user-defined constraints in the body of the rule and where V = vars(H) ∪ vars(H ′ ).
In the given rule, we replace head and guard, and the body, respectively, by simpler yet state equivalent goals. The choice of V allows us to remove local variables if possible, i.e those that occur only in the guard or body of the rule. We temporarily add the guard C when we simplify the body to ensure correctness and improve the simplification.
For correctness we have to show that the same transitions S → T are possible with rule r and rule simplify (r).

Theorem 1 (Correctness of Rule Simplification
Proof. According to the definition of a CHR transition and simplify (r), we know that It suffices to show that S → r T implies S → s T , since the implication in the other direction is symmetric and can be shown in the same way. Hence we have to show that there exists a goal G ′ such that We choose G ′ = C ∧ G. The full proof can be found in the appendix.
Example 3 (Summation, contd.) Recall the unfolded rule For the head and guard we have that For the body we have that Thus the rule can be simplified into the rule sum(N, S) ⇔ N > 2 | S := 2 * N −1+S1 ′ , sum(N −2, S1 ′ ).

Repeated Recursion Unfolding
We now define what it means to unfold a given recursive rule with itself, to simplify it, to repeat this process, and to add the resulting rules up to a given bound to the original program.
Definition 6 (Repeated Recursion Unfolding) Let r be a recursive rule in a given program P. The unfolding of a recursive rule r is defined as The repeated unfolding of a recursive rule r with simplification is a sequence of rules r 0 , r 1 , . . . , r i , . . . where Let n be an upper bound on the number of recursive steps (recursion depth) for rule r. The recursively unfolded program P r,n of rule r is defined as Example 4 (Summation, contd.) Recall the unfolded simplified rule sum(N, S) ⇔ N > 2 | S := 2 * N −1+S1, sum(N −2, S1).
We repeat the unfolding: The unfolded rule can be simplified into the rule The complete program for repeated recursion unfolding sum three times is: Note that for the query sum(9, R) we could use any of the recursive rules with the same result. Of course the most efficient way is to use the first rule. We will discuss optimal rule applications in the next section.

Time Complexity and Super-Linear Speedup
We first show that we can save on rule applications with our recursive unfolding scheme: we will always apply the most unfolded recursive rule to perform a maximum number of recursive steps with a minimum number of rule applications. Significant speedup then crucially depends on the amount of constraint simplification that is possible in the unfolded rules. Then we show that simplification leads to super-linear speedup in the best case, i.e. a change into a lower time complexity class.

Optimal Rule Applications
By definition of correct unfolding, the unfolded rule is redundant with regard to the original rule. The other direction is not necessarily true. Even if the number of recursive steps should admit the application of an unfolded rule instead of the original rule, it may not be possible because the guard of the unfolded rule may be somewhat too strict.
Lemma 1 (Optimal Rule Applications) Given a program P with a recursive rule r. Assume that the unfolded rules in the unfolded program P r,n satisfy the following condition: If a rule r i with i < log 2 (n) can perform two recursive computation steps in a state, then rule r i+1 can perform one computation step. Given a computation with the rule r that takes n recursion steps. Then there exists a computation with at most log 2 (n) recursive rule applications in the unfolded program P r,n that results in an equivalent state. We call these optimal rule applications.
Proof. The original recursive rule r performs one recursive step when applied. With each unfolding, the number of steps covered by the new unfolded rule is doubled. For rule r i , 2 i recursive steps are covered.
From the condition in the claim it follows that for a query with recursion depth n, any unfolded rule r i is applicable with n ≥ 2 i . Since the unfolding is correct, the resulting states will be equivalent. In one application step of rule r i , the recursion depth will be reduced to n − 2 i .
Then the optimal rule application strategy is to apply rule r i of P r,n such that 2 i+1 > n ≥ 2 i . We continue likewise with the resulting recursive goal until n = 0 and we have hit the base case of the recursion. As a consequence of this strategy, each of the rules r j with 0 ≤ j ≤ i is applicable at most once because from 2 j+1 > n j ≥ 2 j it follows that 2 j > n j − 2 j ≥ 0. Since at most log 2 (n) rules have been generated by repeated unfolding, the above claim holds.

Super-Linear Speedup
With repeated unfolding up to log 2 (n) and optimal rule applications we are replacing n by log 2 (n) recursive calls. For a significant speedup, we also need simplification. To formalize the speedup, we need the following definition as a starting point.

Time Complexity Class n ≥ 2 Recursive
Step c(n) Recursion r(n) Unfolded r ′ (n) (poly)logarithmic, constant k ≥ 0 log2(n) k nlog2(n) k log2(n) k+1 polynomial, linear k ≥ 1 n k n k+1 2n k exponential 2 n 2 n+1 2 n+1 Note that by this definition, the runtime bound of the next recursive step will be c(n−1) and so on till c(0) which refers to the base case. We will ignore the runtime of base cases since their complexity is usually constant and since they are not affected by our transformations. A significant speedup can be achieved if we can simplify the built-in constraints in the unfolded rules so that their runtime does not double with each unfolding. In the best case, unfolding does not increase the runtime bound of a recursive step: instead of a time bound of c(n) + c(n) in the unfolded rule, we still have a bound of c(n) with simplified constraints. We call this best-case simplification. In the following theorem we show how this speedup can change the complexity class into a lower one.

Theorem 2 (Super-Linear Speedup of Repeated Recursion Unfolding)
Given an unfolded program P r,n with optimal rule applications. We assume best-case simplification. Let the function c(n) compute a time bound for the first recursive step with any recursive rule r i with i ≤ log 2 (n) for any query with recursion depth n. Then the time complexity classes 1 for the original and unfolded recursion are according to Table 1.
Proof. Then the runtime for the recursive part of the computation r(n) with n ≥ 1 is clearly bounded by nc(n). The time bound can be more precisely modeled by a recurrence relation 2 of the form r(n) = c(n) + r(n − 1).
With optimal rule applications in the unfolded recursion according to Lemma 1, the remaining number of recursive steps to be performed is at least halved going from n to n − 2 i : from the condition for optimal rule application 2 i+1 > n ≥ 2 i it follows that 2 i > n/2, n − 2 i < n − n/2 and thus n − 2 i < n/2. We can therefore model the time bound by the recurrence relation r ′ (n) = c(n) + r ′ (n/2). Table 1 can be proven by solving the recurrences. They can be verified by inserting the solutions. For upper bounds it suffices to show that the left hand side is at least as large as the right hand side of the recurrence relation for n ≥ 2. For example, let c(n) = log 2 (n) then r(n) = nlog 2 (n) = log 2 (n) + (n − 1)log 2 (n) ≥ log 2 (n) + (n − 1)log 2 (n − 1) = c(n) + r(n − 1) and r ′ (n) = log 2 (n) 2 = log 2 (n) + (log 2 (n) − 1)log 2 (n) ≥ log 2 (n) + (log 2 (n) − 1) 2 = log 2 (n) + log 2 (n/2) 2 = c(n) + r ′ (n/2).

Now the results in
For linear and polynomial worst-case time complexity classes a super-linear speedup by the factor O(n/2) is possible, for (poly)logarithmic or constant complexity classes a speedup of O(n/log 2 (n)), while for exponential complexity classes no improvement of the complexity class is possible (but the unfolded recursion will still run faster).

Implementing Optimal Rule Applications
We can readily implement optimal rule applications if we accept some overhead. Besides simply relying on rule order, we present a semi-naive approach in this section called recursionless recursion. One advantage is that this transformation completely eliminates recursion up to a chosen recursion depth. It is therefore well-suited for hardware synthesis [TORF12].

Recursionless Recursion
We transform the recursion away completely based on the observation that in an optimal rule application, each unfolded recursive rule r i will be applied at most once only. We assume that rules are tried in the order in which they appear in the program as stipulated by the refined semantics of CHR.
Definition 8 (Recursionless Recursion) For each i ≤ log 2 (n) we replace the rule where R denotes the recursive call in the body, by the pair of rules where for H, H i denotes the recursive constraint H whose constraint symbol c has been renamed to c i , except for H −1 which is just H, and where H X denotes a user-defined constraint whose arguments are the same sequence of distinct variables given in X. The same syntax applies to R.
Complexity N > n ≥ 2 Recursion Unfolded Just Rule Order Recursionless (poly)logarithmic, c. k ≥ 0 nlog2(n) k log2(n) k+1 log2(N )log2(n) k+1 2log2(N )log2(n) k polynomial, linear k ≥ 1 n k+1 2n k 2log2(N )n k (log2(N ) + 2)n k exponential 2 n+1 2 n+1 log2(N )2 n+1 (log2(N ) + 2)2 n Figure 2: Speedup with worst-case overhead when unfolded up to log 2 (N ) Note that by this construction, each rule is applicable at most once, because there is no recursion left. For each recursion level i, relying on rule order, first rule r i will be tried. It is either applied or otherwise rule r ′ i is applicable. In r ′ i we just pass the argument parameters down to the next lower rule level. So we either we apply rule r i with no additional overhead or we apply the very simple rule r ′ i which has constant runtime plus the overhead of trying rule r i before.

Speedup with Worst-Case Overhead
Rule application attempts that do not lead to rule applications cause an overhead. The overhead depends on the number of unfolded rules and the cost of trying them. In the best case, the cost for head matching attempts and guard checking is constant and the resulting overhead is neglectable. For the worst case we can assume that rule application attempts cost as much time as actual rule applications. This leads to the following lemma. It shows that even in the worst case super-linear speedup is still obtained for most recursion depths.
Lemma 2 (Speedup with Worst-Case Overhead) Let N > n. Assume we have repeatedly unfolded for recursion depth N , i.e. up to log 2 (N ). We have a query with recursion depth n and complexities c(n), r(n) and r ′ (N ) as calculated in Theorem 2. Then Table 2 shows the upper bounds on the worst-case overhead for the corresponding complexity classes.
Proof. When we use rule order alone, up to log 2 (N ) rules will be tried in vain before a rule will be applied. This happens for each recursive call. For the first recursive call this incurs a runtime of c(n) with each attempt in the worst case or each application, for the second of c(n/2) and so on. We already know that the sum of these runtimes is r ′ (n). So instead of the runtime r ′ (n) we have a worst-case time bound of log 2 (N )r ′ (n).
With recursionless recursion we try each rule at most once. With rule order the handling of the additional rules r ′ i at each recursion level takes constant time and we can ignore them in the following. First we try log 2 (N ) − log 2 (n) unfolded rules r i in vain before we reach the rule corresponding to level log 2 (n). From then on, the worst case is the application of all rules below. So overall, log 2 (N )−log 2 (n) rules are tried once each with runtime c(n) and then a runtime of r ′ (n) is incurred, resulting in a bound (log 2 (N ) − log 2 (n))c(n) + r ′ (n).
Using these formulas with the complexities for c(n), r(n) and r ′ (N ) from Theorem 2 gives the upper bounds that are listed in somewhat simplified form in Table 2.
From Table 2 we can see that the worst case overhead is a factor of O(log 2 (N )) for rule order alone. For recursionless recursion, it is a worst case factor of O(2log 2 (N )/log 2 (n)) for polylogarithmic complexity classes, and a factor of O(log 2 (N )/2) for polynomial and exponential complexity.
In this worst case of recursionless recursion, all complexity classes but exponential complexity are still lower than the complexity classes of the original recursions as long as n is larger than log 2 (N ).
Unbounded Recursion. With recursionless recursion, the recursion depth is bounded by N . We can simply eliminate this bound by re-introducing recursion for the most unfolded rule r k with k = ⌊log 2 (N )⌋: For N ≤ n we now apply rule r k as long as possible. Of course, recursionless recursion is now a misnomer.

Examples with Benchmarks
We have implemented a simple prototype for performing repeated recursion unfolding in CHR and Prolog relying on rule order and recursionless recursion. The source code of the resulting example programs is listed in the appendix. In our experiments, we used the CHR system in SWI Prolog Version 6.2.1 running on an Apple Mac mini 2018 with Intel Core i5 8GB RAM and OS-X 10.14.6. In our benchmarks, unfolding is up to the level given by log 2 (N ) with N > n.

Benchmarks for Summation Example
All recursive rules of sum have a constant time for matching the head, checking the guard, computing the sum and doing the recursive call including the subtraction. The recursion depth is determined by the input number n.

Figure 3: Benchmarks of Summation
Super-Linear Speedup. Table 3 lists our benchmark results for repeated unfolding up to log 2 (N ) = 25 and input numbers n from 1024 to 8192. Times are in milliseconds. Summation has been performed once for all numbers in the given range. The given timings are the sum of these execution times. The unfolded versions showed constant timings for the number ranges over the complete set of numbers, with recursionless recursion performing about 200 summations per millisecond. The row Original shows the linear runtime of the given recursive summation. Row Rule Order refers to the unfolded recursion of sum relying on rule order alone, which already shows constant time and at least a ten-fold speedup. Recursionless refers to the recursionless recursion, it is a factor of four faster than the unfolded recursion, again showing constant time. By comparison, the Prolog implementation of the original rules using the cut operator for efficiency shows again the linear time behavior.
According to the Speedup Theorem 2, for the original recursion we expect linear time complexity O(n). According to Lemma 2, for the unfolded program with rule order the complexity is O(log 2 (N )log 2 (n)) and with recursionless recursion O(log 2 (N )). Since N is fixed in our benchmarks, this amounts to constant time.
We attribute the better-than-estimated constant time behavior of the unfolded recursion with rule order to the strong variation in rule attempts and applications with subsequent numbers. For example, while the number 1025 requires just one recursive step with rule r 10 , the previous number 1024 needs all smaller recursive steps from r 9 down to r 0 . This behavior leads to constant runtime when we sum over ranges of numbers as in Table 3.

Complete Example List Reversal
This classical program reverses a given list in a naive way. The constraint r (A, B) holds if list B is the reversal of list A. We use Prolog notation for lists. The built-in constraint a(X, Y, Z) appends (concatenates) two lists X and Y into a third list Z. Its runtime is linear in the length of the first list. Repeated Recursion Unfolding. We try to unfold the recursive rule with a copy of itself: However the recursive call in the original rule r (A, B) is not an instance of the head r([C ′ |A ′ ], D ′ ) of the copy of the rule. This is a mere technicality. We move [C ′ |A ′ ] into the guard and replace it by a new variable A ′′ : This does not change the semantics of the rule because The unfolding is now correct with A ′′ substituted by A in the guard (B, [C], D).

Next we use the guard equality
. This is correct since Now we proceed with the simplification for unfolded rules as defined. For the head and guard we simplify For the body we simplify The eureka moment for best-case simplification is that we can merge the two calls to constraint a into one if we concatenate their known second arguments. As a result the unfolded rule is simplified into the rule   According to our Speedup Theorem 2 and Lemma 2, we expect quadratic behavior for the original recursion and linear behavior for the unfolded recursion, were the recursionless recursion should be twice as fast. This actually holds as the benchmarks show.
All timings show linear time behavior except the original list reversal without unfolding. The fastest program version with recursionless recursion reverses about 100 list elements per millisecond. The transformed code executed twice as fast as the hand-coded well-known linear version of list reversal that does not use list concatenation. Surprisingly, our recursionless recursion proved even faster than the built-in optimized reverse/2 of SWI Prolog.
Note that the runtimes around 1024 almost stay constant. Our most unfolded rule with i = N = 10 handles a list with 2 10 = 1024 elements. Again we attribute this averaging effect of considering ranges of inputs. For example, a list of length 1024 needs one rule application with rule r 10 at recursion level i = 10 before the base case is reached, while with 1023 we need to apply all rules for each level i < 10.

Related Work
Program transformation to improve efficiency is usually concerned with a strategy for the combination of unfolding and folding techniques to replace code starting with [BD77]. In the literature, recursion is usually unfolded several times together with the base case and then simplified. We rely solely on unfolding the recursive part and repeat the process. We ignore the base case. We add redundant rules this way but never remove any.
Program transformation as a tool for specific aims and applications is abundant in CHR, for an overview see [SVWSDK10,Frü15]. General methods for unfolding [GMTW15] exist (which we have used in this paper), for specializing rules with regard to a specific given query [Frü05], and for optimization induced by confluence [AF04].
In [Amt91] unfolding-based meta-level systems for Prolog consist of a hierarchy of additional meta-rules and a hierarchical execution scheme, i.e. a change in semantics. These rules are described as shortcuts obtained from unfold/fold operations. Presumably, when adapted to Prolog, the rules generated by repeated recursion unfolding could be considered as meta-rules in this generic framework.
Directly related literature is sparse. One reason could be that our approach is based on generating and keeping redundant rules which seems counter-intuitive at first. Moreover, super-linear speedups are a rare feat and mostly concern parallel programs, while our approach applies to sequential programs. An exception is work based on supercompilation. In this program transformation, generalisation while unfolding increases the chance for folding. Using advanced generalisation techniques for supercompilation, distillation [Ham09] and equality indices [GKN16] can achieve super-linear speedup on some examples. In contrast, our approach is straightforward, as it does not involve generalisation or folding, and is applied to a programming language in practical use.

Conclusions and Future Work
Repeated recursion unfolding is a new approach that repeatedly unfolds a recursion with itself and simplifies it while keeping all unfolded rules. We proved its correctness.
We showed there exists an optimal rule application strategy such that significant speedups are possible. We proved a super-linear speedup theorem in case of best-case simplification. Then our program transformation lowers the time complexity of a recursion for polylogarithmic classes by a factor of O(n/log 2 (n)) and for polynomial classes by a factor of O(n).
For a semi-naive implementation of repeated recursion unfolding, recursionless recursion, we proved an overhead which is linear in the number of unfolded rules. Super-linear speedup is still obtained in most cases. The actual runtime improvement quickly reaches several orders of magnitude. Our approach improves the time complexity from linear to constant for the summation example and from quadratic to linear for list reversal. The latter runs faster than a built-in hand-optimized version.
While our speedups are super-linear, it is too early to tell which recursive algorithms allow for the necessary best-case simplification. A good simplification requires some insight and thus in general cannot be found automatically.
We defined and implemented repeated recursion unfolding using the rulebased language CHR (Constraint Handling Rules), but we think our approach can be applied to mainstream programming languages and hardware synthesis as well.
Ongoing and future work. To extend our approach to mutual recursion as well as multiple recursive rules should be straightforward. Indeed, we already could derive a novel double recursive linear-time algorithm from a naive exponential-time double recursion for Fibonacci numbers.
In this paper, the super-linear speedup is bounded in the sense that it holds up to a chosen upper bound on the number of recursive steps. In ongoing work, we have succeeded for the examples in this paper to extend our approach to run-time dynamic on-the-fly just-in-time repeated recursion unfolding so that the super-linear speedup is unbounded, i.e. independent of the recursion depth.
The implementation overhead of optimal rule applications can be reduced with indexing on the recursion depth. We already have implemented indexing for the examples in this paper.
One could also transfer our approach from recursion to loop constructs in other programming languages. We have already done examples for Java.

A Proof of Correctness of Rule Simplification
For correctness of rule simplification (see Subsection 3.2) we have to show that the same transitions S → T are possible with rule r and rule simplify (r). Here is the full proof for Theorem 1.
Theorem 1 (Correctness of Rule Simplification) Let r = (H ⇔ C | D ∧ B) be a rule and let s = (H ′ ⇔ C ′ | D ′ \C ′ ∧B ′ ) be the simplified rule simplify (r). For any state S and variables V, S → r T iff S → s T .
Proof. According to the definition of a CHR transition and simplify (r), we know that It suffices to show that S → r T implies S → s T , since the implication in the other direction is symmetric and can be shown in the same way. Hence we have to show that there exists a goal G ′ such that To show the first part concerning state S, we proceed as follows. We choose G ′ = C ∧ G. Let G = (G C ∧ G B ) where G C are the built-in constraints and G B are the user-defined constraints of G. According to the definition of state equivalence and its transitivity we have to show that the two states equivalent to S are equivalent where thex ′ ,ȳ ′ ,x,ȳ are local variables, such that •x ′ are the variables in H ∧ C only that are not in V ′ , •ȳ ′ are the variables in H ′ ∧ C ′ only that are not in V ′ , •x are the variables in H ∧ C ∧ G that are not in V, •ȳ are the variables in H ′ ∧ C ′ ∧ G ′ that are not in V.
By the definition of simplification, V ′ are the variables in H and H ′ . By definition of the transition,x includes the local variables of the given rule, i.e. those not in the head H, andȳ includes the local variables of the simplified rule, i.e. those not in the head H ′ .