11institutetext: DIBRIS, University of Genova

# Enhanced Regular Corecursion
for Data Streams

Davide Ancona  Pietro Barbieri  Elena Zucca

###### Abstract

We propose a simple calculus for processing _data streams_ (infinite flows of
data series), represented by finite sets of equations built on stream
operators. Furthermore, functions defining streams are _regularly corecursive_
, that is, cyclic calls are detected, avoiding non-termination as happens with
ordinary recursion in the call-by-value evaluation strategy. As we illustrate
by several examples, the combination of such two mechanisms provides a good
compromise between expressive power and decidability. Notably, we provide an
algorithm to check that the stream returned by a function call is represented
by a _well-formed set of equations_ which actually admits a unique solution,
hence access to an arbitrary element of the returned stream will never
diverge.

###### Keywords:

Operational semantics, stream programming, regular terms.

##  1 Introduction

Applications often deal with data structures which are conceptually infinite,
among those _data streams_ (infinite flows of data series) are a mainstream
example: as we venture deeper into the Internet of Things (IoT) era, stream
processing is becoming increasingly important. Indeed, all main IoT platforms
provide embedded and integrated engines for real time analysis of potentially
infinite flowing data series; such a process occurs before the data is stored
for efficiency and, as often happens in Computer Science, there is a trade-off
between the expressive power of the language, the efficiency of its
implementation and the decidability of properties important to guarantee
reliability and tractability.

Another related important problem is data stream generation, which is
essential to test complex distributed IoT systems; the deterministic
simulation of sensor data streams through a suitable language offers a
practical solution to IoT testing and favors early detection of some kinds of
bugs that can be fixed more easily before the deployment of the whole system.

A well-established solution to data stream generation and processing is _lazy
evaluation_ , as supported, e.g., in Haskell, and most stream libraries
offered by mainstream languages, as java.util.stream. In this approach,
conceptually infinite data streams are the result of a function or method
call, which is evaluated according to the call-by-need strategy. For instance,
in Haskell we can define one_two = 1:2:one_two, or even represent the list of
natural numbers as from 0, where from n = n:from(n+1). However, such a great
expressive power comes at a cost; let us consider, for instance, the
definition bad_stream = 0:tail bad_stream. The Haskell compiler does not
complain about this definition, and no problem arises at runtime as long as
the manipulation of bad_stream requires only its first element to be accessed;
anyway, any operation which needs to inspect bad_stream at a deeper level is
deemed to diverge. Unfortunately, it is not decidable to check, even at
runtime, whether the stream returned by a Haskell function is _well-defined_ ,
that is, all of its elements can be computed111This is what is also known as a
productive corecursive definition [5].; indeed, the full expressive power of
Haskell can be used to define streams by means of recursive functions. For
similar reasons, it is not decidable to check at runtime whether the streams
returned by two Haskell functions are equal.

More recently, a complementary approach has been considered in different
programming paradigms — functional [11], logic [17, 1, 7], and object-oriented
[2] — based on the following two ideas:

  * •

Infinite streams can be finitely represented by _finite sets of equations_
involving only the stream constructor, e.g., $\textit{x}=1:2:\textit{x}$. Such
a representation corresponds to what has been called by Courcelle in its
seminal paper [6] a _regular_ , a.k.a. _rational_ , tree, that is, a tree with
possibly infinite depth but a finite set of subtrees.

  * •

Functions are _regularly corecursive_ , that is, execution keeps track of
pending function calls, so that, when the same call is considered the second
time, this is detected, avoiding non-termination as happens with ordinary
recursion in the call-by-value evaluation strategy.

In this way, the Haskell stream one_two can be equivalently obtained by the
call222Differently from Haskell, for simplicity in our calculus functions are
uncurried, hence they take as arguments possibly empty tuples, delimited by
parentheses. one_two(), with the function one_two defined by one_two() =
1:2:one_two(). Indeed, with regular corecursion the result of this call is the
value corresponding to the unique solution of the equation
$\textit{x}=1:2:\textit{x}$. On the other hand, since the expressive power is
limited to regular streams, it is not possible to define a corecursive
function whose call returns the stream of natural numbers, as happens for the
from 0 Haskell example. However, there exist procedures for checking well-
defined streams and their equality, even with tractable algorithms.

In this paper, we propose a simple calculus of numeric streams which supports
regular corecursion and goes beyond regular streams by extending equations
with other typical stream operators besides the stream constructor: tail and
pointwise operators can be contained in stream equations and are therefore not
evaluated.

In this way, we are able to achieve a good compromise between expressive power
and decidability. Notably:

  * •

the extended shape of equations allows the definition of functions which
return non-regular streams; for instance, it is possible to obtain the stream
of natural numbers as from(0), by defining from(n)=n:(from(n)[+]repeat(1)),
with [+] the pointwise addition on numeric streams and repeat the function
defined by repeat(n)=n:repeat(n);

  * •

there exists a decidable procedure to dynamically check whether the stream
returned by a corecursive function is well-defined;

  * •

however, it is not possible to express _all_ streams computable with the lazy
evaluation approach, but only those which have a specific structure (that is,
can be expressed as the unique solution of a set of equations built with the
above mentioned operators).

In Sect. 2 we formally define the calculus, in Sect. 3 we show many
interesting examples, and in Sect. 4 we provide an operational
characterization of well-defined streams, proved to be a sufficient and
necessary condition for an access to an arbitrary index to never diverge. In
Sect. 5 we discuss related and further work. The Appendix contains more
examples of derivations.

##  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{op}}\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}&{:}{:}=&+\ \mid\ -\ \mid\ *\ \mid\
/&\mbox{{\small{numeric operation}}}\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,
conditional expressions, expressions built by stream operators, and function
calls. We consider the following stream operators: constructor (prepending a
numeric element), tail, and pointwise arithmetic operations. Numeric
expressions include the access to the $i$-th333For 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. 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 are 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{({pw})}}\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_{\approx\rho})}\\\
\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_{\approx\rho}({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-n})}}\displaystyle\frac{\mathit{at}_{\rho}(\textit{s},i-1)=\textit{n}^{\prime}}{\mathit{at}_{\rho}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},i)=\textit{n}^{\prime}}\
\begin{array}[]{l}i>0\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-
pw}})}}\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{op}}]}\textit{s}_{2},i)=\textit{n}_{1}\mathbin{\textit{op}}\textit{n}_{2}}\
\begin{array}[]{l}\end{array}\par\end{array}$

Figure 2: Stream calculus: operational semantics

To obtain (1), our approach is inspired by _capsules_ [10], which are
essentially expressions supporting cyclic references. That is, the _result_ of
the evaluation 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 and the pointwise
arithmetic operators, and $\rho$ is an _environment_ mapping a finite set of
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 $\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.

Moreover, the rules are parametric in the following other judgments, for which
different definitions will be discussed in Sect. 4:

  * •

$\mathit{wd}(\rho,\textit{x},\textit{s})$, that is, by adding the association
$\textit{x}\mapsto\textit{s}$ to the (well-defined) environment $\rho$, we
still get a well-defined environment.

  * •

${\textit{v}\approx_{\rho}\textit{v}^{\prime}}$, that is, the two values are
equivalent in the given environment444This equivalence is assumed to be the
identity on numeric and boolean values.. Then, $\tau_{\approx\rho}$ is the
extension of $\tau$ _up to equivalence_ in $\rho$:
$\tau_{\approx\rho}({f(\textit{v}_{1},\ldots,\textit{v}_{n})})=\textit{x}$ iff
there exist $\textit{v}^{\prime}_{1},\ldots,\textit{v}^{\prime}_{n}$ such that
$\tau(f(\textit{v}^{\prime}_{1},\ldots,\textit{v}^{\prime}_{n}))=\textit{x}$
and ${\textit{v}_{i}\approx_{\rho}\textit{v}^{\prime}_{i}}$ for all $i\in
1..n$.

Intuitively, a closed result $({{\textit{s}},{\rho}})$ is well-defined if it
denotes a unique stream (infinite sequence of numeric values), 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$). Finally, two stream values s and
$\textit{s}^{\prime}$ such that the results $({{\textit{s}},{\rho}})$ and
$({{\textit{s}^{\prime}},{\rho}})$ are closed and well-defined are equivalent
if they denote the same stream.

These notions can be generalized to open results and environments, assuming
that free variables denote unique streams, as will be formalized in Sect. 4.

Rules for values and conditional are straightforward. In rules (cons), (tail)
and (pw), arguments are evaluated, while the stream operator is applied
without any further evaluation; the fact that the tail and pointwise operators
are treated as the stream constructor ${\\_}\mathbin{\texttt{:}}{\\_}$ is
crucial to get results which denote non-regular streams as shown in Sect. 3.
However, when non-constructors are allowed to occur in values, ensuring well-
defined results become more challenging, because the usual simple syntactic
constraints that can be safely used for constructors [5] no longer work (see
more details in Sect. 4 and 5).

The rules for function call are based on a mechanism of cycle detection,
similar to that in [2]. They are given in a modular way. That is, 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 from such variable to the result of the evaluation of the body
keeps the environment well-defined. 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.

Rule (corec) is applied when a call is considered for the second time, as
expressed by the first side condition (note that cycle detection takes place
up to equivalence in the environment). The variable x is returned as result.
However, there is no associated value in the environment yet; in other words,
the result $({{\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}}\\}}})$.
For the full derivation, see Fig. 5 in the appendix.

As another example, if we consider the program f()=g(2:f()) g(s)=1:s, then the
derivation of 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{:}}{{2}\mathbin{\texttt{:}}{\textit{x}}}\\}$
is built on top of the derivation of
${{{{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{g}}(2:}}}{x}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small)}}}},\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{:}}{{2}\mathbin{\texttt{:}}{\textit{x}}}\\}}})$,
corresponding to the evaluation of g(2:x) where x is an operand of the stream
constructor whose result is passed as argument to the call to g, despite x is
not defined yet. For the full derivation, see Fig. 6 in the appendix.

Finally, rule (at) computes the $i$-th element of a stream expression. After
evaluation of the arguments, the numeric result is obtained by the auxiliary
judgment $\mathit{at}_{\rho}(\textit{s},i)=\textit{n}$, inductively defined in
the bottom part of the figure. If the stream value is a variable ((at-var)),
then the evaluation is propagated to the associated stream value in the
environment, if any. If, instead, the variable is free in the environment,
then execution is stuck; again, an implementation should raise a runtime error
instead. Fig. 7 in the appendix shows an example of stuck derivation. If the
stream value is built by the constructor, then the result is the first element
of the stream if the index is $0$ ((at-cons-0)); otherwise, the evaluation is
recursively propagated to its tail with the predecessor index ((at-cons-n)).
Conversely, if the stream is built by the tail operator ((at-tail)), then the
evaluation is recursively propagated to the stream argument with the successor
index. Finally, if the stream is built by a pointwise operation ((at-pw)),
then the evaluation is recursively propagated to the operands with the same
index and then the corresponding arithmetic operation is computed on the
results.

##  3 Examples

First we show some simple examples, to explain how regular corecursion works.
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 regular 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. 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}{\tiny\textsc{({invk})}}\displaystyle\frac{{\tiny\textsc{({cons})}}\displaystyle\frac{{\tiny\textsc{({value})}}\displaystyle\frac{}{}\hskip
13.50002pt{\tiny\textsc{({corec})}}\displaystyle\frac{}{{\mathtt{repeat(0)},\emptyset,\\{\mathtt{repeat(0)}\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}})}}{{\mathtt{{0}\mathbin{\texttt{:}}{repeat(0)}},\emptyset,\\{\mathtt{repeat(0)}\mapsto\textit{x}\\}}\\!\Downarrow\\!({{{0}\mathbin{\texttt{:}}{\textit{x}}},{\emptyset}})}}{{\mathtt{repeat(0)},\emptyset,\emptyset}\\!\Downarrow\\!({{\textit{x}},{\\{\textit{x}\mapsto{0}\mathbin{\texttt{:}}{\textit{x}}\\}}})}\end{array}$

$\begin{array}[]{l}{\tiny\textsc{({invk})}}\displaystyle\frac{{\tiny\textsc{({cons})}}\displaystyle\frac{{\tiny\textsc{({value})}}\displaystyle\frac{}{}\hskip
13.50002pt{\tiny\textsc{({invk})}}\displaystyle\frac{{\tiny\textsc{({cons})}}\displaystyle\frac{{\tiny\textsc{({value})}}\displaystyle\frac{}{}\hskip
13.50002pt{\tiny\textsc{({corec})}}\displaystyle\frac{}{{\mathtt{one\\_two()},\emptyset,\\{\mathtt{one\\_two()}\mapsto\textit{x},\
\mathtt{two\\_one()}\mapsto\textit{y}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}})}}{{\mathtt{2:one\\_two()},\emptyset,\\{\mathtt{one\\_two()}\mapsto\textit{x},\
\mathtt{two\\_one()}\mapsto\textit{y}\\}}\\!\Downarrow\\!({{2:\textit{x}},{\emptyset}})}}{{\mathtt{two\\_one()},\emptyset,\\{\mathtt{one\\_two()}\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\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}\\}}})}}{{\mathtt{one\\_two()},\emptyset,\emptyset}\\!\Downarrow\\!({{\textit{x}},{\\{\textit{x}\mapsto
1:\textit{y},\ \textit{y}\mapsto 2:\textit{x}\\}}})}\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
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()[+]repeat(1))

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

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

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

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

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

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

The definition of nat uses regular 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 regularly corecursive. For instance,
the call fact() returns
$({{\textit{z}},{\textit{z}\mapsto(\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 following alternative definition

⬇

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

relies, instead, on regular corecursion. Note the difference: the latter
version ensures termination only for regular streams, as in
incr_reg(one_two()), since, eventually, in the recursive call, the expression
s^ turns out to denote the initial stream; however, the computation does not
terminate for non-regular streams, as in incr_reg(nat()), which, however,
converges with incr.

The following function computes the stream of partial sums of the 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 all terms of the Taylor series of the exponential function;
hence, by accessing the $i$-th element of the stream, we have the following
approximation of the series:

>
> sum_expn(n)($i$)$=\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
contiguous data in the stream s w.r.t. a frame of length n:

⬇

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

For instance, aggr(3,s) returns the stream $\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 the frame of length n:

⬇

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

##  4 Well-defined environments and equivalent streams

In the semantic rules, we have left unspecified two notions: _well-defined
environments_ , and _equivalent streams_. We provide now a formal definition
in abstract terms. Then, we provide an operational definition of well-defined
environments.

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{op}}]}\textit{s}_{2}\rrbracket}\theta)(i)={\llbracket\textit{s}_{1}\rrbracket}\theta(i)\mathbin{\textit{op}}{\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$ with domain
$\textit{vars}(\rho)$ such that $\rho[\theta]=\theta$.

A closed environment $\rho$ is _well-defined_ if it has exactly one solution,
denoted $\textsf{sol}(\rho)$. 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.

Given a closed result $({{\textit{s}},{\rho}})$, with $\rho$ well-defined, we
define its semantics by
${\llbracket\textit{s}\rrbracket}{\rho}={\llbracket\textit{s}\rrbracket}\theta$
for $\theta=\textsf{sol}(\rho)$. Then, two stream values s and
$\textit{s}^{\prime}$ are _semantically equivalent in $\rho$_ if
${\llbracket\textit{s}\rrbracket}{\rho}={\llbracket\textit{s}^{\prime}\rrbracket}{\rho^{\prime}}$.

We now consider the non-trivial problem of ensuring that a closed environment
$\rho$ is well-defined; if environments would be allowed to contain only the
stream constructor, then it would suffice to require all non-free variables to
be _guarded_ by the stream constructor [5]. For instance, the environment
${\\{\textit{x}\mapsto{1}\mathbin{\texttt{:}}{\textit{x}}\\}}$ satisfies such
a syntactic condition, and is well-defined, while in the non well-defined
environment ${\\{\textit{x}\mapsto\textit{x}\\}}$ variable x is not guarded by
the constructor.

However, when non constructors as the tail and pointwise operators come into
play, the fact that variables are guarded by the stream constructor no longer
ensures that the environment is well-defined; let us consider for instance
$\rho=\\{\textit{x}\mapsto{0}\mathbin{\texttt{:}}{{\textit{x}}{\char
94\relax}}\\}$ corresponding to the definition of bad_stream shown in Sect. 1:
$\rho$ is not well-defined since it admits infinite solutions (all streams
starting with 0), although variable x is guarded by the stream constructor.

To ensure well-defined environments a more complex check is needed: in Fig. 3
we provide an operational characterization of well-defined environments.

$\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 natural
numbers}}}\end{array}$
$\begin{array}[]{l}\\\
{\tiny\textsc{({main})}}\displaystyle\frac{\mathsf{wd}(\textit{x},\rho\\{\textit{x}\mapsto\textit{v}\\},\emptyset)}{\mathit{wd}(\rho,\textit{x},\textit{v})}\
\begin{array}[]{l}\end{array}\hskip 13.50002pt{\tiny\textsc{({wf-
var})}}\displaystyle\frac{\mathsf{wd}(\rho(\textit{x}),\rho,\mathit{m}\\{\textit{x}\mapsto
0\\})}{\mathsf{wd}(\textit{x},\rho,\mathit{m})}\
\begin{array}[]{l}\textit{x}\not\in\mathit{dom}(\mathit{m})\end{array}\\\\[19.37492pt]
{\tiny\textsc{({wf-
corec})}}\displaystyle\frac{}{\mathsf{wd}(\textit{x},\rho,\mathit{m})}\
\begin{array}[]{l}\textit{x}\in\mathit{dom}(\mathit{m})\\\
\mathit{m}(x)>0\end{array}\hskip 13.50002pt{{\tiny\textsc{({wf-
fv})}}\displaystyle\frac{}{\mathsf{wd}(\textit{x},\rho,\mathit{m})}\
\begin{array}[]{l}\textit{x}\not\in\mathit{dom}(\rho)\end{array}}\\\\[23.24991pt]
{\tiny\textsc{({wf-
cons})}}\displaystyle\frac{\mathsf{wd}(\textit{s},\rho,{\mathit{m}^{+1}})}{\mathsf{wd}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},\rho,\mathit{m})}\
\begin{array}[]{l}\end{array}\hskip 13.50002pt{\tiny\textsc{({wf-
tail})}}\displaystyle\frac{\mathsf{wd}(\textit{s},\rho,{\mathit{m}^{-1}})}{\mathsf{wd}({\textit{s}}{\char
94\relax},\rho,\mathit{m})}\ \begin{array}[]{l}\end{array}{\tiny\textsc{({wf-
pw})}}\displaystyle\frac{\mathsf{wd}(\textit{s}_{1},\rho,\mathit{m})\hskip
7.20003pt\mathsf{wd}(\textit{s}_{2},\rho,\mathit{m})}{\mathsf{wd}(\textit{s}_{1}{[{\textit{op}}]}\textit{s}_{2},\rho,\mathit{m})}\
\begin{array}[]{l}\end{array}\end{array}$

Figure 3: Operational definition of well-defined environments

The judgment $\mathit{wd}(\rho,\textit{x},\textit{s})$ used in the side
condition of rule (invk) holds if
$\mathsf{wd}(\textit{x},\rho\\{\textit{x}\mapsto\textit{v}\\},\emptyset)$
holds. The judgment $\mathsf{wd}(\textit{s},\rho,\emptyset)$ means that a
result is well-defined. 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}(\textit{s},\rho,\mathit{m})$ is a map from variables to natural
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 (wf-var), a variable x
defined in the environment is added in the map, with initial value $0$, the
first time it is found. In rule (wf-corec), when it is found the second time,
it is checked that more constructors than tail operators have been traversed.
In rule (wf-fv), a free variable is considered well-defined.555Indeed, non-
well-definedness can only be detected on closed results. In rules (wf-cons),
(wf-tail), and (wf-pw), the value associated with a variable is
incremented/decremented by one each time a constructor and tail operator are
traversed, respectively.

As an example of derivation of well-definedness and access to the $i$-th
element, in Fig. 4 we consider 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() with nat defined as in Sect. 3.

$\begin{array}[]{l}{\tiny\textsc{({wf-
var})}}\displaystyle\frac{{\tiny\textsc{({wf-
cons})}}\displaystyle\frac{{\tiny\textsc{({{wf-
pw}})}}\displaystyle\frac{{\tiny\textsc{({wf-
corec})}}\displaystyle\frac{}{\mathsf{wd}(\textit{x},\rho,\\{\textit{x}\mapsto
1\\})}\ \begin{array}[]{l}\end{array}\hskip 13.50002pt{\tiny\textsc{({wf-
var})}}\displaystyle\frac{{\tiny\textsc{({wf-
cons})}}\displaystyle\frac{{\tiny\textsc{({wf-
corec})}}\displaystyle\frac{}{\mathsf{wd}(\textit{y},\rho,\\{\textit{x}\mapsto
1,\textit{y}\mapsto 1\\})}\
\begin{array}[]{l}\end{array}}{\mathsf{wd}({1}\mathbin{\texttt{:}}{\textit{y}},\rho,\\{\textit{x}\mapsto
1,\textit{y}\mapsto 0\\})}\
\begin{array}[]{l}\end{array}}{\mathsf{wd}(\textit{y},\rho,\\{\textit{x}\mapsto
1\\})}\ \begin{array}[]{l}\end{array}}{\mathsf{wd}(\textit{x}\ [+]\
\textit{y},\rho,\\{\textit{x}\mapsto 1\\})}\
\begin{array}[]{l}\end{array}}{\mathsf{wd}({0}\mathbin{\texttt{:}}{(\textit{x}\
[+]\ \textit{y})},\rho,\\{\textit{x}\mapsto 0\\})}\
\begin{array}[]{l}\end{array}}{\mathsf{wd}(\textit{x},\rho,\emptyset)}\
\begin{array}[]{l}\end{array}\end{array}$
$\begin{array}[]{l}{\tiny\textsc{({at-
var})}}\displaystyle\frac{{\tiny\textsc{({at-
cons-n})}}\displaystyle\frac{{\tiny\textsc{({at-
op})}}\displaystyle\frac{{\tiny\textsc{({at-
var})}}\displaystyle\frac{\begin{array}[]{c}{\tiny\textsc{({at-
cons-0})}}\displaystyle\frac{}{\mathit{at}_{\rho}({0}\mathbin{\texttt{:}}{(\textit{x}\
[+]\ \textit{y})},0)=0}\ \begin{array}[]{l}\end{array}\\\
\vdots\end{array}}{\mathit{at}_{\rho}(\textit{x},i-1)=i-1}\
\begin{array}[]{l}\end{array}\hskip 13.50002pt{\tiny\textsc{({at-
var})}}\displaystyle\frac{\begin{array}[]{c}{\tiny\textsc{({at-
cons-0})}}\displaystyle\frac{}{\mathit{at}_{\rho}({1}\mathbin{\texttt{:}}{\textit{y}},0)=1}\
\begin{array}[]{l}\end{array}\\\
\vdots\end{array}}{\mathit{at}_{\rho}(\textit{y},i-1)=1}\
\begin{array}[]{l}\end{array}}{\mathit{at}_{\rho}(\textit{x}\ [+]\
\textit{y},i-1)=i}\
\begin{array}[]{l}\end{array}}{\mathit{at}_{\rho}({0}\mathbin{\texttt{:}}{(\textit{x}\
[+]\ \textit{y})},i)=i}\
\begin{array}[]{l}\end{array}}{\mathit{at}_{\rho}(\textit{x},i)=i}\
\begin{array}[]{l}\end{array}\end{array}$

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

In Fig. 8 in the Appendix we consider a trickier example, that is, the result
$({{\textit{x}},{\\{\textit{x}\mapsto{0}\mathbin{\texttt{:}}{{1}\mathbin{\texttt{:}}{{({2}\mathbin{\texttt{:}}{{\textit{x}}{\char
94\relax}})}{\char 94\relax}}}\\}}})$. Its semantics is the stream
$0,1,1,1,\ldots$.

We show now that well-definedness of a result is a necessary and sufficient
condition for termination of access to an arbitrary index. To formally express
and prove this statement, we introduce some definitions and notations.

First of all, since the numeric value obtained as result is not relevant for
the following technical treatment, for simplicity we will write
$\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}(\textit{s}^{\prime},\rho,\mathit{m}^{\prime})\vdash\mathsf{wd}(\textit{s},\rho,\mathit{m})$
to mean that $\mathsf{wd}(\textit{s}^{\prime},\rho,\mathit{m}^{\prime})$ is a
premise of a (meta-)rule where $\mathsf{wd}(\textit{s},\rho,\mathit{m})$ is
the consequence, and $\vdash^{\star}$ for the reflexive and transitive closure
of this relation. Moreover,
$\mathsf{wd}(\textit{x},\rho,\mathit{m}^{\prime})\vdash^{\star}_{\mathcal{X}}\mathsf{wd}(\textit{s},\rho,\mathit{m})$,
with $\textit{x}\not\in\mathcal{X}$, means that in the path there can be nodes
of shape $\mathsf{wd}(\textit{y},\rho,\\_)$ only for
$\textit{y}\in\mathcal{X}$ and non-repeated. We use analogous notations for
the judgment $\mathit{at}_{\rho}(\textit{s},i)$.

###### Lemma 1

  1. 1.

If
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s},i)$,
then
$\mathit{at}_{\rho}(\textit{x},i^{\prime}+k)\vdash^{\star}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s},i+k)$,
for each $k\geq 0$.

  2. 2.

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

  3. 3.

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

###### Proof

  1. 1.

Immediate by induction on the rules.

  2. 2.

For each $\mathsf{wd}(\textit{s},\rho,\mathit{m})$ there is exactly one
applicable rule, unless in the case $\mathsf{wd}(\textit{x},\rho,\mathit{m})$
with $\mathit{m}(\textit{x})\leq 0$. Since $\textit{vars}(\textit{s})$ is a
finite set, the derivation cannot be infinite. Hence, there is no derivation
for $\mathsf{wd}(\textit{s},\rho,\emptyset)$ iff there is a finite path from
$\mathsf{wd}(\textit{s},\rho,\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})$ and
$\mathit{m}^{\prime}(\textit{x})\leq 0$.

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

That is, condition (wf-stuck) holds, with
$\mathcal{X}^{\prime}=\\{\textit{x}_{1},\ldots,\textit{x}_{n}\\}$, and
$\mathcal{X}=\\{\textit{y}_{1},\ldots,\textit{y}_{m}\\}$.

  3. 3.

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 an infinite path from $\mathit{at}_{\rho}(\textit{s},j)$ of judgments
on variables in $\mathit{dom}(\rho)$, and a (first) repeated variable with a
greater or equal index, hence, thanks to Lemma 1-(1), of the shape below,
where $m,n,k\geq 0$:

$\ldots\mathit{at}_{\rho}(\textit{x}_{n},i_{n}+k)\ldots\mathit{at}_{\rho}(\textit{x}_{1},i_{1}+k)\mathit{at}_{\rho}(\textit{x},i+k)\mathit{at}_{\rho}(\textit{x}_{n},i_{n})\ldots$
$\ldots\mathit{at}_{\rho}(\textit{x}_{1},i_{1})\mathit{at}_{\rho}(\textit{x},i)\mathit{at}_{\rho}(\textit{y}_{m},j_{m})\ldots\mathit{at}_{\rho}(\textit{y}_{1},j_{1})\ldots\mathit{at}_{\rho}(\textit{s},j)$

That is, condition (at-$\infty$) holds, with
$\mathcal{X}^{\prime}=\\{\textit{x}_{1},\ldots,\textit{x}_{n}\\}$, and
$\mathcal{X}=\\{\textit{y}_{1},\ldots,\textit{y}_{m}\\}$.

###### Lemma 2

For $\textit{x}\in\mathit{dom}(\mathit{m})$, the following conditions are
equivalent:

  1. 1.

$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s},i)$
for some $i^{\prime},i$

  2. 2.

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

###### Proof

1$\Rightarrow 2$

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

Base

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

Inductive step

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

(at-var)

We have $\mathit{at}_{\rho}(\textit{y},i)$, with $\textit{y}\neq\textit{x}$
since the length of the path is $>0$, and
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\chi\setminus\\{\textit{y}\\}}\mathit{at}_{\rho}(\rho(\textit{y}),i)$.
Moreover, we can derive $\mathsf{wd}(\textit{y},\rho,\mathit{m})$ by rule (wf-
var), and by inductive hypothesis we also have
$\mathsf{wd}(\textit{x},\rho,\mathit{m}^{\prime})\vdash^{\star}_{\chi\setminus\\{\textit{y}\\}}\mathsf{wd}(\rho(\textit{y}),\rho,\mathit{m}\\{\textit{y}\mapsto
0\\})$, and $\mathit{m}^{\prime}(\textit{x})=\mathit{m}\\{\textit{y}\mapsto
0\\}(\textit{x})+i-i^{\prime}$, hence we get the thesis.

(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)

We have $\mathit{at}_{\rho}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},i)$,
and
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s},i-1)$.
Moreover, we can derive
$\mathsf{wd}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},\rho,\mathit{m})$ by
rule (wf-cons), and by inductive hypothesis we also have
$\mathsf{wd}(\textit{x},\rho,\mathit{m}^{\prime})\vdash^{\star}_{\mathcal{X}}\mathsf{wd}(\textit{s},\rho,\mathit{m}^{+1})$,
with
${\mathit{m}^{\prime}(\textit{x})=\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-pw)

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}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s}_{1},i)$,
or
${\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s}_{2},i)}$.
Assume the first case holds, the other is analogous. Moreover, we can derive
$\mathsf{wd}(\textit{s}_{1}{[{\textit{op}}]}\textit{s}_{2},\rho,\mathit{m})$
by rule (wf-pw), and by inductive hypothesis we also have
$\mathsf{wd}(\textit{x},\rho,\mathit{m}^{\prime})\vdash^{\star}_{\mathcal{X}}\mathsf{wd}(\textit{s}_{1},\rho,\mathit{m})$,
with $\mathit{m}^{\prime}(\textit{x})=\mathit{m}(\textit{x})+i-i^{\prime}$,
hence we get the thesis.

2$\Rightarrow$ 1

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

Base

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

Inductive step

By cases on the rule applied to derive
$\mathsf{wd}(\textit{s},\rho,\mathit{m})$.

(wf-var)

We have $\mathsf{wd}(\textit{y},\rho,\mathit{m})$, with
$\textit{y}\notin\mathit{dom}(\mathit{m})$, $\textit{y}\neq\textit{x}$ since
${\textit{x}\in\mathit{dom}(\mathit{m})}$, and
$\mathsf{wd}(\textit{x},\rho,\mathit{m}^{\prime})\vdash^{\star}_{\mathcal{X}\setminus\\{\textit{y}\\}}\mathsf{wd}(\rho(\textit{y}),\rho,\mathit{m}\\{\textit{y}\mapsto
0\\})$. By inductive hypothesis we have
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\mathcal{X}\setminus\\{\textit{y}\\}}\mathit{at}_{\rho}(\rho(\textit{y}),i)$
for some $i^{\prime},i$ such that
$\mathit{m}^{\prime}(\textit{x})=\mathit{m}(\textit{x})+i-i^{\prime}$.
Moreover, since $\textit{y}\in\mathit{dom}(\rho)$,
$\mathit{at}_{\rho}(\rho(\textit{y}),i)\vdash\mathit{at}_{\rho}(\textit{y},i)$
by rule (at-var), hence we get
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\chi}\mathit{at}_{\rho}(\textit{y},i)$.

(wf-corec)

Empty case, since the derivation for $\mathsf{wd}(\textit{y},\rho,\mathit{m})$
would not contain a node $\mathsf{wd}(\textit{x},\rho,\mathit{m})$.

(wf-fv)

Empty case, since the derivation for $\mathsf{wd}(\textit{y},\rho,\mathit{m})$
would not contain a node $\mathsf{wd}(\textit{x},\rho,\mathit{m})$.

(wf-cons)

We have
$\mathsf{wd}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},\rho,\mathit{m})$,
and
$\mathsf{wd}(\textit{x},\rho,\mathit{m}^{\prime})\vdash^{\star}_{\mathcal{X}}\mathsf{wd}(\textit{s},\rho,\mathit{m}^{+1})$.
By inductive hypothesis we have
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s},i)$
for some $i^{\prime},i$ such that
$\mathit{m}^{\prime}(\textit{x})=\mathit{m}^{+1}(\textit{x})+i-i^{\prime}$.
Moreover,
$\mathit{at}_{\rho}(\textit{s},i)\vdash\mathit{at}_{\rho}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},i+1)$
by rule (at-cons-n), hence we get
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\chi}\mathit{at}_{\rho}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},i+1)$
with $\mathit{m}^{\prime}(\textit{x})=\mathit{m}(\textit{x})+i+1-i^{\prime}$,
as requested.

(wf-tail)

We have $\mathsf{wd}({\textit{s}}{\char 94\relax},\rho,\mathit{m})$, and
$\mathsf{wd}(\textit{x},\rho,\mathit{m}^{\prime})\vdash^{\star}_{\mathcal{X}}\mathsf{wd}(\textit{s},\rho,\mathit{m}^{-1})$.
By inductive hypothesis we have
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s},i)$
for some $i^{\prime},i$ such that
$\mathit{m}^{\prime}(\textit{x})=\mathit{m}^{-1}(\textit{x})+i-i^{\prime}$. We
can assume $i>0$ thanks to Lemma 1-(1). Hence,
$\mathit{at}_{\rho}(\textit{s},i)\vdash\mathit{at}_{\rho}({\textit{n}}\mathbin{\texttt{:}}{\textit{s}},i-1)$
by rule (at-tail), hence we get
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\chi}\mathit{at}_{\rho}({\textit{s}}{\char
94\relax},i-1)$ with
$\mathit{m}^{\prime}(\textit{x})=\mathit{m}(\textit{x})+i-1-i^{\prime}$, as
requested.

(wf-pw)

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

###### Lemma 3

For $\textit{x}\not\in\mathit{dom}(\mathit{m})$, the following conditions are
equivalent:

  1. 1.

$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s},i)$
for some $i^{\prime},i$

  2. 2.

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

###### Proof

Easy variant of the proof of Lemma 2.

###### Theorem 4.1

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

###### Proof

We prove that $\mathit{at}_{\rho}(\textit{s},j)$ has an infinite derivation
for some $j$ iff $\mathsf{wd}(\textit{s},\rho,\emptyset)$ has no derivation.

$\Rightarrow$

By Lemma 1-(3),we have that the following condition holds:

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

Then, starting from the right, by Lemma 3 we have
${\mathsf{wd}(\textit{x},\rho,\mathit{m})\vdash^{\star}_{\mathcal{X}}\mathsf{wd}(\textit{s},\rho,\emptyset)}$
for some $\mathit{m}$ such that $\textit{x}\not\in\mathit{dom}(\mathit{m})$;
by rule (wf-var) we have
${\mathsf{wd}(\rho(\textit{x}),\rho,\mathit{m}\\{\textit{x}\mapsto
0\\})\vdash\mathsf{wd}(\textit{x},\rho,\mathit{m})}$, and finally by Lemma 2
we have:
(wf-stuck)
$\mathsf{wd}(\textit{x},\rho,\mathit{m}^{\prime})\vdash^{\star}_{\mathcal{X}^{\prime}}\mathsf{wd}(\rho(\textit{x}),\rho,\mathit{m}\\{\textit{x}\mapsto
0\\})\vdash\mathsf{wd}(\textit{x},\rho,\mathit{m})\vdash^{\star}_{\mathcal{X}}\mathsf{wd}(\textit{s},\rho,\emptyset)$
for some $\textit{x}\in\mathit{dom}(\rho)$,
$\mathcal{X}^{\prime},\mathcal{X}$, and $\mathit{m}^{\prime},\mathit{m}$ s.t.
$\textit{x}\not\in\mathit{dom}(\mathit{m}),\mathit{m}^{\prime}(\textit{x})=k\leq
0$.
hence we get the thesis.

$\Leftarrow$

By Lemma 1-(2),we have that the condition (wf-stuck) above holds. Then,
starting from the left, by Lemma 2 we have
$\mathit{at}_{\rho}(\textit{x},i^{\prime})\vdash^{\star}_{\mathcal{X}^{\prime}}\mathit{at}_{\rho}(\rho(\textit{x}),i)$
for some $i^{\prime},i$ such that $i-i^{\prime}=k\leq 0$; by rule (at-var) we
have
$\mathit{at}_{\rho}(\rho(\textit{x}),i)\vdash\mathit{at}_{\rho}(\textit{x},i)$,
and by Lemma 3 we have
$\mathit{at}_{\rho}(\textit{x},j^{\prime})\vdash^{\star}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s},j)$
for some $j^{\prime},j$. If $i=j^{\prime}+h$, $h\geq 0$, then by Lemma 1-(1)
we have

$\mathit{at}_{\rho}(\textit{x},i+k)\vdash^{\star}_{\mathcal{X}^{\prime}}\mathit{at}_{\rho}(\rho(\textit{x}),i)\vdash\mathit{at}_{\rho}(\textit{x},i)\vdash^{\star}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s},j+h)$

If $j^{\prime}=i+h$, $h\geq 0$, then by Lemma 1-(1) we have

$\mathit{at}_{\rho}(\textit{x},i+k+h)\vdash^{\star}_{\mathcal{X}^{\prime}}\mathit{at}_{\rho}(\rho(\textit{x}),i)\vdash\mathit{at}_{\rho}(\textit{x},i+h)\vdash^{\star}_{\mathcal{X}}\mathit{at}_{\rho}(\textit{s},j)$.

In both cases, the derivation of $\mathit{at}_{\rho}(\textit{s},j)$ is
infinite.

##  5 Related and future work

As mentioned in Sect. 1, our approach extends regular corecursion, where the
semantics keeps track of method/function calls. Regular corecursion originated
from _co-SLD resolution_ [16, 17, 1, 3], where already considered goals (up to
unification), called _coinductive hypotheses_ , are considered successful.
Language constructs that support this programming style have also been
proposed in the functional [11] and object-oriented [4, 2] paradigm.

There have been a few attempts of extending the expressive power of regular
corecursion. Notably, _structural resolution_ [12, 13] is a proposed
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 on infinite trees [6], where Courcelle
introduces algebraic trees and equations as generalizations of regular ones.

For what concerns the operators considered in the calculus and some examples,
our main sources of inspiration have been the works of Rutten [14], where a
coinductive calculus of streams of real numbers is defined, and Hinze [9],
where a calculus of generic streams is defined in a constructive way and
implemented in Haskell.

The problem of ensuring well-defined corecursive definitions has been also
considered in the context of type theory and proof assistants. We have shown
in Sect. 4 that simple guarded definitions [5] do not work properly in case
values are allowed to contain non constuctors as the tail operator; a more
complex approach based on a type system has been proposed by Sacchini [15] for
an extension of the calculus of constructions which is more expressive than
what considered here; however, as opposed to what happens with the judgment
$\mathit{wd}$ defined in Sect. 4, corecursive calls to the result of an
application of tail are never well-typed even in case of well-defined streams
as happens for the definition of fib as given in Sect. 3.

Lastly, D’Angelo et al. presented LOLA [8], a specification language for
runtime monitoring that manipulates streams. The general idea behind the
framework is to generate a set of output streams, starting from a given set of
input streams. The main difference with respect to our work is that LOLA only
allows streams with a finite number of elements. In this framework, well-
formedness is checked by relying on a dependency graph, which keeps track of
relations between the processed streams. The vertices of this graph are the
streams, while the edges represent the dependencies between them. Each edge is
weighted with a value $\omega$ to point the fact that a stream depends on
another one shifted by $\omega$ positions. Then, the well-formedness
constraint is that each closed-walk inside the graph must have a total weight
different from $0$. These syntactic constraints appear to be very similar to
the approach we used for predicate $\mathit{wd}$.

Our main technical result is Theorem 4.1, stating that passing the well-
definedness check performed at runtime for each function call is necessary and
sufficient to prevent non-termination in accessing elements in the resulting
stream at an arbitrary index. In future work, we plan to also prove soundness
of the operational well-definedness with respect to its abstract definition.
Completeness does not hold, as shown by the example zeros() = repeat(0) [*]
zeros() which is not well-defined operationally, but admits as unique solution
the stream of all zeros. On the other hand, the simplest operational
characterization of equivalence of stream values is syntactic equivalence.
This works for all the examples presented in this paper, but is, again, not
complete with respect to the abstract definition, as illustrated below:

⬇

first(s) = s(0):first(s) // works with syntactic equivalence

first2(s) = s(0):first2(s(0):s^) // does not work

Indeed, we get an infinite derivation for first2(repeat(1)) with call traces
of increasing shape
${{{{\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{first2}}({\@listingGroup{}{$x$}})}}}}\mapsto\textit{y}_{1},\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{first2}}(1:{\@listingGroup{}{$x$}}\textasciicircum)}}}}\mapsto\textit{y}_{2},\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\small{\@listingGroup{ltx_lst_identifier}{first2}}(1:(1:{\@listingGroup{}{$x$}}\textasciicircum)\textasciicircum)}}}}\mapsto\textit{y}_{3},\ldots\\}}$
in the environment
$\\{\textit{x}\mapsto{1}\mathbin{\texttt{:}}{\textit{x}}\\}$. In future work
we plan to investigate more expressive operational characterizations of
equivalence.

## 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 and Agostino Dovier.  A theoretical perspective of coinductive logic programming.  Fundamenta Informaticae, 140(3-4):221–246, 2015.
  * [4] Davide Ancona and Elena Zucca.  Corecursive Featherweight Java.  In FTfJP’12 - Formal Techniques for Java-like Programs, pages 3–10. ACM Press, 2012.
  * [5] Thierry Coquand.  Infinite objects in type theory.  In Types for Proofs and Programs, International Workshop TYPES’93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, pages 62–78, 1993.
  * [6] Bruno Courcelle.  Fundamental properties of infinite trees.  Theoretical Computer Science, 25:95–169, 1983.
  * [7] 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.
  * [8] Ben D’Angelo, Sriram Sankaranarayanan, César Sánchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra, and Zohar Manna.  LOLA: runtime monitoring of synchronous systems.  In 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pages 166–174, 2005.
  * [9] Ralf Hinze.  Concrete stream calculus: An extended study.  Journal of Functional Programming, 20(5–6):463–535, 2010.
  * [10] Jean-Baptiste Jeannin and Dexter Kozen.  Computing with capsules.  Journal of Automata, Languages and Combinatorics, 17(2-4):185–204, 2012.
  * [11] Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva.  CoCaml: Functional programming with regular coinductive types.  Fundamenta Informaticae, 150:347–377, 2017.
  * [12] 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.
  * [13] Ekaterina Komendantskaya, John Power, and Martin Schmidt.  Coalgebraic logic programming: from semantics to implementation.  J. Log. Comput., 26(2):745–783, 2016.
  * [14] Jan J. M. M. Rutten.  A coinductive calculus of streams.  Mathematical Structures in Computer Science, 15(1):93–147, 2005\.
  * [15] Jorge Luis Sacchini.  Type-based productivity of stream definitions in the calculus of constructions.  In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 233–242, 2013.
  * [16] Luke Simon.  Extending logic programming with coinduction.  PhD thesis, University of Texas at Dallas, 2006.
  * [17] 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]
{\tiny\textsc{({invk})}}\displaystyle\frac{{\tiny\textsc{({invk})}}\displaystyle\frac{{\tiny\textsc{({cons})}}\displaystyle\frac{{\tiny\textsc{({val})}}\displaystyle\frac{}{{1,\emptyset,\\{\textit{f}()\mapsto\textit{x},\textit{g}()\mapsto\textit{y}\\}}\\!\Downarrow\\!({{1},{\emptyset}})}\
\begin{array}[]{l}\end{array}\hskip
13.50002pt{\tiny\textsc{({corec})}}\displaystyle\frac{}{{\textit{f}(),\emptyset,\\{\textit{f}()\mapsto\textit{x},\textit{g}()\mapsto\textit{y}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}})}\
\begin{array}[]{l}\end{array}}{{1:\textit{f}(),\emptyset,\\{\textit{f}()\mapsto\textit{x},\textit{g}()\mapsto\textit{y}\\}}\\!\Downarrow\\!({{1:\textit{x}},{\emptyset}})}\
\begin{array}[]{l}\end{array}}{{\textit{g}(),\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{y}},{\\{\textit{y}\mapsto
1:\textit{x}\\}}})}\
\begin{array}[]{l}\end{array}}{{\textit{f}(),\emptyset,\emptyset}\\!\Downarrow\\!({{\textit{x}},{\\{\textit{x}\mapsto\textit{y},\textit{y}\mapsto
1:\textit{x}\\}}})}\ \begin{array}[]{l}\end{array}\end{array}$

Figure 5: Example of derivation

$\begin{array}[]{l}\textit{f}()=\textit{g}(2:\textit{f}())\\\
g(s)=1:s\\\\[23.24991pt]
{\tiny\textsc{({invk})}}\displaystyle\frac{{\tiny\textsc{({args})}}\displaystyle\frac{{\tiny\textsc{({cons})}}\displaystyle\frac{{\tiny\textsc{({val})}}\displaystyle\frac{}{{2,\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{2},{\emptyset}})}\
\begin{array}[]{l}\end{array}\hskip
13.50002pt{\tiny\textsc{({corec})}}\displaystyle\frac{}{{\textit{f}(),\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}})}\
\begin{array}[]{l}\end{array}}{{2:\textit{f}(),\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{2:\textit{x}},{\emptyset}})}\
\begin{array}[]{l}\end{array}}{{\textit{g}(2:\textit{f}()),\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{y}},{\\{\textit{y}\mapsto
1:2:\textit{x}\\}}})}\ \begin{array}[]{l}\end{array}\hskip
13.50002ptT_{1}}{{\textit{f}(),\emptyset,\emptyset}\\!\Downarrow\\!({{\textit{x}},{\\{\textit{x}\mapsto\textit{y},\textit{y}\mapsto
1:2:\textit{x}\\}}})}\ \begin{array}[]{l}\end{array}\\\\[30.99988pt]
T_{1}={\tiny\textsc{({invk})}}\displaystyle\frac{{\tiny\textsc{({val})}}\displaystyle\frac{}{{1:2:\textit{x},\emptyset,\\{\textit{g}(2:\textit{x})\mapsto\textit{y},\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{1:2:\textit{x}},{\emptyset}})}\
\begin{array}[]{l}\end{array}}{{\textit{g}(2:\textit{x}),\emptyset,\\{\textit{f}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{y}},{\\{\textit{y}\mapsto
1:2:\textit{x}\\}}})}\ \begin{array}[]{l}\end{array}\end{array}$

Figure 6: Example of derivation

$\begin{array}[]{l}\textit{undef}()=(\textit{undef}()(0)):\textit{undef}()\\\\[23.24991pt]
{\tiny\textsc{({invk})}}\displaystyle\frac{{\tiny\textsc{({cons})}}\displaystyle\frac{T_{1}\hskip
13.50002pt{\tiny\textsc{({corec})}}\displaystyle\frac{}{{\textit{undef}(),\emptyset,\\{\textit{undef}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}})}\
\begin{array}[]{l}\end{array}}{{(\textit{undef}()(0)):\textit{undef}(),\emptyset,\\{\textit{undef}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{?},{?}})}\
\begin{array}[]{l}\end{array}}{{\textit{undef}(),\emptyset,\emptyset}\\!\Downarrow\\!({{?},{?}})}\
\begin{array}[]{l}\end{array}\\\\[30.99988pt]
T_{1}={\tiny\textsc{({at})}}\displaystyle\frac{{\tiny\textsc{({corec})}}\displaystyle\frac{}{{\textit{undef}(),\emptyset,\\{\textit{undef}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{\textit{x}},{\emptyset}})}\
\begin{array}[]{l}\end{array}\hskip
13.50002pt{\tiny\textsc{({val})}}\displaystyle\frac{}{{0,\emptyset,\\{\textit{undef}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{0},{\emptyset}})}\
\begin{array}[]{l}\end{array}}{{\textit{undef}()(0),\emptyset,\\{\textit{undef}()\mapsto\textit{x}\\}}\\!\Downarrow\\!({{?},{?}})}\
\begin{array}[]{l}\mathit{at}_{\emptyset}(\textit{x},0)=?\end{array}\end{array}$

Figure 7: Example of stuck derivation

$\begin{array}[]{l}{\tiny\textsc{({wf-
var})}}\displaystyle\frac{{\tiny\textsc{({wf-
cons})}}\displaystyle\frac{{\tiny\textsc{({wf-
cons})}}\displaystyle\frac{{\tiny\textsc{({wf-
tail})}}\displaystyle\frac{{\tiny\textsc{({wf-
cons})}}\displaystyle\frac{{\tiny\textsc{({wf-
tail})}}\displaystyle\frac{{\tiny\textsc{({wf-
corec})}}\displaystyle\frac{}{\mathsf{wd}(\textit{x},\rho,\\{x\mapsto 1\\})}\
\begin{array}[]{l}\end{array}}{\mathsf{wd}({\textit{x}}{\char
94\relax},\rho,\\{x\mapsto 2\\})}\
\begin{array}[]{l}\end{array}}{\mathsf{wd}({2}\mathbin{\texttt{:}}{{\textit{x}}{\char
94\relax}},\rho,\\{x\mapsto 1\\})}\
\begin{array}[]{l}\end{array}}{\mathsf{wd}({({2}\mathbin{\texttt{:}}{{\textit{x}}{\char
94\relax}})}{\char 94\relax},\rho,\\{x\mapsto 2\\})}\
\begin{array}[]{l}\end{array}}{\mathsf{wd}({1}\mathbin{\texttt{:}}{{({2}\mathbin{\texttt{:}}{{\textit{x}}{\char
94\relax}})}{\char 94\relax}},\rho,\\{x\mapsto 1\\})}\
\begin{array}[]{l}\end{array}}{\mathsf{wd}({0}\mathbin{\texttt{:}}{{1}\mathbin{\texttt{:}}{{({2}\mathbin{\texttt{:}}{{\textit{x}}{\char
94\relax}})}{\char 94\relax}}},\rho,\\{x\mapsto 0\\})}\
\begin{array}[]{l}\end{array}}{\mathsf{wd}(\textit{x},\rho,\emptyset)}\
\begin{array}[]{l}\end{array}\end{array}$
$\begin{array}[]{l}{\tiny\textsc{({at-
var})}}\displaystyle\frac{{\tiny\textsc{({at-
cons-n})}}\displaystyle\frac{{\tiny\textsc{({at-
cons-n})}}\displaystyle\frac{{\tiny\textsc{({at-
tail})}}\displaystyle\frac{{\tiny\textsc{({at-
cons-n})}}\displaystyle\frac{{\tiny\textsc{({at-
tail})}}\displaystyle\frac{{\tiny\textsc{({at-
var})}}\displaystyle\frac{\begin{array}[]{c}{\tiny\textsc{({at-
cons-0})}}\displaystyle\frac{}{\mathit{at}_{\rho}({1}\mathbin{\texttt{:}}{{({2}\mathbin{\texttt{:}}{{\textit{x}}{\char
94\relax}})}{\char 94\relax}},0)=1}\ \begin{array}[]{l}\end{array}\\\
\vdots\end{array}}{\mathit{at}_{\rho}(\textit{x},i-1)={1}}\
\begin{array}[]{l}\end{array}}{\mathit{at}_{\rho}({\textit{x}}{\char
94\relax},i-2)={1}}\
\begin{array}[]{l}\end{array}}{\mathit{at}_{\rho}(2:{\textit{x}}{\char
94\relax},i-1)={1}}\
\begin{array}[]{l}\end{array}}{\mathit{at}_{\rho}({(2:{\textit{x}}{\char
94\relax})}{\char 94\relax},i-2)={1}}\
\begin{array}[]{l}\end{array}}{\mathit{at}_{\rho}(1:{(2:{\textit{x}}{\char
94\relax})}{\char 94\relax},i-1)={1}}\
\begin{array}[]{l}\end{array}}{\mathit{at}_{\rho}(0:1:{(2:{\textit{x}}{\char
94\relax})}{\char 94\relax},i)={1}}\
\begin{array}[]{l}\end{array}}{\mathit{at}_{\rho}(\textit{x},i)={1}}\
\begin{array}[]{l}\end{array}\end{array}$

Figure 8: Reduction of $\mathsf{wd}(\textit{x},\rho,\emptyset)$ and
$\mathit{at}_{\rho}(\textit{x},i)={1}$ with $\rho=\\{\textit{x}\mapsto
0:1:{(2:{\textit{x}}{\char 94\relax})}{\char 94\relax}\\}$ and $i>1$.