Function calls: a signature extended by a typed program

A typed program P (roles ρ), whose inverse program P† = P.inverse ρ is typed too (roles ρi), becomes two operations of a new signature (Sig.declare): fwd, on P's inputs then its weights, and inv, on its outputs then its weights. Each is the other's semi-inverse, with the inputs (outputs) consumed and the weights as parameters. Every operation of the old signature stays, as prim.

The model of the new signature (ModelInv.link) interprets fwd by ⟦P⟧ with log-weight L_θ of P, and inv by ⟦P†⟧ with the log-weight of P†; its laws are theorems about every typed program: the left laws are inverse_sem and sem_inverse, the leaves are density for P and for P†. So a call needs nothing beyond the typings of the callee and its inverse.

Definitions are added one at a time (Linked), each over the signature of the ones before it: a tower Sg₀, Sg₀.declare P₁, (Sg₀.declare P₁).declare P₂, …, so a body may call any function defined before it, and none can recurse. A call to a function k definitions back is its fwd under k prims (Linked.find). Linked.model is the model at the top, and every theorem about typed programs holds for programs with calls (Linked.density, Linked.bijective).

The declared operations

inductive RoleFlow.DeclOp {S : Type} (Sg : Sig S) (P : Prog Sg) : List S → List S → Type

The operations of Sg with P declared: Sg's own, and P's forward and inverse.

• prim {S : Type} {Sg : Sig S} {P : Prog Sg} {as bs : List S} : Sg.Op as bs → DeclOp Sg P as bs
• fwd {S : Type} {Sg : Sig S} {P : Prog Sg} : DeclOp Sg P (P.ins ++ P.wts) P.outs
• inv {S : Type} {Sg : Sig S} {P : Prog Sg} : DeclOp Sg P (P.outs ++ P.wts) P.ins

def RoleFlow.SemiInv.prim {S : Type} {Sg : Sig S} {P : Prog Sg} {as bs : List S} (si : SemiInv Sg.Op as bs) : SemiInv (DeclOp Sg P) as bs

A semi-inverse of Sg as one of the extended signature.

Equations

• si.prim = { cs := si.cs, ps := si.ps, split := ⋯, cs_ne := ⋯, op := RoleFlow.DeclOp.prim si.op }

def RoleFlow.Sig.declare {S : Type} (Sg : Sig S) (P : Prog Sg) (hi : P.ins ≠ []) (ho : P.outs ≠ []) : Sig S

Sg with P declared.

Equations

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

def RoleFlow.Prog.mapOp {S : Type} {Sg Sg' : Sig S} (f : {as bs : List S} → Sg.Op as bs → Sg'.Op as bs) (P : Prog Sg) : Prog Sg'

An operation of Sg applied to every line.

Equations

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

Values of concatenated contexts

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

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

Equations

• x_2.left = RoleFlow.Val.nil
• w.left = RoleFlow.Val.cons w.head w.tail.left

@[simp]

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

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

The model

def RoleFlow.linkSem {S : Type} [Sorts S] {Sg : Sig S} (M : ModelInv Sg) (P : Prog Sg) {ρ ρi : List Role} (hT : P.Typed ρ) (hTi : (P.inverse ρ).Typed ρi) {as bs : List S} : DeclOp Sg P as bs → Val as → Val bs

The interpretation: fwd is ⟦P⟧, inv is ⟦P†⟧, on the inputs (outputs), then the weights.

Equations

• RoleFlow.linkSem M P hT hTi (RoleFlow.DeclOp.prim o) = M.sem o
• RoleFlow.linkSem M P hT hTi RoleFlow.DeclOp.fwd = fun (v : RoleFlow.Val (P.ins ++ P.wts)) => RoleFlow.Prog.sem M.toModel P ⋯ v.right v.left
• RoleFlow.linkSem M P hT hTi RoleFlow.DeclOp.inv = fun (v : RoleFlow.Val (P.outs ++ P.wts)) => RoleFlow.Prog.sem M.toModel (P.inverse ρ) ⋯ v.right v.left

noncomputable def RoleFlow.linkℓ {S : Type} [Sorts S] {Sg : Sig S} (M : ModelInv Sg) (P : Prog Sg) {ρ ρi : List Role} (hT : P.Typed ρ) (hTi : (P.inverse ρ).Typed ρi) {as bs : List S} : DeclOp Sg P as bs → Val as → ℝ

The log-weights: L_θ of P for fwd, of P† for inv.

Equations

• RoleFlow.linkℓ M P hT hTi (RoleFlow.DeclOp.prim o) = M.ℓ o
• RoleFlow.linkℓ M P hT hTi RoleFlow.DeclOp.fwd = fun (v : RoleFlow.Val (P.ins ++ P.wts)) => RoleFlow.Prog.logw M.toModel P ⋯ ρ v.right v.left
• RoleFlow.linkℓ M P hT hTi RoleFlow.DeclOp.inv = fun (v : RoleFlow.Val (P.outs ++ P.wts)) => RoleFlow.Prog.logw M.toModel (P.inverse ρ) ⋯ ρi v.right v.left

theorem RoleFlow.measurable_linkSem {S : Type} [Sorts S] {Sg : Sig S} (M : ModelInv Sg) (P : Prog Sg) {ρ ρi : List Role} (hT : P.Typed ρ) (hTi : (P.inverse ρ).Typed ρi) {as bs : List S} (o : DeclOp Sg P as bs) : Measurable (linkSem M P hT hTi o)

theorem RoleFlow.measurable_linkℓ {S : Type} [Sorts S] {Sg : Sig S} (M : ModelInv Sg) (P : Prog Sg) {ρ ρi : List Role} (hT : P.Typed ρ) (hTi : (P.inverse ρ).Typed ρi) {as bs : List S} (o : DeclOp Sg P as bs) : Measurable (linkℓ M P hT hTi o)

noncomputable def RoleFlow.ModelInv.link {S : Type} [Sorts S] {Sg : Sig S} (M : ModelInv Sg) (P : Prog Sg) {ρ ρi : List Role} (hT : P.Typed ρ) (hTi : (P.inverse ρ).Typed ρi) (hi : P.ins ≠ []) (ho : P.outs ≠ []) : ModelInv (Sg.declare P hi ho)

The model of Sg with P declared: the laws of fwd and inv are concordance (inverse_sem, sem_inverse) and density, for P and for P†.

Equations

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

The tower of definitions

inductive RoleFlow.Linked {S : Type} (Sg₀ : Sig S) : Sig S → Type 1

Definitions added one at a time over the base signature Sg₀, each a typed program (with a typed inverse program) over the signature of the ones before it; Sg is the signature with all of them declared.

• base {S : Type} {Sg₀ : Sig S} : Linked Sg₀ Sg₀
• add {S : Type} {Sg₀ Sg : Sig S} (L : Linked Sg₀ Sg) (name : String) (P : Prog Sg) (ρ ρi : List Role) (hT : P.Typed ρ) (hTi : (P.inverse ρ).Typed ρi) (hi : P.ins ≠ []) (ho : P.outs ≠ []) : Linked Sg₀ (Sg.declare P hi ho)

inductive RoleFlow.Callee {S : Type} (Op : List S → List S → Type) (as bs : List S) : Type

What an operation of the tower is: an operation of the base, or a call of a definition by name, forward or inverse, with the number k of its leading arguments that are values (the rest are its weights).

• base {S : Type} {Op : List S → List S → Type} {as bs : List S} : Op as bs → Callee Op as bs
• call {S : Type} {Op : List S → List S → Type} {as bs : List S} (name : String) (inv : Bool) (k : ℕ) : Callee Op as bs

def RoleFlow.Linked.lift {S : Type} {Sg₀ Sg : Sig S} : Linked Sg₀ Sg → {as bs : List S} → Sg₀.Op as bs → Sg.Op as bs

An operation of the base as one of the tower (under prims).

Equations

• RoleFlow.Linked.base.lift x✝ = x✝
• (L.add name P ρ ρi hT hTi hi ho).lift x✝ = RoleFlow.DeclOp.prim (L.lift x✝)

def RoleFlow.Linked.find {S : Type} {Sg₀ Sg : Sig S} : Linked Sg₀ Sg → String → Option ((as : List S) × (bs : List S) × Sg.Op as bs)

The forward operation of the definition name (the latest of that name).

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.Linked.base.find x✝ = none

def RoleFlow.Linked.view {S : Type} {Sg₀ Sg : Sig S} : Linked Sg₀ Sg → {as bs : List S} → Sg.Op as bs → Callee Sg₀.Op as bs

What an operation of the tower is (Callee).

Equations

• RoleFlow.Linked.base.view x✝ = RoleFlow.Callee.base x✝
• (L.add name P ρ ρi hT hTi hi ho).view (RoleFlow.DeclOp.prim o) = L.view o
• (L.add name P ρ ρi hT hTi hi ho).view RoleFlow.DeclOp.fwd = RoleFlow.Callee.call name false P.ins.length
• (L.add name P ρ ρi hT hTi hi ho).view RoleFlow.DeclOp.inv = RoleFlow.Callee.call name true P.outs.length

noncomputable def RoleFlow.Linked.model {S : Type} {Sg₀ : Sig S} [Sorts S] (M : ModelInv Sg₀) {Sg : Sig S} : Linked Sg₀ Sg → ModelInv Sg

The model of the tower over a model of the base (ModelInv.link at each definition).

Equations

• RoleFlow.Linked.model M RoleFlow.Linked.base = M
• RoleFlow.Linked.model M (L.add name P ρ ρi hT hTi hi ho) = (RoleFlow.Linked.model M L).link P hT hTi hi ho

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

Density of a typed program with calls, under the model of the tower.

theorem RoleFlow.Linked.bijective {S : Type} {Sg₀ : Sig S} [Sorts S] {Sg : Sig S} (L : Linked Sg₀ Sg) (M : ModelInv Sg₀) (P : Prog Sg) {ρ : List Role} (hT : P.Typed ρ) (θ : Val P.wts) : Function.Bijective (Prog.sem (model M L).toModel P ⋯ θ)

Bijectivity of a typed program with calls, with its inverse program as the inverse.