Evaluating De Morgan circuits in polynomial time

CslibFrontier.Computability.Circuit.Encoding.Evaluation defines signature-polymorphic gate-list evaluation (Cslib.Circuits.evalCode) and proves its agreement with typed circuit evaluation (Cslib.Circuits.Program.evalCode_code, Cslib.Circuits.Circuit.eval_eq_getD). This module specializes that evaluator to De Morgan circuits (Cslib.Circuits.Boolean.evalOutput) and proves polynomial-time computability certificates for it.

For De Morgan circuits, evalCode is computable in polynomial time on the binary encoding of gate lists (Cslib.Circuits.Boolean.computableInPolyTime_evalCode), and so is reading an output wire given by its binary number (Cslib.Circuits.Boolean.computableInPolyTime_evalOutput). These are certificates for the fun_prop calculus of polynomial-time computations; the evaluators of CslibFrontier.Computability.Circuit.Evaluation carry no runtime bound. Each gate is evaluated by two lookups at wire numbers, which are capped at the number of values computed so far before they are converted to unary, so wire numbers far beyond the circuit cost only their binary length.

The typed evaluation certificate accepts any bit list. It pads short lists with false and truncates long lists to the declared input arity before invoking the raw evaluator. Circuit generation, input preparation, binary wire lookup and evaluation are all included in its cost.

Main definitions

• Cslib.Circuits.Boolean.evalOutput: the value of a wire after evaluating a list of De Morgan gates.

Main results

• Cslib.Circuits.Circuit.eval_eq_evalOutput: De Morgan circuit evaluation through Cslib.Circuits.Boolean.evalOutput.
• Cslib.Circuits.Circuit.eval_ofList_eq_evalOutput: typed evaluation on an arbitrary input list uses the padded or truncated input word.
• Cslib.Circuits.Boolean.computableInPolyTime_evalCode, Cslib.Circuits.Boolean.computableInPolyTime_evalOutput: evaluation of De Morgan gate lists is polynomial-time.
• Cslib.Circuits.Boolean.computableInPolyTime_evalCircuit: evaluating an efficiently generated typed circuit on an efficiently generated input list is polynomial-time.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

Polynomial time

theorem Cslib.Circuits.Boolean.computableInPolyTime_evalCode {γ : Type} {encIn : γ ↪ List Bool} {x : γ → List Bool} {gates : γ → List (Op × List ℕ)} (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn Turing.MultiTapeTM.encBits) (hgates : Turing.MultiTapeTM.ComputableInPolyTime gates encIn (Turing.MultiTapeTM.encList encGate)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => evalCode interpretation false (x a) (gates a)) encIn Turing.MultiTapeTM.encBits

Polynomial-time evaluation of De Morgan gate lists, for input bits and a gate list in the binary encoding encGate, both computed in polynomial time.

def Cslib.Circuits.Boolean.evalOutput (x : List Bool) (gates : List (Op × List ℕ)) (o : ℕ) : Bool

The value of wire o after evaluating the De Morgan gate list gates on the input bits x: on the code of a circuit and the number of an output wire, the value of that output (Circuit.eval_eq_getD).

theorem Cslib.Circuits.Circuit.eval_eq_evalOutput {n m : ℕ} (c : Circuit Boolean.signature n m) (x : Fin n → Bool) (j : Fin m) : c.eval Boolean.interpretation x j = Boolean.evalOutput (List.ofFn x) c.code.1 (c.outputs j).toNat

Output j of a De Morgan circuit is evalOutput at the number of its output wire.

theorem Cslib.Circuits.Boolean.computableInPolyTime_evalOutput {γ : Type} {encIn : γ ↪ List Bool} {x : γ → List Bool} {gates : γ → List (Op × List ℕ)} {o : γ → ℕ} (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn Turing.MultiTapeTM.encBits) (hgates : Turing.MultiTapeTM.ComputableInPolyTime gates encIn (Turing.MultiTapeTM.encList encGate)) (ho : Turing.MultiTapeTM.ComputableInPolyTime o encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => evalOutput (x a) (gates a) (o a)) encIn Turing.MultiTapeTM.encBool

Polynomial-time evaluation of an output of a De Morgan gate list, for input bits, a gate list in the binary encoding encGate and a binary wire number, all computed in polynomial time.

theorem Cslib.Circuits.Circuit.eval_ofList_eq_evalOutput {n m : ℕ} (c : Circuit Boolean.signature n m) (x : List Bool) (j : Fin m) : c.eval Boolean.interpretation (BitString.ofList n x) j = Boolean.evalOutput (List.take n (x ++ List.replicate n false)) c.code.1 (c.code.2.getD (↑j) 0)

Evaluate a typed circuit on an arbitrary bit list by padding or truncating to its input arity. The output wire is read from the circuit's code at the specified output position.

theorem Cslib.Circuits.Boolean.computableInPolyTime_evalCircuit {γ : Type} {encIn : γ ↪ List Bool} {c : γ → (n : ℕ) × Circuit signature n 1} {x : γ → List Bool} (hc : Turing.MultiTapeTM.ComputableInPolyTime c encIn (encCircuit 1)) (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => (c a).snd.eval interpretation (BitString.ofList (c a).fst (x a)) 0) encIn Turing.MultiTapeTM.encBool

Evaluate an efficiently computed typed circuit on any efficiently computed bit list. No length premise is needed: missing inputs are false, and inputs past the circuit's arity are ignored. The certificate charges circuit generation, input padding and all evaluation.