Single cuts of a straight-line program

The vertices of a straight-line program are its wires: the inputs and the gates. A cut is a set S of wires, with complement Sᶜ. A signal is the value carried by one wire, however many gates read it.

• inputsIn S is the set of input coordinates whose wires lie in S;
• forward p S is the set of wires in S read by some gate outside S;
• backward p S is the set of wires outside S read by some gate in S;
• boundaryKey p I S x records the values of the forward and backward signals of S under the input x;
• mix S x x' takes the coordinates of x whose input wires lie in S and the other coordinates of x';
• leftPart S x and rightPart S x restrict x to the coordinates whose input wires lie in S and outside S, respectively;
• leftParts p I S Z κ and rightParts p I S Z κ collect these restrictions over the members of Z with boundary key κ.

The definitions are generic in the signature and in the value type; the single-cut criterion specializes the value type to Bool.

def Algebraic.Cutwidth.SingleCut.inputsIn {n s : ℕ} (S : Finset (Wire n s)) : Finset (Fin n)

The input coordinates whose wires lie in S.

Equations

• Algebraic.Cutwidth.SingleCut.inputsIn S = {j : Fin n | Cslib.Circuits.Wire.input j ∈ S}

def Algebraic.Cutwidth.SingleCut.forward {σ : Signature} {n s : ℕ} (p : Program σ n s) (S : Finset (Wire n s)) : Finset (Wire n s)

The forward signals of S: the wires in S read by some gate outside S. A wire read by several gates outside S is one signal.

Equations

• Algebraic.Cutwidth.SingleCut.forward p S = {w ∈ S | ∃ (g : Fin s), Cslib.Circuits.Wire.gate g ∉ S ∧ p.Reads g w}

def Algebraic.Cutwidth.SingleCut.backward {σ : Signature} {n s : ℕ} (p : Program σ n s) (S : Finset (Wire n s)) : Finset (Wire n s)

The backward signals of S: the wires outside S read by some gate in S. A wire read by several gates in S is one signal.

Equations

• Algebraic.Cutwidth.SingleCut.backward p S = {w ∉ S | ∃ (g : Fin s), Cslib.Circuits.Wire.gate g ∈ S ∧ p.Reads g w}

def Algebraic.Cutwidth.SingleCut.boundaryKey {σ : Signature} {n s : ℕ} {U : Type u_1} (p : Program σ n s) (I : Interpretation σ U) (S : Finset (Wire n s)) (x : Fin n → U) : (↥(forward p S) → U) × (↥(backward p S) → U)

The values of the forward and of the backward signals of S under the input x.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.SingleCut.mix {n s : ℕ} {U : Type u_1} (S : Finset (Wire n s)) (x x' : Fin n → U) : Fin n → U

The input taking the coordinates of x whose wires lie in S and the other coordinates of x'.

Equations

• Algebraic.Cutwidth.SingleCut.mix S x x' j = if Cslib.Circuits.Wire.input j ∈ S then x j else x' j

def Algebraic.Cutwidth.SingleCut.leftPart {n s : ℕ} {U : Type u_1} (S : Finset (Wire n s)) (x : Fin n → U) : ↥(inputsIn S) → U

The restriction of an input to the coordinates whose wires lie in S.

Equations

• Algebraic.Cutwidth.SingleCut.leftPart S x j = x ↑j

def Algebraic.Cutwidth.SingleCut.rightPart {n s : ℕ} {U : Type u_1} (S : Finset (Wire n s)) (x : Fin n → U) : ↥(inputsIn S)ᶜ → U

The restriction of an input to the coordinates whose wires lie outside S.

Equations

• Algebraic.Cutwidth.SingleCut.rightPart S x j = x ↑j

def Algebraic.Cutwidth.SingleCut.leftParts {σ : Signature} {n s : ℕ} {U : Type u_1} [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) (S : Finset (Wire n s)) (Z : Finset (Fin n → U)) (κ : (↥(forward p S) → U) × (↥(backward p S) → U)) : Finset (↥(inputsIn S) → U)

The left parts of the members of Z whose boundary key is κ.

Equations

• Algebraic.Cutwidth.SingleCut.leftParts p I S Z κ = Finset.image (Algebraic.Cutwidth.SingleCut.leftPart S) ({x ∈ Z | Algebraic.Cutwidth.SingleCut.boundaryKey p I S x = κ})

def Algebraic.Cutwidth.SingleCut.rightParts {σ : Signature} {n s : ℕ} {U : Type u_1} [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) (S : Finset (Wire n s)) (Z : Finset (Fin n → U)) (κ : (↥(forward p S) → U) × (↥(backward p S) → U)) : Finset (↥(inputsIn S)ᶜ → U)

The right parts of the members of Z whose boundary key is κ.

Equations

• Algebraic.Cutwidth.SingleCut.rightParts p I S Z κ = Finset.image (Algebraic.Cutwidth.SingleCut.rightPart S) ({x ∈ Z | Algebraic.Cutwidth.SingleCut.boundaryKey p I S x = κ})

theorem Algebraic.Cutwidth.SingleCut.mem_inputsIn {n s : ℕ} {S : Finset (Wire n s)} {j : Fin n} : j ∈ inputsIn S ↔ Wire.input j ∈ S

theorem Algebraic.Cutwidth.SingleCut.mem_forward {σ : Signature} {n s : ℕ} {p : Program σ n s} {S : Finset (Wire n s)} {w : Wire n s} : w ∈ forward p S ↔ w ∈ S ∧ ∃ (g : Fin s), Wire.gate g ∉ S ∧ p.Reads g w

theorem Algebraic.Cutwidth.SingleCut.mem_backward {σ : Signature} {n s : ℕ} {p : Program σ n s} {S : Finset (Wire n s)} {w : Wire n s} : w ∈ backward p S ↔ w ∉ S ∧ ∃ (g : Fin s), Wire.gate g ∈ S ∧ p.Reads g w

theorem Algebraic.Cutwidth.SingleCut.inputsIn_compl {n s : ℕ} (S : Finset (Wire n s)) : inputsIn Sᶜ = (inputsIn S)ᶜ

The inputs placed in the complement of S are the inputs not placed in S.

theorem Algebraic.Cutwidth.SingleCut.forward_compl {σ : Signature} {n s : ℕ} (p : Program σ n s) (S : Finset (Wire n s)) : forward p Sᶜ = backward p S

The forward signals of the complement are the backward signals.

theorem Algebraic.Cutwidth.SingleCut.backward_compl {σ : Signature} {n s : ℕ} (p : Program σ n s) (S : Finset (Wire n s)) : backward p Sᶜ = forward p S

The backward signals of the complement are the forward signals.