OAI/Computability/UniqueGames/Reduction/MachineTransducer.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.tapeStacks line 14
2. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.update_input line 17
3. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.update_output line 22
4. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.output line 30

   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

5. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.loop line 36
6. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.program line 43
7. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.machine line 51
8. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.maxEmission line 64

   Source documentation

   A finite maximum depending only on the fixed emission table.

   noncomputable def maxEmission (emit : Q → Bool → List Bool) : Nat :=
   …

9. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.emission_le line 67
10. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.statementPushBound_le line 72
11. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.programPushBound_le line 81
12. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.running line 92
13. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.emitting line 97
14. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.halted line 102
15. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.step_empty line 107

    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.UniqueGamesTheorem.Reduction.MachineTransducer.machine, OAI.UniqueGamesTheorem.Reduction.MachineTransducer.running, OAI.UniqueGamesTheorem.Reduction.MachineTransducer.halted

16. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.step_cons line 118
17. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.step_emit line 131

    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.UniqueGamesTheorem.Reduction.MachineTransducer.machine, OAI.UniqueGamesTheorem.Reduction.MachineTransducer.emitting, OAI.UniqueGamesTheorem.Reduction.MachineTransducer.running

18. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.next line 151
19. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.two_steps_cons line 156
20. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.transduce_steps line 170

    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.UniqueGamesTheorem.Reduction.MachineTransducer.next, OAI.UniqueGamesTheorem.Reduction.MachineTransducer.running, OAI.UniqueGamesTheorem.Reduction.MachineTransducer.halted, OAI.UniqueGamesTheorem.Reduction.MachineTransducer.output

21. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.initList_eq line 187
22. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.haltList_eq line 196
23. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.transduce_init_steps line 203
24. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.outputsInTime line 211
25. theorem OAI.UniqueGamesTheorem.Reduction.MachineTransducer.outputsInTime_steps line 219
26. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.reversedComputableInPolyTime line 224

    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.UniqueGamesTheorem.Reduction.MachineTransducer.output

27. def OAI.UniqueGamesTheorem.Reduction.MachineTransducer.computableInPolyTime line 245

    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.UniqueGamesTheorem.Reduction.MachineTransducer.output