Documentation

Complexitylib.RationalHitting.Internal.OutputComputation

Rational hitting lists: output computation #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/OutputComputation.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

source
def Complexity.RationalHitting.StackLanguage.unaryScanBody :
Program (Fin 3)

Strip the one literal separator of the required unary input, remembering its first field in a separate finite stack.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.RationalHitting.StackLanguage.unaryScan :
    Program (Fin 3)

    Copy a unary input segment until its scan register is exhausted.

    Equations
    Instances For
      source
      theorem Complexity.RationalHitting.StackLanguage.eval_unaryScan (n : ℕ) (w : List Bool) (s : Store (Fin 3)) (h0 : s 0 = List.replicate n true ++ false :: w) (h2 : s 2 = [true]) :
      Eval unaryScan s (Function.update (Function.update (Function.update s 0 w) 1 (List.replicate n true ++ s 1)) 2 []) (3 * n + 8)
      source
      def Complexity.RationalHitting.StackLanguage.Procedure.unaryInput :
      Procedure (fun (a : ℕ × ℕ) => ExecutableGenerator.unaryWord a.1 a.2) code fun (a : ℕ × ℕ) => ({ val := a.1 }, { val := a.2 })

      A fixed three-stack parser for the literal, unescaped unary input. Its output is the ordinary typed pair coding used by the closure library.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Complexity.RationalHitting.StackLanguage.Runtime.word (p : Params) :
        BitWord

        Literal canonical output, including dimension and accepted-list length.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Complexity.RationalHitting.StackLanguage.Runtime.word_poly :
          Poly word
          source
          theorem Complexity.RationalHitting.StackLanguage.Runtime.word_eq (n s : ℕ) :
          (word (Params.of n s)).val = ExecutableGenerator.encoded n s
          source
          theorem Complexity.RationalHitting.StackLanguage.Runtime.word_ext {x y : BitWord} (h : x.val = y.val) :
          x = y
          source
          theorem Complexity.RationalHitting.StackLanguage.Runtime.output_poly :
          Poly fun (a : Unary × Unary) => { val := ExecutableGenerator.encoded a.1.val a.2.val }
          source
          theorem Complexity.RationalHitting.StackLanguage.Runtime.raw_feasible :
          Feasible (fun (a : ℕ × ℕ) => ExecutableGenerator.unaryWord a.1 a.2) (fun (x : List Bool) => x) fun (a : ℕ × ℕ) => (ExecutableGenerator.encoded a.1 a.2).reverse

          Polynomial feasibility of the canonical output construction.