# On Bounding Space Usage of Streams Using Interpretation Analysis

Marco Gaboardi, Romain Péchoux

<figure><img src="image_1.png" /></figure>

## To cite this version:

Marco Gaboardi, Romain Péchoux. On Bounding Space Usage of Streams Using Interpretation Analysis. Science of Computer Programming, 2015, pp.44. hal-01112161

HAL Id: hal-01112161

https://inria.hal.science/hal-01112161

Submitted on 2 Apr 2015

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On Bounding Space Usage of Streams Using Interpretation Analysis

Marco Gaboardi<fnref n="1" />,<fnref n="2" />

Harvard University and University of Dundee

Romain Péchoux<fnref n="1" />

Université de Lorraine - INRIA project Carte, Loria, UMR 7503

## Abstract

Interpretation methods are important tools in implicit computational complexity. They have been proved particularly useful to statically analyze and to limit the complexity of programs. However, most of these studies have been so far applied in the context of term rewriting systems over finite data.

In this paper, we show how interpretations can also be used to study properties of lazy first-order functional programs over streams. In particular, we provide some interpretation criteria useful to ensure two kinds of stream properties: *space upper bounds* and *input/output upper bounds*. Our space upper bounds criteria ensures global and local upper bounds on the size of each output stream element expressed in terms of the maximal size of the input stream elements. The input/output upper bounds criteria consider instead the relations between the number of elements read from the input stream and the number of elements produced on the output stream.

This contribution can be seen as a first step in the development of a methodology aiming at using interpretation properties to ensure space safety properties of programs working on streams.

**Keywords:** Stream Programs, Interpretations, Program Space Usage, Lazy Languages, Implicit Computational Complexity.

Email addresses: m.gaboardi@dundee.ac.uk (Marco Gaboardi), pechoux@loria.fr (Romain Péchoux)

URL: http://www.cs.unibo.it/~gaboardi (Marco Gaboardi), http://www.loria.fr/~pechoux (Romain Péchoux)

<footnote n="1">¹Work partially supported by the projects ANR-14-CE25-0005 "ELICA", MIUR-PRIN'07 "CON-CERTO" and INRIA Associated Team "CRISTAL".</footnote>

<footnote n="2">²The research leading to these results has received funding from the European Community's Seventh Framework Programme (FP7/2007-2013) under grant agreement n° 272487.</footnote>
# 1. Introduction

The advances obtained in communication technology in the last two decades have posed new challenges to the software community. One of these challenges comes from the advancements achieved in computer networking where new software able to handle huge amount of data in an efficient way is required.

This situation has brought a renewed interest for stream-like data structures and for programs managing those data structures. Indeed, by representing discrete potentially infinite information flows, streams can be used to formalize and study situations as real-time data processing, network communication flows, audio and video signals flows, etc. Clearly, the problems that stream programs raise are different from the ones generally considered in the usual scenario where data are assumed to be finite. For this reason, several programming languages have been proposed with the aim of modeling stream-based computations, see [39] for a survey.

The aim of the present work is to contribute to the current scenario by developing some static analysis techniques useful to ensure basic properties of lazy functional programs working on streams. This is the first step of a more general investigation of complexity and efficiency properties of programs working on streams.

**Stream-like languages and properties.** Several formal frameworks have been designed for the manipulation of infinite objects including infinitary rewriting [23] and infinitary lambda-calculus [24]. Important properties of these models such as infinitary weak normalization and infinitary strong normalization have been deeply studied in the literature. However, little attention has been paid to space properties of such models. A different setting handling infinite data-structures is computable analysis, which provides several models of computation over real numbers [40]. In this setting a lot of work has been done to adapt the classical concept of complexity class and obtain implicit characterizations. However, even if streams can be considered as particular real numbers, the properties of interest for stream programs are usually different from the ones of interest in computable analysis.

A well-established approach to deal with infinite data, and in particular with streams, is by using *laziness* in functional programming languages [21]. In languages like Haskell, streams are expressions denoting infinite lists whose elements are evaluated on demand. In this way streams can be treated by finitary means. The practical diffusion of lazy programming languages has stimulated the development of tools and techniques in order to prove properties of programs in the presence of infinite data structures.

For example, on the side of program equivalence much attention has been paid to the study of co-induction and bisimulation techniques in languages working on streams [35, 20]. A property of stream definitions that has motivated many studies is productivity [14]. A stream definition is productive if it can be effectively evaluated in a unique constructor infinite normal form. Productivity is in general undecidable, so, many restricted languages and restricted criteria have been studied to ensure it [38, 12, 22, 15].

Besides program equivalence and productivity, other stream program properties, in particular space-related properties, have received little attention. Such properties are studied in this paper through the use of interpretations, a static analysis tool.
**Interpretations.** Interpretation methods originate from the natural observation that, in order to reason about program properties, it is sometimes more convenient to interpret syntactic program constructions into the objects of an abstract domain and prove properties about the obtained abstract objects.

Interpretation methods have been proved useful in many situations and are nowadays well-established verification tools for proving properties of programs. Variants of interpretation have been used for example to prove the termination of term rewriting systems [31, 26], to obtain sound approximations of program behaviors useful to static analysis [13] and to obtain implicit characterizations of complexity classes [7, 32].

One variation of particular interest for implicit computational complexity is the notion of quasi-interpretation [7]. A quasi-interpretation maps program constructions to functions over real numbers. The mapping is chosen in such a way that the function obtained as the interpretation of a program describes an upper bound on the size of the computed values with respect to the size of input values. Thanks to this, quasi-interpretations are particularly adapted to study program complexity in an elegant way.

Another important property of quasi-interpretation is that the problem of finding a quasi-interpretation of a given program for some restricted class of polynomials is decidable [2, 9]. This suggests that quasi-interpretations can be used as a concrete tool to analyze the complexity of functional programs.

An important new issue is whether interpretations can be used in order to infer such properties on programs computing over infinite data. Here we approach this problem by considering lazy programs over stream data.

**Contribution.** In this paper, we consider a simple first-order lazy language and we start a systematic study of *space properties* of programs working on streams by means of interpretation methods.

In many stream applications one is interested in processing data in a fast and memory-safe way. In order to do this, one can think to improve space-efficiency by using some buffering operations to memorize only the part of the stream involved in the actual computation. Following this intuition, it becomes natural to study space properties of programs working on streams in a more abstract way. We study two classes of space properties:

* *Stream Upper Bounds:* these are properties about the size of each stream element produced by a program. They correspond to properties about the elements memorized in the buffer.

* *Bounded Input/Output Properties:* these are properties about the number of stream elements produced by a program. They correspond to properties about the number of elements produced on the output wrt to the number of elements read on the input.

These properties analyze two “dimensions” of programs working on streams. The combination of these properties allows one to study a reasonable class of programs and to obtain the information needed in order to improve the memory management process of programs working on streams.
The results presented in this paper have been originally developed in [18] and [19]. In [19], we mainly studied the space upper bounds properties while in [18] we studied the bounded input/output properties. The present paper generalizes and extends these works, in particular, to a pure functional programming style. Indeed previous works were restricted to term rewrite systems and the adaptation of interpretation methods to pure functional programs is a new non-trivial feature. Consequently, new proofs but also more illustrating diagrams and examples have been provided. Finally, a deeper comparison with the state of the art on stream properties (productivity, complexity, ...) and related works has been provided in Section 7.

**Stream Upper Bounds.** In order to process stream data in a memory-efficient way it is useful to obtain an estimate of the memory needed to store the elements produced by a stream program.

In some situations, an estimate can be obtained by considering in a *global* way the greatest size of the elements produced by the program as outputs. In other situations, however, there is no such a maximal element with respect to the size measure and so only an estimate considering the *local* position of the element in the stream can be given. Consider the following stream definitions:

$$ 
\begin{align*}
\text{ones} &:: [\text{Nat}] & \text{nats} &:: \text{Nat} \rightarrow [\text{Nat}] \\
\text{ones} &\doteq \underline{1} \:: \text{ones} & \text{nats x} &\doteq x \:: (\text{nats}(x+1))
\end{align*}
$$

In both cases, it is easy to obtain such estimates. Indeed, in the stream definition of `ones` all the elements have the same size, while in the definition of `nats` every element has a size depending on its position in the stream.

However, when more complex stream programs are considered, deeper analyses are needed. In this paper, we will use interpretations to define two criteria useful to compute both kinds of space estimates.

Consider the following stream program:

$$ 
\begin{align*}
\text{repeat} &:: \text{Nat} \rightarrow [\text{Nat}] & \text{zip} &:: [a] \rightarrow [a] \rightarrow [a] \\
\text{repeat x} &\doteq x \:: (\text{repeat x}) & \text{zip} (x : xs) ys &\doteq x \:: (\text{zip ys xs})
\end{align*}
$$

It is easy to verify that the size of every element of a stream `s` built only using `repeat` and `zip` is bounded by a constant `n`, i.e. the maximal natural number encoding `n` in a subterm `repeat n` in `s`. In particular, it means that every stream `s` built only using `repeat` and `zip` is globally bounded by a constant `n`. In order to generalize this informal analysis, we study a *Global Upper Bound* (GUB) criterion ensuring that the size of stream elements is bounded by a function in the maximal size of the input elements.

Analogously, consider the following stream program:

$$ 
\begin{align*}
\text{nats} &:: \text{Nat} \rightarrow [\text{Nat}] & \text{sadd} &:: [\text{Nat}] \rightarrow [\text{Nat}] \rightarrow [\text{Nat}] \\
\text{nats x} &\doteq x \:: (\text{nats}(x+1)) & \text{sadd} (x : xs) (y : ys) &\doteq (\text{add x y}) \:: (\text{sadd xs ys})
\end{align*}
$$

Every stream `s` built using `nats` and `sadd` is not globally bounded. Nevertheless it is easy for every such an `s` to compute a function `f` such that every element of `s` in the *local* position `n` has a size bounded by `f(n)`. In order to generalize this informal argument, we study a *Local Upper Bound* (LUB) criterion ensuring that the size of the `n`-th eval-
uated element of a stream is bounded by a function in its index $n$ and the maximal size of the input. All the productive stream functions have a local upper bound, however in order to establish a criteria ensuring it we need an extension of the usual notion of interpretation. For this reason we introduce the notion of parametrized interpretation, i.e. an interpretation where functions depend on external parameters.

**Bounded Input/Output Properties.** Another information that is useful to obtain in order to improve memory-efficiency is an estimate of the number of elements produced by a stream program when fed with only a portion of the input stream. Indeed if one think to online streaming, these properties consist in bounding the speed-up that might occur in the network during communication.

In some situations, such an estimate can be obtained by considering only the *length* of the portion of the input stream. In other situations, however, this is not sufficient and so in order to obtain the estimate one needs to consider also the *size* of the elements in the portion. Consider the following definitions:

$$
\begin{align*}
\mathit{merge} &:: [a] \rightarrow [a] \rightarrow [a \times a] \\
\mathit{merge} (x : \mathit{xs}) (y : \mathit{ys}) &\doteq (x, y) : (\mathit{merge} \ \mathit{ys} \ \mathit{xs})
\end{align*}
$$

$$
\begin{align*}
\mathit{dup} &:: [a] \rightarrow [a] \\
\mathit{dup} (x : \mathit{xs}) &\doteq x : (x : (\mathit{dup} \ \mathit{xs}))
\end{align*}
$$

It is easy to verify that each stream expression built using only merge and dup will only generate a number of output elements that depends on the number of input read elements; e.g. the expression dup (merge (dup s) (dup s)) for each read element of the input stream s produces four elements of the type $a \times a$. In order to generalize this informal argument, we study a *Length-Based Upper Bound* (LBUB) criterion ensuring that the number *m* of output stream elements is bounded by a function in the number *n* of stream elements in input.

Many stream functions have a length-based upper bound. However, there are
stream functions that generate a number of output elements that does not depend only
on the number of input read elements. Consider the following definitions:

$$
\begin{align*}
\mathit{app} &:: [a] \rightarrow [a] \rightarrow [a] & \mathit{upto} &:: \mathit{Nat} \rightarrow [\mathit{Nat}] \\
\mathit{app} (x : \mathit{xs}) \mathit{ys} &\doteq x : (\mathit{app} \ \mathit{xs} \ \mathit{ys}) & \mathit{upto} &0 \doteq \mathit{nil} \\
\mathit{app} \ \mathit{nil} \ \mathit{ys} &\doteq \mathit{ys} & \mathit{upto} & (x + 1) \doteq (x + 1) : (\mathit{upto} \ \mathit{x})
\end{align*}
$$

$$
\begin{align*}
\mathit{extendupto} &:: [\mathit{Nat}] \rightarrow [\mathit{Nat}] \\
\mathit{extendupto} (x : \mathit{xs}) &\doteq \mathit{app} (\mathit{upto} x) (\mathit{extendupto} \mathit{xs})
\end{align*}
$$

It is easy to verify that every stream expression built using only upto and extendupto
will generate a number of output elements that is related to both the number and the
size of input read elements; e.g. the expression: extendupto (extendupto s) for
each natural number n in the input stream s outputs Σ|n| i elements. In order to gen-
eralize this informal argument, we study a Size-Based Upper Bound (SBUB) criterion
ensuring that the number m of output stream elements is bounded by a function in the
number and the size of the stream elements in input.
**Other Technical Contributions.** Besides the study of stream program properties, this
paper contains two other technical contributions:

* a definition of interpretations for a lazy first-order programming language

* a definition of a new kind of interpretations, named parametrized interpretations

Interpretations have been so far presented as tools dealing with properties about
rewriting systems. Here instead, we are interested in programs of a first-order lazy
functional program. A possible approach could have been to translate programs in a
term rewriting system and analyze them using the standard interpretation framework.
Instead, we have adapted the interpretation tools to our case. This choice is due on
the one hand to the desire to have a treatment as close as possible to the programming
language, on the other hand this is also due to the desire of understanding the flexibility
and the adaptability of the interpretation tools.

Parametrized interpretations extend standard interpretations by means of an exter-
nal parameter. In the parametrized interpretations, all the functions appearing in the
assignments can depend on external parameters. However, the parameter has a differ-
ent status with respect to the other arguments of the functions. Thanks to this extension,
we are able to deal with properties about stream local positions as required by the Local
Upper Bound property.

**Outline of the paper.** In Section 2, we introduce the language, named SFL, and some notations. In Section 3, we introduce interpretations and parametrized interpretations. In Section 4, we study the space upper bound properties and the semantic interpretation criteria to ensure them. In Section 5, we consider the bounded input/output upper bound properties and how to ensure them through interpretation criteria. In Section 6, we discuss the problem of computing program interpretations. In Section 7, we present the related works. In Section 8, we draw some conclusions.

## 2. The SFL language

In the present section, we introduce the syntax and the operational semantics of the
language that will be used all along this paper. The language is dubbed SFL, acronym
for *Stream First-order Lazy language*. This is an Haskell-like lazy first-order language
computing on simple *stream* data.

We consider programs of SFL to be well-typed closed expressions of base type.
Programs can be evaluated thanks to a lazy big step semantics where by *lazy* we mean
that the evaluation does not go under a constructor. This permits to deal with streams
and infinite computations in a natural way. Indeed, analogously to what happens in
Haskell, we can prove program properties by equational reasoning. However, our op-
erational semantics differs from the Haskell one since we do not consider sharing.

### 2.1. *Syntax and Types*

Let $\mathcal{X}, \mathcal{C}$ and $\mathcal{F}$ be three disjoint sets representing the set of *variables*, the set of *constructor symbols* (or constructors) and the set of *function symbols* respectively. In the sequel, $x, c, f$ and $t$ denote symbols in $\mathcal{X}, \mathcal{C}, \mathcal{F}$ and $\mathcal{C} \cup \mathcal{F}$, respectively.
**Definition 1.** *The syntax of the SFL language is described by the following grammar:*

<table><tr><td>p</td><td>::=</td><td>x</td><td>|</td><td>c(x, ..., x)</td><td>(Patterns)</td></tr><tr><td>e</td><td>::=</td><td>x</td><td>|</td><td>c(e, ..., e)</td><td>|</td><td>f(e, ..., e)</td><td>|</td><td>LetRec d in e</td><td>(Expressions)</td></tr><tr><td colspan="8">Case e of p → e, ..., p → e</td></tr><tr><td>d</td><td>::=</td><td>f(x, ..., x)</td><td>:=</td><td>e</td><td>(Definitions)</td></tr><tr><td>v</td><td>::=</td><td>c(e, ..., e)</td><td></td><td></td><td>(Lazy Values)</td></tr><tr><td>v</td><td>::=</td><td>c(v, ..., v)</td><td></td><td></td><td>(Strict Values)</td></tr></table>

In the examples presented in the sequel, the set of constructor symbols will include the usual constructors for natural numbers (i.e. 0, + 1), lists (i.e. `nil`, `:`) and pairs (i.e. `(`, `)`). It may also include other standard algebraic data types. Besides, we assume the set of constructors to contain also a constructor `Err` that will be used to track pattern matching failures.

We consider *patterns* that are either a variable or a constructor possibly applied to other variables. For simplicity, we assume that a variable can appear at most once in a pattern and that the patterns are non-overlapping.

*Expressions* can be built using variables, constructors, function symbols, the `LetRec` construction and the `Case` construction. We consider a grammar where constructors and functions symbols do not appear partially applied in an expression, e.g a function symbol `f` of arity two will only appear in the form `f(e₁, e₂)`, for some expressions `e₁` and `e₂`.

The `Case` constructor as usual allows one to perform pattern matching. Note that even if the patterns are built by using (at most) one constructor at a time, by using nested `Case` more complex patterns can be explored. The `LetRec` construction is used to locally define recursive functions. In particular, a construction like `LetRec d in e` has two parameters: a *function definition* `d_f` and an expression `e`. The function definition `d_f` is the actual place where a recursive definition is assigned to the function symbol `f`. The expression `e` is the scope of that definition.

We distinguish two kinds of *values*: *lazy* and *strict values*. The semantics in the next subsection evaluates programs to lazy values. Strict values are specific lazy values that will be used to define the program analyses presented in the following sections. In particular, later in this section, we will show how to define an `eval` program forcing the evaluation of a program to a strict value.

*Free* and *bound* variables are defined as usual. However, free variables in expressions can be also explicitly bound in *definitions*, that is: given a definition `d` of the shape `f(x₁, ..., xₙ) := e`, the bound variables of `d` are the ones of `e` and `x₁, ..., xₙ`. Note also that a `LetRec` construction can bind function symbols. That is, the function symbol `f` is bound in `e'` in an expression of the shape `LetRec f(x₁, ..., xₙ) := e in e'`. For simplicity, we assume that all the bound variables and function symbols have distinct names so that name clashes are avoided.

As outlined above, we are mainly concerned with stream programs properties related to space. So, we need to introduce a notion of *size* for expressions and programs.

**Definition 2 (Size).** *The size of an expression *e*, denoted $|e|$, is defined as*

$$ \bullet |x| = 1 $$
$$ \bullet |t(e_1, \dots, e_n)| = \begin{cases} 0 & \text{if } t \text{ is of arity } 0 \\ \sum_{1 \le i \le n} |e_i| + 1 & \text{if } t \text{ is of arity } n \ge 1 \end{cases} $$

$$ \bullet |\text{LetRec d in } e| = |e| $$

$$ \bullet |\text{Case e of } p_1 \to e_1, \dots, p_n \to e_n| = |e| + \max_{1 \le i \le n} |e_i| $$

Note that if we take $\mathbb{N}$ to be the set of natural number expressions inductively defined using the constructors 0 and + 1 then for each $\underline{n} \in \mathbb{N}$ we have $|\underline{n}| = n$, i.e. the size of a natural number expression is equal to the value it represents.

In the sequel only expressions that are well-formed and well-typed will be considered.

**Definition 3.**

* A definition $f(x_1, \dots, x_n) \doteq e$ is well-formed if and only if all the free variables of $e$ are among $x_1 \cdots x_n$, i.e. the definition has no free variables.

* An expression $e$ is well-formed if and only if for every function symbol $f$ there is exactly one well-formed function definition $d$ defining it, i.e. of the shape $f(x_1, \dots, x_n) \doteq e'$.

We conclude this part by describing some of the notations we will use in the sequel. In presenting the examples we adopt the standard applicative convention for the parenthesis (as in Haskell), e.g. we use $f(x+1)$ 0 to denote $f(x+1, 0)$. We use the vector notation $\vec{e}$ as a shorthand for a sequence of expressions as $e_1, \dots, e_n$. So, for instance the expression $t(e_1, \dots, e_n)$ could be also written as $t \vec{e}$. Finally, given a sequence of expressions $\vec{e}$ and a function $F$ on expressions, we use $F(\vec{e})$ to denote $F(e_1), \dots, F(e_n)$, i.e. the componentwise application of $F$ to the sequence $\vec{e}$. For instance, given a sequence $\vec{e} = e_1, \dots, e_n$, we use $|\vec{e}|$ as a notation for $|e_1|, \dots, |e_n|$.

**Type system.** As stressed before, we want to consider only expressions that are well-typed. Here we introduce the type system that assigns types to all the syntactic constructions of the SFL language. As usual, the type system ensures that a program does not go wrong. Roughly speaking, a *wrong computation* happens when a program cannot be evaluated to a value because of some stuck computation. Note however that this does not prevent a program from either diverging or evaluating to Err. Indeed, in our setting, this fact is important both for making the pattern matching working properly and also for using some program analysis techniques presented in the following sections.

In order to make simpler our analyses, we only consider well-typed first-order programs dealing with lists that do not contain other lists. This is because we want to prevent object like streams of streams that cannot be analyzed in a proper way by the methods that we will present in the sequel. We assure this property by a typing restriction similar to the one of [17]. The following type definition reflects this and the fact that we restrict our attention only to first-order programs.

**Definition 4.** The SFL types are defined by the following grammar:
<figure><img src="image_3.png" /><figcaption>Table 1: SFL type system</figcaption></figure>

<figure><img src="image_4.png" /></figure>

where *a* is a basic type variable, *α* is a type variable, *Nat* is a constant type representing natural numbers, × and [] are base type constructors for pairs and (finite and infinite lists) streams respectively.

As stressed above, it is worth noticing that the above definition can be extended to other algebraic data types. In the sequel, we use *a*, *b* to denote basic type variables, *α*, *β* to denote type variables, *σ*, *τ* for basic data types, *A*, *B* to denote base types and *φ* for types. We will tacitly use restricted polymorphism, i.e. a basic type variable *a* and a type variable *α* will represent every basic and base type respectively.

For notational convenience, we will use the vector notation $\vec{A} \to B$ as an abbreviation for $A_1 \to \dots \to A_n \to B$.

The type system proves two kinds of typing judgments: $\Gamma; \Delta \vdash e :: A$ for expressions, and $\Gamma; \Delta \vdash f(x_1, \dots, x_n) = e :: \phi$ for function definitions. In particular, the judgments for expressions assign a *base type* to an expression, while the judgments for function definitions assign a *type* to a function definition. The symbols $\Gamma$ and $\Delta$ denote variables and function symbols *contexts* respectively; that is, partial functions assigning types to variables and function symbols respectively. Note that we do not consider constants symbols in contexts but instead we assume that they come with a fixed type signature.

**Definition 5.** *Well-typed expressions and function definitions are defined using the type*
system in Table 1.

It is worth noticing that the symbol Err can be typed with each base type A. This is essential in order to get type preservation in the evaluation mechanism. Note also that the functional types can be assigned to constructor and function symbols, but only base types can be assigned to expressions. Consequently, our language only allows programs with first-order function definitions.

**Definition 6.** A SFL program is a well-formed expression e that is typable through a type judgment of the shape $\emptyset; \emptyset \vdash e :: A$ such that A does not contain free type variables.

While the above definition could seem a bit odd, it is easy to verify that this corresponds to the usual notion of programs considered as closed terms of observable types.

**Notations for the examples.** The language we introduced above makes the interpretation definitions we will provide in the following section more formal. In contrast, concrete examples can be cumbersome. So, in the remainder of the paper we will use some syntactic sugar to improve readability. Let us start to show that we can use general forms of pattern matching in our examples. Note that we have introduced patterns following the grammar:

$$p ::= x \mid c(x, \dots, x)$$

So, in particular we do not have patterns for nested constructors. However, more complex pattern matching can be easily simulated through the use of combined Case constructions. As an example consider a function f that we want to define by pattern matching on expressions of the shape $(x + 1) + 1$. This can be defined as follow:

$$f y_1 = \text{Case } y_1 \text{ of } y_2 + 1 \rightarrow \text{Case } y_2 \text{ of } x + 1 \rightarrow e$$

Instead of writing this in full form, we will simply write it as:

$$f ((x + 1) + 1) \doteq e$$

More generally, we will use the notation:

$$f p_1^1 \cdots p_n^1 \doteq e_1$$

⋮

$$f p_1^k \cdots p_n^k \doteq e_k$$

as syntactic sugar for a function definition of the shape:

$$f(x_1, \dots, x_n) \doteq \text{Case } x_1 \text{ of } p_1^1 \rightarrow \dots \text{Case } x_n \text{ of } p_n^1 \rightarrow e_1$$

⋮

$$p_1^k \rightarrow \dots \text{Case } x_n \text{ of } p_n^k \rightarrow e_k$$

More complex examples consisting of function definitions with several distinct function symbols will be treated analogously by juxtaposition of their syntactic sugars. We
then assume these definitions to be bound by a LetRec for some particular expression under consideration. That is, we will usually consider an expression e in isolation but this has to be considered as a program of the shape:

$$ \text{LetRec } d_1, \dots, d_n \text{ in e} $$

where $d_1, \dots, d_n$ are all the function definitions for the function symbols in e.

**Stream terminology.** The program analysis methods we will present in the following sections are specific to the study of stream program properties. This means that we will pay particular attention to programs working on the type [A], the type of both finite and infinite lists of type A.

We distinguish two classes of functions symbols useful to work with streams. Following the terminology of [15], we have:

**Definition 7.**

* A function symbol f is a stream function if $f :: [\sigma_1] \to \dots \to [\sigma_n] \to \vec{\tau} \to [\sigma]$, with $n > 0$. Conversely, a function symbol f is a stream constructor if $f :: \vec{\tau} \to [\sigma]$.

* A function definition $d_f$ such that $f(x_1, \dots, x_n) = e$ is a stream function definition if f is a stream function. Conversely, if f is a stream constructor we say that $d_f$ is a stream definition.

Intuitively, we call stream functions those functions that transform and combine input streams to produce an output stream. Analogously, we call stream constructors those functions that can be used to actually produce new output streams from scratch.

**Example 1.** Consider the following definitions:

<table><tr><td>odd</td><td>::</td><td>[a] &rarr; [a]</td><td>nats</td><td>::</td><td>Nat &rarr; [Nat]</td></tr><tr><td>odd</td><td>(x : y : xs)</td><td>:=</td><td>x : (odd xs)</td><td>nats</td><td>x :=</td><td>x : (nats (x + 1))</td></tr><tr><td>zip</td><td>::</td><td>[a] &rarr; [a] &rarr; [a]</td><td>nodd</td><td>::</td><td>[Nat]</td></tr><tr><td>zip</td><td>(x : xs) ys</td><td>:=</td><td>x : (zip ys xs)</td><td>nodd</td><td>:=</td><td>odd (nats (0 + 1))</td></tr></table>

We have that odd and zip are two stream functions of one and two arguments respectively, while both nats and nodd are stream constructors. Note that the fact of being a stream constructor does not impose limitations on the kind of functions that can be used in the right-hand side of the definition. Indeed, in the nodd example, we use both a stream function (i.e odd) and a stream constructor (i.e. nats).

## 2.2. Lazy operational semantics

In this section, we describe the SFL operational semantics. As outlined above, the operational semantics can be described by means of a lazy big-step semantics. With the term lazy, in the tradition of [33, 1], we identify a semantics that does not evaluate
$$ \frac{c \in \mathcal{C} \qquad \mathcal{H} \cup \{d\}; M \Downarrow v \qquad \mathcal{H}; \text{LetRec d in } M \Downarrow v}{\mathcal{H}; c(e_1, \dots, e_n) \Downarrow c(e_1, \dots, e_n)} \quad \text{(val)} \quad \text{(rec)} $$

$$ \frac{\mathcal{H}; e\{e_1/x_1, \dots, e_n/x_n\} \Downarrow v \quad (f x_1 \cdots x_n \doteq e) \in \mathcal{H}}{\mathcal{H}; f(e_1, \dots, e_n) \Downarrow v} \quad \text{(fun)} $$

$$ \frac{\mathcal{H}; e \Downarrow c(e'_1, \dots, e'_m) \quad p_i = c(x_1, \dots, x_m) \quad \mathcal{H}; e_i\{e'_1/x_1, \dots, e'_m/x_m\} \Downarrow v}{\mathcal{H}; \text{Case e of } p_1 \to e_1, \dots, p_n \to e_n \Downarrow v} \quad \text{(pm)} $$

$$ \frac{\mathcal{H}; e \Downarrow c(e'_1, \dots, e'_m) \quad \forall i \le n, p_i \ne c(x_1, \dots, x_m)}{\mathcal{H}; \text{Case e of } p_1 \to e_1, \dots, p_n \to e_n \Downarrow \text{Err}} \quad \text{(pm_e)} $$

<caption>Table 2: SFL lazy operational semantics</caption>

under the constructors. So in particular, we do not consider the sharing issue that is studied in other lazy and call-by-need semantics [27, 3].

In order to describe the semantics, we need two additional components: *substitutions* and *environments*. A *substitution* {$e_1/x_1, \dots, e_n/x_n$} is a partial function mapping variables to expressions. As usual we denote $e\{e_1/x_1, \dots, e_n/x_n\}$ the result of the application of the substitution {$e_1/x_1, \dots, e_n/x_n$} to the free variables of $e$. An *environment* is simply a set of well-formed function definitions. We will use the letter $\mathcal{H}$ to denote environments.

**Definition 8.** The operational evaluation relation $\Downarrow$ is the relation between environments, expressions and lazy values inductively defined by the rules in Table 2.

Intuitively, the judgment $\mathcal{H}; e \Downarrow v$ means that the expression $e$ can be evaluated to the lazy value $v$ using the rules of the semantics and the function definitions contained in the environment $\mathcal{H}$. For notational convenience, we simply write $e \Downarrow v$ for $\mathcal{H}; e \Downarrow v$ when $\mathcal{H} = \emptyset$. Moreover, in the sequel when we write $\mathcal{H}; e \Downarrow v$ we implicitly assume that $\mathcal{H}$ contains the function definitions for all the function symbols in $e$.

It is worth noticing that as usual in lazy semantics the abstract machine does not explore the entire result but stops once the requested information is found; this is why the axiom rule (val) only refers to lazy values. Moreover, as anticipated in the previous subsection, we use the constructor Err to deal with pattern matching errors. This should not be confused with the errors that can be generated by programs that go wrong. Indeed, to prevent such situations types are sufficient, as usual.

**Strict evaluation.** We have introduced the operational semantics of our language SFL in the previous paragraph. We have defined it to be lazy since our main concern is to deal with infinite computations in a natural way. However, another concern of our work is to describe program analysis techniques using only finitary operational tools without making reference to infinite abstract domains. For this reason, sometimes we will need to consider the complete evaluation of values. This is why we have introduced the category of *strict values* in the grammar definition in Definition 1.
In order to evaluate programs to strict values, we can define a particular function eval<sub>A</sub> for every base type A as follows:

$$
\begin{align*}
\mathit{eval}_A \coloneqq A &\to A \\
\mathit{eval}_A \quad (c \ x_1 \ \cdots \ x_n) &\doteq \hat{C} \ (\mathit{eval}_{A_1} x_1) \ \cdots \ (\mathit{eval}_{A_n} x_n)
\end{align*}
$$

where $\hat{C}$ is a function symbol representing the *strict* version of the primitive constructor c. For instance in the case where c is + 1 we can define $\hat{C}$ to be the function $succ :: Nat \to Nat$ defined as:

$$
\begin{align*}
\mathit{succ} &\quad \mathit{Err} &\doteq \mathit{Err} + 1 \\
\mathit{succ} &\quad 0 &\doteq 0 + 1 \\
\mathit{succ} &\quad (x + 1) &\doteq (x + 1) + 1
\end{align*}
$$

When we want to stress that an expression *e* is completely evaluated (i.e. that besides
being an expression, it is also a strict value) we use the notation *e*. A relevant set of
completely evaluated expressions is the set *N* of *canonical numerals* defined as:

$$
N = \{ \underline{n} \mid \underline{n} = \underbrace{(\cdots (0+1)\cdots)}_{n \text{ times}} + 1 \} \text{ and } \underline{n} :: \text{Nat}
$$

A concrete example of computation by strict evaluation can be found in Appendix B.

**More notations.** For notational convenience, in the sequel we will use the notation:

$\mathcal{H}, e \Downarrow_v \underline{v}$

to denote the judgment:

$\mathcal{H}, \mathit{eval}_A e \Downarrow \underline{v}$

assuming that the type A is made clear by the context. Moreover, we introduce some
notation for some well-established functions that we will use in the following sections.

We use the notation $e_n$ as a shorthand for the expression $e !! n$ where $!!$ is the usual
indexing function returning the $n$-th element of a list. That is:

$$
\begin{align*}
!! &:: [a] \rightarrow \text{Nat} \rightarrow a \\
\text{nil} &\quad !! \quad y \quad \doteq \quad \text{Err} \\
(x : xs) &\quad !! \quad 0 \quad \doteq \quad x \\
(x : xs) &\quad !! \quad (y + 1) \quad \doteq \quad xs !! y
\end{align*}
$$

We use the shorthand $e|_n$ to denote the expression $\mathit{take} \, n \, e$ where $\mathit{take}$ is the usual function which returns the first $n$ elements of a list:

$$
\begin{align*}
\mathit{take} \ :: & \ \mathit{Nat} \to [a] \to [a] \\
\mathit{take} & \quad 0 \quad s \quad \doteq \quad \mathit{nil} \\
\mathit{take} & \quad (x+1) \quad \mathit{nil} \quad \doteq \quad \mathit{Err} \\
\mathit{take} & \quad (x+1) \quad (y:ys) \quad \doteq \quad y:(\mathit{take} \ x \ ys)
\end{align*}
$$

Finally, we use lg to denote the function that returns the number of elements in a finite
partial list:
<figure><img src="image_5.png" /></figure>

In the sequel, we tacitly assume that the above definitions are contained in all the environments $\mathcal{H}$ that we will consider.

### 3. Interpretation

The program analyses that we will introduce in Sections 4 and 5 will be based on the notion of *interpretation*. Intuitively, an interpretation consists of an assignment mapping each symbol of a program to a function over non-negative real numbers. Thanks to the real numbers ordering, such a peculiar assignment combined with some additional criteria permits to prove program properties.

This kind of reasoning is inspired by the notion of *polynomial interpretation* [31, 26, 6], developed in the field of program termination, and by the notions of *quasi-interpretation* [8] and *sup-interpretation* [32], developed more recently in the field of implicit computational complexity.

We now stress the main distinctions between the notion of interpretation presented in this section and the standard notion of interpretations on Term Rewrite Systems (see the survey [7]). In Subsections 3.1 and 3.2, we define the notions of *assignment* and *interpretation*. These definitions are similar to the one on TRS ([7]). The only distinction is that these notions are adapted to the presented functional language (the case construct is treated). The notions of *additive* and *monotonic assignments* are also standard. The only new notion is the notion of *almost-additive* (see Definition 3) allowing to deal with stream construct in a more flexible manner. All the results relating the size of a value and its interpretation (e.g. Corollary 1) or the interpretations of a term and its evaluation (e.g. Proposition 1) are fairly standard so an expert reader may go directly to Subsection 3.3 where a new notion of *parametrized interpretation* is defined. This notion will be useful for the *Local Upper Bound (LUB) criterion*.

#### 3.1. Assignment

In the following, an *assignment* is used as a method to map in a canonical way programs to non-negative real numbers (i.e. elements of $\mathbb{R}^+$) in such a way that a comparison of programs is possible thanks to the usual ordering on real numbers. In order to do this, an assignment maps program components either to non-negative real numbers or to functions over non-negative real numbers.

**Definition 9 (Assignment).**

* A variable assignment, denoted $\rho$ is a map associating to each $x \in \mathcal{X}$ a value $r$ in $\mathbb{R}^+$.

* A symbol assignment, denoted $\xi$ is a map associating to each symbol $t \in \mathcal{C} \cup \mathcal{F}$ a function $F: \mathbb{R}^+ \times \dots \times \mathbb{R}^+ \to \mathbb{R}^+$ of the same *arity*.
* Given a variable assignment $\rho$ and a symbol assignment $\xi$, an assignment is the extension of $\rho$ and $\xi$ to expressions defined as follows:

$$- (\mathit{Err})_{\rho, \xi} = 0$$

$$- (\mathbf{x})_{\rho, \xi} = \rho(x)$$

$$- (\mathbf{t}(\mathbf{e}_1, \dots, \mathbf{e}_n))_{\rho, \xi} = \xi(\mathbf{t})((\mathbf{e}_1)_{\rho, \xi}, \dots, (\mathbf{e}_n)_{\rho, \xi})$$

$$- (\mathit{LetRec} \ \mathit{in} \ \mathbf{e})_{\rho, \xi} = (\mathbf{e})_{\rho, \xi}$$

$$- (\mathit{Case} \ \mathit{of} \ c_1(\vec{x}_1) \to e_1, \dots, c_m(\vec{x}_m) \to e_m)_{\rho, \xi} \\ = \max_{1 \le i \le m} \{ (\mathbf{e}_i)_{\rho\{\vec{x}_i=\vec{r}_i\}, \xi} | \vec{r}_i \in \mathbb{R}^+ \text{ and } (\mathbf{e})_{\rho, \xi} \ge (\mathbf{c}_i(\vec{x}_i))_{\rho\{\vec{x}_i=\vec{r}_i\}, \xi} \}$$

We consider variable and symbol assignments as total functions over program variables and program symbols, respectively. We write $\vec{r} \in \mathbb{R}^+$ as a shorthand for $\forall r \in \vec{r}, r \in \mathbb{R}^+$, and we write $\rho\{\mathbf{x} := r\}$ for the variable assignment defined as $\rho$ except for the variable $\mathbf{x}$ to which it assigns the value $r$. We often abbreviate $\rho\{\mathbf{x}_1 := r_1\} \cdots \{\mathbf{x}_n := r_n\}$ by $\rho\{\vec{\mathbf{x}} = \vec{r}\}$ (as for instance in the definition above). Note that we consider the constructor Err differently from the other constructors. This because as we will see later we want that interpretations behave well with respect to pattern matching.

The definition of assignment for the Case construction requires the existence of a maximal element $((\mathbf{e}_i)_{\rho\{\vec{x}_i=\vec{r}_i\}, \xi})$ for $1 \le i \le m$ and for $\vec{r}$ ranging over values in $\mathbb{R}^+$. The existence of such an element (or equivalently a bound on the search space) is ensured by the side condition $((\mathbf{e})_{\rho, \xi}) \ge ((\mathbf{p}_i)_{\rho\{\vec{x}_i=\vec{r}_i\}, \xi})$ and by the fact that $e$ does not contain the variables $\vec{x}$.

**Example 2.** Consider the following function definitions:

$$\mathit{add} :: \mathit{Nat} \to \mathit{Nat} \to \mathit{Nat}$$

$$\mathit{add} \ 0 \ y \ \doteq \ y$$

$$\mathit{add} \ (z + 1) \ y \ \doteq \ (\mathit{add} \ z \ y) + 1$$

$$\mathit{sadd} :: [\mathit{Nat}] \to [\mathit{Nat}] \to [\mathit{Nat}]$$

$$\mathit{sadd} \ (x' : \mathit{xs}) \ (y' : \mathit{ys}) \ \doteq \ (\mathit{add} \ x' \ y') : (\mathit{sadd} \ \mathit{xs} \ \mathit{ys})$$

Concretely, in SFL they can be computed by the environment $\mathcal{H}$ including the following definitions:

$$\mathit{add} \ x \ y \ \doteq \ \mathit{Case} \ x \ \mathit{of} \ 0 \to y, \ z + 1 \to (\mathit{add} \ z \ y) + 1$$

$$\mathit{sadd} \ x \ y \ \doteq \ \mathit{Case} \ x \ \mathit{of} \ x' : \mathit{xs} \to \mathit{Case} \ y \ \mathit{of} \ y' : \mathit{ys} \to (\mathit{add} \ x' \ y') : (\mathit{sadd} \ \mathit{xs} \ \mathit{ys})$$

For each variable assignment $\rho = \{\mathbf{x} := r, \mathbf{y} := s\}$ and symbol assignment $\xi$ such that $\xi(0) = 0$, $\xi(\mathbf{x})(X, Y) = X + Y + 1$, $\xi(+1)(X) = X + 1$ and $\xi(\mathit{add})(X, Y) = \xi(\mathit{sadd})(X, Y) = X + Y$, we compute the assignment of the expression $\mathit{add} \ x \ y$ as follows:

$$((\mathit{add} \ x \ y))_{\rho, \xi} = \xi(\mathit{add})((\mathbf{x})_{\rho, \xi}, (\mathbf{y})_{\rho, \xi}) \\ = \rho(\mathbf{x}) + \rho(\mathbf{y}) \\ = r + s$$
We compute the assignment of Case x of 0 → y, z + 1 → (add z y) + 1 in a similar way:

$$
\begin{align*}
& (\text{Case x of } 0 \to y, z+1 \to (\text{add z y}) + 1)_{\rho, \xi} \\
&= \max(\max\{(\|y\|)_{\rho, \xi} \mid (\|x\|)_{\rho, \xi} \ge \|0\|_{\rho, \xi}\}, \\
& \qquad \max\{(\|\text{(add z y)}\| + 1)_{\rho\{z:=t\}, \xi} \mid t \in \mathbb{R}^+ \text{ and } (\|x\|)_{\rho, \xi} \ge \|z+1\|_{\rho\{z:=t\}, \xi}\}) \\
&= \max(\rho(y), \max\{\rho(y) + \rho\{z := t\}(z) + 1 \mid t \in \mathbb{R}^+ \text{ and } \rho(x) \ge \rho\{z := t\}(z) + 1\}) \\
&= \max(s, \max_{r \ge t+1}\{s + t + 1\}) \quad \text{as } \rho(x) = r \text{ and } \rho(y) = s \\
&= \max(s, s + r) = r + s
\end{align*}
$$

The usual notion of assignment used in the context of interpretations does not dis-
tinguish between variable and symbol assignments. In our context, we prefer to keep
this distinction because it highlights the extension of assignments to the Case con-
struction and because, as we will see later, an interpretation will fix only the symbol
assignments.

The following property shows that assignments internalize the substitution mechanism.

**Lemma 1 (Assignment Substitution).** *Given an assignment $\|\cdot\|_{\rho, \xi}$ and an expression $\Gamma, x :: A$; $\Delta \vdash e :: B$, for every expression $\Gamma'; \Delta \vdash e' :: A$ we have:*

$$
\langle \mathfrak{e} \{ \mathfrak{e}' / \mathfrak{x} \} \rangle_{\rho, \xi} = \langle \mathfrak{e} \rangle_{\rho} \{ x := \langle \mathfrak{e}' \rangle_{\rho, \xi}, \xi \}
$$

*Proof.* By induction on the structure of *e*. In the case where *e* is the variable *x* then the conclusion follows immediately. The cases where *e* is either *Err* or a variable distinct from *x* are trivial. The case where *e* is a *LetRec* follows directly by induction hypothesis.

Consider now the case e = t(e₁, ..., eₙ), by definition we have (|e{e'/x}|)ρ,ξ = ξ(t)(|e₁{e'/x}|)ρ,ξ, ..., (|eₙ{e'/x}|)ρ,ξ). By induction hypothesis, (|eᵢ{e'/x}|)ρ,ξ = (|eᵢ|)ρ{x:=|e'|)ρ,ξ} for each 1 ≤ i ≤ n. So, we can conclude:

$$
\begin{align*}
(|e\{e'/x\}|)_{\rho, \xi} &= \xi(t)(|e_1\{e'/x\}|)_{\rho, \xi}, \dots, (|e_n\{e'/x\}|)_{\rho, \xi} = \\
&\quad \xi(t)(|e_1|)_{\rho\{x:=|e'|)\}_{\rho, \xi}, \xi, \dots, (|e_n|)_{\rho\{x:=|e'|)\}_{\rho, \xi}, \xi} = (|e|)_{\rho\{x:=|e'|)\}_{\rho, \xi}, \xi}
\end{align*}
$$

Consider the case e = Case e'' of c₁(ŷ₁) → e₁, ..., cₙ(ŷₙ) → eₙ, then by defini-
tion, for x /∈ ŷ₁, ..., ŷₙ (because x is supposed to be free in e), we have:

$$
(|e\{e'/x\}|)_{\rho, \xi} = \max_{1 \le i \le m} \{ (|e_i\{e'/x\}|)_{\rho\{\vec{y}_i := \vec{r}_i\}, \xi} | (|e''\{e'/x\}|)_{\rho, \xi} \ge (|c_i(\vec{y}_i)|)_{\rho\{\vec{y}_i := \vec{r}_i\}, \xi} \}
$$

By induction hypothesis, we obtain:

$$
\{
  \langle \mathfrak{e}_i \{ \mathfrak{e}'/\mathfrak{x} \} \rangle_{\rho \{ \vec{y}_i := \vec{r}_i \}, \xi} | \langle \mathfrak{e}'' \{ \mathfrak{e}'/\mathfrak{x} \} \rangle_{\rho, \xi} \ge \langle \mathfrak{c}_i (\vec{y}_i) \{ \mathfrak{e}'/\mathfrak{x} \} \rangle_{\rho \{ \vec{y}_i := \vec{r}_i \}, \xi} \} = \\
  \{ \langle \mathfrak{e}_i \rangle_{\rho \{ \vec{y} := \vec{r}, x := \langle \mathfrak{e}' \rangle_{\rho, \xi} \}, \xi} | \langle \mathfrak{e}'' \rangle_{\rho \{ x := \langle \mathfrak{e}' \rangle_{\rho, \xi} \}, \xi} \ge \langle \mathfrak{c}_i (\vec{y}_i) \rangle_{\rho \{ \vec{y} := \vec{r}, x := \langle \mathfrak{e}' \rangle_{\rho, \xi} \}, \xi} \}
$$

and so we can conclude $\langle \mathfrak{e} \{ \mathfrak{e}' / \mathfrak{x} \} \rangle_{\rho, \xi} = \langle \mathfrak{e} \rangle_{\rho} \{ x := \langle \mathfrak{e}' \rangle_{\rho, \xi}, \xi \} \quad \square$
In this paper we will only deal with assignments that are *monotonic* where the monotonicity condition is defined as follows.

**Definition 10 (Monotonic Assignment).**

* A symbol assignment $\xi$ is monotonic if for any $t \in C \cup \mathcal{F}$, $\xi(t)$ is a monotonic function, i.e. $\forall r, s \in \mathbb{R}^+$ s.t. $r \ge s$:

$$ \xi(t)(..., r, ...) \ge \xi(t)(..., s, ...) $$

* An assignment $(-)_\rho$ is monotonic if the symbol assignment $\xi$ is monotonic.

Notice that the above definition of monotonicity concerns only the constants and the function symbols. This does not imply that all the functions used in an assignment are monotonic. In particular, the Case construction can be interpreted as a function $(\text{Case e of } p_1 \to e_1, \dots, p_m \to e_m)_\rho$ that is monotonic in $\|e\|_\rho$ and $(\|e_i\|_\rho)_\rho$ but not in $(\|p_i\|_\rho)_\rho$.

Other classes of assignments that will be useful in the sequel are the class of almost-additive and additive assignments.

**Definition 11 (Almost-additive and Additive Assignment).**

* The symbol assignment $\xi$ is almost-additive if $\forall c \in C$ of arity $n$ but the stream constructor $\cdot$, we have:

$$ \xi(c)(r_1, \dots, r_n) = \sum_{i=1}^{n} r_i + \alpha_c, \quad \text{for some constant } \alpha_c \ge 1, \quad \text{whenever } n > 0. $$

$$ \xi(c) = 0, \text{ otherwise.} $$

The symbol assignment $\xi$ is additive if it is almost-additive and

$$ \xi(\cdot)(r_1, r_2) = r_1 + r_2 + \alpha, \quad \text{for some constant } \alpha \ge 1 $$

* An assignment $(-)_\rho$ is an almost-additive (resp. additive) assignment if the symbol assignment $\xi$ is almost-additive (resp. additive).

The fact that an assignment is *additive* is useful in order to relate the interpretation of a strict value to its size. In particular, the following lemma shows that they are linearly related.

**Lemma 2.** Given an additive assignment $(-)_\rho$, there is a constant $\alpha$ such that for each strict value $\cdot \vdash \underline{\cdot}$ :: A we have:

$$ |\underline{\cdot}| \le |\cdot|_\rho \le \alpha \times |\cdot| $$

*Proof.* We consider $\alpha = \max_{c \in C} \alpha_c$ and we prove the lemma by induction on the structure of $\underline{\cdot}$.

In the case $\underline{\cdot}$ is a constructor c of arity 0, by definition we have $|c| = 0 = |\cdot|_\rho$, so the conclusion follows trivially.
Consider now the case $\underline{v} = c(\underline{v}_1, \dots, \underline{v}_n)$. By induction hypothesis for $1 \le i \le n$ we have:

$$|\underline{v}_i| \le (|\underline{v}_i|)_{\rho, \xi} \le \alpha \times |\underline{v}_i|$$

So, since by definition we also have:

$$|\underline{v}| = (\sum_{1 \le i \le n} |\underline{v}_i|) + 1 \quad \text{and} \quad (|\underline{v}|)_{\rho, \xi} = (\sum_{1 \le i \le n} (|\underline{v}_i|)_{\rho, \xi}) + \alpha_c$$

and since $\alpha \ge \alpha_c \ge 1$, using induction hypothesis we can conclude:

$$\sum_{1 \le i \le n} |\underline{v}_i| + 1 \le \sum_{1 \le i \le n} (|\underline{v}_i|)_{\rho, \xi} + \alpha_c \le \sum_{1 \le i \le n} (\alpha \times |\underline{v}_i|) + \alpha_c \le \alpha \times (\sum_{1 \le i \le n} |\underline{v}_i| + 1)$$

□

A similar result can be obtained for almost-additive assignments if we restrict the attention to values that are not streams.

**Corollary 1.** Given an assignment $(|\cdot|)_{\rho, \xi}$ such that the symbol assignment $\xi$ is almost-additive, there is a constant $\alpha$ such that for every strict value $\vdash \underline{v} :: \sigma$ we have:

$$|\underline{v}| \le (|\underline{v}|)_{\rho, \xi} \le \alpha \times |\underline{v}|$$

## 3.2. Interpretations

Now, we are ready to define the main tool that will be used in the next sections: interpretations.

**Definition 12 (Interpretation).** An expression $\Gamma; \Delta \vdash e :: A$ admits an interpretation $(|\cdot|)_{\xi}$ if for each variable assignment $\rho$, the assignment $(|\cdot|)_{\rho, \xi}$ is monotonic and such that for each function definition $f(x_1, \dots, x_n) \coloneqq e'$ the following holds:

$$(|f(x_1, \dots, x_n)|)_{\rho, \xi} \ge (|e'|)_{\rho, \xi}$$

The quantification on all variable assignments allows us to reason in general terms about values assigned to variables. For this reason, in the sequel we will usually write $X, Y, Z, \dots$ to denote variables ranging over real numbers; e.g. we will write $(|f|)_{\xi}(X_1, \dots, X_n)$ for $(|f(x_1, \dots, x_n)|)_{\xi}$. Analogously, we will write $(|e|)_{\xi} \ge (|e'|)_{\xi}$ as a shorthands for: $\forall \rho, (|e|)_{\rho, \xi} \ge (|e'|)_{\rho, \xi}$.

In the sequel, we will need the following substitution property for interpretations.

**Lemma 3 (Interpretation Substitution).** Let $\Gamma; \Delta \vdash e :: A$ and $\Gamma, x :: A; \Delta \vdash e_1, e_2 :: B$ be expressions admitting the interpretation $(|\cdot|)_{\xi}$ and such that $(|e_1|)_{\xi} \ge (|e_2|)_{\xi}$. Then:

$$(|e_1\{e/x\}|)_{\xi} \ge (|e_2\{e/x\}|)_{\xi}$$

*Proof.* By definition of interpretation we have $\forall \rho, (|e_1|)_{\rho, \xi} \ge (|e_2|)_{\rho, \xi}$. Thanks to the quantification over all the variable assignments we also have $\forall \rho, (|e_1|)_{\rho\{x:=(|e|)_{\rho, \xi}\}}, \xi} \ge (|e_2|)_{\rho\{x:=(|e|)_{\rho, \xi}\}}, \xi}$. So, by applying Lemma 1, we can conclude $\forall \rho, (|e_1\{e/x\}|)_{\rho, \xi} \ge (|e_2\{e/x\}|)_{\rho, \xi}$. □
The inequality conditions required by the definition of interpretation can be naturally inherited by the results of an evaluation. In order to show this we need to extend interpretations to environments.

**Definition 13.** An environment $\mathcal{H}$ admits the interpretation $\langle - \rangle_\xi$ if for every variable assignment $\rho$ and every function definition $f(x_1, \dots, x_n) = e$ in it, the following holds:

$$ \langle f(x_1, \dots, x_n) \rangle_{\rho, \xi} \geq \langle e \rangle_{\rho, \xi} $$

We can now show some examples.

**Example 3.** Consider again the environment $\mathcal{H}$ of Example 2. This environment admits an interpretation $\langle - \rangle_\xi$ if the assignment $\langle - \rangle_\xi$ satisfies the following inequalities:

$$ \langle \text{add } x \rangle_\xi \geq \langle \text{Case } x \text{ of } 0 \to y, z + 1 \to (\text{add } z y) + 1 \rangle_\xi $$

$$ \langle \text{sadd } x \rangle_\xi \geq \langle \text{Case } x \text{ of } x' : xs \to \text{Case } y \text{ of } y' : ys \to (\text{add } x' y') : (\text{sadd } xs ys) \rangle_\xi $$

Consider an additive assignment $\langle - \rangle_\xi$ such that $\langle 0 \rangle_{\rho, \xi} = 0$, $\langle : \rangle_{\rho, \xi}(X, Y) = X + Y + 1$ and $\langle +1 \rangle_{\rho, \xi}(X) = X + 1$. Now, we are interested in finding an interpretation for the symbols add and sadd such that $\rho = \{x := r, y := s\}$ satisfies the following inequalities:

$$ \langle \text{add} \rangle_{\rho, \xi}(r, s) \geq \max(\max\{s \mid r \geq 0\}, \max\{1 + \langle \text{add} \rangle_{\rho, \xi}(t, s) \mid t \in \mathbb{R}^+ \text{ and } r \geq t + 1\}) $$

$$ \langle \text{sadd} \rangle_{\rho, \xi}(r, s) \geq \max\{\langle \text{Case } y \text{ of } y' : ys \to (\text{add } x' y') : (\text{sadd } xs ys) \rangle_{\rho\{x' := v, xs := x\}}, \xi \mid x, v \in \mathbb{R}^+ \text{ and } r \geq v + x + 1\} $$

The above can be reformulated as follows:

$$ \langle \text{add} \rangle_{\rho, \xi}(r, s) \geq \max_{\{t \in \mathbb{R}^+ \mid r \geq t+1\}} (s, 1 + \langle \text{add} \rangle_{\rho, \xi}(t, s)) $$

$$ \begin{aligned} \langle \text{sadd} \rangle_{\rho, \xi}(r, s) &\geq \max\{\langle (\text{add } x' y') : (\text{sadd } xs ys) \rangle_{\rho\{x' := v, xs := x, y' := w, ys := y\}}, \xi \mid x, y, v, w \in \mathbb{R}^+ \text{ and } r \geq v + x + 1 \text{ and } s \geq w + y + 1 \} \\ &\geq \max\{\langle \text{add} \rangle_{\rho, \xi}(v, w) + \langle \text{sadd} \rangle_{\rho, \xi}(x, y) + 1 \mid x, y, v, w \in \mathbb{R}^+ \text{ and } r \geq v + x + 1 \text{ and } s \geq w + y + 1 \} \end{aligned} $$

So, for instance we can choose $\xi(\text{add})(X, Y) = \xi(\text{sadd})(X, Y) = X + Y$ (the first inequality is indeed proved to be an equality in Example 2). With this function symbol assignment $\xi$, since it is monotonic, we have that $\langle - \rangle_\xi$ is an interpretation.

**Example 4.** Consider the function symbol eval$_A$ for strict evaluation. The environment $\mathcal{H}$ that contains definitions of the shape:

$$ \text{eval}_A x \doteq \text{Case } x \text{ of } (c x_1 \cdots x_n) \to \hat{C} (\text{eval}_{A_1} x_1) \cdots (\text{eval}_{A_n} x_n) $$

will admit the interpretation $\langle - \rangle_\xi$ defined by $\xi(c)(X_1, \dots, X_n) = \xi(\hat{C})(X_1, \dots, X_n) = \sum_{i=1}^n X_i + \alpha_c$ and $\forall A$, $\xi(\text{eval}_A)(X) = X$.

Indeed, consider the assignment $\langle - \rangle_{\rho, \xi}$ for the environment $\rho$ such that $\rho(x) = r$. On
the one hand, we have $\langle \mathrm{eval}_A(x) \rangle_{\rho, \xi} = \xi(\mathrm{eval}_A)(\langle x \rangle_{\rho, \xi}) = \langle x \rangle_{\rho, \xi} = \rho(x) = r$. On the other hand, setting $\bar{x} = x_1, \dots, x_n$ and $\bar{r} = r_1, \dots, r_n$:

$$ 
\begin{align*}
& \langle \mathrm{Case} \ x \ \mathrm{of} \ c \ x_1 \ \cdots \ x_n \to \hat{C} \ (\mathrm{eval}_{A_1} \ x_1) \ \cdots \ (\mathrm{eval}_{A_n} \ x_n) \rangle_{\rho, \xi} \\
&= \max\{ \langle \hat{C}(\mathrm{eval}_{A_1} \ x_1) \cdots (\mathrm{eval}_{A_n} \ x_n) \rangle_{\rho\{\bar{x}=\bar{r}\}, \xi} \mid \langle x \rangle_{\rho, \xi} \ge \langle c \ x_1 \ \cdots \ x_n \rangle_{\rho\{\bar{x}=\bar{r}\}, \xi} \} \\
&= \max\{ \xi(\hat{C}) (\langle \mathrm{eval}_{A_1} \ x_1 \rangle_{\rho\{\bar{x}=\bar{r}\}, \xi}, \dots, \langle \mathrm{eval}_{A_n} \ x_n \rangle_{\rho\{\bar{x}=\bar{r}\}, \xi}) \\
&\qquad \mid r \ge \xi(c) (\langle x_1 \rangle_{\rho\{\bar{x}=\bar{r}\}, \xi}, \dots, \langle x_n \rangle_{\rho\{\bar{x}=\bar{r}\}, \xi}) \} \\
&= \max\{ \sum_{i=1}^n r_i + \alpha_{\hat{c}} \mid r \ge \sum_{i=1}^n r_i + \alpha_{\hat{c}} \} \le r
\end{align*}
$$

This inequality holds for an arbitrary value $r$ and, consequently, for every environment $\rho$. So, $\langle - \rangle_{\xi}$ is an interpretation of $\mathcal{H}$.

Throughout the paper, we will fix the assignment of the eval_A function symbol by setting $\forall A, \xi(\mathrm{eval}_A)(X) = X$. As illustrated by the above example, such an assignment is a reasonable choice.

Now we can show that the result of an evaluation inherits the property of the interpretation: the interpretation of an expression is an upper bound on the interpretation of its computed value.

**Proposition 1.** Let $\mathcal{H}$ and $\emptyset$; $\Delta \vdash e :: A$ be an environment and an expression admitting both the interpretation $\langle - \rangle_{\xi}$. Then:

$$ \mathcal{H}, e \Downarrow v \text{ implies } \langle e \rangle_{\xi} \ge \langle v \rangle_{\xi} $$

*Proof.* By induction on the derivation proving $\mathcal{H}, e \Downarrow v$. The base case where the derivation consists only in an application of the rule (val) is trivial. The case the derivation ends with an application of the rule (rec) follows directly by induction hypothesis.

Let us consider the case where the derivation ends with:

$$ \frac{\mathcal{H}; e\{e_1/x_1, \dots, e_n/x_n\} \Downarrow v \quad (f x_1 \cdots x_n = e) \in \mathcal{H}}{\mathcal{H}; f(e_1, \dots, e_n) \Downarrow v} $$

By induction hypothesis, we have $\langle e\{e_1/x_1, \dots, e_n/x_n\} \rangle_{\xi} \ge \langle v \rangle_{\xi}$ and by assumption we have $\langle f(x_1, \dots, x_n) \rangle_{\xi} \ge \langle e \rangle_{\xi}$. So, by several applications of Lemma 3 we obtain $\langle f(e_1, \dots, e_n) \rangle_{\xi} \ge \langle e\{e_1/x_1, \dots, e_n/x_n\} \rangle_{\xi}$ and by transitivity the conclusion follows.

Let us consider the case where the derivation ends with:

$$ \frac{\mathcal{H}; e \Downarrow c(e'_1, \dots, e'_m) \quad p_i = c(x_1, \dots, x_m) \quad \mathcal{H}; e_i\{e'_1/x_1, \dots, e'_m/x_m\} \Downarrow v}{\mathcal{H}; \text{Case e of } p_1 \to e_1, \dots, p_n \to e_n \Downarrow v} $$

By induction hypothesis, we have both $\langle e_i\{e'_1/x_1, \dots, e'_m/x_m\} \rangle_{\xi} \ge \langle v \rangle_{\xi}$ and $\langle e \rangle_{\xi} \ge \langle c(e'_1, \dots, e'_m) \rangle_{\xi}$. Consider an arbitrary variable assignment $\rho$. Applying Lemma 1 several times, we have $\langle c(e'_1, \dots, e'_m) \rangle_{\rho, \xi} = \langle c(x_1, \dots, x_m) \rangle_{\rho', \xi}$ for $\rho' = \rho\{x_1 := \langle e'_1 \rangle_{\rho, \xi}, \dots, x_m := \langle e'_m \rangle_{\rho, \xi}\}$. By definition of assignment we have:

$$ \langle \mathrm{Case} \ e \ \mathrm{of} \ p_1 \to e_1, \dots, p_n \to e_n \rangle_{\rho, \xi} \ge \langle e_i \rangle_{\rho', \xi} $$
and by some applications of Lemma 1:

$$ (\text{\textbf{Case e of } } p_1 \to e_1, \dots, p_n \to e_n)_{\rho, \xi} \ge (\|e_i\|)_{\rho', \xi} = (\|e_i\{e'_1/x_1, \dots, e'_m/x_m\}\|)_{\rho, \xi} $$

Since this holds for every $\rho$, the conclusion easily follows by the definition of interpretation. $\square$

The previous result can be easily extended to strict evaluation: the interpretation of an expression is an upper bound on the interpretation of its computed strict value.

**Corollary 2.** Let $\mathcal{H}$ and $\emptyset$; $\Delta \vdash e :: A$ be an environment and an expression admitting both the interpretation $\|\cdot\|_{\xi}$. Then:

$$ \mathcal{H}, e \Downarrow_v \bar{v} \text{ implies } (\|e\|)_{\xi} \ge (\|\bar{v}\|)_{\xi} $$

*Proof.* The notation $\mathcal{H}, e \Downarrow_v \bar{v}$ is just a shorthand for $\mathcal{H}, \text{eval}_A e \Downarrow \bar{v}$, so the conclusion follows directly using Proposition 1 and the fact that we consider assignments such that $\xi(\text{eval}_A)(X) = X$. $\square$

The last important property of interpretations that will be used in the sequel relates the size of an expression with its interpretation.

**Lemma 4.** Let $\|\cdot\|_{\xi}$ be an interpretation. Then, there exists a function $F: \mathbb{R}^{+} \to \mathbb{R}^{+}$ such that for every program $e :: A$ admitting $\|\cdot\|_{\xi}$:

$$ (\|e\|)_{\xi} \le F(|e|) $$

*Proof.* By induction on the shape of $e$. $\square$

The proof of Lemma 4 proceeds in essentially the same way as the one of the subsequent Lemma 6. So, for convenience we detail only the proof of the latter.

### 3.3. Parametrized Interpretations

For the analyses that we will present in the next section it is convenient to extend the notion of interpretations in a parametric way. This notion allows us to obtain more precise analyses on stream programs.

The idea behind a parametrized interpretation is that the interpretations now become of the shape $\|\cdot\|_{\xi}^l$ where $l \in \mathbb{R}$ is a parameter that can be used to refer to a particular element of a stream. In order to obtain this, we need to parametrize all the previous definitions.

**Definition 14 (Parametrized Assignment).**

* A parametrized symbol assignment, denoted $\xi^l$ is a map associating to each symbol $t \in C \cup \mathcal{F}$ and $l \in \mathbb{R}$ a function $F_l: \mathbb{R}^+ \times \dots \times \mathbb{R}^+ \to \mathbb{R}^+$ of the same arity.

* Given a variable assignment $\rho$, a parametrized symbol assignment $\xi^l$, a parametrized assignment $\|\cdot\|_{\xi}^l$ is the extension of $\rho$ and $\xi^l$ to expressions defined as follows:
$$- (\|Err\|)_{\rho, \xi}^l = 0$$

$$- (\|x\|)_{\rho, \xi}^l = \rho(x)$$

$$- (\|e_1 : e_2\|)_{\rho, \xi}^l = \xi^l(\|\|e_1\|\|)_{\rho, \xi}, (\|e_2\|)_{\rho, \xi}^{l-1}$$

$$- (\|t(e_1, \dots, e_n)\|)_{\rho, \xi}^l = \xi^l(t) (\|e_1\|)_{\rho, \xi}^l, \dots, (\|e_n\|)_{\rho, \xi}^l \quad \text{for } t \neq :$$

$$- (\|\text{LetRec d in e}\|)_{\rho, \xi}^l = (\|e\|)_{\rho, \xi}^l$$

$$- (\|\text{Case e of } c_1(\vec{x}_1) \to e_1, \dots, c_m(\vec{x}_m) \to e_m\|)_{\rho, \xi}^l \\ = \max_{1 \le i \le m} \{ (\|e_i\|)_{\rho\{\vec{x}_i=\vec{r}_i\}, \xi}^l \mid \vec{r}_i \in \mathbb{R}^+ \text{ and } (\|e\|)_{\rho, \xi}^l \ge (\|c_i(\vec{x}_i)\|)_{\rho\{\vec{x}_i=\vec{r}_i\}, \xi}^l \}$$

The definitions given for interpretations can be easily adapted to the case of parametrized interpretations.

**Definition 15 (Monotonic Parametrized Assignment).** A parametrized assignment is monotonic if for any $t \in C \cup \mathcal{F}$, $\xi(t)$ is a monotonic function, i.e. $\forall r, s \in \mathbb{R}^+$ s.t. $r \ge s$ and $\forall l, l' \in \mathbb{R}$ s.t. $l \ge l'$:

$$\xi^l(t)(\dots, r, \dots) \ge \xi^{l'}(t)(\dots, s, \dots)$$

**Definition 16 (Almost-additive and Additive Parametrized Assignment).**

* The parametrized symbol assignment $\xi^l$ is almost-additive if $\forall c \in C$ of arity $n$ but the stream constructor : we have:

$$\xi^l(c)(r_1, \dots, r_n) = \sum_{i=1}^{n} r_i + \alpha_c, \text{ for some constant } \alpha_c \ge 1, \text{ whenever } n > 0.$$

$$\xi^l(c) = 0, \text{ otherwise.}$$

The parametrized symbol assignment $\xi^l$ is additive if it is almost-additive and

$$\xi^l(\|\cdot\|)(r_1, r_2) = r_1 + r_2 + \alpha, \text{ for some constant } \alpha \ge 1$$

* A parametrized assignment $(\|\cdot\|)_{\rho, \xi}^l$ is an almost-additive (resp. additive) assignment if the parametrized symbol assignment $\xi^l$ is almost-additive (resp. additive).

Differently from what happens in the case of assignments, parametrized assignments do not internalize the substitution mechanism. However, for monotonic parametrized assignment we have the following important property.

**Lemma 5 (Parametrized Assignment Substitution).** Given a monotonic parametrized assignment $(\|\cdot\|)_{\rho, \xi}^l$ and an expression $\Gamma, x :: A; \Delta \vdash e :: B$, for every expression $\Gamma; \Delta \vdash e' :: A$ and every $l \in \mathbb{R}$ we have:

$$(\|e\|)_{\rho\{x:=\|e'\|\}_{\rho, \xi}^l, \xi}^l \ge (\|e\{e'/x\}\|)_{\rho, \xi}^l$$
*Proof.* By induction on the expression e. We consider just the two most interesting cases.

Consider the case $e = e_1 : e_2$. By definition we have:

$$ (\mathbf{e}_1 : \mathbf{e}_2)^l_{\rho\{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\}} = \xi^l(\mathbf{e}) ((\mathbf{e}_1)^l_{\rho\{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\}}, (\mathbf{e}_2)^{l-1}_{\rho\{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\}}) $$

but by monotonicity we have:

$$ \begin{aligned} \xi^l(\mathbf{e}) ((\mathbf{e}_1)^l_{\rho\{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\}}, (\mathbf{e}_2)^{l-1}_{\rho\{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\}}) & \\ \geq \xi^l(\mathbf{e}) ((\mathbf{e}_1)^l_{\rho\{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\}}, (\mathbf{e}_2)^{l-1}_{\rho\{x:=(\mathbf{e}'_1)^{l-1}_{\rho,\xi}, \xi\}}) \end{aligned} $$

Since by induction hypothesis we have:

$$ \xi^l(\mathbf{e}) ((\mathbf{e}_1)^l_{\rho\{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\}}, (\mathbf{e}_2)^{l-1}_{\rho\{x:=(\mathbf{e}'_1)^{l-1}_{\rho,\xi}, \xi\}}) \geq \xi^l(\mathbf{e}) ((\mathbf{e}_1\{\mathbf{e}'/\mathbf{x}\})^l_{\rho,\xi}, (\mathbf{e}_2\{\mathbf{e}'/\mathbf{x}\})^{l-1}_{\rho,\xi}) $$

and since by definition:

$$ \xi^l(\mathbf{e}) ((\mathbf{e}_1\{\mathbf{e}'/\mathbf{x}\})^l_{\rho,\xi}, (\mathbf{e}_2\{\mathbf{e}'/\mathbf{x}\})^{l-1}_{\rho,\xi}) = ((\mathbf{e}_1 : \mathbf{e}_2)\{\mathbf{e}'/\mathbf{x}\})^l_{\rho,\xi} $$

the conclusion follows.

Consider now the case $e = \text{Case e}''$ of $c_1(\vec{x}_1) \to e_1, \dots, c_m(\vec{x}_m) \to e_m$. Then, by definition we have:

$$ (\mathbf{e})^l_{\rho\{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\}} = \max_{1 \le i \le m} \{ (\mathbf{e}_i)^l_{\rho\{\vec{x}_i=\vec{r}_i\}} \{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\} \\ | (\mathbf{e}''_1)^l_{\rho\{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\}} \ge (\mathbf{c}_i(\vec{x}_i))^l_{\rho\{\vec{x}_i=\vec{r}_i\}}, \xi \} $$

since clearly $x$ is disjoint from the variables in $\vec{x}_i$. By induction hypothesis we can show that:

$$ \begin{aligned} \max_{1 \le i \le m} \{ (\mathbf{e}_i)^l_{\rho\{\vec{x}_i=\vec{r}_i\}} \{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\} | & (\mathbf{e}''_1)^l_{\rho\{x:=(\mathbf{e}'_1)^l_{\rho,\xi}, \xi\}} \ge (\mathbf{c}_i(\vec{x}_i))^l_{\rho\{\vec{x}_i=\vec{r}_i\}}, \xi \} \\ \ge & \max_{1 \le i \le m} \{ (\mathbf{e}_i\{\mathbf{e}'/\mathbf{x}\})^l_{\rho\{\vec{x}_i=\vec{r}_i\}}, \xi | (\mathbf{e}''\{\mathbf{e}'/\mathbf{x}\})^l_{\rho\{\vec{x}_i=\vec{r}_i\}} \ge (\mathbf{c}_i(\vec{x}_i))^l_{\rho\{\vec{x}_i=\vec{r}_i\}}, \xi \} \end{aligned} $$

and so the conclusion follows. The other cases can be obtained similarly. $\square$

<figure><img src="image_6.png" /></figure>

We are now ready to define parametrized interpretations.

**Definition 17 (Parametrized Interpretation).** An expression $\Gamma; \Delta \vdash e : A$ admits a parametrized interpretation $|\cdot|_\xi^l$ if for each variable assignment $\rho$, the assignment $|\cdot|_{\rho,\xi}^l$ is monotonic and such that for each function definition $f(x_1, \dots, x_n) \doteq e'$ and for each $l \in \mathbb{R}$ the following holds:

$$ (\mathbf{f}(x_1, \dots, x_n))^l_{\rho, \xi} \ge (\mathbf{e}')^l_{\rho, \xi} $$
Parametrized interpretations can be extended to environment as expected and thanks to this extension it is easy to verify that parametrized interpretations behave similarly to usual interpretations with respect to program evaluation. Analogously, we will write $\langle\!\langle e \rangle\!\rangle_{\xi}^{l} \geq \langle\!\langle e' \rangle\!\rangle_{\rho, \xi}^{l}$ as a shorthand for $\forall \rho, \langle\!\langle e \rangle\!\rangle_{\rho, \xi}^{l} \geq \langle\!\langle e' \rangle\!\rangle_{\rho, \xi}^{l}$.

Similarly to the case of interpretation, we want to relate parametrized interpretations to the evaluation of programs. However, in order to do this we need to introduce a new evaluation relation counting the number of pattern matchings on stream data. Let $\mathcal{H}$, $e \Downarrow^k v$ be the relation defined in Figure 3. $\mathcal{H}$, $e \Downarrow^k v$ means that $\mathcal{H}$, $e \Downarrow v$ holds using exactly $k$ pattern matching rules on streams for producing $v$. We define $\Downarrow_v^k$ in the same manner: $\mathcal{H}$, $e \Downarrow_v^k v$ if $\mathcal{H}$, $\mathrm{eval}_A e \Downarrow^k v$.

$$
\begin{array}{c}
\displaystyle \frac{c \in C}{\mathcal{H}; c(e_1, \dots, e_n) \Downarrow^0 c(e_1, \dots, e_n)} \qquad \frac{\mathcal{H} \cup \{d\}; M \Downarrow^k v}{\mathcal{H}; \mathrm{LetRec} \mathrm{d} \mathrm{in} M \Downarrow^k v} \\[1.5em]
\displaystyle \frac{\mathcal{H}; e\{e_1/x_1, \dots, e_n/x_n\} \Downarrow^k v \quad (f x_1 \cdots x_n \doteq e) \in \mathcal{H}}{\mathcal{H}; f(e_1, \dots, e_n) \Downarrow^k v} \\[1.5em]
\displaystyle \frac{\mathcal{H}; e \Downarrow^k c(e'_1, \dots, e'_m) \quad p_i = c(x_1, \dots, x_m) \quad \mathcal{H}; e_i\{e'_1/x_1, \dots, e'_m/x_m\} \Downarrow^{k'} v}{\mathcal{H}; \mathrm{Case} \ e \ \mathrm{of} \ p_1 \to e_1, \dots, p_n \to e_n \ \Downarrow^{k+k'} v} \\[1.5em]
\displaystyle \frac{\mathcal{H}; e \Downarrow^k e'_1 : e'_2 \qquad \mathcal{H}; e_i\{e'_1/x_1, e'_2/x_2\} \Downarrow^{k'} v}{\mathcal{H}; \mathrm{Case} \ e \ \mathrm{of} \ x_1 : x_2 \to e_1, \mathrm{nil} \to e_2 \ \Downarrow^{k+k'+1} v} \\[1.5em]
\displaystyle \frac{\mathcal{H}; e \Downarrow^k c(e_1, \dots, e_m) \quad \forall i \le n, p_i \ne c(x_1, \dots, x_m)}{\mathcal{H}; \mathrm{Case} \ e \ \mathrm{of} \ p_1 \to e_1, \dots, p_n \to e_n \ \Downarrow^k \mathrm{Err}}
\end{array}
$$

<caption>Table 3: Counting stream pattern matchings</caption>

**Proposition 2.** Let $\mathcal{H}$ and $\emptyset$; $\Delta \vdash e :: A$ be an environment and an expression admitting both the parametrized interpretation $\langle\!\langle - \rangle\!\rangle_{\xi}^{l}$. Then:

$$
\mathcal{H}, e \Downarrow^k v \quad \text{implies} \quad \forall l \in \mathbb{R}, \quad \langle\!\langle e \rangle\!\rangle_{\xi}^{l} \geq \langle\!\langle v \rangle\!\rangle_{\xi}^{l-k}
$$

*Proof.* The proof is analogous to the proof of Proposition 1. The only interesting case is the one where the derivation ends with:

$$
\frac{\mathcal{H}; e \Downarrow^k e'_1 : e'_2 \quad \mathcal{H}; e_1\{e'_1/x_1, e'_2/x_2\} \Downarrow^{k'} v}{\mathcal{H}; \text{Case e of } x_1 : x_2 \to e_1, \text{nil} \to e_2 \Downarrow^{k+k'+1} v}
$$

By induction hypothesis, we have both $\langle\!\langle e_1\{e'_1/x_1, e'_2/x_2\} \rangle\!\rangle_{\xi}^{l-(k+1)} \geq \langle\!\langle v \rangle\!\rangle_{\xi}^{l-(k+1)-k'}$
and $\langle\|e\|\rangle_{\xi}^{l} \geq \langle\|e'_{1} : e'_{2}\|\rangle_{\xi}^{l-k}$. By definition we have:

$$ \langle\text{Case e of } \mathbf{x}_1 : \mathbf{x}_2 \to \mathbf{e}_1, \text{ nil} \to \mathbf{e}_2\rangle_{\rho, \xi}^{l} \geq \max\{\langle\|e_1\|\rangle_{\rho\{\mathbf{x}_1 = \mathbf{r}_1, \mathbf{x}_2 = \mathbf{r}_2\}, \xi}^{l}, \\ r_1, r_2 \in \mathbb{R}^{+} \text{ and } \langle\|e\|\rangle_{\rho, \xi}^{l} \geq \langle\|\mathbf{x}_1 : \mathbf{x}_2\|\rangle_{\rho\{\mathbf{x}_1 = \mathbf{r}_1, \mathbf{x}_2 = \mathbf{r}_2\}, \xi}^{l}\} $$

By induction hypothesis, we can satisfy the side condition in the max by setting $r_1 = \langle\|e'_{1}\|\rangle_{\rho, \xi}^{l-k}$ and $r_2 = \langle\|e'_{2}\|\rangle_{\rho, \xi}^{l-k-1}$ since by definition of parametrized interpretation $\langle\|e\|\rangle_{\xi}^{l} \geq \langle\|e'_{1} : e'_{2}\|\rangle_{\xi}^{l-k} = \xi^{l}(\langle\|e'_{1}\|\rangle_{\rho, \xi}^{l-k}, \langle\|e'_{2}\|\rangle_{\rho, \xi}^{l-k-1})$. So we have:

$$ \max\{\langle\|e_1\|\rangle_{\rho\{\mathbf{x}_1 = \mathbf{r}_1, \mathbf{x}_2 = \mathbf{r}_2\}, \xi}^{l} | \langle\|e\|\rangle_{\rho, \xi}^{l} \geq \langle\|\mathbf{x}_1 : \mathbf{x}_2\|\rangle_{\rho\{\mathbf{x}_1 = \mathbf{r}_1, \mathbf{x}_2 = \mathbf{r}_2\}, \xi}^{l}\} \\ \geq \langle\|e_1\|\rangle_{\rho\{\mathbf{x}_1 = \langle\|e'_{1}\|\rangle_{\rho, \xi}^{l-k}, \mathbf{x}_2 = \langle\|e'_{2}\|\rangle_{\rho, \xi}^{l-k-1}\}, \xi}^{l} $$

By monotonicity we have:

$$ \langle\|e_1\|\rangle_{\rho\{\mathbf{x}_1 = \langle\|e'_{1}\|\rangle_{\rho, \xi}^{l-k}, \mathbf{x}_2 = \langle\|e'_{2}\|\rangle_{\rho, \xi}^{l-k-1}\}, \xi}^{l} \geq \langle\|e_1\|\rangle_{\rho\{\mathbf{x}_1 = \langle\|e'_{1}\|\rangle_{\rho, \xi}^{l-k-1}, \mathbf{x}_2 = \langle\|e'_{2}\|\rangle_{\rho, \xi}^{l-k-1}\}, \xi}^{l-k-1} $$

Finally, by applying Lemma 5 twice we have:

$$ \langle\|e_1\|\rangle_{\rho\{\mathbf{x}_1 = \langle\|e'_{1}\|\rangle_{\rho, \xi}^{l-k-1}, \mathbf{x}_2 = \langle\|e'_{2}\|\rangle_{\rho, \xi}^{l-k-1}\}, \xi}^{l-k-1} \geq \langle\|e_1\{\mathbf{e}'_{1}/\mathbf{x}_1, \mathbf{e}'_{2}/\mathbf{x}_2\}\rangle_{\rho, \xi}^{l-(k+1)} $$

By induction hypothesis we have $\langle\|e_1\{\mathbf{e}'_{1}/\mathbf{x}_1, \mathbf{e}'_{2}/\mathbf{x}_2\}\|\rangle_{\xi}^{l-(k+1)} \geq \langle\|v\|\rangle_{\xi}^{l-(k+1)-k'}$, so the conclusion follows.

Since this holds for every $\rho$ and every $l \in \mathbb{R}$, the conclusion easily follows by definition of parametrized interpretation. $\square$

**Corollary 3.** Let $\mathcal{H}$ and $\emptyset$; $\Delta \vdash e :: A$ be an environment and an expression both admitting the parametrized interpretation $\langle|-\rangle_{\xi}^{l}$. Then:

$$ \mathcal{H}, e \Downarrow_{v}^{k} \underline{v} \text{ implies } \langle\|e\|\rangle_{\xi}^{l} \geq \langle\|v\|\rangle_{\xi}^{l-k} $$

*Proof.* Just check that we can define a parametrized interpretation of $\mathrm{eval}_A$ by setting $\forall l \in \mathbb{R}, \forall A, \xi^l(\mathrm{eval}_A)(X) = X$ as in Corollary 2. $\square$

**Lemma 6.** Let $\langle|-\rangle_{\xi}^{l}$ be a parametrized interpretation. Then, there exists a function $G : \mathbb{R}^{+} \times \mathbb{R}^{+} \to \mathbb{R}^{+}$ such that for every program $e :: A$ admitting $\langle|-\rangle_{\xi}^{l}$ and every $l \in \mathbb{R}^{+}$:

$$ \langle\|e\|\rangle_{\xi}^{l} \leq G(|\|e\|, l) $$

*Proof.* Define:

$$ F(X, L) = \max(\max_{t \in C \cup \mathcal{F}} \langle\|t\|\rangle_{\xi}^{L}(X, \dots, X), X) $$

and $F^{n+1}(X, L) = F(F^n(X, L), L)$ and $F^0(X, L) = F(X, L)$. It can be shown by induction on the structure of $e$ that $\langle\|e\|\rangle_{\xi}^{l} \leq F^{|e|}(|e|, l)$. If $e$ is a variable, a constructor or a function symbol of arity 0, then conclusion follows directly by definition of $F$, i.e $\langle\|e\|\rangle_{\xi}^{l} \leq F(|e|, l)$. Now, consider $e = t \mathbf{d}_1 \cdots \mathbf{d}_n$ and suppose $|\mathbf{d}_j| = \max_{i=1}^{n} |\mathbf{d}_i|$. By
induction hypothesis, $\langle |d_i| \rangle_{\xi}^l \le F^{|d_i|}(|d_i|, l)$. There are two possibilities depending on the shape of $t$. If $t \neq :$, that is $e \neq e_1 : e_2$, then by induction hypothesis, definition and monotonicity of $F$ we have:

$$ \begin{aligned} \langle |e| \rangle_{\xi}^{l} &= \xi^{l}(t)(\langle |d_1| \rangle_{\xi}^{l}, \dots, \langle |d_n| \rangle_{\xi}^{l}) \le \xi^{l}(t)(F^{|d_1|}(|d_1|, l), \dots, F^{|d_n|}(|d_n|, l)) \\ &\le \xi^{l}(t)(F^{|d_j|}(|d_j|, l), \dots, F^{|d_j|}(|d_j|, l)) \le F(F^{|d_j|}(|d_j|, l), l) \\ &\le F^{|d_j|+1}(|d_j|, l) \le F^{|e|}(|e|, l) \end{aligned} $$

In the case where $t = :$, and so $e = e_1 : e_2$, by definition of parametrized interpretation, induction hypothesis, definition and monotonicity of $F$ we have:

$$ \begin{aligned} \langle |e| \rangle_{\xi}^{l} &= \langle |e_1 : e_2| \rangle_{\xi}^{l} = \xi^{l}(\langle |e_1| \rangle_{\xi}, \langle |e_2| \rangle_{\xi}^{l-1}) \le \xi^{l}(\langle |e_1| \rangle_{|e_1|, l}, \langle |e_2| \rangle_{|e_2|, l-1}) \\ &\le \xi^{l}(\langle |e_1| \rangle_{|e_1|, l}, \langle |e_2| \rangle_{|e_2|, l}) \le F^{|e|}(|e|, l) \end{aligned} $$

We let the reader checking the other cases of the induction including the technical but simple case where $e = \text{Case e}'$ of $c_1(\bar{x}_1) \to e_1, \dots, c_m(\bar{x}_m) \to e_m$. Now the conclusion follows easily by taking $G(X, L) = F^X(X, L)$. $\square$

# 4. Space Upper Bounds

## 4.1. Motivations

In several situations it is useful to have an estimate of the space needed to store the elements produced by a stream program. In some cases, this estimate can be obtained by considering the size of the greatest element produced as an output by the program. In other situations, unfortunately this cannot be done because there is no such a maximal element. However, an interesting estimate can be given by considering the position of the element in the stream. In functional programming, the full evaluation of a stream is never expected. A programmer will evaluate only some elements of a stream using some function like `!!` or `take`. In this case, it may be possible to derive an upper bound on the size of the elements using the output index $n$ of the element we want to reach. For example, we know that the size of the complete evaluation of the expression `(nats 0) !! n`, using the function symbol `nats` of Example 1, is bounded by the size of $n$. Note that such a measure always exists when a stream is productive since it only consists in providing the size of the $n$-th output value, for each integer $n$.

In this section, we will show how to use interpretations to define two criteria useful to compute space estimates similar to the ones described above. The first criterion, named Local Upper Bound (LUB), will ensure that programs admitting a particular interpretation compute streams where the $n$-th element is bounded by a function $f$ in $n$ and in the size of the inputs. Thanks to Lemma 6 the criterion will provide an estimate of such an $f$. This criterion is named "local" because the bound relies also on the output index $n$. The second criterion, named Global Upper Bound (GUB), is a special case of LUB in which the output does not depend on the index $n$. It will ensure that programs admitting a particular interpretation compute stream elements bounded by a function $f$ in the size of the inputs, independently of the index. Again, thanks to Lemma 4 the criterion will provide an estimate of such an $f$. This criterion is named
"global" because the bound holds for all the output stream elements. This situation can be illustrated by the following figure:

<figure><img src="image_7.png" /><figcaption>Figure 1: Local Upper Bound</figcaption></figure>

A program e can be viewed as a box connecting a left tape representing the input stream and a right tape representing the output stream (we do not assume any synchrony between input and output). The program e has a *local upper bound* if each element $\underline{v}_j$ of the output stream has bounded size. Such a bound can depend not only on the size k of the maximal input stream element (in the case such a maximal element exists) but also on the the output element index j. In the particular case where this upper bound is independent of the index j, we say that e has a *global upper bound*. The aim of the LUB and GUB criteria we will present below is to exhibit a function $F: \mathbb{R}^+ \to \mathbb{R}^+$ witnessing these bounds.

## 4.2. Illustrating examples

A typical situation where programs have a local upper bound is described in the following example:

**Example 5.** Consider expressions built using the following definitions already presented in Example 2:

$$ \text{sadd} :: \text{Nat} \to \text{Nat} \to \text{Nat} $$

$$ \text{sadd } 0 \text{ y} \doteq y $$

$$ \text{sadd } (z + 1) y \doteq (\text{sadd } z y) + 1 $$

$$ \text{sadd} :: [\text{Nat}] \to [\text{Nat}] \to [\text{Nat}] $$

$$ \text{sadd}(x' : xs)(y' : ys) \doteq (\text{sadd} x' y') : (\text{sadd} xs ys) $$

Each program will only generate output stream elements whose size is bounded by a function in their index. For example, the program:

$$ e = \text{sadd}(\text{nats } \underline{3}) (\text{sadd}(\text{nats } \underline{5}) (\text{nats } \underline{4})) $$

is not globally bounded but if we evaluate the n-th output stream element as $\mathcal{H}$; $e_n \downarrow_v \underline{y}$, then we know that the size of $\underline{y}$ is bounded by $12 + 3 \times n$. Consequently, this program has a local upper bound given by the function $F(X) = 12 + 3 \times X$ applied to the index $n$.
A typical situation where programs have a global upper bound is described in the following example.

**Example 6.** Consider expressions built using the following function definitions:

repeat :: Nat → [Nat]
repeat x = x : (repeat x)
zip :: [a] → [a] → [a]
zip (x : xs) ys = x : (zip ys xs)
square :: [Nat] → [Nat]
square (x : xs) = (mul x x) : (square xs)
mul :: Nat → Nat → Nat
mul (x + 1) y = add y (mul x y)
mul 0 y = 0

Each program will only produce output stream elements whose size is bounded by some constant $k$. For instance, the program:

square (zip (repeat 5) (square (zip (repeat 7) (repeat 4)))))

computes stream elements whose size is bounded by $k = 2401 = 7^4$. So, its global upper bound is given by the constant $k = 2401$. Now, consider the following generalization of the above program:

$$ \text{square (zip (repeat 5) (square (zip x (repeat 4)))))} \quad (1) $$

It is easy to verify that when $x$ is substituted by a stream $s$ having element sizes bounded by a constant $k$, then the output stream will have only elements whose sizes are bounded either by $4^4$ or by $k^4$. So this expression has a global upper bound given by the function $F$ defined by $F(X) = \max(256, X^4)$.

The above examples clearly illustrate that a global upper bound implies a local upper bound but that the converse does not hold.

### 4.3. Definition

More formally, we can describe the situations outlined above using the formal framework presented in Section 2 as follows.

**Definition 18 (Local and Global Upper Bounds).** A stream program $e :: [\sigma]$ has a local upper bound if there is a function $F \in \mathbb{R}^+ \to \mathbb{R}^+$ such that:

$$ \forall \underline{n} \in \mathbb{N}, \text{ if } \mathcal{H}; \mathbf{e}_{\underline{n}} \Downarrow_{\underline{v}} \underline{v} \text{ then } F(|\underline{n}|) \geq |\underline{v}| $$

In the case the function $F$ is constant, then $e :: [\sigma]$ has also a global upper bound.

Note that the above definition can be used to analyze a stream program $e$ containing both stream functions and stream definitions (programs with stream functions are provided in Examples 11 and 12). Now consider the following examples in order to illustrate this definition.
### 4.5. Soundness

Now we want to show that if a given program $e :: [\sigma]$ is LUB (resp. GUB) then it has a local (resp. global) upper bound. For that purpose, we first show an intermediate technical lemma.

**Lemma 7.** Given an expression $e :: [\sigma]$:

1. If $e$ is a GUB program then $\forall \underline{n} \in \mathbb{N}$, s.t. $\mathcal{H}; e_{\underline{n}} \downarrow_v \underline{v}$ we have:

$$ (\|e\|)_{\xi} \geq (\|\underline{v}\|)_{\xi} $$

2. If $e$ is a LUB program of linearity constant $k$ then $\forall \underline{n} \in \mathbb{N}$, s.t. $\mathcal{H}; e_{\underline{n}} \downarrow_v \underline{v}$ we have:

$$ (\|e\|)_{\xi}^{k \times (|\underline{n}|+1)} \geq (\|\underline{v}\|)_{\xi}^{0} $$

*Proof.* (1) We proceed by induction on $\underline{n} \in \mathbb{N}$.

Let $\underline{n} = \underline{0}$ and $\mathcal{H}; e_{\underline{0}} \downarrow_v \underline{v}$. Then, necessarily we have a value $v'$ such that $\mathcal{H}; e \downarrow v'$. We have three cases, either $v' = \text{Err}$ or $v' = \text{nil}$ or $v' = e' : e''$. The former two cases are trivial. For the latter, by definition of GUB and by Proposition 1 we have:

$$ (\|e\|)_{\xi} \geq (\|e' : e''\|)_{\xi} = (\|\cdot\|)_{\xi}((\|e'\|)_{\xi}, (\|e''\|)_{\xi}) \geq (\|e'\|)_{\xi} $$

Since we clearly have $\mathcal{H}; e' \downarrow_v \underline{v}$, by applying Corollary 1 we obtain $(\|e'\|)_{\xi} \geq (\|\underline{v}\|)_{\xi}$. So by transitivity we can conclude $(\|e\|)_{\xi} \geq (\|\underline{v}\|)_{\xi}$.

Now, let $\underline{n} = \underline{n}' + 1$ and $\mathcal{H}; e_{(\underline{n}'+1)} \downarrow_v \underline{v}$. Again we have a value $v'$ such that $\mathcal{H}; e \downarrow v'$. The case $v' = \text{Err}$ is trivial. So, consider the case $v' = e' : e''$. Again by definition of GUB and by Proposition 1 we have:

$$ (\|e\|)_{\xi} \geq (\|e' : e''\|)_{\xi} = (\|\cdot\|)_{\xi}((\|e'\|)_{\xi}, (\|e''\|)_{\xi}) \geq (\|e''\|)_{\xi} $$

Moreover $\mathcal{H}; e_{(\underline{n}'+1)} \downarrow_v \underline{v}$ implies by definition that $\mathcal{H}; e''_{\underline{n}'} \downarrow_v \underline{v}$ and by induction hypothesis we have $(\|e''\|)_{\xi} \geq (\|\underline{v}\|)_{\xi}$. So we can conclude $(\|e\|)_{\xi} \geq (\|\underline{v}\|)_{\xi}$.

(2) Assume that $e :: [\sigma]$ is a LUB program of linearity constant $k$. We proceed by induction on $\underline{n} \in \mathbb{N}$.

Consider the base case where $\underline{n} = \underline{0}$. By assumption, we have $\mathcal{H}; e_{\underline{0}} \downarrow_v \underline{v}$ and, necessarily we have a value $v'$ such that $\mathcal{H}; e \downarrow v'$. We have three cases, either $v' = \text{Err}$ or $v' = \text{nil}$ or $v' = e' : e''$. The former two cases are trivial. For the latter, by definition of linear program with linearity constant $k$, we know that $\mathcal{H}; e \downarrow^{k'} e' : e''$, for some $e'$ such that $\mathcal{H}; e' \downarrow^{k''} \underline{v}$ with $k' + k'' \leq k$. Consequently, by Proposition 2 we have:

$$ (\|e\|)_{\xi}^{k \times (|\underline{0}|+1)} = (\|e\|)_{\xi}^{k} \geq (\|e' : e''\|)_{\xi}^{k-k'} $$

By definition it is easy to verify that:

$$ (\|e' : e''\|)_{\xi}^{k-k'} \geq (\|e'\|)_{\xi}^{k-k'} $$

and by Corollary 3 and monotonicity (since $k' + k'' \leq k$) we obtain:

$$ (\|e'\|)_{\xi}^{k-k'} \geq (\|\underline{v}\|)_{\xi}^{k-k'-k''} \geq (\|\underline{v}\|)_{\xi}^{0} $$
Now we prove the induction step for $\underline{n}' + 1 = \underline{n}$. Suppose that $\mathcal{H}: e_{\underline{n}} \downarrow_v^{k \times (|\underline{n}|+1)} \underline{v}$. It is easy to verify that necessarily $\mathcal{H}: e \downarrow_j^l e' : e''$ and $\mathcal{H}: e''_{\underline{n}'} \downarrow_v \underline{v}$ for some $j, j < k$. By applying Proposition 2 we have:

$$ (\mathbf{e})_{\xi}^{(|\underline{n}|+1) \times k} \geq (\mathbf{e}' : \mathbf{e}'')_{\xi}^{(|\underline{n}|+1) \times k-j} $$

By definition it is easy to verify that:

$$ (\mathbf{e}' : \mathbf{e}'')_{\xi}^{(|\underline{n}|+1) \times k-j} \geq (\mathbf{e}'')_{\xi}^{(|\underline{n}|+1) \times k-(j+1)} $$

and since $j + 1 \leq k$, by monotonicity:

$$ (\mathbf{e}'')_{\xi}^{(|\underline{n}|+1) \times k-(j+1)} \geq (\mathbf{e}'')_{\xi}^{k \times (|\underline{n}'|+1)} $$

Now, applying induction hypothesis we have:

$$ (\mathbf{e}'')_{\xi}^{k \times (|\underline{n}'|+1)} \geq (\underline{v})_{\xi}^{0} $$

and so the conclusion follows.

<figure><img src="image_8.png" /></figure>

We can now prove the main result of this section.

**Theorem 1.** If a program is LUB (GUB) then it admits a local (global) upper bound.

*Proof.* Consider a LUB program $e :: [\sigma]$ wrt the parametrized interpretation $(|-)_\xi^l$. By Lemma 6, there is a function $G: \mathbb{R}^+ \times \mathbb{R}^+ \to \mathbb{R}^+$ such that $\forall l \in \mathbb{R}^+$, $G(|e|, l) \geq (\mathbf{e})_\xi^l$. Let us take $F(X) = G(|e|, k \times (X+1))$, $k$ being the linearity constant of $e$, and assume for $\underline{n} \in \text{Nat}$ that $e_{\underline{n}} \downarrow_v \underline{v}$. By Lemma 7(2), we have $(\mathbf{e})_\xi^{k \times (|\underline{n}|+1)} \geq (\underline{v})_\xi^0$. Moreover, since $(|-)_\xi^0$ has a fixed parameter, it corresponds to an almost-additive interpretation. So, by Corollary 1 we have $(\underline{v})_\xi^0 \geq |\underline{v}|$. Summing up, we have:

$$ F(|\underline{n}|) = G(|e|, k \times (|\underline{n}| + 1)) \geq (\mathbf{e})_{\xi}^{k \times (|\underline{n}|+1)} \geq (\underline{v})_{\xi}^{0} \geq |\underline{v}| $$

and so the conclusion follows.

Now consider a GUB program $e :: [\sigma]$. By Lemma 4 there is a function $F: \mathbb{R}^+ \to \mathbb{R}^+$ such that $F(|e|) \geq (\mathbf{e})_\xi$. Let us take $K = F(|e|)$ and assume for $\underline{n} \in \text{Nat}$ that $\mathcal{H}: e_{\underline{n}} \downarrow_v \underline{v}$. By Lemma 7(1) we have $(\mathbf{e})_\xi \geq (\underline{v})_\xi$. Moreover, by Corollary 1 we have $(\underline{v})_\xi \geq |\underline{v}|$, since such that $\xi$ is an almost-additive symbol assignment. So, summing up, we have:

$$ K = F(|e|) \geq (\mathbf{e})_{\xi} \geq (\underline{v})_{\xi} \geq |\underline{v}| $$

and the conclusion follows.

<figure><img src="image_9.png" /></figure>

Thanks to the above theorem, if we can find a LUB interpretation for a program $e$, then we also have a local upper bound. Let us consider some examples.
**Example 9.** Consider again the stream definition of nats of Example 1:

$$
\begin{align*}
\mathit{nats} \coloneqq \mathit{Nat} &\to [\mathit{Nat}] \\
\mathit{nats} x &\doteq x : (\mathit{nats} (x + 1))
\end{align*}
$$

We want to show that nats is LUB. First, notice that the program nats is linear with linearity constant $k = 1$. Indeed, the definition of nats does not involve pattern matching on stream data so the only pattern matchings correspond to the !! definition where one read is needed to produce on output. Now, consider the parametrized interpretation $|-)_\rho$ defined by: $\xi^l(\mathit{nats})(X) = X + l$, $\xi^l(+1)(X) = X + 1$, $\xi^l(0) = 0$ and $\xi^l(:)(X, Y) = \max(X, Y)$. We check that $\forall l \in \mathbb{R}$:

$$
\begin{align*}
(\mathit{nats} \mathbf{x})_{\rho, \xi}^l &= (\mathit{nats})_{\rho, \xi}^l ((\mathbf{x})_{\rho, \xi}^l) = \rho(\mathbf{x}) + l \\
&\geq \max(\rho(\mathbf{x}), (\rho(\mathbf{x}) + 1) + (l - 1)) \\
&= \max((\mathbf{x})_{\rho, \xi}^l, (\mathit{nats}(\mathbf{x} + 1))_{\rho, \xi}^{l-1}) = ((\mathbf{x} : (\mathit{nats} (\mathbf{x} + 1)))_{\rho, \xi}^l
\end{align*}
$$

The interpretation $|-)_\rho^l$ clearly respects the required criterion for nats to be LUB. That is, it is almost-additive and it is defined on : as $\xi^l(:)(X, Y) = \max(X, Y)$.
So, nats admits a local upper bound. We obtain the required bound by setting $F(X) = (\mathit{nats}(\underline{m}))_{\rho, \xi}^X = X + (\underline{m})_{\rho, \xi} = X + |\underline{m}|$, for all canonical numerals $\underline{m}$, $n \in \mathbb{N}$ such that $(\mathit{nats} \underline{m}) !! \underline{n} \downarrow_v \mathbf{v}_n$, the following holds $F(|\underline{n}|) \ge |\underline{n}| + |\underline{m}| \ge |\mathbf{v}_n|$ (Indeed for all $\underline{n}$, $\mathbf{v}_n = \underline{m} + \underline{n}$).

**Example 10 (Fibonacci).** The following example computes the Fibonacci sequence:

$$
\begin{align*}
\mathit{tail} \coloneqq [a] &\to a \\
\mathit{tail} x : xs &\doteq xs \\
\mathit{fib} \coloneqq [\mathit{Nat}] \\
\mathit{fib} &\doteq \mathbf{0} : (\underline{\mathbf{1}} : (\mathit{sadd} \ \mathit{fib} \ (\mathit{tail} \ \mathit{fib})))
\end{align*}
$$

We want to show that this program is LUB. First, notice that fib is linear with linearity constant $k = 4$. Now, consider the parametrized interpretation $|-)_\rho$ defined by: $\xi^l(0) = 0$, $\xi^l(+1)(X) = X + 1$, $\xi^l(:)(X, Y) = \max(X, Y)$, $\xi^l(\mathit{sadd})(X, Y) = \xi^l(\mathit{add})(X, Y) = X + Y$, $\xi^l(\mathit{tail})(X) = X$ and $\xi^l(\mathit{fib}) = 2^l$. For the first rule and for each $l \in \mathbb{R}$, the following inequalities are satisfied:

$$
\begin{align*}
(\mathit{fib})_{\xi}^{l} &= 2^{l} & \ge \max(0, 1, 2 \times 2^{l-2}) \\
&= \max((\underline{0})_{\xi}^{l}, \max((\underline{1})_{\xi}^{l-1}, 2 \times (\mathit{fib})_{\xi}^{l-2})) \\
&= \max((\underline{0})_{\xi}^{l}, \max((\underline{1})_{\xi}^{l-1}, (\mathit{sadd fib (tail fib)})_{\xi}^{l-2})) \\
&= \max((\underline{0})_{\xi}^{l}, (\underline{1} : \mathit{sadd fib (tail fib)})_{\xi}^{l-1}) \\
&= (\underline{0} : (\underline{1} : \mathit{sadd fib (tail fib)}))_{\xi}^{l}
\end{align*}
$$

We let the reader check the inequalities for the other definitions. So, we have that $|-)_\rho^l$ respects the required criterion for fib to be LUB. That is, it is almost-additive and it is defined on : as $\xi^l(:)(X, Y) = \max(X, Y)$. Consequently, fib admits a local upper
bound. The function $2^l$ is a parametrized upper bound on the Fibonacci sequence: for each canonical numeral $\underline{n} \in \mathbb{N}$ s.t. $\text{fib}!! \underline{n} \downarrow_v \underline{v_n}$, the inequality $2^{4 \times (|\underline{n}|+1)} \ge |\underline{v_n}|$ is satisfied.

In the same way, if we can find a GUB interpretation for a program e, then we also have a global upper bound. Let us consider some examples.

**Example 11 (Thue-Morse sequence).** The following morse program computes the Thue-Morse sequence:

```
morse  :: [Nat]
morse  ≝  0 : (zip (inv morse) (tail morse))
tail  :: [a]
tail x : xs ≝  xs
inv   :: [Nat] → [Nat]
inv   0 : xs ≝  1 : xs
inv   1 : xs ≝  0 : xs
```

The morse program is GUB with respect to the following interpretation: $([0])_\xi = 0$, $([+1])_\xi(X) = 1 + X$, $([\cdot:\cdot])_\xi(X, Y) = ([\text{zip}])_\xi = \max(X, Y)$, $([\text{inv}])_\xi(X) = \max(1, X)$, $([\text{tail}])_\xi(X) = X$ and $([\text{morse}])_\xi = 1$. For instance, for the first rule the following inequality is satisfied:

$$ \begin{aligned} ([\text{morse}])_\xi = 1 &\ge \max(0, 1, 1, 1) \\ &= \max([0])_\xi, \max(1, ([\text{morse}])_\xi, ([\text{morse}])_\xi)) \\ &= \max([0])_\xi, \max([\text{inv morse}])_\xi, ([\text{tail morse}])_\xi)) \\ &= \max([0])_\xi, ([([\text{zip}](\text{inv morse})(\text{tail morse})))])_\xi) \\ &= ([0] : (\text{zip}(\text{inv morse})(\text{tail morse}))))_\xi \end{aligned} $$

We let the reader check the inequalities for the other definitions.

Note that the Thue-Morse program can be easily checked to have a global upper bound by looking to the (finite) output range even without using the criterion. However, this example shows that the analysis can be done in a modular way. Moreover it shows that even if only simple functions are used in interpretations some interesting examples can be captured.

**Example 12.** The program of Example 6 is GUB with respect to the interpretation $([\cdot])_{\rho,\xi}$ defined by:

$$ \begin{aligned} ([0])_\xi &= 0 \\ ([+1])_\xi(X) &= X + 1 \\ ([\text{add}])_\xi(X, Y) &= X + Y \\ ([\text{zip}])_\xi(X, Y) &= \xi(\cdot)(X, Y) = \max(X, Y) \\ ([\text{square}])_\xi(X) &= X^2 \\ ([\text{mul}])_\xi(X, Y) &= X \times Y \\ ([\text{repeat}])_\xi(X) &= X \end{aligned} $$
Indeed, we can check the inequalities of the interpretation is satisfied for every definition and for every variable assignment $\rho$. For the definition of repeat we have:

$$ 
\begin{align*}
(\text{repeat } x)_{\rho, \xi} &= (\text{repeat})_{\xi}((x)_{\rho, \xi}) \\
&= \rho(x) \\
&\geq \max(\rho(x), \rho(x)) \\
&= \xi(\rho(x))((x)_{\rho, \xi}, (\text{repeat } x)_{\rho, \xi}) \\
&= (x : (\text{repeat } x))_{\rho, \xi}
\end{align*}
$$

For the definition of zip:

$$ \text{zip } y s \doteq \text{Case z of } (x : xs) \to x : (\text{zip } y s xs) $$

we check the following inequality:

$$ 
\begin{align*}
(\text{zip } z ys)_{\rho, \xi} &= \max(\rho(z), \rho(ys)) \\
&\geq \max\{\max(u, v, \rho(ys)) \\
&\qquad | \forall u, v \in \mathbb{R}^+ \text{ s.t. } \rho(z) \geq \max(u, v)\} \\
&= \max\{(x : (\text{zip } ys xs))_{\rho[x=u,xs=v], \xi} \\
&\qquad | \forall u, v \in \mathbb{R}^+ \text{ s.t. } (z)_{\xi} \geq (x : xs)_{\rho[x=u,xs=v], \xi}\} \\
&= (\text{Case z of } (x : xs) \to x : (\text{zip } ys xs))_{\rho, \xi}
\end{align*}
$$

We let the reader check that the inequalities are also satisfied for the remaining definitions. Consequently, the program of Example 6 admits a global upper bound. In this particular setting, the program:

$$ e = \text{square}(\text{zip}(\text{repeat } \underline{5}))(\text{square}(\text{zip}(\text{repeat } \underline{7}))(\text{repeat } \underline{4}))) $$

admits a global upper bound that is equal to:

$$ 
\begin{align*}
(\mathbf{e})_{\rho, \xi} &= (\text{zip}(\text{repeat } \underline{5}))(\text{square}(\text{zip}(\text{repeat } \underline{7}))(\text{repeat } \underline{4})))_{\rho, \xi}^2 \\
&= (\max((\text{repeat } \underline{5})_{\rho, \xi}, (\text{square}(\text{zip}(\text{repeat } \underline{7}))(\text{repeat } \underline{4})))_{\rho, \xi})^2 \\
&= (\max((\underline{5})_{\rho, \xi}, (\max((\underline{7})_{\rho, \xi}, (\underline{4})_{\rho, \xi})))^2) \\
&= (\underline{7})_{\rho, \xi}^4 \\
&= 7^4
\end{align*}
$$

and we obtain that for all $\underline{n} \in \mathbb{N}$ such that $\mathcal{H}, e_n \downarrow_v v_n, 7^4 \geq |v_n|$.

# 5. Bounded Input/Output Properties

## 5.1. Motivations

In this section, we show how interpretations can be used to ensure stream properties relating input reads to output writes. In particular, we are interested in estimating the
ability of a program to return a certain finite amount of elements in the output stream when fed with some (finite part of the) input stream. Giving an upper bound on the quantities of information needed can be particularly useful to implement the program in an efficient way with respect to the needed memory.

Since we are interested in the dependencies with respect to the inputs, the properties we will analyze in this section mainly concern stream functions (whereas the properties presented in the previous sections also concern stream definitions). We will concentrate on two properties of stream functions:

* The length based I/O upper bound that provides an upper bound on the number of written output stream elements in the number of read input elements.

* The size based I/O upper bound, a more precise and general notion, that provides an upper bound on the number of written output stream elements in both the number and the size of read input elements.

The size based I/O upper bound is illustrated in Figure 2.

<figure><img src="image_10.png" /><figcaption>Figure 2: Size based Input/Output upper bound</figcaption></figure>

Here a stream function $e$ after reading $i$ elements from the input produces $j$ elements of the output. What we want is to obtain a relation linking $j$ to $i$. In particular we want a function $F$ describing an upper bound $F(i, |\vec{v}|)$ on $j$ with respect to $i$ and $|\vec{v}|$. We dub this kind of bound *size based* because the upper bound may depend also on the size of the input elements. In the particular case, where the function $F$ is independent from $|\vec{v}|$, we obtain a length based upper bound. We dub this kind of bound *length based* because it only relies on the length $i$ of the input (i.e. the number of input reads).

These properties are of finite nature. For this reason, we will define them in terms of finite stream fragments (i.e. finite lists) in a way that is a reminiscent of Bird and Wadler's *Take Lemma* [5].

**Notation for contexts.** For notational convenience, let $e(x)$ be a notation for the expression $e$ where the free variable $x$ is explicitly mentioned. Let $e(\vec{v})$ be a notation for $e(x)\{\vec{v}/x\}$ and, finally, define $(\|e\|)_{\rho,\xi}(r)$ by $(\|e\|)_{\rho,\xi}(r) = (\|e(x)\|)_{\rho\{x=r\},\xi}.$
## 5.2. Illustrating examples

A typical situation where programs have a length based Input/Output upper bound is described in the following example:

**Example 13.** Consider stream expressions defined in terms of the following definitions:

$$ \begin{aligned} \text{merge} &:: [a] \rightarrow [a] \rightarrow [a \times a] \\ \text{merge} (x:xs) (y:ys) &\doteq (x,y) : (\text{merge} ys xs) \end{aligned} $$

$$ \begin{aligned} \text{dup} &:: [a] \rightarrow [a] \\ \text{dup} (x:xs) &\doteq x : (x:(\text{dup} xs)) \end{aligned} $$

It is easy to verify that each such an expression will only generate a number of output elements related to the number of input read elements. For example, the expression:

$$ \text{dup}(\text{merge}(\text{dup s}) (\text{dup s})) $$

for each read element of the input stream s computes a number of output elements bounded by $k = 4$. Consequently, $F(i) = 4 \times i$ in this particular case.

A situation where programs have a size based Input/Output upper bound is described in the following example:

**Example 14.** Consider stream expressions defined in terms of the following definitions:

$$ \begin{aligned} \text{app} &:: [a] \rightarrow [a] \rightarrow [a] \\ \text{app} (x:xs) ys &\doteq x : (\text{app} xs ys) \\ \text{app} nil ys &\doteq ys \end{aligned} $$

$$ \begin{aligned} \text{upto} &:: \text{Nat} \rightarrow [\text{Nat}] \\ \text{upto} &0 \doteq \text{nil} \\ \text{upto} (x+1) &\doteq (x+1) : (\text{upto } x) \end{aligned} $$

$$ \begin{aligned} \text{extendupto} &:: [\text{Nat}] \rightarrow [\text{Nat}] \\ \text{extendupto} (x:xs) &\doteq \text{app} (\text{upto } x) (\text{extendupto } xs) \end{aligned} $$

It is easy to verify that such expressions will only generate a number of output elements related to the number and the size of input read elements. For example, the expression:

$$ \text{extendupto}(\text{extendupto } s) $$

it performs $\sum_{i=1}^{\lfloor n \rfloor} i$ output writes for each number $n$ it reads on the input stream s. Consequently, it has no length based Input/Output upper bound.

## 5.3. Definition

More formally, we can describe the situations outlined above as follows:

**Definition 22 (Length and Size Based I/O Upper Bounds).**

* A stream function $x :: [\sigma] \vdash e(x) :: [\tau]$ has a length based I/O upper bound if there is a function $F: \mathbb{R}^{+} \rightarrow \mathbb{R}^{+}$ such that for every expression $s :: [\sigma]$ we have:

$$ \forall \underline{n} \in \mathbb{N}, \text{ if } \mathcal{H}; s \upharpoonright_{\underline{n}} \downarrow_{\underline{v}} \text{ and } \mathcal{H}; \lg e(\underline{v}) \downarrow_{\underline{m}} \text{ then } F(|\underline{n}|) \geq |\underline{m}| $$
* A stream function $x :: [\sigma] \vdash e(x) :: [\tau]$ has a size based I/O upper bound if there is a function $F: \mathbb{R}^+ \to \mathbb{R}^+$ such that for every expression $s :: [\sigma]$ we have:

$$ \forall \mathbf{n} \in \mathbb{N}, \text{ if } \mathcal{H}: s \uparrow_{\mathbf{n}} \downarrow_{v} \underline{v} \text{ and } \mathcal{H}: \lg e(\underline{v}) \downarrow_{v} \underline{m} \text{ then } F(|\underline{v}|) \geq |\underline{m}| $$

Note that for simplicity we have defined the length and size based I/O upper bounds only in the case of a unary function. However, the above definition can be easily extended to the case of functions with multiple arguments. Notice that the size based I/O property informally generalizes the length based one, i.e. a size based I/O upper bounded program is also length based I/O program, just because size always bounds the length. However, in some situations it is preferable to have the uniformity given by the length based I/O upper bound.

### 5.4. LBUB and SBUB criteria

We now want to introduce two criteria ensuring that a stream function has a length and size based I/O upper bounds. The definitions of length and size based I/O upper bounds above have been given in terms of the $\lg$ and take function symbols. So, for simplicity in what follows we suppose that the considered stream functions do not use neither $\lg$ symbol nor take symbol.

**Definition 23 (LBUB and SBUB Interpretations).**

* An interpretation $\langle - \rangle_{\rho, \xi}$ is LBUB if $\langle - \rangle_{\rho, \xi}$ is almost-additive with $\xi(+1)(X) = X + 1$ and such that:

$$ \xi(\cdot)(X, Y) = Y + 1 \text{ (resp. } X + Y + 1) $$

* An interpretation $\langle - \rangle_{\rho, \xi}$ is SBUB if $\langle - \rangle_{\rho, \xi}$ is additive with $\xi(+1)(X) = X + 1$ and:

$$ \xi(\cdot)(X, Y) = X + Y + 1 $$

* An expression $x :: [\sigma] \vdash e(x) :: [\tau]$ is LBUB (resp. SBUB) if it admits an interpretation $\langle - \rangle_{\xi}$ such that $\langle - \rangle_{\rho, \xi}$ is LBUB (resp. SBUB).

### 5.5. Soundness

LBUB assignments have some basic properties useful to deal with length based upper bounds. In particular, they give precise measures on natural numbers and lists as shown by the following two lemmas. Note that SBUB assignments behaves similarly on natural numbers.

**Lemma 8.** Given a LBUB or SBUB assignment $\langle - \rangle_{\rho, \xi}$, for every $\mathbf{n} :: \text{Nat}$ we have $\langle \underline{\mathbf{n}} \rangle_{\rho, \xi} = |\underline{\mathbf{n}}|$.

*Proof.* By induction on the length of $\mathbf{n}$. The base case follows easily by additivity of $\langle - \rangle_{\rho, \xi}$. That is $|\underline{0}| = \langle \underline{0} \rangle_{\rho, \xi} = 0$.

Consider now the case $\mathbf{n} + 1$. We have $\langle \underline{\mathbf{n}} + 1 \rangle_{\rho, \xi} = \langle +1 \rangle_{\rho, \xi} (\langle \underline{\mathbf{n}} \rangle_{\rho, \xi}) = \langle \underline{\mathbf{n}} \rangle_{\rho, \xi} + 1$. By induction hypothesis $\langle \underline{\mathbf{n}} \rangle_{\rho, \xi} = |\underline{\mathbf{n}}|$ and so the conclusion follows. $\square$
Second, the interpretation of a finite list is equal to its length:

**Lemma 9.** Given a LBUB assignment $((\neg)\rho, \xi)$, for every $\underline{v}$ :: $[\sigma]$ we have if $\mathcal{H}$; $\lg \underline{v} \downarrow_v \underline{m}$ then $((\underline{v})\rho, \xi) = |\underline{m}|$.

*Proof.* By induction on the length of $\underline{v}$. The base case follows easily by almost-additivity of $((\neg)\rho, \xi)$. That is $|\underline{0}| = ((\text{nil})\rho, \xi) = 0$ since $\mathcal{H}$; $\lg \text{nil} \downarrow_v \underline{0}$.

Consider now the case $\underline{v}_1 : \underline{v}_2$ and suppose that $\mathcal{H}$; $\lg (\underline{v}_1 : \underline{v}_2) \downarrow_v \underline{m} + 1$. We have $((\underline{v}_1 : \underline{v}_2)\rho, \xi) = \xi(\cdot)((\underline{v}_1)\rho, \xi, (\underline{v}_2)\rho, \xi) = (\underline{v}_2)\rho, \xi + 1$. Moreover, $\mathcal{H}$; $\lg \underline{v}_2 \downarrow_v \underline{m}$ and, by induction hypothesis, $((\underline{v}_2)\rho, \xi) = |\underline{m}|$ and so the conclusion follows. $\square$

For simplicity we have assumed that the program expressions of this section do not contain the function symbol $\lg$. However, since our criteria are defined in terms of it, in order to prove their soundness we need to have an interpretation for it. This can be done easily. Indeed, every LBUB or SBUB assignment can be extended to accommodate an interpretation for the $\lg$ function symbol as follows.

**Lemma 10.** Suppose that the environment $\mathcal{H}$ admits the interpretation $((\neg)\rho, \xi)$ and that $((\neg)\rho, \xi)$ is a LBUB or SBUB assignment. Then, $((\neg)\rho, \xi)$ can be extended to the function symbol $\lg$ by setting $\xi(\lg)(X) = X$ in such a way that the environment $\{\lg y = \text{Case y of nil} \to \underline{0}, \text{Err} \to \underline{0}, x : xs \to (\lg xs) + 1\} \cup \mathcal{H}$ admits the interpretation $((\neg)\rho, \xi)$.

*Proof.* Consider the definition $\{\lg y \doteq \text{Case y of nil} \to \underline{0}, \text{Err} \to \underline{0}, x : xs \to (\lg xs) + 1\}$. We have to check that the extension of $((\neg)\rho, \xi)$ still satisfies the inequalities of an interpretation for this definition:

$$ \begin{aligned} ((\lg y)\rho, \xi) &= \rho(y) = r \\ &\geq \max(0, r) \\ &= \max(\max\{(\underline{0})\rho, \xi \mid r \geq ((\text{nil})\rho, \xi)\}, \\ &\qquad \max\{(\underline{0})\rho, \xi \mid r \geq ((\text{Err})\rho, \xi)\}, \\ &\qquad \max\{(\underline{\lg xs}) + 1\}_{\rho[x:=u,xs:=v],\xi} \mid \forall u, v \text{ s.t. } r \geq v + 1\}) \\ &= ((\text{Case y of nil} \to \underline{0}, \text{Err} \to \underline{0}, x : xs \to (\lg xs) + 1)\rho, \xi \end{aligned} $$

This inequality holds for every $\rho$ such that $\rho(y) = r$, for an arbitrary $r \geq 0$, and so the conclusion. $\square$

We are now ready to prove that the LBUB (resp. SBUB) is a criterion to ensure the length (resp. size) based I/O upper bound.

**Theorem 2.** If an expression $x :: [\sigma] \vdash e(x) :: [\tau]$ is LBUB (resp. SBUB) then it has also a length (resp. size) based I/O upper bound.

*Proof.* Given a LBUB expression $e(x)$, suppose $\mathcal{H}$; $s \upharpoonright_{\underline{n}} \downarrow_v \underline{v}$ and $\mathcal{H}$; $\lg e(\underline{v}) \downarrow_v \underline{m}$.

By Corollary 2, we have $((\lg e(\underline{v}))\rho, \xi) \geq ((\underline{m})\rho, \xi)$ and, by Lemma 10, we have $((e(\underline{v}))\rho, \xi) \geq ((\underline{m})\xi)$.

By Lemma 9, we have $((\underline{v})\rho, \xi) = |\underline{m}|$. Applying Lemma 8, we have $((\underline{m})\rho, \xi) = |\underline{m}|$. So, we obtain $((e)\rho, \xi)(|\underline{m}|) \geq |\underline{m}|$ and by taking $F = ((e)\rho, \xi)$ the conclusion follows.
Now suppose that $e(x)$ is SBUB, that $\mathcal{H}$; $s \upharpoonright_n \downarrow \underline{v}$ and that $\mathcal{H}$; $\lg e(\underline{v}) \downarrow_v \underline{m}$.

By Corollary 2, we have $\langle \lg e(\underline{v}) \rangle_{\xi} \ge \langle \underline{m} \rangle_{\xi}$ and by, Lemmata 8 and 10, we have $\langle e(\underline{v}) \rangle_{\xi} \ge \langle \underline{m} \rangle_{\xi} = |\underline{m}|$.

By definition, we obtain $\langle e(\underline{v}) \rangle_{\rho, \xi} = \langle e \rangle_{\rho, \xi}(\langle \underline{v} \rangle_{\rho, \xi})$. Moreover, by Lemma 2, since $\langle - \rangle_{\xi}$ is additive we have a constant $\alpha$ such that $\langle \underline{v} \rangle_{\rho, \xi} \le |\underline{v}| \times \alpha$. So, taking $F(X) = \langle e \rangle_{\rho, \xi}(X \times \alpha)$, the conclusion follows. $\square$

We end this section by showing that the situation presented in Example 13 can be captured using the LBUB criterion while the one in Example 14 can be captured using the SBUB criterion.

**Example 15.** Consider again the stream definitions presented in Example 13:

$$ \begin{align*} \text{merge} &:: [a] \rightarrow [a] \rightarrow [a \times a] \\ \text{merge} (x : xs) (y : ys) &\doteq (x, y) : (\text{merge} ys xs) \end{align*} $$

$$ \begin{align*} \text{dup} &:: [a] \rightarrow [a] \\ \text{dup} (x : xs) &\doteq x : (x : (\text{dup} xs)) \end{align*} $$

To verify that every expression built using these definitions has a length based I/O upper bound it is sufficient to verify that it admits the following LBUB interpretation:

$$ \xi(\text{merge})(X, Y) = \max(X, Y) \quad \xi(\text{dup})(X) = 2X $$

As an example, for each $s$ we have:

$$ \langle \text{dup} (\text{merge} (\text{dup } s) (\text{dup } s)) \rangle_{\rho, \xi} = 4 \langle s \rangle_{\rho, \xi} $$

and this gives a length based I/O upper bound.

**Example 16.** Consider again the stream definitions of Example 14:

$$ \begin{align*} \text{app} &:: [a] \rightarrow [a] \rightarrow [a] \\ \text{app} (x : xs) ys &\doteq x : (\text{app} xs ys) \\ \text{app} \text{ nil} ys &\doteq ys \end{align*} $$

$$ \begin{align*} \text{upto} &:: \text{ Nat} \rightarrow [\text{Nat}] \\ \text{upto} 0 &\doteq \text{ nil} \\ \text{upto} (x + 1) &\doteq (x + 1) : (\text{upto } x) \end{align*} $$

$$ \begin{align*} \text{extendupto} &:: [\text{Nat}] \rightarrow [\text{Nat}] \\ \text{extendupto} (x : xs) &\doteq \text{app} (\text{upto } x) (\text{extendupto } xs) \end{align*} $$

To show that every expression built using these definitions has a size based I/O upper bound it is enough to show that the following interpretation is SBUB:

$$ \xi(\text{nil}) = \langle 0 \rangle_{\xi} = 0 \quad \xi(+1)(X) = X + 1 \quad \xi(\cdot)(X, Y) = X + Y + 1 $$

$$ \xi(\text{app})(X, Y) = X + Y \quad \xi(\text{upto})(X) = \xi(\text{extendupto})(X) = 2 \times X^2 $$

In particular, by taking $F(X) = \langle \text{extendupto} \rangle_{\xi}(\langle \text{extendupto} \rangle_{\xi}(X))$ we obtain a size based upper bound for the expression:

$$ \text{extendupto} (\text{extendupto } s) $$
That is $F(X) = 8 \times X^4$ is an upper bound on the number of output elements. Notice that the bound is less tight than what one would have expected. Indeed, in this example $F$ gives a bound also on the size of produced elements.

# 6. Computing an Interpretation

One of the aspects of interpretation methods that makes them of practical interest is that they do not only provide techniques to ensure the existence of particular upper bounds but in several cases of practical interest they also actually provide a tool to effectively compute those upper bounds. Indeed, Lemma 4 says that if we have an interpretation of a given program $M$, then we can compute an upper bound on the size of the result of its evaluation. So it is natural to consider the corresponding interpretation synthesis problem that can be formulated as follows:

**Interpretation synthesis problem:** given a program $M$ and a class of functions $\mathcal{F}$, is an interpretation for $M$ using only functions in $\mathcal{F}$ computable?

The ability of being able to compute an interpretation clearly depends on the class of functions $\mathcal{F}$ that one wants to consider. In particular as a consequence of the Rice's theorem the interpretation synthesis problem is undecidable for an unrestricted class of computable functions. More interestingly this problem becomes decidable when restricted class of functions are considered. See [34] for a survey.

Even if in this paper we do not concentrate on the synthesis problem for the different criteria we have introduced, the possibility of having efficient procedures to compute the studied bounds is a strong motivation of our work. In particular, the criteria studied here become particularly useful when the interpretations use only small classes of functions as codomain (e.g. polynomials, logarithmic or linear functions). We leave this important study for future works.

Another related problem that we have not addressed here is the complexity of the interpretation synthesis problem. This problem has been previously studied for functions coming from max-plus and max-poly algebras over integers and reals and the results obtained can be adapted to our framework (see [34]).

It is worth noting that this problem has also been studied by the rewriting community both from theoretical and practical points of view [30, 25].

# 7. Related works

In the data processing scenario, a greater attention is paid to the so called streaming algorithms. These are algorithms working with restricted computational power on huge amount of data (not necessarily infinite). Usually they have only limited access to the inputs and they have only a little amount of available memory. Moreover, they may also satisfy some timing constraints. Moreover, the criteria we have designed so far are inspired by the constraints that streaming algorithms should usually satisfy.

It is not surprising that when one wants to implement programs working on streams, one needs to pay attention to memory management. It is indeed not difficult to find examples of stream programs generating subtle buffering or overflow errors. In this
perspective, in [17] Frankau and Mycroft have proposed a framework that, starting
from programs written in a first-order functional language, extracts stream program
implementations avoiding unbounded buffering. In order to achieve this goal, their
programs have to obey some specific linearity and stability typing disciplines. Anal-
ogously, Hughes et al. in their paper introducing sized types [22] show how the latter
can be used to prevent errors related to memory leaks and buffer overflows of embed-
ded programs. Even if sized types have been mainly introduced to prove termination
properties of reactive systems (corresponding to productivity of stream programs) they
have also found several applications in complexity analysis. For instance in [37], the
authors show how to exploit sized types in a system designed to verify the resource
usage of strict first-order programs working on lists. The programming language they
are able to analyze through their type system is similar to the language we consider in
the present paper, a key distinction being that their analysis is restricted to finite lists.

It is quite surprising that in the implicit computational complexity domain only few
works have been carried so far on programs computing over infinite data structures.
This is even more surprising if one thinks that usual tools of complexity theory, well
behaving on finite data types, cannot be directly applied neither to streams nor to other
infinite data structures. In [10] Burrell et al. have developed a sound and complete
polynomial time complexity programming language, dubbed Pola, based on a type
system with restrictions inspired by safe recursion. Interestingly, Pola permits the pro-
grammer to deal with polynomial time functional programs working both on inductive
and coinductive data types.

In [29], Leivant and Ramyaa have proposed a framework based on equational pro-
grams and intrinsic theories, previously introduced by Leivant in [28], that is useful to
reason about programs over inductive and co-inductive types. They used such a frame-
work to obtain an implicit characterization of primitive corecurrence (a weak form of
productivity). More recently, in [36] they have also shown that a ramified version of
co-recurrence gives an implicit characterization of the class of functions over streams
working in logarithmic space. In contrast to our approach considering functions work-
ing on data types, their characterization deals with functions working on streams of
digits; however, they consider the complexity of a stream program as a function of the
output. That is the space needed to compute the *n*-th element of the stream. With this
respect, their characterization uses an approach similar to the one we follow for the
Local Upper Bound property and for the Bounded Input/Output properties.

Using an approach similar to the one presented in this paper, Férée et al. [16] show
that interpretations can be used on stream programs also to characterize type 2 poly-
nomial time functions. In particular, they extend interpretations in order to use second
order polynomials to characterize the set of functions computable in polynomial time
by Oracle Turing Machines and by their unitary version. Thanks to this they obtain
an implicit characterization of the class of the Basic Feasible Functionals of Cook and
Urquhart [11].

Recently, Baillot and Dal Lago [4] have developed a technique inspired by quasi-
interpretations to study the complexity of higher-order rewriting programs. In their
framework infinite data are first class citizens in the form of higher order functions.
However, they do not consider programs working on declarative infinite data structures
as streams that are instead the focus of our work.
## 8. Conclusion

In this paper, we have studied some complexity properties of programs working on streams. In order to do this, in a first step we have adapted the interpretation methods to a functional programming languages able to express in a natural way stream programs. This has required to customize the definitions of interpretations, developed so far in the context of first-order term rewriting, to the more specific case of a first-order lazy functional programming language. As a byproduct, this has shown the flexibility of the interpretation tools in dealing with different object languages and in dealing with streams and infinite data types.

In a second step, we have exploited the use of interpretation methods by defining several criteria for the study of different space properties. These criteria correspond to resource static analyses useful to the programmer that would be able to control the complexity of the stream program he writes. They fall in two main categories:

* The first category, that includes local and global upper bounds, provides an upper bound on the size of each computed stream element. This upper bound can be a constant in the case of the global upper bound or a function of the output element position in the case of the local upper bound. The stream program that can be analyzed with respect to these criteria gives the guarantee that no one of its output elements will provoke a *memory overflow*.

* The second category, that includes the size and length based input and output upper bounds, provides an upper bound on the number of output elements with respect to the number or size of input reads.

The two categories above deal with two different dimensions of streams. By combining together the different criteria one can study several memory management aspects of programs working on streams.

[1] Abramsky, S., Ong, C.-H. L., 1993. Full abstraction in the lazy lambda calculus. Inf. Comput. 105 (2), 159-267.

[2] Amadio, R., 2005. Synthesis of max-plus quasi-interpretations. Fundamenta Informaticae 65(1-2).

[3] Ariola, Z. M., Felleisen, M., 1997. The call-by-need lambda calculus. J. Funct. Program. 7 (3), 265-301.

[4] Baillot, P., Dal Lago, U., 2012. Higher-Order Interpretations and Program Complexity. In: Proceedings of CSL'12. Vol. 16 of Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp. 62-76.

[5] Bird, R., Wadler, P., 1988. Introduction to Functional Programming. Prentice Hall.

[6] Bonfante, G., Cichon, A., Marion, J.-Y., Touzet, H., 2001. Algorithms with polynomial interpretation termination proof. Journal of Functional Programming 11 (1), 33-53.
[7] Bonfante, G., Marion, J., Moyen, J., 2011. Quasi-interpretations a way to control resources. Theoretical Computer Science.

[8] Bonfante, G., Marion, J.-Y., Moyen, J.-Y., Jul 2001. On lexicographic termination ordering with space bound certifications. In: PSI. Vol. 2244 of LNCS. Springer.

[9] Bonfante, G., Marion, J.-Y., Moyen, J.-Y., Péchoux, R., 2005. Synthesis of quasi-interpretations. LCC2005, LICS Workshop.

[10] Burrell, M. J., Cockett, R., Redmond, B. F., August 2009. Pola: a language for PTIME programming. In: Tenth International Workshop on Logic and Computational Complexity. Los Angeles, USA.

[11] Cook, S., Urquhart, A., 1989. Functional interpretations of feasibly constructive arithmetic. In: Proceedings of the twenty-first annual ACM symposium on Theory of computing. STOC '89. ACM, New York, NY, USA, pp. 107–112.

[12] Coquand, T., 1994. Infinite objects in type theory. Vol. 806 of LNCS. Springer, pp. 62–78.

[13] Cousot, P., Cousot, R., 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. Proceedings of ACM POPL'77, 238–252.

[14] Dijkstra, E.-W., 1980. On the productivity of recursive definitions, EWD749. URL http://www.cs.utexas.edu/users/EWD/ewd07xx/EWD749. PDF

[15] Endrullis, J., Grabmayer, C., Hendriks, D., Isihara, A., Klop, J., 2007. Productivity of Stream Definitions. Vol. 4639 of LNCS. Springer, p. 274.

[16] Férée, H., Hainry, E., Hoyrup, M., Péchoux, R., 2010. Interpretation of stream programs: characterizing type 2 polynomial time complexity. Springer, pp. 291–303.

[17] Frankau, S., Mycroft, A., 2003. Stream processing hardware from functional language specifications. Proceeding of IEEE HICSS-36.

[18] Gaboardi, M., Péchoux, R., 2009. Upper bounds on stream I/O using semantic interpretations. In: CSL 2009. Vol. 5771 of LNCS. Springer, pp. 271–286.

[19] Gaboardi, M., Péchoux, R., 2010. Global and local space properties of stream programs. In: 1st International Workshop on Foundational and Practical Aspects of Resource Analysis – FOPARA'09. Vol. 6324 of LNCS. pp. 51–66.

[20] Gordon, A., 1999. Bisimilarity as a theory of functional programming. TCS 228.

[21] Henderson, P., Morris, J., 1976. A lazy evaluator. Proceedings of POPL'76, 95–103.
[22] Hughes, J., Pareto, L., Sabry, A., 1996. Proving the correctness of reactive systems using sized types. Proceedings of ACM POPL'96, 410-423.

[23] Kennaway, J., Klop, J., Sleep, M., de Vries, F., 1989. Transfinite Reductions in Orthogonal Term Rewriting Systems. Vol. 488 of LNCS. pp. 1-12.

[24] Kennaway, J., Klop, J., Sleep, M., de Vries, F., 1997. Infinitary lambda calculus. TCS 175 (1), 93-125.

[25] Korp, M., Sternagel, C., Zankl, H., Middeldorp, A., 2009. Tyrolean termination tool 2. In: RTA. Springer, pp. 295-304.

[26] Lankford, D., 1979. On proving term rewriting systems are noetherian, tech. rep.

[27] Launchbury, J., 1993. A natural semantics for lazy evaluation. Proceedings of POPL'93, 144-154.

[28] Leivant, D., 1995. Intrinsic theories and computational complexity. In: Leivant, D. (Ed.), Logic and Computational Complexity. Vol. 960 of Lecture Notes in Computer Science. Springer Berlin / Heidelberg, pp. 177-194.

[29] Leivant, D., Ramyaa, R., 2012. Implicit complexity for coinductive data: a characterization of corecurrence. In: Marion, J.-Y. (Ed.), Second Workshop on Developments in Implicit Computational Complexity. Vol. 75 of EPTCS. Open Publishing Association, pp. 1-14.

[30] Lucas, S., 2005. Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theoretical Informatics and Applications 39 (3), 547-586.

[31] Manna, Z., Ness, S., 1970. On the termination of Markov algorithms. In: Third hawaii international conference on system science. pp. 789-792.

[32] Marion, J.-Y., Péchoux, R., 2009. Sup-interpretations, a semantic method for static analysis of program resources. ACM Transactions on Computational Logic (TOCL) 10 (4), 27.

[33] Ong, C.-H. L., 1992. Lazy lambda calculus: Theories, models and local structure characterization (extended abstract). In: ICALP. pp. 487-498.

[34] Péchoux, R., 2013. Synthesis of sup-interpretations: A survey. Theor. Comput. Sci. 467, 30-52.

[35] Pitts, A. M., 1997. Operationally-based theories of program equivalence. In: Semantics and Logics of Computation. Cambridge University Press.

[36] Ramyaa, R., Leivant, D., 2011. Ramified corecurrence and logspace. ENTCS 276 (0), 247-261, Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII).

[37] Shkaravska, O., van Eekelen, M., Tamalet, A., July 2009. Collected Size Semantics for Functional Programs over Polymorphic Nested Lists. Tech. Rep. ICIS-R09003, Radboud University Nijmegen.
[38] Sijtsma, B., 1989. On the productivity of recursive list definitions. ACM TOPLAS 11 (4), 633–649.

[39] Stephens, R., 1997. A survey of stream processing. Acta Informatica 34 (7), 491–541.

[40] Weihrauch, K., 1997. A foundation for computable analysis. Vol. 1337 of LNCS. Springer, pp. 185–200.

## Appendix A. Comparison with quasi-interpretation

Quasi-interpretations introduced in [7] are a previous formulation of interpretations that require inequalities of the shape $\|l\|_{\xi} \ge \|r\|_{\xi}$ for each rule $l \to r$ of a TRS. Note that the new definition suggested in this paper is a generalization of these previous works on TRS to functional programs since the interpretation of a definition $f x \doteq$ Case $x$ of $c_1(\vec{x}_1) \to e_1, \dots, c_m(\vec{x}_m) \to e_m$ generates the following inequality:

$$ (\|f x\|_{\rho, \xi} \ge \max_{i \in \{1, m\}} \{\|(e_i)_{\rho(\vec{x}_i := \vec{r}_i)}\|_{\xi} \mid \forall \vec{r}_i \text{ s.t. } (\|x\|_{\rho, \xi} \ge \|(c_i(\vec{x}_i))_{\rho(\vec{x}_i := \vec{r}_i)}\|_{\xi}\}) $$

which implies, using Lemma 3, $\forall i \in \{1, m\}$:

$$ \begin{align*} & (\|f c_i(\vec{x}_i)\|)_{\rho, \xi} \\ &= (\|f x\{c_i(\vec{x}_i)/x\}\|)_{\rho, \xi} \\ &\ge \max_{i \in \{1, m\}} \{\|(e_i)_{\rho(\vec{x}_i := \vec{r}_i)}\|_{\xi} \mid \forall \vec{r}_i \text{ s.t. } (\|x\{c_i(\vec{x}_i)/x\}\|)_{\rho, \xi} \ge \|(c_i(\vec{x}_i))_{\rho(\vec{x}_i := \vec{r}_i)}\|_{\xi}\} \\ &\ge \max\{\|(e_i)_{\rho(\vec{x}_i := \vec{r}_i)}\|_{\xi} \mid \forall \vec{r}_i \text{ s.t. } (\|c_i(\vec{x}_i)\|)_{\rho, \xi} \ge \|(c_i(\vec{x}_i))_{\rho(\vec{x}_i := \vec{r}_i)}\|_{\xi}\} \\ &\ge \|(e_i)_{\rho, \xi}\} \end{align*} $$

The last inequality is obtained by taking the particular values $r_i = \rho(x_i)$ since, in this particular case, $\rho\{\vec{x}_i := \vec{r}_i\} = \rho\{\vec{x}_i := \rho(\vec{x}_i)\} = \rho$ and, consequently, the inequality $\|(c_i(\vec{x}_i))_{\rho, \xi} \ge \|(c_i(\vec{x}_i))_{\rho(\vec{x}_i = \vec{r}_i)}\|_{\xi}$ is satisfied. To conclude, we obtain $\forall i \in \{1, m\}$, $\|(f c_i(\vec{x}_i))_{\rho, \xi} \ge \|(e_i)_{\rho, \xi}\|$ which corresponds exactly to the notion of quasi-interpretation applied to the equivalent TRS defined by the rules $f c_1(\vec{x}_1) \to e_1, \dots, f c_m(\vec{x}_m) \to e_m$.

## Appendix B. An example of Strict Evaluation

Consider an environment $\mathcal{H}$ containing the functions defined in Example 1. As already stressed, the lazy evaluation produces the first bit of information. So, for instance we have:

$$ \frac{\mathcal{H}; 0 : (\text{nats } (0+1)) \downarrow 0 : (\text{nats } (0+1))}{\mathcal{H}; \text{nats } 0 \downarrow 0 : (\text{nats } (0+1))} \quad \begin{array}{l} \text{(val)} \\ \text{(fun)} \end{array} $$

When a pattern matching error occurs this is traced by the Err constant. So, since the definition of zip without syntactic sugar is:

$$ \text{zip } x y \doteq \text{Case } x \text{ of } z : w \to z : (\text{zip } y w) $$
then we clearly have the following evaluation:

$$ \frac{\overline{\mathcal{H}; \text{nil} \downarrow \text{nil}}^{\text{(val)}} \quad \text{nil} \neq \text{z} : \text{w}}{\overline{\mathcal{H}; \text{Case nil of } z : \text{w} \to z : (\text{zip nil } w) \downarrow \text{Err}}^{\text{(pm}_e^{\text{e})}} \quad \text{(fun)}} \quad \mathcal{H}; \text{zip nil nil} \downarrow \text{Err} $$

Note that the following evaluation does not produce a pattern matching error:

$$ \frac{\overline{\mathcal{H}; 0 : \text{nil} \downarrow 0 : \text{nil}} \quad \overline{\mathcal{H}; 0 : (\text{zip nil nil}) \downarrow 0 : (\text{zip nil nil})}}{\overline{\mathcal{H}; \text{Case } (0 : \text{nil}) \text{ of } z : \text{w} \to z : (\text{zip nil } w) \downarrow 0 : (\text{zip nil nil})}} \quad \mathcal{H}; \text{zip } (0 : \text{nil}) \text{ nil} \downarrow 0 : (\text{zip nil nil}) $$

Now, let us consider the environment $\mathcal{H}'$ obtained by adding to $\mathcal{H}$ the functions definitions defining $\text{eval}_{\text{Nat}}$ on lists of numerals:

$$ \begin{align*} \text{eval}_{\text{Nat}} &:: [\text{Nat}] \to [\text{Nat}] \\ \text{eval}_{\text{Nat}} & \quad \text{Err} \quad \doteq \quad \text{Err} \\ \text{eval}_{\text{Nat}} & \quad \text{nil} \quad \doteq \quad \text{nil} \\ \text{eval}_{\text{Nat}} & \quad (x : y) \quad \doteq \quad \text{cons} (\text{eval}_{\text{Nat}} x) (\text{eval}_{\text{Nat}} y) \end{align*} $$

where $\text{eval}_{\text{Nat}}$ is defined analogously using the strict function $\text{succ}$ defined above and $\text{cons}$ is the function symbol for the strict version of the list of natural numbers constructor:

$$ \begin{align*} \text{cons} \quad \text{Err} \quad \text{Err} \quad \doteq \quad \text{Err} : \text{Err} \\ \text{cons} \quad \text{Err} \quad \text{nil} \quad \doteq \quad \text{Err} : \text{nil} \\ \text{cons} \quad 0 \quad \text{nil} \quad \doteq \quad 0 : \text{nil} \\ \text{cons} \quad (x + 1) \quad \text{nil} \quad \doteq \quad (x + 1) : \text{nil} \\ \text{cons} \quad \text{Err} \quad (y : z) \quad \doteq \quad \text{Err} : (y : z) \\ \text{cons} \quad 0 \quad (y : z) \quad \doteq \quad 0 : (y : z) \\ \text{cons} \quad (x + 1) \quad (y : z) \quad \doteq \quad (x + 1) : (y : z) \end{align*} $$

By evaluating the expression $\text{eval}_{\text{Nat}}(\text{zip } (0 : \text{nil}) \text{ nil})$, we obtain a result distinct from the result obtained without using the $\text{eval}_{\text{Nat}}$ function symbol. Indeed, this allows us to explore the entire result as shown by the following derivation where some steps are omitted for clarity:

$$ \begin{array}{c} \displaystyle\frac{\vdots}{\mathcal{H}'; \text{zip nil nil} \downarrow \text{Err}} \\ \\ \displaystyle\frac{\mathcal{H}'; \text{eval}_{\text{Nat}} 0 \downarrow 0}{\mathcal{H}'; \text{eval}_{\text{Nat}} (\text{zip nil nil}) \downarrow \text{Err}} \\ \\ \displaystyle\frac{\vdots}{\mathcal{H}'; \text{cons} (\text{eval}_{\text{Nat}} 0) (\text{eval}_{\text{Nat}} (\text{zip nil nil})) \downarrow 0 : \text{Err}} \\ \\ \displaystyle\frac{\vdots}{\mathcal{H}'; \text{eval}_{\text{Nat}} (\text{zip } (0 : \text{nil}) \text{ nil}) \downarrow 0 : \text{Err}} \end{array} $$