Potop Dumitru
email: dumitru.potop@inria.fr

Butucaru

Albert Cohen

Google Deepmind

France Gordon Plotkin

Dumitru Potop Butucaru

Bidirectional Reactive Programming for Machine Learning

Reactive languages are dedicated to the programming of systems which interact continuously and concurrently with their environment. Values take the form of unbounded streams modeling the (discrete) passing of time or the sequence of concurrent interactions. While conventional reactivity models recurrences forward in time, we introduce a symmetric reactive construct enabling backward recurrences. Constraints on the latter allow to make the implementation practical. Machine Learning (ML) systems provide numerous motivations for all of this: we demonstrate that reverse-mode automatic differentiation, backpropagation, batch normalization, bidirectional recurrent neural networks, training and reinforcement learning algorithms, are all naturally captured as bidirectional reactive programs.

INTRODUCTION

Conventional machine learning (ML) frameworks offer a tensor-centric view of the design and implementation of deep neural networks. But ML models do not stand by themselves as pure tensor functions. ML applications typically interact with an environment and often operate on streams of data collected and processed over time. For instance, the reactive control of a self-driving car [START_REF] Ben Naveed | Trajectory planning for autonomous vehicles using hierarchical reinforcement learning[END_REF][START_REF]Towards AI editorial team. tesla's slef-driving algorithm explained[END_REF] operates on streams of data coming from sensors and controlling actuators. Training algorithms themselves embed a model into a reactive loop: it is decomposed into epochs and (mini-)batches allowing the efficient scheduling of computations and I/O, parameter updates, etc. The same applies to reinforcement learning (RL) agents [START_REF] Dulac-Arnold | Challenges of real-world reinforcement learning: definitions, benchmarks and analysis[END_REF]. Back to the automated driving example, stateful behavior is essential to taking into account previously-inferred facts such as speed limits, whether the current lane is a left turn etc., long after the acquisition of sensor inputs. Other examples of ML components embedded into stateful reactive feedback loops include model-predictive maintenance [START_REF] Serradilla | Deep learning models for predictive maintenance: a survey, comparison, challenges and prospect[END_REF], control [START_REF] Eduardo | Model predictive control[END_REF], and digital twins [START_REF] Michael | Toward predictive digital twins via component-based reduced-order models and interpretable machine learning[END_REF]. ML models themselves involve stateful constructs in the form of recurrent neural network (RNN) layers. When generating optimized code, even matrix products and convolutions in feedforward networks can be folded over time, using (stateful) buffering to reduce memory footprint [START_REF] Rybakov | Streaming Keyword Spotting on Mobile Devices[END_REF]. In distributed settings, the efficient implementation of large models involves pipelined communications and computations [START_REF] Cai | Synthesizing optimal collective algorithms[END_REF][START_REF] Huang | Gpipe: Efficient training of giant neural networks using pipeline parallelism[END_REF][START_REF] Liu | Dive into big model training[END_REF], which amounts to locally recovering a streaming execution pattern.

Considering this broad range of scenarios, we observe that existing ML frameworks inadequately capture reactive aspects, raising barriers between differentiable models and the associated control, optimization, and input/output code. These barriers worsen the gap between ML research and system capabilities [START_REF] Barham | Machine learning systems are stuck in a rut[END_REF], particularly in the area of control automation where embedded ML engineering relies on undisclosed, ad-hoc implementations [START_REF]Towards AI editorial team. tesla's slef-driving algorithm explained[END_REF]. Our contributions are threefold: Dataflow reactive machine learning. We first observe that conventional (dataflow or fold_left) reactive programming allows the natural specification of a variety of ML inference models, optimization and RL algorithms. By indexing data and parameter streams along the logical time steps of computation and interaction, one may integrate the internal processing of ML models with data pre-/post-processing stages, and embed everything into a reactive control loop. Bidirectional reactive programming. We extend such a core reactive language with recurrences backward in time (fold_right). While classical reactive programs compute the values of cycle + 1 from those of cycle , forming recurrences forward in time, bidirectional reactive programs allow a value of cycle to depend on one of cycle + 1. 1 This extension captures reverse-mode automatic differentiation, backpropagation through recurrent layers, training parameter update, distributed and pipelined training, bidirectional recurrent networks, and layers crossing data and time boundaries such as batch normalization; all of this without the need for an explicit gradient tape [START_REF] Radul | You only linearize once: Tangents transpose to gradients[END_REF] or caching mechanism [START_REF] Moses | Instead of rewriting foreign code for machine learning, automatically synthesize fast gradients[END_REF]. This extension preserves the bounded time and memory guarantees of reactive languages whenever recurrences backwards in time have a bounded horizon. Formal semantics. The semantics of this bidirectional reactive language is defined from purely functional stream denotations. We provide a denotational semantics reminiscent of synchronous Kahn networks [START_REF] Caspi | Synchronous kahn networks[END_REF]. To ensure productivity (i.e. the absence of deadlocks), chains of backward dependences must always eventually terminate, so that execution can be implemented as globally forwards and locally backwards with finite buffering.

We unify independently developed ML models and algorithms on top of reactive constructs with deterministic formal semantics. This allows homogeneous and unambiguous specification, spanning from individual layers to RL algorithms. It also paves the way for the combination of efficient ML processing with the scheduling and resource allocation expressiveness of reactive languages.

RELATED WORK

This paper contributes to programming languages for both machine learning and reactive control systems. We address them separately.

Machine learning. While dataflow modeling has long been the norm in deep learning frameworks, the focus has typically been on efficient data processing, one input (batch) and one version of the trained parameters at a time. The design of ML compilers has been primarily driven by this common-case scenario, where both inference and training involve computations over data sets that have been already processed and stored. This contrasts with the needs of control applications that involve reactive and stateful interactions with an environment. Such interactions are represented outside of the ML model, which makes it difficult to provide implementations that satisfy stringent real-time and memory requirements [START_REF] Heitor | Machine learning for streaming data: State of the art, challenges, and opportunities[END_REF][START_REF] Ben Naveed | Trajectory planning for autonomous vehicles using hierarchical reinforcement learning[END_REF][START_REF] Rybakov | Streaming Keyword Spotting on Mobile Devices[END_REF][START_REF]Towards AI editorial team. tesla's slef-driving algorithm explained[END_REF][START_REF] Zhou | A survey on deep learning technique for video segmentation[END_REF]. By comparison, we provide a language allowing the natural representation of reactive programs on streams, to express transformations over these such as automatic differentiation. It has been shown recently [START_REF] Pompougnac | Weaving synchronous reactions into the fabric of ssa-form compilers[END_REF] that dataflow reactive programming [START_REF] Bergerand | Outline of a real time data flow language[END_REF][START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF][START_REF] Caspi | From simulink to scade/lustre to tta: A layered approach for distributed embedded applications[END_REF][START_REF] Potop-Butucaru | Correct-by-construction asynchronous implementation of modular synchronous specifications[END_REF] captures a large class of ML applications-the light and yellow cells of Figure 1. In particular, the variety of ML constructs in these applications can be reduced to just four dataflow constructs. Bidirectional reactivity-the orange cells of Figure 1-improves expressiveness further, with support for the automatic differentiation of arbitrary networks and context-dependent operations such as batch normalization 1 "Bidirectional" borrows here from machine learning terminology. It is not about computing from updated outputs [START_REF] Pierce | Foundations for bidirectional programming[END_REF].

(whose semantics differ in inference and training modes). One no longer needs a different programming model for training in the data center vs. inference on the edge, for latency-vs. throughputoptimization, or a specific "out-of-the-language" toolkit for RL.

Reactive languages. We aim to facilitate the design and implementation of ML applications by exploiting abstractions and methods originating from reactive systems. Our main influence is the dataflow synchronous language Lustre, and its commercial version Scade, introduced in the 1980s [START_REF] Bergerand | Outline of a real time data flow language[END_REF] to allow the formal specification, the efficient execution and the automatic verification of deterministic concurrent systems with feedback and conditional control. Lustre, as well as the broader class of functional reactive languages [START_REF] Elliott | Functional reactive animation[END_REF], 2 do not allow the representation of bidirectional recurrences.

Lucid [START_REF] Ashcroft | Lucid, a nonprocedural language with iteration[END_REF], one of the inspiration for Lustre, did introduce a next construct with semantics similar to the post construct we introduce for bidirectional recurrences. The designers of Lucid explicitely disallowed recurrences into the future however, limiting the usage of next in right-hand side expressions to non-recursive definitions.

LANGUAGE SYNTAX AND OVERVIEW

Figure 2 introduces the syntax of R(ML) 2 -for Reactive Machine Learning Meta Language. It is based on that of the classical dataflow reactive language Lustre [START_REF] Bergerand | Outline of a real time data flow language[END_REF][START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF] from which it borrows its core set of dataflow primitives (in black) [START_REF] Bourke | A formally verified compiler for lustre[END_REF]. The Kleene star stands for comma-separated lists when applied to expressions and variables, for lists of equations in nodes, and for list of nodes at the top level of the program. The main node serves as the entry point to the computation; its inputs and outputs characterize the semantics of the whole program. To this classical reactive core, R(ML) 2 adds the single new primitive post. It brings a fundamental extension over classical reactive languages: recurrences backwards in time, i.e. the ability to traverse time backwards. In a ML context, this is required to represent bidirectional networks [START_REF] Schuster | Bidirectional recurrent neural networks[END_REF], the training or reinforcement learning of stateful networks by means of backpropagation through time [START_REF] Mozer | Backpropagation: theory, architectures, and applications, chapter A focused backpropagation algorithm for temporal pattern recognition[END_REF][START_REF] Werbos | Backpropagation through time: what it does and how to do it[END_REF], and batch normalization [START_REF] Ioffe | Batch normalization: Accelerating deep network training by reducing internal covariate shift[END_REF]. The expressive power of this construct will be discussed in Section 5 and its formal semantics will be defined in Section 6.

Note that R(ML) 2 features neither general recursion nor higher order functions. This choice, inherited from the synchronous reactive language Lustre, allows implementation in bounded time and memory. 3 More expressive variants of the language could be considered in the future, in the spirit of FRP [START_REF] Elliott | Functional reactive animation[END_REF] or Reactive ML [START_REF] Mandel | Reactiveml: a reactive extension to ML[END_REF], but this is left for future work.

For brevity, we did not include tensor notation and tensor algebra operations in this syntax. A few of the examples below use conventional Python notations and Numpy or Keras operations, with square brackets for functional arrays.

As noted in Figure 1 and justified in the next section, the core language (i.e. without post) allows the natural representation of inference and reinforcement learning, for feedforward networks and one-directional RNNswithout batch normalization. This includes models with complex control such as gated mixture of experts [START_REF] Shazeer | Outrageously large neural networks: The sparsely-gated mixture-of-experts layer[END_REF]. In the case of feedforward networks, it can also represent forward-and reverse-mode differentiation, backpropagation, a wide range of (non-pipelined) training algorithms, and mixing ML models with more general reactive control. We dedicate Section 4 to presenting its expressive power from an ML perspective.

Note that synchronous reactive languages like Lustre have clocks, a dependent type system making explicit the otherwise implicit wellformedness of sampled stream expressions, and the associated conditional execution [START_REF] Colaço | Clock as first class abstract types[END_REF]. The inability to infer the clock of a variable results in the program being rejected as incorrect, while properly clocked reactive programs are called synchronous [START_REF] Bergerand | Outline of a real time data flow language[END_REF]. We leave clocks out of this paper for the sake of conciseness, since for the most part, applications to ML and bidirectional extensions are orthogonal to clock types and inference.

DATAFLOW REACTIVE MACHINE LEARNING

Informal semantic principles. The underlying reactive language without post allows the definition of (forward) dataflow nodes that compute streams of outputs from streams of inputs. It has a concurrent semantics that parallels that of the classical fold_left iterator in functional languages. While classical functional languages evaluate recurrences in space, left-to-right along lists or vectors, the iterations of a reactive node unfold in time along potentially infinite input streams of data. At each cycle, the inputs of one recurrence step are acquired along with the current value of the fold_left accumulator, known as the program state in reactive programming; then computations for this cycle take place, yield the associated outputs and the new program state (the value of the accumulator), the latter are propagated to the next cycle before its evaluation may start.

The motivations for choosing a concurrent dataflow semantics are similar in both reactive control [START_REF] Bergerand | Outline of a real time data flow language[END_REF] and ML applications [START_REF] Abadi | A computational model for tensorflow. an introduction[END_REF]. It captures the intrinsic concurrency of sensors and actuators in control automation, and the intrinsic concurrency of compute graphs in ML; it natively models parallel and distributed execution, including pipelining [START_REF] Whitlock | Extending tensorflow's semantics with pipelined execution[END_REF], and it provides ample freedom to the compiler to implement graph-level optimizations such as different forms of fusion [START_REF]The XLA team. XLA[END_REF].

Furthermore, a reactive language generalizes the fold_left iterator by allowing conditional input/output. One cycle does not need to acquire a value on every input stream and produce a value on every output stream. Instead, any variable can be marked as absent in a cycle. Within each cycle, execution is data-driven: computations take place as soon as enough input variables have acquired a value. As a result, variable uses need not be dominated by their definition: the syntactic ordering of equations in a node is semantically irrelevant.

Core constructs. The reactive core of R(ML) 2 uses only four dataflow primitives to implement these semantic principles: function application, initialized delay, conditional (sub-)sampling, and conditional up-sampling a.k.a. merging. All other constructs of Lustre can be reduced to the four primitives by structural expansion, and thus can be implemented on top of core R(ML) 2 . The usual scalar operators (+, *, etc.), lifted to tensors through point-wise application, and other pure functions imported from a classical (non-reactive) language can be used in R(ML) 2 programs. The function application primitive of R(ML) 2 lifts them to streams by pointwise application at each time step. Among these pure functions we mention the (eager) conditional expression on streams if 1 then 2 else 3 , which does not need special handling as a primitive.

The remainder of this section explores these constructs and their intuitive semantics in greater detail. Much of the discussion is based on the example of Figure 3, which implements the gradient descent of a two-layer feedforward network. To simplify the presentation, we apply the layers to scalars instead of higher-dimensional tensors, and we omit the batch dimension. The backpropagation control structure is not simplified however. The model has two parameters (in layer dense); it exercises all R(ML) 2 primitives, including forward recurrences-in blue-and backward recurrences-in red-and as we shall see, it already goes beyond the ML state of the art. The two-layer feedforward network implements the function app

(i) = multiply(dense(i)) = (k × i + b) 2 ,
where k and b are parameters initialized with values 1.0 and 0.0, respectively. During training, the objective is to perform gradient descent on the parameters in order to reduce the Mean Square Error (MSE) with respect to a ground truth gt. If the ground truth provided for input i is gt(i) = (2.0 × i -3.0) 2 , the parameters will converge towards 2.0 and -3.0, respectively.

Hierarchy, dataflow equations, normalization

An R(ML) 2 program consists of a list of dataflow nodes. Each node comprises an interface and zero or more equations connected into a dataflow graph by means of variables. In an ML context, R(ML) 2 dataflow nodes represent elementary computations, layers, inference, training, or the full application. A dataflow node such as app can instantiate another. Semantically, dataflow instantiation (which we inherit from Lustre) has the same effect as inlining the code of the instantiated node. 4 Due to this inlining semantics, while code may be reused across multiple instances of the same node, the storage of stateful nodes is not shared between instances. In our example, node diff_dense contains two instances of node diff_param, each one independently storing the value of one parameter during training (using the fby primitive at Line 2).

Dataflow dependences between primitives of a node are either explicitly represented using named variables, or implicitly within expressions. For instance, in node dense, in Line 8, the operator "+" takes as input the output of operator "*". It is always possible to transform equations with complex expressions into multiple single-primitive equations by exposing implicit dataflow dependences with fresh variables. This process is traditionally referred to as normalization and is analogous to the administrative normal form in continuation-passing style. The result of this process for node app, combined with the inlining of the instantiation of dense and multiply (for easier reference in simulations), is provided in Figure 4. Note in lines 4-5 the single-primitive equations produced as part of the normalization of the dataflow expression in Line 8 of node dense.

Function application

As explained earlier, at each execution cycle, an equation performs its computation as soon as its variables have acquired a value are are known as absent.

node The function application primitive of R(ML) 2 incorporates classical (non-reactive, non-streaming) functions into our reactive language by means of pointwise application. At each cycle, the function application primitive will wait for one value on each input variable before calling the classical function and then assigning its results to the output variables. If one input or output is absent during the cycle, then all inputs and outputs must be absent and the function is not called. If we denote with 0 < 1 < 2 < . . . the indices of the cycles where the inputs and outputs of the function application "o 1 , . . . , o = f(i 1 , . . . , i )", are present and with the value of a variable at cycle , then we will have, for all ≥ 0: o 1 , . . . , o = f(i 1 , . . . , i ). We depict in Figure 5 a possible execution trace-known as a chronogram5 -of the equations in lines 5-6 of Figure 4. The trace is 5 cycles long (indices 0 to 4). In cycle 3 all variables are absent-the symbol.

app(i)->(o) b = 0.0; k = 1.0; t = k * i; x = t + b; o = x * x;
Notice how, inside each cycle, the computation is causal, with the producer of a variable value being executed before all consumers. Function applications can be composed into arbitrarily complex (hierarchic) stateless computations, which can represent the computation of layers (such as dense in Figure 3), or full feedforward models, such as app. The main constraint here is that the resulting dataflow graphs are acyclic. 6Most functions used in ML applications are pure functions such as additions, convolutions, tanh, sigmoid. However, ML practice also makes significant use of functions that are not pure. These are random functions used in initializers (e.g. glorot_uniform, orthogonal) or in dropout layers.

Stateful computations

We have seen in the previous section how function applications can be composed into arbitrarily complex stateless computations represented with acyclic dataflow graphs. However, ML practice always involves stateful behaviors implementing forward recurrences along the time direction. As we shall see, these recurrences are mandatory in the training process (to store the parameter values), but they may already appear at specification level, as in recurrent neural networks (RNNs). Beyond the ML code itself, ML-based systems design also involves significant stateful components, such as data pre-processing involving sliding windows 7 or efficiently-scheduled pipelined implementations [START_REF] Huang | Gpipe: Efficient training of giant neural networks using pipeline parallelism[END_REF][START_REF] Whitlock | Extending tensorflow's semantics with pipelined execution[END_REF]. The R(ML) 2 language construct and a few applications are discussed in this section, while more advanced uses of stateful behaviors in ML are discussed later, in Section 4.5. and Lustre statement allowing to cover all these needs is fby. Its general form is = fby ; where and are expressions of the same type and is a stream variable. Its semantics is that of a loop-carried dependence, and it requires that , and are all present at the same cycles. We will denote with 0 < 1 < 2 < . . . the indices where , and are all present. Then, 0 = 0 and = -1 if > 0. Figure 6 shows one possible execution trace for a fby equation.

Notice that, unlike function application, the output of fby does not depend within the current cycle on its second input. This allows the construction of cyclic dataflow graphs, such as the one in In the first cycle (of index 0) its output (the value of variable o) is the value of the first input, which is 0. In cycle 1, it is the value of its second input (variable u) in cycle 0, which is 1. Inductively, we can prove that in every cycle the value of o is . Note that each fby equation of a node defines one element of the recurrence accumulator which defines the program state. Thus, the counter node above has a state formed of one integer, whereas the state of node app in Figure 4 is formed of two floatingpoint values. For a node that has not yet been inlined, the state is formed of the fby equations defined directly in , plus the state of all the node instances of .

4.3.2

Modeling recurrent neural networks. We start to showcase the expressive power of fby by modeling recurrent neural networks (RNNs), taking as example the classical Long Short-Term Memory (LSTM) [START_REF] Gers | Learning to forget: Continual prediction with lstm[END_REF]. RNNs are stateful networks, where one cycle passes a state that is used in the next. We provide in Figure 8 an implementation of the LSTM later. 8The presentation of the LSTM layer is meant to facilitate its comparison with classical ML frameworks such as Keras, preserving the separation between the cell node lstm_cell representing the function iterated within the recurrence from the lstm node which implements the reduction over time. Parameter initialization follows the Keras default: glorot_uniform for the kernel, zeros for the bias, orthogonal for the recurrent state. Notice how the two LSTM-specific recurrence state elements (c and h) are encoded in node lstm using two fby equations.

Pairing the fby operators within the top-level non-recurrent node is mainly due to the limitations of existing ML frameworks. Using the node hierarchy of R(ML) 2 , we could restructure the LSTM cell to emphasize its internal organization into gates, as defined in the literature [START_REF] Gers | Learning to forget: Continual prediction with lstm[END_REF]. Collecting fby operators for efficient iteration may deferred to the compiler (see Pompougnac et al. [START_REF] Pompougnac | Weaving synchronous reactions into the fabric of ssa-form compilers[END_REF], Section 4).

Pipelined inference.

Given the complexity of mapping ML applications onto heterogeneous hardware, efficient designs may involve source-level mapping and scheduling [START_REF] Huang | Gpipe: Efficient training of giant neural networks using pipeline parallelism[END_REF][START_REF] Whitlock | Extending tensorflow's semantics with pipelined execution[END_REF]. This is cumbersome at best with existing ML frameworks. Figure 3 shows how to split node app in two pipeline stages by inserting a fby operator between the two layers. The result is shown in node app_pipe, and the corresponding backpropagation code in node diff_app_pipe. We showcase this in Figure 9 with a time series application where inputs are buffered into a sliding window (also known as a rotating buffer) of size 4 before being fed to a Multi-Level Perceptron (MLP).

The sliding window node uses a delay line where x1 is x delayed by 1 cycle, x2 is further delayed by 1 cycle, and finally x3 is x delayed by 3 cycles. The sliding window output w is obtained by grouping all four variables into a vector. 9Beyond this small example, data pre-processing and postprocessing can be arbitrarily complex, from signal processing to extract a spectral representation to using the output of the ML algorithm for model-predictive control.

Conditional execution and sampling

Piecewise functions (e.g. ReLU) and data sampling have long been part of ML practice. Yet general primitives such as the tf.where choice operator or tf.cond/xla.conditional/jax.lax.cond for conditional execution 10 are rarely used directly by programmers. However, the pressure to reduce the computational requirements of ML applications naturally results in rapidly growing popularity of conditional execution, such as the sparsely-gated mixture-of-experts layer [START_REF] Shazeer | Outrageously large neural networks: The sparsely-gated mixture-of-experts layer[END_REF].

By comparison, reactive programming exposes powerful conditional execution primitives. The danger associated with conditional execution in a concurrent system is non-determinism: when the producer and the consumer of a variable are executed on different conditions, the consumer may read an undefined value. This is why dataflow reactive formalisms propose correct-by-construction semantics ensuring that all values used in computations are well-defined. This is the approach we follow in R(ML) 2 , borrowing the when and merge conditional execution primitives of Lustre [START_REF] Bergerand | Outline of a real time data flow language[END_REF][START_REF] Biernacki | Clock-directed modular code generation for synchronous data-flow languages[END_REF]. In the dataflow setting of Lustre and R(ML) 2 , where execution is driven by the arrival of data, conditioning the execution of a node in a cycle is done by making its input variables present or absent in that cycle. This is done using the (sub-)sampling operator when. In equation "x = y when c", it is required that variable c is of Boolean type and that c is present in a cycle if and only if y is present. Then, in cycles where c is present with value true, x takes the value of y. In cycles where c is absent or present with value false, x is absent and computations that depend on it are not executed. If c is absent, then x is absent. We provide in Figure 10 a possible execution trace. In cycles 0 and 2, c is present with value true, so the value of y is copied onto x. In cycles 1 and 4, both inputs are present but c is false so x is absent. Finally, all variables are absent in cycle 3.

Primitive "x = merge c y z" defines a deterministic multiplexer. Its inputs must satisfy the following conditions:

• c is known as the control stream of the merge operator and must be of Boolean type;

• y is be present in a cycle iff c is present with value true;

• z is be present in a cycle iff c is present with value false;

• y and z have the same data type. Under these conditions, x is a variable that is present iff c is present, which takes the value of y if c is true and the value of z if c is false. Figure 11 shows a possible execution trace. In cycles 0 and 2, c is present with value true, so the value of y is copied onto x and z must be absent. In cycles 1 and 4, c is present with value false, so the value of z is copied onto x and y must be absent. In cycle 3, all variables are absent.

As a first ML application of when and merge, Figure 12 describes a sparsely-gated mixtureof-experts layer [START_REF] Shazeer | Outrageously large neural networks: The sparsely-gated mixture-of-experts layer[END_REF]. We instantiate it for 3 experts, assuming that they are provided as nodes expert1, expert2, and expert3, which produce tensors of the same shape.

node gating_network(x)->(g1,g2,g3) node expert1(x)->(o) node expert2(x)->(o) node expert3(x)->(o) node mixture_of_experts(shape,x)->(o)
g1,g2,g3 = gating_network(x); o1 = expert1(x when c1); c1 = (g1 != 0); o2 = expert2(x when c2); c2 = (g2 != 0); o3 = expert3(x when c3); c3 = (g3 != 0); o = g1 * (merge c1 o1 zeros(shape)) + g2 * (merge c2 o2 zeros(shape)) + g3 * (merge c3 o3 zeros(shape)); We assume that expert control is performed by node gating_network, which outputs at each cycle one floating point value per expert, serving as weights in the computation of the output (in lines 11-13). In a cycle where the weight corresponding to an expert is 0, the expert must not be computed. This behavior is obtained by sampling the network input x. For expert1 this is done in line 8. Boolean variable c1 stores the Boolean activation condition. To compute the weighted sum output, o1, o2, and o3 cannot be added because they are not present at the same cycle. Instead, the merge operators of lines 11-13 extend the outputs o1, o2, and o3 to variables that are present at all cycles, padding with 0 in cycles where the experts do not produce a value.

Notice that Lustre and R(ML) 2 offer a modular form of logical time, by allowing subsets of equations, including fby operators, to be executed under specific Boolean conditions. For instance, the experts or the gating network of Figure 12 can be themselves stateful/recurrent [START_REF] Chazan | Deep recurrent mixture of experts for speech enhancement[END_REF] involving fby operators. For every such expert, the recurrences relate only the cycles where the expert is active. In the context of control applications-typically multi-periodic and involving multiple execution modes-this facilitates interfacing the ML code with the reactive system-level code driving it [START_REF] Peddinti | A time delay neural network architecture for efficient modeling of long temporal contexts[END_REF][START_REF] Vlaar | Multirate training of neural networks[END_REF].

Backpropagation training of feedforward networks

We are now ready to discuss the reactive modeling of gradient backpropagation when training neural networks. In the example of Figure 3, node diff_app implements backpropagation for the feedforward network app. Note that diff_app preserves all the inputs, outputs, and equations of app, structurally adding to them the error computation and backward path variables and equations and the control governing them. The new Boolean input bp, known as the backpropagation signal, is present at all cycles. Backpropagation is performed in cycles where bp is true. In these cycles, the node also receives a ground truth value gt. Based on the value of gt, the error is computed (on the current sample only), it is multiplied by the learning rate, and then backpropagated. Parameters are eventually updated, with the objective of reducing the error in future cycles.

Note that an execution of node diff_app can mix cycles of training with cycles of pure inference, by choosing the sequence of values of bp. This feature is needed in Reinforcement Learning [START_REF] Dulac-Arnold | Challenges of real-world reinforcement learning: definitions, benchmarks and analysis[END_REF], and our modeling approach supports it out-of-the-box. Pure inference and pure training implementations of our specification (like those produced by TensorFlow) can then be obtained by setting bp to constant false or to constant true, respectively, as we do in nodes infer and train.

The synthesis of the backpropagation and parameter update code from the specification is not detailed in this paper. 11 We only provide the result of this synthesis process to show that R(ML) 2 allows its representation. Backpropagation consists in computing, for each value computed on the forward path, an error estimation d . In our backpropagation approach based on static program transformations, for each specification-level differentiable variable we create in the backpropagating implementation another variable d . The computation of the d variables reverses all the causalities of the forward path. For instance, in node dense of Figure 3 variable o is computed from k, i, and b. Then, in node diff_dense, variables dk, di, and db all depend on do. Furthermore, backward path computations may depend on forward path values (when the forward path function is not affine). For instance, dk depends on i. The forward path depends on the backward path through the update of parameters only. This explains the form of the diff_param node, which accumulates the corrections do at every cycle where bp is present. The updated parameter value is fed to the next cycle regardless of the value of bp.

From a language design perspective, param is an ML-specific primitive (the only one used for the scope of this paper), which is expanded during synthesis of training code (not detailed in this paper) into diff_param. Further coverage of ML parameters, from a recurrent reactive specification perspective, follows in Section 5.3.

RECURRENCES BACKWARD IN TIME

The reactive core of R(ML) 2 , along with the time/space and state manipulation extensions of the previous section, already covers the expressiveness requirements of ML applications in the yellow cells of Figure 1. The particularity of these ML applications is that they only define data dependences (recurrences) forward in time-a value of a cycle cannot depend on values of future cycles.

But to cover the needs of modern Machine Learning, we also need to cover the applications in the orange cells of Figure 1. These applications feature dependences backwards in time coming from 3 main sources: bidirectional networks [START_REF] Schuster | Bidirectional recurrent neural networks[END_REF], batch normalization [START_REF] Ioffe | Batch normalization: Accelerating deep network training by reducing internal covariate shift[END_REF], and backpropagation through time used in the training and reinforcement learning of recurrent networks [START_REF] Mozer | Backpropagation: theory, architectures, and applications, chapter A focused backpropagation algorithm for temporal pattern recognition[END_REF][START_REF] Werbos | Backpropagation through time: what it does and how to do it[END_REF].

To this end, we extend reactive dataflow programming with a new primitive, with the form "y = post x;". This equation specifies that x and y are present at the same cycles and that, if we denote with 0 < 1 < 2 < . . . the indices of the cycles where x and y are both present, then for all we have = +1 . Figure 13 shows one possible execution trace for this equation. We start our exploration of the new primitive by noticing that "post (y fby x)" is always equal to x, whereas "y fby (post x)" is equal to x for all cycles save the first, where it is equal to y (since post discards the first value of x which cannot be recovered).

Backpropagation on pipelined applications

The simplest use of post is in extending the backpropagation method of Section 4.5 to pipelined applications. Recall from Section 4.3.3 that fby primitives can be introduced in feedforward specifications to mark the frontier between pipeline stages of the inference algorithm.

These fby primitives do not create cycles in the dataflow of the node, and backpropagation code can be synthesized for such specifications without considering the full complexity of time recurrences, which is covered in the next section. More precisely, backpropagation in pipelined feedforward applications simply requires the realignment of backward propagation with the forward one by means of post primitives inserted on the backwards path in places where on the forward path a fby primitive exists. We illustrate this on Figure 3: app_pipe is a pipelined version of app, and diff_app_pipe shows the effect of injecting backpropagation code. In the process, the unique fby primitive is replaced with an instance of the diff_fby1 node which not only includes the forward-path fby that separates the pipeline stages, but also includes the backward-path post primitives that realign backpropagated values with the forward path computations. 12In this chronogram, the value 1 is produced by the first pipeline stage (node dense in our example) in cycle 1, but is delayed to be processed by the second pipeline stage in cycle 2. In cycle 2, the backpropagation indicator is true in the second stage (bpo = true) and value 2 must be backpropagated to the cycle 1 of the first pipeline stage. This is realized by the two post primitives in node diff_fby1. The first one simply anticipates the values of bpo to produce bpi. The second is part of a more complex protocol that produces an output di at a different rate from the input do.

Globally-forward, locally-backward propagation

Note that, while the fby and post primitives of R(ML) 2 both embody recurrences over time, they are not symmetrical, as classical functional programming iterators fold_left and fold_right are.

As any execution has a start (in cycle 0) forward recurrences always have a well-defined initialization cycle. By comparison, reactive programming does not identify an end cycle and executions are a priori infinite. For this reason, no initial value is specified by the post primitive.

Like for fby, the output of a post does not depend on its input inside a cycle. This allows the creation of cyclic dataflow graphs, like the counter node of Figure 7, which represent recurrences in time. Replacing in the counter node the fby by a post produces the node of Figure 15(left). We have pictured in Figure 15(right) the data dependences specified by its equations. 13 Clearly, the program can compute no output, as all values depend on the infinite future.

Whenever a program includes a post primitive in a dataflow cycle, we must ensure that, at every execution cycle in the program execution, the dependence on the future is eventually broken. In formal terms, the predicate identifying the cycles where the dependence on the future is broken must satisfy the temporal logic [START_REF] Pnueli | The temporal logic of programs[END_REF] formula always eventually .

1 node pcounter()->(o) 2 o = post u; 3 u = o + 1; cycle 0 1 2 3 4 5 u 0 1 2 3 4 5 o 0 1 2 3 4 5
Fig. 15. Dependences on the infinite future; backward dependences in red, instantaneous ones in brown. This requirement only applies to post, not to fby. Thus, the execution of the program can proceed globally forwards, locally backwards.

In Figure 16(left), the condition breaking the dependence on the future is provided by the bp input. When bp is true, the value of the input is sampled at the current cycle and broadcasted to all previous cycles, until reaching an earlier cycle where bp was true. One execution trace of backfill is pictured in Figure 16(right). Notice how the cycles where bp is true cut the execution into intervals, with the output remaining constant over each interval.

Batch normalization.

We are now ready to study the batch normalization layer [START_REF] Ioffe | Batch normalization: Accelerating deep network training by reducing internal covariate shift[END_REF], which is one of the most complex from a reactive control perspective. In training mode, the forward path is provided in Figure 17 by node batch_norm.

We operate on batches of samples of the input x. Batch termination is identified by the Boolean input batch_end. Node mean_var computes the mean and variance, propagating data both forward and backward in time. The number of samples in a batch and the partial sum of its elements are accumulated in the forward direction in variables cnt and sum, respectively. Node fby_end applies forward in time recurrences piecewise: whenever end is true, the input is dropped and in the next cycle the output is set to init. In other cycles, the output is set to the delayed input. An execution trace of fby_end is provided in Figure 18.

In node mean_var, instances of fby_end are used to reset the accumulation of partial sums at batch ends, so that for each batch starts with an accumulator set to 0. At batch ends, the value of expression "sum/cnt"-the batch mean-is sampled and broadcast to all batch cycles by the first instance of backfill as described above. Using the batch mean, one may again accumulate in forward direction, in variable var_sum, the partial sums needed to compute the variance. At batch end, the variance is broadcast to the whole batch by the second instance of backfill. Fig. 18. Trace of node fby_end of Figure 17.

The computed batch mean and variance are then used to normalize the input, also using two trainable parameters gamma and beta. The use of fby_end in the context of trainable parameters will be covered in detail in the next section.

Backpropagation through time for RNN training

Consider the lstm node of Figure 8, which represents the recurrent layer LSTM. In its first execution cycle, the state accumulator variables h and c are initialized with the value of the two parameters. Then, at every cycle (including the first), the non-recurrent lstm_cell node is executed once, taking as input the current accumulator and the current value of the lstm input x, and producing the updated accumulators (of which one is also output). If we denote with ℎ the value of h at cycle , the computation of ℎ +1 causally depends on that of ℎ for all .

Recall that in a backpropagation training context, for every value computed on the forward path, an error estimation dv is computed on the backward path, and the computation of the latter reverses all the causalities of the forward path. Thus, if the difference associated with ℎ is denoted dh , we know that dh depends on dh +1 for all , and so the computation of dh 0 (to update parameters) depends on the infinite future.

As explained in Section 5.2, such a dependence on the infinite future cannot be effectively resolved: backpropagation must be reduced to a globally forward, locally-backward propagation, where the predicate determining when to restart backpropagation is always eventually true. Such a predicate is readily available when training with mini-batches. Indeed, RNN training samples consist of finite input sequences accompanied by ground truth values. In a training or RL, sequences are provided cylically, possibly separated by samples meant for inference only . The result can be seen as a single stream of inputs, where the end of training sequences is marked by the Boolean input signal end. One may finally weave backpropagation with reset into the LSTM of Figure 8. The result of this source-tosource transformation is provided in Figure 19, where fby and post operators are replaced with the resettable versions fby_end in Figures 17 and18 and post_end in Figure 21, respectively. Parameters also need to be wrapped into separate param_end nodes, which are particular instanciations of fby_end with the output fed back into their delayed input.

The param_end wrappers are required during synthesis of backpropagation code. Indeed, it is expected that RNN parameters are only updated once per training sequence. During backpropagation over a sequence, parameter updates arriving at each cycle must be accumulated before applying the sum when backpropagation reaches the first cycle of the sequence. This is the exact behavior of the backpropagation code for node param_end in Figure 20. Notice in line 12 the accumulation of differences. The behavior of diff_fby_end ensures that the accumulated update is only applied to parameters on sequence start cycles. The actual parameter update is performed by diff_param (see Figure 3). With these definitions, the backpropagation code of the LSTM may be obtained by structural translation, as pictured in Figure 20.

Bidirectional RNNs

We have seen that the 5 reactive primitives of R(ML) 2 -the 4 classical ones and post-allow to model batch normalization and backpropagation with reset, as well as the alternation of training and inference within RL algorithms. We complete our presentation of the expressive power of R(ML) 2 with the encoding of a bidirectional recurrent network [START_REF] Schuster | Bidirectional recurrent neural networks[END_REF].

Bidirectional networks feature recurrences in time in both directions. Thus, post operators are needed in the model itself. For such a specification to be productive, it must include the conditions allowing a globally forward, locally backward execution, as discussed in previous sections. node post_end(shape,end,init,i)->(o) i1 = if (true fby end) then zeros(shape) else i; o = if end then init else (post i1); node lstm_bi(units,shape,x,end)->(o) h_next = lstm_end(units,shape,x,end); h_pred,c_pred = lstm_cell_end(units,shape,h,c,x,end); h = post_end(shape,end,param(orthogonal()),h_pred); c = post_end(shape,end,param(orthogonal()),c_pred); o = h_next + h_pred; We assume that the Boolean input variable end of the node identifies the cycles where backward recurrences begin.

The bidirectional LSTM layer is described in Figure 21. It builds upon the extension of the LSTM with backpropagation reset capability (nodes lstm_end and lstm_cell_endof Figure 19). Between every two cycles where end is true, the layer implements two independent recurrences in time, one forward (implemented by the lstm_end node instance) and one backward. The outputs of the two recurrences are summed at each cycle to produce the output of the layer.

SEMANTICS

As illustrated in the earlier examples, R(ML) 2 significantly extends the expressiveness of reactive (synchronous) languages such as Lustre. In particular, the execution of a program involving post (recurrences backwards in time) may not compute all the stream variables at a cycle before moving on to the next cycle + 1.

Comparison with Kahn networks. As a first attempt at formalizing the semantics of R(ML) 2 , it is tempting to build upon the dataflow framework of Kahn [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF]: concurrent programs whose asynchronous semantics can be defined by means of compositions of monotonous stream functions. Unfortunately this is not so simple. Consider, for instance, in Figure 16 the node backfill and its execution trace. Here, the values of o are not computed as a stream, where new values are always added at the end: the value of o at cycle 2 is known before those of cycles 1 and then 0.

Notations and conventions.

If is a set of values, * denotes the set of finite streams of elements of , is the set of infinite streams, and ∞ = * + . To ease the presentation, we will consider a single set encompassing all values occurring in R(ML) 2 examples.

The empty stream is noted and • is the stream concatenation operator; lifted to infinite streams inductively and allowing the contatenation of a finite stream (left-hand side operand) with a finite or infinite stream (right-hand side operand). The length of a stream is noted | |-it is a natural number or ∞. The -th value of stream is noted , the sub-stream starting from index and ending immediately before index (i.e., excluded) is noted : = { ∈N| ≤ < } , and the suffix starting from index is noted : = { ∈N| ≥ } . For example, 0 • 1: denotes the stream whose head is 0 and tail is 1: . Considering a program in the syntax of Figure 2, we assume has been normalized to an administrative form where every equation of consists of a single primitive.

denotes an environment of stream variables. In such an environment, := denotes the binding of variable to the value , and ( ) denotes the value of variable in the environment . is a function from environments to environments: ( ) denotes the interpretation of expression applied to the environment . Let ( ) be the set of free variables of an expression and ( = ) = ( ) \ { }. Let ( = ) = { } denote the (left-hand side) variables bound by a an equation eq. These notations are lifted to tuples of equations, defining ( 1 , . . . , = 1 , . . . , ) = ( 1 , . . . , ) \ { 1 , . . . , } and ( 1 , . . . , = 1 , . . . , ) = { 1 , . . . , }. For the sake of conciseness, when clear from the context, we overload to denote a tuple of variables, a tuple of expressions, and = a tuple of equations.

Variables and semantic interpretations are defined within a directed-complete partial order (dCPO or simply CPO). We will later (somewhat loosely) refer to any CPO as a domain in the following. Given two CPOs and ′ , their product × ′ and the set of Scott-continuous functions → ′ are also CPOs by considering the pointwise order. If is a continuous function from to where ⊥ is the infimum (a.k.a. greatest lower bound) of , we shall write ( ) = lim →∞ (⊥) for the smallest fix point of by the Kleene fixed point theorem.

Denotational synchronous semantics

We are interested in soundness guarantees about the termination of a single reaction, about the overall productivity (deadlock freedom), and on bounded memory execution. These motivations call for a semantics suitable to offer such guarantees "by construction" or "by design" as opposed to relying on best-effort static or dynamic analyses after the fact. This is the purpose of our denotational synchronous semantics. Note that these guarantees are typically associated with the ability to compile the program to a statically scheduled form with in-place updates [START_REF] Bergerand | Outline of a real time data flow language[END_REF], but such concerns are outside the scope of this paper. Domain of sparsely indexed streams. One may relax the prefix ordering of the Kahn domain [START_REF] Caspi | Synchronous kahn networks[END_REF] with explicitly indexed streams, making all streams effectively infinite and randomly indexable. Given a natural number, one may reason about the value of an infinite stream at this specific index. This value may be an element of , or it may be the special unknown value ⊥ capturing the fact that the actual value in (if any) is yet to be determined in the process of a fixed point computation. Note that finite streams can be extended into infinite ones by concatenating ⊥ ; one may thus model finite computations while considering infinite streams only. We also introduce an explicit absent signal and an error value , and define ⊥ = ∪ {⊥, , }. effectively sparsifies streams and computations, modeling the absence of a value in at a given index, while is associated with incorrectly synchronized programs. 14 One may define a simple ordering relation ⊑ over ⊥ by lifting the flat CPO on individal values ∀ ∈ ⊥ , ⊥ ≤ ∧ ≤ (a.k.a. the Scott domain) to infinite streams. This lets us define the sparsely indexed stream domain = ( ⊥ , ⊑, ⊥ ), a CPO whose join operator is denoted by ⊔, with infimum ⊥ and supremum .

Synchronous semantics on sparsely indexed streams. Figure 22 provides the denotations for the synchronous semantics. is a constant and is a stream variable; , , and are streams in ; and are R(ML) 2 expressions; is a natural integer. The mark # distinguishes the syntactic construct from its interpretation as a stream transformer. Scalar operations are lifted to streams of values of the same type; this includes the usual unary and binary operations -, +, or, etc. The interpretation of a node overloads the environment to hold the biding a node name its implementation; conversely, the node instantiation ( ) looks up the environment to apply the corresponding function to the interpretation of . The projection (eq) retains the tuple of streams associated with the set of variables from the tuple of equations eq. The fixed point operator is applied to every system of equations in a node: considering a tuple of equations = , it is applied to the function = . ( , := ) mapping the tuple of expressions to its tuple of bindings. The environment provides a value for all free variables in except for recursive definitions depending on ; the latter are provided with the tuple of arguments of the -term. Fixed point iterations start with values in already defined while takes the successive iterates (⊥); we establish the existence and unicity of a least fixed point ( ) by proving the Scott continuity of . 15The synchronous stream transformers are provided in Figure 23; and denote individual values in . This semantics insists on providing a cycle-by-cycle interpretation amenable to boundedmemory execution. The subscripted semantics notations and : denote the scalar value of expression at cycle and the suffix stream value of expression at all cycles and above, respectively. The absence of a value is made explicit with . We lift built-in functions, unary and binary operations to ⊥ , yielding ⊥ when one of more operands are ⊥, and yielding when one or more operands are or . We decompose the fby operator to isolate an "initial state" fby # from the "steady state" pre # triggered by the recurrent equations in Figure 23.

• The right-hand side of equations in Figure 23 has been aligned on the • operator, concatenating the value at index with the rest of the stream. The value at index is referred to as instantaneous. It is available for all computations at index and is obtained by restricting both left-and right-and-sides of the equations to this specific index. This instantaneous interpretation is a direct benefit of synchrony: it will form the basis for current cycle effects when deriving an operational semantics. In the conventional forward-reactive case, it also makes efficient in-place evaluation possible with bounded memory limited to the values live within a given cycle-all stream values at index as well as the "state" -1 associated with fby operators. In the bidirectional case, multi-cycle dependences arise from the evaluation of +1 , challenging any in-place evaluation strategy; this is the topic of Section 9. • Equations in Figure 23 provide the full definitions for infinite streams, concatenating the former with recurrences on a stream suffix such as +1: . The value of the stream at index only depends on the left hand side of • in the right-hand-side of the equations, while the stream suffix : depends on the whole right-hand-side beyond the • operator.

All cases not matched in Figure 23 yield error values. Formally, this is enforced by defining any remaining non-matched case at a given index to the value at index ; e.g.

fby #

: ( , , ,

) def = • fby1 # +1: ( , ) merge # : (true • +1: , • +1: , • +1: ) def = • merge # +1:
( +1: , +1: , +1: ) As a corollary, never occurs together with present values in pointwise/scalar computations. In particular, the merge operator enforces one of its branches to be present while the other is absent (or both are unknown).

We may now define a notion of synchrony: a program is synchronous if the value never occurs in the least fixed point solution of the semantic equations in Figure 22; formally, let ⊥ = ∪ {⊥, } = ⊥ \{ } represent non-erroneous, i.e. well-synchronized values, and consider a program from -tuples to ′ -tuples of streams, i.e. :

→ ′ , is synchronous ⇐⇒ ∀ ∈ ( ⊥ ) , ( ) ∈ ( ⊥ )
′ This is actually a problem when operating on constants that (by definition) are always present, preventing then for occuring as arguments of the merging operator. The happens with recursive definitions involving post, which are also always present. To avoid these issues, we enforce that every constant and post expression is sampled with an "appropriate" when expression before being operated upon; here "appropriate" calls for inferring the proper condition to enforce synchrony, which is the purpose of Lustre's clock calculus.

Finally, we define a bounded horizon version of the synchronous semantics of a program denoted as ìℎ , where the recursive evaluation of post # stops at a given index ℎ: the rules are identical except that of Figure 23 are used at index = ℎ. We will use this bounded horizon semantics to establish forward-progress and bounded memory execution guarantees. • . . . Figure 24 illustrates the synchronous semantics on the backfill example. The fixed point computation is best decomposed over two dimensions: for a given stream index , rows correspond to successive iterations of the fixed point computation defining values at index , while the index may be stepped to + 1 as soon as a fixed point is reached at index .

• n+1 • . . . fby # : ( , ) def = • fby # +1: ( , ) if = = fby # : ( , ) def = • pre # +1: ( ) if , ∈ ∪ {⊥} pre # : ( ) def = • pre # +1: ( ) if -1 = pre # : ( ) def = -1 • pre # +1: ( ) if -1 ∈ ∪ {⊥} post # : ( ) def = • post # +1: ( ) if +1 = post # : ( ) def = +1 • post # +1: ( ) if +1 ∈ ∪ {⊥}

Properties

In the following we refer to streams with no unknown (⊥) values as fully defined. One essential property of practically useful reactive programs is productivity, a notion associated with (1) the ability to compute the least fixed point of a system of equation as the result of a finite computation, and (2) the resulting streams being fully defined. In the traditional Lustre setting, productivity (i.e. deadlock-freedom) stems from a conservative and modular interpretation of causality: no instantaneous cycle may exist when stepping through the computation of fixed points, i.e. when any recurrence on a given stream variable at index can be traced back to the previous index -1 through the use of the fby operator. The presence of a fby operator on all cycles in the dataflow graph defined by every node of the program is a sufficient condition for the absence of instantaneous cycles. Weaker conditions and static analyses exist but none of these involve dependences on future indices, deemed non-reactive: the interested reader may refer to [START_REF] Pouzet | Modular static scheduling of synchronous data-flow networks -an efficient symbolic representation[END_REF] for a survey and for extensions improving modularity and efficient compilation. This pushes us to research an extended notion of productivity compatible with bidirectional reactions. Intuitively, lookahead dependences may be allowed as long as they are eventually broken, i.e. they do not form an infinite recurrence into the future. The problem is that allowing dependences into the future, even bounded ones, automatically gives rise to instantaneous cycles by composition with conventional dependences on the past. Reasoning on dependences only is unlikely to lead to solution. This intuition leads us to define the extended notion of bidirectional causality.

Definition 1 (Bidirectional causality). A program is bidirectionally causal if and only if the following condition hold on the synchronous interpretation

:

→ ′ : ∀ ∈ N, ∃ ∈ N, = ì + 0:
We are also interested in a stronger notion of bidirectional bounded reactivity, analogous to the bounded memory, instantaneous termination property of synchronous reactive languages [START_REF] Bergerand | Outline of a real time data flow language[END_REF]. To this end, we combine bidirectional causality with a notion of termination suitable to stream functions. Let : → be a Scott-continuous function; terminates up to index ∈ N if and only if ∃ ∈ N, ( ) 0: = (⊥ ) 0: ; and terminates if and only if it terminates up to index for all ∈ N. A synchronous program terminates (resp. terminates up to index ) if and only if all fixed point computations terminate (resp. terminate up to index ). The proof stems from the observation that incremental left-to-right computation is possible for fby operators, holding the value at the previous index only.

In the following, causal is synonymous with bidirectionally causal, and bounded reactive is synonymous with bidirectionally bounded reactive, unless stated otherwise. It is immediate that a bounded reactive program is causal.

T 4 (E

). For a causal program , the synchronous interpretation up to a certain index coincides with the synchronous semantics with a finite look-ahead horizon applied to a bounded future of the program's inputs. For a bounded reactive program, a global bound exists for both look-ahead horizon and inputs.

Formally, given program with

: → ′ , if is causal then ∀ ∈ , ∀ ∈ N, ∃ ∈ N, ( ) 0: = ( 0: + • ⊥ ) ì + 0:
and if is bounded reactive then

∀ ∈ , ∃¯ ∈ N, ∀ ∈ N, ( ) 0: = ( 0: +¯ • ⊥ ) ì +¯ 0:
The proof is inductive on the structure of semantic equations.

FROM DENOTATIONAL SEMANTICS TO OPERATIONAL SIMULATION

The semantics of the previous section has the advantage introducing backwards recurrences in a conventional Lustre-like setting with minimal changes to the semantic domain. To this end, it makes the simplifying assumption that programs are normalized, i.e. that constants are present at every cycle, that the fby operator of forward recurrences is activated according to its first input, that the post operator of backward recurrences is present at every cycle, and that the execution environment provides the status of every input variable at every cycle. From these primary sources of control information, the status of every other variable can be incrementally constructed at every cycle by traversing every program equation to compute the status of the equation outputs based on that of the equation inputs. In this process, every equation is traversed exactly once per cycle. Formalizations of classical reactive languages rely on similar normalization. In most cases, it is assumed that the activation of every variable and equation is described using a predicate, called a clock, which can be provided by the programmer or computed by means of static analysisthe clock calculus. The main downside of this classical approach is that the clocks need to be available and the normalization to take place even before one is able to define the program semantics. Indeed, the natural programming style implemented in classical compilers of dataflow reactive languages, 16 does not require the definition of clocks nor does it expose the user with the need to normalize programs. An additional drawback is that such normalization may actually be wasteful of memory resources, by forcing the allocation of memory for all inputs of a node at every cycle irrespectively of their downstream sampling through normalization.

In this section, we solve this conundrum by providing a semantics for programs that are not heavily normalized. In doing this, we actually solve an old problem of reactive programming: introducing a semantic reference to establish the correctness of the static analysis algorithms producing clock annotations.

The semantics defined in this section has three more advantages:

• It provides support for the efficient simulation of bidirectionally causal programs (see Definition 1). This is actually the main reason to present this new normalization-free semantics in the context of bidirectional reactivity: bidirectionality within a given cycle is exactly what is needed to eliminate the need for normalization in the first place; while more general bidirectional reactivity amounts to extending the semantics and simulation to multi-cycle windows. • Specifically, one may simulate finite executions of bidirectionally bounded reactive programs (see Definition 2) in a finite number of steps and with a finite memory footprint. • From an system and input/output standpoint, the semantics directly captures the behavior of programs that drive their inputs, possibly driven by their outputs, an important demanddriven pattern in both embedded and datacenter applications.

We formally prove that the simulator provided in Section 7.7 implements the semantics of this section. We also conjecture that our semantics is a strict generalization of that of Section 6 and of that of classical reactive languages such as Lustre. Proving these results is work in progress.

Domain definition

Single-variable domain. Given a variable , we denote with the set of values of its data type. We also overload to stand the data type itself. The semantics may also assign to a variable, during a cycle, another 4 values with specific meaning:

• ⊥ represents the absence of any information on the status of the variable (at the current point in execution). • represents the absent status of a variable during a cycle. It is needed to ensure by semantic means, without requiring preliminary static analysis, that a variable value produced in one execution cycle is always consumed within the same cycle. • ? is the synchronization status of a variable for which we determined that it is present, but

have not yet computed the value. It allows the on-demand triggering of the computation of constants and of recurrence outputs. It also allows triggering input acquisition actions, as opposed to always assuming that the status is provided by the environment. This value is a new addition compared to the sparsely indexed stream domain of the previous section. • signifies that the variable is involved in a synchronization error in the current cycle -its present/absent status is inconsistent with that of other variables. It is required to ensure confluence when control can propagate backwards. 17The domain of is therefore = ∪ {⊥, , ?, }, endowed with the partial order ≤ defined by: ⊥ and respectively are the infimum and supremum of , and ? is lower than the values ∈ . We denote the (always defined) supremum operator of with ∨.

iteration function of . We require that {{ }} is continuous and that {{ }} ≥ ∞ . Then, for all :

( ) = ({{ }}, ) = lim →∞ {{ }} ( ) 7.
2.2 Semantics of stateless equations/programs. If involves no recurrences (no fby or post equation), then its semantics can be described using a stateless iteration function {{ }} # : → that must be continuous and have the property {{ }} # ≥

. The iteration function {{ }} is then defined by {{ }}( ) = {{ }} # ( ) for all 0 ≤ < ( ). This function is greater than ∞ and is continuous, allowing the definition of .

Composing semantic functions

The semantics of R(ML) 2 primitives will be provided directly in Section 7.6. The semantics of program fragments including multiple statements/equations, and that of nodes, is provided in this section. It is obtained by composition from that of the primitives.

7.3.1 Notations. Given two sets of variables ⊆ and ∈ , we denote with | the restriction of to , which is an element of . In the other sense, given ∈ , we denote with ↾ its extension to , which equals over and ⊥ elsewhere. The restriction and extension operators are both extended pointwise to (respectively) elements of ∞ and ∞ . Thus, given ∈

∞ , | is an element of ∞ . Similarly, if ∈ ∞ then ↾ belongs to ∞ .
The extension operator is generalized to allow the embedding of

( ∞ ) ∞ into ( ∞ ) ∞ . If : ∞ → ∞ , then ↾ : ∞ → ∞ is defined by ↾ ( ) = ( | ) ↾ .

Semantics of composition.

We can now define the semantics of composition. The semantics of each equation or set of equations is defined over the variables it involves. For instance, the semantics of "x = merge c y z" is defined over domain { , , , } . When building the semantics of a code fragment (or node) containing an equation, we first use the extension operator to lift the semantics of the individual equation onto the variable set of the code fragment or node, which allows us to define composition by means of upper bound:

1 ; . . . ;

( ) = ({{ 1 ; . . . ; }}, ) {{ 1 ; . . . ; }} = =1 ({{ }} ↾ ) where is the set of variables taken as input or produced as output by equations 1 , . . . , . Note that by applying the Knaster-Tarski theorem we also obtain 1 ; . . . ;

( ) = ( =1 ( ↾ ), ).

Semantics of nodes.

Consider an R(ML) 2 node . We assume that its equations are 1 , . . . , , and that , , and are respectively the (mutually disjoint) sets of input variables, output variables, and local variables that are neither inputs nor outputs. Then, 1 ; . . . ;

: ∞ ∪ ∪ → ∞ ∪ ∪
and we define the semantics of node with functions

, {{ }} : ∞ ∪ → ∞ ∪ : ( ) = ({{ }}, ) {{ }}( ) = {{ 1 ; . . . ; }}( ↾ ∪ ∪ ) | ∪ 7.4
The "fby back" primitive The semantics of this section will cover not only infinite executions/traces of R(ML) 2 programs, 19but also finite ones. In this case, backwards recurrences fully mirror, in time, the behavior of forward recurrences, including their initialization, which for backwards recurrences will happen in the last execution cycle of the recurrence.

As the post primitive does not allow providing an initialization value (instead producing an output that is absent in the last execution cycle), and for symmetry w.r.t. the forward recurrences, we replace post with a new primitive whose general form is " = fby back ;" where and are expressions of the same type and is a stream variable. This primitive requires that , , and are present in the same cycles. We will denote with 0 < 1 < 2 < . . . the indices where , and are all present, and let ∈ N ∪ {∞} be the number of such cycles. Then, the recurrence relation defined by the primitive is:

= if = -1 -initialization +1 otherwise -recurrence backwards in time
Notice that the initialization case of the definition does not apply for infinite executions/traces. The post operator can always be expressed based on fby back:

x = post y; becomes x = (y fby back y) when (false fby back true);

The converse is not true, as it would require a means to identify the last execution cycle of the equation, which post and the other primitives do not provide.

Normalization

In the general form of the recurrence primitives fby and "fby back", the initialization can be performed using any expression. However, this general form can always be reduced to the case where the initializer is a constant: where the constant is any value of the type of x. This transformation improves the orthogonality of our set of primitives, by letting conditional control inside the cycle be always handled by stateless conditional execution primitives, whereas the recurrence primitives only focus on the recurrence itself, being the recurrence initializer, which corresponds to the initial value of the accumulator in a fold_left or fold_right iterator, which is not computed during iteration.

y = i
The definition of the semantics of the primitives will assume that this transformation has been performed, and that furthermore complex expressions have been decomposed, so that:

• Every equation contains a single dataflow operator.

• No variable appears twice in an equation.

• Constants are only used as:

-Right-hand side of constant equations with a single variable as output.

-State initializers in fby and "fby back" equations. Notice that computation values are only propagated from inputs to the outputs (in the first case of the definition, through the application of ), whereas synchronization information will traverse the equation in both senses (the second case of the definition, and the application of ). Whenever a synchronization error is identified on one of the variables, it is propagated to all variables, either explicitly through the application of , or implicitly through the computation of .

The semantics of constant equations (with a constant right-hand side) can be provided as a sub-case of function application. However, for clarity, we prefer defining it separately.

Definition 6 (Constant semantics). Consider equation

="y = k", where ∈ . Its stateless iterator function is {{ }} # : → defined by:

{{ }} # ( ) = ∨ if ≥ ? otherwise
Notice that the value of the constant is produced when the status of the output variable is "?". The same demand-driven protocol also allows inputs to be read on-demand.

Definition 7 (Semantics of when). Consider the equation =" = when ". Its stateless iterator function is {{ }} # : { , , } → { , , } defined as:

{{ }} # = • ℎ • ℎ • ℎ
where:

ℎ ( ) =                ∨ if [ ] = [ և ?] if [ ] = ? [ , և [ ] ∨ ?, ?] if [ ] = true [ , և , ?] if [ ] = false otherwise ℎ ( ) =        ∨ if [ ] = [ և ?] if [ ] ∈ ∪ {?} otherwise ℎ ( ) = ∨ ? if [ ] ∈ ∪ {?} otherwise
Notice how the definition of {{ }} # has been decomposed into multiple semantic functions, each one representing the semantic consequences of setting a particular input or output variable to a particular value. For instance, in the definition of function ℎ , having = true in the input state results in and being set to present, and if already has a value of , it propagates towards . This propagation action can result in taking the value or, if already has a value of or , its value becomes .

To obtain the semantics of the primitive, the per-variable functions are composed, and is applied so that an error detected in one variable is propagated to all other variables. Definition 8 (Semantics of merge). Consider the equation =" = merge ". Its stateless iteration function is {{ }} # : { , , , } → { , , , } defined as:

{{ }} # = • • , •
where:

( ) =                ∨ if [ ] = [ և ?] if [ ] = ? [ , , և [ ] ∨ ?, ?, ] if [ ] = true [ , , և [ ] ∨ ?, , ?] if [ ] = false otherwise , ( ) = [ և ?] if { [ ], [ ]} ∩ ( ∪ {?}) ≠ ∅ otherwise ( ) =        ∨ if [ ] = [ և ?] if [ ] ∈ ∪ {?} otherwise
Notice that the semantics of merge requires that the Boolean condition value is received before the data input can be propagated towards the output.

( , ) =            [ ] if [ ] ∉ ∪ {?} ∨ [ ] if [ ] ∈ ∪ {?} and ∀ < : [ ] = [ ] ∨ [ ] if [ ], [ ] ∈ ∪ {?} and ∀ < < : [ ] = ⊥ otherwise
Definition 10 (Semantics of " fby back"). Consider the equation =" = k fby back ", where ∈ = . Its iteration function is {{ }} : ∞ { , } → ∞ { , } defined by {{ }} = • , where: )] -backward recurrence with:

( ) = [ և ( ,
( , ) =            [ ] if [ ] ∉ ∪ {?} ∨ [ ] if [ ] ∈ ∪ {?} and ∀ < <= ( ) -1 : [ ] = [ ] ∨ [ ] if [ ], [ ] ∈ ∪ {?} and ∀ < < : [ ] = ⊥ otherwise
Note that, if the equation =" = fby back " is activated (inputs or outputs present) only in a finite number of cycles of an infinite trace, then in the last activation cycle its output remains at value ⊥. Indeed, determining that the equation is inactive in all subsequent cycles cannot be done algorithmically over an infinite number of cycles. Such ⊥ values can be filtered out using when equations.

The last primitive we need to consider is node instantiation.

Definition 11 (Node instantiation semantics). Consider equation ="(y 1 , . . . , y ) = n(x 1 , . . . , x )", where n is a node (not a function). Then {{ }} = {{ }} (as defined in Section 7.3.3).

Note that this definition makes the semantics of instantiation equations depend on that of the instantiated nodes, whereas Section 7.3.3 makes the semantics of nodes depend on that of equations. The correction of this recursive definition is guaranteed here by the rule governing module instantiation: no node can directly or indirectly instantiate itself. This rule implies that the nodes instantiated (directly or indirectly) by a node form a finite tree with as root, each node having as children the node instances it has as equations.

Fixed point computation

Consider a node . Assume its set of variables is and its set of inputs is ⊆ . Consider a valuation of its inputs ∈ ∞ . Then, the semantics of for input is ( ), where = ↾ . Under the definition of Section 7.7, ( ) is obtained by cyclically applying {{ }} to compute {{ }} ( ). But one application of {{ }} is already an infinite process, as it may build values at an infinity of cycles of . Therefore, this organization of the fixpoint definition cannot be used as a pattern for operational implementation.

To allow implementation, we need to choose a different order for the computation of variable values. We choose to always compute new values at the lowest cycle where it is possible. This is also the implementation strategy of classical reactive languages, where values are built cycle by cycle. In these languages, when all values of cycle are constructed, execution can move to cycle + 1. But when recurrences backwards in time are allowed, this is not always possible. For instance, in the training of RNNs by means of BPTT (as in Figure 19) a full recurrent input sample is processed by the forward path before back-propagation can start. For this reason, multiple cycles can can have values under construction. At every step of the fixpoint computation, we denote with the last cycle under construction. Whenever no new values can be built between cycles 0 and without using information of cycles of index > , we increment .

We denote with ( ) the set of all equations that, in fixed point simulation state , would change the value of a variable in cycle . It is formally defined as:

( ) = { | {{ }}( | ) > ( | ) }
where denotes the set of variables of equation . Given ∈ ∞ and ∈ , we denote [ ← ] the element of ∞ that equals in cycle and in every cycle ≠ . With these notations, the computation of the fixed point is realized using the algorithm in Figure 25. To simplify presentation, the algorithm assumes that node instantiates no other nodes. To cover node instantiation, the simulation state must be generalized to include not only the valuation of variables, but also the simulation state of every instantiated node, hierarchically under the form of a finite tree, and the state computation and update (lines 13-14) must be updated accordingly.

Notice that the fixed point iteration algorithm considers inputs incrementally. This means that state representations used during iteration are always finite, allowing implementation. Assuming in the theorem hypothesis that ( ) : ≠ : amounts to assuming that the semantics assigns at least one new value to at least one variable in a cycle of index ≥ . Without this assumption, the fixed point iteration algorithm would remain stuck in the internal while loop that computes (lines 7-13), as the semantics has no values to compute. P T 12. We first prove that {{{ }}} ( ) ≤ ( ) for all . This is done by induction. For = 0, {{{ }}} 0 ( ) = ⊥[0 ← 0 ] ≤ ≤ ( ). For the induction step, we denote with that must be used on all variables subject to back-propagation) and a classical notation for tensor shapes. Thus, "i:num [2,3]" defines variable i as a 2-dimensional floating point tensor with 2 lines and 3 columns. To avoid ambiguity, scalars are represented as tensors with 0 dimensions. Thus, "c:bool []" defines a Boolean scalar. Our mlrc compiler relies on XLA to allow efficient execution of functions such as Conv2D.

The front-end includes type and shape inference phases that will assign a fixed type and shape to all variables, starting from those of the inputs. This is required to allow simulation.

Prior to simulation, the front-end will perform full type/shape inference, inlining of all nodes in the main node, and a pass of advanced constant folding (which itself requires clock inference) to reduce the state size.

The algorithm in Figure 25 provides a first method to execute R(ML) 2 programs, one that was designed for generality (equivalence with denotational semantics) and simplicity. To attain efficiency, it must be further refined. The overall event-driven simulation method can be largely improved by optimizing the computation of the sets and the search for an equation to activate, at each step of the algorithm. In mlrc we do both. Each time a new value is computed for a variable in cycle , we determine which equations having as input can compute a new value. These equations are then added to the corresponding set, to be removed when the corresponding value is computed. We also exclude from the search in lines 4-11 the completed cycles where all values have already been computed. Furthermore, the valuations of these cycles can be deleted from the simulation state provided the cycle is not adjacent to a non-completed one. This allows reducing to a minimum the number of currently open cycles of the simulation state.

Of course, in an ML context most performance gains require replacing the event-driven simulation with statically-scheduled code optimizable by a compiler such as XLA. We currently only do it for individual functions.

IMPLEMENTATION

Considering a synchronous, bidirectionally causal program , the properties established in the previous section provide a concrete path to its interpretation. For the computation up to a given index , Theorem 4 states that it is sufficient to evaluate the semantic equations up to some bounded index + , and Theorem 3 states that + 1 live indices are sufficient to interpret the semantics equations of up to index . The value of is a function of in general, unless the program is actually bounded reactivewhere one may further establish an upper bound ¯ such that a maximal amount of ¯ + 1 live indices are sufficient. This is not yet sufficient to allow a practical implementation: one still needs to compute for any . To that end, let worklist denote the set of equations whose right-hand-side lead to a new (higher) value of a variable at cycle : worklist = {( = ) ∈ | = ( ) ⊐ ( ) }. This predicate may be evaluated recursively from the synchronous transformers in Figure 23, considering only the instantaneous left-hand side of the • operator, and memoizing the window of live indices lower or higher than the cycle of interest. In particular, one may choose to always compute new values at the lowest index possible, matching the implementation of classical reactive languages where values are computed cycle by cycle. When all values at index have reached a fixed point, execution can move to cycle +1, and memory for cycle can be reclaimed except for values held by fby operators. When the program is bounded reactive, the window of live indices remains bounded, making the implementation practical.

We implemented a front-end and interpreter for R(ML) 2 called mlrc. The syntax presented in the paper is extended with NumPy-like functional arrays and a (data) type system featuring 3 scalar types (bool, int and a floating point type num that must be used on all variables subject to backpropagation). Functional arrays feature a classical notation for tensor shapes: e.g. "i:num [2,3]" defines variable i as a 2-dimensional floating point tensor with 2 rows and 3 columns. Scalars are represented as tensors with 0 dimensions: e.g. "c:bool []" defines a Boolean scalar. The front-end includes type and shape inference passes to assign a type and shape to all variables, starting from the inputs. The version mlrc provided as supplementary material only supports primitive Ocaml functions and operators, while the full version relies on XLA [START_REF]The XLA team. XLA[END_REF] to support realistic neural networks.

While the algorithm we just sketched interprets any R(ML) 2 program, there is a lot of room for performance improvement. In particular, the mlrc implementation specializes the computation of worklist sets and the search for the next equation to evaluate. Each time a new value is computed for a variable at cycle , one may determine which equations having as input can compute a new value. These equations are then added to the corresponding worklist set, and retired when the value is eventually computed. One may also exclude from the search the completed cycles where all values have already been computed, and one may then recollect the storage locations associated with these unless the cycle is adjacent to a non-completed one.

CONCLUSION

We introduced R(ML) 2 , a bidirectional reactive programming language on unbounded streams with both forward and backward dependences. We illustrated the modularity and expressiveness of the language on a variety of ML models, algorithms and usage scenarios, with unprecedented parsimony-four traditional reactive constructs plus one original backward recurrence primitive. We provided an denotational synchronous semantics with higher expressiveness than traditional synchronous Kahn networks preserving its main productivity and bounded memory execution properties. Starting from a single reactive program, one may transform it structurally to compute both forward and reverse-mode gradients, leveraging bidirectional reactive semantics on streams instead of referring to an external data structure such as a gradient tape or cache. From this single reactive program, one may also derive backpropagation and (batched) training algorithms by inserting dedicated control signals around initialization and sampling primitives. The language also unifies the expression of models interacting with their environment, from reinforcement learning to front-end/back-end data processing and real-time control. A prototype is provided as supplementary material, as well as detailed simulations and discussion of the denotational semantics.

A KAHN SEMANTICS

For reference and comparison, we recall the definition of the Kahn domain then tentatively derive an asynchronous semantics [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF]. We show by example that such a semantics, being limited to prefix-closed stream values, leads to non-interesting least fixed points in the context of bidirectional reactive programming.

Kahn domain.

As announced earlier, we first experiment with providing R(ML) 2 with an asynchronous dataflow semantics over finite and infinite streams by exending the Kahn network formalism.

Let ≤ be the prefix order over streams: ≤ ⇐⇒ ∃ , = • . The ordered set = ( ∞ , ≤ , )-known as the Kahn domain [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF]-is a CPO with infimum and no supremum.

Asynchronous semantics on the Kahn domain. A tentative Kahn semantics extended to bidirectional reactivity is given in Figure 26. The interpretation of the associated stream transformers is given in Figure 27. The mark # distinguishes the syntactic construct from its interpretation as a stream transformer.

Notice the when false case may shrink an infinite stream into a finite (possibly empty) one. Notice also post = when (false fby true) : in this asynchronous semantics, post happens to be syntactic sugar for sampling with the stream false • true . From the merge # (false • 1: , , ) case of the merge # stream transformer, the Kahn semantics computes an empty stream for o at the first iteration. As a result, it immediately reaches a fixed point, making no progress at all in the computation of o. This deadlocking behavior is the direct result of the domain operating on prefixed-closed streams and is common to reactive languages on streams [START_REF] Bergerand | Outline of a real time data flow language[END_REF][START_REF] Elliott | Functional reactive animation[END_REF]. B CYCLE-BY-CYCLE SEMANTIC SIMULATIONS Beyond the backfill example discussed in the main paper, Figure 29 ilustrates a more complex case of sampling over values computed with the lookahead operator. Notice how ⊥ values in o stick in at cycles 0 and 1, and eventually disappear at cycle 2 ( o 0:3 ).

Figure 30 explores the semantics of merge (starting at cycle 2 for readability): the interpretation switches from ⊥ to known (blue) values much earlier, without waiting for the prefix of c to be known in full. Figure 31 goes one step further, illustrating the expressiveness of the synchronous semantics by revisiting the recurrent merge case (starting at cycle 2).

Fig. 1 .

 1 Fig.1. Expressiveness requirements for neural networks operating on streams w.r.t. network type. The core language covers the pale and bright yellow cells. Bidirectional reactivity is required for the orange cells.

Fig. 2 .

 2 Fig. 2. Syntax of the R(ML) 2 reactive language.

1

  node param (init)->(o) node diff_param(init,bp,do)->(o) 2 o = init; o = init fby o1; 3 o1 = o + merge bp do 0.0; 4 node dense(i)->(o) node diff_dense(i,bp,do)->(o,di) 5 b = param(0.0); b = diff_param(0.0,bp,db); 6 k = param(1.0); k = diff_param(1.0,bp,dk);

Fig. 3 .

 3 Fig.3. Complete gradient descent implementation in R(ML)2 . On the le (lines 1-21) the specification (node app) and a pipelined version of it (node app_pipe). On the right, the gradient descent implementation for every node, obtained by structural translation not detailed in this paper. At the bo om, inference and training nodes obtained by specialization of the gradient descent node diff_app_pipe.

Fig. 4 .Fig. 5 .

 45 Fig. 4. Inlining and normalization of the app node

Fig. 7 .Figure 7 .

 77 Fig. 7. Counter node in MLR Figure 7.In the first cycle (of index 0) its output (the value of variable o) is the value of the first input, which is 0. In cycle 1, it is the value of its second input (variable u) in cycle 0, which is 1. Inductively, we can prove that in every cycle the value of o is .Note that each fby equation of a node defines one element of the recurrence accumulator which defines the program state. Thus, the counter node above has a state formed of one integer, whereas the state of node app in Figure4is formed of two floatingpoint values. For a node that has not yet been inlined, the state is formed of the fby equations defined directly in , plus the state of all the node instances of .

Fig. 8 .

 8 Fig. 8. LSTM layer (square brackets index functional arrays).

4. 3 . 4 Fig. 9 .

 349 Fig.9. MLP with embedded data pre-processing.

Fig. 10 .

 10 Fig. 10. Sample chronogram of x = y when c.

Fig. 11 .

 11 Fig. 11. Sample chronogram of x = merge c y z.

Fig. 12 .

 12 Fig. 12. Sparsely-gated Mixture of Experts layer.

Fig. 13 .

 13 Fig. 13. Sample chronogram of x = post y. In red, data dependences.

Fig. 14 .

 14 Fig. 14. Backpropagation in pipelined applications: a possible trace of node diff_fby of Figure 3. In blue, dependences forward in time. In red, dependences backward in time.

Fig. 16 .

 16 Fig. 16. Bounded broadcast towards the past.

Fig. 19 .

 19 Fig. 19. LSTM of Figure 8 extended with backpropagation reset. node diff_fby_end(shape,end,init,i,bp,do)->(o,dinit,di) o = fby_end(end,init,i); rst1 = rst when bp; end1 = end when bp; dinit = merge rst1 (do when rst1) zeros(shape); di = merge end1 zeros(shape) (di1 when not end1); di1 = post (merge rst1 zeros(shape) (do when not rst1)); node diff_param_end(shape,end,p,bp,do)->(o,dp) o = o1; o2 = o1; (* dup *) do1 = do + do2; (* backpropagation for dup *) o1,_,do2 = diff_fby_end(shape,end,p,o2,bp,do1); node diff_lstm_end(units,sizex,x,end,bp,dh_next)->(h_next,dx) h_next,c_next,dh,dc,dx = lstm_cell_end(units,sizex,h, c,x,end,bp,dh_next,dc_next); hp = diff_param(orthogonal([units]),bp,dhp); cp = diff_param(orthogonal([units]),bp,dcp); h,dhp,dh_next = diff_fby_end(end,hp,h_next,bp,dh); c,dcp,dc_next = diff_fby_end(end,cp,c_next,bp,dc);Fig. 20. LSTM backpropagation training code.

Fig. 21 .

 21 Fig. 21. Bidirectional LSTM layer.

Fig. 22 .

 22 Fig. 22. Synchronous semantics.

Fig. 23 .

 23 Fig. 23. Synchronous stream transformers.

Fig. 24 .

 24 Fig. 24. Illustration of the synchronous semantics.

Definition 2 (•

 2 Bidirectional bounded reactivity). A program is bidirectionally bounded reactive if and only if the two following conditions hold on the synchronous interpretation : → ′ : (i) terminates, and (ii) ∃¯ ∈ N, ∀ ∈ N, = ì +¯ 0: . Let us now state two theorems that are essential to making the interpretation of the semantics effective and practical. Finite memory (possibly unbounded): considering a bidirectionally causal program and the look-ahead offset guaranteed by bidirectional causality at a given index , only needs to store windows of stream values of size + 1 to effectively interpret the semantics. • Bounded memory: considering a bounded reactive program and the look-ahead offset ¯ guaranteed by bounded reactivity for all indices, only needs to store windows of stream values of size ¯ + 1 to effectively interpret the semantics.

7. 6

 6 Semantics of primitives Definition 5 (Function application semantics). Consider a function : =1 → =1 , with ≥ 1 and the equation ="(y 1 , . . . , y ) = f(x 1 , . . . , x )". Its stateless iterator function is {{ }} # : =1 × {{ }} # ( 1 , . . . , , 1 , . . . , ) = = (( 1 , . . . , , 1 ∨ 1 , . . . , ∨ )) if = ? and ∀ : ∈ ( ∨ 1 , . . . , ∨ , ∨ 1 , . . . , ∨ ) otherwise where = ( 1 ) ∨ . . . ∨ ( ) ∨ ( 1 ) ∨ . . . ∨ ( ), and (when ∀ : ∈ ) ( 1 , . . . , ) = ( 1 , . . . , ).

Definition 9 (

 9 Semantics of fby). Consider the equation =" = k fby ", where ∈ = . Its iteration function is {{ }} : ∞ { , } → ∞ { , } defined by {{ }} = • , where: ( ) = [ , և ( [ ]), ( [ ])] -synchronization, involving no recurrence ( ) = [ և ( , )] -forward recurrence with:

1 : 2 : 4 = 8 : 8 : 13 : 14 :Fig. 25 .

 12488131425 Fig. 25. Fixed point iteration algorithm. It only terminates (in line 6) if the input is finite.

7. 7 . 1 T 12 .

 7112 Equivalence with denotational semantics. Along a given execution of the algorithm in Figure25, we shall denote with {{{ }}} ( ) the value of at the end of the ℎ iteration of the main iteration loop. Then, the fixed point iteration algorithm and the semantics are related by the following result: Under the previous definitions, for every ≥ 0, if ( ) : ≠ : , then there exists ≥ 0 such that ( ) 0: = {{{ }}} ( ) 0:

Fig. 26 .Fig. 27 .

 2627 Fig. 26. Kahn semantics.

Figure 28

 28 Figure28illustrates these definitions on the backfill example. Each row corresponds to the evaluation of one rule in the fixed point computation, effectively computing a new finite or infinite stream one row at a time. Blank cells are meant for visual alignment only, they are not meaningful in the domain. From the merge # (false • 1: , , ) case of the merge # stream transformer, the Kahn semantics computes an empty stream for o at the first iteration. As a result, it immediately reaches a fixed point, making no progress at all in the computation of o. This deadlocking behavior is the direct result of the domain operating on prefixed-closed streams and is common to reactive languages on streams[START_REF] Bergerand | Outline of a real time data flow language[END_REF][START_REF] Elliott | Functional reactive animation[END_REF].

Fig. 28 .

 28 Fig. 28. Illustration of the Kahn semantics deadlocking on a backward recurrence.

Fig. 29 . 36 DumitruFig. 30 .Fig. 31 .

 29363031 Fig. 29. Illustration of the synchronous semantics, sampling on a lookahead condition.

See also https://en.wikipedia.org/wiki/Functional_reactive_programming.

E.g. for embedded and real-time applications.

The param node deserves a specific note: it has dedicated, non-standard translation during the synthesis of backpropagation code, as discussed in Section 4.5. Yet in inference mode param translates to the identity function. For consistency throughout this paper, we assume that the synthesis of backpropagation code is performed prior to any inlining of param.

A chronogram displays the successive values of streams of interest at every cycle index in a given range. Cyclic execution allows us to graphically align multiple streams, since indexes coincide with computation cycles.

In a cyclic graph formed only of function applications, a computation would depend on its own input, resulting in deadlock.

Also known as rotating buffers.

Node dense1 provides here a more faithful implementation of the Keras layer Dense than the node dense of Figure3.

Specific language constructs, like TensorFlow's stop_gradient, are needed to avoid backpropagation through the data processing code, but these mechanisms are outside the scope of our paper.

And neither are, for of the sake of the presentation presentation, the issues of selectively saving or loading the state of fby primitives.

5

To simplify the code in Figure3, we assume in the definition of diff_fby1 that its first argument is a constant, requiring no backpropagation. A full-fledged version of fby backpropagation is provided in Section 5.3.

As a corollary of continuity, the iterates (⊥) form an ascending chain, i.e. successive iterates of propagate information monotonically, structurally from sub-expressions of and from input arguments bound in .

Which means that, for the same input, the sycnhronization error can be first detected, depending on the equation evaluation order, in different equations. The use of allows propagating the error towards a unique end-state.

Or, equivalently, ( ) is a fixed point of for all .

Like the semantics in Section 6 does.

We define : → {⊥, , ?, } as the function that strips the value of a variable, preserving only its synchronization status:

Multi-variable domain. Given a set of variables , we represent their semantic status at a given execution step with elements of = ∈ . Given ∈ and ∈ , we denote with [ ] the value of in . We overload the ⊥ notation to (also) denote the element of with [ ] = ⊥ for all ∈ . We similarly overload in the notations , ?, and . is naturally endowed with the product domain structure, where ⊥ and are respectively least and greatest elements, ≤ is the partial order over , and ∨ is the (completely-defined) supremum operator. If ∈ , 1 , . . . , ∈ and ∈ , then [ 1 , . . . , ← 1 , . . . , ] is the element of that equals on and [ ] for all ∉ . We also denote [ 1 , . . . , և 1 , . . . , ] = ∨ [ 1 , . . . , ← 1 , . . . , ] the update operator that never loses information. We denote with the endomorphism : → that returns if at least one component of its input is , and returns its input otherwise.

Domain of streams.

If is the set of variables of a program or set of equations , the we will use streams of ∞ to represent both (finite or infinite) execution traces and the semantic states used in the construction of the traces. Recall that if ∈ ∞ , then ∈ is the element of of index ≥ 0. In a trace/semantic state ∈ ∞ , we will say that execution has reached cycle ≥ 0 if there exists ≥ with ≠ ⊥. For ∈ ∞ we denote with ( ) ∈ N ∪ {∞} its length. The partial order ≤ on induces a partial order ≤ on ∞ as follows: 1 ≤ 2 if, by definition, ( 1 ) ≤

( 2 ) and 1 ≤ 2 for all 0 ≤ < ( 1 ). Endowed with ≤, ∞ is a complete lattice with infimum and supremum ∞ . The supremum operator is denoted ∨.

Semantic functions

Given a set , we denote with the identity function over . For instance, ∞ is the identity function over ∞ .

Given a domain ( , ≤), and another set , we also denote with ≤ the poinwise partial order induced on (the set of functions from to ) by the partial order of . We respectively denote with ∨ and ∧ the supremum and infimum operators induced by ≤.

Assume is the set of variables used by a program or set of equations . We will define the semantics of as a function ∈ ( ∞ ) ∞ . We must always have:

, so that applying the semantics does not lose information present in the input. • is idempotent 18 so that all the values that can be computed by given the input will be present in ( ), and applying a second time builds no new values.

Fixpoint iteration function.

Recall that given a directed-complete partial order (CPO) ( , ≤), a continuous function : → , and ∈ , the least fixed point of greater than , denoted ( , ), exists and can be computed as:

To ensure that ( ) can be incrementally computed for every , we will require that it is defined as the least fixed point greater than of another function {{ }} ∈ ( ∞ )

∞ called the fixpoint Dumitru Potop Butucaru, Albert Cohen, Gordon Plotkin, and Hugo Pompougnac +1 the function used to construct {{{ }}} +1 ( ) from {{{ }}} ( ), as defined in lines 15-16 of the algorithm. As +1 is obtained from {{ +1 }} for some equation +1 , it is by construction smaller than {{ }} (itself the union of {{ }} for all equations ). Then: {{{ }}} +1 ( ) = +1 ({{{ }}} ( )) ≤ {{ }}({{{ }}} ( )) ≤ ({{{ }}} ( )) ≤ ( ( )). And since ( ) is a fixed point of , the induction step is complete.

From {{{ }}} ( ) ≤ ( ) for all we can then deduce {{{ }}} ( ) 0: ≤ ( ) 0: for all , . To complete the proof of our theorem, we need to find a value of for which the reverse inequality holds. Since ( ) = lim →∞ {{ }} ( ), we obtain that there exists 0 such that ( ) 0: = {{ }} ( ) 0: for all ≥ 0 . Then, proving our theorem can be done by proving that for every ≥ 0 and ≥ -1 there exists , such that {{{ }}} , ( ) 0: ≥ {{ }} ( ) 0:

(

We prove this by outer induction over and inner induction over . Recall that 0:-1 is the empty stream, so that property (1) is trivially satisfied for = -1 for any and ,-1 . We choose ,-1 = 0 for all , and thus have solved the base case for the inner induction for all .

Induction over , base case. For = 0 and ≥ -1, we need to prove that for every there exists 0, such that {{{ }}} 0 ( ) 0: ≥ 0: . For = -1 the property has been established above. For ≥ 0, from the theorem hypothesis, ( ) : ≠ : , which implies that the fixed point computation proceeds to at least cycle , and each time is incremented the values of for cycle are included in (in line 11). Thus, for 0, = , {{{ }}} 0, ( ) 0: ≥ 0: . Induction step over . As induction hypothesis we assume that for all we have constructed , such that {{{ }}} , ( ) 0: ≥ {{ }} ( ) 0: . From the monotony of {{ }} we have {{ }} ( ) ≤ {{ }} +1 ( ).

If {{ }} ( ) 0: = {{ }} +1 ( ) 0: , then from the induction hypothesis we have {{{ }}} ( ) 0: ≥ {{ }} +1 ( ) 0: , so the induction step is verified for +1, = , .

If {{ }} ( ) 0: ≠ {{ }} +1 ( ) 0: , then {{ }} ( ) 0: < {{ }} +1 ( ) 0: . This is equivalent to there existing ≥ 1 distinct variables 1 , . . . , ∈ and 0 ≤ 1 , . . . , ≤ such that {{ }} +1 ( ) [ ] > {{ }} ( ) [ ]. We will determine that for every 1 ≤ ≤ there exists > , such that {{ }} +1 ( ) [ ] = {{{ }}} ( ) [ ]. Once this is proven, property (1) is satisfied for +1, = max =1 .

Consider ( , ) one of the pairs with {{ }} +1 ( ) [ ] > {{ }} ( ) [ ]. By construction, cannot be an input of , but an output of a unique equation of . Let be this equation. From the definition of {{ }}, we know that the value is produced by {{ }} in the context provided by {{ }} ( ).

If

is not a "fby back" equation, then this context can be restrained to {{ }} ( ) 0: , which is included in {{{ }}} , ( ) 0: . Equation is therefore part of in state {{{ }}} , ( ). As such, it will be executed in a finite number of steps of the fixed point iteration (in the worst case, after all variables are assigned a new value in all cycles ≤ ). Then, we can set

IMPLEMENTATION

To allow the evaluation of R(ML) 2 , we have implemented a full front-end and simulator named mlrc. It covers the language introduced in the paper, extended with NumPy-like functional arrays and a (data) type system featuring 3 scalar types (bool, int, and a type foating point type num