11institutetext: DIBRIS, University of Genova

# Enhancing expressivity
of checked corecursive streams (extended version)

Davide Ancona  Pietro Barbieri  Elena Zucca

###### Abstract

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.

###### Keywords:

operational semantics stream programming runtime checking

##  1 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.

⬇

get_elem 3 (one_two)\-- evaluates to 2

get_elem 3 (from 5)\-- evaluates to 7

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
$\textit{x}=1:2:\textit{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 corecursion111Here we use the syntax of our
calculus, where, differently from Haskell, functions are uncurried, that is,
take as arguments possibly empty tuples delimited by parentheses. 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 well-definedness check non-trivial, but still decidable.

The main formal results are (1) Theorem 4.1 stating the soundness of the
runtime check; (2) Theorem 5.1 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.

##  2 Stream calculus

Fig. 1 shows the syntax of the calculus.

$\begin{array}[t]{llll}\overline{\textit{fd}}&{:}{:}=&\textit{fd}_{1}\ldots\textit{fd}_{n}&\mbox{{\small{program}}}\\\
\textit{fd}&{:}{:}=&\textit{f}(\overline{\textit{x}})=\textit{se}&\mbox{{\small{function
declaration}}}\\\
\textit{e}&{:}{:}=&\textit{se}\mid\textit{ne}\mid\textit{be}&\mbox{{\small{expression}}}\\\
\textit{se}&{:}{:}=&\textit{x}\mid{\texttt{if}\mathrel{\textit{be}}\texttt{then}}\mathrel{\textit{se}_{1}}{\texttt{else}\mathrel{\textit{se}_{2}}}\mid{\textit{ne}}\mathbin{\texttt{:}}{\textit{se}}\mid{\textit{se}}{\char
94\relax}\mid{\textit{se}_{1}{\textit{op\
}}\textit{se}_{2}}\mid\textit{f}(\overline{\textit{e}})&\mbox{{\small{stream
expression}}}\\\
\textit{ne}&{:}{:}=&\textit{x}\mid\textit{se}(\textit{ne})\mid{\textit{ne}_{1}\mathop{\textit{nop}}\textit{ne}_{2}}\mid
0\mid 1\mid 2\mid...&\mbox{{\small{numeric expression}}}\\\
\textit{be}&{:}{:}=&\textit{x}\mid\texttt{true}\mid\texttt{false}\mid...&\mbox{{\small{boolean
expression}}}\\\ \textit{op\
}&{:}{:}=&[{\textit{nop}}]\mid\|&\mbox{{\small{binary stream operator}}}\\\
\textit{nop}&{:}{:}=&+\ \mid\ -\ \mid\ *\ \mid\ /&\mbox{{\small{numeric
operator}}}\end{array}$

Figure 1: Stream calculus: syntax

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$-th222For simplicity, here indexing
and numeric expressions coincide. element of a stream. We use
$\overline{\textit{fd}}$ to denote a sequence
$\textit{fd}_{1},\dots,\textit{fd}_{n}$ of function declarations, and
analogously for other sequences.

The operational semantics, given in Fig. 2, is based on two key ideas:

  1. 1.

some infinite streams can be represented in a finite way

  2. 2.

evaluation keeps trace of already considered function calls

$\begin{array}[t]{llll}\mathit{c}&{:}{:}=&\textit{f}(\overline{\textit{v}})&\mbox{{\small{{(evaluated)}
call}}}\\\
\textit{v}&{:}{:}=&\textit{s}\mid\textit{n}\mid\textit{b}&\mbox{{\small{value}}}\\\
\textit{s}&{:}{:}=&\textit{x}\mid{\textit{n}}\mathbin{\texttt{:}}{\textit{s}}\mid{\textit{s}}{\char
94\relax}\mid\textit{s}_{1}{\textit{op\
}}\textit{s}_{2}&\mbox{{\small{{{(open)} stream value}}}}\\\
{i,\textit{n}}&{:}{:}=&0\mid 1\mid 2\mid...&\mbox{{\small{{index, numeric
value}}}}\\\
\textit{b}&{:}{:}=&\texttt{true}\mid\texttt{false}&\mbox{{\small{boolean
value}}}\\\ \tau&{:}{:}=&\mathit{c}_{1}\mapsto\textit{x}_{1}\ \ldots\
\mathit{c}_{n}\mapsto\textit{x}_{n}\hskip 7.20003pt(n\geq
0)&\mbox{{\small{call trace}}}\\\
\rho&{:}{:}=&{\textit{x}_{1}\mapsto\textit{s}_{1}\ldots\textit{x}_{n}\mapsto\textit{s}_{n}}\hskip
7.20003pt(n\geq 0)&\mbox{{\small{environment}}}\\\ \end{array}$

$\begin{array}[]{l}\\\
{\tiny\textsc{({val})}}\displaystyle\frac{}{{\textit{v},\rho,\tau}\\!\Downarrow\\!({{\textit{v}},{\rho}})}\
\begin{array}[]{l}\end{array}\hskip
7.20003pt{\tiny\textsc{({if-t})}}\displaystyle\frac{{\textit{be},\rho,\tau}\\!\Downarrow\\!({{\texttt{true}},{\rho}})\hskip
7.20003pt{\textit{se}_{1},{\rho},\tau}\\!\Downarrow\\!({{\textit{s}},{\rho^{\prime}}})}{{{\texttt{if}\mathrel{{\textit{be}}}\texttt{then}}\mathrel{\textit{se}_{1}}{\texttt{else}\mathrel{\textit{se}_{2}}},\rho,\tau}\\!\Downarrow\\!({{\textit{s}},{{\rho^{\prime}}}})}\
\begin{array}[]{l}\end{array}\hskip
7.20003pt{\tiny\textsc{({if-f})}}\displaystyle\frac{{\textit{be},\rho,\tau}\\!\Downarrow\\!({{\texttt{false}},{{\rho}}})\hskip
7.20003pt{\textit{se}_{2},{\rho},\tau}\\!\Downarrow\\!({{\textit{s}},{{\rho^{\prime}}}})}{{{\texttt{if}\mathrel{{\textit{be}}}\texttt{then}}\mathrel{\textit{se}_{1}}{\texttt{else}\mathrel{\textit{se}_{2}}},\rho,\tau}\\!\Downarrow\\!({{\textit{s}},{{\rho^{\prime}}}})}\
\begin{array}[]{l}\end{array}\\\\[23.24991pt]
{\tiny\textsc{({cons})}}\displaystyle\frac{{\textit{ne},\rho,\tau}\\!\Downarrow\\!({{\textit{n}},{\rho}})\hskip
7.20003pt{\textit{se},\rho,\tau}\\!\Downarrow\\!({{\textit{s}},{\rho^{\prime}}})}{{{\textit{ne}}\mathbin{\texttt{:}}{\textit{se}},\rho,\tau}\\!\Downarrow\\!({{{\textit{n}}\mathbin{\texttt{:}}{\textit{s}}},{\rho^{\prime}}})}\
\begin{array}[]{l}\end{array}\hskip
13.50002pt{\tiny\textsc{({tail})}}\displaystyle\frac{{\textit{se},\rho,\tau}\\!\Downarrow\\!({{\textit{s}},{\rho^{\prime}}})}{{{\textit{se}}{\char
94\relax},\rho,\tau}\\!\Downarrow\\!({{{\textit{s}}{\char
94\relax}},{\rho^{\prime}}})}\ \begin{array}[]{l}\end{array}\hskip
13.50002pt{{\tiny\textsc{({op})}}\displaystyle\frac{{\textit{se}_{1},\rho,\tau}\\!\Downarrow\\!({{\textit{s}_{1}},{\rho_{1}}})\hskip
7.20003pt{\textit{se}_{2},\rho,\tau}\\!\Downarrow\\!({{\textit{s}_{2}},{\rho_{2}}})}{{\textit{se}_{1}{\textit{op\
}}\textit{se}_{2},\rho,\tau}\\!\Downarrow\\!({{\textit{s}_{1}{\textit{op\
}}\textit{s}_{2}},{\rho_{1}\sqcup\rho_{2}}})}\
\begin{array}[]{l}\end{array}}\\\\[23.24991pt]
{{\tiny\textsc{({args})}}\displaystyle\frac{\begin{array}[]{l}{\textit{e}_{i},\rho,\tau}\\!\Downarrow\\!({{\textit{v}_{i}},{{\rho_{i}}}})\hskip
7.20003pt\forall i\in 1..n\hskip
13.50002pt{\textit{f}(\overline{\textit{v}}),{{\widehat{\rho}}},\tau}\\!\Downarrow\\!({{\textit{s}},{{\rho^{\prime}}}})\end{array}}{{\textit{f}(\overline{\textit{e}}),\rho,\tau}\\!\Downarrow\\!({{\textit{s}},{{\rho^{\prime}}}})}\
\begin{array}[]{l}\overline{\textit{e}}=\textit{e}_{1},\ldots,\textit{e}_{n}\
\mbox{not of shape}\ \overline{\textit{v}}\\\
\overline{\textit{v}}=\textit{v}_{1},\ldots,\textit{v}_{n}\\\
{\widehat{\rho}}=\bigsqcup_{i\in 1..n}\rho_{i}\end{array}\par}\\\\[23.24991pt]
{{\tiny\textsc{({invk})}}\displaystyle\frac{\begin{array}[]{l}{\textit{se}[\overline{\textit{v}}/\overline{\textit{x}}],\rho,\tau\\{\textit{f}(\overline{\textit{v}})\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{s}},{{\rho^{\prime}}}})\end{array}}{{\textit{f}(\overline{\textit{v}}),\rho,\tau}\\!\Downarrow\\!({{{\textit{x}}},{{\rho^{\prime}}\\{\textit{x}\mapsto\textit{s}\\}}})}\
\begin{array}[]{l}{\textit{f}(\overline{\textit{v}})\not\in\mathit{dom}({\tau})}\\\
\textit{x}\ \mbox{fresh}\\\
\mathit{fbody}(\textit{f})=({{\overline{\textit{x}}},{\textit{se}}})\\\
\mathit{wd}({\rho^{\prime}},\textit{x},\textit{s})\end{array}}\hskip
13.50002pt{{\tiny\textsc{({corec})}}\displaystyle\frac{}{{\textit{f}(\overline{\textit{v}}),\rho,\tau}\\!\Downarrow\\!({{\textit{x}},{\rho}})}\
\begin{array}[]{l}{\tau}({f(\overline{\textit{v}})})=\textit{x}\\\
\end{array}}\\\\[30.99988pt]
{\tiny\textsc{({at})}}\displaystyle\frac{{\textit{se},\rho,\tau}\\!\Downarrow\\!({{\textit{s}},{{\rho^{\prime}}}})\hskip
7.20003pt{\textit{ne},\rho,\tau}\\!\Downarrow\\!({{i},{\rho}})\hskip
7.20003pt}{{\textit{se}(\textit{ne}),\rho,\tau}\\!\Downarrow\\!({{\textit{n}},{{\rho}}})}\
\begin{array}[]{l}\mathit{at}_{\rho^{\prime}}(\textit{s},i)=\textit{n}\end{array}\\\\[23.24991pt]
\hline\cr\\\ {\tiny\textsc{({at-
var})}}\displaystyle\frac{\mathit{at}_{\rho}(\rho(\textit{x}),i)=\textit{n}^{\prime}}{\mathit{at}_{\rho}(\textit{x},i)=\textit{n}^{\prime}}\
\begin{array}[]{l}\end{array}\hskip 13.50002pt{\tiny\textsc{({at-
cons-0})}}\displaystyle\frac{}{\mathit{at}_{\rho}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},0)=\textit{n}}\
\begin{array}[]{l}\end{array}\hskip 13.50002pt{{\tiny\textsc{({at-cons-
succ})}}\displaystyle\frac{\mathit{at}_{\rho}(\textit{s},i)=\textit{n}^{\prime}}{\mathit{at}_{\rho}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},i+1)=\textit{n}^{\prime}}\
\begin{array}[]{l}\end{array}}\\\\[23.24991pt] {\tiny\textsc{({at-
tail})}}\displaystyle\frac{\mathit{at}_{\rho}(\textit{s},i+1)=\textit{n}}{\mathit{at}_{\rho}({\textit{s}}{\char
94\relax},i)=\textit{n}}\ \begin{array}[]{l}\end{array}\hskip
13.50002pt{\tiny\textsc{({{at-
nop}})}}\displaystyle\frac{\mathit{at}_{\rho}(\textit{s}_{1},i)=\textit{n}_{1}\hskip
7.20003pt{\mathit{at}_{\rho}(\textit{s}_{2},i)=\textit{n}_{2}}}{\mathit{at}_{\rho}(\textit{s}_{1}{[{\textit{nop}}]}\textit{s}_{2},i)=\textit{n}_{1}\mathbin{\textit{nop}}\textit{n}_{2}}\
\begin{array}[]{l}\end{array}\\\\[23.24991pt]
{{\tiny\textsc{({at-$\|$-even})}}\displaystyle\frac{\mathit{at}_{\rho}(\textit{s}_{1},i)=\textit{n}}{\mathit{at}_{\rho}(\textit{s}_{1}\|\textit{s}_{2},2i)=\textit{n}}\
\begin{array}[]{l}\end{array}\hskip
13.50002pt{\tiny\textsc{({at-$\|$-odd})}}\displaystyle\frac{\mathit{at}_{\rho}(\textit{s}_{2},i)=\textit{n}}{\mathit{at}_{\rho}(\textit{s}_{1}\|\textit{s}_{2},2i+1)=\textit{n}}\
\begin{array}[]{l}\end{array}}\end{array}$

Figure 2: Stream calculus: operational semantics

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 $({{\textit{s}},{\rho}})$, 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 $\rho$ is an _environment_ mapping variables into
stream values. In this way, cyclic streams can be obtained: for instance,
$({{\textit{x}},{\textit{x}\mapsto{\textit{n}}\mathbin{\texttt{:}}{\textit{x}}}})$
denotes the stream constantly equal to n.

We denote by $\mathit{dom}(\rho)$ the domain of $\rho$, by
$\textit{vars}(\rho)$ the set of variables occurring in $\rho$, by
$\textit{fv}(\rho)$ the set of its free variables, that is,
$\textit{vars}(\rho)\setminus\mathit{dom}(\rho)$, and say that $\rho$ is
_closed_ if $\textit{fv}(\rho)=\emptyset$, _open_ otherwise, and analogously
for a result $({{\textit{v}},{\rho}})$.

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
${\textit{e},\rho,\tau}\\!\Downarrow\\!({{\textit{v}},{{\rho^{\prime}}}})$,
where e is the expression to be evaluated, $\rho$ the current environment
defining possibly cyclic stream values that can occur in e, $\tau$ the call
trace, and $({{\textit{v}},{{\rho^{\prime}}}})$ the result. The semantic
judgments should be indexed by an underlying (fixed) program, omitted for sake
of simplicity. Rules use the following auxiliary definitions:

  * •

$\rho\sqcup\rho^{\prime}$ is the union of two environments, which is well-
defined if they have disjoint domains; $\rho\\{\textit{x}\mapsto\textit{s}\\}$
is the environment which gives s on x, coincides with $\rho$ elsewhere; we use
analogous notations for call traces.

  * •

$\textit{se}[\overline{\textit{v}}/\overline{\textit{x}}]$ is obtained by
parallel substitution of variables $\overline{\textit{x}}$ with values
$\overline{\textit{v}}$.

  * •

$\mathit{fbody}(\textit{f})$ returns the pair of the parameters and the body
of the declaration of f, if any, in the assumed program.

Intuitively, a closed result $({{\textit{s}},{\rho}})$ is well-defined if it
denotes a unique stream, and a closed environment $\rho$ is well-defined if,
for each $\textit{x}\in\mathit{dom}(\rho)$, $({{\textit{x}},{\rho}})$ is well-
defined. In other words, the corresponding set of equations admits a unique
solution. For instance, the environment ${\\{\textit{x}\mapsto\textit{x}\\}}$
is not well-defined, since it is undetermined (any stream satisfies the
equation $\textit{x}=\textit{x}$); the environment
$\\{\textit{x}\mapsto\textit{x}[+]\textit{y},\textit{y}\mapsto{1}\mathbin{\texttt{:}}{\textit{y}}\\}$
is not well-defined as well, since it is undefined (the two equations
$\textit{x}=\textit{x}\mapsto\textit{x}[+]\textit{y},\textit{y}={1}\mathbin{\texttt{:}}{\textit{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
$\mathit{wd}(\rho,\textit{x},\textit{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 $({{\textit{x}},{\rho}})$ 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.

For instance, if we consider the program f()=g() g()=1:f(), then the judgment
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{f}}()}}}},\emptyset,\emptyset}\\!\Downarrow\\!({{\textit{x}},{\rho}})$,
with
$\rho=\\{\textit{x}\mapsto\textit{y},\textit{y}\mapsto{1}\mathbin{\texttt{:}}{\textit{x}}\\}$,
is derivable; however, while the final result $({{\textit{x}},{\rho}})$ is
closed, the derivation contains also judgments with open results, as happens
for
${{{{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{f}}()}}}},\emptyset,\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{f}}()}}}}\mapsto\textit{x},\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{g}}()}}}}\mapsto\textit{y}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}})$
and
${{{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{g}}()}}}},\emptyset,\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{f}}()}}}}\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{y}},{\\{\textit{y}\mapsto{1}\mathbin{\texttt{:}}{\textit{x}}\\}}})$.
The full derivation is presented in the Appendix (Fig. 8), together with
another example (Fig. 9).

Finally, rule (at) computes the $i$-th element of a stream expression. After
evaluating the arguments, the result is obtained by the auxiliary judgment
$\mathit{at}_{\rho}(\textit{s},i)=\textit{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 $\mathit{at}_{\rho}(\textit{s},i)$, if s is a variable free in
the environment, then execution is stuck; again, an implementation should
raise a runtime error instead.

##  3 Examples

First we show some simple examples, to explain how corecursive definitions
work. Then we provide some more significant examples.

Consider the following function declarations:

⬇

repeat(n) = n:repeat(n)

one_two() = 1:two_one()

two_one() = 2:one_two()

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
$\mathtt{({{\textit{x}},{\\{\textit{x}\mapsto{0}\mathbin{\texttt{:}}{\textit{x}}\\}}})}$,
and
$\mathtt{({{\textit{x}},{{\\{}\textit{x}\mapsto{1}\mathbin{\texttt{:}}{\textit{y}},\textit{y}\mapsto{2}\mathbin{\texttt{:}}{\textit{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
$\mathtt{{0}\mathbin{\texttt{:}}{\textit{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.

$\begin{array}[]{l}{\mathtt{repeat(0)},\emptyset,\emptyset}\\!\Downarrow\\!({{\textit{x}},{\\{\textit{x}\mapsto{0}\mathbin{\texttt{:}}{\textit{x}}\\}}}){\mathtt{{0}\mathbin{\texttt{:}}{repeat(0)}},\emptyset,\\{\mathtt{repeat(0)}\mapsto\textit{x}\\}}\\!\Downarrow\\!({{{0}\mathbin{\texttt{:}}{\textit{x}}},{\emptyset}})\lx@proof@logical@and{}{\mathtt{repeat(0)},\emptyset,\\{\mathtt{repeat(0)}\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}})\end{array}$

$\begin{array}[]{l}{\mathtt{one\\_two()},\emptyset,\emptyset}\\!\Downarrow\\!({{\textit{x}},{\\{\textit{x}\mapsto
1:\textit{y},\ \textit{y}\mapsto
2:\textit{x}\\}}}){\mathtt{1:two\\_one()},\emptyset,\\{\mathtt{one\\_two()}\mapsto\textit{x}\\}}\\!\Downarrow\\!({{1:\textit{y}},{{\\{\textit{y}\mapsto
2:\textit{x}\\}}}})\lx@proof@logical@and{}{\mathtt{two\\_one()},\emptyset,\\{\mathtt{one\\_two()}\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{y}},{\\{\textit{y}\mapsto
2:\textit{x}\\}}}){\mathtt{2:one\\_two()},\emptyset,\\{\mathtt{one\\_two()}\mapsto\textit{x},\
\mathtt{two\\_one()}\mapsto\textit{y}\\}}\\!\Downarrow\\!({{2:\textit{x}},{\emptyset}})\lx@proof@logical@and{}{\mathtt{one\\_two()},\emptyset,\\{\mathtt{one\\_two()}\mapsto\textit{x},\
\mathtt{two\\_one()}\mapsto\textit{y}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}})\end{array}$

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 non-
regular 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()[+][1])

nat_to_pow(n) = //nat_to_pow(n)(i)=i^n

if n <= 0 then [1] else nat_to_pow(n-1)[*]nat()

fact() = 1:((nat()[+][1])[*]fact())

pow(n) = 1:([n][*]pow(n)) //pow(n)(i)=n^i

fib() = 0:1:(fib()[+]fib()^)

incr(s) = s[+][1]

The definition of nat uses corecursion, since the recursive call nat() is
cyclic. Hence the call nat() returns
$({{\textit{x}},{{\\{}\textit{x}\mapsto{0}\mathbin{\texttt{:}}{(\textit{x}[+]\textit{y})},\textit{y}\mapsto{1}\mathbin{\texttt{:}}{\textit{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), returns

$({{\textit{x}_{2}},{{\\{\textit{x}_{2}\mapsto\textit{x}_{1}[*]\textit{x},\textit{x}_{1}\mapsto\textit{x}_{0}[*]\textit{x},\textit{x}_{0}\mapsto\textit{y},\textit{y}\mapsto{1}\mathbin{\texttt{:}}{\textit{y}},\textit{x}\mapsto{0}\mathbin{\texttt{:}}{(\textit{x}[+]\textit{y}^{\prime})},\textit{y}^{\prime}\mapsto{1}\mathbin{\texttt{:}}{\textit{y}^{\prime}}\\}}}}).$

The definitions of fact, pow, and fib are corecursive. For instance, the call
fact() returns
${({{\textit{z}},{\textit{z}\mapsto{{1}\mathbin{\texttt{:}}{((\textit{x}[+]\textit{y})[*]z)}},\textit{x}\mapsto{0}\mathbin{\texttt{:}}{(\textit{x}[+]\textit{y}^{\prime}}),\textit{y}\mapsto
1:\textit{y},\textit{y}^{\prime}\mapsto 1:\textit{y}^{\prime}}})}$. The
definition of incr is non-recursive, hence always converges, and the call
incr(s) returns
$({{\textit{x}},{{\\{}\textit{x}\mapsto\textit{s}[+]\textit{y},\textit{y}\mapsto{1}\mathbin{\texttt{:}}{\textit{y}}{\\}}}})$.

The next few examples show applications of the interleaving operator.

⬇

dup_occ() = 0:1:(dup_occ() || dup_occ())

Function dup_occ() generates the stream which alternates sequences of
occurrences of 0 and 1, with the number of repetitions of the same number
duplicated at each step, that is, (0:1:0:0:1:1:0:0:0:0...).

A more involved example shows a different way to generate the stream of all
powers of 2 starting from $2^{1}$:

⬇

pow_two=2:4:8:((pow_two^^[*]pow_two)||(pow_two^^[*]pow_two^))

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.

⬇

bfs_index() = 1:((bfs_index()[*][2])||(bfs_index()[*][2][+][1]))

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.

⬇

bfs_level() = 0:((bfs_level()[+][1])||(bfs_level()[+][1]))

In this case, the generated stream is more interesting; indeed, bfs_level()(n)
= floor(log2(n+1)).

The following function computes the stream of partial sums of the first $i+1$
elements of a stream $s$, that is, sum($s$)($i$)$=\sum_{k=0}^{i}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 first $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 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:

⬇

sum_expn(n)($i$)$=\displaystyle\displaystyle\sum_{k=0}^{i}\frac{{\textit{n}}^{k}}{k!}=1+\textit{n}+\frac{{\textit{n}}^{2}}{2!}+\frac{{\textit{n}}^{3}}{3!}+\frac{{\textit{n}}^{4}}{4!}+\cdots+\frac{\textit{n}^{i}}{i!}$

Lastly, we present a couple of examples showing how it is possible to define
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 data
in windows of length n:

⬇

aggr(n,s) = if n<=0 then [0] else s[+]aggr(n-1,s^)

For instance, aggr(3,s) returns the stream $\textit{s}^{\prime}$ s.t.
$\textit{s}^{\prime}(i)=\textit{s}(i)+\textit{s}(i+1)+\textit{s}(i+2)$. On top
of aggr, we can easily define avg(n,s) to compute the stream of average values
of s in windows of length n:

⬇

avg(n,s) = aggr(n,s)[/][n]

##  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
$\mathit{wd}({\rho^{\prime}},\textit{x},\textit{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 $\sigma$ is an infinite
sequence of numeric values, that is, a function which returns, for each index
$i\geq 0$, the $i$-th element $\sigma(i)$. Given a result
$({{\textit{s}},{\rho}})$, we get a stream by instantiating variables in s
with streams, in a way consistent with $\rho$, and evaluating operators. To
make this formal, we need some preliminary definitions.

A _substitution_ $\theta$ is a function from a finite set of variables to
streams. We denote by ${\llbracket\textit{s}\rrbracket}\theta$ the stream
obtained by applying $\theta$ to s, and evaluating operators, as formally
defined below.

> ${\llbracket\textit{x}\rrbracket}\theta=\theta(\textit{x})$
>
> $({\llbracket{\textit{n}}\mathbin{\texttt{:}}{\textit{s}}\rrbracket}\theta)(i)=\begin{cases}\textit{n}&i=0\\\
> ({\llbracket\textit{s}\rrbracket}\theta)(i-1)&i\geq 1\end{cases}$
>  $({\llbracket{\textit{s}}{\char
> 94\relax}\rrbracket}\theta)(i)={\llbracket\textit{s}\rrbracket}\theta(i+1)\hskip
> 15.00002pti\geq 0$
>
> $({\llbracket\textit{s}_{1}{[{\textit{nop}}]}\textit{s}_{2}\rrbracket}\theta)(i)={\llbracket\textit{s}_{1}\rrbracket}\theta(i)\mathbin{\textit{nop}}{\llbracket\textit{s}_{2}\rrbracket}\theta(i)\hskip
> 15.00002pti\geq 0$
>
> $({\llbracket\textit{s}_{1}{\|}\textit{s}_{2}\rrbracket}\theta)(2i)={\llbracket\textit{s}_{1}\rrbracket}\theta(i)\hskip
> 15.00002pti\geq 0$
>
> $({\llbracket\textit{s}_{1}{\|}\textit{s}_{2}\rrbracket}\theta)(2i+1)={\llbracket\textit{s}_{2}\rrbracket}\theta(i)\hskip
> 15.00002pti\geq 0$

Given an environment $\rho$ and a substitution $\theta$ with domain
$\textit{vars}(\rho)$, the substitution $\rho[\theta]$ is defined by:

>
> $\rho[\theta](\textit{x})=\begin{cases}{\llbracket\rho(\textit{x})\rrbracket}\theta&\textit{x}\in\mathit{dom}(\rho)\\\
> \theta(x)&{\textit{x}\in\textit{fv}(\rho)}\end{cases}$

Then, a _solution_ of $\rho$ is a substitution $\theta$ such that
$\rho[\theta]=\theta$.

A closed environment $\rho$ is _well-defined_ if it has exactly one solution.
For instance, ${\\{\textit{x}\mapsto{1}\mathbin{\texttt{:}}{\textit{x}}\\}}$
and ${\\{\textit{y}\mapsto{0}\mathbin{\texttt{:}}{(\textit{y}[+]\textit{x})},\
\textit{x}\mapsto 1:\textit{x}\\}}$ are well-defined, since their unique
solutions map x to the infinite stream of ones, and y to the stream of natural
numbers, respectively. Instead, for ${\\{\textit{x}\mapsto 1[+]\textit{x}\\}}$
there are no solutions. Lastly, an environment can be undetermined: for
instance, a substitution mapping x into an arbitrary stream is a solution of
${\\{\textit{x}\mapsto\textit{x}\\}}$.

An open environment $\rho$ is well-defined if, for each $\theta$ with domain
$\textit{fv}(\rho)$, it has exactly one solution $\theta^{\prime}$ such that
$\theta\subseteq\theta^{\prime}$. For instance, the open environment
$\\{\textit{y}\mapsto{0}\mathbin{\texttt{:}}{(\textit{y}[+]\textit{x})}\\}$ is
well-defined.

In Fig. 3 we provide the operational characterization of well-definedness.

$\begin{array}[t]{llll}\mathit{m}&{:}{:}=&{\textit{x}_{1}\mapsto\textit{n}_{1}\ldots\textit{x}_{n}\mapsto\textit{n}_{k}}\hskip
7.20003pt(n\geq 0)&\mbox{{\small{map from variables to integer
numbers}}}\end{array}$
$\begin{array}[]{l}\\\
{\tiny\textsc{({main})}}\displaystyle\frac{{\mathsf{wd}_{\rho^{\prime}}(\textit{x},\emptyset)}}{\mathit{wd}(\rho,\textit{x},\textit{v})}\
\begin{array}[]{l}{\rho^{\prime}=\rho\\{\textit{x}\mapsto\textit{v}\\}}\end{array}\hskip
13.50002pt{\tiny\textsc{({wd-
var})}}\displaystyle\frac{\mathsf{wd}_{\rho}(\rho(\textit{x}),\mathit{m}\\{\textit{x}\mapsto
0\\})}{\mathsf{wd}_{\rho}(\textit{x},\mathit{m})}\
\begin{array}[]{l}\textit{x}\not\in\mathit{dom}(\mathit{m})\end{array}\\\\[19.37492pt]
{\tiny\textsc{({wd-
corec})}}\displaystyle\frac{}{\mathsf{wd}_{\rho}(\textit{x},\mathit{m})}\
\begin{array}[]{l}{\textit{x}\in\mathit{dom}(\rho)}\\\
\mathit{m}(x)>0\end{array}\hskip 13.50002pt{{\tiny\textsc{({wd-
delay})}}\displaystyle\frac{\mathsf{wd}_{\rho}(\rho(\textit{x}),\mathit{m}\\{\textit{x}\mapsto
0\\})}{\mathsf{wd}_{\rho}(\textit{x},\mathit{m})}\
\begin{array}[]{l}\mathit{m}(x)>0\end{array}}\\\\[19.37492pt]
{{\tiny\textsc{({wd-
fv})}}\displaystyle\frac{}{\mathsf{wd}_{\rho}(\textit{x},\mathit{m})}\
\begin{array}[]{l}\textit{x}\not\in\mathit{dom}(\rho)\end{array}}\hskip
13.50002pt{\tiny\textsc{({wd-
cons})}}\displaystyle\frac{\mathsf{wd}_{\rho}(\textit{s},{\mathit{m}^{+1}})}{\mathsf{wd}_{\rho}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},\mathit{m})}\
\begin{array}[]{l}\end{array}\hskip 13.50002pt{\tiny\textsc{({wd-
tail})}}\displaystyle\frac{\mathsf{wd}_{\rho}(\textit{s},{\mathit{m}^{-1}})}{\mathsf{wd}_{\rho}({\textit{s}}{\char
94\relax},\mathit{m})}\ \begin{array}[]{l}\end{array}\\\\[19.37492pt]
{\tiny\textsc{({wd-
nop})}}\displaystyle\frac{\mathsf{wd}_{\rho}(\textit{s}_{1},\mathit{m})\hskip
7.20003pt\mathsf{wd}_{\rho}(\textit{s}_{2},\mathit{m})}{\mathsf{wd}_{\rho}(\textit{s}_{1}{[{\textit{nop}}]}\textit{s}_{2},\mathit{m})}\
\begin{array}[]{l}\end{array}\hskip
13.50002pt{\tiny\textsc{({wd-$\|$})}}\displaystyle\frac{\mathsf{wd}_{\rho}(\textit{s}_{1},\mathit{m})\hskip
7.20003pt\mathsf{wd}_{\rho}(\textit{s}_{2},\mathit{m}^{+1})}{\mathsf{wd}_{\rho}(\textit{s}_{1}{\|}\textit{s}_{2},\mathit{m})}\
\begin{array}[]{l}\end{array}\end{array}$

Figure 3: Operational definition of well-definedness

The judgment $\mathit{wd}(\rho,\textit{x},\textit{s})$ used in the side
condition of rule (invk) holds if
$\mathsf{wd}_{\rho^{\prime}}(\textit{x},\emptyset)$ holds, with
${\rho^{\prime}}{=}{\rho\\{\textit{x}\mapsto\textit{v}\\}}$. The judgment
$\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ means well-definedness of a result.
That is, restricting the domain of $\rho$ 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,
$\mathit{wd}(\rho,\textit{x},\textit{s})$ holds if adding the association of s
with x preserves well-definedness of $\rho$.

The additional argument $\mathit{m}$ in the judgment
$\mathsf{wd}_{\rho}(\textit{s},\mathit{m})$ is a map from variables to integer
numbers. We write $\mathit{m}^{+1}$ and $\mathit{m}^{-1}$ for the maps
$\\{(\textit{x},\mathit{m}(\textit{x})+1)\mid{\textit{x}\in\mathit{dom}(\mathit{m})}\\}$,
and
$\\{(\textit{x},\mathit{m}(\textit{x})-1)\mid\textit{x}\in\mathit{dom}(\mathit{m})\\}$,
respectively.

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 (wd-corec), 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 is only added for the purpose of the soundness proof
and should be not part of an implementation333Indeed, it does not affect
derivability, see Lemma 4 in the following., 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 $\textit{x}\in\mathit{dom}(\rho)$; 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.444Non-well-
definedness can only be detected on closed results. In rules (wd-cons) 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,
$\mathit{at}_{\rho}(\textit{s}_{1}\|\textit{s}_{2},i)=\mathit{at}_{\rho}(\textit{s}_{1},i)$,
and this happens only for $i=0$, while for odd indexes $i$ we have that
$\mathit{at}_{\rho}(\textit{s}_{1}\|\textit{s}_{2},i)=\mathit{at}_{\rho}(\textit{s}_{2},i-k)$,
with $k\geq 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
$\mathit{at}_{\rho}(\textit{s},i)=\textit{n}$ judgment can be turned into an
algorithm which can possibly diverge (infinite proof tree).

In the Appendix we show two examples of derivation of well-definedness and
access to the $i$-th element: the result
$({{\textit{x}},{\\{\textit{x}\mapsto{0}\mathbin{\texttt{:}}{(\textit{x}\ [+]\
\textit{y})},\textit{y}\mapsto{1}\mathbin{\texttt{:}}{\textit{y}}\\}}})$
obtained by evaluating the call nat()(Fig. 11), and a more involved example,
the result
$({{\textit{x}},{\\{\textit{x}\mapsto{0}\mathbin{\texttt{:}}{(\textit{x}\ [+]\
\textit{y})\ ||\ (\textit{x}\ [+]\ \textit{y}),\textit{y}\mapsto
1:\textit{y}}\\}}})$ obtained by evaluating the call bfs_level() (Fig. 12),
with nat and bfs_level defined as in Sect. 3. Below we show an example of
failing derivation:

$\begin{array}[]{l}\mathsf{wd}_{\rho}(\textit{x},\emptyset)\mathsf{wd}_{\rho}(0:(\textit{x}\
||\ {{\textit{x}}{\char 94\relax}}{\char 94\relax}),\\{\textit{x}\mapsto
0\\})\mathsf{wd}_{\rho}(\textit{x}\ ||\ {{\textit{x}}{\char 94\relax}}{\char
94\relax},\\{\textit{x}\mapsto
1\\})\mathsf{wd}_{\rho}(\textit{x},\\{\textit{x}\mapsto 1\\})\hskip
7.5pt\mathsf{wd}_{\rho}({{\textit{x}}{\char 94\relax}}{\char
94\relax},\\{\textit{x}\mapsto 2\\})\mathsf{wd}_{\rho}({\textit{x}}{\char
94\relax},\\{\textit{x}\mapsto
1\\})\mathsf{wd}_{\rho}(\textit{x},\\{\textit{x}\mapsto
0\\})\mathtt{FAIL}\end{array}$ Figure 4: Failing derivation for
${\rho=\\{\textit{x}\mapsto 0:(\textit{x}\ ||\ {{\textit{x}}{\char
94\relax}}{\char 94\relax})\\}}$

As depicted in Fig. 4, the check succeeds for the left-hand component of the
interleaving operator, while the proof tree cannot be completed for the other
side. Indeed, the double application of the tail operator makes undefined
access to stream elements with index greater than $1$, since the evaluation of
$\mathit{at}_{\rho}(\textit{x},2)$ infinitely triggers the evaluation of
itself.

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
$\mathit{at}_{\rho}(\textit{s},i)$ rather than
$\mathit{at}_{\rho}(\textit{s},i)=\textit{n}$. We call _derivation_ an either
finite or infinite proof tree. We write
$\mathsf{wd}_{\rho}(\textit{s}^{\prime},\mathit{m}^{\prime})\vdash\mathsf{wd}_{\rho}(\textit{s},\mathit{m})$
to mean that $\mathsf{wd}_{\rho}(\textit{s}^{\prime},\mathit{m}^{\prime})$ is
a premise of a (meta-)rule where $\mathsf{wd}_{\rho}(\textit{s},\mathit{m})$
is the conclusion, and $\vdash^{\star}$ for the reflexive and transitive
closure of this relation.

###### Lemma 1

  1. 1.

A judgment $\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ has no derivation iff
the following condition holds:
(wd-stuck)
$\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\rho(\textit{x}),\mathit{m}\\{\textit{x}\mapsto
0\\})\vdash\mathsf{wd}_{\rho}(\textit{x},\mathit{m})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s},\emptyset)$
for some $\textit{x}\in\mathit{dom}(\rho)$, and
$\mathit{m}^{\prime},\mathit{m}$ s.t.
$\textit{x}\not\in\mathit{dom}(\mathit{m}),\mathit{m}^{\prime}(\textit{x})\leq
0$.

  2. 2.

If the derivation of $\mathit{at}_{\rho}(\textit{s},j)$ is infinite, then the
following condition holds:
(at-$\infty$)
$\mathit{at}_{\rho}(\textit{x},i+k)\vdash^{\star}\mathit{at}_{\rho}(\rho(\textit{x}),i)\vdash\mathit{at}_{\rho}(\textit{x},i)\vdash^{\star}\mathit{at}_{\rho}(\textit{s},j)$
for some $\textit{x}\in\mathit{dom}(\rho)$, and $i,k\geq 0$.

###### Lemma 2

If
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}\mathit{at}_{\rho}(\textit{s}^{\prime},i)$,
and
$\mathsf{wd}_{\rho}(\textit{s}^{\prime},\mathit{m})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s},\emptyset)$
with $\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ derivable, and
$\textit{x}\in\mathit{dom}(\mathit{m})$, then

>
> ${\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s}^{\prime},\mathit{m})}$
> for some $\mathit{m}^{\prime}$ such that
> $\mathit{m}^{\prime}(\textit{x})-\mathit{m}(\textit{x})\leq i-i^{\prime}$.

###### Proof

The proof is by induction on the length of the path in
${\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}\mathit{at}_{\rho}(\textit{s}^{\prime},i)}$.

Base

The length of the path is $0$, hence we have
$\mathit{at}_{\rho}(\textit{x},i)\vdash^{\star}\mathit{at}_{\rho}(\textit{x},i)$.
We also have
$\mathsf{wd}_{\rho}(\textit{x},\mathit{m})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{x},\mathit{m})$,
and we get the thesis since
$\mathit{m}(\textit{x})=\mathit{m}(\textit{x})+i-i$.

Inductive step

By cases on the rule applied to derive
$\mathit{at}_{\rho}(\textit{s}^{\prime},i)$.

(at-var)

We have
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}\mathit{at}_{\rho}(\rho(\textit{y}),i)\vdash\mathit{at}_{\rho}(\textit{y},i)$.
There are two cases:

  * •

If $\textit{y}\not\in\mathit{dom}(\mathit{m})$ (hence
$\textit{y}\neq\textit{x}$), we have
$\mathsf{wd}_{\rho}(\rho(\textit{y}),\mathit{m}\\{\textit{y}\mapsto
0\\})\vdash\mathsf{wd}_{\rho}(\textit{y},\mathit{m})$ by rule (wd-var), the
premise is derivable, hence by inductive hypothesis we have
${\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\rho(\textit{y}),\mathit{m}\\{\textit{y}\mapsto
0\\})}$, and
${\mathit{m}^{\prime}(\textit{x})\leq\mathit{m}\\{\textit{y}\mapsto
0\\}(\textit{x})+i-i^{\prime}}=\mathit{m}(\textit{x})+i-i^{\prime}$, hence we
get the thesis.

  * •

If $\textit{y}\in\mathit{dom}(\mathit{m})$, then it is necessarily
$\mathit{m}(\textit{y})>0$, otherwise, by Lemma 1-(1),
$\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ would not be derivable. Hence, we
have ${\mathsf{wd}_{\rho}(\rho(\textit{y}),\mathit{m}\\{\textit{y}\mapsto
0\\})\vdash\mathsf{wd}_{\rho}(\textit{y},\mathit{m})}$ by rule (wd-delay),
hence by inductive hypothesis we have
${\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\rho(\textit{y}),\mathit{m}\\{\textit{y}\mapsto
0\\})}$, and
${\mathit{m}^{\prime}(\textit{x})\leq\mathit{m}\\{\textit{y}\mapsto
0\\}(\textit{x})+i-i^{\prime}}$. There are two subcases:

    * –

If $\textit{y}\neq\textit{x}$, then $\mathit{m}\\{\textit{y}\mapsto
0\\}(\textit{x})=\mathit{m}(\textit{x})$, and we get the thesis as in the
previous case.

    * –

If $\textit{y}=\textit{x}$, then $\mathit{m}\\{\textit{x}\mapsto
0\\}(\textit{x})=0$, hence ${\mathit{m}^{\prime}(\textit{x})\leq
i-i^{\prime}\leq\mathit{m}(\textit{x})+i-i^{\prime}}$, since
$\mathit{m}(\textit{x})>0$.

(at-cons-0)

Empty case, since the derivation for
$\mathit{at}_{\rho}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},0)$ does not
contain a node $\mathit{at}_{\rho}(\textit{x},i^{\prime})$.

(at-cons-succ)

We have $\mathit{at}_{\rho}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},i)$,
and
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}\mathit{at}_{\rho}(\textit{s},i-1)$.
Moreover, we can derive
$\mathsf{wd}_{\rho}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},\mathit{m})$
by rule (wd-cons), and by inductive hypothesis we also have
$\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s},\mathit{m}^{+1})$,
with
$\mathit{m}^{\prime}(\textit{x})\leq\mathit{m}^{+1}(\textit{x})+(i-1)-i^{\prime}$,
hence we get the thesis.

(at-tail)

This case is symmetric to the previous one.

(at-nop)

We have $\mathit{at}_{\rho}(\textit{s}_{1}{[{\textit{op}}]}\textit{s}_{2},i)$,
and either
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}\mathit{at}_{\rho}(\textit{s}_{1},i)$,
or
${\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}\mathit{at}_{\rho}(\textit{s}_{2},i)}$.
Assume the first case holds, the other is analogous. Moreover, we can derive
$\mathsf{wd}_{\rho}(\textit{s}_{1}{[{\textit{op}}]}\textit{s}_{2},\mathit{m})$
by rule (wd-nop), and by inductive hypothesis we also have
$\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s}_{1},\mathit{m})$,
with $\mathit{m}^{\prime}(\textit{x})\leq\mathit{m}(\textit{x})+i-i^{\prime}$,
hence we get the thesis.

(at-$\|$-even)

We have $\mathit{at}_{\rho}(\textit{s}_{1}\|\textit{s}_{2},2i)$ and
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}\mathit{at}_{\rho}(\textit{s}_{1},i)$.
By inductive hypothesis, we have
$\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s}_{1},\mathit{m})$,
with $\mathit{m}^{\prime}(\textit{x})\leq\mathit{m}(\textit{x})+i-i^{\prime}$.
Moreover,
$\mathsf{wd}_{\rho}(\textit{s}_{1},\mathit{m})\vdash{}\mathsf{wd}_{\rho}(\textit{s}_{1}{\|}\textit{s}_{2},\mathit{m})$
holds by rule (wd-$\|$), hence we have
$\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s}_{1}{\|}\textit{s}_{2},\mathit{m})$
with
${\mathit{m}^{\prime}(\textit{x})\leq\mathit{m}(\textit{x})+2i-i^{\prime}}$
and, thus, the thesis.

(at-$\|$-odd)

We have $\mathit{at}_{\rho}(\textit{s}_{1}\|\textit{s}_{2},2i+1)$ and
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}\mathit{at}_{\rho}(\textit{s}_{2},i)$.
By inductive hypothesis, we have
$\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s}_{2},\mathit{m}^{+1})$,
with
$\mathit{m}^{\prime}(\textit{x})\leq\mathit{m}^{+1}(\textit{x})+i-i^{\prime}$.
Moreover,
$\mathsf{wd}_{\rho}(\textit{s}_{2},\mathit{m})\vdash{}\mathsf{wd}_{\rho}(\textit{s}_{1}{\|}\textit{s}_{2},\mathit{m})$
holds by rule (wd-$\|$), hence we have
$\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s}_{1}{\|}\textit{s}_{2},\mathit{m})$
with
$\mathit{m}^{\prime}(\textit{x})\leq\mathit{m}(\textit{x})+2i+1-i^{\prime}$
and, thus, the thesis.

###### Lemma 3

If
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}\mathit{at}_{\rho}(\textit{s},i)$,
and $\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ derivable, then

>
> ${\mathsf{wd}_{\rho}(\textit{x},\mathit{m})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s},\emptyset)}$
> for some $\mathit{m}$ such that $\textit{x}\not\in\mathit{dom}(\mathit{m})$.

###### Proof

Easy variant of the proof of Lemma 2.

###### Theorem 4.1

If $\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ has a derivation then, for all
$j$, $\mathit{at}_{\rho}(\textit{s},j)$ either has no derivation or a finite
derivation.

###### Proof

Assume by contradiction that $\mathit{at}_{\rho}(\textit{s},j)$ has an
infinite derivation for some $j$, and
$\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ is derivable. By Lemma 1-(2), the
following condition holds:

> (at-$\infty$) | $\mathit{at}_{\rho}(\textit{x},i+k)\vdash^{\star}\mathit{at}_{\rho}(\rho(\textit{x}),i)\vdash\mathit{at}_{\rho}(\textit{x},i)\vdash^{\star}\mathit{at}_{\rho}(\textit{s},j)$
> ---|---
> | for some $\textit{x}\in\mathit{dom}(\rho)$, and $i,k\geq 0$.

Then, starting from the right, by Lemma 3 we have
${\mathsf{wd}_{\rho}(\textit{x},\mathit{m})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s},\emptyset)}$
for some $\mathit{m}$ such that $\textit{x}\not\in\mathit{dom}(\mathit{m})$;
by rule (wd-var)
${\mathsf{wd}_{\rho}(\rho(\textit{x}),\mathit{m}\\{\textit{x}\mapsto
0\\})\vdash\mathsf{wd}_{\rho}(\textit{x},\mathit{m})}$, and finally by Lemma 2
we have:

> (wd-stuck) | $\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\rho(\textit{x}),\mathit{m}\\{\textit{x}\mapsto 0\\})\vdash\mathsf{wd}_{\rho}(\textit{x},\mathit{m})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s},\emptyset)$
> ---|---
> | for some $\textit{x}\in\mathit{dom}(\rho)$, and $\mathit{m}^{\prime},\mathit{m}$ s.t. $\textit{x}\not\in\mathit{dom}(\mathit{m}),\mathit{m}^{\prime}(\textit{x}){\leq{-k}}\leq 0$.

hence this is absurd by Lemma 1-(1).

##  5 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 $\rho$ for every variable in its domain. If we consider the
following environment:

> $\rho=(x_{0},\\{x_{0}\mapsto 0:x_{1},x_{1}\mapsto 0:x_{2},x_{2}\mapsto
> 0:x_{3},x_{3}\mapsto 0:x_{4},\ \ldots\ ,x_{n}\mapsto 0:x_{0}\\})$

we get the derivation presented in Fig. 5.

$\begin{array}[]{l}\mathsf{wd}_{\rho}(\textit{x}_{0},\emptyset)\mathsf{wd}_{\rho}(0:\textit{x}_{1},\\{x_{0}\mapsto
0\\})\mathsf{wd}_{\rho}(\textit{x}_{1},\\{x_{0}\mapsto
1\\})\mathsf{wd}_{\rho}(0:\textit{x}_{2},\\{x_{0}\mapsto 1,x_{1}\mapsto
0\\})\mathsf{wd}_{\rho}(\textit{x}_{2},\\{x_{0}\mapsto 2,x_{1}\mapsto
1\\})\mathsf{wd}_{\rho}(0:\textit{x}_{3},\\{x_{0}\mapsto 2,x_{1}\mapsto
1,x_{2}\mapsto 0\\})\mathsf{wd}_{\rho}(\textit{x}_{3},\\{x_{0}\mapsto
3,x_{1}\mapsto 2,x_{2}\mapsto 1\\})\vdots\end{array}$ Figure 5:

Here, the number of constructor occurrences 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 4.1.

In the optimized version, given in Fig. 6, the judgment has shape
$\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},\pi)$, where $\pi$ 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 $\mathsf{m}$ associates with each variable an index
(starting from 0) corresponding to the point in the path $\pi$ where the
variable was found the first time. The only operation performed on a path
$\pi$ is the addition $\pi\mathbin{\cdot}b$ of an element $b$ at the end.

$\begin{array}[t]{llll}\mathsf{m}&{:}{:}=&{\textit{x}_{1}\mapsto
i_{1}\ldots\textit{x}_{n}\mapsto i_{k}}\hskip 7.20003pt(i\geq
0)&\mbox{{\small{map from variables to indexes}}}\\\
\pi&{:}{:}=&b_{1}b_{2}\ldots b_{n}&\mbox{{\small{sequence of either 1 or
-1}}}\\\\[7.74997pt] \end{array}$
$\begin{array}[]{l}\\\
{{\tiny\textsc{({main})}}\displaystyle\frac{\mathsf{owd}_{\rho^{\prime}}(\textit{x},\emptyset,\epsilon)}{\mathit{wd}(\rho,\textit{x},\textit{v})}\
\begin{array}[]{l}\rho^{\prime}=\rho\\{\textit{x}\mapsto\textit{v}\\}\end{array}}\hskip
13.50002pt{\tiny\textsc{({owd-
var})}}\displaystyle\frac{\mathsf{owd}_{\rho}(\rho(\textit{x}),\mathsf{m}\\{\textit{x}\mapsto
i\\},\pi)}{\mathsf{owd}_{\rho}(\textit{x},\mathsf{m},\pi)}\
\begin{array}[]{l}\textit{x}\not\in\mathit{dom}(\mathsf{m})\\\
{i}=\mathit{length(\pi)}\end{array}\\\\[19.37492pt] {\tiny\textsc{({owd-
corec})}}\displaystyle\frac{}{\mathsf{owd}_{\rho}(\textit{x},\mathsf{m},\pi)}\
\begin{array}[]{l}\textit{x}\in\mathit{dom}(\mathsf{m})\\\
{\mathit{sum}(\mathsf{m}(\textit{x}),\pi)>0}\end{array}\hskip
13.50002pt{{\tiny\textsc{({owd-
fv})}}\displaystyle\frac{}{\mathsf{owd}_{\rho}(\textit{x},\mathsf{m},\pi)}\
\begin{array}[]{l}\textit{x}\not\in\mathit{dom}(\rho)\end{array}}\\\\[19.37492pt]
{\tiny\textsc{({owd-
cons})}}\displaystyle\frac{\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},{\pi\mathbin{\cdot}1})}{\mathsf{owd}_{\rho}(n:\textit{s},\mathsf{m},\pi)}\
\begin{array}[]{l}\end{array}\hskip 13.50002pt{\tiny\textsc{({owd-
tail})}}\displaystyle\frac{\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},{\pi\mathbin{\cdot}(-1)})}{\mathsf{owd}_{\rho}({\textit{s}}{\char
94\relax},\mathsf{m},\pi)}\ \begin{array}[]{l}\end{array}\\\\[19.37492pt]
{\tiny\textsc{({owd-
nop})}}\displaystyle\frac{\mathsf{owd}_{\rho}(\textit{s}_{1},\mathsf{m},\pi)\hskip
7.20003pt\mathsf{owd}_{\rho}(\textit{s}_{2},\mathsf{m},\pi)}{\mathsf{owd}_{\rho}(\textit{s}_{1}[{\textit{nop}}]\textit{s}_{2},\mathsf{m},\pi)}\
\begin{array}[]{l}\end{array}\hskip
13.50002pt{{\tiny\textsc{({owd-$\|$})}}\displaystyle\frac{\mathsf{owd}_{\rho}(\textit{s}_{1},\mathsf{m},\pi)\hskip
7.20003pt\mathsf{owd}_{\rho}(\textit{s}_{2},\mathsf{m},\pi\mathbin{\cdot}1)}{\mathsf{owd}_{\rho}(\textit{s}_{1}\|\textit{s}_{2},\mathsf{m},\pi)}\
\begin{array}[]{l}\end{array}}\\\\[19.37492pt]
{{\tiny\textsc{({sum-0})}}\displaystyle\frac{\mathit{sum}(\pi)=n}{\mathit{sum}(0,\pi)=n}\
\begin{array}[]{l}\end{array}}\hskip
13.50002pt{{\tiny\textsc{({sum-n})}}\displaystyle\frac{\mathit{sum}(n-1,{b_{2}\ldots
b_{n}})=n^{\prime}}{\mathit{sum}(n,{b_{1}b_{2}\ldots b_{n}})=n^{\prime}}\
\begin{array}[]{l}n>0\end{array}}\\\\[19.37492pt]
{{\tiny\textsc{({sum-b})}}\displaystyle\frac{}{\mathit{sum}(\epsilon)=0}\
\begin{array}[]{l}\end{array}}\hskip
13.50002pt{{\tiny\textsc{({sum-i})}}\displaystyle\frac{\mathit{sum}({b_{2}\ldots
b_{n}})=n}{\mathit{sum}({b_{1}b_{2}\ldots b_{n}})={b_{1}}+n}\
\begin{array}[]{l}\end{array}}\end{array}$

Figure 6: Optimized operational definition of well-definedness

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 (owd-
corec), when the same variable is found the second time, the auxiliary
function $\mathit{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 $\mathit{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.

Let us now consider again the example above:

> $\rho=(x_{0},\\{x_{0}\mapsto 0:x_{1},x_{1}\mapsto 0:x_{2},x_{2}\mapsto
> 0:x_{3},x_{3}\mapsto 0:x_{4},\ \ldots\ ,x_{n}\mapsto 0:x_{0}\\})$

By the new predicate $\mathsf{owd}$, we get a derivation tree of the same
shape as in Fig. 5. However, $\mathit{sum}$ is applied to the path $\pi$ only
at the leaves, and the length of $\pi$ is linearly proportional to the depth
of the derivation tree, which coincides with the number $N$ of nodes in this
specific case; hence, the time complexity to compute $\mathit{sum}(0,\pi)$
(that is, $\mathit{sum}(\mathsf{m}(x_{0}),\pi)$) is linear in $N$. Finally,
since for inner nodes only constant time operations are performed555This holds
for any valid derivation tree and not for this specific case. (addition at the
end of the path, and map insertion and lookup), the overall time complexity is
linear in $N$.

As worst case in terms of time complexity for the predicate $\mathsf{owd}$,
consider

> ${\rho_{i}=(\textit{x}_{0},\\{\textit{x}_{0}\mapsto
> 0:\textit{x}_{1}[+]\textit{x}_{1},\textit{x}_{1}\mapsto
> 0:\textit{x}_{2}[+]\textit{x}_{2},\textit{x}_{2}\mapsto
> 0:\textit{x}_{3}[+]\textit{x}_{3},\ldots\ ,x_{i}\mapsto 0:x_{0}\\})}$

The derivation tree for this environment is shown in Fig. 7, where
$\mathsf{m}_{i}$ abbreviates the map $\\{\textit{x}_{0}\mapsto
0,\textit{x}_{1}\mapsto 1,\ldots,\textit{x}_{i}\mapsto i\\}$.

$\begin{array}[]{l}\mathsf{owd}_{\rho}(\textit{x}_{0},\emptyset,\epsilon)\mathsf{owd}_{\rho}(0:\textit{x}_{1}[+]\textit{x}_{1},\mathsf{m}_{0},\epsilon)\mathsf{owd}_{\rho}(\textit{x}_{1}[+]\textit{x}_{1},\mathsf{m}_{0},[1])\lx@proof@logical@and\mathsf{owd}_{\rho}(\textit{x}_{1},\mathsf{m}_{0},[1])\mathsf{owd}_{\rho}(0:\textit{x}_{2}[+]\textit{x}_{2},\mathsf{m}_{1},[1])\mathsf{owd}_{\rho}(\textit{x}_{2}[+]\textit{x}_{2},\mathsf{m}_{1},[1,1])\lx@proof@logical@and\mathsf{owd}_{\rho}(\textit{x}_{2},\mathsf{m}_{1},[1,1])\mathsf{owd}_{\rho}(0:\textit{x}_{3}[+]\textit{x}_{3},\mathsf{m}_{2},[1,1])\mathsf{owd}_{\rho}(\textit{x}_{3}[+]\textit{x}_{3},\mathsf{m}_{2},[1,1,1])\vdots\mathsf{owd}_{\rho}(\textit{x}_{2},\mathsf{m}_{1},[1,1])\vdots\mathsf{owd}_{\rho}(\textit{x}_{1},\mathsf{m}_{0},[1])\vdots\end{array}$

Figure 7:

As already noticed, for inner nodes only constant time operations are
performed, and the length of the paths in the leaves is linearly proportional
to the depth $D$ of the derivation tree; however, in this worst case the
number of leaves is not just one, but is linearly proportional to the total
number $N$ of nodes in the derivation tree, hence the depth $D$ is linearly
proportional to $\log N$. Therefore the overall time complexity is $O(N\cdot
D)$, that is, $O(N\cdot\log N)$.

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.

###### Lemma 4

A judgment $\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ has a derivation iff it
has a derivation which does not use rule (wd-delay).

###### Proof

The right-to-left implication is obvious. If
$\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ uses rule (wd-delay), all the
(first in their path) occurrences of the rule can be replaced by rule (wd-
corec), still getting a derivation.

Then, we define a relation between the auxiliary structures used in the two
judgments:

> For all $\mathit{m}$ and $({{\mathsf{m}},{\pi}})$,
> $\mathit{m}\bowtie(\mathsf{m},\pi)$ holds iff
> $\mathit{dom}(\mathit{m})=\mathit{dom}(\mathsf{m})$ and, for all
> $\textit{x}\in\mathit{dom}(\mathit{m})$,
> $\mathit{m}(\textit{x})=\mathit{sum}(\mathsf{m}(x),\pi)$.

In this way, we have the following generalization, whose straightforward proof
is in the Appendix.

###### Theorem 5.1

If $\mathsf{m}\bowtie(\mathsf{m},\pi)$, then, for all s,
$\mathsf{wd}_{\rho}(\textit{s},\mathit{m})$ is derivable iff
$\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},\pi)$ is derivable.

###### Corollary 1

$\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ is derivable iff
$\mathsf{owd}_{\rho}(\textit{s},\emptyset,\epsilon)$ is derivable.

##  6 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 4.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 5.1, stating that the
optimized version is equivalent.

Whereas in [3] the well-definedness check was also a necessary condition to
guarantee termination, this is not the case here, due to the interleaving
operator. Consider, for instance, the following example:
$\rho=\\{s\mapsto({s}{\char 94\relax}\|s)\|0{:}s\\}$. The judgment
$\mathsf{wd}_{\rho}(s,\emptyset)$ is not derivable, in particular because of
${s}{\char 94\relax}$, since ${\mathsf{wd}_{\rho}(s,\\{s\mapsto-1\\})}$ is not
derivable and, hence, $\mathsf{wd}_{\rho}({s}{\char 94\relax},\\{s\mapsto
0\\})$, $\mathsf{wd}_{\rho}({s}{\char 94\relax}\|s,\\{s\mapsto 0\\})$, and
${\mathsf{wd}_{\rho}(({s}{\char 94\relax}\|s)\|0{:}s,\\{s\mapsto 0\\})}$.
However, $\mathit{at}_{\rho}(s,i)$ is well-defined for all indexes $i$;
indeed, $\mathit{at}_{\rho}(s,1)=0$ is derivable, $\mathit{at}_{\rho}(s,0)=k$
is derivable iff $\mathit{at}_{\rho}(s,1)=k$ is derivable, and, for all $i>1$,
$\mathit{at}_{\rho}(s,i)=k$ is derivable iff $\mathit{at}_{\rho}(s,j)=k$ is
derivable for some $j<i$, hence $\mathit{at}_{\rho}(s,i)=0$ is derivable for
all $i$. We leave for future work the investigation of a complete check.

In future work, we plan to also prove soundness of the operational well-
definedness 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:

⬇

incr_reg(s) = (s(0)+1):incr_reg(s^)

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}{\char 94\relax}$ passed to the initial call and to the first recursive
call, respectively, in the environment
$\rho=\\{\textit{x}\mapsto{0}\mathbin{\texttt{:}}{\textit{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.

  * •

Design a static type system to prevent runtime errors such as the non-well-
definedness of a stream.

  * •

Extend corecursive definition to _flexible_ corecursive definitions [9, 10]
where programmers can define specific behaviour when a cycle is detected. In
this way we could get termination in cases where lazy evaluation diverges. For
instance, assuming to allow also booleans results for functions, we could
define the predicate allPos, checking that all the elements of a stream are
positive, specifying as result true when a cycle is detected; in this way,
e.g., allPos(one_two) would return the correct result.

## References

  * [1] Davide Ancona.  Regular corecursion in Prolog.  Computer Languages, Systems & Structures, 39(4):142–162, 2013\.
  * [2] Davide Ancona, Pietro Barbieri, Francesco Dagnino, and Elena Zucca.  Sound regular corecursion in coFJ.  In Robert Hirschfeld and Tobias Pape, editors, ECOOP’20 - Object-Oriented Programming, volume 166 of LIPIcs, pages 1:1–1:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [3] Davide Ancona, Pietro Barbieri, and Elena Zucca.  Enhanced regular corecursion for data streams.  In ICTCS’21 - Italian Conf. on Theoretical Computer Science, 2021\.
  * [4] Davide Ancona, Francesco Dagnino, and Elena Zucca.  Generalizing inference systems by coaxioms.  In Hongseok Yang, editor, 26th European Symposium on Programming, ESOP 2017, volume 10201 of Lecture Notes in Computer Science, pages 29–55, Berlin, 2017. Springer.
  * [5] Davide Ancona and Agostino Dovier.  A theoretical perspective of coinductive logic programming.  Fundamenta Informaticae, 140(3-4):221–246, 2015.
  * [6] Davide Ancona and Elena Zucca.  Corecursive Featherweight Java.  In FTfJP’12 - Formal Techniques for Java-like Programs, pages 3–10. ACM Press, 2012.
  * [7] Bruno Courcelle.  Fundamental properties of infinite trees.  Theoretical Computer Science, 25:95–169, 1983.
  * [8] Lukasz Czajka.  A new coinductive confluence proof for infinitary lambda calculus.  Logical Methods in Computer Science, 16(1), 2020.
  * [9] Francesco Dagnino.  Flexible Coinduction.  PhD thesis, DIBRIS, University of Genova, 2021.
  * [10] Francesco Dagnino, Davide Ancona, and Elena Zucca.  Flexible coinductive logic programming.  Theory and Practice of Logic Programming, 20(6):818–833, 2020.  Issue for ICLP 2020.
  * [11] Ralf Hinze.  Concrete stream calculus: An extended study.  Journal of Functional Programming, 20(5–6):463–535, 2010.
  * [12] Jean-Baptiste Jeannin and Dexter Kozen.  Computing with capsules.  Journal of Automata, Languages and Combinatorics, 17(2-4):185–204, 2012.
  * [13] Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva.  CoCaml: Functional programming with regular coinductive types.  Fundamenta Informaticae, 150:347–377, 2017.
  * [14] Ekaterina Komendantskaya, Patricia Johann, and Martin Schmidt.  A productivity checker for logic programming.  In Manuel V. Hermenegildo and Pedro López-García, editors, Logic-Based Program Synthesis and Transformation - LOPSTR 2016, Revised Selected Papers, volume 10184 of Lecture Notes in Computer Science, pages 168–186. Springer, 2016.
  * [15] Ekaterina Komendantskaya, John Power, and Martin Schmidt.  Coalgebraic logic programming: from semantics to implementation.  J. Log. Comput., 26(2):745–783, 2016.
  * [16] Jan J. M. M. Rutten.  A coinductive calculus of streams.  Mathematical Structures in Computer Science, 15(1):93–147, 2005\.
  * [17] Luke Simon.  Extending logic programming with coinduction.  PhD thesis, University of Texas at Dallas, 2006.
  * [18] Luke Simon, Ajay Bansal, Ajay Mallya, and Gopal Gupta.  Co-logic programming: Extending logic programming with coinduction.  In Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki, editors, Automata, Languages and Programming, 34th International Colloquium, ICALP 2007, volume 4596 of Lecture Notes in Computer Science, pages 472–483. Springer, 2007.

##  Appendix 0.A Examples of derivations

$\begin{array}[]{l}\textit{f}()=\textit{g}()\\\
g()=1:\textit{f}()\\\\[23.24991pt]
{\textit{f}(),\emptyset,\emptyset}\\!\Downarrow\\!({{\textit{x}},{\\{\textit{x}\mapsto\textit{y},\textit{y}\mapsto
1:\textit{x}\\}}}){\textit{g}(),\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{y}},{\\{\textit{y}\mapsto
1:\textit{x}\\}}}){1:\textit{f}(),\emptyset,\\{\textit{f}()\mapsto\textit{x},\textit{g}()\mapsto\textit{y}\\}}\\!\Downarrow\\!({{1:\textit{x}},{\emptyset}})\lx@proof@logical@and{1,\emptyset,\\{\textit{f}()\mapsto\textit{x},\textit{g}()\mapsto\textit{y}\\}}\\!\Downarrow\\!({{1},{\emptyset}}){\textit{f}(),\emptyset,\\{\textit{f}()\mapsto\textit{x},\textit{g}()\mapsto\textit{y}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}})\end{array}$
Figure 8: Example of derivation
$\begin{array}[]{l}\textit{f}()=\textit{g}(2:\textit{f}())\\\
g(s)=1:s\\\\[23.24991pt]
{\textit{f}(),\emptyset,\emptyset}\\!\Downarrow\\!({{\textit{x}},{\\{\textit{x}\mapsto\textit{y},\textit{y}\mapsto
1:2:\textit{x}\\}}}){\textit{g}(2:\textit{f}()),\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{y}},{\\{\textit{y}\mapsto
1:2:\textit{x}\\}}})\lx@proof@logical@and{2:\textit{f}(),\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{2:\textit{x}},{\emptyset}})\lx@proof@logical@and{2,\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{2},{\emptyset}}){\textit{f}(),\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}}){T_{1}}\\\\[30.99988pt]
T_{1}={\textit{g}(2:\textit{x}),\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{y}},{\\{\textit{y}\mapsto
1:2:\textit{x}\\}}}){1:2:\textit{x},\emptyset,\\{\textit{g}(2:\textit{x})\mapsto\textit{y},\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{1:2:\textit{x}},{\emptyset}})\end{array}$
Figure 9: Example of derivation
$\begin{array}[]{l}\textit{undef}()=(\textit{undef}()(0)):\textit{undef}()\\\\[23.24991pt]
{\textit{undef}(),\emptyset,\emptyset}\\!\Downarrow\\!({{?},{?}}){(\textit{undef}()(0)):\textit{undef}(),\emptyset,\\{\textit{undef}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{?},{?}})\lx@proof@logical@and
T_{1}{\textit{undef}(),\emptyset,\\{\textit{undef}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}}){}\\\\[30.99988pt]
T_{1}={\textit{undef}()(0),\emptyset,\\{\textit{undef}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{?},{?}})\lx@proof@logical@and{\textit{undef}(),\emptyset,\\{\textit{undef}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}}){0,\emptyset,\\{\textit{undef}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{0},{\emptyset}})\end{array}$
Figure 10: Example of stuck derivation

$\begin{array}[]{l}\mathsf{wd}_{\rho}(\textit{x},\emptyset)\mathsf{wd}_{\rho}({0}\mathbin{\texttt{:}}{(\textit{x}\
[+]\ \textit{y}{)}},\\{\textit{x}\mapsto 0\\})\mathsf{wd}_{\rho}(\textit{x}\
[+]\ \textit{y},\\{\textit{x}\mapsto
1\\})\lx@proof@logical@and\mathsf{wd}_{\rho}(\textit{x},\\{\textit{x}\mapsto
1\\})\mathsf{wd}_{\rho}(\textit{y},\\{\textit{x}\mapsto
1\\})\mathsf{wd}_{\rho}({1}\mathbin{\texttt{:}}{\textit{y}},\\{\textit{x}\mapsto
1,\textit{y}\mapsto
0\\})\mathsf{wd}_{\rho}(\textit{y},\\{\textit{x}\mapsto{2},\textit{y}\mapsto
1\\})\end{array}$

$\begin{array}[]{l}\mathit{at}_{\rho}(\textit{x},i)=i\mathit{at}_{\rho}({0}\mathbin{\texttt{:}}{(\textit{x}\
[+]\ \textit{y})},i)=i\mathit{at}_{\rho}(\textit{x}\ [+]\
\textit{y},i-1)={i}\lx@proof@logical@and\mathit{at}_{\rho}(\textit{x},i-1)=i-1\begin{array}[]{c}{\mathit{at}_{\rho}({0}\mathbin{\texttt{:}}{(\textit{x}\
[+]\ \textit{y})},0)=0}\\\
\vdots\end{array}\mathit{at}_{\rho}(\textit{y},i-1)={1}\begin{array}[]{c}{\mathit{at}_{\rho}({1}\mathbin{\texttt{:}}{\textit{y}},0)=1}\\\
\vdots\end{array}\end{array}$

Figure 11: Derivations for
$\rho=({{\textit{x}},{\\{\textit{x}\mapsto{0}\mathbin{\texttt{:}}{(\textit{x}\
[+]\ \textit{y})},\ y\mapsto{1}\mathbin{\texttt{:}}{\textit{y}}\\}}})$

$\begin{array}[]{l}\mathsf{wd}_{\rho}(\textit{x},\emptyset)\mathsf{wd}_{\rho}({0}\mathbin{\texttt{:}}{((\textit{x}\
[+]\ \textit{y})\ {\|}\ (\textit{x}\ [+]\ \textit{y}))},\\{\textit{x}\mapsto
0\\})\mathsf{wd}_{\rho}((\textit{x}\ [+]\ \textit{y})\ {\|}\ (\textit{x}\ [+]\
\textit{y}),\\{\textit{x}\mapsto
1\\})\lx@proof@logical@and\mathsf{wd}_{\rho}(\textit{x}\ [+]\
\textit{y},\\{\textit{x}\mapsto
1\\})\lx@proof@logical@and\mathsf{wd}_{\rho}(\textit{x},\\{\textit{x}\mapsto
1\\})\ \begin{array}[]{c}\vdots\\\ \end{array}\mathsf{wd}_{\rho}(\textit{x}\
[+]\ \textit{y},\\{\textit{x}\mapsto
2\\})\lx@proof@logical@and\mathsf{wd}_{\rho}(\textit{x},\\{\textit{x}\mapsto
2\\})\ \begin{array}[]{c}\vdots\\\ \end{array}\end{array}$

$\begin{array}[]{l}\mathit{at}_{\rho}(\textit{x},i)=f_{i}\mathit{at}_{\rho}({0}\mathbin{\texttt{:}}{(\textit{x}\
[+]\ \textit{y})\ {\|}\ (\textit{x}\ [+]\
\textit{y})},i)=f_{i}\mathit{at}_{\rho}((\textit{x}\ [+]\ \textit{y})\ {\|}\
(\textit{x}\ [+]\ \textit{y}),i-1)=f_{i}\mathit{at}_{\rho}(\textit{x}\ [+]\
\textit{y},(i-1)/2)=f_{i}\lx@proof@logical@and\mathit{at}_{\rho}(\textit{x},(i-1)/2)=f_{i}-1\vdots\mathit{at}_{\rho}(\textit{y},(i-1)/2)=1\vdots\end{array}$

Figure 12: Derivations for
${\rho=\\{\textit{x}\mapsto{0}\mathbin{\texttt{:}}{((\textit{x}\ [+]\
\textit{y})\ ||\ (\textit{x}\ [+]\ \textit{y}))},\textit{y}\mapsto
1:\textit{y}\\}}$ and $f_{i}=\mathtt{bfs\\_level()(i)}$, $i>1$

##  Appendix 0.B Proofs

Lemma 1.

  1. 1.

A judgment $\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ has no derivation iff
the following condition holds:
(wd-stuck)
$\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\vdash^{\star}\mathsf{wd}_{\rho}(\rho(\textit{x}),\mathit{m}\\{\textit{x}\mapsto
0\\})\vdash\mathsf{wd}_{\rho}(\textit{x},\mathit{m})\vdash^{\star}\mathsf{wd}_{\rho}(\textit{s},\emptyset)$
for some $\textit{x}\in\mathit{dom}(\rho)$, and
$\mathit{m}^{\prime},\mathit{m}$ s.t.
$\textit{x}\not\in\mathit{dom}(\mathit{m}),\mathit{m}^{\prime}(\textit{x})\leq
0$.

  2. 2.

If the derivation of $\mathit{at}_{\rho}(\textit{s},j)$ is infinite, then the
following condition holds:
(at-$\infty$)
$\mathit{at}_{\rho}(\textit{x},i+k)\vdash^{\star}\mathit{at}_{\rho}(\rho(\textit{x}),i)\vdash\mathit{at}_{\rho}(\textit{x},i)\vdash^{\star}\mathit{at}_{\rho}(\textit{s},j)$
for some $\textit{x}\in\mathit{dom}(\rho)$, and $i,k\geq 0$.

###### Proof

  1. 1.

If $\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ has no derivation, since for
each $\mathsf{wd}_{\rho}(\textit{s}^{\prime},\mathit{m})$ there is an
applicable rule, unless in the case
$\mathsf{wd}_{\rho}(\textit{x},\mathit{m})$ with $\mathit{m}(\textit{x})\leq
0$, then condition (wd-stuck) holds. On the other hand, if
$\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ is derivable, then by Lemma 4 it is
also derivable without using (wd-delay). Hence, there can be no path from
$\mathsf{wd}_{\rho}(\textit{s},\emptyset)$ of judgments on variables in
$\mathit{dom}(\rho)$, and a (first) repeated variable, that is, of the shape
below, where $\textit{x}\not\in\mathit{dom}(\mathit{m})$:

$\mathsf{wd}_{\rho}(\textit{x},\mathit{m}^{\prime})\mathsf{wd}_{\rho}(\textit{x}_{n},\\_)\ldots\mathsf{wd}_{\rho}(\textit{x}_{1},\\_)\mathsf{wd}_{\rho}(\textit{x},\mathit{m})\mathsf{wd}_{\rho}(\textit{y}_{m},\\_)\ldots\mathsf{wd}_{\rho}(\textit{y}_{1},\\_)\ldots\mathsf{wd}_{\rho}(\textit{s},\emptyset)$

  2. 2.

For each $\mathit{at}_{\rho}(\textit{s},i)$ there is exactly one applicable
rule, unless in the case $\mathit{at}_{\rho}(\textit{x},i)$ with
$\textit{x}\not\in\mathit{dom}(\rho)$. Moreover, since $\rho$ has finite
domain, the derivation $\mathit{at}_{\rho}(\textit{s},j)$ is infinite iff
there is a variable, say x, which is repeated infinitely many times, and the
indexes cannot be always decreasing.

Theorem 5.1 If $\mathsf{m}\bowtie(\mathsf{m},\pi)$, then, for all s,
$\mathsf{wd}_{\rho}(\textit{s},\mathit{m})$ is derivable iff
$\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},\pi)$ is derivable.

######  Proof ($\Rightarrow$)

By induction on the definition of $\mathsf{wd}_{\rho}(\textit{s},\mathit{m})$.

(wd-var)

By hypothesis,
$\mathsf{wd}_{\rho}(\rho(\textit{x}),\mathit{m}\\{\textit{x}\mapsto 0\\})$
holds with $\textit{x}\not\in\mathit{dom}(\mathit{m})$. By inductive
hypothesis, $\mathsf{owd}_{\rho}(\rho(\textit{x}),\mathsf{m},\pi)$ holds with
$\mathit{sum}(\mathsf{m}(x),\pi)=0=m(x)$. Thus, we can apply rule (owd-var)
and have the thesis.

(wd-corec)

By hypothesis, $\mathsf{wd}_{\rho}(\textit{x},\mathit{m})$ holds with
$\textit{x}\in\mathit{dom}(\mathit{m})$ and $\mathit{m}(x)>0$. Thus, since
$\mathit{sum}(\mathsf{m}(x),\pi)>0$ by the definition of $\bowtie$, we have
the thesis thanks to rule (owd-corec).

(wd-fv)

By hypothesis, $\mathsf{wd}_{\rho}(\textit{x},\mathit{m})$ holds with
$\textit{x}\not\in\mathit{dom}(\rho)$. We immediately have the thesis thanks
to rule (owd-fv).

(wd-cons)

By hypothesis, $\mathsf{wd}_{\rho}(\textit{s},{\mathit{m}^{+1}})$ holds. By
inductive hypothesis,
$\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},{p\mathbin{\cdot}1})$ holds.
Moreover, for all $\textit{x}\in\mathit{dom}(\mathit{m})$ so that
$\mathit{m}^{+1}(\textit{x})=i+1$, we have that
$\mathit{sum}(\mathsf{m}(x),\pi\mathbin{\cdot}1)=i+1$ by definition of
$\bowtie$. Thus, we have the thesis thanks to rule (owd-cons).

(wd-tail)

By hypothesis, $\mathsf{wd}_{\rho}(\textit{s},{\mathit{m}^{-1}})$ holds. By
inductive hypothesis,
$\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},{p\mathbin{\cdot}(-1)})$ holds.
Moreover, for all $\textit{x}\in\mathit{dom}(\mathit{m})$ so that
$\mathit{m}^{-1}(\textit{x})=i-1$, we have that
$\mathit{sum}(\mathsf{m}(x),\pi\mathbin{\cdot}(-1))=i-1$ by definition of
$\bowtie$. Thus, we have the thesis thanks to rule (owd-tail).

(wd-nop)

By hypothesis, $\mathsf{wd}_{\rho}(\textit{s}_{1},\mathit{m})$ and
$\mathsf{wd}_{\rho}(\textit{s}_{2},\mathit{m})$ hold. By inductive hypothesis,
$\mathsf{owd}_{\rho}(\textit{s}_{1},\mathsf{m},\pi)$ and
$\mathsf{owd}_{\rho}(\textit{s}_{2},\mathsf{m},\pi)$ hold. Thus, we have the
thesis thanks to rule (owd-nop).

(wd-$\|$)

By hypothesis, $\mathsf{wd}_{\rho}(\textit{s}_{1},\mathit{m})$ and
$\mathsf{wd}_{\rho}(\textit{s}_{2},\mathit{m}^{+1})$ hold. By inductive
hypothesis, $\mathsf{owd}_{\rho}(\textit{s}_{1},\mathsf{m},\pi)$ and
$\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},{p\mathbin{\cdot}1})$ hold.
Moreover, for all $\textit{x}\in\mathit{dom}(\mathit{m})$ so that
$\mathit{m}^{+1}(\textit{x})=i+1$, we have that
$\mathit{sum}(\mathsf{m}(x),\pi\mathbin{\cdot}1)=i+1$ by definition of
$\bowtie$. Thus, we have the thesis thanks to rule (owd-$\|$).

######  Proof ($\Leftarrow$)

By induction on the definition of
$\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},\pi)$.

(owd-var)

By hypothesis,
$\mathsf{owd}_{\rho}(\rho(\textit{x}),\mathsf{m}\\{\textit{x}\mapsto
i\\},\pi)$ holds with $\textit{x}\not\in\mathit{dom}(\mathsf{m})$ and
$\l=\mathit{length(\pi)}$. By inductive hypothesis,
$\mathsf{wd}_{\rho}(\rho(\textit{x}),\mathit{m}\\{\textit{x}\mapsto 0\\})$
holds with $\mathit{sum}(\mathsf{m}(x),p)=0=m(x)$. Thus, we can apply rule
(wd-var) and have the thesis.

(owd-corec)

By hypothesis, $\mathsf{owd}_{\rho}(\textit{x},\mathsf{m},\pi)$ holds with
$\textit{x}\in\mathit{dom}(\mathsf{m})$ and
$\mathit{sum}(\mathit{m}(\textit{x}),\pi)>0$. Thus, since $\mathit{m}(x)>0$ by
the definition of $\bowtie$, we have the thesis thanks to rule (wd-corec).

(owd-fv)

By hypothesis, $\mathsf{owd}_{\rho}(\textit{x},\mathsf{m},\pi)$ holds with
$\textit{x}\not\in\mathit{dom}(\rho)$. We immediately have the thesis thanks
to rule (wd-fv).

(owd-cons)

By hypothesis $\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},{p\mathbin{\cdot}1})$
holds. By inductive hypothesis
$\mathsf{wd}_{\rho}(\textit{s},{\mathit{m}^{+1}})$ holds. Moreover, for all
$\textit{x}\in\mathit{dom}(\mathit{m})$ so that
$\mathit{sum}(\mathsf{m}(x),\pi\mathbin{\cdot}1)=i+1$, we have that
$\mathit{m}^{+1}(\textit{x})=i+1$ by definition of $\bowtie$. Thus, we have
the thesis thanks to rule (wd-cons).

(owd-tail)

By hypothesis,
$\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},{p\mathbin{\cdot}(-1)})$ holds. By
inductive hypothesis, $\mathsf{wd}_{\rho}(\textit{s},{\mathit{m}^{-1}})$
holds. Moreover, for all $\textit{x}\in\mathit{dom}(\mathit{m})$ so that
$\mathit{sum}(\mathsf{m}(x),\pi\mathbin{\cdot}(-1))=i-1$, we have that
$\mathit{m}^{-1}(\textit{x})=i-1$ by definition of $\bowtie$. Thus, we have
the thesis thanks to rule (wd-tail).

(owd-nop)

By hypothesis, $\mathsf{owd}_{\rho}(\textit{s}_{1},\mathsf{m},\pi)$ and
$\mathsf{owd}_{\rho}(\textit{s}_{2},\mathsf{m},\pi)$ hold. By inductive
hypothesis, $\mathsf{wd}_{\rho}(\textit{s}_{1},\mathit{m})$ and
$\mathsf{wd}_{\rho}(\textit{s}_{2},\mathit{m})$ holds. Thus, we have the
thesis thanks to rule (wd-nop).

(owd-$\|$)

By hypothesis, $\mathsf{owd}_{\rho}(\textit{s}_{1},\mathsf{m},\pi)$ and
$\mathsf{owd}_{\rho}(\textit{s},\mathsf{m},{p\mathbin{\cdot}1})$ hold. By
inductive hypothesis, $\mathsf{wd}_{\rho}(\textit{s}_{1},\mathit{m})$ and
$\mathsf{wd}_{\rho}(\textit{s}_{2},\mathit{m}^{+1})$ hold. Moreover, for all
$\textit{x}\in\mathit{dom}(\mathit{m})$ so that
$\mathit{sum}(\mathsf{m}(x),\pi\mathbin{\cdot}1)=i+1$ , we have that
$\mathit{m}^{+1}(\textit{x})=i+1$ by definition of $\bowtie$. Thus, we have
the thesis thanks to rule (wd-$\|$).