Documentation

Complexitylib.Models.RandomAccessMachine.Structured.PairValidate.Defs

Structured RAM pair-encoding validator — definitions #

The benchmark-specific implementation is just a numeric presentation of the same five-state automaton used by TM.pairValidateTM. The generic scanner compiler supplies the table-driven structured RAM program.

source
@[implicit_reducible]
instance Complexity.RAM.Structured.PairValidate.instFinEnumPairValidateState :
FinEnum TM.PairValidateState
Equations
  • One or more equations did not get rendered due to their size.
source
def Complexity.RAM.Structured.PairValidate.typedSpec :
Scanner.TypedSpec TM.PairValidateState

Pair validation as a typed finite-state scanner specification.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Complexity.RAM.Structured.PairValidate.spec :
    Scanner.Spec

    Numeric lowering used by the generic structured RAM compiler.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Complexity.RAM.Structured.PairValidate.lengthReg :
      ℕ

      Final verdict register inherited from the scanner layout.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Complexity.RAM.Structured.PairValidate.inputBase :
        ℕ

        First input register for the five-state instance.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Complexity.RAM.Structured.PairValidate.inputStore :
          List Bool → Store

          Reserved-prefix input store for pair validation.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Complexity.RAM.Structured.PairValidate.program :
            Cmd

            Structured RAM pair-validator program.

            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev Complexity.RAM.Structured.PairValidate.compiled :
              Program

              Concrete compiled RAM pair-validator program.

              Equations
              Instances For
                source
                @[reducible, inline]
                abbrev Complexity.RAM.Structured.PairValidate.stepCount :
                ℕ → ℕ

                Exact compiled transition count.

                Equations
                Instances For
                  source
                  @[reducible, inline]
                  abbrev Complexity.RAM.Structured.PairValidate.timeBound :
                  ℕ → ℕ

                  Explicit logarithmic-time budget.

                  Equations
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev Complexity.RAM.Structured.PairValidate.spaceBound :
                    ℕ → ℕ

                    Explicit peak-space budget.

                    Equations
                    Instances For
                      source
                      @[reducible, inline]
                      abbrev Complexity.RAM.Structured.PairValidate.quasilinearBound :
                      ℕ → ℕ

                      Shifted quasilinear comparison function.

                      Equations
                      Instances For