OAI/Computability/MaxCut/Machines/MachineSequential.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

A concrete sequential composition of two finite TM2 programs. The first output is transferred to a temporary stack and then to the second input. Both loops execute actual transitions and reset their shared register on exit. Static renaming changes neither a stack word nor the number of executed transitions.

  1. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineSequential.Tape line 17
  2. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineSequential.Symbols line 18
  3. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineSequential.Label line 21
  4. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineSequential.Register line 22
  5. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineSequential.State line 23
  6. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.firstStates line 25
  7. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.secondStates line 32
  8. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.secondLabels line 39
  9. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.bridgeLabel line 45
  10. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.firstStatement line 48
  11. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.secondStatement line 53
  12. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.program line 61
  13. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.machine line 77
  14. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.firstConfiguration line 104
  15. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.secondConfiguration line 110
  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineSequential.firstStep line 119
  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineSequential.secondStep line 149
  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineSequential.firstConfiguration_init line 174
  19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineSequential.secondConfiguration_halt line 190
  20. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.temporaryTapes line 207
  21. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.temporaryConfiguration line 213
  22. theorem OAI.MaxCutGames.Foundations.Complexity.MachineSequential.firstTransfer_tapes line 218
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineSequential.secondTransfer_tapes line 237
  24. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.firstTransfer line 260
  25. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.secondTransfer line 281
  26. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.execute line 299

    Source documentation

    An execution of each component yields an actual execution of the combined machine. The two transfer loops add exactly twice the intermediate length plus two.

    def execute (first second : FinTM2)
    (relabel : first.Γ first.k₁ → second.Γ second.k₀)
    (fallback : second.Γ second.k₀)
    (input : List (first.Γ first.k₀)) (middle : List (first.Γ first.k₁))
    (output : List (second.Γ second.k₁)) (firstBudget secondBudget : Nat)
    (runFirst : TM2OutputsInTime first input (some middle) firstBudget)
    (runSecond : TM2OutputsInTime second (middle.map relabel) (some output) secondBudget) :
    TM2OutputsInTime (machine first second relabel fallback) input (some output)
      (firstBudget + 2 * (middle.length + 1) + secondBudget) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineSequential.machine

  27. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.compose line 332

    Source documentation

    General sequential composition with an explicit symbol of the intermediate alphabet to totalize the bridge's unused empty-register expression. Its time polynomial uses the transition-derived output-length bound of the first machine.

    noncomputable def compose {α β γ αΓ βΓ γΓ : Type}
    {ea : α → List αΓ} {eb : β → List βΓ} {ec : γ → List γΓ}
    {f : α → β} {g : β → γ}
    (first : TM2ComputableInPolyTime ea eb f)
    (second : TM2ComputableInPolyTime eb ec g) (fallback : βΓ) :
    TM2ComputableInPolyTime ea ec (fun a => g (f a)) := by
…
  28. def OAI.MaxCutGames.Foundations.Complexity.MachineSequential.composeBits line 379
  29. def OAI.MaxCutGames.Reduction.MachineTransducer.tapeStacks line 395
  30. theorem OAI.MaxCutGames.Reduction.MachineTransducer.update_input_inline_MachineTransducer line 398
  31. theorem OAI.MaxCutGames.Reduction.MachineTransducer.update_output_inline_MachineTransducer line 403
  32. def OAI.MaxCutGames.Reduction.MachineTransducer.output line 411

    Source documentation

    The semantic output, with the control state updated after each input bit.

    def output (transition : Q → Bool → Q) (emit : Q → Bool → List Bool) :
    Q → List Bool → List Bool
  | _, [] => []
  | state, symbol :: input =>
      emit state symbol ++ output transition emit (transition state symbol) input
  33. def OAI.MaxCutGames.Reduction.MachineTransducer.loop line 417
  34. def OAI.MaxCutGames.Reduction.MachineTransducer.program line 424
  35. def OAI.MaxCutGames.Reduction.MachineTransducer.machine line 432
  36. def OAI.MaxCutGames.Reduction.MachineTransducer.maxEmission line 445

    Source documentation

    A finite maximum depending only on the fixed emission table.

    noncomputable def maxEmission (emit : Q → Bool → List Bool) : Nat :=
…
  37. theorem OAI.MaxCutGames.Reduction.MachineTransducer.emission_le line 448
  38. theorem OAI.MaxCutGames.Reduction.MachineTransducer.statementPushBound_le line 453
  39. theorem OAI.MaxCutGames.Reduction.MachineTransducer.programPushBound_le line 462
  40. def OAI.MaxCutGames.Reduction.MachineTransducer.running line 473
  41. def OAI.MaxCutGames.Reduction.MachineTransducer.emitting line 478
  42. def OAI.MaxCutGames.Reduction.MachineTransducer.halted line 483
  43. theorem OAI.MaxCutGames.Reduction.MachineTransducer.step_empty line 488

    Source documentation

    The final empty pop also restores the initial finite control state.

    theorem step_empty (initial : Q) (transition : Q → Bool → Q)
    (emit : Q → Bool → List Bool) (state : Q) (accumulator : List Bool)
    (register : Option Bool) :
    (machine initial transition emit).step
        (running initial transition emit state [] accumulator register) =
      some (halted initial transition emit accumulator) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransducer.machine, OAI.MaxCutGames.Reduction.MachineTransducer.running, OAI.MaxCutGames.Reduction.MachineTransducer.halted

  44. theorem OAI.MaxCutGames.Reduction.MachineTransducer.step_cons line 499
  45. theorem OAI.MaxCutGames.Reduction.MachineTransducer.step_emit line 512

    Source documentation

    Emission reads the old state from its label and installs its successor state.

    theorem step_emit (initial : Q) (transition : Q → Bool → Q)
    (emit : Q → Bool → List Bool) (oldState : Q) (symbol : Bool)
    (input accumulator : List Bool) (state : Q × Option Bool) :
    (machine initial transition emit).step
        (emitting initial transition emit oldState symbol input accumulator state) =
      some (running initial transition emit (transition oldState symbol) input
        ((emit oldState symbol).reverse ++ accumulator) state.2) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransducer.machine, OAI.MaxCutGames.Reduction.MachineTransducer.emitting, OAI.MaxCutGames.Reduction.MachineTransducer.running

  46. def OAI.MaxCutGames.Reduction.MachineTransducer.next line 530
  47. theorem OAI.MaxCutGames.Reduction.MachineTransducer.two_steps_cons line 535
  48. theorem OAI.MaxCutGames.Reduction.MachineTransducer.transduce_steps line 549

    Source documentation

    Exact execution from any finite control state, accumulator, and symbol register.

    theorem transduce_steps (initial : Q) (transition : Q → Bool → Q)
    (emit : Q → Bool → List Bool) (state : Q) (input accumulator : List Bool)
    (register : Option Bool) :
    (next initial transition emit)^[2 * input.length + 1]
        (some (running initial transition emit state input accumulator register)) =
      some (halted initial transition emit ((output transition emit state input).reverse ++ accumulator)) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransducer.next, OAI.MaxCutGames.Reduction.MachineTransducer.running, OAI.MaxCutGames.Reduction.MachineTransducer.halted, OAI.MaxCutGames.Reduction.MachineTransducer.output

  49. theorem OAI.MaxCutGames.Reduction.MachineTransducer.initList_eq line 566
  50. theorem OAI.MaxCutGames.Reduction.MachineTransducer.haltList_eq line 575
  51. theorem OAI.MaxCutGames.Reduction.MachineTransducer.transduce_init_steps line 582
  52. def OAI.MaxCutGames.Reduction.MachineTransducer.outputsInTime line 590
  53. theorem OAI.MaxCutGames.Reduction.MachineTransducer.outputsInTime_steps line 598
  54. def OAI.MaxCutGames.Reduction.MachineTransducer.reversedComputableInPolyTime line 603

    Source documentation

    Reversed transducer output in polynomial 2 * X + 1 time.

    noncomputable def reversedComputableInPolyTime (initial : Q) (transition : Q → Bool → Q)
    (emit : Q → Bool → List Bool) :
    TM2ComputableInPolyTime (id : List Bool → List Bool) id
      (fun input => (output transition emit initial input).reverse) where
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransducer.output

  55. def OAI.MaxCutGames.Reduction.MachineTransducer.computableInPolyTime line 624

    Source documentation

    Forward transducer output, using the checked actual reversal composition.

    noncomputable def computableInPolyTime (initial : Q) (transition : Q → Bool → Q)
    (emit : Q → Bool → List Bool) :
    TM2ComputableInPolyTime (id : List Bool → List Bool) id
      (output transition emit initial) := by
…

    Mentions: OAI.MaxCutGames.Reduction.MachineTransducer.output

  56. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.Alphabet line 641
  57. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.State line 642
  58. def OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.scanLoop line 644
  59. def OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.emitter line 653
  60. abbrev OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.tapes line 659
  61. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.update_source_inline_MachineTransducerCopy line 663
  62. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.update_scratch_inline_MachineTransducerCopy line 678
  63. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.update_output_inline_MachineTransducerCopy line 690
  64. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.scanStep_empty line 696
  65. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.scanStep_cons line 714
  66. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.emitterStep line 732
  67. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.twoSteps_cons line 753
  68. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.scanTrace line 779
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.restoreTapes line 813
  70. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.transduceCopyTrace line 832
  71. def OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.transduceCopyInTime line 878
  72. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.scanLoop_pushBound line 904
  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachineTransducerCopy.emitter_pushBound line 910