We propose a simple calculus for processing data streams (innite ows of data series), represented by nite sets of equations built on stream operators. Furthermore, functions de ning streams are regularly corecursive, that is, cyclic calls are detected, avoiding non-termination as happens with ordinary recursion in the call-by-value evaluation strategy. As we illustrate by several examples, the combination of such two mechanisms provides a good compromise between expressive power and decidability. Notably, we provide an algorithm to check that the stream returned by a function call is represented by a well-de ned set of equations which actually admits a unique solution, hence access to an arbitrary element of the returned stream will never diverge.
Applications often deal with data structures which are conceptually in nite, among those data streams (in nite ows of data series) are a mainstream example: as we venture deeper into the Internet of Things (IoT) era, stream processing is becoming increasingly important. Indeed, all main IoT platforms provide embedded and integrated engines for real time analysis of potentially in nite owing data series; such a process occurs before the data is stored for e ciency and, as often happens in Computer Science, there is a trade-o between the expressive power of the language, the e ciency of its implementation and the decidability of properties important to guarantee reliability and tractability.
Another related important problem is data stream generation, which is essential to test complex distributed IoT systems; the deterministic simulation of sensor data streams through a suitable language o ers a practical solution to IoT testing and favors early detection of some kinds of bugs that can be xed more easily before the deployment of the whole system.
A well-established solution to data stream generation and processing is lazy evaluation, as supported, e.g., in Haskell, and most stream libraries o ered by mainstream languages, as java.util.stream. In this approach, conceptually in nite data streams are the result of a function or method call, which is evaluated ? Copyright c 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). according to the call-by-need strategy. For instance, in Haskell we can de ne one_two = 1:2:one_two, or even represent the list of natural numbers as from 0, where from n = n:from(n+1). However, such a great expressive power comes at a cost; let us consider, for instance, the de nition bad_stream = 0:tail bad_stream. The Haskell compiler does not complain about this de nition, and no problem arises at runtime as long as the manipulation of bad_stream requires only its rst element to be accessed; anyway, any operation which needs to inspect bad_stream at a deeper level is deemed to diverge. Unfortunately, it is not decidable to check, even at runtime, whether the stream returned by a Haskell function is wellde ned, that is, all of its elements can be computed1; indeed, the full expressive power of Haskell can be used to de ne streams by means of recursive functions. For similar reasons, it is not decidable to check at runtime whether the streams returned by two Haskell functions are equal.
More recently, a complementary approach has been considered in di erent
programming paradigms | functional [
In this way, the Haskell stream one_two can be equivalently obtained by the call2 one_two(), with the function one_two de ned by one_two() = 1:2:one_two(). Indeed, with regular corecursion the result of this call is the value corresponding to the unique solution of the equation x = 1 : 2 : x. On the other hand, since the expressive power is limited to regular streams, it is not possible to de ne a corecursive function whose call returns the stream of natural numbers, as happens for the from 0 Haskell example. However, there exist procedures for checking well-de ned streams and their equality, even with tractable algorithms.
In this paper, we propose a simple calculus of numeric streams which supports regular corecursion and goes beyond regular streams by extending equations with other typical stream operators besides the stream constructor: tail and pointwise operators can be contained in stream equations and are therefore not evaluated.
In this way, we are able to achieve a good compromise between expressive
power and decidability. Notably:
{ the extended shape of equations allows the de nition of functions which
return non-regular streams; for instance, it is possible to obtain the stream of
1 This is what is also known as a productive corecursive de nition [
In Sect. 2 we de ne the calculus, in Sect. 3 we show examples, and in Sect. 4 we provide an operational characterization of well-de ned streams, proved su cient and necessary for an access to an arbitrary index to never diverge. In Sect. 5 we discuss related and further work. An extended version including more examples of derivations and complete proofs can be found at http: //arxiv.org/abs/2108.00281. 2
fd :: = fd1 : : : fdn program fd :: = f(x) = se function declaration e :: = se j ne j be expression se :: = x j if be then se1 else se2 j ne : se j se^ j se1[op]se2 j f(e) stream expression ne :: = x j se(ne) j ne1 op ne2 j 0 j 1 j 2 j ::: numeric expression be :: = x j true j false j ::: boolean expression op :: = + j j j = numeric operation
A program is a sequence of (mutually recursive) function declarations, for simplicity assumed to only return streams. Stream expressions are variables, conditional expressions, expressions built by stream operators, and function calls. We consider the following stream operators: constructor (prepending a numeric element), tail, and pointwise arithmetic operations. Numeric expressions include the access to the i-th3 element of a stream. We use fd to denote a sequence fd1; : : : ; fdn of function declarations, and analogously for other sequences.
The operational semantics, given in Fig. 2, is based on two key ideas: 1. (some) in nite streams are represented in a nite way 2. evaluation keeps trace of already considered function calls 3 For simplicity, here indexing and numeric expressions coincide, even though indexes are expected to be natural numbers, while values in streams can range over a larger numeric domain. (evaluated) call value (open) stream value index, numeric value boolean value 0) call trace 0) environment (val) v; ; + (v; )
be; ; + (true; ) se1; ; + (s; 0) (if-t) if be then se1 else se2; ; + (s; 0) be; ; + (false; ) se2; ; + (s; 0) (if-f) if be then se1 else se2; ; + (s; 0) (corec) f(v); ; + (x; )
(f (v)) = x (at-cons-n) aatt ((sn; i: s; 1i)) == nn00 i > 0
To obtain (1), our approach is inspired by capsules [
We denote by vars( ) the set of variables occurring in , by fv( ) the set of its free variables, that is, vars( ) n dom( ), and say that is closed if fv( ) = ;, open otherwise, and analogously for a result (v; ).
To obtain point (2) above, evaluation has an additional parameter which is a call trace, a map from function calls where arguments are values (dubbed calls for short in the following) into variables.
Altogether, the semantic judgment has shape e; ; + (v; 0), where e is the expression to be evaluated, the current environment de ning possibly cyclic stream values that can occur in e, the call trace, and (v; 0) the result. The semantic judgments should be indexed by an underlying ( xed) program, omitted for sake of simplicity. Rules use the following auxiliary de nitions: { t 0 is the union of two environments, which is well-de ned if they have disjoint domains; fx 7! sg is the environment which gives s on x, coincides with elsewhere; we use analogous notations for call traces. { se[v=x] is obtained by parallel substitution of variables x with values v. { fbody (f) returns the pair of the parameters and the body of the declaration of f, if any, in the assumed program.
Moreover, the rules are parametric in the following other judgments, for which di erent de nitions will be discussed in Sect. 4: { wd ( ; x; s), that is, by adding the association x 7! s to the (well-de ned) environment , we still get a well-de ned environment. { v v0, that is, the two values are equivalent in the environment4 . Then, is the extension of up to equivalence in : (f (v1; : : : ; vn)) = x i there exist v01; : : : ; v0n such that (f (v01; : : : ; v0n)) = x and vi v0i for i 2 1::n.
Intuitively, a closed result (s; ) is well-de ned if it denotes a unique stream (in nite sequence of numeric values), and a closed environment is well-de ned if, for each x 2 dom( ), (x; ) is well-de ned. In other words, the corresponding set of equations admits a unique solution. For instance, the environment fx 7! xg is not well-de ned, since it is undetermined (any stream satis es the equation x = x); the environment fx 7! x[+]y; y 7! 1 : yg is not well-de ned as well, since it is unde ned (the two equations x = x 7! x[+]y; y = 1 : y admit no solutions for x). Finally, two stream values s and s0 such that the results (s; ) and (s0; ) are closed and well-de ned are equivalent if they denote the same stream.
These notions 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 (pw), arguments are evaluated, while the stream operator is applied without
any further evaluation; the fact that the tail and pointwise operators are treated
as the stream constructor : is crucial to get results which denote non-regular
streams as shown in Sect. 3. However, when non-constructors are allowed to
occur in values, ensuring well-de ned results become more challenging, because
the usual simple syntactic constraints that can be safely used for constructors
[
The rules for function call use a mechanism of cycle detection, similar to
that in [
Rule (invk) is applied when a call is considered for the rst time, as expressed by the rst 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 from such variable to the result of the evaluation of the body keeps the environment well-de ned. If the check succeeds, then the nal 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.
Rule (corec) is applied when a call is considered for the second time, as expressed by the rst side condition (note that cycle detection takes place up to equivalence in the environment). 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 unde ned 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.
For instance, if we consider f()=g() g()=1:f(), then the judgment f(); ;; ; + (x; ), with = fx 7! y; y 7! 1 : xg, is derivable; however, while the nal result (x; ) is closed, the derivation contains also judgments with open results, as, e.g., f(); ;; ff() 7! x; g() 7! yg + (x; ;) and g(); ;; ff() 7! xg + (y; fy 7! 1 : xg).
As another example, if we consider f()=g(2:f()) g(s)=1:s, then the derivation of the judgment f(); ;; ; + (x; ) with = fx 7! y; y 7! 1 : 2 : xg is built on top of the derivation of g(2:x ); ;; ff() 7! xg + (y; fy 7! 1 : 2 : xg), corresponding to the evaluation of g(2:x ) where x is an operand of the stream constructor whose result is passed as argument to the call to g, despite x is not de ned yet.
Finally, rule (at) computes the i-th element of a stream expression. After evaluation of the arguments, the numeric result is obtained by the auxiliary judgment at (s; i) = n, inductively de ned in the bottom part of the gure. If the stream value is a variable, rule (at-var), then the evaluation is propagated to the associated stream value in the environment, if any. If, instead, the variable is free in the environment, then execution is stuck; again, an implementation should raise a runtime error instead. If the stream value is built by the constructor, then the result is the rst element of the stream if the index is 0, rule (at-cons-0); otherwise, the evaluation is recursively propagated to its tail with the predecessor index, rule (at-cons-n). Conversely, if the stream is built by the tail operator, rule (at-tail), then the evaluation is recursively propagated to the stream argument with the successor index. Finally, if the stream is built by a pointwise operation, rule (at-pw), then the evaluation is recursively propagated to the operands with the same index and then the corresponding arithmetic operation is computed on the results.
Derivations of examples in this section can be found in the extended version.
repeat (n) = n: repeat (n) one_two () = 1: two_one () two_one () = 2: one_two () First we show some simple examples, to explain how regular corecursion works. Then we provide some more signi cant examples.
Consider the following function declarations: With the standard semantics of recursion, the calls, e.g., repeat(0) and one_two() lead to non-termination. Thanks to regular corecursion, instead, these calls terminate, producing as result (x; fx 7! 0 : xg), and (x; fx 7! 1 : y; y 7! 2 : xg), 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, nally, the stream value 0 : x is associated in the environment with the result x of the initial call. 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. (value) (corec) one two(); ;; fone two() 7! x; two one() 7! yg + (x; ;) 2 : one two(); ;; fone two() 7! x; two one() 7! yg + (2 : x; ;)
two one(); ;; fone two() 7! xg + (y; fy 7! 2 : xg) 1 : two one(); ;; fone two() 7! xg + (1 : y; fy 7! 2 : xg)
one two(); ;; ; + (x; fx 7! 1 : y; y 7! 2 : xg)
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 once more, when the cyclic call is detected.
The following examples show function de nitions 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. nat () = 0:( nat ()[+] repeat (1)) nat_to_pow (n) = // nat_to_pow (n )( i )= i^n if n <= 0 then repeat (1) else nat_to_pow (n -1)[*] nat () fact () = 1:(( nat ()[+] repeat (1))[*] fact ()) pow (n) = 1:( repeat (n )[*] pow (n )) // pow (n )( i )= n^i fib () = 0:1:( fib ()[+] fib ()^) incr (s) = s [+] repeat (1)
The de nition of nat uses regular corecursion, since the recursive call nat() is cyclic. Hence the call nat() returns (x; fx 7! 0 : (x[+]y); y 7! 1 : yg). 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), returns (x2; fx2 7! x1[ ]x; x1 7! x0[ ]x; x0 7! y; y 7! 1 : y; x 7! 0 : (x[+]y0); y0 7! 1 : y0g): The de nitions of fact, pow, and fib are regularly corecursive. For instance, the call fact() returns (z; z 7! (x[+]y)[ ]z; x 7! 0 : (x[+]y0); y 7! 1 : y; y0 7! 1 : y0). The de nition of incr is non-recursive, hence always converges, and the call incr(s) returns (x; fx 7! s[+]y; y 7! 1 : yg). The following alternative de nition incr_reg (s) = (s (0)+1): incr_reg (s ^) relies, instead, on regular corecursion. Note the di erence: the latter version ensures termination only for regular streams, as in incr_reg(one_two()), since, eventually, in the recursive call, the expression s^ turns out to denote the initial stream; however, the computation does not terminate for non-regular streams, as in incr_reg(nat()), which, however, converges with incr.
The following function computes the stream of partial sums of the rst i + 1 elements of a stream s, that is, sum(s)(i)= Pik=0 s(k): sum (s) = s (0):( s ^[+] sum (s )) 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 rst i + 1 elements of the Taylor series of the exponential function: sum_expn (n) = sum ( pow (n )[/] fact ()) Function sum_expn calls sum with the argument pow(n)[/]fact() corresponding to the stream of all terms of the Taylor series of the exponential function; hence, by accessing the i-th element of the stream, we have the following approximation: sum expn(n)(i)= Pik=0 nkk! = 1 + n + n22! + n33! + n44! + i + ni! Lastly, we present a couple of examples showing how it is possible to de ne primitive operations provided by IoT platforms for real time analysis of data streams; we start with aggr(n,s), which allows aggregation (by addition) of contiguous data in the stream s w.r.t. a frame of length n: aggr (n ,s) = if n <=0 then repeat (0) else s [+] aggr (n -1 , s ^)
For instance, aggr(3,s) returns the stream s0 s.t. s0(i) = s(i)+s(i+1)+s(i+2). On top of aggr, we can easily de ne avg(n,s) to compute the stream of average values of s in the frame of length n: avg (n ,s) = aggr (n ,s )[/] repeat (n)
In the semantic rules, we have left unspeci ed two notions: well-de ned environments, and equivalent streams. We provide now a formal de nition in abstract terms. Then, we provide an operational de nition of well-de ned environments.
Semantically, a stream is an in nite 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 de nitions.
A substitution is a function from a nite set of variables to streams. We denote by JsK the stream obtained by applying to s, and evaluating operators, as formally de ned below.
JxK = (x)
(n i = 0 (Jn : sK )(i) = (JsK )(i 1) i 1 (Js^K )(i) = JsK (i + 1) i 0 (Js1[op]s2K )(i) = Js1K (i) op Js2K (i) i 0
Given an environment stitution [ ] is de ned by: Then, a solution of is a substitution with domain vars( ) such that [ ] = .
A closed environment is well-de ned if it has exactly one solution, denoted sol( ). For instance, fx 7! 1 : xg and fy 7! 0 : (y[+]x); x 7! 1 : xg are wellde ned, since their unique solutions map x to the in nite stream of ones, and y to the stream of natural numbers, respectively. Instead, for fx 7! 1[+]xg there are no solutions. Lastly, an environment can be undetermined: for instance, a substitution mapping x into an arbitrary stream is a solution of fx 7! xg.
An open environment is well-de ned if, for each with domain fv( ), it has exactly one solution 0 such that 0. For instance, the open environment fy 7! 0 : (y[+]x)g is well-de ned.
Given a closed result (s; ), with well-de ned, we de ne its semantics by JsK = JsK for = sol( ). Then, two stream values s and s0 are semantically equivalent in if JsK = Js0K 0.
We now consider the non-trivial problem of ensuring that a closed
environment is well-de ned; if environments would be allowed to contain only the
stream constructor, then it would su ce to require all non-free variables to be
guarded by the stream constructor [
However, when non constructors as the tail and pointwise operators come into play, the fact that variables are guarded by the stream constructor no longer ensures that the environment is well-de ned; for instance, the environment = fx 7! 0 : x^g corresponding to the de nition of bad_stream in Sect. 1 is not wellde ned since it admits in nite solutions (all streams starting with 0), although variable x is guarded by the stream constructor. A more complex check is needed: roughly, more constructors than tail operators should have been traversed when we nd a cyclic reference, as formalized in Fig. 3. m :: = x1 7! n1 : : : xn 7! nk (n
0) map from variables to natural numbers (main) wd(x; fx 7! vg; ;) wd ( ; x; v)
(wf-var) wd( (wx)d;(x;;m;fmx )7! 0g) x 62 dom(m) x 2 dom(m) (wf-corec) wd(x; ; m) m(x) > 0
(wf-fv) wd(x; ; m) x 62 dom( ) wd(s; ; m+1) (wf-cons) wd(n : s; ; m)
wd(s; ; m 1) (wf-tail) wd(s^; ; m) (wf-pw) wd(s1; ; m) wd(s2; ; m)
wd(s1[op]s2; ; m)
The judgment wd ( ; x; s) used in the side condition of rule (invk) holds if wd(x; fx 7! vg; ;) holds. The judgment wd(s; ; ;) means that a result is wellde ned. That is, restricting the domain of to the variables reachable from s (those either occurring in s, or, transitively, in values associated with reachable variables) we get a well-de ned environment; thus, wd ( ; x; s) holds if adding the association of s with x preserves well-de nedness of .
The additional argument m in the judgment wd(s; ; m) is a map from variables to natural numbers. We write m+1 and m 1 for the maps f(x; m(x) + 1) j x 2 dom(m)g, and f(x; m(x) 1) j x 2 dom(m)g, respectively.
In rule (main), this map is initially empty. In rule (wf-var), a variable x de ned in the environment is added in the map, with initial value 0, the rst time it is found. In rule (wf-corec), when it is found the second time, it is checked that more constructors than tail operators have been traversed. In rule (wf-fv), a free variable is considered well-de ned.5 In rules (wf-cons), (wf-tail), and (wf-pw), the value associated with a variable is incremented/decremented by one each time a constructor and tail operator are traversed, respectively.
As an example of derivation of well-de nedness and access to the i-th element, in Fig. 4 we consider the result (x; fx 7! 0 : (x [+] y); y 7! 1 : yg), obtained by evaluating the call nat() with nat de ned as in Sect. 3. 5 Indeed, non-well-de nedness can only be detected on closed results. (wf-cons) (wf-wcodre(c1)w:dy(;y;; f;xf x7!7!1;1y; y7!7!0g1)g) (wf-var) wd(y; ; fx 7! 1g) wd(x [+] y; ; fx 7! 1g) wd(0 : (x [+] y); ; fx 7! 0g)
wd(x; ; ;) (wf-pw)
(wf-corec) wd(x; ; fx 7! 1g) (wf-var)
(wf-cons) (at-var) (at-cons-n) (at-op) (at-var) (at-cons-0) at (0 : (x [+] y); 0) = 0 . .
. at (x; i 1) = i 1 (at-var)
at (x [+] y; i 1) = i at (0 : (x [+] y); i) = i at (x; i) = i (at-cons-0) at (1 : y; 0) = 1 . .
. at (y; i 1) = 1
In the extended version we show the derivation for a trickier example, that is, the result (x; fx 7! 0 : 1 : (2 : x^)^g). Its semantics is the stream 0; 1; 1; 1; : : :.
We show now that well-de nedness of a result is a necessary and su cient condition for termination of access to an arbitrary index. To formally express and prove this statement, we introduce some de nitions and notations.
First of all, since the numeric value obtained as 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 nite or in nite proof tree.
We write wd(s0; ; m0) ` wd(s; ; m) to mean that wd(s0; ; m0) is a premise of a (meta-)rule where wd(s; ; m) is the consequence, and `? for the re exive and transitive closure of this relation. Moreover, wd(x; ; m0) `?X wd(s; ; m), with x 62 X , means that in the path there can be nodes of shape wd(y; ; ) only for y 2 X and non-repeated. We use analogous notations for the judgment at (s; i). Lemma 1. 1. If at (x; i0) `?X at (s; i), then at (x; i0 + k) `?X at (s; i + k), for each k 0. 2. A judgment wd(s; ; ;) has no derivation i the following condition holds: (wf-stuck) wd(x; ; m0) `?X 0 wd( (x); ; mfx 7! 0g) ` wd(x; ; m) `?X wd(s; ; ;) for some x 2 dom( ), X 0; X , and m0; m s.t.
x 62 dom(m); m0(x) = k 0. 3. The derivation of at (s; j) is in nite i the following condition holds: (at-1) at (x; i + k) `?X 0 at ( (x); i) ` at (x; i) `X ? at (s; j) for some x 2 dom( ), X 0; X , and i; k 0.
Lemma 2. For x 2 dom(m), the following conditions are equivalent: 1. at (x; i0) `?X at (s; i) for some i0; i 2. wd(x; ; m0) `?X wd(s; ; m) for some m0 such that m0(x) = m(x) + i i0. 1) 2 By induction on the length of the path in at (x; i0) `?X ?aatt(s(;xi;)i.). We also BasheavTehwe dle(nx;gth;mof)t`h?e wpadt(hx;is ;0m,h)e,nacnedwmeh(xa)ve=amt((xx); i+) `i; i, as requested. Inductive step By c;ases on the rule applied to derive at (s; i). We show the most signi cant cases. (at-var) We have at (y; i), with y 6= x since the length of the path is > 0, and at (x; i0) `? nfyg at ( (y); i).
Moreover, we can derive wd(y; ; m) by rule (wf-var), and by inductive hypothesis we also have wd(x; ; m0) `? nfyg wd( (y); ; mfy 7! 0g), and m0(x) = mfy 7! 0g(x) + i i0, hence we get the thesis. (at-cons-0) Empty case, since the derivation for at (n : s; 0) does not contain a node at (x; i0). (at-cons) We have at (n : s; i), and at (x; i0) `?X at (s; i 1). Moreover, we can derive wd(n : s; ; m) by rule (wf-cons), and by in? wd(s; ; m+1), with ductive hypothesis we also have wd(x; ; m0) `X m0(x) = m+1(x) + (i 1) i0, hence we get the thesis. 2) 1 By induction on the length of the path in wd(x; ; m0) `? wd(s; ; m).
Base The length of the path is 0, hence we have wd(x; ; m) `? wd(x; ; m). ; We also have, for an arbitrary i, at (x; i) `? at (x; i), and m(x) = m(x)+ ; i i, as requested.
Inductive step By cases on the rule applied to derive wd(s; ; m). We show the most signi cant cases. (wf-var) We have wd(y; ; m), with y 2= dom(m), y 6= x since x 2 dom(m), and wd(x; ; m0) `?X nfyg wd( (y); ; mfy 7! 0g). By inductive hy? pothesis we have at (x; i0) `X nfyg at ( (y); i) for some i0; i such that m0(x) = m(x) + i i0. Moreover, since y 2 dom( ), at ( (y); i) ` at (y; i) by rule (at-var), hence we get at (x; i0) `? at (y; i). (wf-corec) Empty case, since the derivation for wd(y; ; m) would not contain a node wd(x; ; m). (wf-fv) Empty case, since the derivation for wd(y; ; m) would not contain a node wd(x; ; m). ? wd(s; ; m+1). (wf-cons) We have wd(n : s; ; m), and wd(x; ; m0) `X
By inductive hypothesis we have at (x; i0) `?X at (s; i) for some i0; i such that m0(x) = m+1(x)+i i0. Moreover, at (s; i) ` at (n:s; i+1) by rule (at-cons-n), hence we get at (x; i0) `? at (n : s; i + 1) with m0(x) = m(x) + i + 1 i0, as requested.
Lemma 3. For x 62 dom(m), the following conditions are equivalent: 1. at (x; i0) `?X at (s; i) for some i0; i 2. wd(x; ; m0) `?X wd(s; ; m) for some m0 such that x 62 dom(m0). Proof. Easy variant of the proof of Lemma 2.
Theorem 1. wd(s; ; ;) is derivable i , for all j, at (s; j) either has no derivation or a nite derivation. Proof. We prove that at (s; j) has an in nite derivation for some j i wd(s; ; ;) has no derivation. ) By Lemma 1-(3),we have that the following condition holds: ? ? at (s; j) (at-1) at (x; i + k) `X 0 at ( (x); i) ` at (x; i) `X
for some x 2 dom( ), X 0; X , and i; k 0.
Then, starting from the right, by Lemma 3 we have wd(x; ; m) `?X wd(s; ; ;) for some m such that x 62 dom(m); by rule (wf-var) we have wd( (x); ; mfx 7! 0g) ` wd(x; ; m), and nally by Lemma 2 we have: (wf-stuck) wd(x; ; m0) `X 0 wd( (x); ; mfx 7! 0g) ` wd(x; ; m) `?X wd(s; ; ;) ? for x 2 dom( ), X 0; X , and m0; m s.t. x 62 dom(m); m0(x) = k 0. hence we get the thesis. ( By Lemma 1-(2),we have that the condition (wf-stuck) above holds. Then, ? starting from the left, by Lemma 2 we have at (x; i0) `X 0 at ( (x); i) for some i0; i such that i i0 = k 0; by rule (at-var) we have at ( (x); i) ` at (x; i), and by Lemma 3 we have at (x; j0) `?X at (s; j) for some j0; j. If i = j0 + h, h 0, then by Lemma 1-(1) we have at (x; i + k) `X 0 at ( (x); i) ` at (x; i) `?X at (s; j + h)
? If j0 = i + h, h 0, then by Lemma 1-(1) we have at (x; i + k + h) `X 0 at ( (x); i) ` at (x; i + h) `?X at (s; j).
?
In both cases, the derivation of at (s; j) is in nite. 5
As mentioned in Sect. 1, our approach extends regular corecursion, where the
semantics keeps track of method/function calls. Regular corecursion originated
from co-SLD resolution [
There have been a few attempts of extending the expressive power of
regular corecursion. Notably, structural resolution [
For the operators considered in the calculus and some examples, our main
sources of inspiration have been the works of Rutten [
The problem of ensuring well-de ned corecursive de nitions has been also
considered in the context of type theory and proof assistants. We have shown in
Sect. 4 that simple guarded de nitions [
Lastly, D'Angelo et al. presented LOLA [
Our main technical result is Theorem 1, stating that passing the well-de nedness check performed at runtime for each function call is necessary and su cient to prevent non-termination in accessing elements in the resulting stream at an arbitrary index. In future work, we plan to also prove soundness of the operational well-de nedness with respect to its abstract de nition. Completeness does not hold, as shown by the example zeros() = repeat(0) [*] zeros() which is not well-de ned operationally, but admits as unique solution the stream of all zeros. On the other hand, the simplest operational characterization of equivalence of stream values is syntactic equivalence. This works for all the examples presented in this paper, but is, again, not complete with respect to the abstract de nition, as illustrated below: first ( s ) = s (0): first ( s ) // works with sy nt ac ti c e q u i v a l e n c e first2 ( s ) = s (0): first2 ( s (0): s ^) // does not work
Indeed, we get an in nite derivation for first2(repeat(1)) with call traces of increasing shape ffirst2(x) 7! y1; first2(1:x^) 7! y2; first2(1:(1:x^)^) 7! y3; : : :g in the environment fx 7! 1 : xg. In future work we plan to investigate more expressive operational characterizations of equivalence.