MIT, USA Eric Atkinson

Guillaume Baudart

Louis Mandel

Charles Yuan

Michael Carbin

Statically bounded-memory delayed sampling for probabilistic streams

Keywords: CCS Concepts:, Theory of computation → Program analysis, Streaming models, • Software and its engineering → Data ow languages Probabilistic programming, reactive programming, streaming inference, semantics, program analysis

published or not. The documents may come

INTRODUCTION

Probabilistic programming languages aid developers performing Bayesian inference [START_REF] Atkinson | Verifying Handcoded Probabilistic Inference Procedures[END_REF][START_REF] Bingham | Pyro: Deep Universal Probabilistic Programming[END_REF][START_REF] Marco F Cusumano-Towner | Gen: a General-purpose Probabilistic Programming System with Programmable Inference[END_REF][START_REF] Ge | Turing: Composable inference for probabilistic programming[END_REF][START_REF] Gelman | Stan: A probabilistic programming language for Bayesian inference and optimization[END_REF][START_REF] Goodman | Church: A language for generative models[END_REF][START_REF] Noah | The Design and Implementation of Probabilistic Programming Languages[END_REF][START_REF] Gordon | Tabular: a schema-driven probabilistic programming language[END_REF][START_REF] Huang | Compiling Markov Chain Monte Carlo Algorithms for Probabilistic Modeling[END_REF][START_REF] Mansingkha | Probabilistic Programming with Programmable Inference[END_REF][START_REF] Milch | BLOG: Probabilistic models with unknown objects[END_REF][START_REF] Narayanan | Probabilistic inference by program transformation in Hakaru (system description)[END_REF][START_REF] Nori | Ecient Synthesis of Probabilistic Programs[END_REF]Pfe er 2009;[START_REF] Tran | Deep probabilistic programming[END_REF]]. These languages provide programming constructs and tools for probabilistic modeling and automated inference. Researchers have developed probabilistic programming languages for several domains, including data science [START_REF] Gelman | Stan: A probabilistic programming language for Bayesian inference and optimization[END_REF], machine learning [START_REF] Bingham | Pyro: Deep Universal Probabilistic Programming[END_REF][START_REF] Tran | Deep probabilistic programming[END_REF], scientic simulation [START_REF] Güneş Baydin | Etalumis: Bringing Probabilistic Programming to Scientic Simulators at Scale[END_REF], and real-time control [START_REF] Baudart | Reactive Probabilistic Programming[END_REF]].

Probabilistic Programming with Streams. In this paper, we consider programs that accept inputs and compute outputs at discrete time steps, with the outputs of each step owing into the environment to aect future inputs to the program. Mathematically, one can model these programs as computations that operate on and produce innite streams. Computing with streams is a common computational model for applications in real-time control, such as robotics and avionics [START_REF] Colaço | SCADE 6: A formal language for embedded critical software development[END_REF]. For example, control for an airplane y-by-wire system can be implemented as a program transforming a stream of altitude measurements into a stream of commands to the engine. [START_REF] Baudart | Reactive Probabilistic Programming[END_REF] introduced a probabilistic programming language, ProbZelus, to enable probabilistic programming in this domain of computations on streams. A key innovation of ProbZelus was to demonstrate that delayed sampling [Murray et al. 2018] could be extended to work with streams to provide high-quality inference procedures. Delayed sampling is an inference algorithm that combines both exact and approximate inference; it takes advantage of exact inference when ecient known closed-formed solutions exist and falls back on sampling-based, approximate inference when required. Specically, delayed sampling combines Bayesian networks -graphs that encode exact distributions of probabilistic models -with particle ltering [START_REF] Del Moral | Sequential Monte Carlo samplers[END_REF]]an approximate inference algorithm.

The challenge in adapting delayed sampling to computations on streams is that such computations run for indenite periods of time and are often subject to stringent limits on resources, such as memory. [START_REF] Baudart | Reactive Probabilistic Programming[END_REF] showed that, in many cases, only a nite number of nodes in delayed sampling's graph data structures were reachable at any given time, and the rest could not inuence the computation in the future and could be removed from memory. However, this behavior depends on the probabilistic model under consideration; delayed sampling is not guaranteed to maintain a bounded amount of memory for all programs. The result is then that though probabilistic programming languages are designed to hide the complexities of developing probabilistic inference algorithms, certain combinations of a model and the inference algorithm will result in undesirable behaviors that the developer did not anticipate. Moreover, the developer has no means to reason about these behaviors except by inspecting the implementation of the inference algorithm.

Bounded-Memory Delayed Sampling. In this paper, we formalize semantic conditions under which applying delayed sampling to probabilistic programs with streams will execute in bounded memory.

The two conditions are dataow properties of the core operations of delayed sampling: assume, observe, and value, which respectively add a new random variable to the delayed sampling graph, observe a random variable, and evaluate a random variable to produce a sampled value. The <consumed property states that all variables introduced with assume are eventually consumed by an observe or a value, or are passed to other assumes resulting in new variables that are themselves (< 1)-consumed. An unseparated path is a sequence of random variables, each passed as parameter to the assume operation of the next, where no variable is passed to an observe or value operation. The unseparated paths property states that no variable maintained in the program state starts an unseparated longer than some xed bound =. A program executes in bounded memory under delayed sampling if, and only if, it satises the <-consumed and unseparated paths properties.

Static Analysis. We propose a static analysis that checks the <-consumed and unseparated paths properties to soundly ensure that any program that passes the analysis satises these properties, and thus executes in bounded memory under delayed sampling.

Contributions. In this paper, we present the following contributions:

• We introduce and formalize the <-consumed and unseparated paths properties, and show these are necessary and sucient for a program to have bounded-memory execution. • We present a static analysis to check these properties, and prove that the analysis is sound.

• We implement the analysis and evaluate it against several probabilistic inference benchmarks.

Our results show that for eight of nine benchmarks, the analysis determines whether the semantic properties necessary for bounded-memory execution are satised, and we identify the precision limitation of conservative static analysis on the remaining benchmark.

This work brings probabilistic programming to control settings with the new benet of static guarantees on the system's resource consumption. To the best of our knowledge, our work is the rst to develop a resource analysis for a probabilistic program in relation to its probabilistic programming system's underlying inference algorithm.

The remainder of the paper is structured as follows. In Section 2, we give an example program to illustrate the concepts in the paper. In Section 3, we present the syntax and semantics of a language for probabilistic programming with streams, adapted from the ` language from [START_REF] Baudart | Reactive Probabilistic Programming[END_REF]. In Section 4, we review background on delayed sampling, based on the contributions from Murray et al. [2018] and [START_REF] Baudart | Reactive Probabilistic Programming[END_REF]. In Section 5, we present the <-consumed and unseparated paths semantic properties. In Sections 6 and 7, we present and evaluate the static analysis. Sections 8 and 9 summarize related work and present conclusions.

EXAMPLE

Figure 1 presents the example of a robot designed to navigate to a desired position target using measurements obs from a noisy position sensor. The robot issues a command u that indicates the acceleration to apply to change its position. The robot (1) estimates its current position with a probabilistic model kalman and (2) uses this estimate to compute the command u with a deterministic controller (e.g., a Linear-Quadratic Regulator [START_REF] Sontag | Mathematical control theory: deterministic nite dimensional systems[END_REF]], the implementation of which we have elided for simplicity). We present the example in ` , a purely functional core calculus for probabilistic programming with streams. The program is a set of stream function denitions that each consist of (1) an initializer, and (2) a step function that given the previous state and an input value produces an output value and a new state [START_REF] Mealy | A method for synthesizing sequential circuits[END_REF]]. The operators init and infer instantiate a stream function by creating an internal state. A stream function can be applied to an input stream to generate an output stream with the operator unfold, which applies the step function using the internal state and the input values. Unlike init, the step function of an instance created using infer performs probabilistic inference and thus returns at each iteration a distribution of outputs and a distribution of states.

The main stream function, robot, has a state composed of two stream function instances: c the deterministic controller, and k the kalman probabilistic model. The robot initializer creates these two instances (L.9). The transition function of instance k performs probabilistic inference to infer a distribution of the robot's state x_dist and an updated instance k (L.11). Then the transition function of instance c computes a command u to go toward the destination target using statistics of the position distribution and an updated instance c (L.12). The transition function of robot returns the command u and the updated state (L.13).

Probabilistic Model

The stream function kalman species a hidden Markov model [START_REF] Baum | Statistical Inference for Probabilistic Functions of Finite State Markov Chains[END_REF], a common probabilistic model for tracking applications in which the goal is to estimate the trajectory of an object given noisy measurements of the object's position.

The stream function's state consists of a latent random variable, pre_x, that denotes the position of the robot at the previous iteration. The robot's state is latent in that the robot is unable to directly observe its position; instead it must leverage a noisy measurement or observation of its position to infer a probability distribution over its potential states.

Inside the denition of kalman, the program models the latent nature of x by sampling the current position from a Gaussian distribution centered around its previous position pre_x (L.4). The program models the observation by taking the observed sensor value as input, obs, and supplying it as an input to the observe operator. In this example, the observe species that obs is an observation from a Gaussian distribution centered around the position x. The observe operator conditions the program's execution on the observed value (L.5) in that it adjusts the distribution that will be inferred for x.

The sequence of diagrams in Figure 2 illustrates the evolution of a representation of the hidden Markov model over the rst four iterations of the program. Each light grey node denotes a latent random variable for pre_x or x at a given iteration. Each dark grey node denotes an observation at the given iteration. Each solid black arrow signies a dependence between random variables as in a traditional Bayesian network representation of a probabilistic graphical model [START_REF] Koller | Probabilistic Graphical Models -Principles and Techniques[END_REF]. Of note, each observation at each iteration depends on the current position and the robot's state at a given iteration depends only on its position at the previous iteration.

Inference with Delayed Sampling

The kalman probabilistic model is not sucient for the robot to reason about its position. Instead, the robot must perform inference on the model to compute a posterior distribution of x conditioned on its observations. As mentioned, the infer operator in the robot stream function applies inference to the probabilistic model it receives as input. In this paper, we study delayed sampling [START_REF] Baudart | Reactive Probabilistic Programming[END_REF]Murray et al. 2018] as the algorithmic implementation of the infer operator.

Delayed sampling is an extension of a particle ltering algorithm that leverages symbolic execution to reason about the relationship between random values and perform exact inference if possible. A particle lter estimates the posterior distribution from a set of particles, i.e., independent executions of the model. For each particle, delayed sampling operates by dynamically maintaining a graph -i.e., a Bayesian network -that records the dependence relationships between the random variables in the program (Figure 2). The key idea is that rather than sample a concrete value for each random variable in the program (e.g., x), delayed sampling instead returns a reference to a node in the graph. This node contains a closed-form representation of the distribution that the sample operator sampled from, along with the distribution's dependence on other random variables in the program. If a symbolic computation fails, delayed sampling can fall back to a particle lter by drawing concrete values for the random variables. [START_REF] Baudart | Reactive Probabilistic Programming[END_REF]. Each node denotes either a value (dark gray) or a distribution (light gray). A plain arrow denotes a dependency in the underlying Bayesian network. A doed arrow denotes a pointer in the implementation of the delayed sampling graph. Each label indicates the program variable that corresponds to a node. An 7 on a node denotes that the node is not reachable from the program state.

Bounded-Memory Delayed Sampling

A key concern when applying delayed sampling to streams, which may execute for an indenite number of iterations, is if the size of the delayed sampling graph is bounded from above by a xed constant for all iterations of the program. If not, then the delayed sampling graph may not consume bounded memory and the program may exhaust its resources if permitted to execute indenitely.

In general, bounding memory use is challenging because the underlying Bayesian network can in fact be unbounded. Nevertheless, a delayed sampling implementation can maintain bounded memory for some programs, depending on the operation of said programs. In this subsection, we review the delayed sampling implementation presented by [START_REF] Baudart | Reactive Probabilistic Programming[END_REF] which can execute in bounded memory for some programs.

Bounded-Memory Example. Figure 2 shows how delayed sampling maintains bounded memory for the program in Figure 1. For each particle, the delayed sampling implementation must keep in memory all the nodes that are reachable from any node referenced in the program state. The dashed lines in Figure 2 visualize the reachability relation, where the node each line points to is reachable from the node the line points from. As the program evolves its state and changes the variables the state contains, nodes in the delayed sampling graph may become unreachable, marked 7.

Figure 2a shows the delayed sampling graph after the rst iteration. The graph consists of two nodes: one introduced by sampling the variable x, and one introduced by the observation of obs. At the end of the step, both are in the program state and reachable.

Figure 2b shows the delayed sampling graph after the second iteration. The program has added two nodes to the graph for sampling x and observing obs. The nodes left over from the rst iteration are still in the graph, but are no longer reachable.

Figures 2c and2d show the delayed sampling graph at iterations 3 and 4 respectively. In each case, the most recently introduced nodes for x and obs are reachable, and the nodes from the previous iterations are unreachable. In general, the program ensures that at any iteration, the most recently introduced nodes are reachable, and the rest are unreachable. Because there are at most two reachable nodes for all iterations, inference executes in bounded memory.

Unbounded-Memory Example. Figure 3 presents an example of a program that does not execute in bounded memory. This is a modied version of kalman from Figure 1 that samples an initial latent position i from a Gaussian distribution and keeps a reference to this random variable in the state. Figure 4 shows how the program in Figure 3 fails to maintain bounded memory.

Figure 4a shows the delayed sampling graph after the rst iteration. The graph consists of three reachable nodes introduced by sampling the variables i and x and by the observation of obs.

val kalman_first = stream { init = (true, 0.0, 0.0); step ((first, i, pre_x), obs) = let (i, pre_x) = if first then (let i = sample (gaussian (0.0, 1.0)) in (i, i)) else (i, pre_x) in let x = sample (gaussian (pre_x, 1.0)) in let () = observe (gaussian (x, 1.0), obs) in (x, (false, i, x)) } Fig. 3. Model with unbounded memory consumption. g 2 = x 1 f nil :: y 1 f x 1 :: obs y 1 :: x 2 f x 1 :: y 2 f x 2 :: obs y 2 iteration 1 iteration 2 Fig. 5. A depiction of a trace of the program in Figure 1. The figure depicts the trace g 2 at the end of iteration 2. The trace is a ::-separated list of primitive operations, where each primitive operation is a sampling operation f or an observation operation obs. In this diagram, we use x = and y = to refer to the random variables introduced at iteration = by, respectively, sampling x and observing obs in Figure 1.

Figure 4b shows the delayed sampling graph after the second iteration. The program has added two nodes to the graph for sampling x and observing obs. Since the variable i is in the program state, the node between i and x is reachable.

Figures 4c and4d show that in the next iterations two new nodes are introduced at each step and one remains reachable. The primary observation to note is that the number of introduced nodes increases at every iteration. Therefore, there is no bound on the size of the delayed sampling graph and, hence, the program does not execute in bounded memory.

Analyzing Delayed Sampling

In this paper, we present an analysis that can show that the program in Figure 1 maintains bounded memory while the program in Figure 3 does not. For that, we dene two dataow properties that encode whether a program executes in bounded memory: the unseparated paths property and the <-consumed property. We then show how these properties can be veried using a static analysis.

Traces. We formalize the dataow properties as properties of traces. A trace is a recording of the important features of a program execution. In our case, a trace records all sampling and observation operations that the program has executed, as well as the variables that were involved in these operations. Figure 5 illustrates a trace of the execution of the program in Figure 1. Unseparated Paths. An unseparated path in a trace is a sequence of variables {G 8 }, where the trace species that each variable G 8 was sampled from its predecessor G 8 1 and no G 8 is observed.

g 2 = i f nil :: x 1 f i :: y 1 f x 1 :: obs y 1 :: x 2 f x 1 :: y 2 f x 2 :: obs y 2 iteration 1 iteration 2

E 2 = (false, i, x 2 )
Fig. 6. A depiction of a trace of the program in Figure 3. The figure depicts the trace g 2 and the value of the program state E 2 at the end of iteration 2. In this diagram, we use i, x = , y = , respectively, to refer to the random variable introduced by sampling i, the variable introduced at iteration = by sampling x, and the variable introduced at iteration = by observing obs in Figure 3. We have highlighted the elements of the unseparated path between 8 and x 2 in green.

The unseparated paths property states that there is a uniform bound 2 so that for all iterations no variable in the program state starts an unseparated path with more than 2 variables in it. Figure 6 illustrates the trace for the program in Figure 3. This program carries the variable i in the program state, and because the trace species that x 1 was sampled from i, and x 2 was sampled from x 1 , the sequence i, x 1 , x 2 is an unseparated path with 3 variables. In general, at iteration =, the program in Figure 3 maintains that i is in the program state and starts an unseparated path with length = + 1. Because no bound can exist on the length of this path for an arbitrary number of iterations, this program fails the unseparated path property. <-consumed. A variable is <-consumed if it is no more than < sampling operations away from a variable that is consumed by an observe statement. The <-consumed property states that there is a uniform bound < such every variable introduced by a sampling operation is <-consumed for some <  <. We note that the traces in Figures 5 and6 satisfy the <-consumed property, because every variable is at most 2-consumed. For all C, y C is 0-consumed because it is directly observed, and x C is 1-consumed because y C is sampled from x C and y C is 0-consumed. The variable i is 2-consumed because x 1 is sampled from i, and x 1 is 1-consumed.

The Outlier benchmark presented in Section 7 is an example of a program that fails the <consumed property, and thus does not execute in bounded memory. This program sometimes observes values close to the true latent state but otherwise observes values from an outlier distribution. When the program observes a value from the outlier distribution, it fails to observe any dependencies of the latent state, and thus cannot guarantee that the latent state is <-consumed. Over time, if the program performs latent state updates that remain unobserved (due to the program always observing from the outlier distribution), the lack of this guarantee results in there being no uniform bound < under which the latent state could be <-consumed.

Analysis. Our goal is ultimately to analyze whether a given program executes in bounded memory. As we show in Section 5, a program execution maintains bounded memory if and only if it satises both the unseparated path and <-consumed properties. This reduces the problem of analyzing the bounded-memory behavior of a program to analyzing these dataow properties. Our analysis utilizes an abstract delayed sampling graph, formally dened in Section 6, with the key aspects of these properties. For <-consumed, the abstract graph maintains a set of variables that have been introduced but not yet consumed, and for unseparated paths, it maintains an upper bound on their length. For example, the abstract graphs for the trace in Figure 6 are given in Figure 7.

g 2 = i f nil :: x 1 f i :: y 1 f x 1 :: obs y 1 :: x 2 f x 1 :: y 2 f x 2 :: obs y 2 iteration 1 iteration 2

<-consumed i x 1 y 1 x 2 y 2
unseparated paths (i, i), 0 (i, x 1 ), 1 (i, y 1 ), 2 (i, x 1 ), 1 (i, x 2 ), 2 (i, y 2 ), 3 (i, x 2 ), 2 Fig. 7. A depiction of the abstract graphs of the program in Figure 3, with the same trace as Figure 6. At each operation, we depict the <-consumed abstract graph, a set of nodes that have been introduced but not consumed. Because this set is empty at the end of any iteration, the program satisfies the <-consumed semantic property. The unseparated paths abstract graph is a mapping, for each unseparated path in the graph, from its endpoints to its length. We depict the longest path in the mapping. Aer each iteration, this longest path continues to lengthen, so the program does not satisfy the unseparated paths semantic property.

LANGUAGE MODEL

In this section, we present a semantics for probabilistic programs with streams using the language ` . We have adapted ` from [START_REF] Baudart | Reactive Probabilistic Programming[END_REF]'s core calculus for probabilistic programs and extended it with syntax for explicit streams.

Syntax

The syntax of the ` language is dened according to the following grammar: A program is a set of value, function, and stream function denitions followed by the name of the main stream function. A stream function < is composed of an initial state (init) and a transition function (step). Given a state and an input, the transition function returns an output and a new state. An expression is either a value (constant, variable, or pair), the application of a primitive operator (arithmetic operator, distribution, etc.), a function call, a conditional, or a local denition. The expression init(<) creates an instance of a stream function, and unfold(G,E) applies the instance G of a stream function on an input and returns the next element and the updated instance. Finally, the set of expressions comprises the probabilistic operators sample, observe, and infer. Nested inference and higher-order functions on streams are not allowed in the language. We require that arguments for all syntactic operators are values to simplify the presentation of the semantics. Since new variables can always be introduced to capture the value of any expression, this choice does not reduce the expressiveness of the language.

Semantics

The execution of a program ? = 3 ⇤ < comprises three steps. First, declarations 3 ⇤ are evaluated to produce an environment W which contains the denition of the main stream function <. Second, an instance of the stream function < is created. Third, the instance is iteratively applied on an input stream (8 = ) = 2N to produce an output stream (> = ) = 2N , dened in the following way: The semantics of deterministic expressions corresponds to a rst order functional language with new constructs to handle streams and the infer(•) operator (the complete denition is given in Figure 16 of Appendix A). The expression init(<) creates an instance of the stream function <: a pair corresponding to the current state, and the transition function. The current state is initialized with the value of the init eld. The expression unfold(G,E) executes the transition function of the instance G on its current state and the input E. This expression produces a pair composed of the transformed value and the updated instance.

»val G = 4… W = W [G »4… W ] »val 5 = fun ? -> 4… W = W [5 (_E. »4… W +[E/? ] )] »val < = stream { init = 4 init ; step(? state ,? input ) = 4 }… W = W [< stream { init = 4 init ; step(? state ,? input ) = 4 } W ] »init(<)… W = let stream { init = 4 init ; step(? state ,? input ) = 4 } W 0 = »<… W in let B init = »4 init … W 0 in (B init , _(B, E). »4… W 0 +[B/? state ,E/? input ] ) if 4 is deterministic »init(<)… W = let stream { init = 4 init ; step(? state ,? input ) = 4 } W 0 = »<… W in let B init = »4 init … W 0 in (B init , _(B, E). {[4]} W 0 +[B/? state ,E/? input ] ) if 4 is probabilistic »unfold(G,E)… W = let E state , 5 = »G… W in let E output , E 0 state = 5 (E state , »E… W ) in (E output , (E 0 state , 5 )) »infer(<)… W = let stream { init = 4 init ; step(? state ,? input ) = 4 } W 0 = »<… W in let B init = »4 init … W 0 in (X B init , infer (_(B, E). {[4]} W 0 +[B/? state ,E/? input ] )) where infer (5 ) = _(f, E). let `= _* . Ø ( f (3B) 5 (B, E)(* ) in let a = _* . `(* )/`(>) in (c 1⇤ (a), c 2⇤ (a))
»?…(8) = = > = where ? = 3 ⇤ < W = »3 ⇤ … ; B 0 = »init(<)… W > = , B =+1 = »unfold(B = ,8 = )… W 8= 0
The ideal semantics of ` probabilistic expressions {[•]} is a measure-based semantics similar to the one presented by [START_REF] Staton | Commutative Semantics for Probabilistic Programming[END_REF] (the complete denition is given in Appendix A). Given an environment W, an expression is interpreted as a measure {[4]} W : ⌃ ⇡ ! [0, 1), that is, a function which associates a positive number to each measurable set * 2 ⌃ ⇡ , where ⌃ ⇡ denotes the ⌃-algebra of the domain of the expression ⇡ (i.e., the set of measurable sets of possible values). sample(E) returns the distribution »E… W . observe(E 1 ,E 2 ) weights execution paths using the likelihood of the observation »E 2 … W w.r.t. the distribution »E 1 … W (for a distribution `we denote its probability density function as `pdf ). Local denitions are interpreted as integration, and we use the Dirac delta measure to interpret deterministic expressions. The infer(<) operator creates an instance of a probabilistic stream: the initial state is a Dirac delta distribution on the initial state of <, and the transition function is infer (5 ) where 5 is the transition function of <. The body of 5 (the expression 4) is interpreted with the probabilistic semantics which denes a measure over pairs of output values and states. The function infer (5 ) takes as arguments a distribution of states f and an input E and returns a distribution of outputs and a distribution of new states. These two distributions are obtained by integrating the transition function 5 along the distribution f of possible states (domain () to build a measure `which is then normalized to build a distribution a of pairs (outputs, states). The distribution a is then split into a pair of marginal distributions using the pushforward of a across the projections c 1 and c 2 .

{[E]} W = _6, F . (»E… W , 6, F) {[op(E)]} W = _6, F . (app(op, »E… W ), 6, F) {[5 (E)]} W = _6, F . W (5 )(»E… W )(6, F) {[let ? = 4 1 in 4 2 ]} W = _6, F . let E 1 , 6 1 , F 1 = {[4 1 ]} W (6, F) in {[4 2 ]} W +[E 1 /? ] (6 1 , F 1 ) {[if E then 4 1 else 4 2 ]} W = _6, F . let 1, 6 1 = value(»E… W , 6) in if 1 then {[4 1 ]} W (6 1 , F) else {[4 2 ]} W (6 1 , F) {[unfold(G,E)]} W = _6, F . let E state , 5 = »G… W in let (E output , E 0 state ), 6 0 F 0 = 5 (E state , »E… W )(6, F) in ((E output , (E 0 state , 5 )), 6 0 F 0 ) {[sample(E)]} W = _6, F . let -, 6 0 = assume(»E… W , 6) in (-, 6 0 , F) {[observe(E 1 ,E 2 )]} W = _6, F . let -, 6 G = assume(»E 1 …, 6) in let E, 6 E = value(»E 2 …, 6 G ) in let 6 0 = observe(-, E, 6 E ) in ((), 6 0 , F ⇤ `pdf (E))

DELAYED SAMPLING

In this section, we present the details of delayed sampling that underpin this work. This is a new formalization of results that were presented by Murray et al. [2018] and [START_REF] Baudart | Reactive Probabilistic Programming[END_REF].

Delayed sampling is a semi-symbolic algorithm combining exact inference and -when exact computation fails -approximate inference with particle ltering [START_REF] Del Moral | Sequential Monte Carlo samplers[END_REF]. A particle lter launches multiple executions of the model. Each execution -or particle -is associated to a weight. In the operational semantics, sample(3) statements draw samples from the corresponding distributions, and observe(G,3) statements update the weight to reect the quality of the samples. At the end of the executions the results of all the particles are normalized according to their weights to form a categorical distribution that approximates the posterior distribution of the model.

In delayed sampling, each particle contains a graph of random variables and their dependencies that can be used to compute closed-form distributions. Observations can be incorporated by analytically conditioning the network. If symbolic conditioning fails, inference falls back to a particle lter, drawing concrete samples for required random variables.

Operational Semantics

The denition of infer in Figure 8 makes use of an intractable integral. The delayed sampling semantics replaces this integral by a discrete sum over the set of particles of the particle lter. Compared to traditional particle ltering, delayed sampling performs exact computations when possible. Thus, we extend values E with symbolic terms. Symbolic terms include random variables (-) -the nodes of the delayed sampling graph -and applications of operators.

E ::= ... | -| app(op, E)
The semantics in Figure 9 rely on the following high-level operations to update the graph 6. E 0 , 6 0 = value(E, 6) samples all the random variables in E to produce a concrete value. 6 0 = observe(-, E, 6) conditions the graph on the fact that the random variabletakes the value E.

-, 6 0 = assume(3, 6) adds and returns a new random variablewith distribution 3.

Probabilistic semantics. The semantics of a probabilistic expressions are dened in Figure 9. The semantics of an expression {[4]} W,6,F takes two additional arguments: 6, the delayed sampling graph, and F, the weight for the particle lter, and returns a symbolic value, an updated graph, and an updated weight. Operator application op(E) introduces a symbolic expression app(op, E). if uses the value operation to sample a concrete value for the condition. sample(E) introduces a new random variable in the graph with distribution E. observe(E 1 ,E 2 ) introduces a fresh random variablewith distribution E 1 , and conditions the graph on the fact thattakes the value E 2 .

Inference. Given a transition function 5 , a distribution over states f from the previous iteration, and inputs E 8 , the infer operator computes a distribution of outputs and new distribution over states for the next iteration. First, the inference draws # states from f. Each of theses states B = is associated with a delayed sampling graph 6 = . Second, the transition function 5 returns a symbolic output value E = , a new state B 0 = , the updated graph 6 0 = , and the importance weight F = . Third, the distribution(> = , 6 0 = ) function returns a distribution of values without altering the graph, and the new distribution over states is a Dirac delta distribution on the pair (B 0 = , 6 0 = ). Finally, results are accumulated in a mixture distribution using the weights F = and this distribution is split into a distribution of values and a distribution of next states.1

»infer(<)… W = let stream { init = 4 init ; step(? state ,? input ) = 4 } W 0 = »<… W in let B init = »4 init … W 0 in (X (B init ,;) , infer (_(? state , ? input ). {[4]} W 0 ))
where infer (5

) = _(f, E 8 ). let `= _* . # Õ ==1 let B = , 6 = = draw(f) in let (> = , B 0 = ), 6 0 = , F = = 5 (B = ,E 8 )(6 = , 1) in let 3 = = distribution(> = , 6 0 = ) in F = ⇤ 3 = (c 1 (* )) ⇤ X B 0 = ,6 0 = (c 2 (* )) in (c 1⇤ (`), c 2⇤ (`))

Graph Manipulation

We now describe the graph manipulation functions that are required to dene the high-level operations value, assume, and observe used in the semantics of Figure 9. [START_REF] Lundén | Delayed sampling in the probabilistic programming language Anglican[END_REF] and Murray et al. [2018] provide detailed explanations of these operations.

Notation. In this section and those that follow, frv(E) denotes the free random variables of a program value E, i.e., the set of variables used in the symbolic expression E.

Graph Data Structure. A delayed sampling graph 6 is dened by a tuple (+ , ⇢, @) where + is a set of vertices -the random variables, ⇢ is a set of directed edges -the dependencies between random variables, and @ is a relation mapping each node to a state: Initialized, Marginalized, or Realized.

A node Initialized (? -|. ) represents a random variablewith a conditional distribution ? -|. where . is the unique parent of -. A node Marginalized (? -) represents a random variablewith a marginal distribution ? -. A Marginalized node has at most one parent. If there is a parent node, the distribution ? -incorporates its distribution. A node Realized (E) represents a random variableassociated to a concrete value E. By construction, a delayed sampling graph is a forest -a set of trees (each node has at most one parent).

value. The operation value(E, 6) converts the symbolic expression E into a concrete value by sampling all the random variables in E. All these random variables become Realized nodes in the graph, and the distributions depending on these variables are updated.

value(E, 6) = (E, 6) if E is a concrete value value(app(op, E), 6) = let E 0 , 6 0 = value(E, 6) in (op(E 0 ), 6 0 ) value(-, 6) = let + , ⇢, @ = 6 in if @(-) = Realized (E) then (E, 6) else let + 0 , ⇢ 0 , @ 0 [- Marginalized (`)] = gra (-, 6) in let E = draw(`) in (E, (+ 0 , ⇢ 0 , @ 0 [- Realized (E)]))
If E is already a concrete value, there is nothing to do. If E is the application of an operator, value recursively samples a concrete value for the argument and applies the operator to this value. If E is a random variablethat is already realized, value returns the corresponding value. Otherwise, value (1) calls the gra function dened in Appendix C to marginalizeand all its ancestors, (2) draws a sample from the marginalized distribution, and (3) returns this value and turnsinto a Realized node. Note that gra might have to realize some nodes since it marginalizes all its ancestors and a marginal node has a single marginalized child. During marginalization, gra also removes edges between Marginalized nodes and their Realized child if any.

assume. The operation assume(E, 6) adds a new random variablewith distribution E in graph 6.

assume(E, 6) = let (+ , ⇢, @) = 6 in let -= fresh(+ ) in if frv(E) = ; then (-, (+ [ {-}, ⇢, @[- Marginalized (E)])) else if frv(E) = {. } ^conj(E, ., 6) then (-, (+ [ {-}, ⇢ [ {(-, . )}, @[- Initialized (E)])) else let E 0 , (+ , 0 ⇢ 0 , @ 0 ) = value(E, (+ [ {-}, ⇢, @)) in (-, (+ 0 , ⇢ 0 , @ 0 [- Marginalized (E 0 )]))
The distribution E is a symbolic expression which can be a marginal distribution that does not depends on other random variables -e.g., app(bernoulli, 0.5)-or a conditional distribution -e.g., app(bernoulli, . ) where . is a random variable. If E is a marginal distribution, assume just adds a new marginalized node in the graph. If E is a conditional distribution, assume tries to keep track of the dependency betweenand a random variable used in E (the delayed sampling graph is a forest where each node has at most one parent).

The value E thus represents a distribution ? -|. wheredepends on a unique random variable . . If the distribution ? -|. and ? . are conjugate (conj(E, ., 6)) -e.g., app(bernoulli, . ) with . ⇠ beta(U, V) -marginalization and conditioning are tractable operations, and assume adds an edge between . and a new initialized nodeto the graph. Otherwise, symbolic computation is not possible; assume calls value to sample a concrete value, thus breaking the dependency, and adds a new independent Marginalized node to the graph.

observe. The operation observe(-, E, 6) assigns the concrete value E toand updates the distributions depending onaccordingly.

observe(-, E, 6) = let (+ , ⇢, @) = gra (-, 6) in (+ , ⇢, @[- Realized (E)])
Similarly to value, the observe operation uses the function gra to marginalize the variableand then turnsto a Realized node associated with the value E.

Memory Usage

Baudart et al. [2020] proposed an implementation of delayed sampling where an Initialized node only has a pointer to its parent, a Marginalized node only has a pointer to its unique Marginalized or Realized child, if any, and a Realized node has no pointers to its parent or any of its children.

Garbage Collection. A node in the delayed sampling graph can be safely removed if none of the program variables depend on its value. We assume the existence of a garbage collection routine that deallocates the nodes of the graph that are not reachable as soon as possible.

Denition 4.1 (Reachability). Given a set of root variables A and a delayed sampling graph 6 = (+ , ⇢, @), the set of reachable variables -written reachable(6, A ) -is dened as follows:

' = {(-, . ) | (-, . ) 2 ⇢ ^@(-) = Initialized _ (., -) 2 ⇢ ^@(-) = Marginalized ^(@(. ) = Marginalized _ @(. ) = Realized) reachable(6, A ) = {. | (' ⇤ (-, . )) ^-2 A ^. 2 + }
where ' ⇤ denotes the reexive transitive closure of the relation '.

If we consider the graph in Figure 2b, reachable(6, {x}) = {x}. In the example of Figure 4b, we have reachable(6, {i, x}) = {i, pre_x, x}, where pre_x is the gray node in between the nodes for i and x. Reachability is the core property used in Denition 5.1 to dene what it means for a program to run in bounded memory.

Graph Expansion. The only operation that increases the size of the graph is assume which introduces new nodes. The operations value and observe can only marginalize and realize nodes. If 6 0 is the graph resulting from the application of value or observe on a graph 6, 6 and 6 0 have the same structure but Initialized nodes can be Marginalized or Realized, and Marginalized nodes can be Realized. The reachability relation of the graph implies that value and observe reduce the number of dependencies in the delayed sampling graph, that is, reachable(6 0 , A) ✓ reachable(6, A ).

Initialized and Marginalized Chains. Two patterns can yield unbounded memory consumption. First, it is possible to keep adding nodes without realizing them (via observation or sampling), thus forming initialized chains. An initialized chain is a sequence of initialized nodes, each of which holds a pointer to its parent and thereby expands the number of random variables that are reachable. Second, it is possible that nodes are only indirectly used to realize one of their children. These marginalized nodes can form marginalized chains. A marginalized chain is a sequence of marginalized nodes, each of which holds a pointer to its child and thus expands the number of random variables that are reachable. The last node of a marginalized chain may be realized.

SEMANTIC PROPERTIES

In this section, we dene conditions under which delayed sampling executes in bounded memory. We dene these conditions as properties of executions. An execution is a sequence of pairs of a state and a delayed sampling graph (B = , 6 = ) = 2N , where each state is a semi-symbolic value as dened in Section 4.1. An execution denes the sequence of states and graphs a model -i.e., an argument of an infer -goes through.

The inference step function infer (5 ) in »infer(<)… may operate over multiple executions of 5 (see Section 4.1). However, infer (5 ) executes in bounded memory if every execution of 5 is bounded-memory. This is because infer (5 ) always updates its state by mapping 5 over states and graphs from the distribution at the previous iteration. Thus, any state and graph in the distribution at the next iteration must have come from some execution of 5 , and if all executions of 5 are bounded-memory, all states and graphs in the distribution must have bounded memory. We have formalized this in more details in Appendix E.1.

Based on this notion of execution, we introduce two notions of bounded-memory executions of delayed sampling, and semantic properties which are necessary and sucient for boundedmemory execution. In Section 5.1 we present a low-level denition of bounded memory that directly corresponds to how the delayed sampling runtime executes. In Section 5.2 we present an alternative high-level denition in terms of dataow properties of the high-level delayed sampling operators: the <-consumed and unseparated paths properties. In Section 5.3 we show that the high-level and low-level formulations are equivalent. In particular, Section 5.3 shows a correspondence between the <-consumed property and a bound on the length of initialized chains, as well as a correspondence between the unseparated paths property and a bound on the length of marginalized chains.

Low-Level Bounded Memory

A program executes in bounded memory if the delayed sampling graph maintains a bounded number of reachable variables over time. We formalize this as follows:

Denition 5.1 (Low-level Bounded-Memory). An execution

(B = , 6 = ) = 2N of a model is low-level bounded-memory if 9:. 8= 0 |reachable(6 = , B = )|  : ⇤ |frv(B = )|
This denition states that at each iteration, the size of the set of reachable nodes in the delayed sampling graph may be at most a constant multiple of the number of free random variables in the state. We do not consider the runtime to violate bounded memory in the trivial case that the program state is intrinsically unbounded, i.e., when |frv(B = )| = 2N is unbounded. Such a program would not execute in bounded memory under any inference algorithm; even a particle lter would require unbounded memory to store the program state.

High-Level Definitions

In this section, we present an alternative high-level denition of bounded memory that is easier to reason about. The high-level denition is in terms of dataow properties of delayed sampling operations. We have formalized these dataow properties by augmenting the delayed sampling operations with tracing. A trace is dened as follows: assume(E, (6, g))

g ::= g :: g 1 | nil g 1 ::= -f -| -f nil | eval(X)
= let -0 , 6 0 = assume(E, 6) in 8 > > > < > > > :

-0 , (6 0 , g :: -0 f nil) frv(E) = ; -0 , (6 0 , g :: -0 f -) { -} = frv(E) ^conj(E, -, 6) -0 , (6 0 , g :: eval(frv(E)) :: -0 f nil) otherwise value(E, (6, g))

= let (E 0 , 6 0 ) = value(E, 6) in E 0 , (6 0 , g :: eval(frv(E))) observe(-, E, (6, g)) = observe(-, E, 6), (g :: obs(-)) A trace is a list of primitive operations, where each primitive is one of:

• Assumption, written -f -0 whenis assumed from another random variable -0 or f nil when it is assumed without a parent. • Evaluation using the eval keyword, which refers to evaluating a set of random variables X.

• Observation using the obs keyword, which refers to observing a random variable -.

We dene an augmented semantics that operates on a pair of a delayed sampling graph and a trace. Figure 10 denes augmented versions of the assume, value, and observe operations, and the full semantics (written »•… and {[•]}) is dened by replacing these operators in Figure 9 with their traced counterparts from Figure 10.

The <-consumed Property. The <-consumed property is used to enforce that every variable introduced with assume is eventually consumed either by directly being passed to a value or observe or transitively by being passed to a assume that introduces a variable that is also <-consumed. Denition 5.2 (<-consumed). A variableis <-consumed in a trace g under the following circumstances:

•is 0-consumed if it is observed or evaluated (i.e., g has eval(-) where -2 X or obs(-)).

•is <-consumed if it is passed to the assume statement that introduces another variable -0 (i.e., -0 fis in g), and -0 is (< 1)-consumed.

The Unseparated Paths Property. The unseparated paths property states the existence of a sequence of variables, each assumed from the previous, with no variable in the sequence observed or evaluated.

Denition 5.3 (Unseparated Paths). An unseparated path in g is a sequence of variables -0 , -1 , . . . , -= such that each -8+1 was assumed from -8 (i.e., -8+1 f -8 is in g) and no -8 is directly observed or evaluated (i.e., g does not contain any eval or obs operations that reference -8 ).

High-level Bounded Memory. We now present the high-level bounded memory property. This property states that all variables must eventually be <-consumed or unused, and there must be a uniform bound across iterations on the length of an unseparated path starting from a program state variable.

Denition 5.4 (High-level Bounded-Memory

). A program execution (B = , (6 = , g = )) = 2N is high-level bounded-

memory if and only if

• There exists an < such that for every iteration = and every variable introduced before = (i.e., such that -f -0 or -f nil is in g = ), either a) there exists a = 0 = such that for all = 00 = 0 ,is <-consumed in g = 00 , or b)is unused -meaning that for all = 0 =,isn't an element of any unseparated path longer than < in g = 0 . • There exists a 2 such that for all =, no random variable referenced in B = starts an unseparated path in g = of length more than 2.

Equivalence of Low-Level and High-Level Definitions

In this section, we show the equivalence of the low-level and high-level denitions. We do so by showing that both properties are equivalent to the delayed sampling graph having a uniform bound (i.e., a bound that holds across all iterations) on the length of initialized and marginalized chains as dened in Section 4.3.

5.

3.1 Low-Level Bounded Memory vs. Infinite Chains.

L 5.5. If the delayed sampling graph is constructed using assume, observe, and value operations, then each random variable starts either an initialized chain, a marginalized chain, or an initialized chain followed by a marginalized chain.

P. The assume, observe, and value operations can only make the following modications to a delayed sampling graph 6. (1) Add a independent Marginalized node which creates a marginalized chain of length zero. (2) Attach a new Initialized nodeto a node . with a conjugate distribution. It means that . is either Initialized or Marginalized and thus it creates either a longer initialized chain or an initialized chain followed by a marginalized chain. (3) Perform a gra which ensures that every ancestor of a node is marginalized and has a single marginalized child. Every non-ancestor variable is either as it was before or becomes realized, so this operation preserves the structure of the previous graph and cannot increase the length of the chains. (4) convert a Marginalized node into a Realized node which can only break a chain. ⇤ T 5.6. A program is low-level bounded-memory i there is a uniform bound < on the length of an initialized chain and a uniform bound 2 on the length of a marginalized chain. P. Assuming a uniform bound, when the number of variables is bounded by # , according to Lemma 5.5, the number of reachable nodes in the graph is bounded by # ⇥ (2 + <).

Conversely, if no uniform bound exists (i.e., for every potential bounds 2 and <, there exists a iteration = such that chains may exceed the bound at =), the execution cannot be low-level bounded-memory, because even if the number of root variables is bounded by # , the reachable variables may exceed # ⇥ (2 + <). ⇤ 5.3.2 High-Level Bounded Memory vs. Infinite Chains.

T 5.7 (H S). In a program execution that is high-level bounded-memory, no innite chains can exist in any of the delayed sampling graphs. P. All initialized chains must be shorter than <, where < is from the <-consumed property of high-level bounded-memory. This is because when a variable's descendant is subject to observe or value, the variable becomes marginalized. Such a descendant can be at most < variables away because of the denition of <-consumed.

All marginalized chains must be shorter than 2 +<, where 2 is from the unseparated path property of high-level bounded-memory and < is from the <-consumed property. By Lemma 5.5, every marginalized chain must start at either a root or an initialized chain. If it starts at a root, the unseparated path property ensures that the path between the root and the end of the chain can contain at most 2 variables. This is because any observed or valued variables become realized and become the end of the chain. If it starts at an initialized chain, by the above reasoning that chain has length at most <, and there was a previous iteration at which the marginalized chain started at a root and had length at most 2, giving an overall length of at most 2 + <. ⇤ L 5.8. If there exists a used variable that is not <-consumed, then the program produces a graph at some iteration with an initialized chain of length <.

P. If a used variable is not <-consumed, then by the denition of <-consumed at some iteration it must start an assume chain of length <. All of the nodes in this chain must be initialized, and therefore form an initialized chain of length <. ⇤ L 5.9. If every variable is <-consumed, and there exists a variable that starts an unseparated path of length 2 where 2 > <, then there exists an iteration with a marginalized chain that has length at least 2 <. P. Note that the rst 2 < variables in the unseparated path must be either marginalized or realized. Otherwise, there would be more than < initialized variables in the tail of the unseparated path that are initialized, which would violate soundness of <-consumed. Letbe the variable that starts the unseparated path and -0 be the last marginalized or realized variable in the unseparated path, and consider the iteration = 0 when -0 was rst marginalized. It must be true that (1)is in the program state at iteration = 0 because it is in the state at the current iteration = > = 0 , and (2) a marginalized chain runs fromto -0 . Thus, at = 0 , the marginalized chain had length 2 <. ⇤ T 5.10 (H C). If a program execution is not high-level boundedmemory, the delayed sampling graph has either unbounded initialized chains or marginalized chains.

P. If the execution is not high-level bounded-memory, it either fails the <-consumed property or the unseparated path property. If it fails the <-consumed property, apply Lemma 5.8. Otherwise, apply Lemma 5.9. ⇤ T 5.11. A program execution is high-level bounded-memory if and only if it is low-level bounded-memory. P. Apply Theorems 5.6, 5.7, and 5.10. ⇤

ANALYSIS

In this section, we develop an analysis to check that a ` program executes in bounded memory. We approach this problem by developing two independent analyses within a shared analysis framework.

One analysis checks the <-consumed property of a program and the other checks the unseparated paths property, which together ensure that the program executes in bounded memory (Section 5).

Our shared analysis framework abstracts the execution of a program as the execution of abstract operations on an abstract graph. An abstract graph abstracts the dynamic state of a program's delayed sampling graph. We implement the analysis framework by means of a type system, such that well-typed programs satisfy the <-consumed and unseparated paths properties, given each analysis's respective instantiation of the abstract graph. The typing judgment , G `U 4 : C, G 0 asserts that in a context , and for an abstract graph G, that an expression 4 accesses the random variables denoted by the type C and yields a new abstract graph G 0 . The parameter U is either mc to denote the <-consumed analysis or up to denote the unseparated paths. We write `U 4 : C as shorthand for , G `U 4 : C, G when 4 has no eect on the graph.

Types and Contexts

A type C captures the random variables the expression could refer to as well as its shape, as primitive data, a product, a function, or a stream instance.

C F A | () | C 1 ⇥ C 2 | C 1 ! C 2 | stream(C, B) | bounded B F stepfn(? state , ? in , 4 , 4)
The type of a primitive expression is a reference set, denoted A , which species the random variables to which the expression refers. We distinguish two types of stream instances, before and after bounded-memory checking. The rst is stream(C, B), where C is the type of the current state and B is a step function representation to be described later. The second is bounded, representing instances that have passed bounded memory analysis and hide their inner structure.

Reference Sets. A reference set of a ` expression, denoted A , species the random variables that are aected when the expression is observed or evaluated. In the presence of branches, we dene A to be a pair of sets (lb, ub), where the lower bound lb contains all random variables which must be aected and the upper bound ub all random variables which may be aected. For example, a constant value in ` such as 1.5 has the reference set (;, ;) because it references no random variables. If the program variables x and y correspond to random variablesand . respectively, then the expression gaussian(x,y), specifying a distribution with two parameters, has reference set ({-, . }, {-, . }), meaning that observing it will observe the random variablesand . .

Contexts.

The context , G : C maps variable G to type C. As ` syntactic patterns ? may be variables or pairs, we use the shorthand , ? : C to dene types for variables in ? by structural correspondence with C, as dened by the rst rule below. We also dene a judgment `? ? : C that synthesizes a deterministic type C from a pattern ?.

, ? 1 : C 1 , ? 2 : C 2 `U 4 : C , (? 1 , ? 2 ) : C 1 ⇥ C 2 `U 4 : C `? G : (;, ;) `? ? 1 : C 1 `? ? 2 : C 2 `? (? 1 ,? 2 ) : C 1 ⇥ C 2

Abstract Graphs

An abstract graph G is an abstraction of the delayed sampling graph that tracks which random variables have been consumed and active paths between random variables, properties relevant to the semantic properties. For each analysis U there exists an abstract graph type, G, and a set of operations that form its interface (Figure 11). Specically, in the <-consumed analysis we dene G to be a pair of sets in and con which respectively represent an over-approximation of variables introduced into the graph and an underapproximation of the variables consumed by observation or sampling (Figure 12). In the unseparated paths analysis, we dene G to be a set sep of separators containing consumed random variables and a partial path function ? mapping a pair of random variables to an upper bound on the length of an unseparated path between them (Figure 13).

Operations on the abstract graph manipulate random variables, graphs, and reference sets. The function assume returns a new graph with a random variablefrom a distribution with reference set A added to G, observe returns a graph whereis observed with a value with reference set A , and value returns a graph where an expression with reference set A is evaluated. The join operator t U represents a conservative choice between two graphs. <-consumed Graph Operations. In Figure 12, assume mc (-, A, G) marks the random variableas introduced. In all cases, the lower bound of random variables in the input is marked consumed. To join two states, we union the introduced variables and intersect the consumed variables.

Unseparated Paths Graph Operations. In Figure 13, observe up and value up mark input variables as separators. In assume up , we set the length of the path from the new variableto itself to zero. For a parent -? that is not a separator, we set the length of the path from any variable -8 toto one more than the length from -8 to -? . To join two states, we intersect the separators and take the maximum length between the results of the two path functions (where dened, or 0 otherwise). G F {? : RV ⇥ RV õ! N; sep ✓ RV} assume up (-, A, G) = {? 0 ; G.sep} where ? 0 (-, -) 7 ! 0, ? 0 (-8 , -) 7 ! G.? (-8 , -? ) + 1 for all -? 2 A .ub \ G.sep, -8 2 RV, ? 0 (-, . ) 7 ! G.? (-, . ) otherwise

assume U : RV ! A ! G ! G observe U : RV ! A ! G ! G value U : A ! G ! G t U : G ! G ! G Fig. 11. Abstract graph interface. G F {8= ✓ RV; con ✓ RV} assume mc (-, A, G) = {G.8= [ {-}; G.con [ A .lb} observe mc (-, A, G) = {G.8=; G.con [ A .lb [ {-}} value mc (A, G) = {G.8=; G.con [ A .lb} G 1 t mc G 2 = {G 1 .8= [ G 2 .8=; G 1 .con \ G 2 .con}
observe up (-, A, G) = {G.?; G.sep [ A .lb [ {-}} value up (A, G) = {G.?; G.sep [ A .lb} G 1 t up G 2 = {? 0 ; G 1 .sep \ G 2 .sep} where ? 0 (E 1 , E 2 ) 7 ! max(G 1 .? (E 1 , E 2 ), G 2 .? (E 1 , E 2 ))
Fig. 13. Unseparated paths abstract graph operations.

Typing Rules

In Figure 14 we present the typing rules that are relevant to analyzing probabilistic streams, with the full denition in Appendix D. Constants reference no random variables. sample introduces a fresh random variable sampled from its argument and adds it to the graph. observe introduces an intermediate random variable for its rst argument by the same mechanism as sample, and observes it to be the evaluation of its second argument.

Operators and Scalar Folding. We use ` operators >? to describe probability distributions and other operations over scalars and assume them to have scalar return values. The auxiliary judgment & folds products and stream instances into scalars by taking unions of variable sets.

() & ( ;, ;) A & A C 1 & (lb, ub) C 2 & (lb 0 , ub 0 ) C 1 ⇥ C 2 & (lb [ lb 0 , ub [ ub 0 ) C & (lb, ub) stream(C, B) & (lb, ub) bounded & (;, ;)
Sequencing. Sequencing using the let-expression follows the standard typing rule for let, and also threads the output graph of evaluating 4 into the evaluation of 4 0 . Conditionals and Join. if-expressions evaluate the condition, check both branches in parallel, and join the resulting reference set and graphs. The join operator t (Figure 15), representing the conservative union of two types, unions the upper bounds and intersects the lower bounds. We disallow ifbranching over functions and stream instances. Streams and Inference. To facilitate typing of stream functions, we dene the following auxiliary judgment, which computes, for a stream function, the type of its initial state and the syntactic fragment for its step function.

() t () = () (C 1 ⇥ C 2 ) t (C 0 1 ⇥ C 0 2 ) = (C 1 t C 0 1 ) ⇥ (C 2 t C 0 2 ) (lb, ub) t (lb 0 , ub 0 ) = (lb \ lb 0 , ub [ ub 0 )
`U 2 : (;, ;) `U E : A -= fresh(G) , G `U sample(E) : ({-}, {-}), assume U (-, A, G) , G `U sample(E 1 ) : ({-}, {-}), G 0 `U E 2 : A 2 , G `U observe(E 1 ,E 2 ) : (), observe U (-, A 2 , value U (A 2 , G 0 )) `U E : C C & A `U op(E) : A , G `U 4 : C, G 0 , ? : C, G 0 `U 4 0 : C 0 , G 00 , G `U let ? = 4 in 4 0 : C 0 , G 00 `U E : A G 0 = value U (A, G) , G 0 `U 4 1 : C 1 , G 1 , G 0 `U 4 2 : C 2 , G 2 , G `U if E then 4 1 else 4 2 : C 1 t C 2 , G 1 t U G 2 `U < : (C, B) `U init(<) : stream(C, B) `U G : stream(C, stepfn(? state , ? in , 4 , 4)) `U E : C in 4 , ? state : C, ? in : C in , G `U 4 : C 0 ⇥ C out , G 0 , G `U unfold(G,E) : C out ⇥ stream(C 0 , stepfn(? state , ? in , 4 , 4)), G 0 `mc < bounded `up < bounded `U infer(<) : bounded `U G : bounded `U E : C C & (;, ;) `U unfold(G,E) : (;, ;) ⇥ bounded
`U 4 0 : C init C init & (;, ;) `U stream { init = 4 0 ; step(? state ,? in ) = 4 } : (C init , stepfn(? state , ? in , , 4))
Correspondingly, we dene the context , < : (C init , stepfn(? state , ? in , 4 , 4)) to map the stream function name < to its initial state type and step function.

Instances that are created by init expose the type of their internal state and their step function. The unfold rule applies the step function to the current state, yielding an output and an instance with the new state. It ensures that the argument E is compatible with the type of the step function.

An infer expression marks the entry point of a new sub-analysis for its new delayed sampling graph. The premises of the typing rule for infer are the success conditions for both analyses that must hold regardless of U. This judgment, `U < bounded, states that the stream function < can be unfolded for an arbitrary number of iterations while satisfying property U starting with an empty delayed sampling graph.

Instances created by infer possess a newly instantiated delayed sampling graph. Their internal state contains the delayed sampling graph and bookkeeping information for the inference algorithm. Thus, the state is hidden to the exterior and the instance is assigned the opaque type bounded. unfold on a bounded type only requires that the input and output are purely deterministic. m-consumed Success Condition. We conclude a stream function passes the <-consumed analysis when all variables that are introduced are consumed by the program. Because an introduced variable may take several stream iterations to be consumed, we repeatedly execute the analysis until we consume all variables and succeed or reach a xed point and fail. Dene the iteration judgment `U (=) < : C 0 , G, where U is either <2 or D?, as follows:

`U < : (C, stepfn(? state , ? in , 4 , 4)) `?

? in : C in 4 , ? in : C in , ? state : C, ? U `U 4 : C out ⇥ C 0 , G `U (0) < : C 0 , G `U < : (C, stepfn(? state , ? in , 4 , 4)) `U (= 1) < : C 0 , G `? ? in : C in 4 , ? in : C in , ? state : C 0 , G `U 4 : C out ⇥ C 00 , G 0 `U (=) < : C 00 , G 0
On each iteration, this judgment applies the appropriate type rule for the step function and returns the result, using the abstract graph from the previous iteration as the context for the step function rule. The initial iteration uses an empty abstract graph as the context, represented by ? U . For the <-consumed analysis, we specialize the judgment to `<2 (=) < : C 0 , G, and dene ? mc to be (;, ;).

The rule continues iterating until it reaches the success condition. The success condition states that every variable introduced that is kept in the program state must be used with in a bounded number of time steps. We formalize this as the following type rule:

`<2 (0) < : C, G C & (;1, D1) `<2 (=) < : C 00 , G 0 (G.8= \ G 0 .con) \ ub = ; `mc < bounded
Alternatively, if evaluating one more iteration does not consume any more variables, we reach a xed point and return failure. Since every iteration we either consume a variable or reach a xed point, the analysis is guaranteed to terminate.

Unseparated Paths Success Condition. Like the <-consumed analysis, the unseparated paths analysis is iterative, and we may need to repeat it for some number of iterations. We specialize the iteration judgment dened in the previous section to `D? (=) < : C, G and dene ? up to be a pair of an empty map and an empty set. Dene path(C, G) where C & (lb, ub) to be the length of the longest path from any random variable in ub to any other variable in G.?. Then we conclude the program passes the unseparated path analysis when the length of the longest path converges after some nite number of iterations:

`D? (=) < : C, G `D? (=+(path(C,G)⇤size(C ))+1) < : C 00 , G 0 path(C, G) = path(C 00 , G 0 ) `up < bounded
The implementation of this rule repeatedly computes a new abstract graph starting from the previous iteration's output. It exits when the longest path length at the current iteration is equal to the longest path after (path(C, G) ⇤ size(C)) + 1 additional iterations. The function size determines, for a given type C, how many values of base type are contained in C.

size(A ) = 1 size(C 1 ⇥ C 2 ) = size(C 1 ) + size(C 2 )
The extra iterations ensure that the path length has stabilized and the analysis can safely conclude that there is a bound on the length of the longest unseparated path.

If the path length check fails, the implementation keeps iterating until a pre-specied bound is reached. Upon reaching this bound, the implementation outputs an analysis failure. Note that the analysis may be imprecise and reject correct programs if the bound is not suciently high.

Soundness. The following theorems establish the soundness of the type system. The rst theorem states that the type system soundly ascribes types to values and soundly updates the abstract delayed sampling graph:

T 6.1 (< U P S). If W, (6, g) ✏ U , G and , G `U 4 : C, G 0 and {[4]} W (6, g), F = E, (6 0 , g 0 ), F 0 , then E, (6 0 , g 0 ) ✏ U C, G 0 .
Next, the type system soundly ensures a stream function maintains bounded memory. T 6.2 (A S). If W ✏ U and `U < : bounded, then »<… W ✏ U bounded.

We prove these theorems in Appendix E.2.

Implementation

We implemented our analysis framework and the <-consumed and unseparated paths analyses in OCaml. Our implementation takes as input a ` program and outputs either true or false for each analysis. It also accepts a parameter for the iteration bound for the unseparated paths analysis. The implementation goes beyond the type system laid out in the paper by supporting functions that have probabilistic eects as well as interfaces for list and array operations. ` programs can further be compiled to OCaml and executed using the ProbZelus delayed sampling runtime. The code is available at https://github.com/psg-mit/probzelus-oopsla21.

EVALUATION

To evaluate the ability of the analysis to accept only ` programs that can execute in bounded memory, we executed it on several benchmarks reective of real-world inference tasks.

Research Questions. We used our implementation to answer two research questions. For realistic probabilistic programs, (1) does the type system precisely verify the properties required for boundedmemory execution, and (2) is a small iteration bound sucient for the unseparated paths analysis?

Methodology

We executed the analysis on example programs from [START_REF] Baudart | Reactive Probabilistic Programming[END_REF] originally written in ProbZelus, a probabilistic programming language featuring probabilistic data streams and delayed sampling. We manually translated them to ` , and they reect a range of realistic control problems with dierent memory usage characteristics. For the unseparated paths analysis, we set an iteration count bound of 10, which was sucient for these programs. We compared the outputs of the analysis to our manual logical reasoning about the ability of each of the following programs to execute in bounded memory. We provide source code for all benchmarks in Appendix F.

Kalman is the simplied core model of Figure 1 and models an agent that estimates position from noisy observations. Applying delayed sampling on this model is equivalent to a Kalman lter [START_REF] Kalman | A New Approach to Linear Filtering and Prediction Problems[END_REF] where each particle returns the exact solution.

Kalman Hold-First is the example from Figure 3 with a reference to the output of the rst iteration.

Gaussian Random Walk is a simplication of Kalman that does not observe of the true position, eectively expressing a Gaussian random walk. Robot is the full example from Figure 1 that includes the Kalman core model as well as a main stream function that invokes a controller based on the inferred position.

Coin models an agent that estimates the bias of a coin. The model chooses the probability of the coin from a uniform distribution, and thereafter chooses the observations by ipping a coin with that probability. Applying delayed sampling to this model is equivalent to exact inference in a Beta-Bernoulli conjugate model [START_REF] Fink | A Compendium of Conjugate Priors[END_REF]] where each particle returns the exact solution.

Gaussian-Gaussian estimates the mean and variance of a Gaussian distribution.

Table 1. Bounded memory analysis on benchmark programs.

<-consumed unsep. paths bounded mem.

output actual output actual output actual Kalman X X X X X X Kalman Hold-First X X 7 7 7 7 Gaussian Random Walk 7 7 X X 7 7 Robot X X X X X X Coin X X X X X X Gaussian-Gaussian X X X X X X Outlier 7 7 X X 7 7 MTT 7 7 X X 7 7 SLAM 7 X X X 7 X
Outlier, adapted from Section 2 of [Minka 2001], models the same situation as the Kalman benchmark, but with a sensor that can occasionally produce invalid readings. The model chooses the probability of an invalid reading from a beta(100,1000) distribution, so that invalid readings occur approximately 10% of the time. At each time step, with the previously chosen probability, the model chooses the observation from either the invalid distribution gaussian(0,100) or the Kalman model. Applying delayed sampling to this model is equivalent to a Rao-Blackwellized particle lter [Doucet et al. 2000b] combining exact inference with approximate particle ltering.

MTT (Multi-Target Tracker) is adapted from [Murray and Schön 2018] and involves a variable number of targets with linear-Gaussian 2D position/velocity motion models that produce measurements of position at each time step. The model randomly introduces targets as a Poisson process and deletes them with xed probability at each step.

SLAM (Simultaneous Localization and Mapping) is adapted from [Doucet et al. 2000a] and models an agent that estimates its position on a one-dimensional grid and also a map of its environment associating each cell with black or white. The robot uses inference to decide its next move, but its motion commands are noisy with some probability that its wheels may slip, and its observations may also be incorrectly reported.

Analysis Results

Table 1 displays the analysis outputs for each of the benchmark programs. For each analysis, the "output" column is the result of the implementation, and the "actual" column is the ground truth, i.e., whether the program satises the semantic property according to manual analysis. The "bounded memory" columns are the logical conjunction of the two semantic properties.

For the rst six benchmarks, the analysis implementation yielded the same answer as manual analysis for whether the program satises both semantic properties and thus permits execution in bounded memory. In every case, the output of the implementation is sound with respect to the ground truth. Furthermore, all unseparated-path analyses converged within 10 iterations.

Kalman. For this program, every variable is <-consumed for <  1 and starts an unseparated path of length at most 1, and thus it can execute in bounded memory.

Kalman Hold-First. For this program, every variable is <-consumed for <  1. However, the analysis detects that unseparated paths starting from the initial value for x grow without bound and fail to converge after 10 iterations, so this program cannot execute in bounded memory.

Gaussian Random Walk. Here, every unseparated path has length at most 1. However, the analysis detects that there is no < such that any variable is <-consumed because no variable is ever observed or evaluated, so this program cannot execute in bounded memory.

Robot. Every variable is 1-consumed and every separated path has length at most 1. The analysis succeeds and indicates this program can execute in bounded memory.

Coin. Every variable is 1-consumed and every unseparated path has length at most 1. The analysis succeeds and indicates this program can execute in bounded memory.

Gaussian-Gaussian. Every variable is 1-consumed and every separated path has length at most 1. The analysis succeeds and indicates this program can execute in bounded memory.

Outlier. Every unseparated path has length at most 1. However, in the event that samples are indenitely considered outliers, no observation will occur that causes the variable xt to be consumed, so this program cannot execute in bounded memory.

MTT. Every unseparated path has length at most 1. However, not all random variables are guaranteed to be consumed, as the nal observe operation is only executed based on a dynamic condition on the lengths of two list data structures. Because this condition is not guaranteed to be met, this program cannot execute in bounded memory.

SLAM. Every unseparated path has length at most 1. The analysis concludes that the environment map array is not consumed because the model makes random choices that are not guaranteed to cover all the entries of the map. However, manual examination shows that an entry of the map that is never covered by a random choice is 0-consumed by virtue of being never used. Thus, the analysis soundly but imprecisely determines that the <-consumed condition fails.

Discussion

For the Outlier and MTT benchmarks, even though both fail the <-consumed semantic property and therefore are not guaranteed to execute in bounded memory, they will almost certainly execute in bounded memory. For example, in Outlier, the only way that the memory consumption of the model will increase indenitely is if a particular random choice always takes one branch, which is a probability-zero event. In general, our semantic properties and analysis implementation reason about the absence of any program execution that yields unbounded memory. However, in practice, almost certain bounded-memory execution may also be a useful property of programs.

In general, the analysis can provide a sound guarantee that a program executes with bounded memory. However, as we saw with SLAM, it is not always precise enough such that if it rejects a program, then the program must have unbounded memory consumption. For example, it is possible to deliberately construct pathological programs requiring a large number of iterations for the unseparated paths analysis. Remaining limitations on precision include common static analysis challenges such as path sensitivity due to if statements and aliasing due to complex data structures.

When facing conditional branches, the analysis takes a conservative approach that may not utilize all statically available knowledge. Specically, it cannot determine that certain branches are taken at most once over the entire input stream or that only certain program paths are valid over multiple sequential branches. The analysis also cannot accurately track variables that are stored into complex data structures, meaning it cannot mark them as consumed. We discuss these challenges in greater detail and provide specic examples in Appendix G.

RELATED WORK

Resource Analysis for Probabilistic Programs. Static resource analysis is capable of automatically determining upper bounds for resources such as time or memory required to execute a probabilistic program. [START_REF] Van Chan Ngo | Bounded Expectations: Resource Analysis for Probabilistic Programs[END_REF] proposed a weakest-precondition approach to determine the expected memory usage of a probabilistic program, which bounds the number of loop iterations executed and number of explicit memory allocation ticks encountered. Our analysis, on the other hand, extends static reasoning to the inherent memory usage of the inference algorithm itself.

Reactive Probabilistic Programming. [START_REF] Gupta | Probabilistic Concurrent Constraint Programming[END_REF] rst introduced the idea of reactive probabilistic programming. They extend a concurrent constraint language with random variables. In contrast, our language is based on a synchronous dataow model and focus on resource analysis. [START_REF] Baudart | Reactive Probabilistic Programming[END_REF] developed ProbZelus, a reactive probabilistic programming language which operates over streams of data and supports inference at each stream iteration. It uses an implementation of delayed sampling designed to provide bounded-memory inference for a class of reactive probabilistic programs. However, ProbZelus provides no static guarantee of bounded-memory inference. In this work, we dene a language that can be used as a target for the compilation of ProbZelus and identify the semantic conditions and a static analysis that makes it possible to provide a static guarantee.

Delayed Sampling and Bounded-Memory Inference. The mechanism of delayed sampling in probabilistic programs was introduced by Murray et al. [2018] and implemented in the Anglican and Birch programming languages, neither of which supports inference over streams. Delayed sampling, a form of Sequential Monte Carlo [START_REF] Liu | Sequential Monte Carlo Methods for Dynamic Systems[END_REF], can execute in bounded memory because it automates the construction of Rao-Blackwellized particle lters [Doucet et al. 2000b], a particularly ecient variant of SMC. By comparison, Markov chain Monte Carlo techniques generally cannot execute in bounded memory because they maintain a sample of the full history of program execution, the size of which can grow without bound for a probabilistic stream. Variational inference has extensions that make it amenable to streaming [START_REF] Broderick | Streaming Variational Bayes[END_REF]], but we are not aware of any probabilistic programming system that makes use of them.

Other programming languages such as Hakaru [START_REF] Narayanan | Probabilistic inference by program transformation in Hakaru (system description)[END_REF]] use static program transformations to accomplish the same goal of deferring approximate inference as much as possible. It is unclear if these transformations apply to a streaming context, where dynamic information is necessary to reect the evolution of the underlying model over many iterations.

CONCLUSION

Probabilistic programming has been augmented by constructs that perform inference over unbounded iterations on streams of data. Underlying this programming model is delayed sampling, which combines the benets of exact inference and the exibility of sampling.

In our paper, we introduce the <-consumed and unseparated path semantic properties, which show that delayed sampling can execute in bounded memory for reactive probabilistic programs. We present a sound static analysis that veries these two properties with a type system and an abstract delayed sampling graph. To the best of our knowledge, our work is the rst to develop a resource analysis for a probabilistic program in relation to its probabilistic programming system's underlying inference algorithm. We hope this work will enable automatic inference mechanisms whose performance is better understood by model developers in probabilistic programming languages.

A IDEAL SEMANTICS

In this section we present the complete semantics of the deterministic part of ` in Figure 16 and the ideal semantics of the probabilistic part in Figure 17.

The probabilistic semantics of Figure 17 is a measure-based semantics similar to one presented in [START_REF] Staton | Commutative Semantics for Probabilistic Programming[END_REF]]. Given an environment W, an expression is interpreted as a measure {[4]} W : ⌃ ⇡ ! [0, 1), that is, a function which associates a positive number to each measurable set * 2 ⌃ ⇡ , where ⌃ ⇡ denotes the ⌃-algebra of the domain of the expression ⇡, i.e., the set of measurable sets of possible values. sample(E) returns the distribution »E… W . observe(E 1 ,E 2 ) weights execution paths using the likelihood of the observation »E 2 … W w.r.t. the distribution »E 1 … W (for a distribution `we note `pdf its probability density function). Local denitions are interpreted as integration, and we use the Dirac delta measure to interpret deterministic expressions.

B CORE TYPES IN `

This section describes a type system for ` programs. All programs we consider in this work must type check according to this system. The type system ensures that if an expression 4 is given a probabilistic typing judgment `prob 4 : ) (which means that 4 will be evaluated using its probabilistic semantics {[4]} rather than its deterministic semantics »4…), then its type ) is a measurable space that does not include nonmeasurable objects such as functions. The type system also prohibits nested inference.

The types of ` are unit, Booleans, reals, functions, and pairs, as well as probability distributions, and deterministic and probabilistic stream functions and stream instances.

) ::= unit | bool | real | ) ! ) | ) ⇥ ) | distr ) | dstreamfn(),) ) | dstream(),) ) | pstreamfn(),) ) | pstream(),) )
Only a subset of these types may act as the support of probability distributions, denoted by the judgment measurable() ). These exclude function and stream types:

measurable(unit) measurable(bool) measurable(real) measurable() 1 ) measurable() 2 ) measurable() 1 ⇥ ) 2 ) measurable() ) measurable(distr ) )
We present the full type system of ` in Figures 18 and19.

C DEFINITION OF gra

In this section, we review the denition of gra from Murray et al. [2018].

C.1 Preliminaries

This denition makes use of an alternative type of marginalized node that maintains its own marginal distribution as well as a conditional distribution that relates the marginalized node to its unique marginalized child. We use the notation Marginalized (`m arg , `cond ) to refer to such a marginalized node with marginal distribution `marg and conditional distribution `cond . We use the notation B = Marginalized (_) to mean that the node state B is a marginalized node of any type. The two types of marginalized nodes only dier in the distributions they store, and have the same reachability and memory consumption properties. Murray et al. [2018] denes invariants of delayed sampling runtimes. Namely, it species that delayed sampling maintains that (1) all nodes in the delayed sampling graph have at most one parent, and (2) all marginalized nodes in the graph have at most one marginalized or realized child. In the following denitions, we use the notation parent (-, ⇢) to mean a function that returns the unique parent ofin the edge set ⇢. We also use the notation child (-, ⇢) to mean a function that returns the unique realized or marginalized child of the marginalized nodein the edge set ⇢.

»val G = 4… W = W [G »4… W ] »val 5 = fun ? -> 4… W = W [5 (_E. »4… W +[E/? ] )] »3 1 3 2 … W = let W 1 = »3 1 … W in »3 2 … W 1 »val < = stream { init = 4 init ; step(? state ,? input ) = 4 }… W = W [< stream { init = 4 init ; step(? state ,? input ) = 4 } W ] »2… W = 2 »G… W = W (G) »(E 1 ,E 2 )… W = (»E 1 … W ,»E 2 … W ) »op(E)… W = op(»E… W ) »5 (E)… W = W (5 )(»E… W ) »let ? = 4 1 in 4 2 … W = let E = »4 1 … W in »4 2 … W +[E/? ] »if E then 4 1 else 4 2 … W = if »E… W then »4 1 … W else »4 2 … W »init(<)… W = let stream { init = 4 init ; step(? state ,? input ) = 4 } W 0 = »<… W in let B init = »4 init … W 0 in (B init , _(B, E). »4… W 0 +[B/? state ,E/? input ] ) if 4 is deterministic »init(<)… W = let stream { init = 4 init ; step(? state ,? input ) = 4 } W 0 = »<… W in let B init = »4 init … W 0 in (B init , _(B, E). {[4]} W 0 +[B/? state ,E/? input ] ) if 4 is probabilistic »unfold(G,E)… W = let E state , 5 = »G… W in let E output , E 0 state = 5 (E state , »E… W ) in (E output , (E 0 state , 5 )) »infer(<)… W = let stream { init = 4 init ; step(? state ,? input ) = 4 } W 0 = »<… W in let B init = »4 init … W 0 in (X B init , infer (_(B, E). {[4]} W 0 +[B/? state ,E/? input ] )) where infer (5 ) = _(f, E). let `= _* . Ø ( f (3B)5 (B, E)(* ) in let a = _* . `(* )/`(>) in (c 1⇤ (a), c 2⇤ (a))

C.2 Definitions

We dene the gra function as follows. When called on an initialized node, gra recursively marginalizes every initialized ancestor of the given node. This means that it performs integration to incorporate parent information into the distributions of each node in the initialized chain. When called on a marginalized node, gra calls the prune function.

`det () : unit 2 2 {true, false} `det 2 : bool 2 2 R `det 2 : real `det 4 1 : ) 1 `det 4 2 : ) 2 `det (4 1 ,4 2 ) : ) 1 ⇥ ) 2 , ? 1 : ) 1 , ? 2 : ) 2 `k 4 : ) 0 , (? 1 , ? 2 ) : ) 1 ⇥ ) 2 `k 4 : ) 0 , G : ) `k G : ) `det 4 : ) `k 5 : ) ! ) 0 `k 5 (4) : ) 0 `det 4 1 : bool `k 4 2 : ) `k 4 3 : ) `k if 4 1 then 4 2 else 4 3 : ) `k 4 1 : ) 1 , ? : ) 1 `k 4 2 : ) 2 `k let ? = 4 1 in 4 2 : ) 2 `det < : dstreamfn() input ,) out ) `det init(<) : dstream() input ,) out ) `det < : pstreamfn() input ,) out ) `det infer(<) : pstream() input ,) out ) `det 4 1 : dstream() input ,) out ) `det 4 2 : ) input `k unfold(4 1 ,4 2 ) : ) out ⇥ dstream() input ,) out ) `det 4 1 : pstream() input ,) out ) `det 4 2 : ) input `k unfold(4 1 ,4 2 ) : distr ) out ⇥ pstream() input ,) out ) `det 4 : ) measurable() ) `prob 4 : ) `det 4 : distr ) `prob sample(4) : ) `det 4 1 : distr ) `det 4 2 : )
`prob observe(4 1 ,4 2 ) : unit Fig. 19. Deterministic and probabilistic type systems for ` . The typing judgment `det 4 : ) means that the ` expression 4 under the context has the deterministic type ) . The judgment `prob 4 : ) means that the ` expression 4 under context has the probabilistic type ) . The judgment `k 4 : ) stands for either the deterministic or the probabilistic judgment, where : is instantiated to be 34C or ?A>1. These rules state that sample and observe can only be used inside the body of a probabilistic stream.

We dene the prune function as follows. When called on a marginalized node with a marginalized or realized child, the function rst recursively prunes that child if the child itself is marginalized. If the node is marginalized, it samples a value for that node and then conditions the current node on the child taking on that value. If the child node is realized, the function proceeds to immediately condition the current node on the child node's value.

In either case, the conditioning proceeds as follows. The prune function rst extracts probability density functions from the relevant measures using the pdf function. It then follows Bayes' rule, multiplying the prior and conditional density functions and normalizing the result with the normalize function. It nally updates the marginal distribution of the given node and removes the edge connecting the node to its child.

prune(-

, 6) = let (+ , ⇢, @) = 6 in if @(-) = Marginalized (`-, `) then let -child = child (-, ⇢) in let 6 0 = prune(-child , 6) in if @(-child ) = Marginalized (`c hild ) then let E, (+ 00 , ⇢ 00 , @ 00 ) = value(-child , 6 0 ) in let ? -, ? child |-= pdf (`-), pdf (`) in let `0 -= normalize(_G .? -(G) ⇤ ? child |-(E |G)) in let @ 000 = @ 00 [-child Realized (E), - Marginalized (`0 -)] in (+ 00 , ⇢ 00 (-, -child ), @ 000 ) else if @(-child ) = Realized (E) then let E, (+ 00 , ⇢ 00 , @ 00 ) = 6 0 in let ? -, ? child |-= pdf (`-), pdf (`) in let `0 -= normalize(_G .? -(G) ⇤ ? child |-(E |G)) in let @ 000 = @ 00 [- Marginalized (`0 -)] in (+ 00 , ⇢ 00 (-child , -), @ 000 ) else 6 else 6 D COMPLETE ANALYSIS TYPE SYSTEM
The following is the complete denition of the typing judgment , G `U 4 : C, G 0 describing the types and abstract graph transitions of expressions. ` programs consist of a series of value, function, and stream function declarations. Thus, we also dene a top-level judgment `U 3 :: program that states that a ` program 3 contains declarations

E.2 Type Soundness

In this section, we show that the type system is sound. We rst dene the ✏ relations referenced in Section 6.5. We then prove the soundness theorems stated in Section 6.5.

Variable Mappings. Both delayed sampling and the type system use a set of fresh variable names to label random variables. Because the type system and the delayed sampling execution may each use a dierent name for conceptually the same random variable, we dene an association that maps between these namespaces. We use the notation ✓ to refer to a function that maps a delayed sampling variable to a type system variable, and ✓ ⇤ to the extension of ✓ to sets: ✓ ⇤ ( -) = {✓ (-) | -2 -}.

E.2.1 Entailment.

Here we establish what it means for a value to entail a type. A value entails a type if the type accurately captures the random variables the value could refer to, as well as the shape of the value (i.e. whether the value is a scalar, a pair, or a stream function). Because step function types include type contexts, we also establish what it means for an environment to entail a type context.

A stream value entails bounded if it produces a sequence of states in which every delayed sampling graph is bounded. We formalize this as follows. Given a sequence of inputs (8 = ) = 2N and an initial state B 0 , we say a stream function 5 produces the sequence of state (B = ) = 2N on (B 0 , 8), if 5 (8 = , B = ) = (> = , B =+1 ) for some output sequence (> = ) = 2N . We say B, is bounded if every sequence delayed sampling graphs contained in B is low-level bounded-memory. The rules for any other values are similar to those in Denition E.3, but pass the setthrough unchanged for recursive denitions.

The fold operation & is designed to generate a scalar type that encapsulates the free variables of a value while disregarding its shape. A traced graph entails an <-consumed abstract graph if the abstract graph soundly approximates the variables that are not used.

Denition E.6 (<-consumed Graph Entailment). A traced graph (6, g) entails an <-consumed abstract graph G, written (6, g) ✏ ✓ mc G, if for every variablenot in G.in \ G.con and for every -0 such that ✓ (-0 ) = -, -0 is used in g.

A traced graph entails an unseparated-path abstract graph if the path function soundly approximates the unseparated paths in the traced graph and the separator set soundly approximates the set of variables that are observed or valued.

Denition E.7 (Unseparated Path Graph Entailment). A graph (6, g) entails an unseparated-path abstract graph G, written (6, g) ✏ ✓ up G if for every -1 , -2 that are referenced in g, G.? (✓ (-1 ), ✓ (-2 )) is at least the length of the unseparated path between -1 and -2 in g, and, for allreferenced in g, G.B4? (✓ (-)) is only true ifis a separator in g.

Entailment from Section 6.5. Here, we dene the entailment relations that are referenced in Section 6.5. These denitions are dened in terms of the relevant denitions in this section with the variable map ✓ existentially quantied:

E ✏ U C () 9✓. E ✏ ✓ C W ✏ U () 9✓. W ✏ ✓
E, (6, g) ✏ U C, G () 9✓. E ✏ ✓ C ^(6, g) ✏ ✓ U G W, (6, g) ✏ U , G () 9✓. W ✏ ✓ ^(6, g) ✏ ✓ U G

We further extend these denitions to incorporate a restricted variable set -.

E ✏ U, -C () 9✓. E ✏ ✓ -C W ✏ U, - () 9✓. W ✏ ✓ - E, (6, g) ✏ U, -C, G () 9✓. E ✏ ✓ -C ^(6, g) ✏ ✓ U G W, (6, g) ✏ U, -, G () 9✓. W ✏ ✓ - ^(6, g) ✏ ✓
U G E.2.2 Soundness Theorems. An <-consumed type judgment is sound if it abstracts the <-consumed property of the semantics according to the entailment relations. S C T 6.1 (< T S). If W, (6, g) ✏ mc , G and , G `mc 4 : C, G 0 and {[4]} W (6, g), F = E, (6 0 , g 0 ), F 0 , then E, (6 0 , g 0 ) ✏ mc C, G 0 P. By structural induction on derivations of `mc . ⇤

Proving the soundness of the <-consumed judgment producing the bounded type requires strengthening this theorem to work with partial traces, meaning the abstract graph applies only to the tail end of the trace rather than the whole trace. Using the notation g 1 g 2 to mean the trace g 1 appended with g 2 , we formalize this as follows: let _ = observe (gaussian (x_prev, 1.), obs) in let x = sample (gaussian (x_prev, 1.)) in (x, x) }

In this example, every sample is eventually consumed but only on the subsequent iteration of the step function. If the <-consumed analysis only considered one iteration, it would reject this example. Allow introduced variables to be consumed over multiple iterations as we do allows this example to pass the analysis.

Most examples do not require a signicant number of iterations for the unseparated paths analysis to converge. However, the analysis may fail to detect convergence in programs with many variables if the iteration bound parameter is too low, as in the following program which requires four iterations: stream { init = (0., 0., 0., 0.); step ((x_p, x_pp, x_ppp, x_pppp), obs) = let x = sample (gaussian (x_p, 1.)) in let _ = observe (gaussian (x, 1.), 1.0) in (x_pppp, (x, x_p, x_pp, x_ppp)) }

In this program, the longest unseparated path increases over four iterations, after which variables start being dropped from the state and the maximum length converges. We suggest that the parameter should be set to be comfortably larger than the number of variables or statements in the program to avoid this issue. Since each iteration is fast to run, it should not cause performance degradation.

Finally, the analysis could incorporate higher-order functions, though they would be hard to analyze statically, and the storage of chains of closures built over many iterations could itself violate a bound on memory usage.

Fig. 1 .

 1 Fig. 1. ` program with main stream function robot.

Fig. 2 .

 2 Fig.2. The evolution of the delayed sampling graph for the hidden Markov model in Figure1(kalman) as implemented by[START_REF] Baudart | Reactive Probabilistic Programming[END_REF]. Each node denotes either a value (dark gray) or a distribution (light gray). A plain arrow denotes a dependency in the underlying Bayesian network. A doed arrow denotes a pointer in the implementation of the delayed sampling graph. Each label indicates the program variable that

Fig. 4 .

 4 Fig. 4. The evolution of the delayed sampling graph for the variant of a Kalman probabilistic model in Figure 3. Nodes and edges have the same meaning as in Figure 2.

  program ::= 3 ⇤ < 3 ::= val ? = 4 | val 5 = fun ? -> 4 | val < = stream { init = 4 ; step(?,?) = 4 } 4 ::= E | op(E) | 5 (E) | if E then 4 else 4 | let ? = 4 in 4 | init(<) | unfold(G,E) | sample(E) | observe(E,E) | infer(<) E ::= 2 | G | (E,E) ? ::= G | (?,?)

Fig. 8 .

 8 Fig. 8. Deterministic semantics of ` (complete definition in Figure16).

Figure 8

 8 Figure8denes the semantics of declarations and deterministic expressions »•…. The declarations build the evaluation environment W which maps names to values, functions, and stream functions.The semantics of deterministic expressions corresponds to a rst order functional language with new constructs to handle streams and the infer(•) operator (the complete denition is given in Figure16of Appendix A). The expression init(<) creates an instance of the stream function <: a pair corresponding to the current state, and the transition function. The current state is initialized with the value of the init eld. The expression unfold(G,E) executes the transition function of the instance G on its current state and the input E. This expression produces a pair composed of the transformed value and the updated instance.The ideal semantics of ` probabilistic expressions {[•]} is a measure-based semantics similar to the one presented by[START_REF] Staton | Commutative Semantics for Probabilistic Programming[END_REF] (the complete denition is given in Appendix A). Given an environment W, an expression is interpreted as a measure {[4]} W : ⌃ ⇡ ! [0, 1), that is, a function which associates a positive number to each measurable set * 2 ⌃ ⇡ , where ⌃ ⇡ denotes the ⌃-algebra of the domain of the expression ⇡ (i.e., the set of measurable sets of possible values). sample(E) returns the distribution »E… W . observe(E 1 ,E 2 ) weights execution paths using the likelihood of the observation »E 2 … W w.r.t. the distribution »E 1 … W (for a distribution `we denote its probability density function as `pdf ). Local denitions are interpreted as integration, and we use the Dirac delta measure to interpret deterministic expressions.

Fig. 9 .

 9 Fig. 9. Delayed sampling semantics. Probabilistic expressions are functions from a graph and a weight to a triplet (value, graph, weight).

  | obs(-) Proc. ACM Program. Lang., Vol. 5, No. OOPSLA, Article 115. Publication date: October 2021. Statically Bounded-Memory Delayed Sampling for Probabilistic Streams 115:15

Fig. 10 .

 10 Fig. 10. Tracing semantics of delayed sampling operators.

Fig. 12 .

 12 Fig. 12. <-consumed abstract graph operations.

Fig. 15 .

 15 Fig. 15. Join operator for types.

Fig. 14 .

 14 Fig. 14. Delayed sampling type system.

Fig. 16 .

 16 Fig. 16. Deterministic semantics of ` .

`U 2

 2 : (;, ;) , G : C `U G : C , < : (C init , stepfn(? state , ? in , 4 , 4)) `U < : (C init , stepfn(? state , ? in , 4 , 4))`U E : A -= fresh(G) , G `U sample(E) : ({-}, {-}), assume U (-, A, G) , G `U sample(E 1 ) : ({-}, {-}), G 0 `U E 2 : A 2 , G `U observe(E 1 ,E 2 ) : (), observe U (-, A 2 , value U (A 2 , G 0 )) `U E : C C & A `U op(E) : A , G `U 4 : C, G 0 , ? : C, G 0 `U 4 0 : C 0 , G 00 , G `U let ? = 4 in 4 0 : C 0 , G 00 `U E 1 : C 1 `U E 2 : C 2 `U (E 1 ,E 2 ) : C 1 ⇥ C 2 `U E : A G 0 = value U (A, G) , G 0 `U 4 1 : C 1 , G 1 , G 0 `U 4 2 : C 2 , G 2 , G `U if E then 4 1 else 4 2 : C 1 t C 2 , G 1 t U G 2 `? ? : C , ? : C `U 4 : C 0 `U fun ? -> 4 : C ! C 0 `U 5 : C ! C 0 `U E : C `U 5 (E) : C 0 `U < : (C, B) `U init(<) : stream(C, B) `<2 < bounded `D? < bounded `U infer(<) : bounded `U G : stream(C, stepfn(? state , ? in , 4 , 4)) `U E : C in 4 , ? state : C, ? in : C in , G `U 4 : C 0 ⇥ C out , G 0 , G `U unfold(G,E) : C out ⇥ stream(C 0 ,stepfn(? state , ? in , 4 , 4)), G 0 `U G : bounded `U E : C C & (;, ;) `U unfold(G,E) : (;, ;) ⇥ bounded

  Denition E.3 (Type Entailment).A value E entails a type C, written E ✏ ✓ C, under the following circumstances:2 ✏ ✓ (;, ub) -✏ ✓ (lb, ub) () lb ✓ {✓ (-)} ✓ ub app(op, E) ✏ ✓ (lb, ub) () lb ✓ ✓ ⇤ (frv(E)) ✓ ub (E 1 ,E 2 ) ✏ ✓ C 1 ⇥ C 2 () E 1 ✏ ✓ C 1 and E 2 ✏ ✓ C 2 stream { init = 4 init ; step(? in ,? state ) = 4 state } W 4 ✏ ✓ (C init , stepfn(? in , ? state , 4 , 4 state )) () 4 init ✏ ✓ C init ^W4 ✏ ✓ 4 (B 0 , 5 ) ✏ ✓ stream(C init , () () B 0 ✏ ✓ C init and 5 ✏ ✓ ( 5 ✏ ✓ stepfn(? in , ? state , 4 , 4) () 9W. W ✏ ✓ 4 and 5 = _(B, E). {[4]} W +[B/? state ,E/? in ] W ✏ ✓ () 8G : C 2 . W (G) = E s.t. E ✏ ✓ C (B 0 , 5 ) ✏ bounded () 8i. 5 produces B on (B 0 , 8) ) B is boundedWe further dene a version of type entailment that only applies to a restricted set of variables.Denition E.4 (Restricted Type Entailment).A value E entails a type C -restricted to the variable set -, written E ✏ ✓ -C, under the following circumstances:2 ✏ ✓ -(;, ub) -✏ ✓ -(lb, ub) () -2 -) lb ✓ {✓ (-)} ✓ ub app(op, E) ✏ ✓ -(lb, ub) () -2 -) lb ✓ ✓ ⇤ (frv(E)) ✓ ub

  L E.5 (F E). If E ✏ ✓ C and C & (lb, ub), then lb ✓ ✓ ⇤ (frv(E)) ✓ ub.

Proc. ACM Program. Lang., Vol. 5, No. OOPSLA, Article 115. Publication date: October 2021.

we write F 8 = F 8 / Õ # 8=1 F 8 for the normalized weights. Proc. ACM Program. Lang., Vol. 5, No. OOPSLA, Article 115. Publication date: October

ACKNOWLEDGMENTS

We would like to thank Cambridge Yang, Alex Renda, Jesse Michel, and Ben Sherman, who all provided feedback on drafts of this paper. This work was supported in part by the MIT-IBM Watson AI Lab and the Oce of Naval Research (ONR N00014-17-1-2699). Any opinions, ndings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reect the views of the Oce of Naval Research.

Example Type Derivation

This section presents an example type derivation used by the analysis to conrm that the program in Figure 1 satises the <-consumed property. In particular, we conrm that the stream function kalman passes the <-consumed analysis.

Using 4 as shorthand for the body of its step function, we derive the following <-consumed success condition for kalman:

`mc kalman bounded

The second and fourth premises follow immediately from denitions and set operations. The derivation of the rst and third premises is as follows:

`mc kalman : ((;, ;), stepfn(pre_x, obs, 4 , 4)) `? obs : (;, ;) 4 , obs : (;, ;), pre_x : (;, ;), (;, ;) `mc 4 : (({-}, {-}) ⇥ ({-}, {-})), ({-}, {-}) `mc(0) kalman : (({-}, {-}) ⇥ ({-}, {-}))

The second premise follows from denitions. The derivation of the rst premise is as follows:

4 `mc 0.0 : (;, ;) (;, ;) & (;, ;) `mc stream { init = 0.0 ; step(pre_x,obs) = 4 } : ((;, ;), stepfn(pre_x, obs, 4 , 4))

where the premises follow immediately. Finally, let 0 be the context 4 , obs : (;, ;), pre_x : (;, ;) and C be the type (;, ;). The derivation of the third premise is as follows. The rst premise follows from the typing rule for sample. The second premise follows from the typing rule for let as follows:

where the rst premise follows from the rule for observe and the second from the rule for pairs.

Soundness

Here, we outline how we show the type system is sound. We give a high-level overview of the approach; the details are in Appendix E.

Entailment Relations. In Appendix E.2, we establish several entailment relations that relate semantic objects to their type-level counterparts. These relations are parameterized by U which is either <2 for the <-consumed relation or D? for the unseparated path relation. We write E ✏ U C to mean a value entails a type. We write W ✏ U to mean an environment entails a type context. We write E, (6, g) ✏ U C, G to mean a value and traced graph (see Section 5.2 for the denition of a traced graph) entail a type and abstract graph. We write W, (6, g) ✏ U , G to mean an environment and traced graph entail a type context and abstract graph. `det 4 : )

`decl val ? = 4 : , ? : ) , ? : ) `det 4 : ) 0 `decl val 5 = fun ? -> 4 : , ? : Fig. 18. Typing rules for programs in ` . The judgment `decl 3 : 0 means that the ` declaration 3, when typed under the typing context , produces the typing context 0 .

gra (-,

that are all well-formed. This judgment is dened as follows:

where if 3 is empty (i.e. all streams including main are valid) the judgment holds trivially.

E SOUNDNESS E.1 Executions

During the execution of a program, the only constructs that can dynamically allocate memory are sample and observe which add a new node to the delayed sampling graph using the assume operation. These two probabilistic constructs can only be used in a model, i.e., the argument of the infer operator. We thus focus on the memory footprint of infer's transition function.

The execution of the transition function infer of infer comprises three steps (see Section 4.1): (1) draw a set of particles, i.e., pairs (state, graph), (2) execute the model for each particle, (3) extract the distributions of state and outputs. The only operation that can dynamically allocate memory is the second one, where the delayed sampling graph can be altered.

At iteration =, for each particle, the current pair (state, graph) is obtained from a succession of application of the model transition function from the initial state B 0 and an empty graph 6 0 = ; (step (1) in the denition of infer can only drop some execution paths). We call this sequence (B 0 , 6 0 ), (B 1 , 6 1 ), . . . an execution of the model. The following properties states that if only boundedmemory execution are possible, then the infer function executes in bounded-memory.

L E.1 (E S). For all stream functions < and environments W, let stream { init = 4 init ; step(? state ,? input ) = 4 } W 0 = »<… W and let B < = »4 init … W 0 and let 5 < = _(B, E). {[4]} W +[B/? state ,E/? input ] and let B 8 , 5 8 = »infer(<)… W . We say that 5 8 produces a sequence of distributions (`=) = 2N given an input sequence (8 = ) = 2N if 5 8 (`=, 8 = ) = (l = , `=+1 ) for some sequence of output distributions (l = ) = 2N . Similarly, we say 5 < produces the execution

The lemma states that for all input sequences (8 = ) = 2N , if 5 8 produces the sequence (`=) = 2N , then for all = and (6 = , B = ) 2 support(`=), there exists an execution

Proceed by induction on =. If = = 0, the distribution `0 is obtained by the execution of 5 < by each particle on the initial state and the empty graph. So the support of `0 is obtained by the execution of 5 < . If = > 0, by denition of infer, each pair (6 = , B = ) from the support of the distribution `= is obtained by the application of 5 < on (6 = 1 , B = 1 ) drawn from the distribution `= 1 . By application of the induction hypothesis, (6 8 , B 8 ) 08<= is an execution produced by 5 < , and therefore (6 8 , B 8 ) 08 = is also produced by 5 < . ⇤ C E.2. If all executions of 5 < are bounded-memory, then for any input sequence (8 = ) = 2N and any execution (6 = , B = ) = 2N such that for all =, every (6 = , B = ) 2 support(`=), (6 = , B = ) = 2N has bounded memory when `= is produced by 5 8 . L E.8. <-consumed Soundness on Partial Traces If W, (6, g 2 ) ✏ mc , G and , G `mc 4 : C, G 0 and {[4]} W (6, g 1 g 2 ), F = E, (6 0 , g 0 ), F 0 , then g 0 = g 1 g 0

2 and E, (6 0 , g 0 2 ) ✏ mc C, G 0 P. By structural induction on derivations of `mc . The individual steps are the same as the previous theorem, except that they also use the associativity of . ⇤

An unseparated-path type judgment is sound if it abstracts the unseparated path property of the semantics according to the entailment relations. S C T 6.1 (U P T S). If W, (6, g) ✏ up , G and , G `up 4 : C, G 0 and {[4]} W (6, g), F = E, (6 0 , g 0 ), F 0 , then E, (6 0 , g 0 ) ✏ up C, G 0

We also strengthen this theorem to aid in proving the soundness of the bounded judgment. L E.9. Unseparated Paths Soundness on Partial Traces If W, (6, g 1 g 3 ) ✏ up,frv (g 1 g 3 ) , G and , G `up 4 : C, G 0 and {[4]} W (6, g 1 g 2 g 3 ), F = E, (6 0 , g 0 ), F 0 , then g 0 = g 1 g 2 g 0

3 and E, (6 0 , g 1 g 0

3 ) ✏ up,frv (g 1 g 0 3 ) C, G 0 P. By structural induction on derivations of `up . The individual steps are the same as the previous theorem, except that they also use the associativity of .

⇤ T E.10 (A S). If W ✏ U and `U < : bounded, then »<… W ✏ U bounded.

P. We rst show that any execution of a stream function < satisfying `mc < bounded satises the high-level <-consumed semantic property. We then show that any execution of a stream function < satisfying `up < bounded satises the high-level unseparated paths semantic property. Then, by Theorem 5.11 and Lemma E.1, if < satises both these properties, then calling infer on < must be bounded.

<-consumed.

Here, we show that any execution of a stream function < satisfying `mc < bounded satises the <-consumed semantic property. We proceed by induction on the steps of the execution. Note that at each step the program only adds to the trace and thus only adds new introduced variables we ust reason about. We show that the variables introdued at each time step will all be <-consumed.

We show this using the denition of `mc . Let (6 8 , g 8 ) be the 8th step of the execution. By Lemma E.8, G captures all variables introduced at time 8. Also by Lemma E.8, G 0 captures the variables that are guaranteed to be consumed between 8 and 8 + =. Thus, any variable introduced at time step 8 must be consumed within = steps (where = is a static bound). If it is consumed, the variable will be <-consumed at all future time steps where < is at most = times a constant bound based on the number of sample statements in the stream function.

Unseparated Paths. We proceed by contradiction. Assume that B 8 , (6 8 , g 8 ) 8 2N is an execution that violates the unseparated paths semantic property. At some time step 9, the execution must a) add a variable to the delayed sampling graph in such a way that it increases the unseparated path starting from some variable in the graph, and b) store the variable starting the increased path in B 9+1 . Otherwise, the execution would easily satisfy the property. According to Lemma E.9, we must have that after each iteration the abstract graph also has a variable with starting an increased path and that some reference A ⇤ contained in the type C 0 references this variable. Letting ' be the set of all possible references A ⇤ , by the pidgeonhole principle, after : size(C) = size(C 0 ) | '| iterations, 2 the longest path in the abstract graph starting from a variable referenced by an element of ' must have increased by at least 1. Similarly, after = path(C, G) instances of this pattern, the longest 2 the equality of size(C ) and size(C 0 ) is enforced by the type rules in Figure 18 path in the abstract graph starting from a variable referenced in ' must have increased by at least path(G, C) and thus be the longest such graph starting from a state variable. This contradicts the termination condition that path(C, G) = path(C 00 , G 0 ). ⇤

F BENCHMARKS

Each of these benchmarks are followed by a main stream that serves as the entry point of the program:

F.2 Kalman Hold-First val kalman = stream { init = (true, 0., 0.); step ((first, i, pre_x), obs) = let (i, pre_x) = if first then (let i = sample (gaussian(0., 1.)) in (i, i)) else (i, pre_x) in let x = sample (gaussian (pre_x, 1.)) in let () = observe (gaussian (x, 1.), obs) in (x, (false, i, x)) }

F.3 Gaussian Random Walk

G PRECISION LIMITATIONS

The precision of the analysis is limited by path and complex sensitivity, two common challenges for static analysis. The analysis can be overly conservative when facing conditional branches, for example in the following snippet: let x = sample bernoulli(0.5) in let y = sample gaussian (0., 1.) in let () = if x then observe (gaussian (y, 1.), 1.) else () in let () = if x then () else observe (gaussian (y, 1.), -1.) in y

According to the analysis, y is not consumed because each branch is separately and conservatively judged to not consume y, even though there is no path where y is unobserved. A more sophisticated analysis that reasons about actual values, not just aected variables, would be more precise here.

Similarly, the analysis can be imprecise in the presence of complex data such as tuples. Consider the following snippet: let x = sample (gaussian(0., 1.)) in let y = sample (gaussian(0., 1.)) in let (a, b) = if (sample (bernoulli(0.5))) then (gaussian (x, 1.), gaussian (y, 1.)) else (gaussian (y, 1.), gaussian (x, 1.)) in let () = observe (a, 1.) in let () = observe (b, 2.) in (x, y)

Like the previous example, x, y are not considered consumed even though there is no path that does not observe both. The analysis can determine that both a and b may reference x and y but neither alone must do so. Knowledge about a and b taken as a pair is lost when they are stored into the tuple. In this case, some kind of alias or shape analysis might recover the relationship between the elds of a tuple.

Without executing for multiple iterations, the <-consumed analysis would be occasionally too conservative due to requiring that all variables be used before the end of the current iteration of the step function. Consider: stream { init = 0.; step (x_prev, obs) =