Polarity propagation

The four-point polarity domain records independence, positive dependence, negative dependence, or mixed dependence. A local polarity for each operation argument induces a compositional analysis of every circuit. As with degree, a concrete monotonicity theorem only needs to establish soundness of the selected local policy.

inductive Algebraic.Polarity : Type

Abstract dependence polarity.

• none : Polarity
• positive : Polarity
• negative : Polarity
• mixed : Polarity

@[instance_reducible]

instance Algebraic.instDecidableEqPolarity : DecidableEq Polarity

Equations

• Algebraic.instDecidableEqPolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Algebraic.instReprPolarity.repr : Polarity → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.instReprPolarity.repr Algebraic.Polarity.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Algebraic.Polarity.none")).group prec✝
• Algebraic.instReprPolarity.repr Algebraic.Polarity.mixed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Algebraic.Polarity.mixed")).group prec✝

@[instance_reducible]

instance Algebraic.instReprPolarity : Repr Polarity

Equations

• Algebraic.instReprPolarity = { reprPrec := Algebraic.instReprPolarity.repr }

def Algebraic.Polarity.join : Polarity → Polarity → Polarity

Join information coming from two dependency paths.

Equations

• Algebraic.Polarity.none.join x✝ = x✝
• x✝.join Algebraic.Polarity.none = x✝
• Algebraic.Polarity.mixed.join x✝ = Algebraic.Polarity.mixed
• x✝.join Algebraic.Polarity.mixed = Algebraic.Polarity.mixed
• Algebraic.Polarity.positive.join Algebraic.Polarity.positive = Algebraic.Polarity.positive
• Algebraic.Polarity.negative.join Algebraic.Polarity.negative = Algebraic.Polarity.negative
• Algebraic.Polarity.positive.join Algebraic.Polarity.negative = Algebraic.Polarity.mixed
• Algebraic.Polarity.negative.join Algebraic.Polarity.positive = Algebraic.Polarity.mixed

def Algebraic.Polarity.comp : Polarity → Polarity → Polarity

Compose the polarity of an operation argument with the polarity carried by the argument expression.

Equations

• Algebraic.Polarity.none.comp x✝ = Algebraic.Polarity.none
• x✝.comp Algebraic.Polarity.none = Algebraic.Polarity.none
• Algebraic.Polarity.positive.comp x✝ = x✝
• Algebraic.Polarity.negative.comp Algebraic.Polarity.positive = Algebraic.Polarity.negative
• Algebraic.Polarity.negative.comp Algebraic.Polarity.negative = Algebraic.Polarity.positive
• Algebraic.Polarity.negative.comp Algebraic.Polarity.mixed = Algebraic.Polarity.mixed
• Algebraic.Polarity.mixed.comp x✝ = Algebraic.Polarity.mixed

def Algebraic.Polarity.inputProfile {n : ℕ} (input : Fin n) : Fin n → Polarity

One-hot positive dependency profile of an original input.

Equations

• Algebraic.Polarity.inputProfile input coordinate = if input = coordinate then Algebraic.Polarity.positive else Algebraic.Polarity.none

@[reducible, inline]

abbrev Algebraic.PolarityPolicy (σ : Signature) : Type u_1

Local polarity of every argument of every operation.

Equations

• Algebraic.PolarityPolicy σ = ((op : σ.Op) → Fin (σ.Arity op) → Algebraic.Polarity)

def Cslib.Circuits.Signature.polarityInterpretation (σ : Signature) (policy : Algebraic.PolarityPolicy σ) (n : ℕ) : Interpretation σ (Fin n → Algebraic.Polarity)

Polarity interpretation induced by a local argument policy.

Equations

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

def Cslib.Circuits.Circuit.polarityProfile {σ : Signature} {n m : ℕ} (circuit : Circuit σ n m) (policy : Algebraic.PolarityPolicy σ) : Fin m → Fin n → Algebraic.Polarity

Per-output, per-input polarity profile of a circuit.

Equations

• circuit.polarityProfile policy = circuit.eval (σ.polarityInterpretation policy n) Algebraic.Polarity.inputProfile

theorem Algebraic.Translation.compile_polarityProfile {σ : Signature} {τ : Signature} {n m : ℕ} (translation : Translation σ τ) (circuit : Circuit σ n m) (targetPolicy : PolarityPolicy τ) : (translation.compile circuit).polarityProfile targetPolicy = circuit.eval (translation.pull (τ.polarityInterpretation targetPolicy n)) Polarity.inputProfile

Translation preserves the exact abstract polarity propagation induced by its target operation gadgets.