Documentation

Complexity.Computability.Circuit.Pointwise

Circuits on truth tables #

An interpretation I of a signature over a carrier U lifts pointwise to the functions X → U (Cslib.Circuits.Interpretation.pointwise): an operation applied to functions is applied value by value. Evaluation at a point x : X is a homomorphism from the lifted interpretation to I (Cslib.Circuits.Interpretation.evalAt), so the value of every wire of a circuit under the lifted interpretation is, at each point, the value of that wire under I (Cslib.Circuits.Program.trace_pointwise_apply, Cslib.Circuits.Circuit.eval_pointwise_apply).

Take X = Fin n → U and start from the coordinate projections. Then every wire carries its truth table, the function it computes (Cslib.Circuits.Program.trace_pointwise_proj), so the values of the wires are exactly the functions available in the program (Cslib.Circuits.available_eq_range_trace_pointwise), and the outputs of a circuit are the functions it computes (Cslib.Circuits.Circuit.eval_pointwise_proj). A circuit computes f exactly when its lifted evaluation at the projections is the truth table of f (Cslib.Circuits.Circuit.computes_iff_eval_pointwise_proj). This is the description of a circuit as a sequence of functions, each obtained by applying a basis operation to earlier ones [Juk12], and it makes truth tables ordinary semantic values: geometric statements about functions, such as Hamming distances between wires, are statements about values of the lifted interpretation.

Main definitions #

Main results #

References #

The pointwise lift #

source
def Cslib.Circuits.Interpretation.pointwise {σ : Signature} {U : Type u_1} (X : Type u_2) (I : Interpretation σ U) :
Interpretation σ (X → U)

The pointwise lift of I to functions X → U: an operation is applied value by value.

Instances For
    source
    @[simp]
    theorem Cslib.Circuits.Interpretation.pointwise_apply {σ : Signature} {U : Type u_1} (X : Type u_2) (I : Interpretation σ U) (op : σ.Op) (args : Fin (σ.Arity op) → X → U) (x : X) :
    pointwise X I op args x = I op fun (i : Fin (σ.Arity op)) => args i x
    source
    def Cslib.Circuits.Interpretation.evalAt {σ : Signature} {U : Type u_1} (I : Interpretation σ U) {X : Type u_2} (x : X) :
    Homomorphism (pointwise X I) I

    Evaluation at a point is a homomorphism from the pointwise lift.

    Instances For
      source
      @[simp]
      theorem Cslib.Circuits.Interpretation.evalAt_map {σ : Signature} {U : Type u_1} (I : Interpretation σ U) {X : Type u_2} (x : X) (f : X → U) :
      (I.evalAt x).map f = f x

      Evaluation is pointwise #

      source
      theorem Cslib.Circuits.Program.trace_pointwise_apply {σ : Signature} {U : Type u_1} {n g : ℕ} (p : Program σ n g) (I : Interpretation σ U) {X : Type u_2} (a : Fin n → X → U) (w : Wire n g) (x : X) :
      p.trace (Interpretation.pointwise X I) a w x = p.trace I (fun (j : Fin n) => a j x) w

      Every wire of a program, under the pointwise lift, takes at each point the value of that wire under I.

      source
      theorem Cslib.Circuits.Circuit.eval_pointwise_apply {σ : Signature} {U : Type u_1} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ U) {X : Type u_2} (a : Fin n → X → U) (o : Fin m) (x : X) :
      c.eval (Interpretation.pointwise X I) a o x = c.eval I (fun (j : Fin n) => a j x) o

      Every output of a circuit, under the pointwise lift, takes at each point the value of that output under I.

      Truth tables #

      source
      theorem Cslib.Circuits.Program.trace_pointwise_proj {σ : Signature} {U : Type u_1} {n g : ℕ} (p : Program σ n g) (I : Interpretation σ U) :
      (p.trace (Interpretation.pointwise (Fin n → U) I) fun (j : Fin n) (x : Fin n → U) => x j) = p.wireFunction I

      Wires carry truth tables. Under the pointwise lift, started at the coordinate projections, every wire of a program carries the function it computes.

      source
      theorem Cslib.Circuits.available_eq_range_trace_pointwise {σ : Signature} {U : Type u_1} {n : ℕ} (I : Interpretation σ U) {g : ℕ} (p : Program σ n g) :
      available I p = Set.range (p.trace (Interpretation.pointwise (Fin n → U) I) fun (j : Fin n) (x : Fin n → U) => x j)

      The functions available in a program are the values of its wires under the pointwise lift, started at the coordinate projections.

      source
      theorem Cslib.Circuits.Circuit.eval_pointwise_proj {σ : Signature} {U : Type u_1} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ U) (o : Fin m) :
      c.eval (Interpretation.pointwise (Fin n → U) I) (fun (j : Fin n) (x : Fin n → U) => x j) o = fun (x : Fin n → U) => c.eval I x o

      Outputs are truth tables. Under the pointwise lift, started at the coordinate projections, every output of a circuit is the function that output computes.

      source
      theorem Cslib.Circuits.Circuit.computes_iff_eval_pointwise_proj {σ : Signature} {U : Type u_1} {n m : ℕ} (c : Circuit σ n m) (I : Interpretation σ U) (f : (Fin n → U) → Fin m → U) :
      c.Computes I f ↔ (c.eval (Interpretation.pointwise (Fin n → U) I) fun (j : Fin n) (x : Fin n → U) => x j) = fun (o : Fin m) (x : Fin n → U) => f x o

      A circuit computes f exactly when its lifted evaluation at the coordinate projections is the truth table of f.