Documentation

Complexity.Computability.Circuit.Boolean.Tournament

Tournaments: selecting a record with the least key #

Records made of a key of k bits, read as a number with the least significant bit first, and a payload of p bits are compared by their keys. A tournament plays keyed minimums (keyedMinCircuit k p) along a balanced binary tree (Circuit.balanced): the winner of each match, the record with the smaller key, meets the winner of the neighbouring match. On m + 1 records it outputs one of them whose key is the least (exists_eval_tournamentCircuit), with m keyed minimums, that is m (8 k + 3 p + 2) gates beyond those computing the records (size_tournamentCircuit), and depth at most (4 k + 4) ⌈log₂ (m + 1)⌉ above them (depth_tournamentCircuit_le).

The records may be computed by any circuits on shared inputs, or read from the inputs, packed one after the other (packedTournamentCircuit). There is always at least one record; m = 0 returns the sole leaf circuit, and the packed version uses wiring alone. The least-key theorem does not specify which tied record wins.

Main definitions #

Main results #

References #

Adapted from Samuel Schlesinger's earlier Complexitylib module Circuits/KeyedMinimumTournament.

source
def Cslib.Circuits.Boolean.tournamentCircuit {n m : ℕ} (k p : ℕ) (leaves : Fin (m + 1) → Circuit signature n (k + p)) :
Circuit signature n (k + p)

The tournament among the records computed by the circuits leaves: keyed minimums along a balanced binary tree.

Instances For
    source
    theorem Cslib.Circuits.Boolean.exists_eval_tournamentCircuit {k p n m : ℕ} (leaves : Fin (m + 1) → Circuit signature n (k + p)) (x : BitString n) :
    ∃ (i : Fin (m + 1)), (tournamentCircuit k p leaves).eval interpretation x = (leaves i).eval interpretation x ∧ ∀ (j : Fin (m + 1)), (BitString.equivFin k) (BitString.recordKey ((leaves i).eval interpretation x)) ≤ (BitString.equivFin k) (BitString.recordKey ((leaves j).eval interpretation x))

    The tournament selects a least key. Its output is the record computed by one of the circuits, whose key is at most the key of every record.

    source
    @[simp]
    theorem Cslib.Circuits.Boolean.size_tournamentCircuit {k p n m : ℕ} (leaves : Fin (m + 1) → Circuit signature n (k + p)) :
    (tournamentCircuit k p leaves).size = ∑ i : Fin (m + 1), (leaves i).size + m * (8 * k + 3 * p + 2)

    A tournament among m + 1 records uses m keyed minimums beyond the circuits computing the records.

    source
    theorem Cslib.Circuits.Boolean.depth_tournamentCircuit_le {k p n m : ℕ} (leaves : Fin (m + 1) → Circuit signature n (k + p)) {D : ℕ} (h : ∀ (i : Fin (m + 1)), (leaves i).depth ≤ D) :
    (tournamentCircuit k p leaves).depth ≤ D + (4 * k + 4) * Nat.clog 2 (m + 1)

    A tournament has logarithmic depth. Among m + 1 records computed by circuits of depth at most D, it has depth at most D + (4 k + 4) ⌈log₂ (m + 1)⌉.

    Records given as inputs #

    source
    def Cslib.Circuits.Boolean.packedTournamentCircuit (k p m : ℕ) :
    Circuit signature ((m + 1) * (k + p)) (k + p)

    The tournament among m + 1 records given as inputs, packed one after the other.

    Instances For
      source
      theorem Cslib.Circuits.Boolean.exists_eval_packedTournamentCircuit {k p m : ℕ} (records : Fin (m + 1) → BitString (k + p)) :
      ∃ (i : Fin (m + 1)), (packedTournamentCircuit k p m).eval interpretation (BitString.packRecords records) = records i ∧ ∀ (j : Fin (m + 1)), (BitString.equivFin k) (records i).recordKey ≤ (BitString.equivFin k) (records j).recordKey

      The packed tournament selects a least key.

      source
      @[simp]
      theorem Cslib.Circuits.Boolean.size_packedTournamentCircuit (k p m : ℕ) :
      (packedTournamentCircuit k p m).size = m * (8 * k + 3 * p + 2)
      source
      theorem Cslib.Circuits.Boolean.depth_packedTournamentCircuit_le (k p m : ℕ) :
      (packedTournamentCircuit k p m).depth ≤ (4 * k + 4) * Nat.clog 2 (m + 1)

      The packed tournament has logarithmic depth: (4 k + 4) ⌈log₂ (m + 1)⌉.