Documentation

Complexity.Algorithms.WordRAM.FusionTree.Binary

Two-child node search #

Below the large-width fusion threshold, the tree branches in two. Direct comparison of the two child minima supplies a uniform constant-time fallback. The eighteen-word header and interleaved key/pointer table use the same layout as larger nodes.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.registers :
ℕ

The register interface agrees with the larger fusion-node query.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.query :
    Fin registers

    Bounded query, preserved.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.pointer :
      Fin registers

      Record base, preserved.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.out :
        Fin registers

        Final inclusive rank, zero, one, or two.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.two :
          Fin registers

          Distance between the two child minima.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.offset :
            Fin registers

            Offset of the child table.

            Instances For
              source
              @[reducible, inline]
              abbrev Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.address :
              Fin registers

              Address scratch.

              Instances For
                source
                @[reducible, inline]
                abbrev Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.first :
                Fin registers

                First child minimum.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.second :
                  Fin registers

                  Second child minimum.

                  Instances For
                    source
                    def Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.code :
                    WordRAM.Code WordRAM.Basis.standard registers

                    Two direct full-key comparisons, with charged constants and memory loads.

                    Instances For
                      source
                      def Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.rank (q a b : ℕ) :
                      ℕ

                      The inclusive rank among two increasing full keys.

                      Instances For
                        source
                        def Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.result (x : WordRAM.Data registers) :
                        WordRAM.Data registers

                        Exact data after reading both minima and returning their rank.

                        Instances For
                          source
                          theorem Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.rank_eq {q a b : ℕ} (hab : a < b) :
                          rank q a b = Lean.FusionTree.upperRank ![a, b] q

                          The direct comparison expression equals inclusive rank, with equality counted.

                          source
                          theorem Cslib.Algorithms.WordRAM.FusionTree.BinaryNodeProgram.exec {w : ℕ} (x : WordRAM.Data registers) (ha : WordRAM.Fits w (x.regs pointer + 20)) :
                          WordRAM.ExecWithin w code x (result x) 11 ∧ (result x).mem = x.mem ∧ (result x).regs out = rank (x.regs query) (x.mem (x.regs pointer + 18)) (x.mem (x.regs pointer + 20))

                          Eleven instructions suffice for the binary fallback. All address and constant bounds follow from the address of the second key; all memory, query, and record base are preserved. Only registers two through seven change.