Inference of roles for invertibility

Unlike role typing, invertibility does not determine the roles: a line whose results nobody needs may take either role. And the roles of the backward pass (backward) may fail where others succeed: a line whose results are needed is marked spine, but if its data is returned, only its conditioner recipe helps (see Examples.lean).

Without roles, every line contributes both of its recipes (xrecsAll). By monotonicity of Known, these reach at least what the recipes of any roles reach. Conversely, in one closure only one recipe of a line can add anything: after the conditioner recipe, its arguments, among them the data, are known; after the spine recipe, its sources, among them the results, are known (known_pair_spine, known_pair_cond). inferAll picks that recipe line by line, deciding Known by the schedule (knownSet), so its roles reach everything that xrecsAll reaches (inferAll_known). Hence P is invertible under some roles iff the inputs are Known under xrecsAll (Prog.exists_invertible_iff), and then under Prog.rolesAll (Prog.invertible_rolesAll).

Prog.inferInv tries the roles of the backward pass first, so it agrees with Prog.infer where that succeeds (inferInv_of_infer), and falls back to Prog.rolesAll; it is sound and complete (inferInv_sound, inferInv_complete, inferInv_isSome_iff).

Deciding Known

def RoleFlow.knownSet {S : Type} {Sg : Sig S} (R : List (XRecipe Sg)) (B : List ℕ) : Std.HashSet ℕ

The schedule's known set from B, ignoring the emitted lines.

Equations

• RoleFlow.knownSet R B = (RoleFlow.fire R.length R 0 id (RoleFlow.insertAll ∅ B)).2.2

theorem RoleFlow.mem_knownSet {S : Type} {Sg : Sig S} {R : List (XRecipe Sg)} {B : List ℕ} {v : ℕ} : v ∈ knownSet R B ↔ Known R {w : ℕ | w ∈ B} v

All recipes

def RoleFlow.xrecsAll {S : Type} {Sg : Sig S} : ℕ → List (Line Sg) → List (XRecipe Sg)

The recipes of the lines under every role: each line's conditioner recipe and, if it has a partial inverse, its spine recipe.

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.xrecsAll x✝ [] = []

theorem RoleFlow.mem_xrecsAll_of_mem {S : Type} {Sg : Sig S} {n : ℕ} {ls : List (Line Sg)} {ρ : List Role} {x : XRecipe Sg} (h : x ∈ xrecs n ls ρ) : x ∈ xrecsAll n ls

theorem RoleFlow.Known.xrecsAll {S : Type} {Sg : Sig S} {n : ℕ} {ls : List (Line Sg)} {ρ : List Role} {B : Set ℕ} {v : ℕ} (h : Known (xrecs n ls ρ) B v) : Known (RoleFlow.xrecsAll n ls) B v

Roles never beat all recipes.

One line's two recipes

theorem RoleFlow.known_pair_spine {S : Type} {Sg : Sig S} {rc rs : XRecipe Sg} {R : List (XRecipe Sg)} {A : Set ℕ} (hc : (∀ a ∈ rc.line.args, Known (rs :: R) A a) → ∀ y ∈ rc.tgt, Known (rs :: R) A y) {v : ℕ} (h : Known (rc :: rs :: R) A v) : Known (rs :: R) A v

If the conditioner recipe rc only fires once its targets are known anyway, it can be dropped.

theorem RoleFlow.known_pair_cond {S : Type} {Sg : Sig S} {rc rs : XRecipe Sg} {R : List (XRecipe Sg)} {A : Set ℕ} (hcs : ∀ t ∈ rs.tgt, t ∈ rc.line.args) (hsc : ∀ t ∈ rc.tgt, t ∈ rs.line.args) (ha : ∀ a ∈ rc.line.args, Known (rs :: R) A a) (hy : ¬∀ y ∈ rc.tgt, Known (rs :: R) A y) {v : ℕ} (h : Known (rc :: rs :: R) A v) : Known (rc :: R) A v

If the sources of the conditioner recipe rc are known without it and its targets are not, the spine recipe rs, whose sources contain those targets, never fires, and can be dropped.

Choosing the roles

def RoleFlow.inferAll {S : Type} {Sg : Sig S} (B : List ℕ) : List (XRecipe Sg) → ℕ → List (Line Sg) → List Role

The roles, line by line, from the base B: F holds the recipes chosen so far. A line becomes a conditioner if, with all later recipes, its arguments are known but its results are not; otherwise a spine step. A line without a partial inverse becomes a conditioner.

Equations

• One or more equations did not get rendered due to their size.
• RoleFlow.inferAll B x✝¹ x✝ [] = []

theorem RoleFlow.length_inferAll {S : Type} {Sg : Sig S} (B : List ℕ) (F : List (XRecipe Sg)) (n : ℕ) (ls : List (Line Sg)) : (inferAll B F n ls).length = ls.length

theorem RoleFlow.inferAll_known {S : Type} {Sg : Sig S} (B : List ℕ) (F : List (XRecipe Sg)) (n : ℕ) (ls : List (Line Sg)) {v : ℕ} : Known (F ++ xrecsAll n ls) {w : ℕ | w ∈ B} v → Known (F ++ xrecs n ls (inferAll B F n ls)) {w : ℕ | w ∈ B} v

The chosen roles reach what all recipes reach.

Programs

def RoleFlow.Prog.rolesAll {S : Type} {Sg : Sig S} (P : Prog Sg) : List Role

The roles chosen from the weights and the returned variables.

Equations

• P.rolesAll = RoleFlow.inferAll (List.range P.nw ++ P.ret) [] P.ctx₀.length P.lines

theorem RoleFlow.Prog.length_rolesAll {S : Type} {Sg : Sig S} (P : Prog Sg) : P.rolesAll.length = P.lines.length

theorem RoleFlow.Prog.base_eq {S : Type} {Sg : Sig S} (P : Prog Sg) : {w : ℕ | w ∈ List.range P.nw ++ P.ret} = {w : ℕ | w < P.nw} ∪ ↑P.ret.toFinset

theorem RoleFlow.Prog.invertible_rolesAll_of_known {S : Type} {Sg : Sig S} {P : Prog Sg} (hwf : P.WF) (hk : ∀ x ∈ List.range' P.nw P.ins.length, Known (xrecsAll P.ctx₀.length P.lines) ({w : ℕ | w < P.nw} ∪ ↑P.ret.toFinset) x) : P.Invertible P.rolesAll

theorem RoleFlow.Prog.exists_invertible_iff {S : Type} {Sg : Sig S} {P : Prog Sg} : (∃ (ρ : List Role), P.Invertible ρ) ↔ P.WF ∧ ∀ x ∈ List.range' P.nw P.ins.length, Known (xrecsAll P.ctx₀.length P.lines) ({w : ℕ | w < P.nw} ∪ ↑P.ret.toFinset) x

Invertibility under some roles is invertibility under all recipes at once.

theorem RoleFlow.Prog.invertible_rolesAll {S : Type} {Sg : Sig S} {P : Prog Sg} (h : ∃ (ρ : List Role), P.Invertible ρ) : P.Invertible P.rolesAll

rolesAll is complete: if any roles invert P, these do.

theorem RoleFlow.Prog.length_backward {S : Type} {Sg : Sig S} (n : ℕ) (ls : List (Line Sg)) (N : Finset ℕ) : (backward n ls N).1.length = ls.length

def RoleFlow.Prog.inferInv {S : Type} {Sg : Sig S} [DecidableEq S] (P : Prog Sg) : Option (List Role)

Inverse inference without density: the backward pass's roles if they invert P, and otherwise rolesAll if they do.

Equations

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

theorem RoleFlow.Prog.inferInv_sound {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [DecidableEq S] (h : P.inferInv = some ρ) : P.Invertible ρ

theorem RoleFlow.Prog.inferInv_invTyped {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [DecidableEq S] (h : P.inferInv = some ρ) : P.InvTyped ρ

The roles found have one role per line, so they also give an invertibility typing.

theorem RoleFlow.Prog.inferInv_of_infer {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [DecidableEq S] (h : P.infer = some ρ) : P.inferInv = some ρ

theorem RoleFlow.Prog.inferInv_complete {S : Type} {Sg : Sig S} {P : Prog Sg} {ρ : List Role} [DecidableEq S] (h : P.Invertible ρ) : P.inferInv.isSome = true

Completeness: if any roles invert P, inference succeeds.

theorem RoleFlow.Prog.inferInv_isSome_iff {S : Type} {Sg : Sig S} {P : Prog Sg} [DecidableEq S] : P.inferInv.isSome = true ↔ ∃ (ρ : List Role), P.InvTyped ρ