OAI/Computability/MaxCut/Machines/AddressMachineProgram.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MaxCutGames.Reduction.AddressMachineProgram.Tape line 14
2. abbrev OAI.MaxCutGames.Reduction.AddressMachineProgram.State line 16
3. def OAI.MaxCutGames.Reduction.AddressMachineProgram.accumulator line 20
4. def OAI.MaxCutGames.Reduction.AddressMachineProgram.output line 21
5. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.accumulator_ne_output line 23
6. def OAI.MaxCutGames.Reduction.AddressMachineProgram.clearKeys line 27

   Source documentation

   The finalizer visits every other tape in a fixed finite order.

   def clearKeys : List (Tape k T) := by
   …

   Mentions: OAI.MaxCutGames.Reduction.AddressMachineProgram.Tape

7. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.mem_clearKeys line 32
8. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.accumulator_not_mem_clearKeys line 37
9. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.output_not_mem_clearKeys line 38
10. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.clearKeys_covers line 40
11. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.clearKeys_nodup line 43
12. abbrev OAI.MaxCutGames.Reduction.AddressMachineProgram.HeaderLabel line 47
13. abbrev OAI.MaxCutGames.Reduction.AddressMachineProgram.BodyLabel line 48
14. abbrev OAI.MaxCutGames.Reduction.AddressMachineProgram.FinishLabel line 50
15. inductive OAI.MaxCutGames.Reduction.AddressMachineProgram.Label line 52
16. def OAI.MaxCutGames.Reduction.AddressMachineProgram.headerLabels line 62
17. def OAI.MaxCutGames.Reduction.AddressMachineProgram.initializeLabels line 63
18. def OAI.MaxCutGames.Reduction.AddressMachineProgram.bodyLabels line 64
19. def OAI.MaxCutGames.Reduction.AddressMachineProgram.finishLabels line 65
20. def OAI.MaxCutGames.Reduction.AddressMachineProgram.start line 67
21. def OAI.MaxCutGames.Reduction.AddressMachineProgram.initializeStart line 68
22. def OAI.MaxCutGames.Reduction.AddressMachineProgram.bodyStart line 69
23. def OAI.MaxCutGames.Reduction.AddressMachineProgram.checkLabel line 70
24. def OAI.MaxCutGames.Reduction.AddressMachineProgram.resetLabel line 71
25. def OAI.MaxCutGames.Reduction.AddressMachineProgram.finishStart line 72
26. def OAI.MaxCutGames.Reduction.AddressMachineProgram.next line 74
27. def OAI.MaxCutGames.Reduction.AddressMachineProgram.resetAt line 77
28. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.next_lt line 80
29. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.next_ge line 82
30. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.resetAt_lt line 84
31. def OAI.MaxCutGames.Reduction.AddressMachineProgram.program line 89

    Source documentation

    Header, digit initialization, physical tuple body, carry loops, and complete finalization are placed in a single actual finite transition program.

    def program : Label k T → TM2.Stmt (fun _ : Tape k T => Bool) (Label k T) (State k)
      | .header l => MachineAddressHeaders.statement
          (AddressMachineSpace.fullHeaderSlots k s d T.vectors.length)
          (headerLabels k T) (some (initializeStart k T)) l
      | .initialize l => MachineOdometerInit.statement
          (AddressMachineSpace.odometerSlots k s d T.vectors.length)
          (initializeLabels k T) (some (bodyStart k T)) l
      | .body l => Integration.AddressTupleBody.instruction (AddressOutcomeSpecs.rows k T)
          (bodyLabels k T) (some (next k T 0)) l
      | .check j => MachineTupleOdometer.increment
          (AddressMachineSpace.current k s d T.vectors.length j)
          (AddressMachineSpace.remaining k s d T.vectors.length j)
    …

    Mentions: OAI.MaxCutGames.Reduction.AddressMachineProgram.Label, OAI.MaxCutGames.Reduction.AddressMachineProgram.Tape, OAI.MaxCutGames.Reduction.AddressMachineProgram.State, OAI.MaxCutGames.Reduction.MachineAddressHeaders.statement, OAI.MaxCutGames.Reduction.AddressMachineSpace.fullHeaderSlots, OAI.MaxCutGames.Reduction.AddressMachineProgram.headerLabels, OAI.MaxCutGames.Reduction.AddressMachineProgram.initializeStart, OAI.MaxCutGames.Reduction.AddressMachineSpace.odometerSlots, OAI.MaxCutGames.Reduction.AddressMachineProgram.initializeLabels, OAI.MaxCutGames.Reduction.AddressMachineProgram.bodyStart, OAI.MaxCutGames.Integration.AddressTupleBody.instruction, OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.rows, OAI.MaxCutGames.Reduction.AddressMachineProgram.bodyLabels, OAI.MaxCutGames.Reduction.AddressMachineProgram.next, OAI.MaxCutGames.Reduction.AddressMachineSpace.current, OAI.MaxCutGames.Reduction.AddressMachineSpace.remaining

32. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.atHeader line 111
33. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.atInitialize line 115
34. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.atBody line 120
35. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.atCheck line 124
36. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.atReset line 129
37. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.atFinish line 134
38. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.finishStartStep line 139

    Source documentation

    This bridge has no data-dependent action and costs exactly one transition.

    theorem finishStartStep (state : State k) (base : Tape k T → List Bool) :
        TM2.step (program k T) ⟨some (finishStart k T),state,base⟩ =
          some ⟨SourceRuntimeFinish.entry (clearKeys k T) (finishLabels k T),state,base⟩ := by
    …

    Mentions: OAI.MaxCutGames.Reduction.AddressMachineProgram.State, OAI.MaxCutGames.Reduction.AddressMachineProgram.Tape, OAI.MaxCutGames.Reduction.AddressMachineProgram.program, OAI.MaxCutGames.Reduction.AddressMachineProgram.finishStart, OAI.MaxCutGames.Reduction.AddressMachineProgram.clearKeys, OAI.MaxCutGames.Reduction.AddressMachineProgram.finishLabels

39. def OAI.MaxCutGames.Reduction.AddressMachineProgram.finishStartInTime line 146
40. def OAI.MaxCutGames.Reduction.AddressMachineProgram.machine line 155

    Source documentation

    All alphabets and registers are finite. Counts live solely on Bool stacks.

    def machine : FinTM2 where
    …

41. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.machine_main line 166
42. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.machine_program line 167
43. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.machine_initialState line 168
44. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.machine_input line 169
45. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.machine_output line 170
46. def OAI.MaxCutGames.Reduction.AddressMachineProgram.inputAlphabet line 173

    Source documentation

    Identity alphabet encodings at both ends of the concrete machine.

    def inputAlphabet : (machine k T).Γ (machine k T).k₀ ≃ Bool := Equiv.refl Bool

    Mentions: OAI.MaxCutGames.Reduction.AddressMachineProgram.machine

47. def OAI.MaxCutGames.Reduction.AddressMachineProgram.outputAlphabet line 174
48. def OAI.MaxCutGames.Reduction.AddressMachineProgram.inputTapes line 176
49. def OAI.MaxCutGames.Reduction.AddressMachineProgram.outputTapes line 179
50. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.inputTapes_source line 182
51. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.inputTapes_other line 185
52. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.outputTapes_output line 188
53. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.outputTapes_other line 191
54. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.initList_eq line 194
55. theorem OAI.MaxCutGames.Reduction.AddressMachineProgram.haltList_eq line 206