Documentation

WeightedNetKAT.Papers.PLDI2026

Definitions, lemmas and theorems listed in order #

This file contains links to all definitions, lemmas and theorems from the paper.

They are listed roughly in the order they appear in the paper. This file should serve as a jumping off point to navigate and explore the formalization, and not as a reference to how things are defined. We invite the reader to click on the names in each definition to jump to their original definition. In Visual Studio Code one can Ctrl/CMD+Click on symbols to jump to their definition.

Section 3 – wNetKAT: Syntax and Semantics #

source
def WeightedNetKAT.Paper.PLDI2026.Section3.Definition1 :
Paper.Link Countsupp
Equations
Instances For
    source
    def WeightedNetKAT.Paper.PLDI2026.Section3.Figure6 {F N 𝒮 : Type} [DecidableEq F] [Listed F] [DecidableEq N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {p : Pol[F,N,𝒮]} {t : Pred[F,N]} :
    Paper.Link (Pol[F,N,𝒮], p.sem, t.test)
    Equations
    Instances For
      source
      def WeightedNetKAT.Paper.PLDI2026.Section3.Figure7 {F N 𝒮 : Type} [Listed F] :
      Paper.Link (RPol 𝒮)
      Equations
      Instances For

        Section 4 – Language Model #

        source
        theorem WeightedNetKAT.Paper.PLDI2026.Section4.Inline1 :
        Paper.Link GS
        source
        def WeightedNetKAT.Paper.PLDI2026.Section4.Definition2 {F N 𝒮 : Type} [DecidableEq F] [Listed F] [DecidableEq N] [Listed N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {p' : RPol 𝒮} :
        Paper.Link G⟦~p'⟧
        Equations
        Instances For
          source
          theorem WeightedNetKAT.Paper.PLDI2026.Section4.Lemma1 {F N 𝒮 : Type} [DecidableEq F] [Listed F] [Inhabited F] [DecidableEq N] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p' : RPol 𝒮} :
          Paper.LinkLem (p'.sem = fun (h : Pk[F,N] × List Pk[F,N]) => ω∑ (x : ↑G⟦~p'⟧.support), G⟦~p'⟧ ↑x * (↑x).sem h)

          Section 5 – wNetKAT Automata #

          source
          def WeightedNetKAT.Paper.PLDI2026.Section5.Definition3 {F N 𝒮 : Type} [Listed F] [Semiring 𝒮] {p' : RPol 𝒮} :
          Paper.Link WNKA[F,N,𝒮,S p']
          Equations
          Instances For
            source
            theorem WeightedNetKAT.Paper.PLDI2026.Section5.Inline1 {F N 𝒮 : Type} [DecidableEq F] [Listed F] [Inhabited F] [DecidableEq N] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p' : RPol 𝒮} :
            Paper.Link RPol.𝒜⟦~p'⟧
            source
            theorem WeightedNetKAT.Paper.PLDI2026.Section5.Table1 {F N 𝒮 : Type} [DecidableEq F] [Listed F] [Inhabited F] [DecidableEq N] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p' : RPol 𝒮} :
            Paper.Link (S p', p'.wnka.ι, p'.wnka.δ, p'.wnka.𝒪)

            We use 𝒪 in stead of λ due it it being reserved for lambda functions in lean

            source
            theorem WeightedNetKAT.Paper.PLDI2026.Section5.Lemma2 {F N 𝒮 : Type} [DecidableEq F] [Listed F] [Inhabited F] [DecidableEq N] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p' : RPol 𝒮} :
            Paper.LinkLem (RPol.𝒜⟦~p'⟧ = G⟦~p'⟧)
            source
            theorem WeightedNetKAT.Paper.PLDI2026.Section5.Corollary1 {F N 𝒮 : Type} [DecidableEq F] [Listed F] [Inhabited F] [DecidableEq N] [Listed N] [Inhabited N] [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] [KStar 𝒮] [LawfulKStar 𝒮] [MulLeftMono 𝒮] [MulRightMono 𝒮] [OmegaContinuousNonUnitalSemiring 𝒮] {p : Pol[F,N,𝒮]} :
            Paper.LinkCol (∀ (π : Pk[F,N]) (h : Pk[F,N] × List Pk[F,N]), (p.sem (π, [])) h = RPol.𝒜⟦~p.toRPol⟧ (π, h.2.reverse, h.1))
            source
            def WeightedNetKAT.Paper.PLDI2026.Section5.Definition4 {𝒮 : Type} [Semiring 𝒮] [OmegaCompletePartialOrder 𝒮] [OrderBot 𝒮] [IsPositiveOrderedAddMonoid 𝒮] {n : Type} [Fintype n] [DecidableEq n] :
            Paper.Link Matrix.KStar.instKStar
            Equations
            Instances For