Compiling observed signals into a monoid network

Each selected signal emits its contribution exactly once, at its own vertex. Copy vertices emit the identity. A gate's value is computed from its input slots even when it has no outgoing edge. Consequently arbitrary observation of sinks preserves the wire graph, its degree-three bound, and its edge excess. The monoid need not have cancellation or inverses.

noncomputable def Algebraic.Cutwidth.Aggregate.Wiring.contribution {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (I : Interpretation σ Bool) {M : Type} [CommMonoid M] (φ : MultiOutput.Internal.WireGraph.Signal K → Bool → M) : MultiOutput.Internal.WireGraph.Vertex K → (MultiOutput.Internal.WireGraph.Edge K → Bool) → M

Each signal emits once; fanout copies contribute the identity.

Equations

• Algebraic.Cutwidth.Aggregate.Wiring.contribution K I φ (Sum.inl w) x✝ = φ w (Algebraic.Cutwidth.Aggregate.Wiring.localValue K I x✝ w)
• Algebraic.Cutwidth.Aggregate.Wiring.contribution K I φ (Sum.inr val) x✝ = 1

noncomputable def Algebraic.Cutwidth.Aggregate.Wiring.aggregateNetwork {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) {M : Type} [CommMonoid M] (φ : MultiOutput.Internal.WireGraph.Signal K → Bool → M) (Accept : M → Prop) : AggregateNetwork n (MultiOutput.Internal.WireGraph.Vertex K) (MultiOutput.Internal.WireGraph.Edge K) M

The closed wire graph compiled to an aggregate network.

Equations

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

theorem Algebraic.Cutwidth.Aggregate.Wiring.accumulated_eq {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) {M : Type} [CommMonoid M] (φ : MultiOutput.Internal.WireGraph.Signal K → Bool → M) (Accept : M → Prop) (α : MultiOutput.Internal.WireGraph.Edge K → Bool) : (aggregateNetwork K hinput I φ Accept).accumulated Finset.univ α = ∏ w : MultiOutput.Internal.WireGraph.Signal K, φ w (localValue K I α w)

The product at all vertices contains each selected signal exactly once.

theorem Algebraic.Cutwidth.Aggregate.Wiring.accumulated_eq_trace {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) {M : Type} [CommMonoid M] (φ : MultiOutput.Internal.WireGraph.Signal K → Bool → M) (Accept : M → Prop) {x : Fin n → Bool} {α : MultiOutput.Internal.WireGraph.Edge K → Bool} (hα : (network K hinput I).Satisfies x α) : (aggregateNetwork K hinput I φ Accept).accumulated Finset.univ α = ∏ w : MultiOutput.Internal.WireGraph.Signal K, φ w (p.trace I x ↑w)

The global aggregate of a satisfying local evaluation is the aggregate of the trace.

theorem Algebraic.Cutwidth.Aggregate.Wiring.exists_satisfies_iff {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) {M : Type} [CommMonoid M] (φ : MultiOutput.Internal.WireGraph.Signal K → Bool → M) (Accept : M → Prop) (x : Fin n → Bool) : (∃ (α : MultiOutput.Internal.WireGraph.Edge K → Bool), (aggregateNetwork K hinput I φ Accept).Satisfies x α) ↔ Accept (∏ w : MultiOutput.Internal.WireGraph.Signal K, φ w (p.trace I x ↑w))

Exact compiler semantics for an arbitrary final predicate on the aggregate.

theorem Algebraic.Cutwidth.Aggregate.Wiring.aggregateNetwork_computes {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) {M : Type} [CommMonoid M] (φ : MultiOutput.Internal.WireGraph.Signal K → Bool → M) (Accept : M → Prop) : (aggregateNetwork K hinput I φ Accept).Computes fun (x : Cslib.BitString n) => decide (Accept (∏ w : MultiOutput.Internal.WireGraph.Signal K, φ w (p.trace I x ↑w)))

The compiled network computes the Boolean predicate of the observed trace product.

theorem Algebraic.Cutwidth.Aggregate.Wiring.aggregateNetwork_toMultigraph {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) {M : Type} [CommMonoid M] (φ : MultiOutput.Internal.WireGraph.Signal K → Bool → M) (Accept : M → Prop) : (aggregateNetwork K hinput I φ Accept).toMultigraph = MultiOutput.Internal.WireGraph.graph K

Observation adds no graph structure.