Turing.jl

Per-target obligations of Transpilation correctness for \(\mathsf{T} = \mathrm{Turing.jl}\).

Semantics

Turing.jl's denotational semantics is the trace semantics of Ge, Xu, and Ghahramani (2018) implemented via the @model macro that rewrites ~-statements into joint log-density accumulator updates. The log-density probe is Turing.logjoint(model, θ), returning the joint log-density at a parameter point.

Unconstrained-space change of variables

Turing applies per-distribution Bijectors.jl transformations during inference; logjoint returns the constrained-space density. \(\Psi_{\mathsf{Turing}} = \mathrm{id}\) at the renderer level.

Family parameterizations

Turing consumes Distributions.jl which uses the canonical parameterizations of Wikipedia: List of probability distributions. The QVR ↔ Turing mapping is identity for every family with a Distributions.jl counterpart. \(\pi_{F, \mathsf{Turing}} = \mathrm{id}\) and \(c_{F, \mathsf{Turing}} = 0\).

The Turing renderer composes HalfNormal / HalfCauchy (which have no Distributions.jl primitive) as truncated(Normal(0, sigma), 0, Inf) via the documented truncated wrapper, contributing \(c_{\mathrm{HalfNormal}, \mathsf{Turing}} = \log 2\) to the per-program constant.

Per-construct emit

Sample / observe. <name> ~ <Family>(<args>) inside the @model function model(...) body; observations appear as function parameters that bind to specific values when logjoint is called.

Plate. filldist(D, B) for index-independent batches; arraydist([D_i for i in 1:B]) for index-dependent batches. Both denote the documented product measure (Turing.jl documentation, "Composing distributions").

Marginalize. The renderer may keep a finite latent explicit. Turing can use discrete-capable samplers or composed inference for such a model; HMC and NUTS do not directly update discrete states.

Score / let / return. Turing.@addlogprob!(expr) for score; native <name> = <expr> for let; native return for return.

Acceptance

  • Tier 1 structural. Every emit has @model function model(...) ... end with ~ statements wrapping filldist / arraydist per plate axis.
  • Tier 1 pipeline composition. Direct and composed pipeline calls agree.
  • Tier 2 external syntax. julia --eval "Meta.parse(read(stdin, String); raise=true)" accepts every emit.
  • Tier 3 numeric equivalence. The Turing probe evaluates the selected fixture grids under the shared constant-spread tolerance.