Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Halver.Defs

Comparator networks, ε-halvers, and their wire graphs #

A comparator network on n wires with s comparators (ComparatorNetwork n s) applies its comparators in the order 0, 1, …, s - 1. Comparator c acts on two distinct wires minWire c and maxWire c: it puts the smaller of their two values on minWire c and the larger on maxWire c. The wires need not satisfy minWire c < maxWire c. The network acts on wire values in any linear order (ComparatorNetwork.eval); on {0, 1}, encoded as Bool with false < true, the minimum is and and the maximum is or.

The bottom half consists of the wires w < ⌊n/2⌋ and the top half of the others. The network is an ε-halver (ComparatorNetwork.IsHalver) when on every input x ∈ {0, 1}ⁿ with k ≤ n/2 ones, at most ε k ones end in the bottom half, and on every input with k ≤ n/2 zeros, at most ε k zeros end in the top half. For even n this is the 0-1 form of the ε-halvers of Ajtai, Komlós and Szemerédi: among the k ≤ n/2 largest inputs at most ε k end in the bottom half, and among the k smallest at most ε k end in the top half.

The wire graph (ComparatorNetwork.wireGraph) is a directed multigraph. Its vertices (WireVertex) are an input and an output terminal for every wire and, for every comparator c, two vertices gate c false and gate c true, the ends of c on minWire c and on maxWire c. Its edges (WireEdge) are the wire segments, which follow each wire from its input terminal through the ends of the comparators acting on it, in order, to its output terminal, and for every comparator a link from gate c false to gate c true. A wire segment is named after the vertex it enters: into c b enters gate c b and last w enters the output terminal of w. It leaves lastStop w t, the end on wire w of the last comparator before time t acting on w, or the input terminal of w if there is none.

source
structure Algebraic.Cutwidth.ComparatorNetwork (n s : ℕ) :
Type

A comparator network on n wires with s comparators, applied in the order 0, 1, …, s - 1. Comparator c acts on the distinct wires minWire c and maxWire c.

  • minWire : Fin s → Fin n

    The wire that receives the smaller value at comparator c.

  • maxWire : Fin s → Fin n

    The wire that receives the larger value at comparator c.

  • minWire_ne_maxWire (c : Fin s) : self.minWire c ≠ self.maxWire c

    The two wires of a comparator are distinct.

Instances For
    source
    inductive Algebraic.Cutwidth.WireVertex (n s : ℕ) :
    Type

    A vertex of the wire graph of a comparator network on n wires with s comparators.

    Instances For
      source
      @[instance_reducible]
      instance Algebraic.Cutwidth.instDecidableEqWireVertex {n✝ s✝ : ℕ} :
      DecidableEq (WireVertex n✝ s✝)
      Equations
      source
      def Algebraic.Cutwidth.instDecidableEqWireVertex.decEq {n✝ s✝ : ℕ} (x✝ x✝¹ : WireVertex n✝ s✝) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        source
        @[instance_reducible]
        instance Algebraic.Cutwidth.instFintypeWireVertex {n✝ s✝ : ℕ} :
        Fintype (WireVertex n✝ s✝)
        Equations
        source
        inductive Algebraic.Cutwidth.WireEdge (n s : ℕ) :
        Type

        An edge of the wire graph of a comparator network on n wires with s comparators.

        • last {n s : ℕ} (w : Fin n) : WireEdge n s

          The last segment of wire w, which enters its output terminal.

        • into {n s : ℕ} (c : Fin s) (b : Bool) : WireEdge n s

          The wire segment entering the end gate c b of comparator c.

        Instances For
          source
          def Algebraic.Cutwidth.instDecidableEqWireEdge.decEq {n✝ s✝ : ℕ} (x✝ x✝¹ : WireEdge n✝ s✝) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            source
            @[instance_reducible]
            instance Algebraic.Cutwidth.instDecidableEqWireEdge {n✝ s✝ : ℕ} :
            DecidableEq (WireEdge n✝ s✝)
            Equations
            source
            @[instance_reducible]
            instance Algebraic.Cutwidth.instFintypeWireEdge {n✝ s✝ : ℕ} :
            Fintype (WireEdge n✝ s✝)
            Equations
            source
            def Algebraic.Cutwidth.ComparatorNetwork.apply {n s : ℕ} (N : ComparatorNetwork n s) {α : Type u_1} [LinearOrder α] (c : Fin s) (x : Fin n → α) :
            Fin n → α

            Apply comparator c to the wire values x: the smaller of the values on minWire c and maxWire c goes to minWire c, the larger to maxWire c, and the other wires keep their values.

            Equations
            Instances For
              source
              def Algebraic.Cutwidth.ComparatorNetwork.state {n s : ℕ} (N : ComparatorNetwork n s) {α : Type u_1} [LinearOrder α] (x : Fin n → α) :
              ℕ → Fin n → α

              The wire values after the first t comparators, on input x.

              Equations
              Instances For
                source
                def Algebraic.Cutwidth.ComparatorNetwork.eval {n s : ℕ} (N : ComparatorNetwork n s) {α : Type u_1} [LinearOrder α] (x : Fin n → α) :
                Fin n → α

                The output of the network on input x: the wire values after all s comparators.

                Equations
                Instances For
                  source
                  def Algebraic.Cutwidth.ComparatorNetwork.IsHalver {n s : ℕ} (N : ComparatorNetwork n s) (ε : ℝ) :
                  Prop

                  N is an ε-halver. The bottom half is the wires w < ⌊n/2⌋ and the top half the others. On every input x ∈ {0, 1}ⁿ with k ≤ n/2 ones (true), at most ε k ones end in the bottom half; on every input with k ≤ n/2 zeros (false), at most ε k zeros end in the top half.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Algebraic.Cutwidth.ComparatorNetwork.sideWire {n s : ℕ} (N : ComparatorNetwork n s) (c : Fin s) (b : Bool) :
                    Fin n

                    The wire of the end of comparator c on side b: minWire c for false, maxWire c for true.

                    Equations
                    Instances For
                      source
                      def Algebraic.Cutwidth.ComparatorNetwork.lastStop {n s : ℕ} (N : ComparatorNetwork n s) (w : Fin n) (t : ℕ) :
                      WireVertex n s

                      The vertex of wire w last visited before time t: the end on w of the last comparator c < t acting on w, or the input terminal of w if no comparator before time t acts on it.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Algebraic.Cutwidth.ComparatorNetwork.wireGraph {n s : ℕ} (N : ComparatorNetwork n s) :
                        Multigraph (WireVertex n s) (WireEdge n s)

                        The wire graph of N. The segment last w runs from the last vertex of wire w to its output terminal, the segment into c b from the previous vertex of wire sideWire c b to the end gate c b, and the link of comparator c from gate c false to gate c true.

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