The density theorem (docs/roleflow.tex, sec:density)

Fix the context Γ of all variables and a family of traces T : Ω → Val Γ (for a program at fixed weights: the trace of each input). Det T A v says that v is determined by the positions A: some measurable function of the live state on A gives its value on every trace. A recipe holds (Holds) if its targets are determined by its sources.

Factorization (det_of_known, Recov.det, Recov.det_params): if all recipes hold and the weights are determined by nothing (they are constant), then everything in Known R (Θ ∪ K) is determined by K. With Recov this gives the recomputation r_v of every variable in scope from the live state, and at a spine step that of the parameters from the live variables the step does not consume.

Density (density_aux, by Typed.induction_recov): given that the recipes of the lines hold (xrecs_holds), at each node of a derivation (NodeInv) there are a measurable F : X_Λ → X_O and L : X_Λ → ℝ with Cov (lvol Λ) (vol O) F e^L that give the returned tuple and the remaining log-weight on every trace. At a spine step, F = F' ∘ step with step(c, q) = (q, ⟦o⟧(c, z q)), where z recomputes the parameters from q; its Cov is Tri with the leaf at z q, between measure-preserving splittings. Prog.density reads this at the root, and Prog.density_joint is the joint statement over the weights, which covers conditional flows. Only the left law is used.

Determined positions

def RoleFlow.Det {S : Type} [Sorts S] {Γ : List S} {Ω : Type u_1} (T : Ω → Val Γ) (A : Finset ℕ) (v : ℕ) : Prop

v is determined by the positions A on the traces T.

Equations

• RoleFlow.Det T A v = ∀ (a : S) (h : Γ[v]? = some a), ∃ (g : RoleFlow.LState Γ A → RoleFlow.X a), Measurable g ∧ ∀ (ω : Ω), (T ω).get v h = g (RoleFlow.LState.restrict A (T ω))

def RoleFlow.Holds {S : Type} [Sorts S] {Sg : Sig S} {Γ : List S} {Ω : Type u_1} (T : Ω → Val Γ) (r : XRecipe Sg) : Prop

A recipe holds on the traces T: its targets are determined by its sources.

Equations

• RoleFlow.Holds T r = ∀ v ∈ r.tgt, RoleFlow.Det T r.line.args.toFinset v

theorem RoleFlow.Det.of_mem {S : Type} [Sorts S] {Γ : List S} {Ω : Type u_1} {T : Ω → Val Γ} {A : Finset ℕ} {v : ℕ} (hv : v ∈ A) : Det T A v

theorem RoleFlow.Det.state {S : Type} [Sorts S] {Γ : List S} {Ω : Type u_1} {T : Ω → Val Γ} {A B : Finset ℕ} (hB : ∀ w ∈ B, Det T A w) : ∃ (G : LState Γ A → LState Γ B), Measurable G ∧ ∀ (ω : Ω), G (LState.restrict A (T ω)) = LState.restrict B (T ω)

If every position of B is determined by A, so is the live state on B.

theorem RoleFlow.Det.comp {S : Type} [Sorts S] {Γ : List S} {Ω : Type u_1} {T : Ω → Val Γ} {A B : Finset ℕ} {v : ℕ} (hB : ∀ w ∈ B, Det T A w) (h : Det T B v) : Det T A v

theorem RoleFlow.Det.pick {S : Type} [Sorts S] {Γ : List S} {Ω : Type u_1} {T : Ω → Val Γ} {A : Finset ℕ} {xs : List ℕ} {as : List S} (hxs : ∀ x ∈ xs, Det T A x) (h : Args Γ xs as) : ∃ (Z : LState Γ A → Val as), Measurable Z ∧ ∀ (ω : Ω), Z (LState.restrict A (T ω)) = (T ω).pick xs h

Determined positions can be picked by a measurable function of the live state.

theorem RoleFlow.det_of_pick {S : Type} [Sorts S] {Γ : List S} {Ω : Type u_1} {T : Ω → Val Γ} {xs ys : List ℕ} {as bs : List S} (hx : Args Γ xs as) (hy : Args Γ ys bs) {G : Val as → Val bs} (hG : Measurable G) (hT : ∀ (ω : Ω), (T ω).pick ys hy = G ((T ω).pick xs hx)) (v : ℕ) : v ∈ ys → Det T xs.toFinset v

If the values at ys are a measurable function of those at xs on every trace, then every position of ys is determined by xs.

theorem RoleFlow.det_of_known {S : Type} [Sorts S] {Sg : Sig S} {Γ : List S} {Ω : Type u_1} {T : Ω → Val Γ} {v nw : ℕ} {R : List (XRecipe Sg)} {K : Finset ℕ} (hR : ∀ r ∈ R, Holds T r) (hw : ∀ w < nw, Det T ∅ w) (hv : Known R ({w : ℕ | w < nw} ∪ ↑K) v) : Det T K v

Factorization: if the recipes hold and the weights are determined by nothing, everything known from the weights and K is determined by K.

theorem RoleFlow.Recov.det {S : Type} [Sorts S] {Sg : Sig S} {Γ : List S} {Ω : Type u_1} {T : Ω → Val Γ} {v nw n : ℕ} {Λ : Finset ℕ} {R : List (XRecipe Sg)} {D : List (Finset ℕ)} (hrec : Recov nw n Λ R D) (hR : ∀ r ∈ R, Holds T r) (hw : ∀ w < nw, Det T ∅ w) (hv : v < n) : Det T Λ v

Factorization, the live-state recomputation r_v: under Recov, every variable in scope is determined by the live state.

theorem RoleFlow.Recov.det_params {S : Type} [Sorts S] {Sg : Sig S} {Γ : List S} {Ω : Type u_1} {T : Ω → Val Γ} {nw n : ℕ} {Λ : Finset ℕ} {R : List (XRecipe Sg)} {D : List (Finset ℕ)} {l : Line Sg} {k p : ℕ} (hrec : Recov nw n Λ R D) (hR : ∀ r ∈ R, Holds T r) (hw : ∀ w < nw, Det T ∅ w) (hargs : ∀ x ∈ l.args, x < n) (hacyc : ∀ p ∈ List.drop k l.args, ∀ c ∈ List.take k l.args, c ∉ D.getD p ∅) (hp : p ∈ List.drop k l.args) : Det T (Λ \ (List.take k l.args).toFinset) p

Factorization at a spine step: the parameters factor through the live variables the step does not consume, since their supports avoid them.

Density along a derivation

def RoleFlow.NodeInv {S : Type} [Sorts S] {Sg : Sig S} (M : Model Sg) {Γ outs : List S} {Ω : Type u_1} (T : Ω → Val Γ) (Γ' : List S) (Λ : Finset ℕ) (ls : List (Line Sg)) (xs : List ℕ) (ρ : List Role) : Prop

The invariant at a node of a derivation, with live set Λ, remaining lines ls, returned xs and roles ρ: a measurable F and L on live states with Cov (lvol Λ) (vol O) F e^L, which give the returned tuple and the remaining log-weight on every trace. The node starts in the context Γ', and pre ω is the value of Γ' from which the trace T ω continues.

Equations

• One or more equations did not get rendered due to their size.

theorem RoleFlow.density_aux {S : Type} [Sorts S] {Sg : Sig S} (M : Model Sg) {Γ outs : List S} {Ω : Type u_1} (T : Ω → Val Γ) (nw : ℕ) (hw : ∀ w < nw, Det T ∅ w) {R : List (XRecipe Sg)} (hR : ∀ r ∈ R, Holds T r) {O Γ' : List S} {Λ : Finset ℕ} {D : List (Finset ℕ)} {ls : List (Line Sg)} {xs : List ℕ} {ρ : List Role} (hT : Typed Sg O Γ' Λ D ls xs ρ) (hrec : Recov nw Γ'.length Λ R D) (hX : ∀ x ∈ xrecs Γ'.length ls ρ, x ∈ R) : NodeInv M T Γ' Λ ls xs ρ

Density at every node of a derivation, given recipes R that hold and contain those of the lines.

The density theorem

theorem RoleFlow.Prog.density_surj {S : Type} [Sorts S] {Sg : Sig S} (M : Model Sg) (P : Prog Sg) {ρ : List Role} (hT : P.Typed ρ) (θ : Val P.wts) : (Cov (vol P.ins) (vol P.outs) (sem M P ⋯ θ) fun (x : Val P.ins) => expw (logw M P ⋯ ρ θ x)) ∧ (M.RightLaw → Function.Surjective (sem M P ⋯ θ))

Density (thm:density) at the root of the derivation, together with surjectivity under the right law.

theorem RoleFlow.Prog.density {S : Type} [Sorts S] {Sg : Sig S} (M : Model Sg) (P : Prog Sg) {ρ : List Role} (hT : P.Typed ρ) (θ : Val P.wts) : Cov (vol P.ins) (vol P.outs) (sem M P ⋯ θ) fun (x : Val P.ins) => expw (logw M P ⋯ ρ θ x)

Density (thm:density): a typed program pushes e^{L_θ} · μ_I forward to μ_O, for every value of the weights.

theorem RoleFlow.Prog.surjective {S : Type} [Sorts S] {Sg : Sig S} (M : Model Sg) (hM : M.RightLaw) (P : Prog Sg) {ρ : List Role} (hT : P.Typed ρ) (θ : Val P.wts) : Function.Surjective (sem M P ⋯ θ)

Under the right law, the semantics of a typed program is surjective (prop:surj): every live-state step is solved by the semi-inverse.

theorem RoleFlow.Prog.density_joint {S : Type} [Sorts S] {Sg : Sig S} (M : Model Sg) (P : Prog Sg) {ρ : List Role} (hT : P.Typed ρ) : Cov ((vol P.wts).prod (vol P.ins)) ((vol P.wts).prod (vol P.outs)) (fun (q : Val P.wts × Val P.ins) => (q.1, sem M P ⋯ q.1 q.2)) fun (q : Val P.wts × Val P.ins) => expw (logw M P ⋯ ρ q.1 q.2)

Joint density (cor:joint): over the weights and the inputs together. Conditioning values of conditional flows are weights, so this is the density of the joint distribution with them.