OAI/Computability/UniqueGames/Machines/MachineBinaryNameMachine.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.BinaryNameMachine.frame line 15
2. def OAI.UniqueGamesTheorem.BinaryNameMachine.finalDigit line 19
3. def OAI.UniqueGamesTheorem.BinaryNameMachine.canonical line 23
4. structure OAI.UniqueGamesTheorem.BinaryNameMachine.Result line 25
5. def OAI.UniqueGamesTheorem.BinaryNameMachine.scanSpec line 32

   Source documentation

   A specification with the same one- or two-symbol cases as the program.

   def scanSpec : List Bool → List Bool → Option Bool → Result
     | [], acc, _ => ⟨false, [], acc⟩
     | false :: rest, acc, last => ⟨last.getD true, rest, acc⟩
     | [true], acc, _ => ⟨false, [], acc⟩
     | true :: bit :: rest, acc, _ => scanSpec rest (bit :: acc) (some bit)

   Mentions: OAI.UniqueGamesTheorem.BinaryNameMachine.Result

6. def OAI.UniqueGamesTheorem.BinaryNameMachine.steps line 38
7. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.steps_le line 42
8. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.frame_length line 51
9. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.scanSpec_frame line 57
10. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.steps_frame line 66
11. abbrev OAI.UniqueGamesTheorem.BinaryNameMachine.Alphabet line 76
12. abbrev OAI.UniqueGamesTheorem.BinaryNameMachine.State line 77
13. def OAI.UniqueGamesTheorem.BinaryNameMachine.clean line 79
14. def OAI.UniqueGamesTheorem.BinaryNameMachine.exitAt line 81
15. def OAI.UniqueGamesTheorem.BinaryNameMachine.finish line 86
16. def OAI.UniqueGamesTheorem.BinaryNameMachine.scan line 90

    Source documentation

    Only the finite head and final-digit registers are inspected by branches.

    def scan (source destination : K) (again : Λ) (accepted rejected : Option Λ) :
        TM2.Stmt (Alphabet (K := K)) Λ (State A) :=
    …

    Mentions: OAI.UniqueGamesTheorem.BinaryNameMachine.Alphabet, OAI.UniqueGamesTheorem.BinaryNameMachine.State

17. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.stepAux_finish line 105
18. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.update_source line 110
19. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.update_destination line 121
20. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.step_empty line 135
21. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.step_end line 143
22. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.step_truncated line 154
23. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.step_digit line 162
24. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.scanTrace line 173

    Source documentation

    Total correspondence, including malformed input and its exact unread suffix.

    theorem scanTrace (input output : List Bool) (last register : Option Bool) :
        (advance (TM2.step program))^[steps input]
          (some ⟨some again, (ambient, last, register),
            tapesAt source destination base input output⟩) =
          some ⟨if (scanSpec input output last).accepted then accepted else rejected,
            clean ambient, tapesAt source destination base
              (scanSpec input output last).remaining (scanSpec input output last).reversedPayload⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.BinaryNameMachine.steps, OAI.UniqueGamesTheorem.BinaryNameMachine.scanSpec, OAI.UniqueGamesTheorem.BinaryNameMachine.clean

25. def OAI.UniqueGamesTheorem.BinaryNameMachine.scanInTime line 208

    Source documentation

    A real timed execution; the instruction equation is the only program premise.

    def scanInTime (input output : List Bool) (last register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some again, (ambient, last, register), tapesAt source destination base input output⟩
          (some ⟨if (scanSpec input output last).accepted then accepted else rejected,
            clean ambient, tapesAt source destination base
              (scanSpec input output last).remaining (scanSpec input output last).reversedPayload⟩)
          (input.length + 1) where
    …

    Mentions: OAI.UniqueGamesTheorem.BinaryNameMachine.scanSpec, OAI.UniqueGamesTheorem.BinaryNameMachine.clean

26. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.framedTrace line 222

    Source documentation

    A complete framed name needs exactly one transition per digit and one for the terminator. No transition inspects the magnitude denoted by the payload.

    theorem framedTrace (bits suffix output : List Bool) (register : Option Bool) :
        (advance (TM2.step program))^[bits.length + 1]
          (some ⟨some again, (ambient, none, register),
            tapesAt source destination base (frame bits ++ suffix) output⟩) =
          some ⟨if canonical bits then accepted else rejected, clean ambient,
            tapesAt source destination base suffix (bits.reverse ++ output)⟩ := by
    …

    Mentions: OAI.UniqueGamesTheorem.BinaryNameMachine.frame, OAI.UniqueGamesTheorem.BinaryNameMachine.canonical, OAI.UniqueGamesTheorem.BinaryNameMachine.clean

27. def OAI.UniqueGamesTheorem.BinaryNameMachine.machine line 237

    Source documentation

    One concrete machine with two Boolean stacks and finite control. The two exit labels expose acceptance to a caller; the scanner leaves them unexecuted.

    def machine : FinTM2 where
    …

28. theorem OAI.UniqueGamesTheorem.BinaryNameMachine.machine_finiteAlphabet line 248
29. def OAI.UniqueGamesTheorem.BinaryNameMachine.machineInTime line 254

    Source documentation

    The bounded run instantiated with the displayed finite machine, including its actual entry and two actual exit labels.

    def machineInTime (input output : List Bool) :
        StateTransition.EvalsToInTime machine.step
          ⟨some (0 : Fin 3), clean (), tapesAt false true (fun _ : Bool => []) input output⟩
          (some ⟨if (scanSpec input output none).accepted then some (1 : Fin 3) else some (2 : Fin 3),
            clean (), tapesAt false true (fun _ : Bool => [])
              (scanSpec input output none).remaining (scanSpec input output none).reversedPayload⟩)
          (input.length + 1) :=
    …

    Mentions: OAI.UniqueGamesTheorem.BinaryNameMachine.clean, OAI.UniqueGamesTheorem.BinaryNameMachine.scanSpec