Marco Gaboardi
email: m.gaboardi@dundee.ac.uk

Romain Péchoux
email: pechoux@loria.fr

On Bounding Space Usage of Streams Using Interpretation Analysis

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

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.

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 realtime 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 streambased computations, see [START_REF] Stephens | A survey of stream processing[END_REF] 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 [START_REF] Kennaway | Transfinite Reductions in Orthogonal Term Rewriting Systems[END_REF] and infinitary lambda-calculus [START_REF] Kennaway | Infinitary lambda calculus[END_REF]. 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 [START_REF] Weihrauch | A foundation for computable analysis[END_REF]. 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 [START_REF] Henderson | A lazy evaluator[END_REF]. 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 [START_REF] Pitts | Operationally-based theories of program equivalence[END_REF][START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF]. A property of stream definitions that has motivated many studies is productivity [START_REF] Dijkstra | On the productivity of recursive definitions[END_REF]. 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 [START_REF] Sijtsma | On the productivity of recursive list definitions[END_REF][START_REF] Coquand | Infinite objects in type theory[END_REF][START_REF] Hughes | Proving the correctness of reactive systems using sized types[END_REF][START_REF] Endrullis | Productivity of Stream Definitions[END_REF].

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 [START_REF] Manna | On the termination of Markov algorithms[END_REF][START_REF] Lankford | On proving term rewriting systems are noetherien[END_REF], to obtain sound approximations of program behaviors useful to static analysis [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] and to obtain implicit characterizations of complexity classes [START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF][START_REF] Marion | Sup-interpretations, a semantic method for static analysis of program resources[END_REF].

One variation of particular interest for implicit computational complexity is the notion of quasi-interpretation [START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF]. 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, quasiinterpretations 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 [START_REF] Amadio | Synthesis of max-plus quasi-interpretations[END_REF][START_REF] Bonfante | Synthesis of quasiinterpretations[END_REF]. 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 [START_REF] Gaboardi | Upper bounds on stream I/O using semantic interpretations[END_REF] and [START_REF] Gaboardi | Global and local space properties of stream programs[END_REF]. In [START_REF] Gaboardi | Global and local space properties of stream programs[END_REF], we mainly studied the space upper bounds properties while in [START_REF] Gaboardi | Upper bounds on stream I/O using semantic interpretations[END_REF] 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: 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:

repeat :: Nat → [Nat] repeat x . = x : (repeat x) zip :: [a] → [a] → [a] zip (x : xs) ys . = x : (zip ys xs)
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:

nats :: Nat → [Nat] nats x . = x : (nats (x + 1)) sadd :: [Nat] → [Nat] → [Nat]
sadd (x : xs) (y : ys) . = (add x y) : (sadd xs ys)

Every stream s built using nats and sadd is not globally bound. 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:

merge :: [a] → [a] → [a × a] merge (x : xs) (y : ys) . = (x, y) : (merge ys xs) dup :: [a] → [a] dup (x : xs) . = x : (x : (dup xs))
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 × 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:

app :: [a] → [a] → [a] app (x : xs) ys . = x : (app xs ys) app nil ys . = ys upto :: Nat → [Nat] upto 0 . = nil upto (x + 1) . = (x + 1) : (upto x) extendupto :: [Nat] → [Nat] extendupto (x : xs) . = app (upto x) (extendupto xs)
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=1 i elements. In order to generalize 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 external parameter. In the parametrized interpretations, all the functions appearing in the assignments can depend on external parameters. However, the parameter has a different 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.

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 operational semantics differs from the Haskell one since we do not consider sharing.

Syntax and Types

Let X , C and 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 X , C, F and C ∪ F, respectively. Definition 1. The syntax of the SFL language is described by the following grammar: 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. •, • ) and 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.

p ::= x | c(x, . . . , x) (
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 1 , e 2 ), for some expressions e 1 and e 2 .

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 f 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 1 , • • • , x n )
. = e, the bound variables of d are the ones of e and x 1 , . . . , x n . 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 1 , • • • , x n ) .
= 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

• |x| = 1 • |t(e 1 , • • • , e n )| = 0 if t is of arity 0 1≤i≤n |e i | + 1 if t is of arity n ≥ 1 • |LetRec d in e| = |e| • |Case e of p 1 → e 1 , . . . , p n → e n | = |e| + max 1≤i≤n |e i |
Note that if we take N to be the set of natural number expressions inductively defined using the constructors 0 and + 1 then for each n ∈ N we have |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 , • • • , x n )
. = e is well-formed if and only if all the free variables of e are among x 1 • • • 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 , • • • , x n ) . = 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 e as a shorthand for a sequence of expressions as e 1 , . . . , e n . So, for instance the expression t(e 1 , . . . , e n ) could be also written as t e. Finally, given a sequence of expressions e and a function F on expressions, we use F ( e) to denote F (e 1 ), . . . , F (e n ), i.e. the componentwise application of F to the sequence e. For instance, given a sequence e = e 1 , • • • , e n , we use | e| as a notation for |e 1 |, . . . , |e n |.

Type system. As stressed before, we want to consider only expressions that are welltyped. 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 [START_REF] Frankau | Stream processing hardware from functional language specifications[END_REF]. 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:

Γ(x) = A Γ; ∆ x :: A (Var) Γ; ∆ Err :: A (A -Err) c :: A 1 → • • • → A n → A Γ; ∆ e i :: A i (1 ≤ i ≤ n) Γ; ∆ c(e 1 , . . . , e n ) :: A (Con) ∆(f) = A 1 → • • • → A n → A Γ; ∆ e i :: A i (1 ≤ i ≤ n) Γ; ∆ f(
, ; ∆, f : A 1 → • • • → A n → A e :: A Γ; ∆ f(x 1 , . . . , x n ) . = e :: A 1 → • • • → A n → A (Def) Γ; ∆ f(x 1 , . . . , x n ) . = e :: φ Γ; ∆, f :: φ e 1 :: A Γ; ∆ LetRec f(x 1 , . . . , x n )
. = e in e 1 :: A (Letrec)

σ ::= a | Nat | σ × σ (basic types) A ::= α | σ | A × A | [σ] (base types) φ ::= A | A → φ (types)
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

- → A → B as an abbrevi- ation for A 1 → • • • → A n → B.
The type system proves two kinds of typing judgments: Γ; ∆ e :: A for expressions, and Γ; ∆ f(x 1 , . . . , x n ) . = e :: φ 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 Γ and ∆ 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 ∅; ∅ 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 | c(x, . . . , 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 = Case y 1 of y 2 + 1 → Case y 2 of x + 1 → e
Instead of writing this in full form, we will simply write it as:

f ((x + 1) + 1) . = e
More generally, we will use the notation:

f p 1 1 • • • p 1 n . = e 1 . . . f p k 1 • • • p k n . = e k
as syntactic sugar for a function definition of the shape:

f(x 1 , • • • , x n ) . = Case x 1 of p 1 1 → . . . Case x n of p 1 n → e 1 . . . p k 1 → . . . Case x n of p k n → 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 10 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:

LetRec d 1 , . . . , d n in e
where d 1 , . . . , 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 [START_REF] Endrullis | Productivity of Stream Definitions[END_REF], we have:

Definition 7. • A function symbol f is a stream function if f :: [σ 1 ] → • • • → [σ n ] → - → τ → [σ],
with n > 0. Conversely, a function symbol

f is a stream constructor if f :: - → τ → [σ]. • A function definition d f such that f(x 1 , . . . , x n ) = e is a stream function defini- tion 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:

odd :: [a] → [a] odd (x : y : xs) . = x : (odd xs) nats :: Nat → [Nat] nats x . = x : (nats (x + 1)) zip :: [a] → [a] → [a] zip (x : xs) ys . = x : (zip ys xs) nodd :: [Nat] nodd . = odd (nats (0 + 1))
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).

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 [START_REF] Ong | Lazy lambda calculus: Theories, models and local structure characterization[END_REF][START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF], we identify a semantics that does not evaluate

c ∈ C H; c(e 1 , • • • , e n ) ⇓ c(e 1 , • • • , e n ) (val) H ∪ {d}; M ⇓ v H; LetRec d in M ⇓ v (rec) H; e{e 1 /x 1 , • • • , e n /x n } ⇓ v (f x 1 • • • x n . = e) ∈ H H; f(e 1 , • • • , e n ) ⇓ v (fun) H; e ⇓ c(e 1 , • • • , e m ) p i = c(x 1 , • • • , x m ) H; e i {e 1 /x 1 , • • • , e m /x m } ⇓ v H; Case e of p 1 → e 1 , . . . , p n → e n ⇓ v (pm) H; e ⇓ c(e 1 , • • • , e m ) ∀i ≤ n, p i = c(x 1 , • • • , x m ) H; Case e of p 1 → e 1 , . . . , p n → e n ⇓ Err (pm e )
Table 2: SFL lazy operational semantics under the constructors. So in particular, we do not consider the sharing issue that is studied in other lazy and call-by-need semantics [START_REF] Launchbury | A natural semantics for lazy evaluation[END_REF][START_REF] Ariola | The call-by-need lambda calculus[END_REF].

In order to describe the semantics, we need two additional components: substitutions and environments. A substitution {e 1 /x 1 , . . . , e n /x n } is a partial function mapping variables to expressions. As usual we denote e{e 1 /x 1 , . . . , e n /x n } the result of the application of the substitution {e 1 /x 1 , . . . , 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 H to denote environments. Definition 8. The operational evaluation relation ⇓ is the relation between environments, expressions and lazy values inductively defined by the rules in Table 2.

Intuitively, the judgment H; e ⇓ 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 H. For notational convenience, we simply write e ⇓ v for H; e ⇓ v when H = ∅. Moreover, in the sequel when we write H; e ⇓ v we implicitly assume that 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 A for every base type A as follows:

eval A :: A → A eval A (c x 1 • • • x n ) . = Ĉ (eval A1 x 1 ) • • • (eval An x n )
where Ĉ 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 Ĉ to be the function succ :: Nat → Nat defined as:

succ Err . = Err + 1 succ 0 . = 0 + 1 succ (x + 1) . = (x + 1) + 1
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 = {n | n = ((• • • (0 + 1) • • • ) + 1)
n times and n :: 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:

H, e ⇓ v v
to denote the judgment:

H, eval A e ⇓ 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:

!! :: [a] → Nat → a nil !! y . = Err (x : xs) !! 0 . = x (x : xs) !! (y + 1) . = xs !! y
We use the shorthand e n to denote the expression take n e where take is the usual function which returns the first n elements of a list:

take :: Nat → [a] → [a] take 0 s . = nil take (x + 1)
nil . = Err take (x + 1) (y : ys) . = y : (take x ys)

Finally, we use lg to denote the function that returns the number of elements in a finite partial list:

lg :: [a] → Nat lg nil . = 0 lg Err . = 0 lg (x : xs) . = (lg xs) + 1
In the sequel, we tacitly assume that the above definitions are contained in all the environments H that we will consider.

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 [START_REF] Manna | On the termination of Markov algorithms[END_REF][START_REF] Lankford | On proving term rewriting systems are noetherien[END_REF][START_REF] Bonfante | Algorithms with polynomial interpretation termination proof[END_REF], developed in the field of program termination, and by the notions of quasiinterpretation [START_REF] Bonfante | On lexicographic termination ordering with space bound certifications[END_REF] and sup-interpretation [START_REF] Marion | Sup-interpretations, a semantic method for static analysis of program resources[END_REF], 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 [START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF]). In Subsections 3.1 and 3.2, we define the notions of assignment and interpretation. These definitions are similar to the one on TRS ( [START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF]). 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.

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 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 ρ is a map associating to each x ∈ X a value r in R + .

• A symbol assignment, denoted ξ is a map associating to each symbol t ∈ C ∪ F a function F : R + × . . . × R + → R + of the same arity.

• Given a variable assignment ρ and a symbol assignment ξ, an assignment is the extension of ρ and ξ to expressions defined as follows:

-Err ρ,ξ = 0

-x ρ,ξ = ρ(x) -t(e 1 , . . . , e n ) ρ,ξ = ξ(t)( e 1 ρ,ξ , . . . , e n ρ,ξ ) -LetRec d in e ρ,ξ = e ρ,ξ
-Case e of c 1 (

x 1 ) → e 1 , . . . , c m ( x m ) → e m ρ,ξ = max 1≤i≤m { e i ρ{ xi= ri},ξ | r i ∈ R + and e ρ,ξ ≥ c i ( x i ) ρ{ xi= ri},ξ }
We consider variable and symbol assignments as total functions over program variables and program symbols, respectively. We write r ∈ R + as a shorthand for ∀r ∈ r, r ∈ R + , and we write ρ{x := r} for the variable assignment defined as ρ except for the variable x to which it assigns the value r. We often abbreviate ρ{x 1 := r 1 } • • • {x n := r n } by ρ{ x = 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 e i ρ{ xi= ri},ξ for 1 ≤ i ≤ m and for r ranging over values in R + . The existence of such an element (or equivalently a bound on the search space) is ensured by the side condition e ρ,ξ ≥ p i ρ{ xi= ri},ξ and by the fact that e does not contain the variables x. For each variable assignment ρ = {x := r, y := s} and symbol assignment ξ such that ξ(0) = 0, ξ(:

)(X, Y ) = X + Y + 1, ξ(+1)(X) = X + 1 and ξ(add)(X, Y ) = ξ(sadd)(X, Y ) = X + Y ,
we compute the assignment of the expression add x y as follows:

add x y ρ,ξ = ξ(add)( x ρ,ξ , y ρ,ξ ) = ρ(x) + ρ(y) = r + s
We compute the assignment of Case x of 0 → y, z + 1 → (add z y) + 1 in a similar way:

Case x of 0 → y, z + 1 → (add z y) + 1 ρ,ξ = max(max{ y ρ,ξ | x ρ,ξ ≥ 0 ρ,ξ }, max{ (add z y) + 1 ρ{z:=t},ξ | t ∈ R + and x ρ,ξ ≥ z + 1 ρ{z:=t},ξ }) = max(ρ(y), max{ρ(y) + ρ{z := t}(z) + 1 | t ∈ R + and ρ(x) ≥ ρ{z := t}(z) + 1}) = max(s, max r≥t+1 {s + t + 1}) as ρ(x) = r and ρ(y) = s = max(s, s + r) = r + s
The usual notion of assignment used in the context of interpretations does not distinguish between variable and symbol assignments. In our context, we prefer to keep this distinction because it highlights the extension of assignments to the Case construction 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ρ,ξ and an expression Γ, x :: A; ∆ e :: B, for every expression Γ; ∆ e :: A we have: 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 ξ is monotonic if for any t ∈ C ∪ F, ξ(t) is a monotonic function, i.e. ∀r, s ∈ R + s.t. r ≥ s: ξ(t)(. . . , r, . . .) ≥ ξ(t)(. . . , s, . . .)

• An assignmentρ,ξ is monotonic if the symbol assignment ξ 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 Case e of p 1 → e 1 , . . . , p m → e m ρ,ξ that is monotonic in e ρ,ξ and e i ρ,ξ but not in p i ρ,ξ .

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

Definition 11 (Almost-additive and Additive Assignment).

• The symbol assignment ξ is almost-additive if ∀c ∈ C of arity n but the stream constructor :, we have:

ξ(c)(r 1 , • • • , r n ) = n i=1
r i + α c , for some constant α c ≥ 1, whenever n > 0.

ξ(c) = 0, otherwise.

The symbol assignment ξ is additive if it is almost-additive and ξ(:)(r 1 , r 2 ) = r 1 + r 2 + α, for some constant α ≥ 1

• An assignmentρ,ξ is an almost-additive (resp. additive) assignment if the symbol assignment ξ 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ρ,ξ , there is a constant α such that for each strict value v :: A we have:

|v| ≤ v ρ,ξ ≤ α × |v|
Proof. We consider α = max c∈C α c and we prove the lemma by induction on the structure of v.

In the case v is a constructor c of arity 0, by definition we have |c| = 0 = c ρ,ξ , so the conclusion follows trivially.

Consider now the case v = c(v 1 , . . . , v n ). By induction hypothesis for 1 ≤ i ≤ n we have:

|v i | ≤ v i ρ,ξ ≤ α × |v i |
So, since by definition we also have:

|v| = ( 1≤i≤n |v i |) + 1 and v ρ,ξ = ( 1≤i≤n v i ρ,ξ ) + α c
and since α ≥ α c ≥ 1, using induction hypothesis we can conclude:

1≤i≤n |v i | + 1 ≤ 1≤i≤n v i ρ,ξ + α c ≤ 1≤i≤n (α × |v i |) + α c ≤ α × ( 1≤i≤n |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ρ,ξ such that the symbol assignment ξ is almostadditive, there is a constant α such that for every strict value v :: σ we have:

|v| ≤ v ρ,ξ ≤ α × |v|

Interpretations

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

Definition 12 (Interpretation). An expression Γ; ∆ e :: A admits an interpretation ξ if for each variable assignment ρ, the assignmentρ,ξ is monotonic and such that for each function definition f(x 1 , . . . , x n )

. = e the following holds:

f(x 1 , . . . , x n ) ρ,ξ ≥ e ρ,ξ
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, . . . to denote variables ranging over real numbers; e.g. we will write f ξ (X 1 , . . . , X n ) for f(x 1 , . . . , x n ) ξ . Analogously, we will write e ξ ≥ e ξ as a shorthands for: ∀ρ, e ρ,ξ ≥ e ρ,ξ .

In the sequel, we will need the following substitution property for interpretations. 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 H admits the interpretationξ if for every variable assignment ρ and every function definition f(x 1 , . . . , x n ) = e in it, the following holds:

f(x 1 , . . . , x n ) ρ,ξ ≥ e ρ,ξ
We can now show some examples.

Example 3. Consider again the environment H of Example 2. This environment admits an interpretationξ if the assignmentξ satisfies the following inequalities: Consider an additive assignmentξ such that 0 ρ,ξ = 0, : ρ,ξ (X, Y ) = X + Y + 1 and +1 ρ,ξ (X) = X + 1. Now, we are interested in finding an interpretation for the symbols add and sadd such that ρ = {x := r, y := s} satisfies the following inequalities: So, for instance we can choose ξ(add)(X, Y ) = ξ(sadd)(X, Y ) = X + Y (the first inequality is indeed proved to be an equality in Example 2). With this function symbol assignment ξ, since it is monotonic, we have thatξ is an interpretation.

add ρ,ξ (r, s) ≥ max(max{s | r ≥ 0}, max{1 + add ρ,ξ (t, s) | t ∈ R + and r ≥ t + 1})
Example 4. Consider the function symbol eval A for strict evaluation. The environment H that contains definitions of the shape:

eval A x . = Case x of (c x 1 • • • x n ) → Ĉ (eval A1 x 1 ) • • • (eval An x n ) will admit the interpretation -ξ defined by ξ(c)(X 1 , • • • , X n ) = ξ( Ĉ)(X 1 , • • • , X n ) = n i=1 X i + α c and ∀A, ξ(eval A )(X) = X.
Indeed, consider the assignmentρ,ξ for the environment ρ such that ρ(x) = r. On the one hand, we have eval

A (x) ρ,ξ = ξ(eval A )( x ρ,ξ ) = x ρ,ξ = ρ(x) = r. On the other hand, setting x = x 1 , • • • , x n and r = r 1 , • • • , r n : Case x of c x 1 • • • x n → Ĉ (eval A1 x 1 ) • • • (eval An x n ) ρ,ξ = max{ Ĉ(eval A1 x 1 ) • • • (eval An x n ) ρ{ x= r},ξ | x ρ,ξ ≥ c x 1 • • • x n ρ{ x= r},ξ } = max{ξ( Ĉ)( eval A1 x 1 ρ{ x= r},ξ , • • • , eval An x n ρ{ x= r},ξ ) | r ≥ ξ(c)( x 1 ρ{ x= r},ξ , • • • , x n ρ{ x= r},ξ )} = max{ n i=1 r i + α Ĉ | r ≥ n i=1 r i + α Ĉ} ≤ r
This inequality holds for an arbitrary value r and, consequently, for every environment ρ. So,ξ is an interpretation of H.

Throughout the paper, we will fix the assignment of the eval A function symbol by setting ∀A, ξ(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 H and ∅; ∆ e :: A be an environment and an expression admitting both the interpretationξ . Then:

H, e ⇓ v implies e ξ ≥ v ξ
Proof. By induction on the derivation proving H, e ⇓ 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:

H; e{e 1 /x 1 , • • • , e n /x n } ⇓ v (f x 1 • • • x n = e) ∈ H H; f(e 1 , • • • , e n ) ⇓ v
By induction hypothesis, we have e{e 1 /x Let us consider the case where the derivation ends with: Since this holds for every ρ, the conclusion easily follows by the definition of interpretation.

H; e ⇓ c(e 1 , • • • , e m ) p i = c(x 1 , • • • , x m ) H; e i {e 1 /x 1 , • • • , e m /x m } ⇓ v H;
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 H and ∅; ∆ e :: A be an environment and an expression admitting both the interpretationξ . Then:

H, e ⇓ v v implies e ξ ≥ v ξ
Proof. The notation H, e ⇓ v v is just a shorthand for H, eval A e ⇓ v, so the conclusion follows directly using Proposition 1 and the fact that we consider assignments such that ξ(eval A )(X) = X.

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ξ be an interpretation. Then, there exists a function F : R + → R + such that for every program e :: A admittingξ :

e ξ ≤ F (|e|)
Proof. By induction on the shape of e.

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.

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 -l ξ where l ∈ 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 ξ l is a map associating to each symbol t ∈ C ∪ F and l ∈ R a function F l : R + × . . . × R + → R + of the same arity.

• Given a variable assignment ρ, a parametrized symbol assignment ξ l , a parame--trized assignment -l ξ is the extension of ρ and ξ l to expressions defined as follows: The definitions given for interpretations can be easily adapted to the case of parametrized interpretations.

-Err l ρ,ξ = 0 -x l ρ,ξ = ρ(x) -
Definition 15 (Monotonic Parametrized Assignment). A parametrized assignment is monotonic if for any t ∈ C ∪F, ξ(t) is a monotonic function, i.e. ∀r, s ∈ R + s.t. r ≥ s and ∀l, l ∈ R s.t. l ≥ l : ξ l (t)(. . . , r, . . .) ≥ ξ l (t)(. . . , s, . . .) Definition 16 (Almost-additive and Additive Parametrized Assignment).

• The parametrized symbol assignment ξ l is almost-additive if ∀c ∈ C of arity n but the stream constructor : we have:

ξ l (c)(r 1 , • • • , r n ) = n i=1
r i + α c , for some constant α c ≥ 1, whenever n > 0.

ξ l (c) = 0, otherwise.

The parametrized symbol assignment ξ l is additive if it is almost-additive and ξ l (:)(r 1 , r 2 ) = r 1 + r 2 + α, for some constant α ≥ 1

• A parametrized assignment -l ρ,ξ is an almost-additive (resp. additive) assignment if the parametrized symbol assignment ξ 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 -l ρ,ξ and an expression Γ, x :: A; ∆ e :: B, for every expression Γ; ∆ e :: A and every l ∈ R we have:

e l ρ{x:= e l ρ,ξ },ξ ≥ e{e /x} 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: and so the conclusion follows. The other cases can be obtained similarly.

We are now ready to define parametrized interpretations.

Definition 17 (Parametrized Interpretation

). An expression Γ; ∆ e : A admits a parametrized interpretation -l ξ if for each variable assignment ρ, the assignment l ρ,ξ is monotonic and such that for each function definition f(x 1 , . . . , x n )

. = e and for each l ∈ R the following holds:

f(x 1 , . . . , x n ) l ρ,ξ ≥ e l ρ,ξ
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 e l ξ ≥ e l ξ as a shorthand for ∀ρ, e l ρ,ξ ≥ e 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 H, e ⇓ k v be the relation defined in Figure 3. H, e ⇓ k v means that H, e ⇓ v holds using exactly k pattern matching rules on streams for producing v. We define ⇓ k v in the same manner: ). So we have:

H, e ⇓ k v v if H, eval A e ⇓ k v. c ∈ C H; c(e 1 , • • • , e n ) ⇓ 0 c(e 1 , • • • , e n ) H ∪ {d}; M ⇓ k v H; LetRec d in M ⇓ k v H; e{e 1 /x 1 , • • • , e n /x n } ⇓ k v (f x 1 • • • x n . = e) ∈ H H; f(e 1 , • • • , e n ) ⇓ k v H; e ⇓ k c(e 1 , • • • , e m ) p i = c(x 1 , • • • , x m ) H; e i {e 1 /x 1 , • • • , e m /x m } ⇓ k v H;
max{ e 1 l ρ{x1=r1,x2=r2},ξ | e l ρ,ξ ≥ x 1 : x 2 l ρ{x1=r1,x2=r2},ξ } ≥ e 1 l ρ{x1= e 1 l-k ρ,ξ ,x2= e 2 l-k-1 ρ,ξ },ξ
By monotonicity we have:

e 1 l ρ{x1= e 1 l-k ρ,ξ ,x2= e 2 l-k-1 ρ,ξ },ξ ≥ e 1 l-k-1 ρ{x1= e 1 l-k-1 ρ,ξ ,x2= e 2 l-k-1 ρ,ξ },ξ
Finally, by applying Lemma 5 twice we have:

e 1 l-k-1 ρ{x1= e 1 l-k-1 ρ,ξ ,x2= e 2 l-k-1 ρ,ξ },ξ ≥ e 1 {e 1 /x 1 , e 2 /x 2 } l-(k+1) ρ,ξ
By induction hypothesis we have e

1 {e 1 /x 1 , e 2 /x 2 } l-(k+1) ξ ≥ v l-(k+1)-k ξ
, so the conclusion follows.

Since this holds for every ρ and every l ∈ R, the conclusion easily follows by definition of parametrized interpretation.

Corollary 3. Let H and ∅; ∆ e :: A be an environment and an expression both admitting the parametrized interpretation -l ξ . Then:

H, e ⇓ k v v implies e l ξ ≥ v l-k ξ Proof.
Just check that we can define a parametrized interpretation of eval A by setting ∀l ∈ R, ∀A, ξ l (eval A )(X) = X as in Corollary 2.

Lemma 6. Let -l ξ be a parametrized interpretation. Then, there exists a function G : R + × R + → R + such that for every program e :: A admitting -l ξ and every l ∈ R + : There are two possibilities depending on the shape of t. If t = : , that is e = e 1 : e 2 , then by induction hypothesis, definition and monotonicity of F we have:

e l ξ ≤ G(|e|, l) Proof. Define: F (X, L) = max( max t∈C∪F t L ξ (X, . . . , X), X) and F n+1 (X, L) = F (F n (X, L), L) and F 0 (X, L) = F (X, L).
e l ξ = ξ l (t)( d 1 l ξ , . . . , d n l ξ ) ≤ ξ l (t)(F |d1| (|d 1 |, l), . . . , F |dn| (|d n |, l)) ≤ ξ l (t)(F |dj | (|d j |, l), . . . , F |dj | (|d j |, l)) ≤ F (F |dj | (|d j |, l), l) ≤ F |dj |+1 (|d j |, l) ≤ F |e| (|e|, l)
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:

e l ξ = e 1 : e 2 l ξ = ξ l (:)( e 1 l ξ , e 2 l-1 ξ ) ≤ ξ l (:)(F |e1| (|e 1 |, l), F |e2| (|e 2 |, l -1)) ≤ ξ l (:)(F |e1| (|e 1 |, l), F |e2| (|e 2 |, l)) ≤ F |e| (|e|, l)
We let the reader checking the other cases of the induction including the technical but simple case where e = Case e of c 1 ( x 1 ) → e 1 , . . . , c m ( x m ) → e m . Now the conclusion follows easily by taking G(X, L) = F X (X, L).

Space Upper Bounds

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 s 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:

• • • |v i | ≤ ∞ max r=0 |v r | = k v i • • • v 1 e v 1 • • • |v j | ≤ F (k, j) v j • • • Figure 1: Local Upper Bound
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 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 : R + → R + witnessing these bounds.

Illustrating examples

A typical situation where programs have a local upper bound is described in the following example: is not globally bounded but if we evaluate the n-th output stream element as H; e n ⇓ v v, then we know that the size of v is bounded by 12 + 3 × n. Consequently, this program has a local upper bound given by the function F (X) = 12 + 3 × X applied to the index n.

A typical situation where programs have a global upper bound is described in the following example.

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.

Definition

More formally, we can describe the situations outlined above using the formal framework presented in Section 2 as follows. Clearly, nats e produces a stream whose elements are of unbounded size. However it is easy to verify that ∀n ∈ N, if H;

Definition 18 (Local and Global Upper Bounds). A stream program e

:: [σ] has a local upper bound if there is a function F ∈ R + → R + such that: ∀n ∈ N, if H; e n ⇓ v v then F (|n|) ≥ |v|
(nats e) n ⇓ v then v = ((e +1) + • • • ) + 1 n times .
Consequently, by taking F (X) = 2×X, the following inequalities are satisfied ∀n ∈ N:

|v| = |n| + |e| ≤ 2 × max(|n|, |e|) = F (max(|n|, |e|))
Example 8. Consider the program ones defined as:

ones . = 1 : ones
Clearly, it has an obvious global upper bound (K = 1). Analogously, consider the program repeat n for every n ∈ Nat where:

repeat x . = x : (repeat x)
Clearly, repeat n has a global upper bound that can be given by the function F (X) = X. That is, for every n we have a constant K n = F (|n|) = |n|. In the same spirit, going back to Equation 1 of Example 6, the function F (X) = max(256, X 4 ) provides for every input stream s of data of size bounded by k a constant K s = max(256, k 4 ).

LUB and GUB criteria

To ensure a Local Upper Bound we present a combined criterion consisting in a semantic condition on programs and in a semantic condition on interpretations.

Concerning the criterion on programs, we need to identify a restricted class of programs that we dub linear programs. These are programs that produce outputs with only a linear number of reads (stream pattern matchings in our concern). We can define them formally as follows.

Definition 19 (Linear program). Let ↓ k and ↓ k v be the relations defined by H; e ↓ k v if there exists k ≤ k such that H; e ⇓ k v and H; e ↓ k v v if there exists k ≤ k such that H; e ⇓ k v v, respectively. A program e :: [σ] is linear if there is a k ≥ 1 such that for all n ∈ N, H; e n ↓ k×(|n|+1) v v holds. The constant k is called the linearity constant. Now we are ready to define our criterion.

Definition 20 (LUB Criterion).

A program e :: [σ] is LUB if it is linear and it admits a parametrized interpretation -l ξ that is almost-additive and such that:

ξ l (:)(X, Y ) = max(X, Y )
Now we can provide a similar criterion for Global Upper Bound:

Definition 21 (GUB Criterion). A program e :: [σ] is GUB if it admits an interpretationξ that is almost-additive and such that:

ξ(:)(X, Y ) = max(X, Y )
e k-k ξ ≥ v k-k -k ξ ≥ v 0 ξ
Now we prove the induction step for n + 1 = n. Suppose that H; e n ↓ k×(|n|+1) v v. It is easy to verify that necessarily H; e ⇓ j e : e and H; e n ⇓ v v for some j, j < k. By applying Proposition 2 we have: We can now prove the main result of this section. 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 -l ρ,ξ defined by: ξ l (nats)(X) = X + l, ξ l ( + 1)(X) = X + 1, ξ l (0) = 0 and ξ l (:)(X, Y ) = max(X, Y ). We check that ∀l ∈ R:

nats x l ρ,ξ = nats l ρ,ξ ( x l ρ,ξ ) = ρ(x) + l ≥ max(ρ(x), (ρ(x) + 1) + (l -1)) = max( x l ρ,ξ , nats(x + 1) l-1 ρ,ξ ) = x : (nats (x + 1)) l ρ,ξ
The interpretation -l ρ,ξ clearly respects the required criterion for nats to be LUB. That is, it is almost-additive and it is defined on : as ξ l (:)(X, Y ) = max(X, Y ). So, nats admits a local upper bound. We obtain the required bound by setting 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ρ,ξ defined by:

F (X) = nats(m) X ρ,ξ = X + m ρ,ξ = X + |m|, for all canonical numerals m, n ∈ N such that (nats m) !! n ⇓ v v n , the following holds F (|n|) ≥ |n| + |m| ≥ |v n | (Indeed for all n, v n = m + n).
ξ l (0) = 0, ξ l (+1)(X) = X + 1, ξ l (:)(X, Y ) = max(X, Y ), ξ l (sadd)(X, Y ) = ξ l (add)(X, Y ) = X + Y , ξ l (tail)(X) = X and ξ l (fib) = 2 l .
For the first rule and for each l ∈ R, the following inequalities are satisfied:

fib l ξ = 2 l ≥ max(0, 1, 2 × 2 l-2 ) = max( 0 l ξ , max( 1 l-1 ξ , 2 × fib l-2 ξ )) = max( 0 l ξ , max( 1 l-1 ξ , sadd fib (tail fib) l-2 ξ )) = max( 0 l ξ , 1 : sadd fib (tail fib) l-1 ξ ) = 0 : (1 : sadd fib (tail fib)) l ξ
We let the reader check the inequalities for the other definitions. So, we have that -l ρ,ξ respects the required criterion for fib to be LUB. That is, it is almost-additive and it is defined on : as ξ 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 n ∈ N s.t. fib !! n ⇓ v v n , the inequality 2 4×(|n|+1) ≥ |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. The morse program is GUB with respect to the following interpretation:

0 ξ = 0, +1 ξ (X) = 1 + X, : ξ (X, Y ) = ξ = max(X, Y ), inv ξ (X) = max(1, X),
tail ξ (X) = X and morse ξ = 1. For instance, for the first rule the following inequality is satisfied:

morse ξ = 1 ≥ max(0, 1 , 1, 1)
= max( 0 ξ , max(1, morse ξ , morse ξ )) = max( 0 ξ , max( inv morse ξ , tail morse ξ )) = max( 0 ξ , (zip (inv morse) (tail morse)) ξ ) = 0 : (zip (inv morse) (tail morse)) ξ

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 ρ,ξ defined by:

0 ξ = 0 +1 ξ (X) = X + 1 add ξ (X, Y ) = X + Y zip ξ (X, Y ) = ξ(:)(X, Y ) = max(X, Y ) square ξ (X) = X 2 mul ξ (X, Y ) = X × Y repeat ξ (X) = X
Indeed, we can check the inequalities of the interpretation is satisfied for every definition and for every variable assignment ρ. For the definition of repeat we have:

repeat x ρ,ξ = repeat ξ ( x ρ,ξ ) = ρ(x) ≥ max(ρ(x), ρ(x)) = ξ(:)( x ρ,ξ , repeat x ρ,ξ ) = x : (repeat x) ρ,ξ
For the definition of zip: zip z ys . = Case z of (x : xs) → x : (zip ys xs)

we check the following inequality: and we obtain that for all n ∈ N such that H, e n ⇓ v v n , 7 4 ≥ |v n |.

zip z ys ρ,ξ = max(ρ(z), ρ(ys)) ≥ max{max(u, v, ρ(ys)) | ∀u, v ∈ R + s.t. ρ(z) ≥ max(u, v)} = max{ x : (zip ys xs) ρ[x=u,xs=v],ξ | ∀u, v ∈ R + s.t. z ξ ≥ x : xs ρ[x=u,

Bounded Input/Output Properties

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. 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, | v|) on j with respect to i and | 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 | 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).

• • • i v i • • • v 1 e j ≤ F (i, | v|) v 1 • • • v j • • •
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 [START_REF] Bird | Introduction to Functional Programming[END_REF].

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(v) be a notation for e(x){v/x} and, finally, define e ρ,ξ (r) by e ρ,ξ (r) = e(x) ρ{x=r},ξ .

Illustrating examples

A typical situation where programs have a length based Input/Output upper bound is described in the following example: 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:

dup (merge (dup s) (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 × 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: • An interpretationρ,ξ is LBUB ifρ,ξ is almost-additive with ξ(+1)(X) = X + 1 and such that:

app :: [a] → [a] → [
∀ n ∈ N, if H; s n ⇓ v v
ξ(:)(X, Y ) = Y + 1 (resp. X + Y + 1) • An interpretation -ρ,ξ is SBUB if -ρ,ξ is additive with ξ(+1)(X) = X + 1 and: ξ(:)(X, Y ) = X + Y + 1
• An expression x :: [σ] e(x) :: [τ ] is LBUB (resp. SBUB) if it admits an interpretationξ such thatρ,ξ is LBUB (resp. SBUB).

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ρ,ξ , for every n :: Nat we have n ρ,ξ = |n|.

Proof. By induction on the length of n. The base case follows easily by additivity of ρ,ξ . That is |0| = 0 ρ,ξ = 0. Consider now the case n + 1. We have n + 1 ρ,ξ = +1 ρ,ξ ( n ρ,ξ ) = n ρ,ξ + 1. By induction hypothesis n ρ,ξ = |n| and so the conclusion follows.

Second, the interpretation of a finite list is equal to its length: Lemma 9. Given a LBUB assignmentρ,ξ , for every v ::

[σ] we have if H; lg v ⇓ v m then v ρ,ξ = |m|.
Proof. By induction on the length of v. The base case follows easily by almostadditivity ofρ,ξ . That is |0| = nil ρ,ξ = 0 since H; lg nil ⇓ v 0. Consider now the case v 1 : v 2 and suppose that H

; lg (v 1 : v 2 ) ⇓ v m + 1. We have v 1 : v 2 ρ,ξ = ξ(:)( v 1 ρ,ξ , v 2 ρ,ξ ) = v 2 ρ,ξ + 1. Moreover, H; lg v 2 ⇓ v
m and, by induction hypothesis, v 2 ρ,ξ = |m| and so the conclusion follows.

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 soundess 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 H admits the interpretationρ,ξ and thatρ,ξ is a LBUB or SBUB assignment. Then,ρ,ξ can be extended to the function symbol lg by setting ξ(lg)(X) = X in such a way that the environment {lg y = Case y of nil → 0, Err → 0, x : xs → (lg xs) + 1} ∪ H admits the interpretationρ,ξ .

Proof. Consider the definition {lg y . = Case y of nil → 0, Err → 0, x : xs → (lg xs) + 1}. We have to check that the extension ofρ,ξ still satisfies the inequalities of an interpretation for this definition:

lg y ρ,ξ = ρ(y) = r ≥ max(0, r) = max(max{ 0 ρ,ξ | r ≥ nil ρ,ξ }, max{ 0 ρ,ξ | r ≥ Err ρ,ξ }, max{ (lg xs) + 1 ρ[x:=u,xs:=v],ξ | ∀u, v s.t. r ≥ v + 1}) = Case y of nil → 0, Err → 0, x : xs → (lg xs) + 1 ρ,ξ
This inequality holds for every ρ such that ρ(y) = r, for an arbitrary r ≥ 0, and so the conclusion.

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. By definition, we obtain e(v) ρ,ξ = e ρ,ξ ( v ρ,ξ ). Moreover, by Lemma 2, since ξ is additive we have a constant α such that v ρ,ξ ≤ |v| × α. So, taking F (X) = e ρ,ξ (X × α), the conclusion follows.

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. 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:

ξ(merge)(X, Y ) = max(X, Y ) ξ(dup)(X) = 2X
As an example, for each s we have: 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:

ξ(nil) = 0 ξ = 0 ξ(+1)(X) = X + 1 ξ(:)(X, Y ) = X + Y + 1 ξ(app)(X, Y ) = X + Y ξ(upto)(X) = ξ(extendupto)(X) = 2 × X 2
In particular, by taking F (X) = extendupto ξ ( extendupto ξ (X)) we obtain a size based upper bound for the expression:

extendupto (extendupto s)
That is F (X) = 8 × 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.

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 F, is an interpretation for M using only functions in F computable?

The ability of being able to compute an interpretation clearly depends on the class of functions 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 [START_REF] Péchoux | Synthesis of sup-interpretations: A survey[END_REF] 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 [START_REF] Péchoux | Synthesis of sup-interpretations: A survey[END_REF]).

It is worth noting that this problem has also been studied by the rewriting community both from theoretical and practical points of view [START_REF] Lucas | Polynomials over the reals in proofs of termination: from theory to practice[END_REF][START_REF] Korp | Tyrolean termination tool 2[END_REF].

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 [START_REF] Frankau | Stream processing hardware from functional language specifications[END_REF] 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. Analogously, Hughes et al. in their paper introducing sized types [START_REF] Hughes | Proving the correctness of reactive systems using sized types[END_REF] show how the latter can be used to prevent errors related to memory leaks and buffer overflows of embedded 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 [START_REF] Shkaravska | Collected Size Semantics for Functional Programs over Polymorphic Nested Lists[END_REF], 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 [START_REF] Burrell | Pola: a language for PTIME programming[END_REF] 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 programmer to deal with polynomial time functional programs working both on inductive and coinductive data types.

In [START_REF] Leivant | Implicit complexity for coinductive data: a characterization of corecurrence[END_REF], Leivant and Ramyaa have proposed a framework based on equational programs and intrinsic theories, previously introduced by Leivant in [START_REF] Leivant | Intrinsic theories and computational complexity[END_REF], that is useful to reason about programs over inductive and co-inductive types. They used such a framework to obtain an implicit characterization of primitive corecurrence (a weak form of productivity). More recently, in [START_REF] Ramyaa | Ramified corecurrence and logspace[END_REF] 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 working 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. [START_REF] Férée | Interpretation of stream programs: characterizing type 2 polynomial time complexity[END_REF] show that interpretations can be used on stream programs also to characterize type 2 polynomial 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 [START_REF] Cook | Functional interpretations of feasibly constructive arithmetic[END_REF].

Recently, Baillot and Dal Lago [START_REF] Baillot | Higher-Order Interpretations and Program Complexity[END_REF] have developed a technique inspired by quasiinterpretations 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.

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.

  ones :: [Nat] ones . = 1 : ones nats :: Nat → [Nat] nats x . = x : (nats (x + 1))

  Patterns) e ::= x | c(e, . . . , e) | f(e, . . . , e) | LetRec d in e | (Expressions) Case e of p → e, . . . , p → e d ::= f(x, . . . , x) . = e (Definitions) v ::= c(e, . . . , e) (Lazy Values) v ::= c(v, . . . , v) (Strict Values)

Example 2 .

 2 Consider the following function definitions: add :: Nat → Nat → Nat add 0 y . = y add (z + 1) y . = (add z y) + 1 sadd :: [Nat] → [Nat] → [Nat] sadd (x : xs) (y : ys) . = (add x y ) : (sadd xs ys) Concretely, in SFL they can be computed by the environment H including the following definitions: add x y . = Case x of 0 → y, z + 1 → (add z y) + 1 sadd x y . = Case x of x : xs → Case y of y : ys → (add x y ) : (sadd xs ys)

  e{e /x} ρ,ξ = e ρ{x:= e ρ,ξ },ξ 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 1 , . . . , e n ), by definition we have e{e /x} ρ,ξ = ξ(t)( e 1 {e /x} ρ,ξ , . . . , e n {e /x} ρ,ξ ). By induction hypothesis, e i {e /x} ρ,ξ = e i ρ{x:= e ρ,ξ },ξ for each 1 ≤ i ≤ n. So, we can conclude: e{e /x} ρ,ξ = ξ(t)( e 1 {e /x} ρ,ξ , . . . , e n {e /x} ρ,ξ ) = ξ(t)( e 1 ρ{x:= e ρ,ξ },ξ , . . . , e n ρ{x:= e ρ,ξ },ξ ) = e ρ{x:= e ρ,ξ },ξ Consider the case e = Case e of c 1 ( y 1 ) → e 1 , . . . , c n ( y n ) → e n , then by definition, for x / ∈ y 1 , . . . , y n (because x is supposed to be free in e), we have: e{e /x} ρ,ξ = max 1≤i≤m { e i {e /x} ρ{ yi:= ri},ξ | e {e /x} ρ,ξ ≥ c i ( y i ) ρ{ yi:= ri},ξ } By induction hypothesis, we obtain: { e i {e /x} ρ{ yi:= ri},ξ | e {e /x} ρ,ξ ≥ c i ( y i ){e /x} ρ{ yi:= ri},ξ } = { e i ρ{ y:= r,x:= e ρ,ξ },ξ | e ρ{x:= e ρ,ξ },ξ ≥ c i ( y i ) ρ{ y:= r,x:= e ρ,ξ },ξ } and so we can conclude e{e /x} ρ,ξ = e ρ{x:= e ρ,ξ },ξ .

Lemma 3 (

 3 Interpretation Substitution). Let Γ; ∆ e :: A and Γ, x :: A; ∆ e 1 , e 2 :: B be expressions admitting the interpretationξ and such that e 1 ξ ≥ e 2 ξ . Then: e 1 {e/x} ξ ≥ e 2 {e/x} ξ Proof. By definition of interpretation we have ∀ρ, e 1 ρ,ξ ≥ e 2 ρ,ξ . Thanks to the quantification over all the variable assignments we also have ∀ρ, e 1 ρ{x:= e ρ,ξ },ξ ≥ e 2 ρ{x:= e ρ,ξ },ξ . So, by applying Lemma 1, we can conclude ∀ρ, e 1 {e/x} ρ,ξ ≥ e 2 {e/x} ρ,ξ .

  add x y ξ ≥ Case x of 0 → y, z + 1 → (add z y) + 1 ξ sadd x y ξ ≥ Case x of x : xs → Case y of y : ys → (add x y ) : (sadd xs ys) ξ

  sadd ρ,ξ (r, s) ≥ max{ Case y of y : ys → (add x y ) : (sadd xs ys) ρ{x :=v,xs:=x},ξ | x, v ∈ R + and r ≥ v + x + 1} The above can be reformulated as follows: add ρ,ξ (r, s) ≥ max {t∈R + | r≥t+1} (s, 1 + add ρ,ξ (t, s)) sadd ρ,ξ (r, s) ≥ max{ (add x y ) : (sadd xs ys) ρ{x :=v,xs:=x,y :=w,ys:=y},ξ | x, y, v, w ∈ R + and r ≥ v + x + 1 and s ≥ w + y + 1} ≥ max{ add ρ,ξ (v, w) + sadd ρ,ξ (x, y) + 1 | x, y, v, w ∈ R + and r ≥ v + x + 1 and s ≥ w + y + 1}

Case e of p 1 →

 1 e 1 , . . . , p n → e n ⇓ v By induction hypothesis, we have both e i {e 1 /x 1 , • • • , e m /x m } ξ ≥ v ξ and e ξ ≥ c(e 1 , • • • , e m ) ξ . Consider an arbitrary variable assignment ρ. Applying Lemma 1 several times, we have c(e 1 , • • • , e m ) ρ,ξ = c(x 1 , • • • , x m ) ρ ,ξ for ρ = ρ{x 1 := e 1 ρ,ξ , • • • , x m := e m ρ,ξ }. By definition of assignment we have: Case e of p 1 → e 1 , . . . , p n → e n ρ,ξ ≥ e i ρ ,ξ and by some applications of Lemma 1: Case e of p 1 → e 1 , . . . , p n → e n ρ,ξ ≥ e i ρ ,ξ = e i {e 1 /x 1 , • • • , e m /x m } ρ,ξ

e 1 : e 2 l 1 l-

 21 ) t(e 1 , . . . , e n ) l ρ,ξ = ξ l (t)( e Case e of c 1 ( x 1 ) → e 1 , . . . , c m ( x m ) → e ri},ξ | r i ∈ R + and e l ρ,ξ ≥ c i ( x i ) l ρ{ xi= ri},ξ }

e 1 : e 2 l 1 l

 21 ρ{x:= e l ρ,ξ },ξ = ξ l (:)( e },ξ ) ≥ ξ l (:)( e 1 l ρ{x:= e l ρ,ξ },ξ , e 2 l-1 ρ{x:= e l-1 ρ,ξ },ξ )Since by induction hypothesis we have:ξ l (:)( e 1 l ρ{x:= e l ρ,ξ },ξ , e 2 l-1 ρ{x:= e l-1 ρ,ξ },ξ ) ≥ ξ l (:)( e 1 {e /x} l ρ,ξ , e 2 {e /x} l-1 ρ,ξ )and since by definition:ξ l (:)( e 1 {e /x} l ρ,ξ , e 2 {e /x} l-1 ρ,ξ ) = (e 1 : e 2 ){e /x} l ρ,ξ the conclusion follows. Consider now the case e = Case e of c 1 ( x 1 ) → e 1 , . . . , c m ( x m ) → e m . Then, by definition we have: e l ρ{x:= e l ρ,ξ },ξ = max 1≤i≤m { e i l ρ{ xi= ri}{x:= e l ρ,ξ },ξ | e l ρ{x:= e l ρ,ξ },ξ ≥ c i ( x i ) l ρ{ xi= ri},ξ } since clearly x is disjoint from the variables in x i . By induction hypothesis we can show that: max 1≤i≤m { e i l ρ{ xi= ri}{x:= e l ρ,ξ },ξ | e l ρ{x:= e l ρ,ξ },ξ ≥ c i ( x i ) l ρ{ xi= ri},ξ } ≥ max 1≤i≤m { e i {e /x} l ρ{ xi= ri},ξ | e {e /x} l ρ,ξ ≥ c i ( x i ) l ρ{ xi= ri},ξ }

Case e of x 1 : x 2 → e 1 , nil → e 2 lρ,ξ ≥ max{ e 1 l 1 l-k ρ,ξ and r 2 = e 2 l

 1212112 ρ{x1=r1,x2=r2},ξ | r 1 , r 2 ∈ R + and e l ρ,ξ ≥ x 1 : x 2 l ρ{x1=r1,x2=r2},ξ }By induction hypothesis, we can satisfy the side condition in the max by setting r 1 = e

  It can be shown by induction on the structure of e that e l ξ ≤ 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 e l ξ ≤ F (|e|, l). Now, consider e = t d 1 • • • d n and suppose |d j | = max n i=1 |d i |. By induction hypothesis, d i l ξ ≤ F |di| (|d i |, l).

Example 5 .

 5 Consider expressions built using the following definitions already presented in Example 2: add :: Nat → Nat → Nat add 0 y . = y add (z + 1) y . = (add z y) + 1 sadd :: [Nat] → [Nat] → [Nat] sadd (x : xs) (y : ys) . = (add x y ) : (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 = sadd (nats 3) (sadd (nats 5) (nats 4))

Example 6 . 0

 60 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 . = 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: square (zip (repeat 5) (square (zip x (repeat 4))))

Example 7 .

 7 In the case the function F is constant, then e :: [σ] 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. Consider again the stream definition of nats: nats :: Nat → [Nat] nats x . = x : (nats (x + 1))

4. 5 .Lemma 7 . 1 . 2 .

 5712 Soundness Now we want to show that if a given program e :: [σ] is LUB (resp. GUB) then it has a local (resp. global) upper bound. For that purpose, we first show an intermediate technical lemma. Given an expression e :: [σ]: If e is a GUB program then ∀n ∈ N, s.t. H; e n ⇓ v v we have: e ξ ≥ v ξ If e is a LUB program of linearity constant k then ∀n ∈ N, s.t. H; e n ⇓ v v we have: e k×(|n|+1) ξ ≥ v 0 ξ Proof. (1) We proceed by induction on n ∈ N. Let n = 0 and H; e 0 ⇓ v v. Then, necessarily we have a value v such that H; e ⇓ v . We have three cases, either v = Err or v = 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 ξ ≥ e : e ξ = : ξ ( e ξ , e ξ ) ≥ e ξ Since we clearly have H; e ⇓ v v, by applying Corollary 1 we obtain e ξ ≥ v ξ . So by transitivity we can conclude e ξ ≥ v ξ . Now, let n = n + 1 and H; e (n +1) ⇓ v. Again we have a value v such that H; e ⇓ v . The case v = Err is trivial. So, consider the case v = e : e . Again by definition of GUB and by Proposition 1 we have: e ξ ≥ e : e ξ = : ξ ( e ξ , e ξ ) ≥ e ξ Moreover H; e (n +1) ⇓ v v implies by definition that H; e n ⇓ v v and by induction hypothesis we have e ξ ≥ v ξ . So we can conclude e ξ ≥ v ξ . (2) Assume that e :: [σ] is a LUB program of linearity constant k. We proceed by induction on n ∈ N. Consider the base case where n = 0. By assumption, we have H; e 0 ⇓ v v and, necessarily we have a value v such that H; e ⇓ v . We have three cases, either v = Err or v = 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 H; e ⇓ k e : e , for some e such that H; e ⇓ k v v with k + k ≤ k. Consequently, by Proposition 2 we have: e k×(|0|+1) ξ = e k ξ ≥ e : e k-k ξ By definition it is easy to verify that: e : e k-k ξ ≥ e k-k ξ and by Corollary 3 and monotonicity (since k + k ≤ k) we obtain:

  By definition it is easy to verify that:e : e (|n|+1)×k-j ξ ≥ e (|n|+1)×k-(j+1) ξ and since j + 1 ≤ k, by monotonicity: e (|n|+1)×k-(j+1) ξ ≥ e k×(|n |+1) ξ Now, applying induction hypothesis we have: e k×(|n |+1) ξ ≥ v 0 ξ and so the conclusion follows.

Theorem 1 .Example 9 .

 19 If a program is LUB (GUB) then it admits a local (global) upper bound. Proof. Consider a LUB program e :: [σ] wrt the parametrized interpretation -l ξ . By Lemma 6, there is a function G : R + ×R + → R + such that ∀l ∈ R + , G(|e|, l) ≥ e l ξ . Let us take F (X) = G(|e|, k×(X+1)) , k being the linearity constant of e, and assume for n ∈ Nat that e n ⇓ v v. By Lemma 7(2), we have e k×(|n|+1) ξ ≥ v 0 ξ . Moreover, since -0 ξ has a fixed parameter, it corresponds to an almost-additive interpretation. So, by Corollary 1 we have v 0 ξ ≥ |v|. Summing up, we have: F (|n|) = G(|e|, k × (|n| + 1)) ≥ e k×(|n|+1) ξ ≥ v 0 ξ ≥ |v| and so the conclusion follows. Now consider a GUB program e :: [σ]. By Lemma 4 there is a function F : R + → R + such that F (|e|) ≥ e ξ . Let us take K = F (|e|) and assume for n ∈ Nat that H; e n ⇓ v v. By Lemma 7(1) we have e ξ ≥ v ξ . Moreover, by Corollary 1 we have v ξ ≥ |v|, since such that ξ is an almost-additive symbol assignment. So, summing up, we have: K = F (|e|) ≥ e ξ ≥ v ξ ≥ |v| and the conclusion follows. 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. Consider again the stream definition of nats of Example 1: nats :: Nat → [Nat] nats x . = x : (nats (x + 1))

Example 10 (

 10 Fibonacci). The following example computes the Fibonacci sequence: tail :: [a] → a tail x : xs . = xs fib :: [Nat] fib . = 0 : (1 : (sadd fib (tail fib)))

Example 11 (

 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

2 =

 2 xs=v],ξ } = Case z of (x : xs) → x : (zip ys xs) ρ,ξ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 = square (zip (repeat 5) (square (zip (repeat 7) (repeat 4)))) admits a global upper bound that is equal to: e ρ,ξ = zip (repeat 5) (square (zip (repeat 7) (repeat 4))) 2 ρ,ξ = (max( repeat 5 ρ,ξ , square (zip (repeat 7) (repeat 4)) ρ,ξ )) (max( 5 ρ,ξ , (max( 7 ρ,ξ , 4 ρ,ξ )) 2 ))2

Figure 2 :

 2 Figure 2: Size based Input/Output upper bound

Example 13 .

 13 Consider stream expressions defined in terms of the following definitions: merge :: [a] → [a] → [a × a] merge (x : xs) (y : ys) . = (x, y) : (merge ys xs) dup :: [a] → [a] dup (x : xs) . = x : (x : (dup xs))

  and H; lg e(v) ⇓ v m then F (|v|) ≥ |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).

Theorem 2 .

 2 If an expression x :: [σ] e(x) :: [τ ] 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 H; s n ⇓ v v and H; lg e(v) ⇓ v m. By Corollary 2, we have lg e(v) ρ,ξ ≥ m ρ,ξ and, by Lemma 10, we have e(v) ξ ≥ m ξ . By Lemma 9, we have v ρ,ξ = |n|. Applying Lemma 8, we have m ρ,ξ = |m|. So, we obtain e ξ (|n|) ≥ |m| and by taking F = e ρ,ξ the conclusion follows. Now suppose that e(x) is SBUB, that H; s n ⇓ v and that H; lg e(v) ⇓ v m. By Corollary 2, we have lg e(v) ξ ≥ m ξ and by, Lemmata 8 and 10, we have e(v) ξ ≥ m ξ = |m|.

Example 15 .

 15 Consider again the stream definitions presented in Example 13: merge :: [a] → [a] → [a × a] merge (x : xs) (y : ys) . = (x, y) : (merge ys xs) dup :: [a] → [a] dup (x : xs) . = x : (x : (dup xs))

Table 1 :

 1 SFL type system

Table 3 :

 3 Counting stream pattern matchings The proof is analogous to the proof of Proposition 1. The only interesting case is the one where the derivation ends with:H; e ⇓ k e 1 : e 2 H; e 1 {e 1 /x 1 , e 2 /x 2 } ⇓ k v H; Case e of x 1 : x 2 → e 1 , nil → e 2 ⇓ k+k +1 vBy induction hypothesis, we have both e 1 {e 1 /x 1 , e 2 /x 2 }

	l-(k+1)
	ξ

Case e of p 1 → e 1 , . . . ,

p n → e n ⇓ k+k v H; e ⇓ k e 1 : e 2 H; e i {e 1 /x 1 , e 2 /x 2 } ⇓ k v H; Case e of x 1 : x 2 → e 1 , nil → e 2 ⇓ k+k +1 v H; e ⇓ k c(e 1 , • • • , e m ) ∀i ≤ n, p i = c(x 1 , • • • , x m )

H; Case e of p 1 → e 1 , . . . , p n → e n ⇓ k Err Proposition 2. Let H and ∅; ∆ e :: A be an environment and an expression admitting both the parametrized interpretation -l ξ . Then:

H, e ⇓ k v implies ∀l ∈ R, e l ξ ≥ v l-k ξ Proof.

  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:

	a] = x : (app xs ys) . = ys app (x : xs) ys app nil ys .
	upto :: Nat → [Nat] upto 0 . = nil upto (x + 1) . = (x + 1) : (upto x)
		extendupto (extendupto s)
	it performs	|n| i=1 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 :: [σ] e(x) :: [τ ] has a length based I/O upper bound if
	there is a function F : R

extendupto :: [Nat] → [Nat] extendupto (x : xs) . = app (upto x) (extendupto xs) + → R + such that for every expression s :: [σ] we have: ∀ n ∈ N, if H; s n ⇓ v v and H; lg e(v) ⇓ v m then F (|n|) ≥ |m| • A stream function x :: [σ] e(x) :: [τ ] has a size based I/O upper bound if there is a function F : R + → R + such that for every expression s :: [σ] we have:

˜pechoux (Romain Péchoux) 1 Work partially supported by the projects ANR-14-CE25-0005 "ELICA", MIUR-PRIN'07 "CON-CERTO" and INRIA Associated Team "CRISTAL". 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.

Appendix A. Comparison with quasi-interpretation

Quasi-interpretations introduced in [START_REF] Bonfante | Quasi-interpretations a way to control resources[END_REF] are a previous formulation of interpretations that require inequalities of the shape l ξ ≥ r ξ for each rule l → 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 . = Case x of c 1 ( x 1 ) → e 1 , . . . , c m ( x m ) → e m generates the following inequality:

which implies, using Lemma 3, ∀i ∈ {1, m}:

The last inequality is obtained by taking the particular values r i = ρ(x i ) since, in this particular case, ρ{ x i := r i } = ρ{ x i := ρ( x i )} = ρ and, consequently, the inequality c i ( x i ) ρ,ξ ≥ c i ( x i ) ρ{ x:= ri},ξ is satisfied. To conclude, we obtain ∀i ∈ {1, m}, f c i ( x i ) ξ ≥ e i ξ which corresponds exactly to the notion of quasi-interpretation applied to the equivalent TRS defined by the rules f c 1 ( x 1 ) → e 1 , . . . , f c m ( x m ) → e m .

Appendix B. An example of Strict Evaluation

Consider an environment 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:

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

where eval Nat is defined analogously using the strict function succ defined above and cons is the function symbol for the strict version of the list of natural numbers constructor: