Enhancing expressivity of checked corecursive streams (extended version)

We propose a novel approach to stream definition and manipulation. Our solution is based on two key ideas. Regular corecursion, which avoids non termination by detecting cyclic calls, is enhanced, by allowing in equations defining streams other operators besides the stream constructor. In this way, some non-regular streams are definable. Furthermore, execution includes a runtime check to ensure that the stream generated by a function call is well-defined, in the sense that access to an arbitrary index always succeeds. We extend the technique beyond the simple stream operators considered in previous work, notably by adding an interleaving combinator which has a non-trivial recursion scheme.


Introduction
Applications often deal with data structures which are conceptually infinite; among those data streams (unbounded sequences of data) are a paradigmatic example, important in several application domains as the Internet of Things. Lazy evaluation is a well-established and widely-used solution to data stream generation and processing, supported, e.g., in Haskell, and in most stream libraries offered by mainstream languages, as java.util.stream. In this approach, data streams can be defined as the result of an arbitrary function. For instance, in Haskell we can write one_two = 1:2: one_two --1:2:1:2:1: ... from n = n : from ( n +1) --n:n+1:n+2: ...
Functions which only need to inspect a finite portion of the structure, e.g., getting the i-th element, can be correctly implemented, thanks to the lazy evaluation strategy as exemplified below. More recently, another approach has been proposed [13,18,10,2], called regular corecursion, which exploits the fact that streams as one_two above are periodic, a.k.a. regular following the terminology in [7], meaning that the term 1:2:1:2:1: ... is infinite but has a finite number of subterms. Regular streams can be actually represented at runtime by a finite set of equations involving only the stream constructor, in the example x = 1 : 2 : x. Furthermore, function definitions are corecursive, meaning that they do not have the standard inductive semantics; indeed, even though the evaluation strategy is call-by-value, thanks to the fact that pending function calls are tracked, cyclic calls are detected, avoiding in this case non-termination.
For instance, with regular corecursion 1 we have: one_two () = 1:2: one_two () from ( n ) = n : from ( n +1) get_elem (3 , one_two ()) --evaluates to 2 get_elem (3 , from (5)) --leads to non-termination Despite their differences, in both approaches programmers are allowed to write intuitively ill-formed definitions such as bad_stream() = bad_stream(); any access to indexes of the stream returned by this function leads to non-termination both with lazy evaluation and regular corecursion. However, while in the regular case it is simple to reject the result of calling bad_stream by checking a guardedness syntactic condition, the Haskell compiler does not complain if one calls such a function. In this paper, we propose a novel approach to stream generation and manipulation, providing, in a sense, a middle way between those described above. Our solution is based on two key ideas: -Corecursion is enhanced, by allowing in stream equations other typical operators besides the stream constructor; in this way, some non-regular streams are supported. For instance, we can define from(n)=n:(from(n)[+]repeat(1)), with [+] the pointwise addition and repeat defined by repeat(n)=n:repeat(n). -Execution includes a runtime check which rejects the stream generated by a function call if it is ill-formed, in the sense that access to an index could possibly diverge. For instance, the call bad_stream() raises a runtime error.
In this way we achieve a convenient trade-off between expressive power and reliability; indeed, we do not have the full expressive power of Haskell, where we can manipulate streams generated as results of arbitrary functions, but, clearly, the well-definedness check described above would be not decidable. On the other hand, we significantly augment the expressive power of regular corecursion, allowing several significant non-regular streams, at the price of making the welldefinedness check non-trivial, but still decidable. The main formal results are (1) Theorem 1 stating the soundness of the runtime check; (2) Theorem 2 stating that the optimized definition of the runtime check in Sect. 5 is equivalent to the simpler one given in Sect. 4. In particular, for contribution (1) the interleaving operator requires a more involved proof in comparison with [3] (see Sect. 6), while for (2) we show that the optimized definition improves the time complexity from O(N 2 ) to O(N log N ).
In Sect. 2 we formally define the calculus, in Sect. 3 we show examples, in Sect. 4 we define the well-formedness check, and in Sect. 5 its optimized version. Finally, in Sect. 6 we discuss related and further work. The Appendix contains more examples of derivations and omitted proofs.   A program is a sequence of (mutually recursive) function declarations, for simplicity assumed to only return streams. Stream expressions are variables, conditionals, expressions built by stream operators, and function calls. We consider the following stream operators: constructor (prepending a numeric element), tail, pointwise arithmetic operators, and interleaving. Numeric expressions include the access to the i-th 2 element of a stream. We use fd to denote a sequence fd 1 , . . . , fd n of function declarations, and analogously for other sequences.

Stream calculus
The operational semantics, given in Fig. 2, is based on two key ideas: 1. some infinite streams can be represented in a finite way 2. evaluation keeps trace of already considered function calls To obtain (1), our approach is inspired by capsules [12], which are expressions supporting cyclic references. That is, the result of a stream expression is a pair (s, ρ), where s is an (open) stream value, built on top of stream variables, numeric values, the stream constructor, the tail destructor, the pointwise arithmetic and the interleaving operators, and ρ is an environment mapping variables into stream values. In this way, cyclic streams can be obtained: for instance, (x, x → n : x) denotes the stream constantly equal to n.
We denote by dom(ρ) the domain of ρ, by vars(ρ) the set of variables occurring in ρ, by fv(ρ) the set of its free variables, that is, vars(ρ) \ dom(ρ), and say that ρ is closed if fv(ρ) = ∅, open otherwise, and analogously for a result (v, ρ).
Altogether, the semantic judgment has shape e, ρ, τ ⇓ (v, ρ ′ ), where e is the expression to be evaluated, ρ the current environment defining possibly cyclic stream values that can occur in e, τ the call trace, and (v, ρ ′ ) the result. The semantic judgments should be indexed by an underlying (fixed) program, omitted for sake of simplicity. Rules use the following auxiliary definitions: ρ ⊔ ρ ′ is the union of two environments, which is well-defined if they have disjoint domains; ρ{x → s} is the environment which gives s on x, coincides with ρ elsewhere; we use analogous notations for call traces. Intuitively, a closed result (s, ρ) is well-defined if it denotes a unique stream, and a closed environment ρ is well-defined if, for each x ∈ dom(ρ), (x, ρ) is welldefined. In other words, the corresponding set of equations admits a unique solution. For instance, the environment {x → x} is not well-defined, since it is undetermined (any stream satisfies the equation x = x); the environment {x → x[+]y, y → 1 : y} is not well-defined as well, since it is undefined (the two equations x = x → x[+]y, y = 1 : y admit no solutions for x). This notion can be generalized to open results and environments, assuming that free variables denote unique streams, as will be formalized in Sect. 4.
Rules for values and conditional are straightforward. In rules (cons), (tail) and (op), arguments are evaluated and the stream operator is applied without any further evaluation. That is, we treat all these operators as constructors.
The rules for function call are based on a mechanism of cycle detection [2]. Evaluation of arguments is handled by a separate rule (args), whereas the following two rules handle (evaluated) calls.
Rule (invk) is applied when a call is considered for the first time, as expressed by the first side condition. The body is retrieved by using the auxiliary function fbody, and evaluated in a call trace where the call has been mapped into a fresh variable. Then, it is checked that adding the association of such variable with the result of the evaluation of the body keeps the environment well-defined, as expressed by the judgment wd (ρ, x, s), which will be defined in Sect. 4. If the check succeeds, then the final result consists of the variable associated with the call and the updated environment. For simplicity, here execution is stuck if the check fails; an implementation should raise a runtime error instead. An example of stuck derivation is presented in the Appendix (Fig. 10).
Rule (corec) is applied when a call is considered for the second time, as expressed by the first side condition. The variable x is returned as result. However, there is no associated value in the environment yet; in other words, the result (x, ρ) is open at this point. This means that x is undefined until the environment is updated with the corresponding value in rule (invk). However, x can be safely used as long as the evaluation does not require x to be inspected; for instance, x can be safely passed as an argument to a function call.
Finally, rule (at) computes the i-th element of a stream expression. After evaluating the arguments, the result is obtained by the auxiliary judgment at ρ (s, i) = n, whose straightforward definition is at the bottom of the figure. Rules (at--even) and (at--odd) define the behaviour of the interleaving operator, which merges two streams together by alternating their elements.
When evaluating at ρ (s, i), if s is a variable free in the environment, then execution is stuck; again, an implementation should raise a runtime error instead. With the standard semantics of recursion, the calls, e.g., repeat(0) and one_two() lead to non-termination. Thanks to corecursion, instead, these calls terminate, producing as result (x, {x → 0 : x}), and (x, {x → 1 : y, y → 2 : x}), respectively. Indeed, when initially invoked, the call repeat(0) is added in the call trace with an associated fresh variable, say x. In this way, when evaluating the body of the function, the recursive call is detected as cyclic, the variable x is returned as its result, and, finally, the stream value 0 : x is associated in the environment with the result x of the initial call. In the sequel, we will use [k] as a shorthand for repeat(k). The evaluation of one_two() is analogous, except that another fresh variable y is generated for the intermediate call two_one(). The formal derivations are given below.

Examples
For space reasons, we did not report the application of rule (value). In both derivations, note that rule (corec) is applied, without evaluating the body of one_two once more, when the cyclic call is detected.
The following examples show function definitions whose calls return nonregular streams, notably, the natural numbers, the natural numbers raised to the power of a number, the factorials, the powers of a number, the Fibonacci numbers, and the stream obtained by pointwise increment by one. The definition of nat uses corecursion, since the recursive call nat() is cyclic. Hence the call nat() returns (x, {x → 0 : (x[+]y), y → 1 : y}). The definition of nat_to_pow is a standard inductive one where the argument strictly decreases in the recursive call. Hence, the call, e.g., nat_to_pow (2) . The definitions of fact, pow, and fib are corecursive. For instance, the call fact() returns (z, z → 1 : The following definition is an instance of a schema generating the infinite sequence of labels obtained by a breadth-first visit of an infinite complete binary tree where the labels of children are defined in terms of that of their parent.
In particular, the root is labelled by 1, and the left and right child of a node with label i are labelled by 2*i and 2*i+1, respectively. Hence, the generated stream is the sequence of natural numbers starting from 1, as it happens in the array implementation of a binary heap.
In the other instance below, the root is labelled by 0, and children are labelled with i+1 if their parent has label i . That is, nodes are labelled by their level.
The following function computes the stream of partial sums of the first i + 1 elements of a stream s, that is, Such a function is useful for computing streams whose elements approximate a series with increasing precision; for instance, the following function returns the stream of partial sums of the first i + 1 elements of the Taylor series of the exponential function: Function sum_expn calls sum with the argument pow(n)[/]fact() corresponding to the stream of terms of the Taylor series of the exponential; hence, by accessing the i-th element of the stream, we have the following approximation of the series: 4 Well-definedness check A key feature of our approach is the runtime check ensuring that the stream generated by a function call is well-defined, see the side condition wd (ρ ′ , x, s) in (invk); in this section we formally define the corresponding judgment and prove its soundness. Before doing this, we provide, for reference, a formal abstract definition of well-definedness. Intuitively, an environment is well-defined if each variable in its domain denotes a unique stream. Semantically, a stream σ is an infinite sequence of numeric values, that is, a function which returns, for each index i ≥ 0, the i-th element σ(i). Given a result (s, ρ), we get a stream by instantiating variables in s with streams, in a way consistent with ρ, and evaluating operators. To make this formal, we need some preliminary definitions.
A substitution θ is a function from a finite set of variables to streams. We denote by s θ the stream obtained by applying θ to s, and evaluating operators, as formally defined below.
Given an environment ρ and a substitution θ with domain vars(ρ), the substitution ρ[θ] is defined by: Then, a solution of ρ is a substitution θ such that ρ[θ] = θ. An open environment ρ is well-defined if, for each θ with domain fv(ρ), it has exactly one solution θ ′ such that θ ⊆ θ ′ . For instance, the open environment {y → 0 : (y[+]x)} is well-defined.
In Fig. 3 we provide the operational characterization of well-definedness. The judgment wd (ρ, x, s) used in the side condition of rule (invk) holds if wd ρ ′ (x, ∅) holds, with ρ ′ =ρ{x → v}. The judgment wd ρ (s, ∅) means well-definedness of a result. That is, restricting the domain of ρ to the variables reachable from s (that is, either occurring in s, or, transitively, in values associated with reachable variables) we get a well-defined environment; thus, wd (ρ, x, s) holds if adding the association of s with x preserves well-definedness of ρ.
The additional argument m in the judgment wd ρ (s, m) is a map from variables to integer numbers. We write m +1 and m −1 for the maps In rule (main), this map is initially empty. In rule (wd-var), when a variable x defined in the environment is found the first time, it is added in the map with initial value 0 before propagating the check to the associated value. In rule (wdcorec), when it is found the second time, it is checked that constructors and right operands of interleave are traversed more times than tail operators, and if it is the case the variable is considered well-defined. Rule (wd-delay), which m :: = x1 → n1 . . . xn → n k (n ≥ 0) map from variables to integer numbers

Fig. 3. Operational definition of well-definedness
is only added for the purpose of the soundness proof and should be not part of an implementation 3 , performs the same check but then considers the variable occurrence as it is was the first, so that success of well-definedness is delayed. Note that rules (wd-var), (wd-corec), and (wd-delay) can only be applied if x ∈ dom(ρ); in rule (wd-corec), this explicit side condition could be omitted since satisfied by construction of the proof tree.
In rule (wd-fv), a free variable is considered well-defined. 4 In rules (wdcons) and (wd-tail) the value associated with a variable is incremented/decremented by one, respectively, before propagating the check to the subterm. In rule (wd-nop) the check is simply propagated to the subterms. In rule (wd-), the check is also propagated to the subterms, but on the right-hand side the value associated with a variable is incremented by one before propagation; this reflects the fact that, in the worst case, at ρ (s 1 s 2 , i) = at ρ (s 1 , i), and this happens only for i = 0, while for odd indexes i we have that at ρ (s 1 s 2 , i) = at ρ (s 2 , i − k), with k ≥ 1; more precisely, k = 1 only when i = 1; for all indexes i > 1 (both even and odd), k > 1. For instance, the example s() = 1:(s() s()^), which has the same semantics as [1], would be considered not well-defined if we treated the interleaving as the pointwise arithmetic operators.
Note that the rules in Fig. 3 can be immediately turned into an algorithm which, given a stream value s, always terminates either successfully (finite proof tree), or with failure (no proof tree can be constructed). On the other hand, the rules in Fig. 2 defining the at ρ (s, i) = n judgment can be turned into an algorithm which can possibly diverge (infinite proof tree).
To formally express and prove that well-definedness of a result implies termination of access to an arbitrary index, we introduce some definitions and notations. First of all, since the result is not relevant for the following technical treatment, for simplicity we will write at ρ (s, i) rather than at ρ (s, i) = n. We call derivation an either finite or infinite proof tree. We write wd ρ (s ′ , m ′ ) ⊢ wd ρ (s, m) to mean that wd ρ (s ′ , m ′ ) is a premise of a (meta-)rule where wd ρ (s, m) is the conclusion, and ⊢ ⋆ for the reflexive and transitive closure of this relation. Lemma 1.
Proof. The proof is by induction on the length of the path in at ρ (x, i ′ ) ⊢ ⋆ at ρ (s ′ , i).
Base The length of the path is 0, hence we have at ρ (x, i) ⊢ ⋆ at ρ (x, i). We also have wd ρ (x, m) ⊢ ⋆ wd ρ (x, m), and we get the thesis since m(x) = m(x)+i−i.
for some m such that x ∈ dom(m).
Proof. Easy variant of the proof of Lemma 2.
Theorem 1. If wd ρ (s, ∅) has a derivation then, for all j, at ρ (s, j) either has no derivation or a finite derivation.
Proof. Assume by contradiction that at ρ (s, j) has an infinite derivation for some j, and wd ρ (s, ∅) is derivable. By Lemma 1-(2), the following condition holds: for some x ∈ dom(ρ), and i, k ≥ 0.

An optimized algorithm for well-definedness
The definition of well-definedness in Fig. 3 can be easily turned into an algorithm, since, omitting rule (wd-delay), at each point in the derivation there is at most one applicable rule. Now we will discuss its time complexity, assuming that insertion, update and lookup are performed in constant time. It is easy to see that when we find a stream constructor we need to perform an update of the map ρ for every variable in its domain. If we consider the following environment: we get the derivation presented in Fig. 5. Here, the number of constructor oc- (wd-var) wdρ(0 : x3, {x0 → 2, x1 → 1, x2 → 0}) (wd-cons) wdρ(x2, {x0 → 2, x1 → 1}) (wd-var) wdρ(0 : x2, {x0 → 1, x1 → 0}) (wd-cons) wdρ(x1, {x0 → 1}) (wd-var) wdρ(0 : x1, {x0 → 0}) (wd-cons) wdρ(x0, ∅) currences for which we have to perform an update of all variables in the domain of the map is linearly proportional to the number N of nodes in the derivation tree; since the domain is increased by one for each new variable, and the total number of variables is again linearly proportional to N , it is easy to see that we have a time complexity quadratic in N .
We propose now an optimized version of the well-definedness check, having a time complexity of O (N log N ). On the other hand, the version we provided in Fig. 3 is more abstract, hence more convenient for the proof of Theorem 1.
In the optimized version, given in Fig. 6, the judgment has shape owd ρ (s, m, π), where π represents a path in the proof tree where each element corresponds to a visit of either the constructor or the right operand of interleave (value 1 for both) or the tail operator (value -1), and m associates with each variable an index (starting from 0) corresponding to the point in the path π where the variable was found the first time. The only operation performed on a path π is the addition π · b of an element b at the end. m :: = x1 → i1 . . . xn → i k (i ≥ 0) map from variables to indexes π :: = b1b2 . . . bn sequence of either 1 or -1 owdρ(s, m, π · 1) owdρ(n : s, m, π) (owd-tail) owdρ(s, m, π · (−1)) owdρ(sˆ, m, π) (owd-nop) owdρ(s1, m, π) owdρ(s2, m, π) owdρ(s1[nop]s2, m, π) (owd-) owdρ(s1, m, π) owdρ(s2, m, π · 1) owdρ(s1 s2, m, π) In rule (main), both the map and the path are initially empty. In rule (owd-var), a variable x defined in the environment, found for the first time, is added in the map with as index the length of the current path. In rule (owdcorec), when the same variable is found the second time, the auxiliary function sum checks that more constructors and right operands of interleave have been traversed than tail operators (see below). In rule (owd-fv), a free variable is considered well-defined as in the corresponding rule in Fig. 3. In rules (owd-cons), (owd-tail) and (op-wd), the value corresponding to the traversed operator is added at the end of the path (1 for the constructor and the right operand of interleave, -1 for the tail operator). Lastly, rules (owd-nop) behaves in a similar way as in Fig. 3. The semantics of the auxiliary function sum is straightforward: starting from the point in the path where the variable was found the first time, the sum of all the elements is returned.
We now show that the optimized version of the judgment has the same semantics as its counterpart presented in Sect. 4. First of all we formally state that, in Fig. 3, rule (wd-delay) does not affect derivability. Proof. The right-to-left implication is obvious. If wd ρ (s, ∅) uses rule (wd-delay), all the (first in their path) occurrences of the rule can be replaced by rule (wdcorec), still getting a derivation.
Then, we define a relation between the auxiliary structures used in the two judgments: For all m and (m, π), m ⊲⊳ (m, π) holds iff dom(m) = dom(m) and, for all x ∈ dom(m), m(x) = sum(m(x), π).
In this way, we have the following generalization, whose straightforward proof is in the Appendix.

Related and future work
As mentioned in Sect. 1, our approach extends regular corecursion, which originated from co-SLD resolution [17,18,1,5], where already considered goals (up to unification), called coinductive hypotheses, are successfully solved. Language constructs that support this programming style have also been proposed in the functional [13] and object-oriented [6,2] paradigm.
There have been a few attempts of extending the expressive power of regular corecursion. Notably, structural resolution [14,15] is an operational semantics for logic programming where infinite derivations that cannot be built in finite time are generated lazily, and only partial answers are shown. Another approach is the work in [7], introducing algebraic trees and equations as generalizations of regular ones. Such proposals share, even though with different techniques and in a different context, our aim of extending regular corecursion; on the other hand, the fact that corecursion is checked is, at our knowledge, a novelty of our work.
For the operators considered in the calculus and some examples, our main sources of inspiration have been the works of Rutten [16], where a coinductive calculus of streams of real numbers is defined, and Hinze [11], where a calculus of generic streams is defined in a constructive way and implemented in Haskell.
In this paper, as in all the above mentioned approaches derived from co-SLD resolution, the aim is to provide an operational semantics, designed to directly lead to an implementation. That is, even though streams are infinite objects (terms where the constructor is the only operator, defined coinductively), evaluation handles finite representations, and is defined by an inductive inference system. Coinductive approaches can be adopted to obtain more abstract semantics of calculi with infinite terms. For instance, [8] defines a coinductive semantics of the infinitary lambda-calculus where, roughly, the semantics of terms with an infinite reduction sequence is the infinite term obtained as limit. In coinductive logic programming, co-SLD resolution is the operational counterpart of a coinductive semantics where a program denotes a set of infinite terms. In [2], analogously, regular corecursion is shown to be sound with respect to an abstract coinductive semantics using flexible coinduction [4,9], see below.
Our calculus is an enhancement of that presented in [3], with two main significant contributions: (1) the interleaving operator, challenging since it is based on a non-trivial recursion schema; (2) an optimized definition of the runtime well-definedness check, as a useful basis for an implementation. Our main technical results are Theorem 1, stating that passing the runtime well-definedness check performed for a function call prevents non-termination in accessing elements in the resulting stream, and Theorem 2, stating that the optimized version is equivalent.
In future work, we plan to also prove soundness of the operational welldefinedness with respect to its abstract definition. Completeness does not hold, as shown by the example zeros() = [0] [*] zeros() which is not well-formed operationally, but admits as unique solution the stream of all zeros.
Finally, in the presented calculus a cyclic call is detected by rule (corec) if it is syntactically the same of some in the call trace. Although such a rule allows cycle detection for all the examples presented in this paper, it is not complete with respect to the abstract notion where expressions denoting the same stream are equivalent, as illustrated by the following alternative definition of function incr as presented in Sect. 3: If syntactic equivalence is used to detect cycles, then the call incr_reg([0]) diverges, since the terms passed as argument to the recursive calls are all syntactically different; as an example, consider the arguments x and xˆpassed to the initial call and to the first recursive call, respectively, in the environment ρ = {x → 0 : x}; they are syntactically different, but denote the same stream.
In future work we plan to investigate more expressive operational characterizations of equivalence.
Other interesting directions for future work are the following.
-Investigate additional operators and the expressive power of the calculus.