OAI/Computability/MaxCut/Machines/MachineCanonicalOutput.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Canonical output for finite Boolean machines

A raw machine may halt with retained metadata and a changed finite state. This wrapper redirects its halt to a fixed list of actual tape drains, then executes one state-reset instruction. The output tape is preserved and the result is literally haltList. Its cost follows from the raw execution and the maximum number of pushes in a raw statement.

The cleanup list is fixed with the program, not selected from the input. It may contain repetitions and may be empty when output is the only tape.

  1. structure OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.Program line 24

    Source documentation

    The homogeneous parts of a finite machine, without dependent alphabet casts.

    structure Program (K Λ σ : Type) where
…
  2. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.extendedLabel line 35
  3. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.extendedCfg line 39
  4. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.extendedStmt line 45

    Source documentation

    Add one finite scratch register while preserving each raw transition.

    def extendedStmt (labels : Λ → Λ') (haltTarget : Option Λ') :
    TM2.Stmt (fun _ : K => Bool) Λ σ →
      TM2.Stmt (fun _ : K => Bool) Λ' (σ × Option Bool)
  | .push k f next => .push k (fun state => f state.1)
      (extendedStmt labels haltTarget next)
  | .peek k f next => .peek k (fun state symbol => (f state.1 symbol, state.2))
      (extendedStmt labels haltTarget next)
  | .pop k f next => .pop k (fun state symbol => (f state.1 symbol, state.2))
      (extendedStmt labels haltTarget next)
  | .load f next => .load (fun state => (f state.1, state.2))
      (extendedStmt labels haltTarget next)
  | .branch test yes no => .branch (fun state => test state.1)
…
  5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.stepAux_extended line 63
  6. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.sourceMachine line 87
  7. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.Label line 98
  8. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.cleanupLabel line 100
  9. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.resetLabel line 103
  10. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.cleanupEntry line 105
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.completedProgram line 108
  12. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.completedMachine line 116

    Source documentation

    A fixed finite program over the same Boolean tapes as the raw machine.

    def completedMachine (P : Program K Λ σ) (chosen : List K) : FinTM2 where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.Program

  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.finiteAlphabet line 127
  14. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.embeddedCfg line 132
  15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.step_simulation line 136
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.embedded_init line 152
  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.finalTapes_eq line 157
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.haltList_eq line 168
  19. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.cleanupExecution line 174

    Source documentation

    The cleanup path consists of actual drains and one physical state reset.

    def cleanupExecution (P : Program K Λ σ) (chosen : List K)
    (complete : ∀ k, k ∈ chosen ↔ k ≠ P.output) (state : σ)
    (register : Option Bool) (base : K → List Bool) :
    StateTransition.EvalsToInTime (completedMachine P chosen).step
      ⟨cleanupEntry chosen, (state, register), base⟩
      (some (haltList (completedMachine P chosen) (base P.output)))
      (MachineDrainMany.steps chosen base + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.Program, OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.completedMachine, OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.cleanupEntry, OAI.MaxCutGames.Foundations.Complexity.MachineDrainMany.steps

  20. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.outputsInTime line 206

    Source documentation

    No assumption about cleanup execution or clean raw work tapes is required.

    def outputsInTime (P : Program K Λ σ) (chosen : List K)
    (complete : ∀ k, k ∈ chosen ↔ k ≠ P.output)
    (input output : List Bool) (state : σ) (base : K → List Bool) (budget : Nat)
    (raw : StateTransition.EvalsToInTime (sourceMachine P).step
      (initList (sourceMachine P) input) (some ⟨none, state, base⟩) budget)
    (correctOutput : base P.output = output) :
    TM2OutputsInTime (completedMachine P chosen) input (some output)
      (budget + chosen.length *
        (input.length + budget * Runtime.programPushBound (sourceMachine P) + 1) + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.Program, OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.sourceMachine, OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.completedMachine, OAI.MaxCutGames.Foundations.Complexity.Runtime.programPushBound

  21. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.completedTime line 231
  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.completedTime_eval line 236
  23. structure OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.TerminalRun line 244

    Source documentation

    An actual raw terminal execution, with arbitrary remaining state and tapes.

    structure TerminalRun (P : Program K Λ σ) (input output : List Bool) (budget : Nat) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.Program

  24. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime line 252

    Source documentation

    A polynomial raw run becomes a full canonical-output computation certificate.

    noncomputable def computableInPolyTime {α β : Type}
    (P : Program K Λ σ) (chosen : List K)
    (complete : ∀ k, k ∈ chosen ↔ k ≠ P.output)
    (encodeIn : α → List Bool) (encodeOut : β → List Bool) (f : α → β)
    (rawTime : Polynomial Nat)
    (run : ∀ a, TerminalRun P (encodeIn a) (encodeOut (f a))
      (rawTime.eval (encodeIn a).length)) :
    TM2ComputableInPolyTime encodeIn encodeOut f where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.Program, OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.TerminalRun

  25. theorem OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime_finite_alphabet line 275
  26. def OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTimeOfEnumeration line 287

    Source documentation

    An explicit finite enumeration supplies the fixed cleanup list.

    noncomputable def computableInPolyTimeOfEnumeration {α β : Type} {N : Nat}
    (P : Program K Λ σ) (enumeration : Fin N ≃ K)
    (encodeIn : α → List Bool) (encodeOut : β → List Bool) (f : α → β)
    (rawTime : Polynomial Nat)
    (run : ∀ a, TerminalRun P (encodeIn a) (encodeOut (f a))
      (rawTime.eval (encodeIn a).length)) :
    TM2ComputableInPolyTime encodeIn encodeOut f :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.Program, OAI.MaxCutGames.Foundations.Complexity.MachineCanonicalOutput.TerminalRun