Documentation

Complexitylib.Circuits.AC0.NormalForm.Defs

Negation-normal unbounded formulas for AC0 #

AC0Formula N is an unbounded-fan-in formula over exactly N variables. Negation occurs only in literal polarity, which is the representation needed by restriction and switching-lemma arguments. Unlike a circuit, this syntax is a tree and therefore records repeated subcomputations separately.

Children are stored in the mutually inductive AC0Forest. This gives Lean a direct structural induction principle for unbounded formulas; ofList and toList provide the usual list interface. Empty conjunctions and disjunctions denote true and false, respectively.

source
inductive Complexity.AC0Formula (N : ℕ) :
Type

A negation-normal Boolean formula with unbounded AND and OR gates.

Instances For
    source
    inductive Complexity.AC0Forest (N : ℕ) :
    Type

    A structurally recursive forest of unbounded-formula children.

    Instances For
      source
      @[implicit_reducible]
      instance Complexity.instReprAC0Formula {N✝ : ℕ} :
      Repr (AC0Formula N✝)
      Equations
      source
      partial def Complexity.instReprAC0Formula.repr_2 {N✝ : ℕ} :
      AC0Forest N✝ → ℕ → Std.Format
      source
      partial def Complexity.instReprAC0Formula.repr_1 {N✝ : ℕ} :
      AC0Formula N✝ → ℕ → Std.Format
      source
      partial def Complexity.instReprAC0Forest.repr_2 {N✝ : ℕ} :
      AC0Forest N✝ → ℕ → Std.Format
      source
      partial def Complexity.instReprAC0Forest.repr_1 {N✝ : ℕ} :
      AC0Formula N✝ → ℕ → Std.Format
      source
      @[implicit_reducible]
      instance Complexity.instReprAC0Forest {N✝ : ℕ} :
      Repr (AC0Forest N✝)
      Equations
      source
      @[implicit_reducible]
      instance Complexity.instDecidableEqAC0Formula {N✝ : ℕ} :
      DecidableEq (AC0Formula N✝)
      Equations
      source
      def Complexity.instDecidableEqAC0Formula.decEq_1 {N✝ : ℕ} (x✝ x✝¹ : AC0Formula N✝) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        def Complexity.instDecidableEqAC0Formula.decEq_2 {N✝ : ℕ} (x✝ x✝¹ : AC0Forest N✝) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          source
          @[implicit_reducible]
          instance Complexity.instDecidableEqAC0Forest {N✝ : ℕ} :
          DecidableEq (AC0Forest N✝)
          Equations
          source
          def Complexity.instDecidableEqAC0Forest.decEq_2 {N✝ : ℕ} (x✝ x✝¹ : AC0Forest N✝) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            def Complexity.instDecidableEqAC0Forest.decEq_1 {N✝ : ℕ} (x✝ x✝¹ : AC0Formula N✝) :
            Decidable (x✝ = x✝¹)
            Equations
            Instances For
              source
              def Complexity.AC0Forest.ofList {N : ℕ} :
              List (AC0Formula N) → AC0Forest N

              Convert a list to the structurally recursive forest representation.

              Equations
              Instances For
                source
                def Complexity.AC0Forest.toList {N : ℕ} :
                AC0Forest N → List (AC0Formula N)

                Convert a formula forest back to a list.

                Equations
                Instances For
                  source
                  def Complexity.AC0Forest.length {N : ℕ} :
                  AC0Forest N → ℕ

                  Number of formulas in a forest.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem Complexity.AC0Forest.toList_ofList {N : ℕ} (formulas : List (AC0Formula N)) :
                    (ofList formulas).toList = formulas
                    source
                    @[simp]
                    theorem Complexity.AC0Forest.ofList_toList {N : ℕ} (formulas : AC0Forest N) :
                    ofList formulas.toList = formulas

                    Converting a forest to a list and back is exact.

                    source
                    @[simp]
                    theorem Complexity.AC0Forest.length_ofList {N : ℕ} (formulas : List (AC0Formula N)) :
                    (ofList formulas).length = formulas.length
                    source
                    def Complexity.AC0Formula.eval {N : ℕ} (input : BitString N) :
                    AC0Formula N → Bool

                    Evaluate an unbounded formula on an N-bit input.

                    Equations
                    Instances For
                      source
                      def Complexity.AC0Formula.evalAll {N : ℕ} (input : BitString N) :
                      AC0Forest N → Bool

                      Evaluate a forest as a conjunction.

                      Equations
                      Instances For
                        source
                        def Complexity.AC0Formula.evalAny {N : ℕ} (input : BitString N) :
                        AC0Forest N → Bool

                        Evaluate a forest as a disjunction.

                        Equations
                        Instances For
                          source
                          def Complexity.AC0Formula.size {N : ℕ} :
                          AC0Formula N → ℕ

                          Total tree size, counting constants, literal occurrences, and gates.

                          Equations
                          Instances For
                            source
                            def Complexity.AC0Formula.forestSize {N : ℕ} :
                            AC0Forest N → ℕ

                            Sum of the tree sizes in a forest.

                            Equations
                            Instances For
                              source
                              def Complexity.AC0Formula.depth {N : ℕ} :
                              AC0Formula N → ℕ

                              Formula depth. Leaves have depth zero and every unbounded gate adds one.

                              Equations
                              Instances For
                                source
                                def Complexity.AC0Formula.forestDepth {N : ℕ} :
                                AC0Forest N → ℕ

                                Maximum formula depth in a forest.

                                Equations
                                Instances For
                                  source
                                  theorem Complexity.AC0Formula.depth_le_forestDepth_of_mem {N : ℕ} (formula : AC0Formula N) (formulas : AC0Forest N) (hmem : formula ∈ formulas.toList) :
                                  formula.depth ≤ forestDepth formulas

                                  Every member of a forest has depth at most the forest maximum.

                                  source
                                  def Complexity.AC0Formula.vars {N : ℕ} :
                                  AC0Formula N → Finset (Fin N)

                                  The finite set of input variables mentioned by a formula.

                                  Equations
                                  Instances For
                                    source
                                    def Complexity.AC0Formula.forestVars {N : ℕ} :
                                    AC0Forest N → Finset (Fin N)

                                    Union of the variable supports of every formula in a forest.

                                    Equations
                                    Instances For
                                      source
                                      def Complexity.AC0Formula.neg {N : ℕ} :
                                      AC0Formula N → AC0Formula N

                                      De Morgan negation, retaining negation-normal form.

                                      Equations
                                      Instances For
                                        source
                                        def Complexity.AC0Formula.negForest {N : ℕ} :
                                        AC0Forest N → AC0Forest N

                                        Negate every formula in a forest.

                                        Equations
                                        Instances For
                                          source
                                          def Complexity.AC0Formula.ofOp {N : ℕ} (op : AndOrOp) (children : AC0Forest N) :
                                          AC0Formula N

                                          Build the gate selected by an AND/OR operation.

                                          Equations
                                          Instances For
                                            source
                                            def Complexity.AC0Formula.andList {N : ℕ} (children : List (AC0Formula N)) :
                                            AC0Formula N

                                            Build an unbounded conjunction from an ordinary list.

                                            Equations
                                            Instances For
                                              source
                                              def Complexity.AC0Formula.orList {N : ℕ} (children : List (AC0Formula N)) :
                                              AC0Formula N

                                              Build an unbounded disjunction from an ordinary list.

                                              Equations
                                              Instances For
                                                source
                                                theorem Complexity.AC0Formula.one_le_size {N : ℕ} (formula : AC0Formula N) :
                                                1 ≤ formula.size

                                                Every AC0 formula has at least one syntax-tree node.