RePPL

Note

RePPL is research software, so its interfaces can change from one release to the next. A preprint describing it is in preparation.

• Purpose: A probabilistic programming language which separates the representation of a measure (as a program) from computations on that measure (also as programs) into two languages. The first is an expressive higher-order probabilistic programming language ($\lambda_{Ch}$), and the second is a dependently typed language with reflection on the first ($\lambda_{Ag}$). Computations on measures are written as programs in $\lambda_{Ag}$ as certified compilers from $\lambda_{Ch}$ to $\lambda_{Ch}$.

RePPL is a probabilistic programming system in Lean 4. RePPL distinguishes the representation of a measure by a probabilistic program from the implementation of computational requests on that measure. Requests encompass things such as sampling, density evaluation, integration, and derivatives.

To answer a request, the system interactively helps users to write compiler programs that implement the request for their probabilistic program. The result of this process couples runnable code with a proof that it meets the requirements of the request.

Install

The source archive is attached to the GitHub release, and gh downloads it:

gh release download v26.10.3 --repo a-tiny-project/reppl --pattern 'reppl-v26.10.3.tar.gz'
tar -xzf reppl-v26.10.3.tar.gz

The extracted directory is a Nix flake. nix build builds the library and runs its checks on x86_64 Linux. nix develop enters a shell with Lake, the Lean release that lean-toolchain pins (leanprover/lean4:v4.34.1), and the official Zig 0.17.0 release, which builds its native code. The lake commands below run from the archive root, inside that shell.

Use

The example in RePPL/Examples/Linkage.lean asks whether two hospital records, one reading "Smith" and the other "Smyth", belong to one patient or to two. The model is a $\lambda_{Ch}$ program, written with ch def:

ch def name : Prob String := do
  let u ← uniform
  return (if u < half then "Smith" else "Smyth")

ch def typo (seen : String) (meant : String) ⊢ ℝ≥0 :=
  if seen == meant then keep else slip

ch def linkage :
    Measure (𝔹 × String × String) := do
  let same ← flip half
  let n₁ ← name
  let fresh ← name
  let n₂ := if same then n₁ else fresh
  score (typo "Smith" n₁)
  score (typo "Smyth" n₂)
  return (same, n₁, n₂)

linkage flips a fair coin same to choose between one patient and two, draws a name for the first patient (and a fresh name for a possible second), and gives the second record the first patient's name when same holds. Each name is "Smith" or "Smyth" with probability 1/2, and a record copies its patient's name with probability 3/4 (keep), so typo is 3/4 when the names match and 1/4 (slip) when they differ. score multiplies the weight of a run by its argument, so linkage denotes a measure: each set of outcomes receives the total weight of the runs that return an outcome in it. (Programs marked Prob, such as name, denote probability measures.) The measure of all outcomes together, the mass of linkage, is 7/32, the probability of the two records. Dividing by the mass gives the posterior, under which the records share a patient with probability 3/7.

WeightedSampler linkage is a request for a sampler: a program that returns a draw x with a nonnegative weight w, such that weighted averages estimate integrals against linkage. For every nonnegative measurable f, the expectation of w · f x must equal the integral of f under linkage (Lew et al., PLDI 2023, call such a program properly weighted, after Liu and Chen, JASA 1998). The user answers the request with a compiler program, a $\lambda_{Ag}$ program whose type is the request. Writing K for the rest of the model once same is drawn, the compiler program inference delivers a program that draws same from its prior, draws the names exactly from K normalized, and returns K's mass as the weight:

noncomputable def inference :
    WeightedSampler linkage := by
  cut_with weightedBind
  case weightedBind.next =>
    cut_with exactBlock

Lean's goals after each line of inference. cut_with weightedBind opens sourceMeaning, continuationMeaning, initial and next. derive answers the first three and leaves next open, and the case arm takes it. In that arm, cut_with exactBlock opens interpreted, mass and sampler, and derive answers all three, so no goals remain. A chip names each goal and a check marks a goal derive answered.

cut_with weightedBind splits the model at the draw of same, and cut_with exactBlock answers K by asking for its mass and for exact draws from it. The result couples the delivered program with a proof that it is properly weighted for linkage, and Lean checks both when it builds the example.

inference is noncomputable because its answer names the measurable spaces the request is stated over, which have no code. The program it delivers is ordinary $\lambda_{Ch}$ code: it draws same at weight 1, binds K's mass at same (3/16 with one patient and 1/4 with two), draws the names from K's normalized table with one uniform number, and returns them with the product of the two weights. The example states this program as delivered, checks that inference delivers it, and checks what the weights estimate: the expected weight is 7/32, the mass, and the weighted fraction of draws with one patient is 3/7, the posterior. Ignoring the weights gives the prior's 1/2.

RePPL builds with Lean v4.34.1 (de Moura and Ullrich, CADE 2021) and no Mathlib, and its Lean dependencies ship with the release.

• lake build RePPL builds the library, the example included, from the package root.
• lake build RePPL.Axioms audits every claim and allows only Lean's three standard axioms. A claim is a declaration tagged @[trust_claim], or a name listed in RePPL/Axioms.lean.

How it works

The user writes a model e in λ_Ch and a request R e about it in λ_Ag. To answer the request, the user writes a compiler program in λ_Ag that builds an answer: a program c with a proof of correctness that Lean checks. The program c compiles to native code. Blue marks λ_Ch and purple marks λ_Ag, with solid outlines for what the user writes and dashed for what RePPL builds.

In the example, the model is linkage, the request is WeightedSampler linkage, the compiler program is inference, and its answer is the program delivered with its proof. Code in $\lambda_{Ag}$ can read a $\lambda_{Ch}$ program as its syntax tree, while its types state facts about the measure the program denotes (reflection). So a request names the model it is about, and code in $\lambda_{Ag}$ can inspect the model's code to build an answer.

A user trusts Lean's type checker, the definition of what a $\lambda_{Ch}$ program means, and the definitions of the requests. cut_with, derive and every inference tactic sit outside what a user trusts. Lean checks whatever cut_with and derive produce and rejects a wrong answer, so a mistake in them can at worst leave a goal open. An inference tactic cannot be declared unless Lean checks its proof of correctness.

The program in an answer is ordinary $\lambda_{Ch}$ code. RePPL lowers it to a small intermediate language (called Choir), which a native backend shipped with the release compiles. The lowering accepts only part of $\lambda_{Ch}$: it refuses a program that scores, normalizes, lifts a probability program to a measure, sums over an index (superpose), memoizes a random function (mem), or suspends a program (a thunk). It accepts recursion only as a guarded loop (Code.loop), which repeats an attempt until the attempt succeeds: the native program tries each loop's attempt at most a given number of times and answers inl () when a loop runs out. It also refuses index arithmetic and tensor literals with more than 256 entries or with entries that are not scalars (Lowerable). For a closed program it accepts, the lowering is proved correct. Without a loop, the lowered program's law is the program's meaning (lowerModule_law). With loops, it is the program's law with each loop limited to the same number of attempts, whose mass is the chance that every loop succeeds in time (lowerWithin_law). Every program the lowering accepts meets these theorems' premises (interpretable_of_lowered, withinLaw_of_lowerable). For other programs it accepts, the lowering is trusted. The native compiler is trusted for all programs. The example checks that delivered lowers.

A request that has no answer yet is a goal: Lean shows the open goals after each line of a compiler program. One step of an inference algorithm together with its proof of correctness is an inference tactic, a $\lambda_{Ag}$ definition whose type reads as an inference rule (a tactic in the sense of LCF, Gordon et al., LNCS 1979): from answers to smaller requests about parts of the program, it builds an answer to a request about the whole. Each of those smaller requests is a subgoal, and applying an inference tactic turns one goal into its subgoals. weightedBind's subgoals are initial, a sampler for the draw of same, and next, a sampler for K at every value of same: inference's case weightedBind.next arm takes the second. An inference tactic's code is built from the code of its subgoals' answers. Its proof of correctness states that the code the tactic builds answers its goal whenever the code it is given answers its subgoals. It is proved once, when the tactic is declared, and Lean checks it. The figure below shows the goals inference opens and the program it delivers.

The compiler program inference opens a goal (a shaded row) under each cut_with line, each with an arrow to the part of the model linkage it asks about, and a check marks each goal derive answered. The rows show the request subgoals and leave out the conditions, such as sourceMeaning, which derive also answers. Below is the program inference delivers, with its proof: each goal's chip names the code that answers it, and it returns same and the names with weight z. The panel inlines the weight-1 draw of same (the code returns 1 · z) and writes K's normalized table as thresholds on one uniform number. Teal marks same and red marks K.

The figure below shows an inference tactic at a draw: its goal, its two subgoals, and what each subgoal asks about. For weightedBind on linkage, P is flip half, x is same, K is the rest of linkage, and R, R₁ and R₂ are all WeightedSampler.

An inference tactic T splits a goal at a draw of x from P, followed by K, the rest of the program. It answers the goal below the line from answers to the subgoals above: the requests R₁ about P and R₂ about K at every value of x (the "∀ x"). Teal marks x and red marks K.

weightedBind answers a sampler request for a draw followed by the rest of a program, and exactBlock answers one for a block by asking for its mass and for exact draws from it, then returning each draw with the mass as its weight. Keeping the mass is what makes the answer correct. unitWeighted, which returns exact draws at weight 1, asks for a probability program, so it does not apply to K in the case arm, and the example checks that refusal.

Besides its subgoals, an inference tactic can ask for conditions, propositions that must hold for its code to be correct: for weightedBind the conditions are sourceMeaning and continuationMeaning, that the draw and K each have a meaning as a measure. RePPL proves that an answer built from parts that carry their own proofs (inference tactics carry their proofs of correctness, and the answers to subgoals carry theirs) meets its request whenever the conditions collected while building it hold. cut_with T applies the inference tactic T to the current goal: it matches the request T answers against the goal, which locates a region of the model, and opens a goal for each subgoal and condition, named after it (for example weightedBind.next). cut_with leaves each goal a case arm names to that arm and runs derive on the other goals it opens. derive searches the library's registered answers. flip half is a probability program, so it is its own sampler at weight 1. Given same, K has at most four outcomes, so its mass and its exact draws come from tables that the term evaluator computes while Lean checks the program. A goal derive cannot answer stays open for the user. cut_with? prints the inference tactic it applied, the parameters it filled, and, for each goal it opens, whether derive answered it or why the goal stays open.

In the code, most of the library's inference tactics live under RePPL/Ag/Templates/. Some, such as importance, are declared with the command template, a shorthand that takes the tactic's parameters, its subgoals and conditions, its code and its proof of correctness, while weightedBind and exactBlock are written as ordinary definitions.

λCh and λAg

$\lambda_{Ch}$ is the language in which a user writes a model, and each $\lambda_{Ch}$ program denotes a measure. $\lambda_{Ag}$ is the language in which requests say what inference code must deliver for a model and in which Lean checks that the code delivers it: a dependent type theory that can take $\lambda_{Ch}$ programs apart.

Each construct of λ_Ch is an operation on measures: each panel shows a program, the measure it denotes, and its mass. All panels share one vertical scale: height is mass for bars and stems and density for curves. In the bind panel the red dashed curves are K's measures at the two values of z (K is the rest of the program after the draw of z), and elsewhere a grey dashed outline is a measure to compare against: the uniform before score with $w(x) = 4x(1 - x)$, the hump before normalize, a mixture beside superpose, and the branch match does not take.

pure v (or return v inside a do block) puts all mass on the value v as a point mass, so pure 2 places mass 1 at 2. uniform is a primitive draw, with its flat density of height 1 on [0, 1]. categorical is the other primitive draw, which picks one of $n$ outcomes in proportion to $n$ nonnegative weights. Drawing u from uniform and returning u < 0.3 cuts [0, 1] at 0.3, sending the outcomes to a bar of 0.3 at true and a bar of 0.7 at false. This program is flip 0.3, and named distributions such as flip are programs over the primitive draws. A bind mixes the measures of the continuation K, weighted by the draw: drawing z from flip 0.3 and then drawing from gaussian (if z then 2 else -1, 1/4), where gaussian (m, v) is the Gaussian with mean m and variance v, mixes K's two Gaussian measures weighted by 0.3 and 0.7 to produce two bumps at 2 and -1.

score multiplies a density pointwise by a weight and changes the mass: weighting uniform by w forms a hump with mass 2/3. normalize divides a measure by its mass, so dividing that hump by its mass 2/3 yields the density $6x(1 - x)$ with peak 1.5 and mass 1. Where a mixture averages measures, superpose adds them, one for each value of a countable type (here the Booleans 𝔹): adding lifted point masses over 𝔹 yields two bars of height 1 with mass 2 (lift lets a probability program be used where a general measure is expected). A match on a value of a sum type means the branch that the value selects, so matching v at inl 0.3 selects the branch yielding a point mass at 0.3 with mass 1.

The score and superpose panels have masses other than one, so $\lambda_{Ch}$ records in a program's type which kind of measure it denotes. That kind is the program's grade. Prob τ is the type of a program that denotes a probability measure on τ (mass one). Measure τ is the type of one that denotes a countable sum of finite measures, an s-finite measure (Staton, ESOP 2017), whose mass may be any value, including zero and infinity. score is itself Measure code, and superpose needs Measure code to sum over a countable type. normalize turns Measure code into Prob code, and lift turns Prob code into Measure code. The closest precedent for the two grades is the pair of probability and measure monads in LazyPPL (Dash et al., POPL 2023). A bind is Measure if either of its parts is, so a program that scores outside any normalize has type Measure. That is why linkage has type Measure and name has type Prob. A well-typed program need not have a meaning, and its type describes the meaning only where one exists: normalize needs its body's mass to be finite and nonzero, so normalize (score 0) has no meaning, and a recursive program needs the conditions below.

Because superpose adds measures over a countable type, a Measure program can have infinite mass, as in halfLine:

ch def halfLine : Measure ℝ :=
  superpose fun (n : ℕ) => lift (do
    let u ← uniform
    return toReal n + u)

For each n, the piece draws u from uniform and returns toReal n + u (toReal n is the natural number n read as a real number). The piece denotes the uniform measure on [n, n + 1), with density 1 and mass 1. It is a Prob program, and lift lets superpose sum it. The whole program denotes Lebesgue measure on [0, ∞), with density 1 everywhere on the nonnegative reals and infinite mass, both proved in the library. Lebesgue measure is the usual reference measure for the densities in the Requests section, and here it is a $\lambda_{Ch}$ program. The figure below shows the pieces and their sum.

The four rows show the sums of the pieces for n = 0, n ≤ 1, n ≤ 2 and all n, with masses 1, 2, 3 and ∞. Each block is one piece, with density 1 on one unit interval and mass 1. Adjacent blocks alternate two shades only to tell them apart.

A recursive program is written recur fun (f : Thunk ...) => body: the body receives f, a suspended copy of the whole program (a thunk), and calls itself with force f. Its meaning is a limit. Starting from the zero measure (no mass anywhere), unrolling the body over it $n$ times gives the approximation $\Phi^n(0)$, where $\Phi$ is the body read as a function from the measure of the recursive call to the measure of the whole. The meaning is the limit (the supremum) of these approximations as $n$ grows. A recursive program has a meaning only when its body is the call itself, or when the call sits only inside a bind or in the branches of a match (an if included) whose scrutinee does not mention it. At grade Prob, the limit must also have mass one at every input. The figure below shows two programs that meet the conditions, one whose limit has mass one and one whose limit stays at the zero measure.

A recursive program means the limit of its approximations $\Phi^n(0)$, the body unrolled $n$ times over the zero measure: the top row counts flips until a fair coin lands true, while the bottom row only calls itself. The top limit has mass one, so it has a meaning as a Prob program (labeled "prob"), while the bottom stays at the zero measure, a meaning only as a Measure program (labeled "sfin" for s-finite).

$\lambda_{Ag}$ is implemented in Lean, and the figure below shows the reflection named in How it works on flip 0.3. The syntax of $\lambda_{Ch}$ is one family of $\lambda_{Ag}$ types, Phrase, indexed by a context (the types of the variables in scope) and a judgment (what kind of term it is and its type). So only well-typed $\lambda_{Ch}$ programs exist as values of Phrase. Variables are numbered by position in the context (de Bruijn indices: de Bruijn, Indag. Math. 1972): var head is the most recently bound one. Because syntax is a family of types, a $\lambda_{Ag}$ program can match on a $\lambda_{Ch}$ program's constructors: split it at its first bind, read the weight of a score, or build new code. And the meaning of $\lambda_{Ch}$ is a $\lambda_{Ag}$ function on Phrase, which gives a measure for each program that meets the conditions on normalize and recursion, so $\lambda_{Ag}$ types can state facts about the measure a program denotes.

λ_Ag holds a λ_Ch program as a tree of the family Phrase, which its code can split at the first bind into P and K, and the meaning function ⟦·⟧ maps the same tree to its measure. Each node label shows a constructor over its context and judgment, where 𝕀 is the unit interval [0, 1] and var head is the variable u just drawn.

Requests

In the example, the user stated one request, WeightedSampler linkage. A user can state others, and an inference tactic's subgoals ask for them too: draws that follow a distribution exactly, a population of weighted draws, a random step that leaves a distribution in place, or a number, such as a mass or a density. Each kind of code is correct in a different sense, and its request writes that sense down as an equation about the program's measure, which every answer satisfies. For a program p, write μ for its measure.

Each request asks code to compute something about the measure μ of a program p, and states it as an equation that every answer satisfies. Every row draws the same μ, a curve with two bumps. The top four rows ask for samplers, which return draws (dots), weighted draws (a stem's height is the weight), n ≥ 1 weighted draws from one run (a box), or one random step (an arrow). The bottom three ask for numbers: the mass z, a density against a reference measure ν (the dashed line), and a random estimate of that density.

ExactSampler p asks for draws distributed exactly as μ, so it applies only when μ has total weight one. NormalizedSampler p asks for draws from μ divided by its mass z, given z as an input. WeightedSampler p lets draws land anywhere, as long as their weights correct for where they land: the average of w · f(x) is the integral of f under μ. Importance sampling (Kahn and Marshall, Oper. Res. 1953) rests on this guarantee. WeightedSampler p (count := n) makes the same promise for n weighted draws (particles) that one run returns together, as in sequential Monte Carlo (Del Moral et al., JRSS B 2006): averaged over the particles, wᵢ · f(xᵢ) has mean equal to the integral of f. InvariantSampler p asks for one step of Markov chain Monte Carlo (Metropolis et al., J. Chem. Phys. 1953, and Hastings, Biometrika 1970), a random step that keeps μ in place: if x is distributed as μ normalized, so is the step's output.

The other rows are numbers that inference tactics ask for while they build samplers. A program's mass z is the integral of 1 under μ, and Mass p asks for code that computes it. Density p ν asks for code that computes a function d whose integral over every measurable set B, against a reference measure ν, is μ(B). Lebesgue measure, which gives each interval its length, is a common choice of ν. DensityEstimate p ν asks for random code whose mean at each x is d(x) (Lew et al., PLDI 2023, and Lew, MIT thesis 2025).

In the example, a sampler for linkage has to return K's mass as the weight, and the reason is Bayes' rule. The two records enter the program only through K's scores, so K's mass at a value of same is the probability of these records given that value: 3/16 with one patient and 1/4 with two. Weighting each draw of same by that probability moves the probability of one patient from the prior, 1/2, to the posterior, 3/7. With each value at prior 1/2, the expected weights are 3/32 with one patient and 1/8 with two. They sum to 7/32, the mass of linkage, and dividing by that total gives 3/7 and 4/7. A simpler sampler would normalize K, draw the names from it, and return weight 1. Its draws are correct for K only up to the factor 1/z, and z varies with same, so that factor cancels the evidence the records carry and the draws keep the prior. WeightedSampler allows no such factor. Both probabilities are ratios of expected weights, which a finite run of the sampler estimates.

In both panels the sampler draws same from its prior and the names from K normalized, and only the returned weight differs: K's mass at same on the left (red: 3/16 with one patient, 1/4 with two), weight 1 on the right. Each value of same gets a column as wide as its prior probability, 1/2, and as tall as the expected weight returned with it. Segments are the name pairs K enumerates, labeled in 64ths on the left. The scales differ: the left runs from 0 to 1/4, the right from 0 to 1. On the left, one patient holds 12 of 28 parts of the area, 3/7, the posterior. On the right both columns have height 1, so one patient holds 1/2, the prior.

Continuations

In the example, weightedBind splits linkage at its first draw, the draw of same, and asks for a sampler for flip half and for one for K at every value of same. exactBlock answers that second subgoal without splitting K further: it asks for K's mass and for exact draws from K normalized. Many inference tactics split a program where it draws a value, let x ← P, from the rest of the program, K, which may read x. K is the draw's continuation. What such a tactic's subgoals ask of K takes one of three directions.

An inference tactic splits a program at a draw of x from P and asks something of the rest of the program, the continuation K, in one of three directions. Forward, a subgoal asks for an answer about K at every x (weightedBind, prefixSMC, keepBlockWeighted, mhBlock). Back, K's mass at x enters the weight of x in three forms: exactly in exactBlock, as a factor of a density in collapsed (its answer is the prior's density times K's mass), and as an unbiased estimate in pmmh (a population's mean weight estimates K's mass). Down, K's integral, g(x) = ∫ f dK_x, becomes the integrand of the request about P (derive's ADEV plan, and the proofs of correctness of inference tactics at a draw). Back is Down with f = 1, since K's mass is the integral of 1 against K. Red arrows show what passes between P and K, and each card lists the inference tactics, or parts of derive, that ask in that direction.

Forward, a subgoal asks for an answer about K at every x. The subgoal next of weightedBind asks for a properly weighted sampler for K at every x. The code that answers it runs after the draw, and weightedBind returns the result with the product of both weights. prefixSMC asks the same of its step at every input, and mhBlock asks for K's density. Some steps keep part of the current state and draw a new part (the block) given the kept part. For such a step, keepBlockWeighted asks for a properly weighted sampler for the block at every kept value.

Back, a subgoal asks for K's mass at every x, and the inference tactic folds it into the weight of x. exactBlock and collapsed ask this way, as does the collapsed Gibbs sampler (Liu, JASA 1994). pmmh (particle marginal Metropolis–Hastings, Andrieu et al., JRSS B 2010) asks for a population sampler for K and uses the particles' mean weight as an unbiased estimate of K's mass, as pseudo-marginal methods do (Andrieu and Roberts, Ann. Stat. 2009).

Down, the inference tactic hands K's integral to the request about P, as the function P's answer must integrate. When derive estimates the derivative of an expected value, it asks this way, following ADEV (Lew et al., POPL 2023): it builds an estimator for K first, then one for P whose integrand is $g(x) = \int f , dK_x$. With $f = 1$, $g(x)$ is K's mass at x, so the back direction is the down direction with $f = 1$.

The down direction also explains why answers compose. Requests state their guarantees as integrals against the program's measure, and the measure of a bind is itself an integral (Kozen, JCSS 1985, and Ramsey and Pfeffer, POPL 2002): integrating f over the whole program is the same as integrating f over K at each x and then integrating the result over P. Write $\mu_P$ for P's measure, $K_x$ for K's measure at x, and $\mu_M$ for the measure of the whole program. For every nonnegative measurable $f$,

$$\int f \, d\mu_M = \int g \, d\mu_P, \qquad g(x) = \int f \, dK_x .$$

The figure below shows both sides of the equation for one small program: a Gaussian draw x followed by a Gaussian centered at x, with $f$ the indicator of landing above 1.

Integrating $f$ against the whole program's measure μ_M = $N(0, 2)$ and integrating $g$ against the first draw's measure μ_P = $N(0, 1)$ both give about 0.24, with $N(m, v)$ the Gaussian with mean $m$ and variance $v$. Sideways curves show K's measure at four values of $x$ (K_x = $N(x, 1)$ at $x = -1, 0, 1, 2$), with the red area above $y = 1$ equal to $g(x)$. $g(x)$ is the probability that the rest of the program lands above 1 once $x$ is drawn, a function of $x$ whose values at the four slices, rounded, are 0.02, 0.16, 0.50 and 0.84 along the red curve below. Black curves are measures, and red is $f$ and what integrating it gives.

The proof of correctness of weightedBind follows in three steps. P's answer returns a weighted draw (x, u), K's answer reads x and returns (y, v), and weightedBind returns (y, u · v):

$$\begin{aligned} \mathbb{E}[u\,v\,f(y)] &= \mathbb{E}[u\,g(x)] && \text{K's answer: } \mathbb{E}[v\,f(y) \mid x] = g(x) \\\ &= \textstyle\int g \, d\mu_P && \text{P's answer, with } g \text{ as its integrand} \\\ &= \textstyle\int f \, d\mu_M && \text{the measure of the bind} \end{aligned}$$

Tonelli's theorem (Tonelli, Rend. Lincei 1909) allows the change of order, because every integrand is nonnegative. These are the steps of the proof of weighted_bind in Problib, a Lean probability library included in the release, and each step reads an answer only through its request's equation. So any code that answers a subgoal will do, whoever wrote it: a case arm in the compiler program, another inference tactic, or derive.

A particle filter (Doucet et al., Stat. Comput. 2000) builds this way, from three cut_with lines. Its model tracks an object's position through two images. It draws a start position. At each image it keeps the current position, draws a new one near it (drift), and, for each of three pixels, draws whether the object covers the pixel and scores the pixel's observation (frame). The compiler program filter asks for a properly weighted population sampler for this model.

The compiler program filter asks for a particle filter for the tracking model. Under each line, shaded rows are the goals it opens, and a chip names each goal. Teal lists the inputs a goal ranges over, and its answer must hold at every value of them. A check marks a goal derive answered, with the code it delivered at the right. Red marks Z, the frame's mass at the new position, one exact answer that serves two subgoals.

cut_with prefixSMC runs sequential Monte Carlo over the model's prefixes, the model up to each image. At each image it resamples the particles, extends each one by a properly weighted sampler for the step, and, when a refresh is given, moves each one by an invariant sampler. In the extend case, cut_with importance (proposal := drift) gives a sampler for the new position only, the block, but the step returns both positions. keepBlockWeighted is registered with the library, so the goal's shape selects it, and cut_with applies it without the user naming it. It turns the sampler for the block into one for the whole step: it reads the kept position, draws the new one with its weight, and returns the pair with that weight. In the refresh case, cut_with mhBlock (proposal := nudge) (reference := lebesgue) asks for a Metropolis–Hastings step, with densities against Lebesgue measure. derive answers every other goal. Both cases ask back for the frame's mass Z at the new position, with each pixel's coverage summed out. The density for importance is 1 · Z, and the target density for mhBlock is the drift's Gaussian density times Z, so one exact answer serves two subgoals.

Limits

RePPL is research code.

• normalize requires finite, nonzero total weight at every input.
• Exact finite answers enumerate outcomes, whose number can grow exponentially with the program.
• Programs that draw from continuous distributions use Problib, a Lean probability library included in the release. Their answers can leave premises such as measurability or integrability for the user to prove.
• A program that returns a function or a suspended program has a quasi-Borel meaning (Heunen et al., LICS 2017), but derive answers no request about it yet. The meaning leaves out recursion and memoized random functions (Goodman et al., UAI 2008) that return functions or suspended programs.

Code

• RePPL.lean: library root.
• RePPL/Ch/: λCh, the language of measures.
• RePPL/Ag/: requests, answers, inference tactics, and derive.
• RePPL/Examples/Linkage.lean: the example and its numbers.
• lakefile.lean: build configuration.

References

Languages and semantics

• Dash et al., Affine monads and lazy structures for Bayesian programming, POPL 2023.
• de Bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indag. Math. 1972.
• Goodman et al., Church: a language for generative models, UAI 2008.
• Heunen et al., A convenient category for higher-order probability theory, LICS 2017.
• Kozen, A probabilistic PDL, JCSS 1985.
• Ramsey and Pfeffer, Stochastic lambda calculus and monads of probability distributions, POPL 2002.
• Staton, Commutative semantics for probabilistic programming, ESOP 2017.
• Tonelli, Sull'integrazione per parti, Rend. Lincei (5) 18, 1909.

Inference

• Andrieu and Roberts, The pseudo-marginal approach for efficient Monte Carlo computations, Ann. Stat. 2009.
• Andrieu et al., Particle Markov chain Monte Carlo methods, JRSS B 2010.
• Del Moral et al., Sequential Monte Carlo samplers, JRSS B 2006.
• Doucet et al., On sequential Monte Carlo sampling methods for Bayesian filtering, Stat. Comput. 2000.
• Hastings, Monte Carlo sampling methods using Markov chains and their applications, Biometrika 1970.
• Kahn and Marshall, Methods of reducing sample size in Monte Carlo computations, Oper. Res. 1953.
• Lew, Automatic integration and differentiation of probabilistic programs, MIT thesis 2025.
• Lew et al., Probabilistic programming with stochastic probabilities, PLDI 2023.
• Lew et al., ADEV: sound automatic differentiation of expected values of probabilistic programs, POPL 2023.
• Liu, The collapsed Gibbs sampler in Bayesian computations with applications to a gene regulation problem, JASA 1994.
• Liu and Chen, Sequential Monte Carlo methods for dynamic systems, JASA 1998.
• Metropolis et al., Equation of state calculations by fast computing machines, J. Chem. Phys. 1953.

Verification

• de Moura and Ullrich, The Lean 4 theorem prover and programming language, CADE 2021.
• Gordon et al., Edinburgh LCF: a mechanised logic of computation, LNCS 1979.

License

AGPL-3.0-or-later. See LICENSE.