Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Symmetric algebraic branching programs

Lax461425.SymmetricABPs · concepts/Lax461425/SymmetricABPs.lean · lax-461425

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    An algebraic branching program (ABP) is a finite simple directed acyclic graph with affine edge labels, a unique source and a unique sink; it computes the sum over all source-to-sink paths of the product of the edge labels. An ABP in matrix variables is matrix-symmetric if every row and column permutation extends to an ABP automorphism, and its vertex orbits range over all such extending automorphisms. symVBPsymVBP is the class of families computed by matrix-symmetric ABPs with polynomial vertex orbits.

    Concept map
    8 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax461425.MatrixSymmetry
    2import Lax461425.SymmetricFamilies
    3import Lax461425.SymmetricClasses
    4import Lax461425.SymmetricVNP
    5import Lax461425.HomomorphismPolynomials
    6import Mathlib.LinearAlgebra.Span.Defs
    7import Mathlib.Data.Fintype.Pi
    8import Mathlib.Algebra.MvPolynomial.Rename
    9
    10/-!
    11---
    12title: Symmetric algebraic branching programs
    13type: definition
    14---
    15An algebraic branching program (ABP) is a finite simple directed acyclic graph with
    16affine edge labels, a unique source and a unique sink; it computes the sum over all
    17source-to-sink paths of the product of the edge labels. An ABP in matrix variables is
    18matrix-symmetric if every row and column permutation extends to an ABP automorphism, and
    19its vertex orbits range over all such extending automorphisms. `symVBP` is the class of
    20families computed by matrix-symmetric ABPs with polynomial vertex orbits.
    21-/
    22
    23namespace Lax461425.SymmetricABPs
    24
    25open Circuits MatrixSymmetry HomomorphismPolynomials
    26
    27/-- An affine linear form, with an explicit coefficient for every variable. -/
    28structure AffineForm (V K : Type*) where
    29 constant : K
    30 coeff : V → K
    31
    32/-- The polynomial represented by an affine form. -/
    33noncomputable def AffineForm.polynomial {V K : Type*} [Fintype V] [CommSemiring K]
    34 (a : AffineForm V K) : MvPolynomial V K :=
    35 MvPolynomial.C a.constant + ∑ x, MvPolynomial.C (a.coeff x) * MvPolynomial.X x
    36
    37/-- A finite directed acyclic ABP. Every vertex occurs on a source-to-sink path. -/
    38structure ABP (V K : Type*) where
    39 Vertex : Type
    40 [fintypeVertex : Fintype Vertex]
    41 [decEqVertex : DecidableEq Vertex]
    42 edge : Vertex → Vertex → Prop
    43 [decEdge : DecidableRel edge]
    44 label : Vertex → Vertex → AffineForm V K
    45 source : Vertex
    46 sink : Vertex
    47 source_no_incoming : ∀ v, ¬ edge v source
    48 sink_no_outgoing : ∀ v, ¬ edge sink v
    49 acyclic : ∀ v, ¬ Relation.TransGen edge v v
    50 source_reaches : ∀ v, Relation.ReflTransGen edge source v
    51 reaches_sink : ∀ v, Relation.ReflTransGen edge v sink
    52
    53attribute [instance] ABP.fintypeVertex ABP.decEqVertex ABP.decEdge
    54
    55namespace ABP
    56
    57variable {V K : Type*} (G : ABP V K)
    58
    59/-- A bounded vertex sequence. Acyclic paths have fewer edges than there are vertices. -/
    60abbrev PathData := (l : Fin (Fintype.card G.Vertex)) × (Fin (l.val + 1) → G.Vertex)
    61
    62/-- A vertex sequence traverses directed edges from the source to `v`. -/
    63def IsPathTo (v : G.Vertex) (p : G.PathData) : Prop :=
    64 p.2 0 = G.source ∧ p.2 (Fin.last p.1.val) = v ∧
    65 ∀ i : Fin p.1.val, G.edge (p.2 i.castSucc) (p.2 i.succ)
    66
    67/-- All directed paths from the source to a specified vertex. -/
    68abbrev PathTo (v : G.Vertex) := {p : G.PathData // G.IsPathTo v p}
    69
    70/-- A vertex sequence traverses directed edges from the source to the sink. -/
    71abbrev IsPath := G.IsPathTo G.sink
    72
    73/-- All source-to-sink paths, including the empty path when source and sink coincide. -/
    74abbrev Path := G.PathTo G.sink
    75
    76noncomputable instance (v : G.Vertex) : Fintype (G.PathTo v) := Fintype.ofFinite _
    77
    78/-- The product of the labels along a path with any endpoint. -/
    79noncomputable def pathWeightTo [Fintype V] [CommSemiring K] {v : G.Vertex}
    80 (p : G.PathTo v) : MvPolynomial V K :=
    81 ∏ i : Fin p.1.1.val,
    82 (G.label (p.1.2 i.castSucc) (p.1.2 i.succ)).polynomial
    83
    84/-- The product of the labels along a source-to-sink path. -/
    85noncomputable def pathWeight [Fintype V] [CommSemiring K] (p : G.Path) : MvPolynomial V K :=
    86 G.pathWeightTo p
    87
    88/-- The sum of all source-to-`v` path weights. -/
    89noncomputable def polynomialAt [Fintype V] [CommSemiring K] (v : G.Vertex) :
    90 MvPolynomial V K := ∑ p : G.PathTo v, G.pathWeightTo p
    91
    92/-- The sum of the weights of all source-to-sink paths. -/
    93noncomputable def polynomial [Fintype V] [CommSemiring K] : MvPolynomial V K :=
    94 G.polynomialAt G.sink
    95
    96/-- The ABP computes the given polynomial. -/
    97def Computes [Fintype V] [CommSemiring K] (p : MvPolynomial V K) : Prop :=
    98 G.polynomial = p
    99
    100/-- An ABP automorphism extending a renaming of the variables. Values of labels on
    101nonedges are immaterial. -/
    102def Extends [Fintype V] [CommSemiring K] (σ : G.Vertex ≃ G.Vertex) (π : V → V) : Prop :=
    103 σ G.source = G.source ∧ σ G.sink = G.sink ∧
    104 (∀ u v, G.edge (σ u) (σ v) ↔ G.edge u v) ∧
    105 ∀ u v, G.edge u v →
    106 (G.label (σ u) (σ v)).polynomial = MvPolynomial.rename π (G.label u v).polynomial
    107
    108variable {n : ℕ} (G : ABP (Fin n × Fin n) K)
    109
    110/-- Every matrix-variable permutation extends to an ABP automorphism. -/
    111def IsMatrixSymmetric [CommSemiring K] : Prop :=
    112 ∀ γ : Γ n, ∃ σ : G.Vertex ≃ G.Vertex, G.Extends σ (actVar γ)
    113
    114/-- The vertex orbit under all extending ABP automorphisms. -/
    115def orbit [CommSemiring K] (v : G.Vertex) : Set G.Vertex :=
    116 {w | ∃ (γ : Γ n) (σ : G.Vertex ≃ G.Vertex), G.Extends σ (actVar γ) ∧ σ v = w}
    117
    118/-- The largest vertex orbit under all extending ABP automorphisms. -/
    119noncomputable def orbitSize [CommSemiring K] : ℕ :=
    120 Finset.univ.sup fun v => (G.orbit v).ncard
    121
    122end ABP
    123
    124open SymmetricFamilies SymmetricClasses SymmetricVNP
    125
    126/-- Families computed by matrix-symmetric ABPs of polynomial vertex-orbit size. No bound on
    127the total size or the degree is imposed. -/
    128def InSymVBP {K : Type*} [CommSemiring K] (f : MatrixFamily K) : Prop :=
    129 ∃ b : ℕ → ℕ, PolynomiallyBounded b ∧ ∀ n, ∃ G : ABP (Fin n × Fin n) K,
    130 G.Computes (f n) ∧ G.IsMatrixSymmetric ∧ G.orbitSize ≤ b n
    131
    132end Lax461425.SymmetricABPs
    133
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…