Documentation

Complexitylib.Models.TuringMachine.Subroutines.BinaryFor.Defs

Canonical binary count-up loops — definitions #

This module defines an output-safe loop driver for a body indexed by a canonical little-endian binary counter. A second, distinct work tape stores a preserved limit. Before each iteration, the driver compares the two tapes in lockstep, remembers whether every scanned symbol agreed, and rewinds both heads to cell one. Equality halts the loop; inequality runs the body and then increments the counter with TM.binarySuccTM.

The comparison deliberately scans through the full limit width even after a mismatch. Under the intended invariant counter ≤ limit, this gives the value-independent exact comparison time 2 * limit.size + 2. The controller never moves the output head left and does not alter its contents; output behavior during an iteration is entirely delegated to the body.

The wrapper-free certificate structures at the end of the file separate the executable controller from later correctness and all-prefix space proofs.

source
inductive Complexity.TM.BinaryForPhase :
Type

Controller phases for a canonical binary count-up loop.

The Boolean carried by scan and rewind records whether the counter and limit symbols seen so far were equal.

Instances For
    source
    @[implicit_reducible]
    instance Complexity.TM.instDecidableEqBinaryForPhase :
    DecidableEq BinaryForPhase
    Equations
    source
    def Complexity.TM.instDecidableEqBinaryForPhase.decEq (x✝ x✝¹ : BinaryForPhase) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Complexity.TM.instFintypeBinaryForPhase :
      Fintype BinaryForPhase

      BinaryForPhase is finite, as required by the concrete machine model.

      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Complexity.TM.binaryForIterationTM {n : ℕ} (body : TM n) (counterIdx : Fin n) :
      TM n

      One count-up iteration: run body, take the seqTM seam, and increment the designated canonical binary counter.

      Equations
      Instances For
        source
        def Complexity.TM.binaryForTM {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) :
        TM n

        Count upward from a canonical binary counter to a preserved canonical binary limit.

        The intended correctness interface assumes counterIdx ≠ limitIdx. In the driver phases both work heads move in lockstep. A complete scan records tape equality without writing a verdict, and a complete rewind either halts or enters binaryForIterationTM body counterIdx. When that composite iteration halts, one content-preserving seam returns to a fresh equality scan.

        Input, unrelated work tapes, and output use read-back/idle actions throughout the controller. In particular, the driver itself is compatible with append-only output; any output writes come only from body.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.TM.binaryForCompareTime (limit : ℕ) :
          ℕ

          Exact time for one full-width equality scan and synchronized rewind when the counter is bounded by limit.

          Equations
          Instances For
            source
            def Complexity.TM.binaryForIterationTime (bodyTime : ℕ → ℕ) (value : ℕ) :
            ℕ

            Exact time of the composite iteration before the outer loopback seam: the body run, one seqTM transition, and canonical binary successor.

            Equations
            Instances For
              source
              def Complexity.TM.binaryForLoopTime (bodyTime : ℕ → ℕ) (limit value : ℕ) :
              ℕ → ℕ

              Exact remaining count-up-loop time.

              value is the current counter and count is the number of nonterminal iterations remaining. The zero case performs the final successful comparison. Each successor case performs one unsuccessful comparison, one composite iteration, one outer loopback seam, and the remaining loop. Intended uses supply value + count = limit.

              Equations
              Instances For
                source
                structure Complexity.TM.BinaryForLoopSpec {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (bodyTime : ℕ → ℕ) (limitValue : ℕ) :
                Type

                Wrapper-free certificate for exact control flow of a canonical binary count-up loop.

                All configurations use the public state type of binaryForTM body counterIdx limitIdx. The client supplies the intended canonical configuration family and proves that a nonterminal test reaches the composite iteration, which runs the body and successor before one loopback step advances to the next scanner configuration. At limitValue, the client supplies the final comparison run.

                Instances For
                  source
                  structure Complexity.TM.BinaryForLoopSpaceSpec {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {limitValue : ℕ} (spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue) (inputLength spaceBound : ℕ) :
                  Prop

                  All-prefix auxiliary-space obligations for a certified binary count-up loop. The comparison and composite-iteration obligations concern prefixes of their advertised exact runs; later execution may already have crossed the corresponding seam.

                  Instances For