pith. sign in

arxiv: 2606.05348 · v1 · pith:WPIRJR3Inew · submitted 2026-06-03 · 💻 cs.PL · cs.LO· stat.CO

Incremental Computation for Efficient Programmable Inference in Probabilistic Programs

Fabian Zaiser , Jack Czenszak , Martin C. Rinard , Vikash K. Mansinghka , Alexander K. Lew This is my paper

Pith reviewed 2026-06-28 02:30 UTC · model grok-4.3

classification 💻 cs.PL cs.LOstat.CO
keywords probabilistic programmingincremental computationMonte Carlo inferencedensity functionslambda calculuscorrectness proofsnonparametric modelsruntime optimization
0
0 comments X

The pith

Probabilistic programs compile to incremental densities that accelerate Monte Carlo inference algorithms including for nonparametric models.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how to compile expressive probabilistic programs into deterministic programs that compute density functions. These densities are then incrementalized using techniques from the incremental λ-calculus so that repeated evaluations during inference share expensive intermediate results instead of recomputing them. The resulting incremental densities speed up a range of Monte Carlo algorithms and work for nonparametric models. Separating the compilation step from the incrementalization step lets the authors prove correctness of each part independently with denotational logical relations. A Julia prototype achieves asymptotic runtime gains as dataset size grows across tested models and algorithms.

Core claim

Expressive probabilistic programs can be compiled to deterministic programs that compute their density functions, which can then be compositionally incrementalized using the incremental λ-calculus. The resulting incremental densities accelerate Monte Carlo inference algorithms, including for nonparametric models not well supported by existing systems. The decomposition into separate density and incrementalization steps permits modular denotational logical relations arguments for the correctness of each step independently.

What carries the argument

The incremental λ-calculus technique for compositionally incrementalizing functional programs, applied after compiling probabilistic programs to deterministic density functions.

If this is right

  • Incremental densities accelerate a broad range of Monte Carlo inference algorithms.
  • The method supports nonparametric models not well supported by existing systems.
  • Decomposition into density and incrementalization steps enables modular correctness proofs via logical relations.
  • Asymptotic runtime improvements occur in the size of the dataset on a range of models and inference algorithms.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The modular correctness technique could transfer to incrementalization in other probabilistic programming systems.
  • Efficiency gains might allow scaling inference to datasets larger than those feasible with current ad-hoc methods.
  • The compilation-plus-incrementalization split could be combined with other program transformations such as automatic differentiation.

Load-bearing premise

Expressive probabilistic programs can be compiled to deterministic programs that compute their density functions, and the incremental λ-calculus applies compositionally to these without breaking the semantics needed for inference.

What would settle it

A case where running the incrementalized density computation produces different inference results from the non-incremental version, or where runtime fails to improve asymptotically with dataset size on the range of models tested in the prototype.

Figures

Figures reproduced from arXiv: 2606.05348 by Alexander K. Lew, Fabian Zaiser, Jack Czenszak, Martin C. Rinard, Vikash K. Mansinghka.

Figure 1
Figure 1. Figure 1: Overview of our staged approach to incremental density computation for programmable inference. [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Example: modeling and inference for a 2D Gaussian mixture model with incremental densities. [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Syntax of our languages 𝜆gen, 𝜆inc, 𝜆core. Labels ℓ are from a countable set L. ⟦𝜎 →𝜅 𝜏⟧ = ⟦𝜎⟧⇒ ⟦𝜏⟧(where ⇒ constructs the semantic function space). For example, we have 𝑦 : R, 𝑧 : N ⊢ 𝜆𝑥. 𝑥 < 𝑦 : R →R B because the function 𝜆𝑥. 𝑥 < 𝑦 closes over the variable 𝑦 of type R. 4 (It is admittedly unusual to track this information in the type of a function. More details will be provided in Section 4, but the int… view at source ↗
Figure 4
Figure 4. Figure 4: Selected Typing Rules. We write Γ|FV(𝑡) for the restriction of Γ to the free variables of 𝑡. The 𝜆inc Calculus. As in 𝜆gen, 𝜆inc function types 𝜎 →𝜅 𝜏 are annotated with captured environment types 𝜅. But in 𝜆inc, the semantics of a function tracks how it depends on its closed-over data: ⟦𝜎 →𝜅 𝜏⟧ = ⟦𝜅⟧× (⟦𝜅⟧× ⟦𝜎⟧⇒ ⟦𝜏⟧) The semantics of function abstraction and application explicitly manipulate these closure… view at source ↗
Figure 5
Figure 5. Figure 5: Semantics of 𝜆inc (selected rules). ⟦𝜏 → 𝜏 ′ ⟧ = ⟦𝜏⟧⇒ ⟦𝜏 ′ ⟧ ⟦Upd(𝜏; 𝜏 ′ )⟧ = ⟦𝜏⟧ + ⇒ ⟦𝜏 ′⟧ where 𝑆 + = Ð∞ 𝑛=1 𝑆 𝑛 ⟦Sub{ℓ1 : 𝜏1, . . . , ℓ𝑛 : 𝜏𝑛 }⟧ = {𝑟 : 𝑆 → Ð𝑛 𝑖=1 ⟦𝜏𝑖⟧ | 𝑆 ⊆ {ℓ1, . . . , ℓ𝑛 }, 𝑟(ℓ𝑖) ∈ ⟦𝜏𝑖⟧} ⟦mkUpd(𝑠;𝑡)⟧ (𝛾) = ( (𝑥1, . . . , 𝑥𝑛) ∈ ⟦𝜏⟧ 𝑛 ) ↦→ 𝑦𝑛 where cache1 = ⟦𝑠⟧ (𝛾), 𝑓 = ⟦𝑡⟧ (𝛾) and (𝑦𝑖 ,cache𝑖+1) = 𝑓 (𝑥𝑖 ,cache𝑖) for 𝑖 = 1, . . . , 𝑛 ⟦𝑠.apply(𝑡)⟧ (𝛾) = (𝑓 (𝑥 ∈ ⟦𝜏⟧ 1 ), (xs ∈ ⟦𝜏⟧ 𝑛 ) ↦→… view at source ↗
Figure 6
Figure 6. Figure 6: Semantics of 𝜆core (selected rules). 3 Density Transformation The first step in our pipeline is to translate a probabilistic 𝜆gen program into a deterministic 𝜆inc program that computes its trace distribution’s density function. This isolates all probabilistic reasoning from incrementalization, which we discuss in Section 4. 3.1 Densities of Traced Programs with Name Generation Given a program of type P 𝜎 … view at source ↗
Figure 7
Figure 7. Figure 7: Computing the density of a probabilistic program. In this figure, [PITH_FULL_IMAGE:figures/full_fig_p012_7.png] view at source ↗
Figure 9
Figure 9. Figure 9: Density transformation from 𝜆gen to 𝜆inc on types (selected rules). W{𝑐} = 𝑐inc W{ret 𝑡 } = 𝝀(tr, U). (W{𝑡 } , 1) W{sample 𝑡 } = 𝝀(tr, U). (tr, (W{𝑡 } (tr, U)).2) W{𝑡 @ ℓ } = 𝝀(tr, U).W{𝑡 } (tr.ℓ, U) W{𝑥 ← 𝑡1;𝑡2} = 𝝀(tr, U). (𝑥,𝑤1) := W{𝑡1} (tr|𝐿1 , U); (𝑦,𝑤2) := W{𝑡2} (tr|𝐿2 , U ∪ names(tr|𝐿1 )); (𝑦,𝑤1 · 𝑤2) where 𝑡1 : P {ℓ : 𝜎ℓ | ℓ ∈ 𝐿1} 𝜏1 and 𝑡2 : P {ℓ : 𝜎 ′ ℓ | ℓ ∈ 𝐿2} 𝜏2 W  for 𝑥 inRange 𝑑 : Dist N … view at source ↗
Figure 10
Figure 10. Figure 10: Density transformation from 𝜆gen to 𝜆inc on terms (selected rules). Intuitively, the density program works by executing the same logic as the original probabilistic program. When a primitive random choice is encountered, we look up the corresponding value in the trace. We use the primitive distribution’s built-in density (passing in the choice’s value and the current support set U of names) to compute its… view at source ↗
Figure 11
Figure 11. Figure 11: Incrementalizing transformation I{−} from 𝜆inc to 𝜆core on types and change types Δ(−). 𝜋Γ↦→𝑥 : CtxType(Γ) → 𝜎 (assuming (𝑥 : 𝜎) ∈ Γ) 𝜋Γ,𝑥:𝜏↦→𝑥 = 𝝀(_, 𝑥). 𝑥 𝜋Γ,𝑦:𝜏↦→𝑥 = 𝝀(𝛾, _). 𝜋Γ↦→𝑥 (𝛾) if 𝑦 ≠ 𝑥 𝜋Γ↦→xs : CtxType(Γ) → CtxType(Γ|xs) 𝜋•↦→∅ = 𝝀_. {} 𝜋(Γ,𝑥:𝜏 ) ↦→xs = ( 𝝀(𝛾, 𝑣). (𝜋Γ↦→xs\{𝑥 } (𝛾), 𝑣) if 𝑥 ∈ xs 𝝀(𝛾, _). 𝜋Γ↦→xs(𝛾) otherwise [PITH_FULL_IMAGE:figures/full_fig_p016_11.png] view at source ↗
Figure 14
Figure 14. Figure 14: Incrementalizing transformation from 𝜆inc to 𝜆core on terms (selected rules). The transformation rule for variables ( [PITH_FULL_IMAGE:figures/full_fig_p016_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Pseudocode for incrementalizing simplified for-expressions (without accumulators or [PITH_FULL_IMAGE:figures/full_fig_p017_15.png] view at source ↗
Figure 17
Figure 17. Figure 17: Logical relation between 𝜆inc and 𝜆core (selected rules). tplΓ : ⟦Γ⟧→ ⟦CtxType(Γ)⟧ tpl• (∅) = {}, tplΓ,𝑥:𝜏 (𝛾) = (tplΓ (𝛾 \ {𝑥}),𝛾 (𝑥)) ctxΓ : ⟦CtxType(Γ)⟧→ ⟦Γ⟧ ctx• ({}) = ∅, ctxΓ,𝑥:𝜏 (𝛾) = ctxΓ (𝜋1 (𝛾)) [𝑥 ↦→ 𝜋2 (𝛾)] [PITH_FULL_IMAGE:figures/full_fig_p018_17.png] view at source ↗
Figure 19
Figure 19. Figure 19: Representative log-log scaling plots for individual MCMC moves. Although our approach incurs [PITH_FULL_IMAGE:figures/full_fig_p020_19.png] view at source ↗
Figure 20
Figure 20. Figure 20: Linear scaling plots for entire MCMC parameter sweeps. [PITH_FULL_IMAGE:figures/full_fig_p020_20.png] view at source ↗
Figure 21
Figure 21. Figure 21: List of constant symbols (𝑐 : typeOf(𝑐)) ∈ Constants. Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 238. Publication date: June 2026 [PITH_FULL_IMAGE:figures/full_fig_p028_21.png] view at source ↗
Figure 22
Figure 22. Figure 22: Syntactic sugar B is ground N is ground R is ground Name is ground 𝜎 is ground 𝜎 ′ is ground 𝜎 × 𝜎 ′ is ground 𝜎 is ground List 𝜎 is ground 𝜎 is ground NameMap 𝜎 is ground 𝜎 is ground 𝜅 is type Dist𝜅 𝜎 is type 𝜎 is ground 𝜏 is type 𝜅 is type P𝜅 𝜎 𝜏 is type 𝜎 is type 𝜏 is type 𝜅 is type 𝜎 →𝜅 𝜏 is type 𝐿 ⊆ L finite 𝜎𝑙 is ground for all 𝑙 ∈ 𝐿 {𝑙 : 𝜎𝑙 | 𝑙 ∈ 𝐿} is ground [PITH_FULL_IMAGE:figures/full_fig_p029… view at source ↗
Figure 23
Figure 23. Figure 23: Restrictions on ground types. Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 238. Publication date: June 2026 [PITH_FULL_IMAGE:figures/full_fig_p029_23.png] view at source ↗
Figure 24
Figure 24. Figure 24: Typing Rules. We write CtxType(Γ) for the product of the types appearing in Γ; Γ|𝑆 for the restriction of Γ to the variables in 𝑆; and FV(𝑡) for the set of free variables in 𝑡. Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 238. Publication date: June 2026 [PITH_FULL_IMAGE:figures/full_fig_p030_24.png] view at source ↗
Figure 25
Figure 25. Figure 25: Type semantics for 𝜆inc and 𝜆core. Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 238. Publication date: June 2026 [PITH_FULL_IMAGE:figures/full_fig_p031_25.png] view at source ↗
Figure 26
Figure 26. Figure 26: Term semantics for 𝜆inc and 𝜆core. Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 238. Publication date: June 2026 [PITH_FULL_IMAGE:figures/full_fig_p032_26.png] view at source ↗
Figure 27
Figure 27. Figure 27: Semantics of 𝜆gen types as 𝜈Qbs objects. Definition A.8 (Rose trees). Let Ω = [0, 1] N ∗ denote the quasi-Borel space of rose trees [15, §5.4.1] and take 𝜇Ω to be the uniform probability distribution on Ω. The space Ω extends to a functor: Ω(𝑈 ) = n 𝜔 ∈ Ω | ∀𝜌 ∈ N ∗ , 𝜔(𝜌) ∈ 𝑈 o Definition A.9 (Probability monad). The probability monad on 𝜈Qbs is given by the quadruple (P, 𝜂, 𝜇, 𝜏), where the endofunctor … view at source ↗
Figure 28
Figure 28. Figure 28: Semantics of 𝜆gen terms as 𝜈Qbs morphisms. For readability, we present the Set concretization of each interpretation, ⟦Γ ⊢ 𝑡 : 𝜏⟧ = ⟦Γ ⊢ 𝑡 : 𝜏⟧[0,1] . In general, ⟦Γ ⊢ 𝑡 : 𝜏⟧𝑈 = ⟦Γ ⊢ 𝑡 : 𝜏⟧|⟦Γ⟧(𝑈 ) . Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 238. Publication date: June 2026 [PITH_FULL_IMAGE:figures/full_fig_p036_28.png] view at source ↗
Figure 29
Figure 29. Figure 29: Density transformation from 𝜆gen to 𝜆inc on types. W{𝑥} = 𝑥 W{𝑐} = 𝑐inc W{ret 𝑡 } = 𝝀(tr, U). (W{𝑡 } , 1) W{𝑥 ← 𝑡1;𝑡2} = 𝝀(tr, U). (𝑥,𝑤1) := W{𝑡1} (tr|𝐿1 , U); (𝑦,𝑤2) := W{𝑡2} (tr|𝐿2 , U ∪ names(tr|𝐿1 )); (𝑦,𝑤1 · 𝑤2) where 𝑡1 : P {ℓ : 𝜎ℓ | ℓ ∈ 𝐿1} 𝜏1 and 𝑡2 : P {ℓ : 𝜎 ′ ℓ | ℓ ∈ 𝐿2} 𝜏2 W{sample 𝑡 } = 𝝀(tr, U). (tr, (W{𝑡 } (tr, U)).2) W{𝑡 @ ℓ } = 𝝀(tr, U).W{𝑡 } (tr.ℓ, U) W  for 𝑥 inRange 𝑑 : Dist N with 𝑧 … view at source ↗
Figure 30
Figure 30. Figure 30: Density transformation from 𝜆gen to 𝜆inc on terms. ⟦freshinc⟧ ( (𝛾, 𝑑)) = [PITH_FULL_IMAGE:figures/full_fig_p037_30.png] view at source ↗
Figure 32
Figure 32. Figure 32: The logical relation R𝜏 . Case: Return Suppose Γ ⊢ ret 𝑡 : PCtxType(Γ|FV(𝑡 ) ) {} 𝜏 and let (𝜇, 𝑓 ) = ⟦ret 𝑡⟧ (𝛾1) and (𝛾, ⟨𝑔,𝑤⟩) = ⟦W{ret 𝑡 }⟧ (𝛾2). By the inductive hypothesis, (𝑡1, 𝑡2) := (⟦𝑡⟧ (𝛾1), ⟦W{𝑡 }⟧ (𝛾2)) ∈ R𝜏 . • For any ( (𝑠1,𝑈1), (𝑠2,𝑈2)) ∈ R{ }×NameSet, we have (𝑓 (𝑠1), 𝑔(𝛾, 𝑠2,𝑈2)) = (𝑡1, 𝑡2) ∈ R𝜏 . • Recall 𝜇 = 𝛿⟦{ }⟧. For 𝜌 = ⟦{}⟧and any 𝑈 , it follows that  d𝛿⟦{}⟧ d𝜈 {} 𝑈  (𝜌) = 1 = 𝑤… view at source ↗
Figure 33
Figure 33. Figure 33: Incrementalizing transformation from 𝜆inc to 𝜆core on types. C Incrementalizing Transformation: Full Definition and Correctness The full type and term translations are given in Figs. 33 and 34, and the full version of the for￾expression translation is given in [PITH_FULL_IMAGE:figures/full_fig_p046_33.png] view at source ↗
Figure 34
Figure 34. Figure 34: Incrementalizing transformation from 𝜆inc to 𝜆core on terms. It satisfies the invariant that Γ ⊢ 𝑡 : 𝜏 in 𝜆inc implies I{Γ} ⊢ IΓ {𝑡 } : I{𝜏 } × Upd(Δ(CtxType(Γ)); Δ(𝜏)) in 𝜆core. Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 238. Publication date: June 2026 [PITH_FULL_IMAGE:figures/full_fig_p047_34.png] view at source ↗
Figure 35
Figure 35. Figure 35: Incrementalizing transformation from 𝜆inc to 𝜆core on for-expressions. For simplicity, the figure only handles modifications of list elements, not insertions or deletions, and we further assume that each collection expression 𝑦𝑗 does not depend on the loop variable 𝑥 or the accumulator 𝑧, so it can be typed in just Γ, matching the cache type declared for collectionUpds𝑗 . Proc. ACM Program. Lang., Vol. 10… view at source ↗
Figure 36
Figure 36. Figure 36: Relation of valid changes. R𝜎 = {(𝑥, 𝑥′ ) | 𝑥 = 𝑥 ′ } for ground types 𝜎 R𝜎×𝜏 = {( (𝑥, 𝑦), (𝑥 ′ , 𝑦′ )) | (𝑥, 𝑥′ ) ∈ R𝜎 ∧ (𝑦, 𝑦′ ) ∈ R𝜏 } RList 𝜎 = {(xs, xs′ ) | length(xs) = length(xs′ ) ∧ ∀𝑖 < length(xs). (xs[𝑖], xs′ [𝑖]) ∈ R𝜎 } RNameMap 𝜎 = {(𝑚,𝑚′ ) | keys(𝑚) = keys(𝑚 ′ ) ∧ ∀𝑛 ∈ keys(𝑚). (𝑚(𝑛),𝑚′ (𝑛)) ∈ R𝜎 } R{ℓ1:𝜏1,...,ℓ𝑛:𝜏𝑛 } = {(𝑟, 𝑟′ ) | ∀𝑖 ∈ {1, . . . , 𝑛}. (𝑟(ℓ𝑖), 𝑟′ (ℓ𝑖)) ∈ R𝜏𝑖 } R𝜎→𝜅𝜏 = {( (env… view at source ↗
Figure 37
Figure 37. Figure 37: Logical relation between 𝜆inc and 𝜆core. We abbreviate ⟦I{𝑡 }⟧1 := 𝜋1 ◦ ⟦I{𝑡 }⟧, ⟦𝑡⟧tpl := ⟦𝑡⟧◦ ctxΓ, and ⟦I{𝑡 }⟧2 := 𝜋2 ◦ ⟦I{𝑡 }⟧. Lemma C.3 (Fundamental Lemma). Assume Γ ⊢ 𝑡 : 𝜏 in 𝜆inc, and thus I{Γ} ⊢ IΓ {𝑡 } : I{𝜏 } × Upd(Δ(CtxType(Γ)); Δ(𝜏)) in 𝜆core. Then for all (𝛾,𝛾∗) ∈ RΓ, we have (⟦𝑡⟧ (𝛾), ⟦I{𝑡 }⟧1 (𝛾∗)) ∈ R𝜏 and ⟦I{𝑡 }⟧2 (𝛾∗) ∈ U⟦𝑡⟧tpl ,tplΓ (𝛾 ) CtxType(Γ){𝜏 Proof. By induction on the typing … view at source ↗
read the original abstract

Inference in probabilistic programs generally requires evaluating many possible program executions to find those of high posterior density. To scale inference to large datasets, it is crucial that expensive intermediate results are shared across these many evaluations, rather than recomputed from scratch. This paper presents a new approach to realizing this sharing, based on \textit{incremental computation}, a technique for efficiently recomputing (deterministic) program outputs when program inputs change. First, we show how expressive probabilistic programs can be compiled to deterministic ones that compute their density functions. Then, building on the incremental $\lambda$-calculus, we develop a general technique for compositionally incrementalizing expressive functional programs, and apply it to these densities. The resulting incremental densities can be used to accelerate a broad range of Monte Carlo inference algorithms, including for nonparametric models not well supported by existing systems. Furthermore, our decomposition of incremental density computation into separate density and incrementalization steps allows for modular reasoning about correctness -- a key pain point in existing systems, where ad-hoc incrementalization features are a known source of soundness bugs. We develop denotational logical relations arguments for the correctness of each step independently, and implement the approach in a Julia prototype, finding that it leads to asymptotic runtime improvements in the size of the dataset on a range of models and inference algorithms.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper claims that expressive probabilistic programs can be compiled to deterministic programs computing their density functions; these densities can then be incrementalized compositionally via the incremental λ-calculus. The resulting incremental densities accelerate Monte Carlo inference algorithms (including for nonparametric models). The approach decomposes density computation and incrementalization, enabling independent denotational logical-relations proofs of correctness for each step; a Julia prototype is reported to deliver asymptotic runtime improvements with dataset size on a range of models and algorithms.

Significance. If the compilation and incrementalization steps are shown to preserve the necessary semantics, the work supplies a modular, formally justified route to efficient sharing in programmable inference. The separation into independently verifiable phases directly addresses known soundness risks in ad-hoc incremental features of existing systems, and the claimed applicability to nonparametric models would fill a gap in current tooling.

minor comments (2)
  1. The abstract states that the Julia prototype yields 'asymptotic runtime improvements in the size of the dataset'; the full manuscript should include explicit big-O statements or scaling plots with dataset size as the independent variable to make this claim precise.
  2. The logical-relations arguments are described at a high level; if the paper contains the full definitions of the relations and the key lemmas, they should be cross-referenced to the relevant theorems so readers can locate the modular proofs without searching the text.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary, significance assessment, and recommendation to accept the paper.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's core derivation decomposes incremental density computation into two independent steps—compiling probabilistic programs to deterministic density functions, then applying a general incrementalization technique from the incremental λ-calculus—with separate denotational logical-relations arguments supplied for the correctness of each step. No self-definitional reductions, fitted inputs renamed as predictions, or load-bearing self-citations appear in the stated approach; the Julia prototype supplies external empirical validation of asymptotic improvements. The derivation chain is therefore self-contained against external benchmarks and does not reduce to its inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard assumptions from programming languages and incremental computation literature, without introducing new free parameters or entities. The central technique builds on the incremental λ-calculus as a given.

axioms (1)
  • domain assumption The incremental λ-calculus provides a general technique for compositionally incrementalizing expressive functional programs.
    Invoked as the basis for the incrementalization step applied to the compiled densities.

pith-pipeline@v0.9.1-grok · 5778 in / 1326 out tokens · 49527 ms · 2026-06-28T02:30:38.839456+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

52 extracted references · 27 canonical work pages

  1. [1]

    Umut A. Acar. 2005.Self-Adjusting Computation. Ph. D. Dissertation. Carnegie Mellon University

    2005

  2. [2]

    Umut A. Acar. 2009. Self-adjusting computation: (an overview). InProceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2009, Savannah, GA, USA, January 19-20, 2009, Germán Puebla and Germán Vidal (Eds.). ACM, 1–6. doi:10.1145/1480945.1480946

    work page doi:10.1145/1480945.1480946 2009

  3. [3]

    Christophe Andrieu and Gareth O. Roberts. 2009. The pseudo-marginal approach for efficient Monte Carlo computations. The Annals of Statistics37, 2 (2009), 697–725. doi:10.1214/07-AOS574

    work page doi:10.1214/07-aos574 2009

  4. [4]

    John Baez and Alexander Hoffnung. 2011. Convenient categories of smooth spaces.Trans. Amer. Math. Soc.363, 11 (2011), 5789–5825

    2011

  5. [5]

    Becker, Mathieu Huot, George Matheos, Xiaoyan Wang, Karen Chung, Colin Smith, Sam Ritchie, Rif A

    McCoy R. Becker, Mathieu Huot, George Matheos, Xiaoyan Wang, Karen Chung, Colin Smith, Sam Ritchie, Rif A. Saurous, Alexander K. Lew, Martin C. Rinard, and Vikash K. Mansinghka. 2026. Probabilistic Programming with Vectorized Programmable Inference.Proc. ACM Program. Lang.10, POPL (2026), 2523–2554. doi:10.1145/3776729

    work page doi:10.1145/3776729 2026

  6. [6]

    Blei, Andrew Y

    David M. Blei, Andrew Y. Ng, and Michael I. Jordan. 2003. Latent Dirichlet allocation.Journal of Machine Learning Research3, Jan (2003), 993–1022

    2003

  7. [7]

    Markus Böck and Jürgen Cito. 2025. Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops.CoRRabs/2508.20922 (2025). arXiv:2508.20922 doi:10.48550/ARXIV.2508.20922

    work page doi:10.48550/arxiv.2508.20922 2025

  8. [8]

    George E. P. Box and George C. Tiao. 1968. A Bayesian approach to some outlier problems.Biometrika55, 1 (1968), 119–129

    1968

  9. [9]

    Giarrusso, Tillmann Rendel, and Klaus Ostermann

    Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, and Klaus Ostermann. 2014. A theory of changes for higher-order languages: incrementalizing 𝜆-calculi by static differentiation. InACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014, Michael F. P. O’Boyle and Keshav Pingali (Eds....

    work page doi:10.1145/2594291.2594304 2014

  10. [10]

    Simon Castellan and Hugo Paquet. 2019. Probabilistic Programming Inference via Intensional Semantics. InProgram- ming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings (Lecture Notes ...

    work page doi:10.1007/978-3-030-17184-1_12 2019

  11. [11]

    Cusumano-Towner

    Marco F. Cusumano-Towner. 2020.Gen: a high-level programming platform for probabilistic inference. Ph. D. Dissertation. Massachusetts Institute of Technology

    2020

  12. [12]

    Cusumano-Towner, Benjamin Bichsel, Timon Gehr, Martin T

    Marco F. Cusumano-Towner, Benjamin Bichsel, Timon Gehr, Martin T. Vechev, and Vikash K. Mansinghka. 2018. Incremental inference for probabilistic programs. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018. ACM, 571–585. doi:10.1145/3192366.3192399

    work page doi:10.1145/3192366.3192399 2018

  13. [13]

    Cusumano-Towner, Alexander K

    Marco F. Cusumano-Towner, Alexander K. Lew, and Vikash K. Mansinghka. 2020. Automating Involutive MCMC using Probabilistic and Differentiable Programming. arXiv:2007.09871 [stat.CO] https://arxiv.org/abs/2007.09871

    arXiv 2020

  14. [14]

    Cusumano-Towner, Feras A

    Marco F. Cusumano-Towner, Feras A. Saad, Alexander K. Lew, and Vikash K. Mansinghka. 2019. Gen: a general-purpose probabilistic programming system with programmable inference. InProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, Kathryn S. McKinley and Kathleen F...

    work page doi:10.1145/3314221.3314642 2019

  15. [15]

    Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton. 2023. Affine monads and lazy structures for Bayesian programming.Proc. ACM Program. Lang.7, POPL (2023), 1338–1368. doi:10.1145/3571239

    work page doi:10.1145/3571239 2023

  16. [16]

    Jean Diebolt and Christian P. Robert. 1994. Estimation of finite mixture distributions through Bayesian sampling. Journal of the Royal Statistical Society: Series B (Methodological)56, 2 (1994), 363–375

    1994

  17. [17]

    Hong Ge, Kai Xu, and Zoubin Ghahramani. 2018. Turing: A Language for Flexible Probabilistic Inference. InProceedings of the Twenty-First International Conference on Artificial Intelligence and Statistics (AISTATS) (Proceedings of Machine Learning Research, Vol. 84). PMLR, 1682–1690. Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 238. Publication dat...

    2018

  18. [18]

    Giarrusso, Yann Régis-Gianas, and Philipp Schuster

    Paolo G. Giarrusso, Yann Régis-Gianas, and Philipp Schuster. 2019. Incremental𝜆-Calculus in Cache-Transfer Style - Static Memoization by Program Transformation. InProgramming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czec...

    work page doi:10.1007/978-3-030-17184-1_20 2019

  19. [19]

    Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S

    Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael W. Hicks, and David Van Horn. 2015. Incremental computation with names. InProceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, Octob...

    work page doi:10.1145/2814270.2814305 2015

  20. [20]

    Hammer, Yit Phang Khoo, Michael Hicks, and Jeffrey S

    Matthew A. Hammer, Yit Phang Khoo, Michael Hicks, and Jeffrey S. Foster. 2014. Adapton: composable, demand-driven incremental computation. InACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014, Michael F. P. O’Boyle and Keshav Pingali (Eds.). ACM, 156–166. doi:10.1145/2594291.2594324

    work page doi:10.1145/2594291.2594324 2014

  21. [21]

    Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. 2017. A convenient category for higher-order probability theory. In32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017. IEEE Computer Society, 1–12. doi:10.1109/LICS.2017.8005137

    work page doi:10.1109/lics.2017.8005137 2017

  22. [22]

    Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang. 2020. Towards Verified Stochastic Variational Inference for Probabilistic Programs.Proc. ACM Program. Lang.4, POPL (2020), 16:1–16:33. doi:10.1145/3371084

    work page doi:10.1145/3371084 2020

  23. [23]

    Lew, Marco F

    Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michael Carbin, and Vikash K. Mansinghka. 2020. Trace types and denotational semantics for sound programmable inference in probabilistic languages.Proc. ACM Program. Lang.4, POPL (2020), 19:1–19:32. doi:10.1145/3371087

    work page doi:10.1145/3371087 2020

  24. [24]

    Jianlin Li, Leni Aniva, Pengyuan Shi, and Yizhou Zhang. 2023. Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference.Proc. ACM Program. Lang.7, POPL (2023), 1454–1482. doi:10. 1145/3571243

    2023

  25. [25]

    Sangho Lim, Hyoungjin Lim, Wonyeol Lee, Xavier Rival, and Hongseok Yang. 2026. Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation.Proc. ACM Program. Lang.10, POPL (2026), 597–627. doi:10.1145/3776663

    work page doi:10.1145/3776663 2026

  26. [26]

    1998.Categories for the Working Mathematician(2nd ed.)

    Saunders Mac Lane. 1998.Categories for the Working Mathematician(2nd ed.). Graduate Texts in Mathematics, Vol. 5. Springer

    1998

  27. [27]

    1994.Sheaves in Geometry and Logic: A First Introduction to Topos Theory

    Saunders Mac Lane and Ieke Moerdijk. 1994.Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer

    1994

  28. [28]

    Vikash Mansinghka, Daniel Selsam, and Yura N. Perov. 2014. Venture: a higher-order probabilistic programming platform with programmable inference.CoRRabs/1404.0099 (2014). arXiv:1404.0099 http://arxiv.org/abs/1404.0099

    Pith/arXiv arXiv 2014

  29. [29]

    Mansinghka, Ulrich Schaechtle, Shivam Handa, Alexey Radul, Yutian Chen, and Martin C

    Vikash K. Mansinghka, Ulrich Schaechtle, Shivam Handa, Alexey Radul, Yutian Chen, and Martin C. Rinard. 2018. Probabilistic programming with programmable inference. InProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, Jeffrey S. Foster and Dan Grossman (Eds....

    work page doi:10.1145/3192366.3192409 2018

  30. [30]

    Moss, and Sam Staton

    Cristina Matache, Sean K. Moss, and Sam Staton. 2022. Concrete categories and higher-order recursion. In37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022. ACM, 57:1–57:14. doi:10.1145/3531130.3533370

    work page doi:10.1145/3531130.3533370 2022

  31. [31]

    Lew, Matin Ghavamizadeh, Stuart Russell, Marco F

    George Matheos, Alexander K. Lew, Matin Ghavamizadeh, Stuart Russell, Marco F. Cusumano-Towner, and Vikash Mansinghka. 2021. Transforming Worlds: Automated Involutive MCMC for Open-Universe Probabilistic Models. In Third Symposium on Advances in Approximate Bayesian Inference. https://openreview.net/forum?id=8Itm8dQnJRc

    2021

  32. [32]

    Kazutaka Matsuda, Samantha Frohlich, Meng Wang, and Nicolas Wu. 2023. Embedding by Unembedding.Proc. ACM Program. Lang.7, ICFP (2023), 1–47. doi:10.1145/3607830

    work page doi:10.1145/3607830 2023

  33. [33]

    Brian Milch and Stuart Russell. 2006. General-Purpose MCMC inference over relational structures. InProceedings of the Twenty-Second Conference on Uncertainty in Artificial Intelligence (UAI’06). AUAI Press, 349–358

    2006

  34. [34]

    Miller and Matthew T

    Jeffrey W. Miller and Matthew T. Harrison. 2018. Mixture models with a prior on the number of components.J. Amer. Statist. Assoc.113, 521 (2018), 340–356

    2018

  35. [35]

    Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads. InProceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS 1989). IEEE Computer Society, 14–23. doi:10.1109/LICS.1989.39155

    work page doi:10.1109/lics.1989.39155 1989

  36. [36]

    Eugenio Moggi. 1991. Notions of computation and monads.Information and computation93, 1 (1991), 55–92

    1991

  37. [37]

    Akimasa Morihata. 2020. Short Cut to Incremental Typed Functional Programs (Extended Abstract). InWPTE 2020: 7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation. http://maude.ucm.es/ wpte20/papers/WPTE_2020_morihata.pdf Informal proceedings

    2020

  38. [38]

    Radford M. Neal. 2000. Markov chain sampling methods for Dirichlet process mixture models.Journal of computational and graphical statistics9, 2 (2000), 249–265. Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 238. Publication date: June 2026. Incremental Computation for Efficient Programmable Inference in Probabilistic Programs 238:25

    2000

  39. [39]

    Daniel Ritchie, Andreas Stuhlmüller, and Noah D. Goodman. 2016. C3: Lightweight Incrementalized MCMC for Probabilistic Programs using Continuations and Callsite Caching. InProceedings of the 19th International Conference on Artificial Intelligence and Statistics, AISTATS 2016, Cadiz, Spain, May 9-11, 2016 (JMLR Workshop and Conference Proceedings, Vol. 51...

    2016

  40. [40]

    Marcin Sabok, Sam Staton, Dario Stein, and Michael Wolman. 2021. Probabilistic programming semantics for name generation.Proc. ACM Program. Lang.5, POPL (2021), 1–29. doi:10.1145/3434292

    work page doi:10.1145/3434292 2021

  41. [41]

    Moss, Chris Heunen, and Zoubin Ghahramani

    Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani. 2018. Denotational validation of higher-order Bayesian inference.Proc. ACM Program. Lang.2, POPL (2018), 60:1–60:29. doi:10.1145/3158148

    work page doi:10.1145/3158148 2018

  42. [42]

    Steven L. Scott. 2002. Bayesian methods for Hidden Markov Models: Recursive computing in the 21st century.J. Amer. Statist. Assoc.97, 457 (2002), 337–351

    2002

  43. [43]

    Sam Staton. 2017. Commutative Semantics for Probabilistic Programming. InProgramming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 (Lecture Notes in Computer Science, Vol. 10201). Springer, 855–879. doi:10.1007/978-3-662-54434-1_32

    work page doi:10.1007/978-3-662-54434-1_32 2017

  44. [44]

    Joseph Tassarotti and Jean-Baptiste Tristan. 2023. Verified Density Compilation for a Probabilistic Programming Language.Proc. ACM Program. Lang.7, PLDI (2023), 615–637. doi:10.1145/3591245

    work page doi:10.1145/3591245 2023

  45. [45]

    Arora, Yucen Lily Li, Kinjal Divesh Shah, David Noursi, Michael Tingley, Narjes Torabi, Sepehr Masouleh, Eric Lippert, and Erik Meijer

    Nazanin Khosravani Tehrani, Nimar S. Arora, Yucen Lily Li, Kinjal Divesh Shah, David Noursi, Michael Tingley, Narjes Torabi, Sepehr Masouleh, Eric Lippert, and Erik Meijer. 2020. Bean Machine: A Declarative Probabilistic Programming Language For Efficient Programmable Inference. InInternational Conference on Probabilistic Graphical Models, PGM 2020, 23-25...

    2020

  46. [46]

    Matthijs Vákár, Ohad Kammar, and Sam Staton. 2019. A domain theory for statistical probabilistic programming.Proc. ACM Program. Lang.3, POPL (2019), 36:1–36:29. doi:10.1145/3290349

    work page doi:10.1145/3290349 2019

  47. [47]

    Matthijs Vákár and Luke Ong. 2018. On s-finite measures and kernels. arXiv:1810.01837 https://arxiv.org/abs/1810.01837

    Pith/arXiv arXiv 2018

  48. [48]

    Di Wang, Jan Hoffmann, and Thomas Reps. 2021. Sound Probabilistic Inference via Guide Types. InProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021. ACM, 788–803. doi:10.1145/3453483.3454077

    work page doi:10.1145/3453483.3454077 2021

  49. [49]

    Lingfeng Yang, Pat Hanrahan, and Noah D. Goodman. 2014. Generating Efficient MCMC Kernels from Probabilistic Programs. InProceedings of the Seventeenth International Conference on Artificial Intelligence and Statistics, AISTATS 2014, Reykjavik, Iceland, April 22-25, 2014 (JMLR Workshop and Conference Proceedings). JMLR.org, 1068–1076. http: //proceedings....

    2014

  50. [50]

    Incremental Computation for Efficient Programmable Inference in Probabilistic Programs

    Fabian Zaiser, Jack Czenszak, Martin Rinard, Vikash Mansinghka, and Alexander Lew. 2026.Artifact for: “Incremental Computation for Efficient Programmable Inference in Probabilistic Programs” (PLDI 2026). doi:10.5281/zenodo.19080766 Received 2025-11-14; accepted 2026-04-03 Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 238. Publication date: June 202...

    work page doi:10.5281/zenodo.19080766 2026

  51. [51]

    toVisit contains only iterations not yet processed

    where 𝛾 ′ 1 =𝛾 ′ [𝑥↦→ ⟦𝑠⟧ (𝛾 ′)]. To apply Theo- rem C.2, we define admissible caches 𝐴 ˆ𝛾 :={(𝑢 𝑥, 𝑢𝑦) |𝑢 𝑥 ∈ U ⟦𝑠⟧tpl , ˆ𝛾 CtxType(Γ){𝜎 , 𝑢𝑦 ∈ U ⟦𝑡⟧tpl ,( ˆ𝛾,⟦𝑠⟧tpl ( ˆ𝛾) ) CtxType(Γ,𝑥:𝜎){𝜏 } The cache update function is 𝑢:=𝝀(𝑑𝛾,(𝑢 𝑥, 𝑢𝑦)).(dx, 𝑢 ′ 𝑥 ):=𝑢 𝑥 .apply(𝑑𝛾);(dy, 𝑢 ′ 𝑦):=𝑢 𝑦 .apply((𝑑𝛾,dx));(dy,(𝑢 ′ 𝑥, 𝑢′ 𝑦)) Stepping 𝑢𝑥 with d ˆ𝛾 yields (dv, ...

    2026

  52. [52]

    By validity of each collectionUpds𝑗, stepping it yields (dy 𝑗,collectionUpds ′ 𝑗 ) with (⟦𝑦𝑗 ⟧ (𝛾),dy 𝑗,⟦𝑦 𝑗 ⟧ (𝛾′)) ∈ Proc

    ∈ C 𝜌 where 𝑧′ 0 =⟦𝑠⟧ (𝛾 ′), and also seedUpd′ ∈ U ⟦𝑠⟧tpl , ˆ𝛾 ′ CtxType(Γ){𝜌 , so clause 2 of the admissible-cache definition is preserved. By validity of each collectionUpds𝑗, stepping it yields (dy 𝑗,collectionUpds ′ 𝑗 ) with (⟦𝑦𝑗 ⟧ (𝛾),dy 𝑗,⟦𝑦 𝑗 ⟧ (𝛾′)) ∈ Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 238. Publication date: June 2026. Incrementa...

    2026