OAI/Computability/WLIdentification/StackMachines.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.WLIdentification.StackModel.Instruction line 12
2. structure OAI.WLIdentification.StackModel.Program line 19
3. structure OAI.WLIdentification.StackModel.Config line 24
4. def OAI.WLIdentification.StackModel.initial line 31
5. def OAI.WLIdentification.StackModel.step line 34
6. def OAI.WLIdentification.StackModel.run line 46
7. abbrev OAI.WLIdentification.StackModel.Alphabet line 49
8. inductive OAI.WLIdentification.StackModel.Phase line 51
9. def OAI.WLIdentification.StackModel.emptyData line 62
10. def OAI.WLIdentification.StackModel.inputData line 64
11. def OAI.WLIdentification.StackModel.symbol line 67
12. def OAI.WLIdentification.StackModel.decodeSymbol line 73
13. theorem OAI.WLIdentification.StackModel.symbol_empty line 78
14. theorem OAI.WLIdentification.StackModel.symbol_input line 81
15. theorem OAI.WLIdentification.StackModel.decode_symbol line 94
16. def OAI.WLIdentification.StackModel.state line 105
17. theorem OAI.WLIdentification.StackModel.state_ne_one line 109
18. theorem OAI.WLIdentification.StackModel.state_ne_two line 112
19. def OAI.WLIdentification.StackModel.dispatch line 115
20. abbrev OAI.WLIdentification.StackModel.compile line 143

    Source documentation

    A concrete finite local table, using only the three frozen I/O codes and finitely many fixed extra symbols and states.

    noncomputable abbrev compile (P : Program K Λ R) (input : K) : Machine where
    …

    Mentions: OAI.WLIdentification.StackModel.Program, OAI.WLIdentification.Machine

21. theorem OAI.WLIdentification.StackModel.transition_state line 151
22. def OAI.WLIdentification.StackModel.column line 156
23. def OAI.WLIdentification.StackModel.tape line 158
24. theorem OAI.WLIdentification.StackModel.tape_marker line 162
25. theorem OAI.WLIdentification.StackModel.tape_nat line 165
26. def OAI.WLIdentification.StackModel.config line 169
27. theorem OAI.WLIdentification.StackModel.step_config line 179

    Source documentation

    Literal one-transition equation for every interpreter phase.

    theorem step_config (p : Phase K Λ R) (z : ℤ) (S : K → Word) :
        WLIdentification.step (compile P input) (config P input p z S) =
          let t := dispatch P input p (tape input S z)
    …

    Mentions: OAI.WLIdentification.StackModel.Phase, OAI.WLIdentification.Word, OAI.WLIdentification.step, OAI.WLIdentification.StackModel.compile, OAI.WLIdentification.StackModel.config, OAI.WLIdentification.StackModel.dispatch, OAI.WLIdentification.StackModel.tape

28. theorem OAI.WLIdentification.StackModel.step_readonly line 191
29. theorem OAI.WLIdentification.StackModel.step_back_nat line 201
30. theorem OAI.WLIdentification.StackModel.step_back_marker line 208
31. theorem OAI.WLIdentification.StackModel.back_to_marker line 215
32. theorem OAI.WLIdentification.StackModel.back_to_ready line 226
33. theorem OAI.WLIdentification.StackModel.scan_push line 233

    Source documentation

    No random access is used: a full rightward scan costs one transition per cell.

    theorem scan_push (k : K) (label : Λ) (s : R) (b : Bool) (S : K → Word)
        (n : ℕ) (hn : n ≤ (S k).length) :
        (WLIdentification.step (compile P input))^[n]
          (config P input (.push k label s b) 0 S) =
            config P input (.push k label s b) n S := by
    …

    Mentions: OAI.WLIdentification.Word, OAI.WLIdentification.step, OAI.WLIdentification.StackModel.compile, OAI.WLIdentification.StackModel.config

34. theorem OAI.WLIdentification.StackModel.scan_pop line 247
35. theorem OAI.WLIdentification.StackModel.tape_push line 262

    Source documentation

    Erasing the end of a stack, like pushing, only edits one physical cell.

    theorem tape_push (S : K → Word) (k : K) (b : Bool) :
        tape input (Function.update S k (S k ++ [b])) =
          Function.update (tape input S) ((S k).length : ℤ)
            (symbol input (some (Function.update (column S (S k).length) k (some b)))) := by
    …

    Mentions: OAI.WLIdentification.Word, OAI.WLIdentification.StackModel.tape, OAI.WLIdentification.StackModel.symbol, OAI.WLIdentification.StackModel.column