In recent work, non-regular streams have been defined corecursively, by representing them with finitary equational systems built on top of various operators, besides the standard constructor. With finitary equational systems based only on the stream constructor, one can use the free theory of regular (a.k.a. rational) trees to get a sound and complete procedure to decide whether two streams are equal. However, this is not the case if one allows other operators in equations, since the underlying equational theory becomes non-trivial, hence equality of regular trees is too strong to guarantee termination of corecursive functions defined even only with the constructor and tail operators. To overcome this problem, we provide a weaker definition of equality between streams denoted by finitary equational systems built on diferent stream operators, including tail operator and constructor, and prove its soundness.
In recent work [
This mechanism generalizes regular corecursion [
nat() = 0:(nat()[+] repeat(1))
Such an augmented expressive power comes at some price: (1) conditions on equational systems
are needed to ensure unique solutions and (2) equality on streams becomes more complex. While
previous work [
However, while the theory of regular trees is free, when one allows in the equational systems operators which are not constructors, the underlying equational theory becomes non-trivial and, hence, equality of regular trees is too strong; for instance, it fails to identify (x, {x ↦→ 1:x}) and (y, {x ↦→ 1:x, y ↦→ x^}) where _^ is the tail operator. This has a negative impact on cycle detection, which is based on equality of function calls to avoid non termination: if a suitable notion of equality is not adopted, then the augmented expressive power achieved with finite representations of non-regular streams is partially lost. Indeed, some function calls may not terminate since cycle detection fails.
After recalling the calculus in Sect. 2, in Sect. 3 we provide our definition of equality and prove its soundness, in the sense that getting the -th element of provably equal stream expressions gives the same result. In Sect. 4 we show examples of equality checks, Sect. 5 provides an alternative definition of equality, which ensures termination in the positive case by a cycle detection mechanism, and in Sect. 6 we discuss further work. 1See for instance, the support for cyclic terms in SWI-Prolog https://www.swi-prolog.org/pldoc/man?section=cyclic
In this section we present the calculus and discuss its features. Fig. 1 shows the syntax.
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 (denoted by a caret), pointwise arithmetic
operations and the interleaving operator (‖), giving a stream whose elements are alternatively
those of the arguments. This latter operator is interesting because it cannot be derived from
the others; indeed, implementing the interleaving with just a recursive call involving the first
element and the tail of a stream would only work for cyclic streams. Numeric expressions
include the access to the -th2 element of a stream. We use fd to denote a sequence fd1, . . . , fd,
with ≥ 0, of function declarations, and analogously for other sequences.3
The operational semantics, given in Fig. 2, is based on two key ideas:
1. streams are represented with finitary equational systems built with the aforementioned
stream operators
2. evaluation keeps track of already considered calls to allow cycle detection
To obtain point (1), an equational system is modeled by an environment mapping a finite
set of variables into (open) stream values s, built on top of stream variables, numeric values and
the stream operators; consequently, the result of the evaluation of a stream expression is a pair
(s, ), similarly as done with capsules [
To obtain point (2), evaluation has an additional parameter which is a call trace, a map from function calls where arguments have been evaluated, that is, of shape f(v) (calls for short), into variables.
Altogether, the semantic judgment has shape e, , ⇓ (v, ′), where e is the expression to be evaluated, the current environment defining variables 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: 2For 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. 3Hence, declarations and calls of constant functions are included. v s , n b :: = :: = :: = :: = :: = :: = :: = f(v) s | n | b c1 ↦→ x1 . . . c ↦→ x ( ≥ {x1 ↦→ s1 . . . x ↦→ s} ( ≥ 0) 0) (evaluated) call value • ⊔ ′ 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. • 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, rules for calls depend on an equality judgment v1 ≈ v2, which will be defined in Sect. 3, stating that v1 and v2 are considered equal in the environment . Indeed, look-up of a call in the the call trace is performed modulo equality, that is: • c ≈ c′ if c = f(v1, . . . , v), c′ = f(v′1, . . . , v′) and v ≈ v′ for all ∈ 1.. • ≈ (c) = x if (c′) = x, c′ ≈ c for some c′ • hence, c ̸∈ dom( ≈ ) if there is no c′ ∈ dom( ) s.t. c ≈ c′.
Rules for values and conditional are straightforward. In rules (cons), (tail) and (op), arguments are evaluated, while the stream operator is applied without any further evaluation.
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 first time, as expressed by the first side condition. The body is retrieved by the auxiliary function fbody, and evaluated in a call trace where the call has been mapped into a fresh variable.
Rule (corec) is applied when a call is considered for the second time, as expressed by the side condition ≈ (c) = x, which means that, in the call trace, a variable was already associated with some c′ considered equivalent to c; indeed, as already explained, cycle detection takes place up to equality in the environment. At this point, 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; e.g., 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 = {x ↦→ y, y ↦→ 1:x}, is derivable; however, while the final result (x, ) is closed, the derivation contains also judgments with open results, as, e.g., f(), ∅, {f() ↦→ x, g() ↦→ y} ⇓ (x, ∅) and g(), ∅, {f() ↦→ x} ⇓ (y, {y ↦→ 1:x}).
Finally, rule (at) computes the -th element of a stream expression. After evaluation of the arguments, the numeric result is obtained by the auxiliary judgment at (s, )=n, inductively defined at the bottom of the figure.
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 the execution is stuck; an implementation should raise a runtime error
instead. Rules (at-‖-even) and (at-‖-odd) handle the interleaving operator. The first one is used
for even indexes, and propagates the evaluation to the left-hand side stream; analogously, for
odd indexes, the second rule is applied and the evaluation is propagated to the right-hand side
stream. The remaining rules are self-explanatory; for examples of derivations in this calculus,
we point the reader to [
In this section, we consider the problem of the equality of values. As discussed in the Introduction, and shown in the operational semantics in Fig. 2, this issue is relevant not only to provide an equality operator which can be used by the programmer, but also for cycle detection in calls. To illustrate the second issue we show an example. ones() = 1:ones() incr_reg(s) = (s(0)+1) : incr_reg(s^)
Intuitively, the result of incr_reg(ones()) should be the stream consisting of infinite occurrences of number 2. However, it is easy to see that this is not the case if cycle detection is based on mere syntactic equality. Indeed, if incr_reg is called on ones(), that is, on the result (x, {x ↦→ 1:x}), then incr_reg is recursively called on (x^, {x ↦→ 1:x}) and cycle detection fails because x and x^ are not syntactically equal, despite they denote the same stream. This leads to non-termination, since rule (corec) will never be applied.
Again as anticipated in the Introduction, the first step towards a more expressive definition is
to consider equality in the free theory of regular terms, as in [
In order to deal with the tail operator, our solution is based on the key idea that the equality check performs a partial symbolic evaluation of the tail. For instance, with this solution the example incr_reg(ones()) is correctly handled, since the symbolic evaluation of the tail of (x, {x ↦→ 1:x}) returns (x, {x ↦→ 1:x}).
The equality check is formalized by the judgment s1 ≈ s2, coinductively defined in Fig. 3. In rules (var-l) and (var-r), a variable defined in the environment is equal to a stream value if the same holds for its associated stream value. In rule (var), a variable is equal to itself. In rule (cons), prepending the same element to equal streams gives equal streams. Analogously, in rule (tail-tail), the tails of two equal streams are equal. In rule (op), two streams defined using the same binary operation are equal if their arguments are respectively equal.
The most interesting rules are those handling the case when one of the two sides of the equality is of shape s^. Indeed, in such cases an attempt is made at computing (a stream value equal to) the tail of s, through the auxiliary judgment Tail (s)=s′ defined at the bottom of the ifgure. 5 Function Tail is inductively defined, and the base case is the constructor, rule (tailcons), where the result is simply the tail stream. In the other cases, the function is propagated as expected. In particular, in rule (tail), to obtain the result we need two subsequent applications of Tail , the former getting the tail of the argument. Note also, in rule (‖), that, given a stream 4As further discussed at the end of this section, for regular terms the coinductive definition can be turned into an equivalent inductive and algorithmic one. 5Note the diference between this judgment and the notation s^ which is part of the syntax of streams (Fig. 1). x1 ↦→ s1 . . . x ↦→ s (≥ 0) environment binary stream operator (var-l) x ≈ s (x) ≈ s (var-r) s ≈s ≈ (xx) (var) x ≈ x
s1 ≈ s2 (cons) n:s1 ≈ n:s2 (op) ss11 o≈p s2s′1≈ s2s′1≈ o p ss′2′2 those of the second argument and the tail of the first.
To explain what does it mean that the definition of the judgment s1 ≈ s2 in Fig. 3 is
coinductive, we briefly recall some notions on inference systems [
are those with a finite proof tree, whereas the set of judgments coinductively defined
are those with an either finite or infinite proof tree. In our case, the coinductive
definition is the most natural and abstract for infinite objects such as streams, and is convenient
for the soundness proof. It is possible to provide an alternative inductive definition by following
the standard technique, adopted in co-SLD resolution [
We now prove the soundness of the equality check. That is, if we derive that two streams are equal, then they are equal in the sense that access to an arbitrary index will give the same result. Soundness of the equality check (Theorem 3.2) relies on soundness of the Tail judgment (Theorem 3.1). To the aim of the proof of Theorem 3.2, we introduce the notation at (s, + 1) = n, meaning that the proof tree of at (s, + 1)=n has depth .
Theorem 3.1. If Tail (s)=s′ holds, then, for all , ≥ 0, at (s, + 1) = n implies at (s′, )=′ n for some ′≤ .
Proof. By induction on the rules defining Tail (s)=s′. (tail-cons) This is an axiom with conclusion Tail (n:s)=s. We have to show that, for all ≥ 0, at (n:s, + 1) = n implies at (s, )=′ n with ′≤ , and this is true since at (n:s, + 1) = n is necessarily derived from at (s, )=−1n by rule (at-cons-succ). (var) Tail ( (x))=s is the premise and Tail (x)=s the conclusion. We have to show that, for all ≥ 0, at (x, + 1) = n implies at (s, )=′ n with ′≤ . Since at (x, + 1) = n is necessarily derived from at ( (x), + 1)=−1n by rule (at-var), by inductive hypothesis we have at (s, )=′ n with ′≤ − 1<. (tail) Tail (s)=s′, Tail (s′)=s′′ are the premises, and Tail (s^)=s′′ the conclusion. We have to show that, for all ≥ 0, at (s^, + 1) = n implies at (s′′, )=′′n with ′′≤ . Since at (s^, + 1) = n is necessarily derived from at (s, +2)=−1n by rule (at-tail), by inductive hypothesis on the first premise we have at (s′, + 1)=′ n, with ′≤ − 1<. Moreover, by inductive hypothesis on the second premise, we have at (s′′, )=′′n, with ′′≤ ′≤ − 1<. (nop) Tail (s1)=s′1, Tail (s2)=s′2 are the premises, and Tail (s1[nop]s2)=s′1[nop]s′2 the conclusion. We have to show that, for all ≥ 0, at (s1[nop]s2, + 1) = n implies at (s′1[nop]s′2, )=′ n with ′≤ . Since at (s1[nop]s2, + 1) = n is necessarily derived from at (s1, + 1)=−1n1 and at (s2, + 1)=−1n2, with n = n1 nop n2, by rule (atnop), by inductive hypothesis on the first and second premise we have at (s′1, )=1n1 and at (s′2, )=2n2 with 1, 2≤ − 1, respectively. Hence, by rule (at-nop), we have at (s′1[nop]s′2, )=′ n1 nop n2 = n, with ′ = max(1, 2) + 1≤ − 1 + 1 = . (‖) Tail (s1)=s′1 is the premise and Tail (s1 ‖ s2)=s2 ‖ s′1 the conclusion. We have to show that, for all ≥ 0, at (s1 ‖ s2, + 1) = n implies at (s2 ‖ s′1, )=′ n with ′≤ . The proof proceeds by case analysis on the parity of : even: at (s1 ‖ s2, + 1) = n is necessarily derived from at (s2, 2 )=−1n by rule (at-‖-odd); hence, by rule (at-‖-even) we have at (s2 ‖ s′1, )=′ n with ′ = . odd: at (s1 ‖ s2, + 1) = n is necessarily derived from at (s1, +21 )=−1n by rule (at-‖even); that is, at (s1, − 21 + 1)=−1n, hence, by inductive hypothesis, at (s′1, − 21 )=′′n with ′′≤ − 1. Finally, by rule (at-‖-odd) we have at (s2 ‖ s′1, )=′ n with ′ = ′′ + 1≤ . Theorem 3.2. For all ≥ 0, if at (s, )=n, at (s′, )=n′, and s ≈ s′, then n = n′. Proof. Assume that at (s, ) = n, at (s′, )=′ n′. The proof is by Noetherian induction on the pairs (, ′), with the componentwise order, that is, (1, 2)≤ (1′, 2′) if 1≤ 1′ and 2≤ 2′. Base We consider the pair (0, 0), that is, the case when the two judgments are derived by axiom (at-cons-0), hence, for = 0. We have at (n:s, 0)=n, and at (n′:s′, 0)=n′. Moreover, we have n:s ≈ n′:s′, which has been necessarily derived by rule (cons), hence n=n′. Inductive step We consider pairs (, ′) where either >0 or ′>0, and proceed by case analysis on the (last) rule applied to derive the judgment s ≈ s′. (var-l) We have x ≈ s and (x) ≈ s. Moreover, we have at (x, ) = n, at (s, )=′ n′ and, since the former judgment has been necessarily derived by rule (at-var), at ( (x), )=−1n. We apply the inductive hypothesis and get the thesis. (var-r) This case is symmetrical to the one above. (var) We have x ≈ x. We conclude by the fact that the judgment at (s, )=n is deterministic, therefore at (x, )=n1 and at (x, )=n2 implies n1 = n2. (cons) We have :s ≈ ′:s′ and s ≈ s′. Moreover, we have at (:s, ) = n, at (′:s′, )=′ n′ and, since >0 or ′>0, we have >0 and these judgments at (s′, − 1)′=−1n′. We apply the inductive hypothesis and get the thesis.
have been necessarily derived by rule (at-cons-succ); therefore, at (s, − 1)=−1n, (tail-tail) We have s^≈ s′^ and s≈ s′. Moreover, we have at (s^, ) = n, at (s′^, )=′ n′ and, since these judgments have been necessarily derived by rule (at-tail), at (s, + 1)=−1n, and at (s′, + 1)′=−1n′. We apply the inductive hypothesis and get the thesis. (op) By cases on the binary operator op.
(nop): We have s1 [nop] s2 ≈ s′1 [nop] s′2, s1 ≈ s′1 and s2 ≈ s′2. Moreover, we have at (s1 [nop] s2, ) = n, at (s′1 [nop] s′2, )=′ n′ and, since these judgments have been necessarily derived by rule (at-nop), at (s1, )=−1, at (s2, )=−1, at (s′1, )′=−1′, at (s′2, )′=−1′, n = nop , n′ = ′ nop ′. We apply the inductive hypothesis and get the thesis. (‖): By cases on the parity of . even: We have s1 ‖ s2 ≈ s′1 ‖ s′2 and s1 ≈ s′1. Moreover, we have at (s1 ‖ s2, ) = n, at (s′1 ‖ s′2, )=′ n′ and, since these judgments have been necessarily derived by rule (at-‖-even), at (s1, 2 )=−1, at (s′1, 2 )′=−1′. We apply the inductive hypothesis and get the thesis.
odd: This case is symmetrical to the one above. (tail-r) We have s1≈ s2^ and s1≈ s′, with Tail (s2)=s′. Moreover, we have at (s1, ) = n, at (s2^, )=′ n′ and, since the latter judgment has been necessarily derived by rule (at-tail), at (s2, + 1)′=−1n′. From Theorem 3.1 we have that at (s′, )=′′n′ with ′′≤ ′ − 1<′. We apply the inductive hypothesis and get the thesis.
(tail-l) This case is symmetrical to the one above.
We illustrate how the equality check works by some examples. The first one is shown in Fig. 4. . .
.
x ≈ ^^ 1 : x ≈ 1 : ^^ (var-l) (cons)
Tail (y^)=1 : ^^ 1 : x ≈ ^^
(var-l) x ≈ ^^
In this proof tree, rule (var-l) is applied first, and then rule (tail-r); we could have applied the rules in the other order as well. The proof tree of Tail (y^)=1 : ^^ is shown in the bottom part of the figure. The result is computed by applying twice the tail operator, and unfolding y. Then, in the main proof tree, rule (cons) is applied since the first element of both streams is 1. It is easy to see that there is a regular infinite proof tree, denoted by the dots.
In the second one, in Fig. 5, we show how the equality check deals with non-regular streams. . .
. x ≈ y (var-l) . .
. x ≈ y (var-l) (op)
Here, both x and y denote the stream of all powers of 2. The derivation starts with the unfolding of both variables, followed by the application of rule (cons). Then, the tail of the second component is computed, with the proof tree shown as additional premise in rule (tail-r). After that, the derivation continues by distributing the equality check to the substreams x and y. It is easy to see that there is a regular infinite proof tree, denoted by the dots.
We provide an alternative definition of equality, which ensures termination in the positive case by a cycle detection mechanism. The judgment ⊢ s1 ≈ s2, defined in Fig. 6, means that s1 and s2 are equal in under the equality trace , containing coinductive hypotheses as pairs of already considered stream values. The trace is abstractly considered as a set, so order and repetitions are immaterial.
:: = (s1, s′1) . . . (s, s′)
( ≥ 0) (var-l) · (x, s) ⊢ (x) ≈ s (var-r) · (s, x) ⊢ s ≈ (x) ⊢ s ≈ x (var) ⊢ x ≈ x
⊢ s1 ≈ s2 (cons) ⊢ n:s1 ≈ n:s2
The rules are analogous to those in Fig. 3, except that in (var-l) and (var-r) considered pairs
are added as coinductive hypotheses in the trace, and rule (corec) states that two stream values
are equal if the same pair is contained in the trace of coinductive hypotheses, that is, it has
been already considered. The function Tail is that defined in Fig. 3. Whereas the judgment
s1 ≈ s2 in Fig. 3 is defined coinductively, the judgment ⊢ s1 ≈ s2 is defined inductively. The
soundness of ∅ ⊢ s1 ≈ s2 with respect to s1 ≈ s2 follows from a general result proved in [
We provided an operational characterization of equality between streams which goes beyond equality of regular terms, by performing a partial symbolic evaluation of the tail operator.
Such operational characterization has been described by a coinductive inference system, that
is, infinite derivations are allowed. This description is very natural and abstract, and convenient
for the soundness proof, but clearly non-algorithmic. Thus, the first objective for future work is
to provide a sound algorithm to check equality. To this end, the first step, shown in Sect. 5, is to
convert the coinductive definition into an inductive one, where derivations are finite. This has
been done by the standard technique, adopted in co-SLD resolution [
The following further steps are required to actually get an algorithm sound and complete w.r.t. the coinductive definition in Fig. 3, that is, a procedure which always terminates and returns a positive answer if s1 ≈ s2 is derivable: 1. a proof that there exists a sound and complete algorithm for the judgment Tail (s)=s′; 2. a proof that derivation trees for s1 ≈ s2 are all regular, that is, the set of checked pairs is ifnite . This is not so simple as happens for equality of regular terms, because checking that s1 ≈ s2 is derivable needs inspection of not only the sub-terms of s1 and s2, but also the possibly new terms generated by the symbolic computation of tail.
Another issue for further research is completeness; indeed, the characterization proposed in this work fails to capture some laws that hold in the equational theory defined by index access. For instance, if = {x ↦→ 0 : }, then, for all ≥ 0, at (x, )=at (x [+] x, )=at (x ‖ x, )=0 holds, while x ≈ x [+] x and x ≈ x ‖ x are not derivable according to the definition in Fig. 3. Hence, a long-term goal is to investigate more expressive definitions of equality, and decidability of equality for (fragments of) the stream calculus.