def Listed.«termLi[_]» : Lean.ParserDescr

Equations

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

def Listed.Li.getSum {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] : Fin (size (α ⊕ β)) ≃ Fin (size α) ⊕ Fin (size β)

Equations

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

def Listed.Li.getProd {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] : Fin (size (α × β)) ≃ Fin (size α) × Fin (size β)

Equations

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

theorem Listed.decodeFin_getSum {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] (i : Fin (size (α ⊕ β))) : decodeFin i = Sum.map decodeFin decodeFin (Li.getSum i)

theorem Listed.decodeFin_getProd {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] (i : Fin (size (α × β))) : decodeFin i = Prod.map decodeFin decodeFin (Li.getProd i)

@[simp]

theorem Listed.Li.getSum_encodeFin {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] (i : α ⊕ β) : getSum (encodeFin i) = Sum.map encodeFin encodeFin i

@[simp]

theorem Listed.Li.getProd_encodeFin {α : Type u_1} {β : Type u_2} [Listed α] [Listed β] (i : α × β) : getProd (encodeFin i) = Prod.map encodeFin encodeFin i

@[simp]

theorem Listed.array_sum_eq_finset_sum {ι : Type u_1} {α : Type u_2} [Listed ι] [AddCommMonoid α] (f : ι → α) : (Array.map f array).sum = ∑ i : Fin (size ι), f (decodeFin i)

structure WeightedNetKAT.EWNKA (F : Type u_4) (N : Type u_5) (𝒮 : Type u_6) (Q : Type u_7) [Semiring 𝒮] [Listed F] [Listed N] [Listed Q] : Type u_6

An efficient version of [WNKA] that uses explicit matrices.

• ι : EMatrix Unit Q 𝒮

  ι is the initial weightings.

• δ : EMatrix Pk[F,N] Pk[F,N] (EMatrix Q Q 𝒮)

  δ is a family of transition functions δ[α,β] : Q → 𝒞 𝒮 Q indexed by packet pairs.

• 𝒪 : EMatrix Pk[F,N] Pk[F,N] (EMatrix Q Unit 𝒮)

  𝒪 is a family of output weightings 𝒪[α,β] : 𝒞 𝒮 Q indexed by packet pairs. Note that we use 𝒪 instead of λ, since λ is the function symbol in Lean.

def WeightedNetKAT.«termEWNKA[_,_,_,_]» : Lean.ParserDescr

Equations

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

def WeightedNetKAT.S.EC {𝒮 : Type u_3} {X : Type u_4} {Y : Type u_5} [Listed X] [Listed Y] : EMatrix Unit X 𝒮 → EMatrix Unit Y 𝒮 → EMatrix Unit (X ⊕ Y) 𝒮

Equations

• EC[m₁,m₂] = EMatrix.ofFn fun (x : Li[Unit]) (x_1 : Li[X ⊕ Y]) => Sum.elim (fun (x : Li[X]) => m₁.asNMatrix 0 x) (fun (x : Li[Y]) => m₂.asNMatrix 0 x) (Listed.Li.getSum x_1)

def WeightedNetKAT.«termEC[_,_]» : Lean.ParserDescr

Equations

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

@[simp]

theorem WeightedNetKAT.S.EC_eq_C {𝒮 : Type u_3} {X : Type u_4} {Y : Type u_5} [Listed X] [Listed Y] {m₁ : EMatrix Unit X 𝒮} {m₂ : EMatrix Unit Y 𝒮} {i : Unit} {j : X ⊕ Y} : EC[m₁,m₂] i j = m₁.asMatrix.fromCols m₂.asMatrix i j

def WeightedNetKAT.S.ER {𝒮 : Type u_3} {X : Type u_4} {Y : Type u_5} [Listed X] [Listed Y] : EMatrix X Unit 𝒮 → EMatrix Y Unit 𝒮 → EMatrix (X ⊕ Y) Unit 𝒮

Equations

• ER[m₁,m₂] = EMatrix.ofFn fun (x : Li[X ⊕ Y]) (x_1 : Li[Unit]) => Sum.elim (fun (x : Li[X]) => m₁.asNMatrix x 0) (fun (x : Li[Y]) => m₂.asNMatrix x 0) (Listed.Li.getSum x)

def WeightedNetKAT.«termER[_,_]» : Lean.ParserDescr

Equations

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

@[simp]

theorem WeightedNetKAT.S.ER_eq_C {𝒮 : Type u_3} {X : Type u_4} {Y : Type u_5} [Listed X] [Listed Y] {m₁ : EMatrix X Unit 𝒮} {m₂ : EMatrix Y Unit 𝒮} {i : X ⊕ Y} {j : Unit} : ER[m₁,m₂] i j = m₁.asMatrix.fromRows m₂.asMatrix i j

def EMatrix.fromBlocks {𝒮 : Type u_3} {X : Type u_4} {Y : Type u_5} {Z : Type u_6} {W : Type u_7} [Listed X] [Listed Y] [Listed Z] [Listed W] : EMatrix X Y 𝒮 → EMatrix X W 𝒮 → EMatrix Z Y 𝒮 → EMatrix Z W 𝒮 → EMatrix (X ⊕ Z) (Y ⊕ W) 𝒮

Equations

• EMatrix.fromBlocks = NMatrix.fromBlocks

def WeightedNetKAT.«termEB[[_,_],[_,_]]» : Lean.ParserDescr

Equations

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

@[simp]

theorem WeightedNetKAT.S.EB_eq_δ {𝒮 : Type u_3} {X : Type u_4} {Y : Type u_5} {Z : Type u_6} {W : Type u_7} [Listed X] [Listed Y] [Listed Z] [Listed W] (mxy : EMatrix X Y 𝒮) (mxw : EMatrix X W 𝒮) (mzy : EMatrix Z Y 𝒮) (mzw : EMatrix Z W 𝒮) {i : X ⊕ Z} {j : Y ⊕ W} : EB[[mxy,mxw],[mzy,mzw]] i j = Matrix.fromBlocks mxy.asMatrix mxw.asMatrix mzy.asMatrix mzw.asMatrix i j

@[reducible, inline]

abbrev WeightedNetKAT.Eη₂ {𝒮 : Type u_3} [Semiring 𝒮] {X : Type u_4} {Y : Type u_5} [instX : Listed X] [instY : Listed Y] (i : X) (j : Y) : EMatrix X Y 𝒮

Equations

• WeightedNetKAT.Eη₂ i j = EMatrix.ofFn fun (i' : Li[X]) (j' : Li[Y]) => if Listed.encode i = ↑i' ∧ Listed.encode j = ↑j' then 1 else 0

def WeightedNetKAT.EC {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] (p : RPol 𝒮) : EMatrix Unit (S p) 𝒮

Equations

• WeightedNetKAT.EC WeightedNetKAT.RPol.Drop = WeightedNetKAT.Eη₂ () ()
• WeightedNetKAT.EC wnk_rpol {skip} = WeightedNetKAT.Eη₂ () ()
• WeightedNetKAT.EC wnk_rpol {@test ~pk} = WeightedNetKAT.Eη₂ () ()
• WeightedNetKAT.EC wnk_rpol {@mod ~pk} = WeightedNetKAT.Eη₂ () ()
• WeightedNetKAT.EC wnk_rpol {dup} = WeightedNetKAT.Eη₂ () (Sum.inl ())
• WeightedNetKAT.EC wnk_rpol {~w ⨀ ~p₁} = w • WeightedNetKAT.EC p₁
• WeightedNetKAT.EC wnk_rpol {~p₁ ⨁ ~p₂} = EC[WeightedNetKAT.EC p₁,WeightedNetKAT.EC p₂]
• WeightedNetKAT.EC wnk_rpol {~p₁; ~q} = EC[WeightedNetKAT.EC p₁,0]
• WeightedNetKAT.EC wnk_rpol {~p_2*} = EC[0,1]

def WeightedNetKAT.boxₑ {Pk : Type u_4} [Listed Pk] {X : Type u_7} [Listed X] {Q : Type u_5} [Mul Q] [AddCommMonoid Q] {Z : Type u_6} [Listed Z] [Unique Z] (l : EMatrix Z X Q) (r : EMatrix Pk Pk (EMatrix X Z Q)) : EMatrix Pk Pk Q

Equations

• (l ⊠ₑ r) = EMatrix.ofFn fun (α β : Li[Pk]) => (l * r.asNMatrix α β).asNMatrix ⟨0, ⋯⟩ ⟨0, ⋯⟩

def WeightedNetKAT.«term_⊠ₑ_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊠ₑ_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊠ₑ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊠ₑ ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem Liste.decodeFin_unique {α : Type u_5} [Listed α] [Unique α] (i : Li[α]) : Listed.decodeFin i = default

@[simp]

theorem WeightedNetKAT.boxₑ_eq_box {Pk : Type u_4} [Listed Pk] {X : Type u_7} [Listed X] [Fintype X] {Q : Type u_5} [Mul Q] [AddCommMonoid Q] {Z : Type u_6} [Listed Z] [Unique Z] (l : EMatrix Z X Q) (r : EMatrix Pk Pk (EMatrix X Z Q)) : (l ⊠ₑ r) = EMatrix.ofMatrix (l.asMatrix ⊠ r.asMatrix₂)

def WeightedNetKAT.foxₑ {Pk : Type u_4} [Listed Pk] {A : Type u_5} {B : Type u_6} {C : Type u_7} {Q : Type u_8} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [Listed C] (l : EMatrix A B Q) (r : EMatrix Pk Pk (EMatrix B C Q)) : EMatrix Pk Pk (EMatrix A C Q)

Equations

• (l ⊡ₑ r) = EMatrix.ofFn fun (α β : Li[Pk]) => l * r.asNMatrix α β

def WeightedNetKAT.«term_⊡ₑ_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊡ₑ_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊡ₑ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊡ₑ ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem WeightedNetKAT.foxₑ_eq_fox {Pk : Type u_4} [Listed Pk] {A : Type u_5} {B : Type u_6} {C : Type u_7} {Q : Type u_8} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [Listed C] [Fintype A] [Fintype B] [Fintype C] (l : EMatrix A B Q) (r : EMatrix Pk Pk (EMatrix B C Q)) : (l ⊡ₑ r) = EMatrix.ofMatrix₂ (l.asMatrix ⊡ r.asMatrix₂)

@[inline, specialize #[]]

def WeightedNetKAT.soxₑ {Pk : Type u_4} [Listed Pk] {A : Type u_5} {B : Type u_6} {Q : Type u_7} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] (l : EMatrix Pk Pk Q) (r : EMatrix Pk Pk (EMatrix A B Q)) : EMatrix Pk Pk (EMatrix A B Q)

Equations

• (l ⊟ₑ r) = EMatrix.ofFn fun (α β : Li[Pk]) => ∑ m : Li[Pk], l.asNMatrix α m • r.asNMatrix m β

def WeightedNetKAT.«term_⊟ₑ_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊟ₑ_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊟ₑ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊟ₑ ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem WeightedNetKAT.soxₑ_eq_sox {Pk : Type u_4} [Listed Pk] {A : Type u_5} {B : Type u_6} {Q : Type u_7} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [Fintype A] [Fintype B] [Fintype Pk] (l : EMatrix Pk Pk Q) (r : EMatrix Pk Pk (EMatrix A B Q)) : (l ⊟ₑ r) = EMatrix.ofMatrix₂ (l.asMatrix ⊟> r.asMatrix₂)

def WeightedNetKAT.sox'ₑ {Pk : Type u_4} [Listed Pk] {A : Type u_5} {B : Type u_6} {Q : Type u_7} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] (l : EMatrix Pk Pk (EMatrix A B Q)) (r : EMatrix Pk Pk Q) : EMatrix Pk Pk (EMatrix A B Q)

Equations

• (l ⊟'ₑ r) = EMatrix.ofFn fun (α β : Li[Pk]) => ∑ m : Li[Pk], MulOpposite.op (r.asNMatrix m β) • l.asNMatrix α m

def WeightedNetKAT.«term_⊟'ₑ_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊟'ₑ_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊟'ₑ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊟'ₑ ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem WeightedNetKAT.sox'ₑ_eq_sox' {Pk : Type u_4} [Listed Pk] {A : Type u_5} {B : Type u_6} {Q : Type u_7} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [Fintype A] [Fintype B] [Fintype Pk] (l : EMatrix Pk Pk (EMatrix A B Q)) (r : EMatrix Pk Pk Q) : (l ⊟'ₑ r) = EMatrix.ofMatrix₂ (l.asMatrix₂ <⊟ r.asMatrix)

def WeightedNetKAT.croxₑ {Pk : Type u_4} [Listed Pk] {A : Type u_5} {B : Type u_6} {C : Type u_7} {Q : Type u_8} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [Listed C] (l : EMatrix Pk Pk (EMatrix A B Q)) (r : EMatrix Pk Pk (EMatrix B C Q)) : EMatrix Pk Pk (EMatrix A C Q)

Equations

• (l ⊞ₑ r) = EMatrix.ofFn fun (α β : Li[Pk]) => ∑ m : Li[Pk], l.asNMatrix α m * r.asNMatrix m β

def WeightedNetKAT.«term_⊞ₑ_» : Lean.TrailingParserDescr

Equations

• WeightedNetKAT.«term_⊞ₑ_» = Lean.ParserDescr.trailingNode `WeightedNetKAT.«term_⊞ₑ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊞ₑ ") (Lean.ParserDescr.cat `term 50))

@[simp]

theorem WeightedNetKAT.croxₑ_eq_crox {Pk : Type u_4} [Listed Pk] {A : Type u_5} {B : Type u_6} {C : Type u_7} {Q : Type u_8} [AddCommMonoid Q] [Mul Q] [Listed A] [Listed B] [Listed C] [Fintype A] [Fintype B] [Fintype C] [Fintype Pk] (l : EMatrix Pk Pk (EMatrix A B Q)) (r : EMatrix Pk Pk (EMatrix B C Q)) : (l ⊞ₑ r) = EMatrix.ofMatrix₂ (l.asMatrix₂ ⊞ r.asMatrix₂)

def WeightedNetKAT.RPol.ER {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [KStar 𝒮] [Listed N] (p : RPol 𝒮) : EMatrix Pk[F,N] Pk[F,N] (EMatrix (S p) Unit 𝒮)

Equations

• One or more equations did not get rendered due to their size.
• WeightedNetKAT.RPol.Drop.ER = 0
• wnk_rpol {skip}.ER = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => if α = β then EMatrix.ofFn fun (x : Li[WeightedNetKAT.S wnk_rpol {skip}]) => 1 else 0
• wnk_rpol {@test ~γ}.ER = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => if α = β ∧ ↑β = Listed.encode γ then EMatrix.ofFn fun (x : Li[WeightedNetKAT.S wnk_rpol {@test ~γ}]) => 1 else 0
• wnk_rpol {@mod ~π}.ER = EMatrix.ofFn fun (x β : Li[Pk[F,N]]) => if ↑β = Listed.encode π then EMatrix.ofFn fun (x : Li[WeightedNetKAT.S wnk_rpol {@mod ~π}]) => 1 else 0
• wnk_rpol {dup}.ER = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => if α = β then WeightedNetKAT.Eη₂ (Sum.inr ()) () else 0
• wnk_rpol {~w ⨀ ~p₁}.ER = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => p₁.ER.getN α β
• wnk_rpol {~p₁ ⨁ ~p₂}.ER = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => ER[p₁.ER.getN α β,p₂.ER.getN α β]

def WeightedNetKAT.RPol.ER_heart {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [KStar 𝒮] [Listed N] [DecidableEq N] (p₁ : RPol 𝒮) : EMatrix Pk[F,N] Pk[F,N] 𝒮

Equations

• p₁.ER_heart = KStar.kstar (WeightedNetKAT.EC p₁ ⊠ₑ p₁.ER)

theorem WeightedNetKAT.RPol.ER_iter {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [KStar 𝒮] [Listed N] [DecidableEq N] (p₁ : RPol 𝒮) : wnk_rpol {~p₁*}.ER = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => ER[∑ γ : Li[Pk[F,N]], MulOpposite.op (p₁.ER_heart.asNMatrix γ β) • p₁.ER.asNMatrix α γ,EMatrix.ofFn fun (x x_1 : Li[Unit]) => p₁.ER_heart.asNMatrix α β]

@[simp]

theorem WeightedNetKAT.RPol.EMatrix.asMatrix_one {X : Type u_4} {α : Type u_5} [Listed X] [DecidableEq X] [Zero α] [One α] : EMatrix.asMatrix 1 = 1

@[simp]

theorem WeightedNetKAT.RPol.EC_eq_C {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] {p : RPol 𝒮} : EC p = EMatrix.ofMatrix p.ι

theorem WeightedNetKAT.RPol.ER_heart_eq_𝒪_heart {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [DecidableEq F] [Listed N] [DecidableEq N] [LawfulKStar (NMatrix (Listed.size Pk[F,N]) (Listed.size Pk[F,N]) 𝒮)] {p : RPol 𝒮} (h : p.ER = EMatrix.ofMatrix₂ p.𝒪) : p.ER_heart = EMatrix.ofMatrix p.𝒪_heart

theorem EMatrix.apply_encodeFin {m : Type u_4} {n : Type u_5} {α : Type u_6} [Listed m] [Listed n] {M : NMatrix (Listed.size m) (Listed.size n) α} {i : m} {j : n} : M i j = M (Listed.encodeFin i) (Listed.encodeFin j)

@[simp]

theorem WeightedNetKAT.RPol.ER_eq_C {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [DecidableEq F] [Listed N] [DecidableEq N] [LawfulKStar (NMatrix (Listed.size Pk[F,N]) (Listed.size Pk[F,N]) 𝒮)] {p : RPol 𝒮} : p.ER = EMatrix.ofMatrix₂ p.𝒪

def WeightedNetKAT.RPol.ι_aux {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] (p : RPol 𝒮) : Matrix Unit (S p) 𝒮

Equations

• p.ι_aux = (WeightedNetKAT.EC p).asMatrix

def WeightedNetKAT.RPol.𝒪_aux {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [KStar 𝒮] [Listed N] (p : RPol 𝒮) : Matrix Pk[F,N] Pk[F,N] (Matrix (S p) Unit 𝒮)

Equations

• p.𝒪_aux = p.ER.asMatrix₂

def WeightedNetKAT.RPol.EB {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [KStar 𝒮] [Listed N] [DecidableEq N] (p : RPol 𝒮) : EMatrix Pk[F,N] Pk[F,N] (EMatrix (S p) (S p) 𝒮)

Equations

• One or more equations did not get rendered due to their size.
• WeightedNetKAT.RPol.Drop.EB = EMatrix.ofFn fun (x x_1 : Li[Pk[F,N]]) => 0
• wnk_rpol {skip}.EB = EMatrix.ofFn fun (x x_1 : Li[Pk[F,N]]) => 0
• wnk_rpol {@test ~pk}.EB = EMatrix.ofFn fun (x x_1 : Li[Pk[F,N]]) => 0
• wnk_rpol {@mod ~pk}.EB = EMatrix.ofFn fun (x x_1 : Li[Pk[F,N]]) => 0
• wnk_rpol {dup}.EB = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => EMatrix.ofFn fun (s : Li[WeightedNetKAT.S wnk_rpol {dup}]) => if s = 0 ∧ α = β then WeightedNetKAT.η₁ 1 else 0
• wnk_rpol {~w ⨀ ~p₁}.EB = p₁.EB
• wnk_rpol {~p₁ ⨁ ~p₂}.EB = EMatrix.ofFn fun (α β : Li[Pk[F,N]]) => EB[[p₁.EB.getN α β,0],[0,p₂.EB.getN α β]]

@[simp]

theorem WeightedNetKAT.RPol.EB_eq_δ {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [DecidableEq F] [Listed N] [DecidableEq N] [LawfulKStar (NMatrix (Listed.size Pk[F,N]) (Listed.size Pk[F,N]) 𝒮)] {p : RPol 𝒮} : p.EB = EMatrix.ofMatrix₂ p.δ

def WeightedNetKAT.RPol.δ_aux {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [KStar 𝒮] [Listed N] [DecidableEq N] (p : RPol 𝒮) : Matrix Pk[F,N] Pk[F,N] (Matrix (S p) (S p) 𝒮)

Equations

• p.δ_aux = p.EB.asMatrix₂

def WeightedNetKAT.RPol.ewnka {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [KStar 𝒮] [Listed N] [DecidableEq N] (p : RPol 𝒮) : EWNKA[F,N,𝒮,S p]

Equations

• p.ewnka = { ι := WeightedNetKAT.EC p, δ := p.EB, 𝒪 := p.ER }

def WeightedNetKAT.WNKA.toEWNKA {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] (𝔄 : WNKA[F,N,𝒮,Q]) : EWNKA[F,N,𝒮,Q]

Equations

• 𝔄.toEWNKA = { ι := EMatrix.ofMatrix 𝔄.ι, δ := EMatrix.ofMatrix₂ 𝔄.δ, 𝒪 := EMatrix.ofMatrix₂ 𝔄.𝒪 }

def WeightedNetKAT.EWNKA.toWNKA {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) : WNKA[F,N,𝒮,Q]

Equations

• 𝔈.toWNKA = { ι := 𝔈.ι.asMatrix, δ := 𝔈.δ.asMatrix₂, 𝒪 := 𝔈.𝒪.asMatrix₂ }

@[simp]

theorem WeightedNetKAT.WNKA.toWNKA_toEWNKA {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] (𝔄 : WNKA[F,N,𝒮,Q]) : 𝔄.toEWNKA.toWNKA = 𝔄

@[simp]

theorem WeightedNetKAT.EWNKA.toEWNKA_toWNKA {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) : 𝔈.toWNKA.toEWNKA = 𝔈

@[simp]

theorem WeightedNetKAT.RPol.wnka_toEWNKA {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [Listed N] [DecidableEq F] [DecidableEq N] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] (p : RPol 𝒮) : p.wnka.toEWNKA = p.ewnka

@[simp]

theorem WeightedNetKAT.RPol.ewnka_toWNKA {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [Listed N] [DecidableEq F] [DecidableEq N] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] (p : RPol 𝒮) : p.ewnka.toWNKA = p.wnka

def WeightedNetKAT.RPol.wnka_fast {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] [DecidableEq N] [KStar 𝒮] (p : RPol 𝒮) : WNKA[F,N,𝒮,S p]

Equations

• p.wnka_fast = p.ewnka.toWNKA

@[simp]

def WeightedNetKAT.EWNKA.toEWNKA_ι_apply {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) {α : Unit} {β : Q} : 𝔈.toWNKA.ι α β = 𝔈.ι α β

Equations

• ⋯ = ⋯

@[simp]

def WeightedNetKAT.EWNKA.toEWNKA_δ_apply {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) {α β : Pk[F,N]} : 𝔈.toWNKA.δ α β = (𝔈.δ α β).asMatrix

Equations

• ⋯ = ⋯

@[simp]

def WeightedNetKAT.EWNKA.toEWNKA_𝒪_apply {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) {α β : Pk[F,N]} : 𝔈.toWNKA.𝒪 α β = (𝔈.𝒪 α β).asMatrix

Equations

• ⋯ = ⋯

def WeightedNetKAT.EWNKA.sem {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] [DecidableEq N] (𝒜 : EWNKA[F,N,𝒮,Q]) : GS F N →c 𝒮

Equations

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

structure WeightedNetKAT.EWNKA.Precompute {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] (𝔈 : EWNKA[F,N,𝒮,Q]) : Type (max u_2 u_3)

Stores partial computation of the weight of a trace.

We want to compute the prefix as little as possible, and reuse it the final computation with 𝒪. This structure turned out to be crucial for performance, as Lean would push the computation of the prefix into the lambda where the final β was given, leading it to recomputing the prefix for every final packet.

This gives roughly a |Pk[F,N]| times speed up.

• m : EMatrix Unit Q 𝒮
• γ : Pk[F,N]

@[inline, specialize #[]]

def WeightedNetKAT.EWNKA.Precompute.finish {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] {𝔈 : EWNKA[F,N,𝒮,Q]} (p : 𝔈.Precompute) (β : Pk[F,N]) : 𝒮

Equations

• p.finish β = (p.m * 𝔈.𝒪 p.γ β) () ()

@[noinline, specialize #[]]

def WeightedNetKAT.EWNKA.semArray_aux {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] (𝒜 : EWNKA[F,N,𝒮,Q]) (α_xs : Array Pk[F,N]) (h : 0 < α_xs.size) : 𝒜.Precompute

Equations

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

@[inline, specialize #[]]

def WeightedNetKAT.EWNKA.semArray {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] (𝒜 : EWNKA[F,N,𝒮,Q]) (α_xs : Array Pk[F,N]) (h : 0 < α_xs.size) : 𝒜.Precompute

Equations

• 𝒜.semArray α_xs h = 𝒜.semArray_aux α_xs h

theorem WeightedNetKAT.EWNKA.semArray_eq_sem {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [Listed N] {Q : Type u_4} [Listed Q] [DecidableEq N] {𝔈 : EWNKA[F,N,𝒮,Q]} {α_xs : Array Pk[F,N]} {β : Pk[F,N]} (h : 0 < α_xs.size) : (𝔈.semArray α_xs h).finish β = 𝔈.sem (α_xs.toList.head ⋯, α_xs.toList.tail, β)

theorem WeightedNetKAT.RPol.ewnka_sem_eq_wnka_sem {F : Type u_1} [Listed F] {N : Type u_2} {𝒮 : Type u_3} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [Listed N] [DecidableEq F] [DecidableEq N] [KStar 𝒮] [LawfulKStar 𝒮] [KStarIter 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] (p : RPol 𝒮) : p.ewnka.sem = 𝒜⟦~p⟧