Documentation

Complexity.Computability.Circuit.Boolean.SemiCircuit.OfCircuit

The semi-circuit of a circuit #

A circuit over the full binary basis with n inputs and one output is a fair semi-circuit without equations (SemiCircuit.ofCircuit): input i is the parameter i, gate j is the gate n + j, and a constant line becomes a gate with a constant operation. It is well formed (SemiCircuit.wellFormed_ofCircuit), and the output of a consistent assignment is the output of the circuit on the values of the parameters (SemiCircuit.out_eval_ofCircuit).

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.SemiCircuit.wireName {n g : ℕ} :
Wire n g → ℕ

The name of a wire of a circuit with n inputs: input i is i and gate j is n + j.

Instances For
    source
    def Cslib.Circuits.Boolean.SemiCircuit.lineGate {n g : ℕ} :
    Line (fullSignature 2 Bool) n g → Gate

    The gate of a line of a circuit over the full binary basis; a constant becomes a gate with a constant operation.

    Instances For
      source
      theorem Cslib.Circuits.Boolean.SemiCircuit.eval_lineGate {n g : ℕ} (line : Line (fullSignature 2 Bool) n g) (val : ℕ → Bool) :
      (lineGate line).eval val = fullInterpretation line.op fun (a : Fin ((fullSignature 2 Bool).Arity line.op)) => val (wireName (line.wires a))

      Evaluating lineGate line under val equals applying fullInterpretation line.op to the values of line's input wires.

      source
      def Cslib.Circuits.Boolean.SemiCircuit.ofCircuit {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) :
      SemiCircuit

      The semi-circuit of a circuit over the full binary basis with one output: its inputs are the parameters, its lines the gates, and it has no auxiliary variables and no equations.

      Instances For
        source
        @[simp]
        theorem Cslib.Circuits.Boolean.SemiCircuit.ofCircuit_params {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) :
        (ofCircuit C).params = Finset.range n

        The parameters of ofCircuit C are Finset.range n.

        source
        @[simp]
        theorem Cslib.Circuits.Boolean.SemiCircuit.ofCircuit_aux {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) :
        (ofCircuit C).aux = ∅

        The semi-circuit ofCircuit C has no auxiliary variables.

        source
        @[simp]
        theorem Cslib.Circuits.Boolean.SemiCircuit.ofCircuit_gates {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) :
        (ofCircuit C).gates = Finset.Ico n (n + C.size)

        The gate indices of ofCircuit C are Finset.Ico n (n + C.size).

        source
        @[simp]
        theorem Cslib.Circuits.Boolean.SemiCircuit.ofCircuit_eqns {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) :
        (ofCircuit C).eqns = ∅

        The semi-circuit ofCircuit C has no affine equations.

        source
        theorem Cslib.Circuits.Boolean.SemiCircuit.wireName_mem_live {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) (w : Wire n C.size) :
        wireName w ∈ (ofCircuit C).live

        The node index wireName w of any wire w of C is live in ofCircuit C.

        source
        theorem Cslib.Circuits.Boolean.SemiCircuit.exists_eq_add_of_mem_gates {n : ℕ} {C : Circuit (fullSignature 2 Bool) n 1} {J : ℕ} (hJ : J ∈ (ofCircuit C).gates) :
        ∃ (k : Fin C.size), J = n + ↑k

        Every gate index of ofCircuit C has the form n + k for some k : Fin C.size.

        source
        theorem Cslib.Circuits.Boolean.SemiCircuit.wellFormed_ofCircuit {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) :
        (ofCircuit C).WellFormed

        The semi-circuit of a circuit is well formed.

        source
        theorem Cslib.Circuits.Boolean.SemiCircuit.out_eval_ofCircuit {n : ℕ} (C : Circuit (fullSignature 2 Bool) n 1) {val : ℕ → Bool} (hval : (ofCircuit C).Consistent val) :
        (ofCircuit C).out.eval val = C.eval fullInterpretation (fun (i : Fin n) => val ↑i) 0

        On a consistent assignment, the output of the semi-circuit of a circuit is the output of the circuit on the values of the parameters.