Adrien Guatto
email: guatto@irif.frvienot@irif.fr

Christine Tasson
email: christine.tasson@lip6.fr

Ada Vienot

A reactive operational semantics for a lambda-calculus with time warps

Many computer systems are reactive: they execute in continuous interaction with their environment. From the perspective of functional programming, reactive systems can be modeled and programmed as stream functions. Several lines of research have exploited this point of view. Works based on Nakano's guarded recursion use type-theoretical modalities to guarantee productivity. Works based on synchronous programming use more specialized methods but guarantee incremental processing of stream fragments.

In this paper, we contribute to a recent synthesis between the two approaches by describing how a language with a family of type-theoretical modalities can be given an incremental semantics in the synchronous style. We prove that this semantics coincides with a more usual big-step semantics.

Introduction

Reactive systems can be found in a variety of application domains, ranging from hard real-time and life-critical systems such as airplane control to more mundane areas like video games and graphical user interfaces. Their specificity as computer systems lies in their continuous interaction with an external environment.

At a low level of abstraction, reactive systems can be modeled as state machines. Yet, reasoning about state machines and, more generally, state transition systems requires beautiful but complex notions of bisimilarity. Furthermore, in practice, the dominant approach to the implementation of state machines is via a mix of callbacks and mutable state, which makes compositional reasoning delicate. These difficulties have motivated a lot of works in the imperative world, such as the well-known model-view-controller pattern.

An alternative approach to the programming of reactive systems is to use functional programming with infinite data structures. In this view, a reactive program is seen as a pure function from some infinite data structure describing incoming events to some other infinite data structure describing outgoing events. This idea can be traced back to the seminal work of Kahn [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], in which he observed how interacting parallel processes could be described as well-behaved functions between infinite sequences -or streams, for short. Thanks to this approach, all the classical tools from functional programming (e.g., higher-order functions) can be applied to reactive systems.

The idea of reactive programming with pure functions has been fertile, and has developed into several distinct lines of research. To introduce these works, and explain how the present paper fits into them, let us consider the example below, given in functional pseudocode. This function takes a stream of integers and returns its running sum, that is, the ith element of the output stream ys is the sum of the first i elements of the input stream xs. Here (::) denotes the stream constructor and map2 f xs ys applies the function f to xs and ys pointwise.

Handling stream functions like sum in a programming language for reactive programming raises two interconnected questions.

1. What constructions and data types does the language offer, and under what conditions?

For example, should one allow arbitrary higher-order functions? Arbitrary recursive definitions? Other infinite data types such as infinite trees or streams of streams?

2. How is the language implemented? A reactive program, being in continuous interaction with its environment, ought to be able to process streams in an incremental fashion. Moreover, this processing should use as little space and time as possible.

Different research lines have answered these questions differently, leading to distinct tradeoffs between expressiveness, safety, and efficiency. A first answer is that of synchronous functional programming languages in the vein of Lustre [START_REF] Caspi | LUSTRE: A declarative language for programming synchronous systems[END_REF], which favor efficiency and safety over expressiveness. In synchronous functional programming, base types are that of streams of scalars, computed along an infinite sequence of execution ticks. In exchange for this restrictive focus, synchronous languages benefit from specialized yet powerful type systems:

• causality types classify productive recursive definitions, e.g., rejecting a variant of sum without the initial 0 on the last argument to map2;

• clock types classify stream types according to its clock : the set of ticks at which a new stream element must appear.

These analyses serve as a foundation to the backends of synchronous compilers, which turn clocked stream functions into state machines realized as memory-frugal imperative code. While well-suited to hard real-time and life-critical systems, synchronous programming can feel restrictive from the perspective of mainstream functional programming. Indeed, even an expressive higher-order synchronous language such as Lucid Synchrone [START_REF] Caspi | Synchronous Kahn Networks[END_REF][START_REF] Pouzet | Lucid Synchrone, version 3. Tutorial and reference manual[END_REF] does not support streams of streams, nor streams of arbitrary functions. This is to be contrasted with the situation in a second approach to reactive programming, functional reactive programming.

Functional reactive programming, as originally proposed by Elliott and Hudak [START_REF] Elliott | Functional Reactive Animation[END_REF], consists in realizing infinite data structures by way of laziness in a language such as Haskell. The expressiveness of Haskell makes it simple to write concise and elegant reactive code, making it especially relevant for prototyping. Unfortunately, using the full power of a lazy language and its facilities for general recursion comes at a cost. This cost is the ease with which one can inadvertently write a non productive definition or introduce unbounded memory usage [START_REF] Liu | Causal commutative arrows[END_REF].

To be used in applications with performance or safety needs, functional reactive programming has to be tamed. This can be achieved in two ways. One possibility is to implement a restrictive domain-specific language for reactive programming as a Haskell library. From this perspective, Haskell serves as a powerful macro language for the embedded language. This is the approach used in, e.g., causal commutative arrows [START_REF] Liu | Causal commutative arrows[END_REF].

Another choice is to drop Haskell and develop a standalone domain-specific language. This approach has become increasingly popular since the seminal work of Krishnaswami and Benton [START_REF] Neelakantan | Ultrametric Semantics of Reactive Programs[END_REF]. They remarked that a certain unary connective (or modality) studied in foundational works on modal logic [START_REF] Nakano | A Modality for Recursion[END_REF] and denotational semantics [START_REF] Appel | A Very Modal Model of a Modern, Major, General Type System[END_REF][START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF] can be used to give a type-theoretical criterion for productive recursion. This criterion consists in Figure 1. The type £A (pronounced "later A") is a slightly weaker version of A that does not give any information at the beginning of execution. This guarded recursion rule, by requiring the body of the definition to have type £A → A, makes sure that the definition actually extends x before using it. In particular, computing the fixed point of the identity function is no longer permitted. This simple idea has led to many developments, including memory-conscious implementations [START_REF] Neelakantan | Higher-Order Functional Reactive Programming without Spacetime Leaks[END_REF][START_REF] Bahr | The Clocks Are Ticking: No More Delays! Reduction Semantics for Type Theory with Guarded Recursion[END_REF].

Interestingly, the introduction of the later modality in functional reactive programming brings it closer to synchronous concepts. Indeed, the type £A should be thought of as "A but without the data available at the first execution tick." For example, the type £ Stream N is that of streams that start growing at the second tick rather than the first one. Thus, the later modality introduces an idea of global discrete time akin to that found in synchronous programming. Moreover, its effect on types is tantalizingly similar to that of the clocks used in synchronous programming. In light of these similarities, the first author built a unifying calculus, termed λ * , that bridges synchronous programming and functional reactive programming [START_REF] Guatto | A Generalized Modality for Recursion[END_REF].

In λ * , the later modality arises as a special case of a more general warping modality. The warping modality p -acts upon a type as prescribed by the time warp denoted p. A time warp is, briefly speaking, a well-behaved map from the discrete time scale to itself. The type p A should be thought of as a variant of A suitably stretched or compressed so that, at tick n, one can observe from it what can be observed from A at tick p(n). The calculus can be thought of as connecting two lines of research in the sense that all synchronous clocks are time warps and all modalities used in guarded recursion can be described as time warps. Moreover, many time warps where hitherto unavailable as type connectives.

In addition to a type system, λ * comes equipped with an execution mechanism expressed as an operational semantics. It can be seen as an evaluator parameterized with a quantity of fuel. It is a theorem of λ * that a closed term of type Stream B, when evaluated with n units of fuel, converges to a list of n booleans. This list is a prefix of the ideal conceptually-infinite stream computed by the program. While this is satisfactory from a metatheoretical perspective, this process leaves much to be desired in the reactive setting. The evaluation process is not incremental: the evaluation process with n + 1 units of fuel cannot reuse any of the computations that arose while computing the shorter prefixes.

Contributions.

In this paper, we continue to bridge the gap between synchronous functional programming and functional reactive programming by introducing an incremental semantics for λ * . Taking inspiration from compilation techniques introduced for Lucid Synchrone [START_REF] Caspi | A co-iterative characterization of synchronous stream functions[END_REF][START_REF] Pouzet | Lucid Synchrone, version 3. Tutorial and reference manual[END_REF], we introduce a notion of typed program states that store results to be reused, and replace prefix values with collections of instantaneous deltas that we call increments. We prove by a logicalrelation argument that our incremental semantics is sound: glueing together the consecutive increments recovers the prefix computed by the reference semantics.

In Section 2, we introduce the first author's λ * calculus, and our modifications of its type system needed to type-check program states. We then describe our incremental semantics in depth in Section 3, including its metatheory and the adequacy theorem for our logical relation. Finally, in Section 4 we discuss our results and their relation to previous works.

Notations. We write ω for the first infinite ordinal and ω + 1 for its successor ordinal ω ∪ {ω}. Additition and subtraction extend to ω + 1 by setting n + ω = ω and n -ω = 0 for all n ∈ ω + 1. The domain of a partial map f : X Y , denoted dom(f ), is defined as f -1 (Y ). A finite map is a partial map of finite domain. Given a finite map f , the notation f (x) implies x ∈ dom(f ). We write f, x : y or f [y/x] for the finite map sending x to y and x ∈ dom(f ) \ {x} to f (x ).

The λ * calculus

In order to save space, we leave aside the treatment of product and sum types in the short version of this paper. A complete treatment of λ * can be found in the full version of the paper, available at http://hal.archives-ouvertes.fr/hal-03465519.

Type system

Time warps and terms. In reactive languages, types are implicitly indexed by logical time steps. In λ * , this indexing can be changed through the use of the warping modality p -. To explain how this modality works, we must first define what a time warp p exactly is.

Definition 2.1. A time warp is a suprema-preserving map p : ω + 1 → ω + 1.
Equivalently, a time warp is a monotonic map from ω + 1 to itself such that p(0) = 0 and p(ω) = max i<ω p(i). Time warps are denoted p, q, r. The time warps id and lat respectively correspond to the maps n → n and n → n -1.

Time warps appear in the terms of λ * as well as in its types: they decorate the term constructors delay q p (M ) and M by p. The other terms of the language are those of a simplytyped λ-calculus with streams, constants c belonging to some fixed set C, and recursive definitions.

M, N

::= x | c | λx A . M | M N | rec x A . M | M :: N | hd M | tl M | M by p | delay q p (M )
Types. The types of λ * are those of the simply-typed λ-calculus with a fixed set of ground types G (whose elements are denoted ν) and streams, as well as the warping modality p (-). 1A, B ::

= ν | Str A | A S = ⇒ B | p A
The label S annotating the arrow type A S = ⇒ B is new to the present paper. It is linked to the proposed incremental semantics. We explain the purpose this state type S serves in Section 3.

Informally, the values of type p A at tick n are those of A at tick p(n). Another possible way to think of p A is as a type where time passes "p-times" faster than in type A. For example, a value of type p Str Nat at tick n is a list of p(n) numbers.

We assume that for every ground type ν there exists a set C ν ⊆ C such that every constant c ∈ C belongs to exactly one such C ν .

Typing contexts. Typing contexts are finite maps from identifiers to types, and are denoted Γ, ∆. We write p Γ for the typing context sending x ∈ dom(Γ) to p ⇒ Γ(x).

Typing judgements. The typing judgment Γ M : A | S states that if the free variables of M respect the types prescribed by Γ then M computes a result of type A using a state of type S. Its rules are given in Figure 2. Most of them are those of the simply-typed λ-calculus, thus we focus our explanation on the rules specific to temporal constructs. The state-type aspect is new and we discuss it in the next section.

In λ * , the type Str A classifies streams that unfold at the rate of one element per step. This is reflected by the rules Head, Tail, and Cons, which state that the head of a stream is available now while its tail is only available at type lat Str A. This type describes streams which start to grow strictly after the first tick. Thus, the ith element of a stream of type Str A is only available at tick i. Rule Rec is that of guarded recursive definitions. It mirrors the rule GuardedRec described in the introduction, but expresses the later modality £ as a special application of the warping modality with lat as time warp. This rule enforces productivity by forbidding instantaneous dependencies in recursive definitions.

Γ M : A | S Var Γ, x : A x : A | 1 Scalar c ∈ C ν Γ c : ν | 1 Lam Γ, x : A M : B | S Γ λx A . M : A S = ⇒ B | 1 App Γ M : A S = = ⇒ B | S Γ N : A | S Γ M N : B | S × S × S Head Γ M : Str A | S Γ hd M : A | S Tail Γ M : Str A | S Γ tl M : lat Str A | S Cons Γ M : A | S Γ N : lat Str A | S Γ M :: N : Str A | S × S Rec Γ, x : lat A M : A | S Γ rec x A . M : A | S × ∫A By Γ M : A | S p Γ M by p : p A | p S Delay q p Γ M : p A | S Γ delay q p (M ) : q A | S × ∫(p A)
The by construction (Rule By) is used to introduce and eliminate the warp modality. It states that if a program M produces an output at rate A by consuming inputs at rate Γ, then one can always speed M up to produce an output at rate p A, at the cost of consuming inputs at rate p Γ, for any p.

If q(n) p(n) then the values of type p A at the nth tick can be truncated into values of type q A at the nth tick. Rule Delay generalizes this reasoning to all ticks: the delay construction turns results of type p A into results of type q A as long as q p, where denotes the pointwise ordering. We describe the operational content of truncation in the next section.

Prefix semantics

The terms of λ * manipulate ideal, infinite data structures, but they have to execute on a concrete machine that only deals with finite syntax. For this reason, the reference semantics of the language computes finite yet arbitrarily precise approximants, or prefixes, of streams and other infinite data structures. The length of these prefixes is controlled by a parameter to the evaluation judgment, which can be thought of alternatively as the current tick or as a quantity of fuel (as in step-indexing [START_REF] Appel | A Very Modal Model of a Modern, Major, General Type System[END_REF]). Using this parameter, one may evaluate, e.g., a program computing the stream of natural numbers at tick 1 and obtain the prefix 0 :: stop, or evaluate at tick 2 and obtain the prefix 0 :: 1 :: stop, and so on. For this reason, we call this evaluation semantics the prefix semantics.

Prefix values and environments. Prefix values, denoted V , should be thought of as prefixes of a certain length of an infinite object of a certain type. A prefix of length n is the result of a computation at tick n. Figure 3 describes the typing rules of the judgment V : A a O n, which states that V is a prefix of length n of an object of type A.

The special value stop is a prefix of every value at 0. Prefixes at ω should be infinite but Environments, denoted E, are partial maps from identifiers to values. We write w (p, E) for the environment E sending x ∈ dom(E) to w (p, E(x)).

V : A @ n VStop stop : A @ 0 VBox Γ M : A | S E : Γ @ ω box(M ){E} : A @ ω VScalar c ∈ C ν c : ν @ n + 1 VWarp V : A @ p(n + 1) w (p, V ) : p A @ n + 1 VClo Γ, x : A M : B | S E : Γ @ n + 1 (x.M ){E} : A S = ⇒ B @ n + 1 VStream V : A @ n + 1 V : Str A @ n V :: V : Str A @ n + 1 E : Γ @ n VEnv dom(Γ) = dom(E) ∀x ∈ dom(Γ). E(x) : Γ(x) @ n E : Γ @ n
V n V 0 = stop V ω = V c n+1 = c w (p, V ) n+1 = w p, V p(n+1) (x.M ){E} n+1 = (x.M ){ E n+1 } V 1 :: V 2 n+1 = V 1 n+1 :: V 2 n box(M ){E} n+1 = V if M ; E n+1 ⇓ n+1 V

Figure 4 Truncation of prefixes

As mentioned before, prefixes can be truncated. Given a prefix V of length m and n ≤ m, one may obtain a shorter prefix V n as defined in Figure 4. This extends to environments pointwise. Since the evaluation judgment is deterministic [START_REF] Guatto | A Generalized Modality for Recursion[END_REF],n defines a partial (because of the box case) function rather than a relation.

The special value stop is a 0-length prefix of every other value. Truncating at ω does nothing. Truncating a closure means truncating its environment. Truncating a stream prefix of length n > 0 involves truncating its tail at length n -1; for example 1 :: 2 :: stop 1 = 1 :: stop.

To truncate a thunk one has to evaluate it.

In addition to being total on well-typed terms, truncation preserves typing [START_REF] Guatto | A Generalized Modality for Recursion[END_REF].

Theorem 2.1. If V : A @ n, then for all m n, we have V m : A @ m.

Evaluation judgement. The judgment given in Figure 5 is mostly that of a big-step semantics for call-by-value λ-calculus with environments and closures, extended to depend on a time step n.

We explain the rules that have a time-specific aspect. Rule PZero states that a program evaluated at time 0 always returns the same initial value named stop. Rule POmega freezes both the code and the environment in a thunk. When an actual value is required, the program can then be evaluated as needed to any finite length. Rule PBy formalizes the idea that type p A is composed of p-long prefixes of type A. Rule PRec is reminiscent of the Kleene fixed point theorem as, in essence, it computes the value of rec x. M at n as the iterated application (λx. M ) n (stop). This process is formalized by the iteration judgment M ; E ; x ; V ⇑ n m V , whose iterative behavior is captured by the lemma below.

Lemma 2.1. If M ; E ; x ; V ⇑ k i V then for all j such that i j k, there is V such that M ; E j ; x ; V ⇑ j i V and M ; E ; x ; V ⇑ k j V . M ; E ⇓ n V PZero M ; E ⇓ 0 stop POmega M ; E ⇓ ω box(M ){E} PScalar c ; E ⇓ n+1 c PVar x ∈ dom(E) x ; E ⇓ n+1 E(x) PLam λx A . M ; E ⇓ n+1 (x.M ){E} PApp M ; E ⇓ n+1 (x.P ){E } N ; E ⇓ n+1 V P ; E V / x ⇓ n+1 V M N ; E ⇓ n+1 V PHead M ; E ⇓ n+1 V :: V hd M ; E ⇓ n+1 V PTail M ; E ⇓ n+1 V :: V tl M ; E ⇓ n+1 w (lat, V ) PCons M ; E ⇓ n+1 V N ; E ⇓ n+1 w (lat, V ) M :: N ; E ⇓ n+1 V :: V PBy M ; E ⇓ p(n+1) V M by p ; w (p, E) ⇓ n+1 w (p, V ) PRec M ; E ; x ; stop ⇑ n+1 0 V rec x A . M ; E ⇓ n+1 V PDelay M ; E ⇓ n+1 w (p, V ) delay q p (M ) ; E ⇓ n+1 w q, V q(n+1) M ; E ; x ; V ⇑ n m V PIFinish M ; E ; x ; V ⇑ n n V PIIter m < n M ; E ; x ; V ⇑ n m+1 V M ; E w (lat, V ) / x ⇓ m+1 V M ; E ; x ; V ⇑ n m V

Figure 5 Prefix evaluation judgement

As an illustration on how the prefix evaluation works, consider the following program defining the stream of natural numbers. The function incr : Str Int 1 = ⇒ Str Int adds one to all of the constituents of a stream of integers. For the example to be well-typed, we need to use the function shift A : A 1 = ⇒ (lat A), which acts as a causality-preserving type coercion. 2let incr = shift incr in let rec nat = 0 :: (incr nat by lat)

The table below gives the first prefixes produced by evaluating the program nat. The program nat is recursive. The fixed point rule evaluates the body of the rec block by recomputing the value obtained at the previous tick, which is incremented by calling incr . At the first step, this yields stop. For the recursion to be guarded, the by lat wraps it under a special constructor to indicate its provenance: this yields w (lat, stop). Finally, 0 is concatenated to it, yielding 0 :: stop. Next step, the process is repeated: we obtain 0 :: stop again at the first tick. We increment it using incr , which yields 1 :: stop, and wrap it under a constructor, turning it into w (lat, 1 :: stop). Concatenating 0 to it yields 0 :: 1 :: stop, and so on.

Metatheory. We state the correctness theorems of [START_REF] Guatto | A Generalized Modality for Recursion[END_REF] that will be important to the rest of the paper. Combined, they express that the evaluation of well-typed terms defines a total function, and that this function is monotonic with respect to truncation.

Theorem 2.2 (Subject reduction). If Γ M : A | S and M ; E ⇓ n V with E : Γ @ n, then V : A @ n. Theorem 2.3 (Totality). If Γ M : A | S and E : Γ @ n, then there exists V such that M ; E ⇓ n V . Theorem 2.4 (Determinism). If M ; E ⇓ n V 1 and M ; E ⇓ n V 2 , then V 1 = V 2 . Theorem 2.5 (Monotonicity). If m n and M ; E ⇓ n V then M ; E m ⇓ m V m .
3 Reactive semantics for λ *

In this section, we present a new semantics for the λ * calculus, quite different from the prefix one. In this semantics, program execution consists in a sequence of reaction steps, each of which consumes a slice of the inputs, produces a slice of the outputs, and updates some internal state. To define this semantics, we first describe states and their types, as well as increments, a new sort of values describing these "slices." We show in Section 3.4 that this semantics computes the same results as the prefix semantics, in the appropriate sense.

Increments and states

Increments. Increments, denoted δ, are syntactic objects representing the information gained by running the program for one step. For example, each time a program of type Str Nat does a step, it produces a number. The syntax of increments is defined by the following grammar.

δ, δ ::= nil | c | (x.M ){γ} | δ :: δ | (δ i ) i
The null increment is denoted nil, c denotes a constant, (x.M ){γ} denotes an incremental closure, δ :: δ denotes a temporal sequence of increments and (δ i ) i<n denotes a warped family of increments.

Incremental environments, denoted γ, are finite maps from identifiers to increments. If the context permits no ambiguity, they will also be referred to simply as "environments" for the sake of brevity. By abuse of notation, if (γ i ) i<n is a family of environments with a common domain D, we write (γ i ) i<n for the environment sending x ∈ D to (γ i (x)) i<n .

Families of increments and typing. Another intuition behind increments is that they represent one-step-wide slices of prefixes. A collection of n increments then represents a prefix of length n. Such collections are represented by possibly infinite families of increments (δ i ) i<n . The empty family is written ε. The concatenation of two families of increments

(δ i ) i<n and (δ i ) i<m , denoted (δ i ) i<n ⊕ (δ i ) i<m , is the family (δ i ) i<n+m such that δ i is either δ i when i < n or δ i-m when m i < m + n.
As families of increments are intended to represent prefixes, they are typed according to the judgement rules given in Figure 6. We explain three interesting rules.

Rule IScalar states that scalars do not evolve as time passes. They yield all of their informational content at the very first tick, and they bring no additional information during subsequent ticks. Thus, families of increments of a scalar type comprise an initial scalar value followed by the null increment nil forever after.

(δ i ) i<n : A @ n IStop ε : A @ 0 IScalar c ∈ C ν (c) ⊕ (nil) i<n : ν @ n + 1 IWarp (δ i ) i<p(n+1) : A @ p(n + 1) (δ j ) p(i) j<p(i+1) i<n+1 : p A @ n + 1 IClo Γ, x : A M : B | S (γ i ) i<n+1 : Γ @ n + 1 (x.M ){γ i } i<n+1 : A S = ⇒ B @ n + 1 IStream (δ i ) i<n+1 : A @ n + 1 (δ i ) i<n+1 : lat Str A @ n + 1 (δ i :: δ i ) i<n+1 : Str A @ n + 1 IBox ∀m ∈ ω. (δ i ) i<m : A @ m (δ i ) i<ω : A @ ω (γ i ) i<n : Γ @ n IEnv ∀i < n. dom(Γ) = dom(γ i ) ∀x ∈ dom(Γ). (γ i (x)) i<n : Γ(x) @ n (γ i ) i<n : Γ @ n Figure 6
Typing judgement for λ * increments Rule IWarp expresses that flattening the n lists under the constructor yields a family of size p(n). Recall that a prefix of p A at time n is a prefix of A at time p(n). Thus, while one step from time n -1 to n is performed on the outside of the program, ∂p(n) = p(n) -p(n -1) steps are performed under the by during this time. Since increments represent the informational content of the program during one step, an increment of p A at time n is a family of increments of size ∂p(n), encompassing steps from p(n -1) to p(n) -1.

Finally, rule IBox is the incremental counterpart to rule VBox. The main difference is that we no longer represent infinite prefixes as thunks (as in the prefix semantics) but as infinite families of increments. For this reason, truncation in the incremental semantics consists in restricting a (possibly infinite) family of increments to one of its initial segments. This is simpler than in the prefix semantics, where truncating a thunk actually consists in evaluating its body. However, this means that a program may return an infinite family of increments in finite time, e.g., as the result of M by p at the ith tick for p such that p(i) = ω. We discuss the consequences of this choice in Section 4.

We now prove a counterpart to Theorem 2.1 by induction over typing derivations. A welltyped family of increments can be truncated and preserve its typing, albeit at a shorter length. Theorem 3.1 (Type safety of increment truncation). If (δ i ) i<n : A @ n and m n then

(δ i ) i<m : A @ m.
Notice that the typing judgement is only applicable on family of increments, and not increments alone. As an illustration, let x : A M : B | S and x : A N : B | S be two different well-typed terms. Now, consider the family of increments (x.M ){}, (x.N ){} with M and N unrelated terms of the same type. It maps to no prefix of type A S = ⇒ B, since the code inside the two closures differs. If we could somehow type increments on their own, there would be families of increments that are well-typed but do not correspond to a prefix. This is undesirable, as we want well-typed families of increments to map one-to-one to prefixes.

States and their types. States, denoted s, are syntactic objects. They are classified by a special category of types, state types, denoted S, according to the rules given in Figure 7.

s, s ::= stop | done | unit | w (p, s) | (s, s ) | inc ((δ i ) i ) S, S ::= 1 | p S | S × S | ∫A
These rules are similar to the ones used for typing prefixes (cf. Figure 3), except for SDone and SIncr. Rule SDone reflects the fact that a program that has performed ω reactions no longer needs to store any relevant state. We will develop this point shortly. Rule SIncr introduces the type constructor ∫, which embeds families of increments into states. As such, ∫A denotes a "buffer" able to store values of type A -this allows us to store previously computed values into our states for further computations. Notice that it is the only interesting base state type, as the only other one is 1, and denotes a stateless computation.

s : S a O n SStop stop : S a O 0 SDone done : S a O ω SUnit unit : 1 a O n + 1 SWarp s : S a O p(n + 1) w (p, s) : p S a O n + 1 SPair s 1 : S 1 a O n + 1 s 2 : S 2 a O n + 1 (s 1 , s 2 ) : S 1 × S 2 a O n + 1 SIncr (δ i ) i<n+1 : A @ n + 1 inc ((δ i ) i<n+1 ) : ∫A a O n + 1
Figure 7 Typing judgement for states

We can now explain the state-type component S of the typing judgment Γ M : A | S that we deliberately ignored in Section 2.1. This state type describes the state that our incremental semantics associates to M . It is handled in the same way as effect annotations in type-and-effect disciplines [START_REF] Lucassen | Polymorphic effect systems[END_REF]. In particular, App expresses that an application requires three substates: one for the function, one for the argument, and one for the body of the function. Most other rules follow simpler patterns, with the states from subterms becoming substates of the parent term. Only the rules dealing with the warping modality require further component.

Rule By asserts that the state of p by M is just the state of M at rhythm p. This is because running a term under a by is akin to running it under an independant local clock p -thus, its state also grows at this rhythm.

We have seen how the prefix semantics mimicks Kleene's iteration sequence, approximating the fixed point of M at n by (λx. M ) n (stop), so to speak. In the incremental semantics, at the (n + 1)th tick, rather than recompute n + 1 applications of M we apply M once to the previously-computed result. In order to be able to do so, we include a copy of the output of M in the state of rec x. M , as expressed by Rec. This behavior is a key ingredient of the incremental semantics.

Rule Delay specifies a nontrivial state type due to our wish to incrementalize the computations. To understand the specified state type, imagine that we receive incremental results from some term M at rythm p, and wish to produce incremental results at rythm q. If q is slow enough with respect to p, we may have to output now increments received previously. Hence, we choose to store the output of M in the state of delay q p (M ). (We discuss how much buffering is needed in Section 4.)

Evaluation judgements

Discrete derivatives. We are now interested in how data changes from one tick to the next. Thus we define the discrete derivative of a time warp p, denoted ∂p, as n → p(n) -p(n -1).

M s ; γ = ⇒ s ; δ EScalar c unit ; γ = ⇒ unit ; nil EScalarI c ∈ C ν c stop ; γ = ⇒ unit ; c EVar x ∈ dom(γ) x unit ; γ = ⇒ unit ; γ(x) ELam λx A . M unit ; γ = ⇒ unit ; (x.M ){γ} EApp M s M ; γ = ⇒ s M ; (x.P ){γ } N s N ; γ = ⇒ s N ; δ P s P ; γ δ/ x = ⇒ s P ; δ M N (s M , s N , s P ) ; γ = ⇒ (s M , s N , s P ) ; δ EHead M s ; γ = ⇒ s ; δ :: δ hd M s ; γ = ⇒ s ; δ ETail M s ; γ = ⇒ s ; δ :: δ tl M s ; γ = ⇒ s ; δ ECons M s M ; γ = ⇒ s M ; δ N s N ; γ = ⇒ s N ; δ M :: N (s M , s N ) ; γ = ⇒ (s M , s N ) ; δ :: δ EBy M s ; (γ i ) i<∂p(n) ∂p(n) ===⇒ s ; (δ i ) i<∂p(n) M by p w (p, s) ; (γ i ) i<∂p(n) = ⇒ w (p, s ) ; (δ i ) i<∂p(n) ERecI M stop ; γ ε/ x = ⇒ s ; δ rec x A . M stop ; γ = ⇒ (s , inc (δ)) ; δ ERec M s ; γ (δ n-1 )/ x = ⇒ s ; δ n rec x A . M s, inc (δ i ) i<n ; γ = ⇒ s , inc (δ i ) i<n+1 ; δ n EDelay M s ; γ = ⇒ s ; (δ i ) p(n) i<p(n+1) delay q p (M ) s, inc (δ j ) p(i) j<p(i+1) i<n ; γ = ⇒ s , inc (δ j ) p(i) j<p(i+1) i<n+1 ; (δ i ) q(n) i<q(n+1) Figure 8 Single-step evaluation judgement γ δ s s Γ M : A | S S a O n S a O n + 1

Figure 9 Terms as block diagrams

Single-step evaluation judgement. The main idea behind the incremental semantics is to have a relation that advances a computation by one tick. Such a relation can be pictured by viewing the well-typed term Γ M : A | S as an automaton (see Figure 9). It is given a state s of type S, and an incremental environment γ representing a slice of a prefix environment of type Γ. The automaton produces an increment δ representing a slice of the output value of type A, and a new state s that is ready to be used to advance the program another step. To this end, we introduce the single-step evaluation judgement, denoted M s ; γ = ⇒ s ; δ. The rules composing this judgement are given in Figure 8. All rules -except two -that handle cases where the initial state is equal to stop have been omitted here for shortness sake. 3 The reason for singling out EScalarI and ERecI is that unlike the other rules, they are not just structural coercions. EScalarI expresses that once a scalar has yielded its full informational content at the first step, it becomes inert and returns the vacuous increment, nil. ERecI is in charge of initializing the recursion. It does so by binding ε in the environment, which corresponds to the first increment of a family of type lat A.

We detail three remarkable rules of the judgement. Rule EBy makes use of the many-step evaluation judgement in its premise, which will formally be introduced in the next paragraph. It corresponds to repeated application of the single-step judgement. When the program M by p makes a step from time n -1 to time n, the subterm M makes a step from time p(n -1) to p(n), thus producing ∂p(n) increments. The ∂p(n)-family of increments output by the subterm M is then turned into a single increment by the constructor. The input and output states are p-shifted in time, and protected under the constructor w (p, -).

Rule ERec is the most surprising one, due to the fact that it only needs to use the increment produced at the previous tick to produce the one for the current step. While it receives by way of its state a family of increments intended to represent the entierety of the previously-computed prefix, it only uses the very last one to produce a result. Apart from this particular observation, the rule behaves similarly to its prefix counterpart PRec, as the premise of ERec behaves similarly to the iteration judgement (cf. Figure 5): a value of type A and length n -1 is inserted under a constructor for a value of type lat A, and bound to the environment. Once this increment has been produced, it is appended to the input state's increments.

p(n -1) p(n) n 0 q(n -1) q(n) from state from M output Figure 10
EDelay timings Rule EDelay states that at time n, the subterm M of type p A produces a warped increment family encompassing ticks from p(n -1) to p(n) -1. To produce an increment of q A at time n, we need a warped increment family encompassing ticks from q(n -1) to q(n) -1. We buffer the increments produced by the subterm M by appending them to the input state. This yields a family of increments encompassing times 0 to times p(n) -1, which becomes a new output. From this family, we extract increments ranging from time q(n -1) to time q(n) -1. This is always possible since q p. By warping this subfamily extracted from the output state, we produce our final result (see Figure 10).

Recall the program nat given in Section 2.2. The table below gives the first increments produced by evaluating it using the single-step reduction. The fixed point rule evaluates the body under rec. At the first tick, the warped empty increment [ ] is bound in the context. Applying incr on it leaves it unchanged. Notice that at the very first tick, the program '0' returns its value as an increment. Thus, when '0 ::' is called, it produces the increment 0 :: [ ]. The result is then stored in the state before being returned by the whole program. At the next tick, we take this state, and unwrap rec again. This time, the previous increment is 0 :: [ ], and applying incr on it yields 1 :: [ ]. Then, we call '0 ::' on it. However, since we are not at the first tick, the program '0' is inert and produces the increment nil. Thus, when evaluated at tick 1, the program returns the increment nil :: [1 :: [ ]]. The same reasoning applies for subsequent evaluations.

Many-step evaluation judgement. We define a relation n = ⇒, the many-step evaluation judgement, whose rules are given in Figure 11. The statement M s ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n expresses that repeated applications of single-step reduction starting from state s leads to state s , with step i ∈ [0, n) consuming γ i and producing δ i .

Rule EOmega deserves special attention. Being able to run a program for ω steps means being able to run it for m steps, for every finite m. The infinite family of increments returned as output is defined elementwise by all the finite runs of the program. However, the output state of all the finite runs is thrown away, and an infinite run always has output state done. Intuitively speaking, the final state of a program after ω steps is irrelevant since it can never do any further step. Since the rules in Figure 8 do not contain any rule that takes done as input state, EStep can never be applied, making done final -which is the intended behavior. Any two many-step reductions originating from the same term, inputs, and initial state yield the same outputs for both state and produced increments. In other words, the automaton described by M is deterministic.

M s ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n EZero M s ; ε 0 = ⇒ s ; ε EStep M s ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n M s ; γ n = ⇒ s ; δ n M s ; (γ i ) i<n+1 n+1 = == ⇒ s ; (δ i ) i<n+1 EOmega ∀m ≤ ω, M s ; (γ i ) i<m m = ⇒ s m ; (δ i ) i<m M s ; (γ i ) i<ω ω = ⇒ done ; (δ i ) i<ω
Theorem 3.2 (Determinism). If M s; (γ i ) i<n n = ⇒ s 1 ; (δ 1 i ) i<n and M s ; (γ i ) i<n n = ⇒ s 2 ; (δ 2 i ) i<n , then s 1 = s 2 and δ 1 i = δ 2 i for all i.
Since the many-step evaluation judgement depends on the single-step evaluation judgement and vice-versa due to rules EStep and EBy respectively, the proof has to proceed by mutual induction on the judgements using a lemma that proves determinism in the single-step case.

Lemma 3.1 (Determinism, single-step). If we have M s ; γ = ⇒ s 1 ; δ 1 and M s ; γ = ⇒ s 2 ; δ 2 then s 1 = s 2 and δ 1 = δ 2 .

Metatheory

We now prove metatheoretical properties of the type system in relation with the many-step evaluation judgment. These theorems prove that our incremental semantics is as well-behaved as the prefix semantics: it is a type-respecting total function on well-typed terms. Since the type system of increments applies to families of increments indexed by a downward-closed subset of ω + 1, the theorems only apply with stop as the initial state.

Many-step reduction is type-safe. Running a closed term of type A with initial state stop for n steps produces a family of increments (δ i ) i<n of type A at n. This result, generalized to open terms, is proved by induction over typing derivations.

Theorem 3.3 (Type safety). Let Γ M : A | S, and n ω. For all (γ i ) i<n : Γ @ n and

(δ i ) i<n such that M stop ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n , we have (δ i ) i<n : A @ n and s : S a O n.
Many-step reduction is a total function. For any well-typed closed term M , there exists a unique family of increments (δ i ) i<n such that running M for n steps produces (δ i ) i<n . This is due to Theorem A.2 and to the theorem below, proved again by induction over typing derivations.

Theorem 3.4 (Totality). Let Γ M : A | S, and n ω. For all (γ i ) i<n : Γ @ n, there exists s and

(δ i ) i≤n such that M stop ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n . ε |= A 0 stop (δ i ) i<ω |= A ω box(M ){E} ⇐⇒ ∀n < ω. (δ i ) i<n |= A n box(M ){E} n (c) ⊕ (nil) i<n-1 |= ν n c (δ j ) p(i) j<p(i+1) i<n |= p A n w (p, V ) ⇐⇒ (δ i ) i<p(n) |= A p(n) V δ i :: δ j i-1 j<i i<n |= Str A n V :: V ⇐⇒ (δ i ) i<n |= A n V and (δ i ) i<n-1 |= Str A n-1 V (x.M ){γ i } i<n |= A S = ⇒B n (x.N ){E} ⇐⇒ ∀m n, ∀(δ i ) i<m |= A m V, ∃s, (δ i ) i<m , V ,      M stop ; γ i δ i / x i<m m = ⇒ s ; (δ i ) i<m N ; E m V / x ⇓ m V (δ i ) i<m |= B m V Figure 12
Logical relation for values

Correctness

While the many-step evaluation judgments define a total function, it remains to be proved that it is correct, in the sense that it computes the same results as the prefix semantics. In particular, we wish to prove the following result. This theorem is more general than it looks. In the presence of by in the language, the term M may contain subterms which have to run for more than one step. In particular, the result c could be the ith element of some stream of numbers, for i fixed but arbitrary. For this reason, to prove this theorem, we must generalize it to many-step reduction, in addition to open terms of arbitrary types. We do so by way of the logical relation defined in Figure 12.

The logical relation specifies how families of increments assemble into prefix values. Given a family of increments (δ i ) i<n : A @ n and a prefix value V : A @ n, we say that (δ i ) i is a coherent slicing of V when ∆ |= A n V holds. This relation is defined by well-founded induction on the lexicographical product < ty × lex < ω+1 between the strict subtree ordering on types < ty and the canonical strict ordering < ω+1 on ω + 1.

The case of scalars, pairs, sums, and streams are unremarkable. Thunks representing infinite prefixes are coherently sliced into infinite families of prefixes in such a way that truncation at a finite length always produces coherent slicings. A warped increment family is a coherent slicing of a warped value if their unfoldings are coherent slicings of each other. Finally, functions follow the usual pattern of logical relations, adapted to our setting: a (prefix) closure is coherently sliced by a family of incremental closures when, applied to coherent arguments, they return coherent results.

The logical relation over values extends to incremental and prefix environments.

Definition 3.1 (Logical relation for environments). A family

(γ i ) i : Γ @ n is a coherent slicing of E : Γ @ n, denoted (γ i ) i |= Γ n E, when, for all x ∈ dom(Γ), we have (γ i (x)) i |= Γ(x) n E(x).
We extend the logical relation to terms. Intuitively, two closed terms M and N are logically related when the increments produced by n reactions of M coherently slice the prefix of length n computed from N . The definition below generalizes this to open terms. Definition 3.2 (Logical relation for terms). The terms M and N are logically related at Γ and A, denoted M |= Γ A N , when, for all n, E, (γ i ) i<n , V , (δ i ) i<n and s such that

(γ i ) i<n |= Γ n E, if N ; E ⇓ n V and M stop ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n , then (δ i ) i<n |= A n V .
Adequacy. The adequacy lemma for our logical relation immediately implies Theorem 3.5 by the definition of AScalar and the fact that the single-step reduction is a special case of the many-step one.

Lemma 3.2 (Adequacy). If Γ M : A | S, then M |= Γ A M .
The proof is done by induction over the typing hypothesis. Inversion lemmas are needed to invert whole chains of many-step reductions, as it is defined in term of single-step reductions. Such lemmas are not needed for inverting the prefix reduction. The induction hypothesis is then to be applied on subterms, which in turn proves that they produce coherent slicings. Application of the rules of Figure 12 yields the desired results.

To prove the adequacy lemma, we need a result connecting truncation in the original prefix semantics with our incremental semantics in the following sense.

Lemma 3.3 (Coherence of truncation). If (δ i ) i<n |= A n V and m n, then (δ i ) i<m |= A m V m .
The key case is the one of Rec. It is dealt with by an inner induction on the number of steps, using Lemma A.9 to connect the intermediate families of increments with the values computed by the prefix semantics.

Perspectives

Limitations

Increments storage in states. Because our increment typing judgement only classifies whole families of increments, states have to store entire families of increments as well to be well-typed. As a consequence, a naive implementation of our semantics of delays and fixed points would keep all past increments in memory, resulting in unbounded space usage. This is very unsatisfactory since the elimination of such spurious "space leaks" is a core concern in reactive programming. Fortunately, inspection of the single-step judgement shows that the rules that use state to store intermediate computations only rely on a subset of the increments stored in this state. For example, the semantics of fix actually uses only the last increment from its state, and thus only requires a buffer of size one.

Infinitary syntax. As mentioned in Section 3, in the original semantics, prefixes are always finite since prefixes of type A @ ω are thunks. In contrast, families of increments can be actually infinite. This choice makes for simple semantics but cannot be used in a non-lazy implementation. We believe that using thunks in the incremental semantics would be technically heavier but would not raise any conceptual issue.

Structural coercions of the warping modality. The original presentation of λ * includes primitive constructs to mediate between isomorphic types such as p (A × B) and (p A) × (p B). We have omitted their unremarkable treatment from this paper for lack of space.

Recursive states. Our state types do not include recursive types such as streams. This restriction makes it impossible to capture most higher-order recursive functions, such as the general map function over streams. This function should have type

Related work

The implementation of reactive programs is a wide area that has been explored in distinct directions by distinct lines of research. We briefly discuss two of them.

Synchronous programming. Synchronous languages restrict stream elements to be of scalar types, eschewing types such as streams of streams. This restriction allows for efficient if specialized implementation techniques. Our incremental semantics is directly inspired from their "single-loop" state-passing transform [START_REF] Raymond | Compilation efficace d'un langage déclaratif synchrone : Le générateur de code Lustre-V3[END_REF][START_REF] Caspi | Synchronous Kahn Networks[END_REF][START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF], but handles streams of arbitrary element type, such as streams of streams, as well as higher-order functions.

We owe a particularly large debt to Lucid Synchrone [START_REF] Pouzet | Lucid Synchrone, version 3. Tutorial and reference manual[END_REF], whose compiler introduced the idea of type-checking program states in a higher-order reactive language more than twenty years ago. In contrast with the present work, in Lucid Synchrone state types are almost 4invisible at the source level and only appear in the generated OCaml code, relying on the OCaml compiler for this part of type-checking. Our choice to include state types in the source type system simplifies metatheoretical proofs and would facilitate an implementation of separate compilation. However, the absence of recursive state types forces us to reject many higher-order programs (see Section 4.2), some of which are accepted by Lucid Synchrone.

Functional reactive programming. Several works in functional reactive programming use techniques similar to that of synchronous programming. For example, causal commutative arrows [START_REF] Liu | Causal commutative arrows[END_REF] can be compiled to simple state-passing code but are purely first-order.

Several recent proposals such as that of Krishnaswami [START_REF] Neelakantan | Higher-Order Functional Reactive Programming without Spacetime Leaks[END_REF] or Bahr et al. [START_REF] Bahr | The Clocks Are Ticking: No More Delays! Reduction Semantics for Type Theory with Guarded Recursion[END_REF] exploit a modal type discipline to reject certain recursion patterns and rule out implicit memory leaks in an expressive higher-order language. In their operational semantics, program state is untyped and dynamically allocated in a global store, while in ours it is typed and thus controlled by term structure. An in-depth comparison of the two styles remains for future work.

Conclusion

We have presented a new operational semantics for λ * , a λ-calculus for productive reactive programming proposed in previous work. This semantics, in contrast with the existing one, is incremental. It can be seen as an adaptation of classic synchronous-language compilation techniques to a setting featuring rich temporal types such as streams of streams or streams of stream functions. Our incremental semantics enjoys the same desirable metatheoretical properties: type safety, totality, and determinism. Using a logical relation to specify how prefixes can be sliced into families of incremental values, we have proved that it is fully consistent with respect to the existing semantics.

In future work, we plan to refine the space usage of the new semantics, extend it beyond streams to arbitrary guarded recursive types, and capture its incremental character in a denotational model by adapting the existing interpretation of λ * in the topos of trees. We would also like to adapt it into an implementation.

A Interesting proofs

A.1 Inversion and construction lemmas

A.1.1 Inversion lemmas Lemma A.1 (Inversion lemma for by). Let 0 < n ω. Suppose that:

M by p stop ; (γ j ) p(i) j<p(i+1) i<n n = ⇒ s ; (δ i ) i<n
Then, we have:

∃s . ∃(δ i ) i<p(n) .              M stop ; (γ i ) i<p(n) p(n) = == ⇒ s ; (δ i ) i<p(n) δ i = (δ j ) p(i)<j p(i+1) for all i < n s = w (p, s ) if n < ω done otherwise
Proof. By induction on n.

• Case n = 1 . By hypothesis and inversion of EStep we have:

M by p stop ; (γ i ) i<p(1) = ⇒ s ; δ 0
Then, by inversion of EByI, we obtain what we wanted:

M stop ; (γ i ) i<p(1) p(1) ==⇒ s ; (δ i ) i<p(1) δ 0 = (δ i ) i<p(1) s = w (p, s )
• Case 1 < n < ω . By hypothesis and inversion of EStep we have:

M by p stop ; (γ j ) p(i) j<p(i+1) i<n-1 n-1 = == ⇒ s I ; (δ i ) i<n-1 (a) M by p s I ; (γ j ) p(n-1) j<p(n) = ⇒ s ; δ n (b)
Applying the induction hypothesis to (a) yields:

M stop ; (γ i ) i<p(n-1) p(n-1) ====⇒ s I ; (δ i ) i<p(n-1) (c)
δ i = (δ j ) p(i)<j p(i+1) ∀i < n -1 (d) s I = w (p, s I ) (e)
Now, we distinguish two cases.

p(n -1) = ω. In this case, s I = done, p(n) = ω and ∂p(n) = 0. We have by EZero that :

M s I ; ε ∂p(n) ===⇒ s I ; ε Thus, δ n-1 = ε. Substituting p(n -1) = p(n) = ω
M stop ; (γ i ) i<p(n) p(n) = == ⇒ s ; (δ i ) i<p(n) δ i = (δ j ) p(i)<j p(i+1) ∀i < n s = w (p, s ) = w (p, done)
p(n -1) < ω. In this case, s I = w (p, s I ). By substituting (e) in (b) and then inverting EBy, we obtain:

M s I ; (γ i ) p(n-1) i<p(n) ∂p(n) ===⇒ s ; (δ i ) p(n-1) i<p(n) (f) δ n-1 = (δ j ) p(n-1)<j p(n) (g) s = w (p, s ) if ∂p(n) < ω done otherwise (h) Notice that if ∂p(n) = ω, then p(n) = ω
Since p(n) = p(n -1) + ∂p(n), combining (c) and (f) yields what we wanted:

M stop ; (γ i ) i<p(n) p(n) = == ⇒ s ; (δ i ) i<p(n) δ i = (δ j ) p(i)<j p(i+1) ∀i < n s = w (p, s ) if p(n) < ω done otherwise • Case n = ω .
By hypothesis and inversion of EOmega we have:

∀m < ω. M by p stop ; (γ j ) p(i) j<p(i+1) i<m m = ⇒ s m ; (δ i ) i<m
The induction hypothesis applies, and gives :

∀m < ω.    M stop ; (γ i ) i<p(m) p(m) = == ⇒ s p(m) ; (δ i ) i<p(m) δ i = (δ j ) p(i)<j p(i+1) ∀i < m (i)
By inversion of EOmega on the hypothesis we have that s = done. By (i), we obtain that ∀i < ω. δ i = (δ j ) p(i)<j p(i+1) .

We conclude in different ways depending on the finiteness of p(ω).

p(ω) = ω. Let k < ω. Since p is monotonic due to being a time warp, and p(ω) = ω, there exists a M such that k p(M ). By p(M ) -k inversions of EStep (or EOmega if p(M ) = ω), we obtain that :

∃s k . M stop ; (γ i ) i<k k = ⇒ s k ; (δ i ) i<k
Thus, we have that :

∀k < ω. M stop ; (γ i ) i<k k = ⇒ s k ; (δ i ) i<k
Immediately applying EOmega and substituting p(ω) = ω, we obtain :

M stop ; (γ i ) i<p(ω) p(ω) = == ⇒ done ; (δ i ) i<p(ω)
Which concludes our proof.

p(ω) < ω. In this case, p is ultimately constant: there is some finite M such that p(M ) = p(ω). Thus, by instantiating (i) with m := M , we obtain :

M stop ; (γ i ) i<p(M ) p(M ) ===⇒ s M ; (δ i ) i<p(M )
By substituting p(M ) for p(ω) in the above, we prove that:

M stop ; (γ i ) i<p(ω) p(ω) = == ⇒ s M ; (δ i ) i<p(ω)
Which concludes our proof.

Lemma A.2 (Inversion lemma for rec). Let 0 < n ω. Suppose that:

rec x A . M stop ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n
Then, we have:

∃s .        M stop ; γ 0 ε/ x ⊕ γ i (δ i-1 )/ x 1 i<n n = ⇒ s ; (δ i ) i<n s = s , inc (δ i ) i<n if n < ω done otherwise
Proof. By induction on n.

• Case n = 1 . By hypothesis and inversion of EStep we have:

rec x A . M stop ; γ 0 = ⇒ s ; δ 0
Then, by inversion of EFixI, we obtain:

M stop ; γ 0 ε/ x = ⇒ s ; δ 0 s = s , inc (δ)
Applying

EStep yields what we wanted.

• Case 1 < n < ω . By hypothesis and inversion of EStep we have:

rec x A . M stop ; (γ i ) i<n-1 n-1 = == ⇒ s I ; (δ i ) i<n-1 (a) rec x A . M s I ; γ n-1 = ⇒ s ; δ n-1 (b)
Applying the induction hypothesis to (a) yields :

M stop ; γ 0 ε/ x ⊕ γ i (δ i-1 )/ x 1 i<n-1 n-1 = == ⇒ s I ; (δ i ) i<n-1 (c)
s I = s I , inc (δ i ) i<n-1 (d)
By substituting (d) in (b) and then inverting ERec, we obtain:

M s I ; γ n-1 (δ n-2 )/ x = ⇒ s ; δ n-1 (e) s = s , inc (δ i ) i<n (f)
Together with (f), applying EStep to (c) and (e) yields what we wanted:

M stop ; γ 0 ε/ x ⊕ γ i (δ i-1 )/ x 1 i<n n = ⇒ s ; (δ i ) i<n s = s , inc (δ i ) i<n
• Case n = ω . By hypothesis and inversion of EOmega we have s = done and:

∀m < ω. rec x A . M stop ; (γ i ) i<m m = ⇒ s m ; (δ i ) i<m
The induction hypothesis applies, and gives :

∀m < ω. M stop ; γ 0 ε/ x ⊕ γ i (δ i-1 )/ x 1 i<m m = ⇒ s m ; (δ i ) i<m
Applying EOmega to the above equation gives what we wanted.

Lemma A.3 (Inversion lemma for delay). Let 0 < n ω. Suppose that:

delay q p (M ) stop ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n
Then, we have:

∃s . ∃(δ i ) i<p(n) .              M stop ; (γ i ) i<n n = ⇒ s ; (δ i ) p(i)<j p(i+1) i<n δ i = (δ j ) q(i)<j q(i+1) for all i < n s = s , inc (δ j ) p(i) j<p(i+1) i<n if n < ω done otherwise
Proof. By induction on n.

• Case n = 1 . By hypothesis and inversion of EStep we have:

delay q p (M ) stop ; γ 0 = ⇒ s ; δ 0
Then, by inversion of EDelayI and immediate application of EStep, we obtain what we wanted:

M stop ; (γ 0 ) 1 = ⇒ s ; (δ i ) i<q(1) δ 0 = (δ i ) i<q(1) s = s , inc (δ i ) i<p(1)
• Case 1 < n < ω . By hypothesis and inversion of EStep we have:

delay q p (M ) stop ; (γ i ) i<n-1 n-1 = == ⇒ s I ; (δ i ) i<n-1 (a)
delay q p (M ) s I ; γ n = ⇒ s ; δ n (b)
Applying the induction hypothesis to (a) yields:

M stop ; (γ i ) i<n-1 n-1 = == ⇒ s I ; (δ i ) p(i)<j p(i+1) i<n-1 (c)
δ i = (δ j ) q(i)<j q(i+1) for all i < n -1 (d)
s I = s I , inc (δ j ) p(i) j<p(i+1) i<n-1 (e)
Now, by substitution of (e) in (b) and immediate inversion of EDelay, we get:

M s I ; γ n = ⇒ s ; (δ i ) p(n-1)<j p(n) (f) δ n = (δ j ) q(n-1)<j q(1) (g)
s = s , inc (δ j ) p(i) j<p(i+1) i<n (h)
Applying EStep on (c) and (f), merging (d) with (g), and (h) yield what we wanted:

M stop ; (γ i ) i<n n = ⇒ s ; (δ i ) p(i)<j p(i+1) i<n δ i = (δ j ) q(i)<j q(i+1) for all i < n s = s , inc (δ j ) p(i) j<p(i+1) i<n
• Case n = ω . By hypothesis and inversion of EOmega we have:

∀m < ω. delay q p (M ) stop ; (γ i ) i<m m = ⇒ s m ; (δ i ) i<m
The induction hypothesis applies, and gives :

∀m < ω. M stop ; (γ i ) i<m m = ⇒ s m ; (δ i ) p(i)<j p(i+1) i<m δ i = (δ j ) q(i)<j q(i+1) for all i < m (i)
By inversion of EOmega on the hypothesis we have that s = done. By (i), we obtain that ∀i < ω. δ i = (δ j ) q(i)<j q(i+1) .

Applying EOmega on (i) gives:

M stop ; (γ i ) i<ω ω = ⇒ done ; (δ i ) p(i)<j p(i+1) i<ω
Which concludes our proof.

A.1.2 Construction lemmas

Lemma A.4 (Construction lemma for variables). Let 0 < n ω. Let (γ i ) i<n , such that:

∀i < n. x ∈ dom(γ i (x))
Then, we have:

x stop ; (γ i ) i<n n = ⇒ s ; (γ i (x)) i<n -with s = unit if n < ω done elsewise
Proof. By induction on n.

• Case n = 1 . By hypothesis, since x ∈ dom(γ 0 ), then EVarI applies and yields:

x stop ; γ 0 = ⇒ unit ; γ 0 (x)

Immediate application of

EStep yields what we wanted.

• Case 1 < n < ω . The induction hypothesis gives:

x stop ; (γ i ) i<n-1 n-1 = == ⇒ unit ; (γ i (x)) i<n-1
By hypothesis, since x ∈ dom(γ n-1 ), then EVar applies and yields:

x unit ; γ n-1 = ⇒ unit ; γ n-1 (x)

Immediate application of

EStep yields what we wanted.

• Case n = ω . Since x ∈ dom(γ m ) for all m < ω, the induction hypothesis applies and gives:

∀m < ω. x stop ; (γ i ) i<m m = ⇒ unit ; (γ i (x)) i<m

Immediate application of

EOmega yields what we wanted.

Lemma A.5 (Construction lemma for by). Let 0 < n ω. Suppose that:

M stop ; (γ i ) i<p(n) p(n) = == ⇒ s ; (δ i ) i<p(n)
Then, we have:

M by p stop ; (γ j ) p(i) j<p(i+1) i<n n = ⇒ s ; (δ j ) p(i) j<p(i+1) i<n
With s such that:

s = w (p, s ) if n < ω done elsewise
Proof. By induction on n.

• Case n = 1 . By hypothesis we have:

M stop ; (γ i ) i<p (1) p(1)
==⇒ s ; (δ i ) i<p(1)
Notice that since p is a time warp, p(0) = 0. We apply EByI:

M by p stop ; (δ j ) p(0) j<p(1) = ⇒ w (p, s ) ; (γ j ) p(0) j<p(1)

Applying

EStep yields what we wanted.

• Case 1 < n < ω . By hypothesis and inversion of EStep we have:

M stop ; (γ i ) i<p(n-1) p(n-1) ====⇒ s I ; (δ i ) i<p(n-1) (a)
M s I ; (γ i ) p(n-1) i<p(n) ∂p(n) ===⇒ s ; (δ i ) p(n-1) i<p(n) (b)
Applying the induction hypothesis to (a), and EBy to (b) yields :

M by p stop ; (γ j ) p(i) j<p(i+1) i<n-1 n-1 = == ⇒ w (p, s I ) ; (δ j ) p(i) j<p(i+1) i<n-1 M by p w (p, s I ) ; (γ j ) p(n-1) j<p(n) = ⇒ w (p, s ) ; (δ j ) p(n-1) j<p(n)

Immediate application of

EStep yields what we wanted:

M by p stop ; (γ j ) p(i) j<p(i+1) i<n n = ⇒ w (p, s ) ; (δ j ) p(i) j<p(i+1) i<n
• Case n = ω . By hypothesis we have:

M stop ; (γ i ) i<p(ω) p(ω) = == ⇒ s ; (δ i ) i<p(ω) (c)
We distinguish to cases, depending on the value of p(ω).

-Case p(ω) < ω. p is ultimately constant -this means that there is a finite N such that p(N ) = p(ω). Thus, (c) rewrites to:

M stop ; (γ i ) i<p(N ) p(N ) = == ⇒ s ; (δ i ) i<p(N )
By application of the induction hypothesis, we obtain:

M by p stop ; (γ j ) p(i) j<p(i+1) i<N N = ⇒ w (p, s ) ; (δ j ) p(i) j<p(i+1) i<N (d)
By EZero, we always have M s ; ε 0 = ⇒ s ; ε. Thus, by EBy:

M by p w (p, s ) ; ε = ⇒ w (p, s ) ; ε
Notice that since p is ultimately constant at N , then for all m N , we have:

(γ i ) p(m) i<p(m+1) = (δ i ) p(m) i<p(m+1) = ε
Thus, EStep applies any number of times to (d) and yields:

∀m < ω. M by p stop ; (γ j ) p(i) j<p(i+1) i<m m = ⇒ w (p, s ) ; (δ j ) p(i) j<p(i+1) i<m
Applying EOmega proves what we wanted.

-Case p(ω) = ω. Immediate inversion of EOmega in (c) yields:

∀m < ω. M stop ; (γ i ) i<m m = ⇒ s m ; (δ i ) i<m
This especially gives: Applying EOmega proves what we wanted.

Lemma A.6 (Construction lemma for rec). Let 0 < n ω. Suppose that:

M stop ; γ 0 ε/ x ⊕ γ i (δ i-1 )/ x 1 i<n n = ⇒ s ; (δ i ) i<n
Then, we have:

rec x A . M stop ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n -with s = (s , inc ((δ i ) i<n )) if n < ω done elsewise
Proof. By induction on n.

• Case n = 1 . By hypothesis and inversion of EStep we have:

M stop ; γ 0 ε/ x = ⇒ s ; δ 0
Then, by application of EFixI, we obtain:

rec x A . M stop ; γ 0 = ⇒ (s , inc (δ 0 )) ; δ 0
Applying EStep yields what we wanted.

• Case 1 < n < ω . By hypothesis and inversion of EStep we have:

M stop ; γ 0 ε/ x ⊕ γ i (δ i-1 )/ x 1 i<n-1 n-1 = == ⇒ s I ; (δ i ) i<n-1 (a) M s I ; γ n-1 (δ n-2 )/ x = ⇒ s ; δ n-1 (b)
Applying the induction hypothesis to (a), and ERec to (b) yields :

rec x A . M stop ; (γ i ) i<n-1 n-1 = == ⇒ (s I , inc ((δ i ) i<n-1 )) ; (δ i ) i<n-1 rec x A . M (s I , inc ((δ i ) i<n-1 )) ; γ n-1 = ⇒ (s , inc ((δ i ) i<n )) ; δ n-1

Immediate application of

EStep yields what we wanted:

rec x A . M stop ; (γ i ) i<n n = ⇒ (s , inc ((δ i ) i<n )) ; (δ i ) i<n
• Case n = ω . By hypothesis and inversion of EOmega we have:

∀m < ω. M stop ; γ 0 ε/ x ⊕ γ i (δ i-1 )/ x 1 i<m m = ⇒ s m ; (δ i ) i<m
Applying the induction hypothesis gives:

∀m < ω. rec x A . M stop ; (γ i ) i<m m = ⇒ s m , inc (δ i ) i<m ; (δ i ) i<m

Immediate application of

EOmega yields what we wanted.

A.2 Metatheory

A.2.1 Preliminaries

We first prove some preliminary theorems.

Theorem A.1 (Type safety of increment truncation). If (δ i ) i<n : A @ n and m n then (δ i ) i<m : A @ m.

Proof. Let m < n, and (δ i ) i<n : A @ n. In the case where m = 0, then (δ i ) i<m = ε. Consequently, we have (δ i ) i<m : A @ m by rule IStop, which proves what we wanted. In all the following, we thus suppose that m > 0. We proceed by induction over the typing judgement.

• Rule IStop . We have n = 0, and (δ i ) i<n = ε. Since m > 0 by the above and m n, this case never happens (we have already demonstrated that the theorem always holds when m = 0).

• Rule IScalar . We have n > 0, (δ i ) i<n = (c) ⊕ (nil) i<n and A = ν. Since m > 0, rule IScalar gives that (c) ⊕ (nil) i<m . This proves what we wanted.

• Rule IProd . We have n > 0, (δ i ) i<n = (δ 1 i , δ 2 i )

i<n and A = A 1 × A 2 . Inversion of rule IProd gives that (δ 1 i ) i<n : A 1 @ n and (δ 2 i ) i<n : A 2 @ n. The induction hypothesis gives us that (δ 1 i ) i<m : A 1 @ m and (δ 2 i ) i<m : A 2 @ m. Immediate application of rule IProd allows us to conclude that (δ

1 i , δ 2 i ) i<m : A 1 × A 2 @ m.
This proves what we wanted.

• Rule IInj . We have n > 0, (δ i ) i<n = (inj j (δ i )) i<n and A = A 1 +A 2 . Inversion of rule IInj gives that (δ i ) i<n : A j @ n. The induction hypothesis gives us that (δ i ) i<m : A j @ m. Immediate application of rule IInj allows us to conclude that (inj j (δ i )) i<m :

A 1 + A 2 @ m.
This proves what we wanted.

• Rule IWarp . We have n > 0, (δ i ) i<n = (δ j ) p(i) j<p(i+1) i<n and A = p A . Inversion of rule IWarp gives that (δ i ) i<p(n) : A @ p(n). Since m n =⇒ p(m) p(n), the induction hypothesis gives us that (δ i ) i<p(m) : A @ p(m). Immediate application of rule IWarp allows us to conclude that (δ j ) p(i) j<p(i+1) i<m : p A @ m. This proves what we wanted.

• Rule IClo . We have n > 0, (δ i ) i<n = (x.M ){γ i } i<n and A = A • Rule IStream . We have n > 0, (δ i ) i<n = (δ 1 i :: δ 2 i ) i<n and A = Str A . Inversion of rule IStream gives that (δ 1 i ) i<n : A @ n and (δ 2 i ) i<n : lat Str A @ n. The induction hypothesis gives us that (δ 1 i ) i<m : A @ m and (δ 2 i ) i<m : lat Str A @ m. Immediate application of rule IStream allows us to conclude that (δ 1 i ::

δ 2 i ) i<m : Str A @ m.
This proves what we wanted.

• Rule IBox . We have n = ω. If m = ω, we are done. Suppose m < n. Inversion of rule IBox gives that ∀k < ω. (δ i ) i<k : A @ k. Since m < ω, this especially gives us that (δ i ) i<m : A @ m. This proves what we wanted.

• Rule IEnv . We have (γ i ) i<n : Γ @ n. Inversion IEnv gives that dom(Γ) = dom (γ i ) for all i < n, and (γ i (x)) i<n : Γ(x) @ n for all x ∈ dom(Γ). Since m n, we also have dom(Γ) = dom (γ i ) for all i < m. Furtherore, the induction hypothesis applies, and gives (γ i (x)) i<m : Γ(x) @ m for all x ∈ dom(Γ). Immediate application of rule IEnv allows us to conclude that (γ i ) i<m : Γ @ m. This proves what we wanted.

A.2.2 Determinism

In the following, Theorem A.2 and Lemma A.7 are proved by mutual induction.

Theorem A.2 (Determinism). If M s; (γ i ) i<n n = ⇒ s 1 ; (δ 1 i ) i<n and M s; (γ i ) i<n n = ⇒ s 2 ; (δ 2 i ) i<n , then s 1 = s 2 and δ 1 i = δ 2 i for all i.
Proof. Let us denote:

(π 1 ) ≡ M s ; (γ i ) i<n n = ⇒ s 1 ; (δ 1 i ) i<n (π 2 ) ≡ M s ; (γ i ) i<n n = ⇒ s 2 ; (δ 2 i ) i<n
We proceed by structural induction over (π 1 ).

• Rule EZero . We have n = 0, (δ 1 i ) i<0 = ε and s 1 = s. Thus, substitution in (π 2 ) and immediate inversion yields that rule EZero applies and (δ 2 i ) i<0 = ε and s 2 = s. This gives the following, which concludes the proof:

(δ 1 i ) i<0 = (δ 2 i ) i<0 = ε s 1 = s 2 = s • Rule EStep .
We have 1 n < ω, and:

M s ; (γ i ) i<n-1 n-1 = == ⇒ s 1 ; (δ 1 i ) i<n-1 (a) M s 1 ; γ n-1 = ⇒ s 1 ; δ 1 n-1 (b)
Substitution of n in (π 2 ) and immediate inversion yields that rule EStep applies, and:

M s ; (γ i ) i<n-1 n-1 = == ⇒ s 2 ; (δ 2 i ) i<n-1 (c) M s 2 ; γ n-1 = ⇒ s 2 ; δ 2 n-1 (d)
Application of the induction hypothesis over eq. (a) and eq. (c) gives:

δ 1 i = δ 2 i forall i < n -1 s 1 = s 2
Application of the mutual induction hypothesis yields that Lemma A.7 applies on eq. (b) and eq. (d):

δ 1 n-1 = δ 2 n-1 s 1 = s 2
This gives the following, which concludes the proof:

δ 1 i = δ 2 i forall i < n s 1 = s 2
• Rule EOmega . We have n = ω, and:

∀m < ω. M s ; (γ i ) i<m m = ⇒ s 1,m ; (δ 1 i ) i<m (e) s 1 = done (f)
Substitution of n in (π 2 ) and immediate inversion yields that rule EStep applies, and:

∀m < ω. M s ; (γ i ) i<m m = ⇒ s 2,m ; (δ 2 i ) i<m (g) s 2 = done (h)
Application of the induction hypothesis over eq. (e) and eq. (g) gives:

δ 1 m = δ 2 m forall m < ω s 1,m = s 2,m
The above especially gives (δ 1 i ) i<ω = (δ 2 i ) i<ω . Since s 1 = s 2 = done, this concludes the proof.

Lemma A.7 (Determinism, single-step). If we have M s ; γ = ⇒ s 1 ; δ 1 and M s ; γ = ⇒ s 2 ; δ 2 then s 1 = s 2 and δ 1 = δ 2 .

Proof. Let us denote:

(π 1 ) ≡ M s ; γ = ⇒ s 1 ; δ 1 (π 2 ) ≡ M s ; γ = ⇒ s 2 ; δ 2
We proceed by structural induction over (π 1 ). For most cases, immediate inversion of the rule gives us values for M , s and γ. Then, by substitution, we notice that inversion of (pi 2 ) gives the exact same rule. Application of the induction hypothesis yields the desired result. The only cases which requires a slightly different argument are those of rules EBy and EByI. Since their premises make use of the many-step judgement, we must use Theorem A.2 by using the mutual induction hypothesis. Due to the large number of rules and the many uninteresting cases, we will give a detailed proof only for those two cases, and rule EPair (as a more general example).

• Rule EPair . We have:

N s N ; γ = ⇒ s 1,N ; δ 1,N P s P ; γ = ⇒ s 1,P ; δ 1,P (N, P ) =M (s N , s P ) =s ; γ = ⇒ (s 1,N , s 1,P ) =s 1 ; (δ 1,N , δ 1,P ) =δ1 (a)
By immediate substitution of M , s and γ in (π 2 ), we obtain that its last deduction rule is also EPair. This gives: By the induction hypothesis, we have s 1,N = s 2,N , s 1,P = s 2,P , as well as δ 1,N = δ 2,N and δ 1,P = δ 2,P . Thus, we have the following, which concludes the proof:

s 1 = (s 1,N , s 1,P ) = (s 2,N , s 2,P ) = s 2 δ 1 = (δ 1,N , δ 1,P ) = (δ 2,N , δ 2,P ) = δ 2
• Rule EByI . We have:

N stop ; (γ i ) i<p(1) p(1) ==⇒ s 1 ; (δ 1 i ) i<p(1) N by p =M stop =s ; (γ i ) i<p(1) =γ = ⇒ w (p, s 1 ) =s 1 ; (δ 1 i ) i<p(1) =δ1 (c)
By immediate substitution of M , s and γ in (π 2 ), we obtain that its last deduction rule is also EByI. This gives:

N stop ; (γ i ) i<p(1) p(1) ==⇒ s 2 ; (δ 2 i ) i<p(1) N by p =M stop =s ; (γ i ) i<p(1) =γ = ⇒ w (p, s 2 ) =s 2 ; (δ 2 i ) i<p(1) =δ2 (d)
Inversion of eq. (c) and eq. (d) yields:

N stop ; (γ i ) i<p(1) p(1) ==⇒ s 1 ; (δ 1 i ) i<p(1) N stop ; (γ i ) i<p(1) p(1)
==⇒ s 2 ; (δ 2 i ) i<p(1) By the mutual induction hypothesis, Theorem A.2 applies and gives s 1 = s 2 , and δ 1 i = δ 2 i for all i < p(1). Thus, we have the following, which concludes the proof:

s 1 = w (p, s 1 ) = w (p, s 2 ) = s 2 δ 1 = (δ 1 i ) i<p(1) = (δ 2 i ) i<p(1) = δ 2
• Rule EBy . We have:

N s N ; (γ i ) i<∂p(n) ∂p(n) ===⇒ s 1 ; (δ 1 i ) i<∂p(n) N by p =M w (p, s N ) =s ; (γ i ) i<∂p(n) =γ = ⇒ w (p, s 1 ) =s 1 ; (δ 1 i ) i<∂p(n) =δ1 (e)
By immediate substitution of M , s and γ in (π 2 ), we obtain that its last deduction rule is also EBy. This gives:

N s N ; (γ i ) i<∂p(n) ∂p(n) ===⇒ s 2 ; (δ 2 i ) i<∂p(n) N by p =M w (p, s N ) =s ; (γ i ) i<∂p(n) =γ = ⇒ w (p, s 2 ) =s 2 ; (δ 2 i ) i<∂p(n) =δ2 (f)
Inversion of eq. (e) and eq. (f) yields:

N s N ; (γ i ) i<∂p(n) ∂p(n) ===⇒ s 1 ; (δ 1 i ) i<∂p(n) N s N ; (γ i ) i<∂p(n) ∂p(n)
===⇒ s 2 ; (δ 2 i ) i<∂p(n) By the mutual induction hypothesis, Theorem A.2 applies and gives s 1 = s 2 , and δ 1 i = δ 2 i for all i < p(1). Thus, we have the following, which concludes the proof:

s 1 = w (p, s 1 ) = w (p, s 2 ) = s 2 δ 1 = (δ 1 i ) i<p(1) = (δ 2 i ) i<p(1) = δ 2 A.2.

Type safety

In order to simplify our proof, we deal with the base case n = 0 in a separate lemma.

Lemma A.8 (Type safety at n = 0). Let Γ M : A | S. Proof. Let M be a well-typed term such that (π) : Γ M : A | S. By induction over (π). Almost all cases can be dealt with by inverting the typing derivation, obtaining the shape of the term, observing that subject reduction holds for subterms due to the induction hypothesis, and using these hypotheses to conclude that the property holds for the term. Thus, we will focus on three nontrivial examples -By, Rec, and Delay.

If we have

(γ i ) i<0 : Γ @ 0 M stop ; (γ i ) i<0 0 = ⇒ s ; (δ i ) i<0 -then (δ i ) i<0 : A @ 0 s : S a O 0 Proof. Since n = 0, (γ i ) i = ε.
• Case Rec . We have Γ rec x A . M : A | S × ∫A. By inversion of Rec, we obtain:

Γ, x : lat A M : A | S (a)
Now, we proceed by induction over n ∈ ω + 1.

n = 0. True by Lemma A.8.

-1 n < ω. Suppose that we have:

(γ i ) i<n : Γ @ n (b) rec x A . M stop ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n (c)
By inversion of EStep in (c), we also have:

rec x A . M stop ; (γ i ) i<n-1 n-1 = == ⇒ s I ; (δ i ) i<n-1 (d)
By Theorem A.1, we have (γ i ) i<n-1 : Γ @ n -1. Thus, the induction hypothesis over n applies to (d), and immediate application of IWarp yields:

(δ i ) i<n-1 : A @ n -1 ( ε) ⊕ (δ i-1 ) 1 i<n : lat A @ n (e)
Applying IEnv to (b) and (e) gives:

γ 0 ε/ x ⊕ γ i (δ i-1 )/ x 1 i<n : lat A @ n (f)
Finally, we apply Lemma A.2 to (d) -this yields:

∃s .    M stop ; γ 0 ε/ x ⊕ γ i (δ i-1 )/ x 1 i<n n = ⇒ s ; (δ i ) i<n s = s , inc (δ i ) i<n (g)
Inversion of IEnv and IWarp in (b) gives:

∃(γ i ) i<p(n) . (γ i ) i<p(n) : Γ @ p(n) γ i = (γ j ) p(i) j<p(i+1) for all i < n (d)
Substitution of (d) in (c) and immediate application of Lemma A.1 yields:

∃s . ∃(δ i ) i<p(n) .              M stop ; (γ i ) i<p(n) p(n) = == ⇒ s ; (δ i ) i<p(n) δ i = (δ j ) p(i)<j p(i+1) for all i < n s = w (p, s ) if n < ω done elsewise (e)
Since (d) gives that (γ i ) i<p(n) : Γ @ p(n), and (a) gives that M is well-typed -the induction hypothesis applies on (e) and gives: • Case Delay . We have Γ delay q p (M ) : q A | S × ∫(p A). By inversion of Delay, δ i = (δ j ) q(i)<j q(i+1) for all i < n s = s , inc (δ j ) p(i) j<p(i+1) i<n if n < ω done otherwise (d)

(δ i ) i<p(n) : A @ p(
Since (b) gives that (γ i ) i<n : Γ @ n, and (a) gives that M is well-typed -the induction hypothesis applies on (d) and gives:

(δ i ) p(i)<j p(i+1) i<n : p A @ n (e)

s : S a O n (f)
Inversion of IWarp in (e) gives that (δ i ) i<p(n) : A @ p(n). Since the typing of increments is monotonic (cf. Theorem A.1), and q(n) p(n) (for we have q p by (a)) -we have that (δ i ) i<q(n) : A @ q(n).

Immediate application of IWarp proves that:

(δ i ) q(i)<j q(i+1) i<n : q A @ n (g)

If n = ω, then s = done, and SDone immediately gives that s : S a O ω. Otherwise, if n < ω, application of SIncr on (e) followed immediate application of SPair with (f) give: Proof. Let M be a well-typed term such that (π) : Γ M : A | S. By induction over (π).

• Var . Inversion of this rule gives M = x and x ∈ dom(Γ) -(π) rewrites to :

Γ , x : A Γ x : A | 1 (a)
We proceed by case over n.

n = 0. By immediate application of EZero.

n > 0. Suppose we have (γ i ) i<n : Γ @ n. Inversion of IEnv yields that for all i < n, we have dom(γ i ) = dom(Γ). Since (a) gives x ∈ dom(Γ), we have that for all i < n, x ∈ dom(γ i ). Thus, Lemma A.4 applies, which proves what we wanted.

• Rec . We have Γ rec x A . M : A | S × ∫A. Immediate inversion of Rec gives:

Γ, x : lat A M : A | S (a)
By induction over n.

n = 0. By immediate application of EZero.

-1 n < ω. Suppose we have (γ i ) i<n : Γ @ n. Since increment typing is monotonic (cf. Theorem A.1), it also gives (γ i ) i<n-1 : Γ @ n -1. Thus, the induction hypothesis over n applies and gives: (δ i ) i<n-1 : A @ n -1 ( ε) ⊕ ( (δ i-1 )) 1 i<n : lat Γ @ n γ 0 ε/ x ⊕ γ i (δ i-1 )/ x 1 i<n : Γ, x : lat A @ n This allows us to apply on the subterm N the induction hypothesis over (π):

N stop ; γ 0 ε/ x ⊕ γ i (δ i-1 )
n = ω. Suppose we have (γ i ) i<ω : Γ @ ω. Inversion of IBox and IEnv gives that for all m < ω, we have (γ i ) i<m : Γ @ m. Thus, the induction hypothesis over n applies and gives: We proceed by case over n.

n = 0. By immediate application of EZero.

n > 0. Suppose we have (γ i ) i<n : p Γ @ n. Inversion of IWarp and IEnv gives:

∃(γ i ) i<p(n) .
(γ i ) i<p(n) : A @ p(n) γ i = γ j p(i) j<p(i+1) for all i < n (b) Thus, the induction hypothesis applies on (a) and yields: Such that for all k n:

M stop ; (γ i ) i<p(n) p(n) = ==
∀(δ i ) i<k |= A1 k V , ∃s, (δ i ) i<k , V ,      M stop ; γ i δ i / x i<k k = ⇒ s ; (δ i ) i<k N ; E k V / x ⇓ k V (δ i ) i<k |= A2 k V (a)
Let m n. If m = 0, Lemma A.10 proves what we wanted. Thus, suppose that 1 m < ω. Since m n, if the property (a) holds for all k n, it also holds for all k m. Due to the functoriality of truncation, we have that E m k = E min(k,m) . However, when k m, this rewrites as E m k = E k . All of these arguments thus yield that, for all k m: Proof. Let M be a well-typed term such that (π) : Γ M : A | S. By induction over (π).

∀(δ i ) i<k |= A1 k V , ∃s, (δ i ) i<k , V ,      M stop ; γ i δ i / x i<k k = ⇒ s ; (δ i ) i<k N ; E m k V / x ⇓ k V (δ i ) i<k |= A2 k V (
• Var . Immediate inversion of (π) yields:

Γ , x : A Γ x : A | S (a)
Let n ω -let (γ i ) i<n : Γ @ n, and E : Γ @ n. Suppose that:

x stop ; (γ i ) i<n n = ⇒ -; (δ i ) i<n (b)
x ; E ⇓ n V (c)

(γ i ) i<n |= Γ n E (
(δ i ) i<ω |= A ω box(rec x A . M ){E}

  sum : Stream Nat -> Stream Nat sum xs = ys where rec ys = map2 (+) xs (0 :: ys)

GuardedRecΓFigure 1

 1 Figure 1 Guarded recursion

Figure 2

 2 Figure 2 Typing judgement for λ *

Figure 3

 3 Figure 3 Typing judgement for prefixes

  nil :: [1 :: [ ]] nil :: [nil :: [2 :: [ ]]]

Figure 11

 11 Figure 11 Many-step evaluation judgement

Theorem 3 . 5 .

 35 If M : Nat | S and M ; ∅ ⇓ 1 c then there is s such that M stop ; ∅ = ⇒ s ; c.

1 =

 1 ⇒ Str A Str S = == ⇒ Str B, reflecting how map f xs creates a new copy of the state of f for each element of xs.

  in the above equations yields what we wanted:

  ∀m < ω. M stop ; (γ i ) i<p(m) p(m) = == ⇒ s p(m) ; (δ i ) i<p(m) Applying the induction hypothesis gives: ∀m < ω. M by p stop ; (γ j ) p(i) j<p(i+1) i<m m = ⇒ w p, s p(m) ; (δ j ) p(i) j<p(i+1) i<m

S=

  ⇒ B. Inversion of rule IClo gives that Γ, x : A M : B | S and (γ i ) i<n : Γ @ n. The induction hypothesis gives us that (γ i ) i<m : Γ @ m. Immediate application of rule IClo allows us to conclude that (x.M ){γ i } i<m : A S = ⇒ B @ m. This proves what we wanted.

2 ;

 2 N s N ; γ = ⇒ s 2,N ; δ 2,N P s P ; γ = ⇒ s 2,P ; δ 2,P (N, P ) =M (s N , s P ) =s ; γ = ⇒ (s 2,N , s 2,P ) =s (δ 2,N , δ 2,P ) =δ2 (b) Inversion of eq. (a) and eq. (b) yields: N s N ; γ = ⇒ s 1,N ; δ 1,N P s P ; γ = ⇒ s 1,P ; δ 1,P N s N ; γ = ⇒ s 2,N ; δ 2,N P s P ; γ = ⇒ s 2,P ; δ 2,P

M

  we obtain: Γ M : p A | S and q p (a)If n = 0, Lemma A.8 proves what we want. Thus, suppose that n > 0. Let:(γ i ) i<n : Γ @ n (b)delay q p (M ) stop ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n (c)Application of Lemma A.3 yields:∃s . ∃(δ i ) i<p(n) . stop ; (γ i ) i<n n = ⇒ s ; (δ i ) p(i)<j p(i+1) i<n

  s , inc (δ i ) p(i)<j p(i+1) i<n : S × ∫(p A) a O n (h) Substitution of s and δ i in (h) and (g) yield what we wanted. A.2.4 Totality Theorem A.4 (Totality). Let Γ M : A | S, and n ω. For all (γ i ) i<n : Γ @ n, there exists s and (δ i ) i≤n such that M stop ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n .

1 =

 1 ∃s I . ∃(δ i ) i<n-1 . rec x A . N stop ; (γ i ) i<n-1 n-== ⇒ s I ; (δ i ) i<n-1 (b)By applying subject reduction (cf. Theorem A.3) on (b), then immediate application of IWarp and IEnv, we respectively obtain:

  ∀m < ω. ∃s m . rec x A . M stop ; (γ i ) i<m m = ⇒ s m ; (δ i ) i<mImmediate application ofEOmega yields what we wanted. • By . We have p Γ M by p : p A | p S. Immediate inversion of By gives us: Γ M : A | S (a)

  ⇒ s ; (δ i ) i<p(n) Applying Lemma A.5 proves what we wanted: M by p stop ; (γ i ) i<n n = ⇒ w (p, s ) ; (δ j ) p(i) j<p(i+1) i<n

  b) This is precisely the right hand side of the definition of the logical relation on functions. Thus, applying said relation to the above yields:((x.M ){γ i }) i<m |= A S = ⇒B m (x.N ){ E m } Immediate substitution of V m = (x.M ){ E m } and δ i = (x.M ){γ i } inthe above proves what we wanted. • Inductive case (A, ω). The induction hypothesis gives us that the property holds for each (A , n ) such that A < ty A ∨ (A = A ∧ n < ω). Let V , and (δ i ) i<ω such that (δ i ) i<ω |= A ω V . By definition of the logical relation, we have that: V = box(M ){E} st. for all m < ω, (δ i ) i<m |= A m box(M ){E} m Since m < ω implies that m n, the above equation proves what we wanted. A.3.2 Adequacy lemma Lemma A.12 (Adequacy). If Γ M : A | S, then M |= Γ A M .

  d) obtain:∀m < ω. rec x A . M stop ; (γ i ) i<m m = ⇒ s m ; (δ i ) i<m (r) ∀m < ω. (γ i ) i<m |= Γ m E m (s)The induction hypothesis obtained by our induction over n applied on the three above equations yields:∀m < ω. (δ i ) i<m |= A m box(rec x A . M){E} m By the definition of the logical relation given in Figure12, this gives what we wanted:

  By EZero, we have M stop ; ε Thus, (δ i ) i = ε and s = stop. Rules IStop and SStop yield (δ i ) i = ε : A @ 0 and s = stop : S a Theorem A.3 (Type safety). Let Γ M : A | S, and n ω. For all (γ i ) i<n : Γ @ n and (δ i ) i<n such that M stop ; (γ i ) i<n n = ⇒ s ; (δ i ) i<n , we have (δ i ) i<n : A @ n and s : S a O n.

	O	0 -which is what
	we wanted.
	Let us restate Theorem A.3:

0 = ⇒ stop ; ε.

  / x 1 i<n n = ⇒ s ; (δ i ) i<nImmediate application of Lemma A.6 proves what we wanted:rec x A . N stop ; (γ i ) i<n

n = ⇒ s , inc (δ i ) i<n ; (δ i ) i<n

The warping modality was denoted p * (-) in the original λ * paper[START_REF] Guatto | A Generalized Modality for Recursion[END_REF].

For brevity's sake, we do not make explicit how this function works. An explanation can be found in Guatto's original paper[START_REF] Guatto | A Generalized Modality for Recursion[END_REF]. We discuss this choice in more detail in Section 4.1.

They can be found in the full version of the paper, available at http://hal.archives-ouvertes.fr/ hal-03465519.

Lucid Synchrone distinguishes between functions of unit state type and functions of non-unit state types at the source level, grouping all of the former functions into a single type.

This work is supported by the Emergence project "ReaLiSe" funded by the city of Paris.

Since, by (a), and (f): Γ, x : lat A M : A | S γ 0 ε/ x ⊕ γ i (δ i-1 )/ x 1 i<n : lat A @ n Then, the induction hypothesis applies to (g) and yields:

Immediate application of SPair and SIncr gives us:

Which is what we wanted.

n = ω. Suppose that we have:

By inversion of EOmega in (i), we have:

By SDone, we obtain :

By applying Theorem A.1 on (h), then (γ i ) i<m : Γ @ m for all m. Consequently, the induction hypothesis applies on (k) and yields:

Which by immediate application of IBox yields:

In the end, (l) and (m) prove what we wanted.

• Case By . We have p Γ M by p : p A | p S. By inversion of By, we obtain:

If n = 0, Lemma A.8 proves what we want. Thus, suppose that n > 0.

Let:

A.3 Correctness

A.3.1 Preliminaries

Recall Lemma A.9, presented in Section 3.3.

Lemma A.9. If M ; E ; x ; V ⇑ k i V then for all j such that i j k, there is V such that M ; E j ; x ; V ⇑ j i V and M ; E ; x ; V ⇑ k j V . Proof. Let's proceed by induction over k -i.

• Base case . We have k -i = 0, which in turn gives gives i = j = k.

We have

. This concludes our proof for k = 0

Suppose the theorem is true for every value of k -i n.

If i = j, the theorem is trivially true, since rule PIFinish gives V = V . Thus, in all the following, we will suppose that j > i.

Suppose that N ; E ; x ; V ⇑ k+1 i V . By inversion of rule PIIter, we obtain:

Since i+1 j and (k+1)-(i+1) = n, applying the induction hypothesis on N ; E; x; V 0 ⇑ k+1 i+1

V is allowed, and yields:

Notice that i + 1 j gives that i < j. Now, consider the following proof tree:

Since all hypotheses hold, this proves that N ; E ; x ; V ⇑ j i V . Since we also had N ; E ; x ; V ⇑ k+1 j V , this concludes the proof. This lemma immediately implies the following result:

By Lemma A.9, with i = 0, j = n, k = n + 1. Then, notice that the iteration judgement over n n + 1 is equivalent to performing just one step of the reduction ⇒.

We then give the proof of Lemma A.11, which we will need in order to prove the full adequacy lemma. In order to do so, we need the following lemma, which handles the case of truncating a coherent slicing to a size of zero.

the proof immediately follows from the definition of the logical relation.

We now prove the general case.

We proceed by induction over the pair (A, n) using the well-founded lexicographical product order < ty × lex < ω+1 between the strict subtree ordering on types < ty and the canonical strict ordering < ω+1 on ω + 1.

• Case (A, 0). Let V , and

• Inductive case (A, n) with 1 n < ω. The induction hypothesis gives us that the property holds for each

Let V , and (δ i ) i<n such that (δ i ) i<n |= A n V . We now proceed by case over A:

-A = ν . By definition of the logical relation in Figure 12, we have V = c, δ 0 = c ∈ S ν , and δ i = nil for all i > 0. Let m n. If m = 0, Lemma A.10 proves what we wanted. Thus, suppose that 1 m < ω. By definition, we have that:

By definition of the logical relation in Figure 12, we have:

10 proves what we wanted. Thus, suppose that 1 m < ω. Since A 1 and A 2 are structural subtypes of A, the induction hypothesis applies and gives:

By definition of the logical relation, this gives:

in the above proves what we wanted.

By definition of the logical relation in Figure 12, we have:

10 proves what we wanted. Thus, suppose that 1 m < ω. Since A 1 and A 2 are structural subtypes of A, the induction hypothesis applies and gives:

By definition of the logical relation, this gives: -A = p A By definition of the logical relation in Figure 12, we have:

10 proves what we wanted. Thus, suppose that 1 m < ω. Since A 1 and A 2 are structural subtypes of A, the induction hypothesis applies and gives:

By definition of the logical relation, this gives:

Substitution of V m = w p, V p(m) and δ i = (δ j ) p(i) j<p(i+1) in the above proves what we wanted.

-A = Str A . By definition of the logical relation in Figure 12, we have:

10 proves what we wanted. Thus, suppose that 1 m < ω. Since (A , n) < lex (Str A , n) and (Str A , n -1) < lex (Str A , n), the induction hypothesis applies and gives:

By definition of the logical relation, this gives:

Substitution of V m = V m :: V m-1 and δ i = δ i :: (δ j ) i-1 j<i in the above proves what we wanted.

By definition of the logical relation in Figure 12, we have:

Notice that if n = 0, then by PZero and EZero, we have V = stop and (δ i ) i<n = ε. Therefore, by definition of the logical relation, we automatically have (δ i ) i<n |= A 0 V . Consequently, we will suppose that n > 0 in all the following.

By hypothesis, we have (γ i ) i<n : Γ @ n, and E : Γ @ n. Inversion of IEnv and VEnv yield:

By (a), we have that x ∈ dom(Γ). Thus, we have x ∈ dom(Γ) and ∀i < n. x ∈ dom(γ i ). From this, Lemma A.4 to (b) and inversion of PVar in (c) respectively yield:

Since x is in the domain of both environments, unfolding Definition 3.1 in (d) yields:

Immediate substitution of (e) concludes our proof.

• By . We have (π) : p Γ M by p : p A | p S. Immediate inversion of (π) yields:

Let n ω -let (γ i ) i<n : p Γ @ n, and E : p Γ @ n. Thus, there exists (γ i ) i<p(n) and E such that :

Now, suppose that:

Notice that if n = 0, then by PZero and EZero, we have V = stop and (δ i ) i<n = ε. Therefore, by definition of the logical relation, we have (δ i ) i<n |= A 0 V . We will thus suppose that n > 0 in all the following. By application of Lemma A.1 to (c), inversion of PWarp in (d), and unfolding the definition of the logical relation in (e), we obtain:

The induction hypothesis gives:

Its immediate application to (f), (g), and (h) yields:

V By definition of the logical relation, this gives:

By substition of the equalities given in (f) and (g), we obtain the following, which concludes our proof:

We have (π) : Γ rec x A . M : A | S × ∫A. Immediate inversion of (π) yields:

We want to prove that rec x A . M |= Γ A rec x A . M , whose definition is that for all n ω, ∀E, V.

∀s.

We prove the property by induction over n.

-Case n = 0. By PZero and EZero, we have V = stop and (δ i ) i<n = ε. Therefore, by definition of the logical relation, we have (δ i ) i<n |= A 0 V .

-Case 1 n < ω. Let (γ i ) i<n : Γ @ n, and E : Γ @ n. Now, suppose that:

By application of Lemma A.2 to (b), we obtain that there exists s such that:

By inversion of EStep in (e), we split the many step reduction and obtain that there exists s I such that:

Inversion of PRec in (c) gives us that M ; E ; x ; stop ⇑ n 0 V . Immediate application of Corollary A.4.1 gives us that there exists a value V I such that:

We turn back (f) and (h) into reductions over a rec by respectively applying to them Lemma A.6 and PRec:

Since Lemma A.11 gives us that the logical relation preserves truncation, (d) gives us that (γ i<n-1 ) |= Γ n-1 E n-1 . Thus, since (j) and (k) also hold, we can apply the induction hypothesis given by our induction over n, and we obtain:

The induction hypothesis given by our induction over (π) gives that:

M |= Γ, x:lat A A M Thus, since we have that the reductions (e) and (i) hold, and that their environments are coherent slicings by (l), we obtain that:

Which is what we wanted.

-Case n = ω. Let (γ i ) i<ω : Γ @ ω, and E : Γ @ ω. Now, suppose that:

By inversion of POmega in (n), we obtain:

Since rec x A . M is well typed, by totality (Theorem 2.3) and determinism (Theorem 2.4) of the prefix reduction, we have:

Then, by inversion of EOmega in (m) and application of Lemma A.11 in (o) we