Programs and their semantics (docs/roleflow.tex, sec:prog)

A program has a weight context wts (Θ), an input context ins (I), output sorts outs (O), a list of lines ys = op(args) and the returned positions ret. Variables are named by their position: weights, then inputs, then the results of each line in order. The body let ys = o(xs) in e of the design is the list of lines followed by ret.

Well-formedness (Prog.WF, decidable) asks that every argument is in scope with the sort its operation expects and that the returned variables have the output sorts. The trace semantics extends the value of the context line by line (trace); the semantics Prog.sem picks the returned positions of the final trace, and Prog.logw sums the log-weights of the lines whose role is spine. All three are measurable jointly in the weights and the inputs.

structure RoleFlow.Line {S : Type} (Sg : Sig S) : Type

A line ys = op(args); its results ys get the next free positions.

• as : List S
• bs : List S
• op : Sg.Op self.as self.bs
• args : List ℕ

structure RoleFlow.Prog {S : Type} (Sg : Sig S) : Type

A program (Θ, I, e) in A-normal form, with variables named by position.

• wts : List S
• ins : List S
• outs : List S
• lines : List (Line Sg)
• ret : List ℕ

inductive RoleFlow.Role : Type

The role of a line: a spine step or a conditioner.

• spine : Role
• cond : Role

@[implicit_reducible]

instance RoleFlow.instDecidableEqRole : DecidableEq Role

Equations

• RoleFlow.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RoleFlow.instReprRole.repr : Role → ℕ → Std.Format

Equations

• RoleFlow.instReprRole.repr RoleFlow.Role.spine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RoleFlow.Role.spine")).group prec✝
• RoleFlow.instReprRole.repr RoleFlow.Role.cond prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RoleFlow.Role.cond")).group prec✝

@[implicit_reducible]

instance RoleFlow.instReprRole : Repr Role

Equations

• RoleFlow.instReprRole = { reprPrec := RoleFlow.instReprRole.repr }

def RoleFlow.ctxAfter {S : Type} {Sg : Sig S} : List S → List (Line Sg) → List S

The context after some lines.

Equations

• RoleFlow.ctxAfter x✝ [] = x✝
• RoleFlow.ctxAfter x✝ (l :: ls) = RoleFlow.ctxAfter (x✝ ++ l.bs) ls

def RoleFlow.LinesWF {S : Type} {Sg : Sig S} : List S → List (Line Sg) → Prop

Every line's arguments are in scope, with the sorts its operation expects.

Equations

• RoleFlow.LinesWF x✝ [] = True
• RoleFlow.LinesWF x✝ (l :: ls) = (RoleFlow.Args x✝ l.args l.as ∧ RoleFlow.LinesWF (x✝ ++ l.bs) ls)

@[implicit_reducible]

instance RoleFlow.decLinesWF {S : Type} {Sg : Sig S} [DecidableEq S] (Γ : List S) (ls : List (Line Sg)) : Decidable (LinesWF Γ ls)

Equations

• RoleFlow.decLinesWF x✝ [] = isTrue ⋯
• RoleFlow.decLinesWF x✝ (l :: ls) = RoleFlow.decLinesWF._aux_2 x✝ l ls (RoleFlow.decLinesWF (x✝ ++ l.bs) ls)

theorem RoleFlow.ctxAfter_append {S : Type} {Sg : Sig S} (Γ : List S) (ls : List (Line Sg)) : ∃ (Δ : List S), ctxAfter Γ ls = Γ ++ Δ

theorem RoleFlow.length_ctxAfter {S : Type} {Sg : Sig S} (Γ : List S) (ls : List (Line Sg)) : (ctxAfter Γ ls).length = Γ.length + (List.map (fun (l : Line Sg) => l.bs.length) ls).sum

theorem RoleFlow.getElem?_ctxAfter {S : Type} {Sg : Sig S} {Γ : List S} (ls : List (Line Sg)) {i : ℕ} (hi : i < Γ.length) : (ctxAfter Γ ls)[i]? = Γ[i]?

theorem RoleFlow.Args.ctxAfter {S : Type} {Sg : Sig S} {Γ : List S} {xs : List ℕ} {as : List S} (h : Args Γ xs as) (ls : List (Line Sg)) : Args (RoleFlow.ctxAfter Γ ls) xs as

Arguments stay valid after more lines.

@[reducible, inline]

abbrev RoleFlow.Prog.ctx₀ {S : Type} {Sg : Sig S} (P : Prog Sg) : List S

The initial context: weights, then inputs.

Equations

• P.ctx₀ = P.wts ++ P.ins

@[reducible, inline]

abbrev RoleFlow.Prog.ctx {S : Type} {Sg : Sig S} (P : Prog Sg) : List S

The context of all variables.

Equations

• P.ctx = RoleFlow.ctxAfter P.ctx₀ P.lines

def RoleFlow.Prog.WF {S : Type} {Sg : Sig S} (P : Prog Sg) : Prop

A well-formed program.

Equations

• P.WF = (RoleFlow.LinesWF P.ctx₀ P.lines ∧ RoleFlow.Args P.ctx P.ret P.outs)

@[implicit_reducible]

instance RoleFlow.Prog.instDecidableWFOfDecidableEq {S : Type} {Sg : Sig S} [DecidableEq S] (P : Prog Sg) : Decidable P.WF

Equations

• P.instDecidableWFOfDecidableEq = RoleFlow.Prog.instDecidableWFOfDecidableEq._aux_1 P

@[reducible, inline]

abbrev RoleFlow.Prog.nw {S : Type} {Sg : Sig S} (P : Prog Sg) : ℕ

The number of weights.

Equations

• P.nw = P.wts.length

def RoleFlow.Prog.inputs {S : Type} {Sg : Sig S} (P : Prog Sg) : Finset ℕ

The input positions.

Equations

• P.inputs = Finset.Ico P.wts.length (P.wts.length + P.ins.length)

Trace semantics

def RoleFlow.stepLine {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) (l : Line Sg) {Γ : List S} (h : Args Γ l.args l.as) (v : Val Γ) : Val (Γ ++ l.bs)

One line: extend the value of the context by the line's results.

Equations

• RoleFlow.stepLine M l h v = v.append (M.sem l.op (v.pick l.args h))

def RoleFlow.trace {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) {Γ : List S} (ls : List (Line Sg)) : LinesWF Γ ls → Val Γ → Val (ctxAfter Γ ls)

The trace: run the lines from a value of the context they start in.

Equations

• RoleFlow.trace M [] x_5 x_1 = x_1
• RoleFlow.trace M (l :: ls) h x_1 = RoleFlow.trace M ls ⋯ (RoleFlow.stepLine M l ⋯ x_1)

noncomputable def RoleFlow.logwLines {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) {Γ : List S} (ls : List (Line Sg)) : LinesWF Γ ls → List Role → Val Γ → ℝ

The log-weight of the lines with role spine, from a value of the context they start in. Missing roles count as conditioners.

Equations

• RoleFlow.logwLines M [] x_6 x_1 x_2 = 0
• RoleFlow.logwLines M (head :: tail) x_6 [] x_1 = 0
• RoleFlow.logwLines M (l :: ls) h (r :: ρ) x_1 = (if r = RoleFlow.Role.spine then M.ℓ l.op (x_1.pick l.args ⋯) else 0) + RoleFlow.logwLines M ls ⋯ ρ (RoleFlow.stepLine M l ⋯ x_1)

def RoleFlow.Prog.tr {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) (P : Prog Sg) (h : P.WF) (θ : Val P.wts) (x : Val P.ins) : Val P.ctx

tr_θ(x): the value of every variable.

Equations

• RoleFlow.Prog.tr M P h θ x = RoleFlow.trace M P.lines ⋯ (θ.append x)

def RoleFlow.Prog.sem {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) (P : Prog Sg) (h : P.WF) (θ : Val P.wts) (x : Val P.ins) : Val P.outs

⟦P⟧_θ(x): the returned variables.

Equations

• RoleFlow.Prog.sem M P h θ x = (RoleFlow.Prog.tr M P h θ x).pick P.ret ⋯

noncomputable def RoleFlow.Prog.logw {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) (P : Prog Sg) (h : P.WF) (ρ : List Role) (θ : Val P.wts) (x : Val P.ins) : ℝ

L_θ(x): the sum of the log-weights of the spine steps under the roles ρ.

Equations

• RoleFlow.Prog.logw M P h ρ θ x = RoleFlow.logwLines M P.lines ⋯ ρ (θ.append x)

Measurability

theorem RoleFlow.measurable_stepLine {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) (l : Line Sg) {Γ : List S} (h : Args Γ l.args l.as) : Measurable (stepLine M l h)

theorem RoleFlow.measurable_trace {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) {Γ : List S} (ls : List (Line Sg)) (h : LinesWF Γ ls) : Measurable (trace M ls h)

theorem RoleFlow.measurable_logwLines {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) {Γ : List S} (ls : List (Line Sg)) (h : LinesWF Γ ls) (ρ : List Role) : Measurable (logwLines M ls h ρ)

theorem RoleFlow.Prog.measurable_tr {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) (P : Prog Sg) (h : P.WF) : Measurable fun (q : Val P.wts × Val P.ins) => tr M P h q.1 q.2

The trace is measurable jointly in the weights and the inputs.

theorem RoleFlow.Prog.measurable_sem {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) (P : Prog Sg) (h : P.WF) : Measurable fun (q : Val P.wts × Val P.ins) => sem M P h q.1 q.2

(θ, x) ↦ ⟦P⟧_θ(x) is measurable.

theorem RoleFlow.Prog.measurable_logw {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) (P : Prog Sg) (h : P.WF) (ρ : List Role) : Measurable fun (q : Val P.wts × Val P.ins) => logw M P h ρ q.1 q.2

(θ, x) ↦ L_θ(x) is measurable.

Traces extend values

theorem RoleFlow.get_trace {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) {Γ : List S} (ls : List (Line Sg)) (h : LinesWF Γ ls) (v : Val Γ) {i : ℕ} {a : S} (hi : (ctxAfter Γ ls)[i]? = some a) (hlt : i < Γ.length) : (trace M ls h v).get i hi = v.get i ⋯

theorem RoleFlow.pick_trace {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) {Γ : List S} (ls : List (Line Sg)) (h : LinesWF Γ ls) (v : Val Γ) {xs : List ℕ} {as : List S} (hx : Args Γ xs as) (hx' : Args (ctxAfter Γ ls) xs as) : (trace M ls h v).pick xs hx' = v.pick xs hx

A trace keeps the values it starts from.

theorem RoleFlow.pick_trace_results {S : Type} {Sg : Sig S} [Sorts S] (M : Model Sg) {Γ : List S} (l : Line Sg) (ls : List (Line Sg)) (h : LinesWF Γ (l :: ls)) (v : Val Γ) (hy : Args (ctxAfter Γ (l :: ls)) (List.range' Γ.length l.bs.length) l.bs) : (trace M (l :: ls) h v).pick (List.range' Γ.length l.bs.length) hy = M.sem l.op (v.pick l.args ⋯)

The results of a line, in a trace from before it.