Documentation

Complexitylib.Circuits.AC0.Restriction

Restricting negation-normal AC0 formulas #

Finite-arity restrictions substitute fixed literals by constants while retaining the unbounded connective tree. Evaluation commutes with this operation, tree size and depth are preserved exactly, and variable support is filtered to the free variables.

source
def Complexity.AC0Formula.restrict {N : ℕ} (restriction : Restriction.On N) :
AC0Formula N → AC0Formula N

Apply a finite-arity restriction to an AC0 formula.

Equations
Instances For
    source
    def Complexity.AC0Formula.restrictForest {N : ℕ} (restriction : Restriction.On N) :
    AC0Forest N → AC0Forest N

    Apply a restriction to every formula in a forest.

    Equations
    Instances For
      source
      theorem Complexity.AC0Formula.eval_restrict {N : ℕ} (restriction : Restriction.On N) (input : BitString N) (formula : AC0Formula N) :
      eval input (restrict restriction formula) = eval (restriction.applyTo input) formula

      Evaluation commutes with restricting an AC0 formula.

      source
      theorem Complexity.AC0Formula.evalAll_restrictForest {N : ℕ} (restriction : Restriction.On N) (input : BitString N) (formulas : AC0Forest N) :
      evalAll input (restrictForest restriction formulas) = evalAll (restriction.applyTo input) formulas

      Conjunctive forest evaluation commutes with restriction.

      source
      theorem Complexity.AC0Formula.evalAny_restrictForest {N : ℕ} (restriction : Restriction.On N) (input : BitString N) (formulas : AC0Forest N) :
      evalAny input (restrictForest restriction formulas) = evalAny (restriction.applyTo input) formulas

      Disjunctive forest evaluation commutes with restriction.

      source
      theorem Complexity.AC0Formula.size_restrict {N : ℕ} (restriction : Restriction.On N) (formula : AC0Formula N) :
      (restrict restriction formula).size = formula.size

      Restriction preserves total syntax-tree size exactly.

      source
      theorem Complexity.AC0Formula.forestSize_restrictForest {N : ℕ} (restriction : Restriction.On N) (formulas : AC0Forest N) :
      forestSize (restrictForest restriction formulas) = forestSize formulas

      Restriction preserves total forest size exactly.

      source
      theorem Complexity.AC0Formula.depth_restrict {N : ℕ} (restriction : Restriction.On N) (formula : AC0Formula N) :
      (restrict restriction formula).depth = formula.depth

      Restriction preserves connective depth exactly.

      source
      theorem Complexity.AC0Formula.forestDepth_restrictForest {N : ℕ} (restriction : Restriction.On N) (formulas : AC0Forest N) :
      forestDepth (restrictForest restriction formulas) = forestDepth formulas

      Restriction preserves maximum forest depth exactly.

      source
      theorem Complexity.AC0Formula.vars_restrict {N : ℕ} (restriction : Restriction.On N) (formula : AC0Formula N) :
      (restrict restriction formula).vars = {index ∈ formula.vars | restriction index = none}

      Restriction removes exactly the variables it fixes.

      source
      theorem Complexity.AC0Formula.forestVars_restrictForest {N : ℕ} (restriction : Restriction.On N) (formulas : AC0Forest N) :
      forestVars (restrictForest restriction formulas) = {index ∈ forestVars formulas | restriction index = none}

      Forest support is filtered to the free variables by restriction.