Signatures and models (docs/roleflow.tex, sec:sig)

Sorts carry a measurable space and a σ-finite measure each (Sorts). Contexts are flat lists of sorts, and a value of a context Γ is a dependent tuple Val Γ, measured by the product vol Γ. Values are accessed by position through Val.get, which takes the sort as an argument with a proof Γ[i]? = some a, so no caller ever casts between sorts.

A signature (Sig) has operations Op as bs with bs ≠ [], and declares for some of them one semi-inverse (SemiInv): the first cs arguments are consumed and solved from the results and the remaining arguments ps. A model (Model) interprets operations by measurable maps and gives each operation a log-weight; for operations with a semi-inverse it must satisfy the left law and the leaf (change of variables at each parameter). ModelInv adds the right law. leaf_dag derives the leaf of a semi-inverse with the derived log-weight dagWeight; it needs only the left law.

class RoleFlow.Sorts (S : Type) : Type 1

Sorts, each with a measurable space and a σ-finite reference measure.

• X : S → Type

  The space of a sort.

• meas (s : S) : MeasurableSpace (X s)
• μ (s : S) : MeasureTheory.Measure (X s)

  The reference measure of a sort.

• sigmaFinite (s : S) : MeasureTheory.SigmaFinite (μ s)

Signatures

structure RoleFlow.SemiInv {S : Type} (Op : List S → List S → Type) (as bs : List S) : Type

A semi-inverse of an operation Op as bs: it solves the first arguments cs from the results and the remaining arguments ps (the parameters). The split point of the design is k = cs.length, and cs ≠ [] is k ≥ 1.

• cs : List S
• ps : List S
• split : self.cs ++ self.ps = as
• cs_ne : self.cs ≠ []
• op : Op (bs ++ self.ps) self.cs

structure RoleFlow.Sig (S : Type) : Type 1

A signature: operations, each with at most one semi-inverse.

• Op : List S → List S → Type
• bs_ne {as bs : List S} : ∀ (a : self.Op as bs), bs ≠ []
• inv {as bs : List S} : self.Op as bs → Option (SemiInv self.Op as bs)

@[reducible, inline]

abbrev RoleFlow.SemiInv.k {S : Type} {Op : List S → List S → Type} {as bs : List S} (si : SemiInv Op as bs) : ℕ

The split point: how many leading arguments a semi-inverse consumes.

Equations

• si.k = si.cs.length

Arguments

@[reducible, inline]

abbrev RoleFlow.Args {S : Type} (Γ : List S) (xs : List ℕ) (as : List S) : Prop

The arguments xs (positions of Γ) have the sorts as.

Equations

• RoleFlow.Args Γ xs as = List.Forall₂ (fun (x : ℕ) (a : S) => Γ[x]? = some a) xs as

theorem RoleFlow.Args.lt {S : Type} {Γ : List S} {xs : List ℕ} {as : List S} (h : Args Γ xs as) {x : ℕ} (hx : x ∈ xs) : x < Γ.length

theorem RoleFlow.Args.append {S : Type} {Γ : List S} {xs : List ℕ} {as : List S} (h : Args Γ xs as) (Δ : List S) : Args (Γ ++ Δ) xs as

Arguments stay valid when the context grows.

theorem RoleFlow.Args.lt_length {S : Type} {Γ : List S} {xs : List ℕ} {as : List S} (h : Args Γ xs as) {j : ℕ} (hj : j < as.length) : j < xs.length

theorem RoleFlow.Args.getElem? {S : Type} {Γ : List S} {xs : List ℕ} {as : List S} (h : Args Γ xs as) (j : ℕ) (hj : j < xs.length) : Γ[xs[j]]? = some as[j]

The j-th argument has the j-th sort.

theorem RoleFlow.Args.range' {S : Type} (Γ Δ : List S) : Args (Γ ++ Δ) (List.range' Γ.length Δ.length) Δ

The positions |Γ|, …, |Γ| + |Δ| - 1 of Γ ++ Δ have the sorts Δ.

theorem RoleFlow.Args.append' {S : Type} {Γ : List S} {xs ys : List ℕ} {as bs : List S} (h₁ : Args Γ xs as) (h₂ : Args Γ ys bs) : Args Γ (xs ++ ys) (as ++ bs)

Values of contexts

@[reducible, inline]

abbrev RoleFlow.Val {S : Type} [Sorts S] (Γ : List S) : Type

A value of the context Γ: one value per position.

Equations

• RoleFlow.Val Γ = ((i : Fin Γ.length) → RoleFlow.X (Γ.get i))

noncomputable def RoleFlow.vol {S : Type} [Sorts S] (Γ : List S) : MeasureTheory.Measure (Val Γ)

The product measure on a context.

Equations

• RoleFlow.vol Γ = MeasureTheory.Measure.pi fun (i : Fin Γ.length) => RoleFlow.μ (Γ.get i)

instance RoleFlow.instSigmaFiniteValVol {S : Type} [Sorts S] (Γ : List S) : MeasureTheory.SigmaFinite (vol Γ)

def RoleFlow.Val.nil {S : Type} [Sorts S] : Val []

The empty tuple.

Equations

• RoleFlow.Val.nil i = i.elim0

def RoleFlow.Val.cons {S : Type} [Sorts S] {Γ : List S} {a : S} (x : X a) (v : Val Γ) : Val (a :: Γ)

Prepend a value.

Equations

• RoleFlow.Val.cons x v = Fin.cons x v

def RoleFlow.Val.head {S : Type} [Sorts S] {Γ : List S} {a : S} (v : Val (a :: Γ)) : X a

Equations

• v.head = v 0

def RoleFlow.Val.tail {S : Type} [Sorts S] {Γ : List S} {a : S} (v : Val (a :: Γ)) : Val Γ

Equations

• v.tail i = v i.succ

@[simp]

theorem RoleFlow.Val.head_cons {S : Type} [Sorts S] {Γ : List S} {a : S} (x : X a) (v : Val Γ) : (cons x v).head = x

@[simp]

theorem RoleFlow.Val.tail_cons {S : Type} [Sorts S] {Γ : List S} {a : S} (x : X a) (v : Val Γ) : (cons x v).tail = v

@[simp]

theorem RoleFlow.Val.cons_head_tail {S : Type} [Sorts S] {Γ : List S} {a : S} (v : Val (a :: Γ)) : cons v.head v.tail = v

theorem RoleFlow.Val.lt_of_getElem? {S : Type} {Γ : List S} {a : S} {i : ℕ} (h : Γ[i]? = some a) : i < Γ.length

theorem RoleFlow.Val.get_eq_of_getElem? {S : Type} {Γ : List S} {a : S} {i : ℕ} (h : Γ[i]? = some a) : Γ.get ⟨i, ⋯⟩ = a

def RoleFlow.Val.get {S : Type} [Sorts S] {Γ : List S} {a : S} (v : Val Γ) (i : ℕ) (h : Γ[i]? = some a) : X a

The value at position i, of the sort a that Γ has there.

Equations

• v.get i h = RoleFlow.tr RoleFlow.X ⋯ (v ⟨i, ⋯⟩)

theorem RoleFlow.Val.apply_eq_get {S : Type} [Sorts S] {Γ : List S} (v : Val Γ) (i : Fin Γ.length) : v i = v.get ↑i ⋯

theorem RoleFlow.Val.ext {S : Type} [Sorts S] {Γ : List S} {v w : Val Γ} (h : ∀ (i : ℕ) (a : S) (hi : Γ[i]? = some a), v.get i hi = w.get i hi) : v = w

theorem RoleFlow.Val.ext_iff {S : Type} [Sorts S] {Γ : List S} {v w : Val Γ} : v = w ↔ ∀ (i : ℕ) (a : S) (hi : Γ[i]? = some a), v.get i hi = w.get i hi

@[simp]

theorem RoleFlow.Val.get_cons_zero {S : Type} [Sorts S] {Γ : List S} {a b : S} (x : X b) (v : Val Γ) (h : (b :: Γ)[0]? = some a) : (cons x v).get 0 h = tr X ⋯ x

@[simp]

theorem RoleFlow.Val.get_cons_succ {S : Type} [Sorts S] {Γ : List S} {a b : S} (x : X b) (v : Val Γ) {i : ℕ} (h : (b :: Γ)[i + 1]? = some a) : (cons x v).get (i + 1) h = v.get i h

def RoleFlow.Val.cast {S : Type} [Sorts S] {Γ Δ : List S} (h : Γ = Δ) (v : Val Γ) : Val Δ

Transport along an equality of contexts.

Equations

• RoleFlow.Val.cast h v = h ▸ v

@[simp]

theorem RoleFlow.Val.cast_rfl {S : Type} [Sorts S] {Γ : List S} (v : Val Γ) : cast ⋯ v = v

@[simp]

theorem RoleFlow.Val.get_cast {S : Type} [Sorts S] {Γ Δ : List S} {a : S} (h : Γ = Δ) (v : Val Γ) {i : ℕ} (hi : Δ[i]? = some a) : (cast h v).get i hi = v.get i ⋯

def RoleFlow.Val.append {S : Type} [Sorts S] {Δ Γ : List S} : Val Γ → Val Δ → Val (Γ ++ Δ)

Concatenation.

Equations

• x_3.append x✝ = x✝
• v.append x✝ = RoleFlow.Val.cons v.head (v.tail.append x✝)

def RoleFlow.Val.right {S : Type} [Sorts S] {Δ Γ : List S} : Val (Γ ++ Δ) → Val Δ

The part of a value of Γ ++ Δ that belongs to Δ.

Equations

• w.right = w
• w.right = w.tail.right

@[simp]

theorem RoleFlow.Val.right_append {S : Type} [Sorts S] {Γ Δ : List S} (v : Val Γ) (w : Val Δ) : (v.append w).right = w

theorem RoleFlow.Val.get_append_left {S : Type} [Sorts S] {Γ Δ : List S} {a : S} (v : Val Γ) (w : Val Δ) {i : ℕ} (hi : i < Γ.length) (h : (Γ ++ Δ)[i]? = some a) : (v.append w).get i h = v.get i ⋯

theorem RoleFlow.Val.get_append_right {S : Type} [Sorts S] {Γ Δ : List S} {a : S} (v : Val Γ) (w : Val Δ) {i : ℕ} (h : (Γ ++ Δ)[Γ.length + i]? = some a) : (v.append w).get (Γ.length + i) h = w.get i ⋯

def RoleFlow.Val.pick {S : Type} [Sorts S] {Γ : List S} (v : Val Γ) (xs : List ℕ) {as : List S} : Args Γ xs as → Val as

Select the positions xs.

Equations

• v.pick [] x_3 = RoleFlow.Val.nil
• v.pick (x_3 :: xs) h = RoleFlow.Val.cons (v.get x_3 ⋯) (v.pick xs ⋯)
• v.pick [] h = absurd h ⋯
• v.pick (head :: tail) h = absurd h ⋯

Picking

theorem RoleFlow.Val.tr_get {S : Type} [Sorts S] {Γ : List S} {a b : S} (v : Val Γ) (e : a = b) {i : ℕ} (h : Γ[i]? = some a) : tr X e (v.get i h) = v.get i ⋯

theorem RoleFlow.Val.get_congr {S : Type} [Sorts S] {Γ : List S} {a : S} (v : Val Γ) {i j : ℕ} (e : i = j) (hi : Γ[i]? = some a) (hj : Γ[j]? = some a) : v.get i hi = v.get j hj

theorem RoleFlow.Val.get_pick {S : Type} [Sorts S] {Γ : List S} {a : S} (v : Val Γ) {xs : List ℕ} {as : List S} (h : Args Γ xs as) {j : ℕ} (hj : as[j]? = some a) : (v.pick xs h).get j hj = v.get xs[j] ⋯

theorem RoleFlow.Val.pick_eq_of_get {S : Type} [Sorts S] {Γ Γ' : List S} (v : Val Γ) (w : Val Γ') {xs : List ℕ} {as : List S} (h : Args Γ xs as) (h' : Args Γ' xs as) (H : ∀ x ∈ xs, ∀ (a : S) (hx : Γ[x]? = some a) (hx' : Γ'[x]? = some a), v.get x hx = w.get x hx') : v.pick xs h = w.pick xs h'

Picking from two values that agree at the picked positions.

theorem RoleFlow.Val.pick_append {S : Type} [Sorts S] {Γ : List S} {xs ys : List ℕ} {as bs : List S} (v : Val Γ) (h₁ : Args Γ xs as) (h₂ : Args Γ ys bs) : v.pick (xs ++ ys) ⋯ = (v.pick xs h₁).append (v.pick ys h₂)

theorem RoleFlow.Val.pick_cast {S : Type} [Sorts S] {Γ Δ : List S} (e : Γ = Δ) (v : Val Γ) {xs : List ℕ} {as : List S} (h : Args Δ xs as) : (cast e v).pick xs h = v.pick xs ⋯

theorem RoleFlow.Val.pick_range'_append {S : Type} [Sorts S] {Γ Δ : List S} (v : Val Γ) (w : Val Δ) : (v.append w).pick (List.range' Γ.length Δ.length) ⋯ = w

Picking the positions of Δ from a value of Γ ++ Δ.

Measurability

theorem RoleFlow.Val.measurable_get {S : Type} [Sorts S] {Γ : List S} {a : S} {i : ℕ} (h : Γ[i]? = some a) : Measurable fun (v : Val Γ) => v.get i h

theorem RoleFlow.Val.measurable_head {S : Type} [Sorts S] {Γ : List S} {a : S} : Measurable fun (v : Val (a :: Γ)) => v.head

theorem RoleFlow.Val.measurable_tail {S : Type} [Sorts S] {Γ : List S} {a : S} : Measurable fun (v : Val (a :: Γ)) => v.tail

theorem RoleFlow.Val.measurable_cons {S : Type} [Sorts S] {Γ : List S} {a : S} : Measurable fun (p : X a × Val Γ) => cons p.1 p.2

theorem RoleFlow.Val.measurable_cons' {S : Type} [Sorts S] {Γ : List S} {a : S} {Y : Type u_1} [MeasurableSpace Y] {g : Y → X a} {h : Y → Val Γ} (hg : Measurable g) (hh : Measurable h) : Measurable fun (y : Y) => cons (g y) (h y)

cons of measurable maps, in the form fun_prop uses.

theorem RoleFlow.Val.measurable_cast {S : Type} [Sorts S] {Γ Δ : List S} (h : Γ = Δ) : Measurable (cast h)

theorem RoleFlow.Val.measurable_append {S : Type} [Sorts S] {Γ Δ : List S} : Measurable fun (p : Val Γ × Val Δ) => p.1.append p.2

theorem RoleFlow.Val.measurable_right {S : Type} [Sorts S] {Γ Δ : List S} : Measurable fun (w : Val (Γ ++ Δ)) => w.right

theorem RoleFlow.Val.measurable_pick {S : Type} [Sorts S] {Γ : List S} {xs : List ℕ} {as : List S} (h : Args Γ xs as) : Measurable fun (v : Val Γ) => v.pick xs h

Products over contexts

theorem RoleFlow.Val.measurePreserving_uncons {S : Type} [Sorts S] {Γ : List S} {a : S} : MeasureTheory.MeasurePreserving (fun (v : Val (a :: Γ)) => (v.head, v.tail)) (vol (a :: Γ)) ((μ a).prod (vol Γ))

theorem RoleFlow.Val.eq_nil {S : Type} [Sorts S] (v : Val []) : v = nil

theorem RoleFlow.Val.vol_nil {S : Type} [Sorts S] : vol [] = MeasureTheory.Measure.dirac nil

instance RoleFlow.Val.instIsProbabilityMeasureNilVol {S : Type} [Sorts S] : MeasureTheory.IsProbabilityMeasure (vol [])

theorem RoleFlow.Val.measurePreserving_cons {S : Type} [Sorts S] {Γ : List S} {a : S} : MeasureTheory.MeasurePreserving (fun (p : X a × Val Γ) => cons p.1 p.2) ((μ a).prod (vol Γ)) (vol (a :: Γ))

theorem RoleFlow.Val.measurePreserving_head {S : Type} [Sorts S] {a : S} : MeasureTheory.MeasurePreserving (fun (v : Val [a]) => v.head) (vol [a]) (μ a)

A one-element context is its sort.

theorem RoleFlow.Val.measurePreserving_single {S : Type} [Sorts S] {a : S} : MeasureTheory.MeasurePreserving (fun (x : X a) => cons x nil) (μ a) (vol [a])

Models

def RoleFlow.SemiInv.glue {S : Type} [Sorts S] {Op : List S → List S → Type} {as bs : List S} (si : SemiInv Op as bs) (c : Val si.cs) (p : Val si.ps) : Val as

Glue the consumed arguments and the parameters into the argument tuple.

Equations

• si.glue c p = RoleFlow.Val.cast ⋯ (c.append p)

theorem RoleFlow.SemiInv.measurable_glue {S : Type} [Sorts S] {Op : List S → List S → Type} {as bs : List S} (si : SemiInv Op as bs) : Measurable fun (q : Val si.cs × Val si.ps) => si.glue q.1 q.2

theorem RoleFlow.SemiInv.args_take {S : Type} {Op : List S → List S → Type} {as bs : List S} (si : SemiInv Op as bs) {Γ : List S} {xs : List ℕ} (h : Args Γ xs as) : Args Γ (List.take si.k xs) si.cs

theorem RoleFlow.SemiInv.args_drop {S : Type} {Op : List S → List S → Type} {as bs : List S} (si : SemiInv Op as bs) {Γ : List S} {xs : List ℕ} (h : Args Γ xs as) : Args Γ (List.drop si.k xs) si.ps

theorem RoleFlow.SemiInv.glue_pick {S : Type} [Sorts S] {Op : List S → List S → Type} {as bs : List S} (si : SemiInv Op as bs) {Γ : List S} (v : Val Γ) {xs : List ℕ} (h : Args Γ xs as) : si.glue (v.pick (List.take si.k xs) ⋯) (v.pick (List.drop si.k xs) ⋯) = v.pick xs h

Gluing the consumed arguments and the parameters of a picked argument tuple.

structure RoleFlow.Model {S : Type} [Sorts S] (Sg : Sig S) : Type

A model: measurable interpretations and log-weights; for every operation with a semi-inverse, the left law and the leaf. The log-weight ℓ o is read on the whole argument tuple, ℓ_o(c, p) = ℓ o (glue c p); it is irrelevant for operations without a semi-inverse.

• sem {as bs : List S} : Sg.Op as bs → Val as → Val bs
• ℓ {as bs : List S} : Sg.Op as bs → Val as → ℝ
• sem_meas {as bs : List S} (o : Sg.Op as bs) : Measurable (self.sem o)
• ℓ_meas {as bs : List S} (o : Sg.Op as bs) : Measurable (self.ℓ o)
• left {as bs : List S} (o : Sg.Op as bs) (si : SemiInv Sg.Op as bs) : Sg.inv o = some si → ∀ (c : Val si.cs) (p : Val si.ps), self.sem si.op ((self.sem o (si.glue c p)).append p) = c
• leaf {as bs : List S} (o : Sg.Op as bs) (si : SemiInv Sg.Op as bs) : Sg.inv o = some si → ∀ (p : Val si.ps), Cov (vol si.cs) (vol bs) (fun (c : Val si.cs) => self.sem o (si.glue c p)) fun (c : Val si.cs) => expw (self.ℓ o (si.glue c p))

def RoleFlow.Model.RightLaw {S : Type} [Sorts S] {Sg : Sig S} (M : Model Sg) : Prop

The right law of a model: every semi-inverse is also a right inverse.

Equations

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

structure RoleFlow.ModelInv {S : Type} [Sorts S] (Sg : Sig S) extends RoleFlow.Model Sg : Type

A model with the right law as well (Model± of the design).

• sem {as bs : List S} : Sg.Op as bs → Val as → Val bs
• ℓ {as bs : List S} : Sg.Op as bs → Val as → ℝ
• sem_meas {as bs : List S} (o : Sg.Op as bs) : Measurable (self.sem o)
• ℓ_meas {as bs : List S} (o : Sg.Op as bs) : Measurable (self.ℓ o)
• left {as bs : List S} (o : Sg.Op as bs) (si : SemiInv Sg.Op as bs) : Sg.inv o = some si → ∀ (c : Val si.cs) (p : Val si.ps), self.sem si.op ((self.sem o (si.glue c p)).append p) = c
• leaf {as bs : List S} (o : Sg.Op as bs) (si : SemiInv Sg.Op as bs) : Sg.inv o = some si → ∀ (p : Val si.ps), Cov (vol si.cs) (vol bs) (fun (c : Val si.cs) => self.sem o (si.glue c p)) fun (c : Val si.cs) => expw (self.ℓ o (si.glue c p))
• right : self.RightLaw

Derived log-weights of semi-inverses

def RoleFlow.dagWeight {S : Type} [Sorts S] {as bs cs ps : List S} (G : Val (bs ++ ps) → Val cs) (ℓ : Val as → ℝ) (split : cs ++ ps = as) (w : Val (bs ++ ps)) : ℝ

The derived log-weight of a semi-inverse G of F, on G's argument tuple (b, p): -ℓ_F(G(b, p), p).

Equations

• RoleFlow.dagWeight G ℓ split w = -ℓ (RoleFlow.Val.cast split ((G w).append w.right))

theorem RoleFlow.measurable_dagWeight {S : Type} [Sorts S] {as bs cs ps : List S} {G : Val (bs ++ ps) → Val cs} {ℓ : Val as → ℝ} (hG : Measurable G) (hℓ : Measurable ℓ) (split : cs ++ ps = as) : Measurable (dagWeight G ℓ split)

theorem RoleFlow.leaf_dag {S : Type} [Sorts S] {as bs cs ps : List S} {F : Val as → Val bs} {G : Val (bs ++ ps) → Val cs} {ℓ : Val as → ℝ} {split : cs ++ ps = as} (hG : Measurable G) (hℓ : Measurable ℓ) (left : ∀ (c : Val cs) (p : Val ps), G ((F (Val.cast split (c.append p))).append p) = c) (leaf : ∀ (p : Val ps), Cov (vol cs) (vol bs) (fun (c : Val cs) => F (Val.cast split (c.append p))) fun (c : Val cs) => expw (ℓ (Val.cast split (c.append p)))) (p : Val ps) : Cov (vol bs) (vol cs) (fun (b : Val bs) => G (b.append p)) fun (b : Val bs) => expw (dagWeight G ℓ split (b.append p))

The leaf of a semi-inverse, with the derived log-weight, by Inv. Only the left law of the forward operation is used.