OAI/Computability/MaxCut/Machines/MachineFieldTemplate.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MaxCutGames.Reduction.MachineFieldTemplate.Token line 14
  2. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.tokenOutput line 19
  3. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.templateOutput line 23
  4. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.tokenSteps line 26
  5. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.workSteps line 30
  6. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.templateSteps line 33
  7. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.copiedLength line 36
  8. inductive OAI.MaxCutGames.Reduction.MachineFieldTemplate.Label line 39
  9. abbrev OAI.MaxCutGames.Reduction.MachineFieldTemplate.State line 47
  10. abbrev OAI.MaxCutGames.Reduction.MachineFieldTemplate.Alphabet line 48
  11. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.reset line 50
  12. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.reset_reset line 52
  13. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.startAt line 54
  14. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.jump line 57
  15. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.identityEmit line 62
  16. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.instruction line 66

    Source documentation

    Local finite labels are placed in an arbitrary caller label space, with an explicit continuation. Every instruction is determined by the fixed template.

    def instruction (tokens : List (Token q)) (field : Fin q → K) (scratch output : K)
    (place : Label tokens.length → Λ) (exit : Option Λ) :
    Label tokens.length → TM2.Stmt (Alphabet (K := K)) Λ (State σ)
…

    Mentions: OAI.MaxCutGames.Reduction.MachineFieldTemplate.Token, OAI.MaxCutGames.Reduction.MachineFieldTemplate.Label, OAI.MaxCutGames.Reduction.MachineFieldTemplate.Alphabet, OAI.MaxCutGames.Reduction.MachineFieldTemplate.State

  17. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.program line 86

    Source documentation

    A standalone local program, also usable with a local continuation.

    def program (tokens : List (Token q)) (field : Fin q → K) (scratch output : K)
    (exit : Option (Label tokens.length)) :
    Label tokens.length → TM2.Stmt (Alphabet (K := K)) (Label tokens.length) (State σ) :=
…

    Mentions: OAI.MaxCutGames.Reduction.MachineFieldTemplate.Token, OAI.MaxCutGames.Reduction.MachineFieldTemplate.Label, OAI.MaxCutGames.Reduction.MachineFieldTemplate.Alphabet, OAI.MaxCutGames.Reduction.MachineFieldTemplate.State

  18. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.outputTapes line 93
  19. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.outputTapes_self line 96
  20. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.outputTapes_output line 99
  21. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.outputTapes_other line 102
  22. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.outputTapes_append line 106
  23. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.fieldValues_outputTapes line 111
  24. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.identity_output line 117
  25. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.chain_inline_MachineFieldTemplate line 123
  26. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.doneStep line 139
  27. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.literalStep line 146
  28. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.copySetupStep line 157
  29. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.copyTrace line 167
  30. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.tokenTrace line 190
  31. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.suffixTrace_inline_MachineFieldTemplate line 207
  32. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.phaseTrace line 253

    Source documentation

    The complete phase is derived from concrete instruction traces. The code placement premise identifies instructions; it assumes no whole-phase run.

    theorem phaseTrace (base : K → List Bool) (scratchEmpty : base scratch = [])
    (state : State σ) :
    (MachineComposition.advance (TM2.step P))^[templateSteps tokens (fun j => base (field j))]
      (some ⟨some (place (startAt tokens.length 0)), state, base⟩) =
      some ⟨exit, reset state,
        outputTapes base output (templateOutput tokens (fun j => base (field j)))⟩ := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineFieldTemplate.State, OAI.MaxCutGames.Reduction.MachineFieldTemplate.templateSteps, OAI.MaxCutGames.Reduction.MachineFieldTemplate.startAt, OAI.MaxCutGames.Reduction.MachineFieldTemplate.reset, OAI.MaxCutGames.Reduction.MachineFieldTemplate.outputTapes, OAI.MaxCutGames.Reduction.MachineFieldTemplate.templateOutput

  33. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.programTrace line 267

    Source documentation

    Direct execution of the emitted local finite program; its instructions are discharged by construction rather than supplied by the caller.

    theorem programTrace (tokens : List (Token q)) (field : Fin q → K) (scratch output : K)
    (fieldScratch : ∀ j, field j ≠ scratch) (fieldOutput : ∀ j, field j ≠ output)
    (scratchOutput : scratch ≠ output) (exit : Option (Label tokens.length))
    (base : K → List Bool) (scratchEmpty : base scratch = []) (state : State σ) :
    (MachineComposition.advance (TM2.step (program tokens field scratch output exit)))^[
      templateSteps tokens (fun j => base (field j))]
      (some ⟨some (startAt tokens.length 0), state, base⟩) =
      some ⟨exit, reset state,
        outputTapes base output (templateOutput tokens (fun j => base (field j)))⟩ :=
…

    Mentions: OAI.MaxCutGames.Reduction.MachineFieldTemplate.Token, OAI.MaxCutGames.Reduction.MachineFieldTemplate.Label, OAI.MaxCutGames.Reduction.MachineFieldTemplate.State, OAI.MaxCutGames.Reduction.MachineFieldTemplate.program, OAI.MaxCutGames.Reduction.MachineFieldTemplate.templateSteps, OAI.MaxCutGames.Reduction.MachineFieldTemplate.startAt, OAI.MaxCutGames.Reduction.MachineFieldTemplate.reset, OAI.MaxCutGames.Reduction.MachineFieldTemplate.outputTapes, OAI.MaxCutGames.Reduction.MachineFieldTemplate.templateOutput

  34. theorem OAI.MaxCutGames.Reduction.MachineFieldTemplate.templateSteps_le line 279
  35. def OAI.MaxCutGames.Reduction.MachineFieldTemplate.phaseInTime line 292