OAI/Computability/Superstring/Programs.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Superstring.BitCode.Block.clear line 11

   Source documentation

   Clearing and transfers are explicit bit programs. In particular, reversing or copying a variable-width label is never given unit cost.

   def clear (k : K) : Block K := .loop k (.pop k)

   Mentions: OAI.Superstring.BitCode.Block

2. def OAI.Superstring.BitCode.Block.transfer line 13
3. theorem OAI.Superstring.BitCode.Block.clear_exec line 16
4. theorem OAI.Superstring.BitCode.Block.transfer_exec line 37
5. def OAI.Superstring.BitCode.Block.fanout line 87
6. theorem OAI.Superstring.BitCode.Block.fanout_exec line 91
7. def OAI.Superstring.BitCode.Block.copy line 145
8. theorem OAI.Superstring.BitCode.Block.copy_exec line 148
9. def OAI.Superstring.BitCode.Block.rename line 184

   Source documentation

   Change the names of registers; loops and instructions are unchanged.

   def rename (f : K → L) : Block K → Block L
     | .push k b => .push (f k) b
     | .pop k => .pop (f k)
     | .skip => .skip
     | .branch k a b c => .branch (f k) (a.rename f) (b.rename f) (c.rename f)
     | .seq a b => .seq (a.rename f) (b.rename f)
     | .loop k a => .loop (f k) (a.rename f)
   
   /-- A syntax tree mentions only finitely many registers. -/

   Mentions: OAI.Superstring.BitCode.Block

10. def OAI.Superstring.BitCode.Block.support line 193

    Source documentation

    A syntax tree mentions only finitely many registers.

    def support [DecidableEq K] : Block K → Finset K
      | .push k _ | .pop k => {k}
      | .skip => ∅
      | .branch k a b c => insert k (a.support ∪ b.support ∪ c.support)
      | .seq a b => a.support ∪ b.support
      | .loop k a => insert k a.support

    Mentions: OAI.Superstring.BitCode.Block

11. theorem OAI.Superstring.BitCode.Block.update_comp line 200
12. theorem OAI.Superstring.BitCode.Block.Exec.pullback line 211

    Source documentation

    Restrict an execution to any injective family of registers containing all registers in its syntax. The rest of an infinite ambient store is irrelevant.

    theorem Exec.pullback [DecidableEq K] [DecidableEq L] (f : K → L) (g : L → K)
        (hg : Function.Injective g) {b : Block K} {s t : Store K} {n : ℕ}
        (h : b.Exec s t n) (hf : ∀ k ∈ b.support, g (f k) = k) :
        (b.rename f).Exec (s ∘ g) (t ∘ g) n := by
    …

    Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Store, OAI.Superstring.BitCode.Block.Exec

13. inductive OAI.Superstring.BitCode.Program line 263

    Source documentation

    A bounded-loop register language. Every repeat uses the ORIGINAL input length, not a mutable register. Nesting is static in the finite program. Copy is assignment, not concatenation; the only operation increasing maximum word length is a one-bit push. This gives uniform polynomial bounds for every program.

    inductive Program (K : Type)
      | push (k : K) (b : Bool)
      | pop (k : K)
      | clear (k : K)
      | copy (source target : K)
      | skip
      | branch (k : K) (empty low high : Program K)
      | seq (first second : Program K)
      | repeat (body : Program K)
    
    namespace Program
    …

14. def OAI.Superstring.BitCode.Program.run line 277
15. def OAI.Superstring.BitCode.Program.work line 290
16. def OAI.Superstring.BitCode.Program.polynomial line 296
17. theorem OAI.Superstring.BitCode.Program.eval_polynomial line 303
18. theorem OAI.Superstring.BitCode.Program.work_pos line 307
19. def OAI.Superstring.BitCode.Program.Bounded line 311

    Source documentation

    All stack lengths are bounded by a common number.

    def Bounded (s : Store K) (M : ℕ) : Prop := ∀ k, (s k).length ≤ M
    …

    Mentions: OAI.Superstring.BitCode.Store

20. theorem OAI.Superstring.BitCode.Program.Bounded.mono line 314
21. theorem OAI.Superstring.BitCode.Program.Bounded.update line 317
22. theorem OAI.Superstring.BitCode.Program.iterate_bounded line 325
23. theorem OAI.Superstring.BitCode.Program.run_bounded line 336
24. def OAI.Superstring.BitCode.Program.depth line 367

    Source documentation

    Only the maximum loop-nesting depth determines the number of counters.

    def depth : Program K → ℕ
      | .push _ _ | .pop _ | .clear _ | .copy _ _ | .skip => 0
      | .branch _ a b c => max a.depth (max b.depth c.depth)
      | .seq a b => max a.depth b.depth
      | .repeat a => a.depth + 1

    Mentions: OAI.Superstring.BitCode.Program

25. def OAI.Superstring.BitCode.Program.compile line 374
26. def OAI.Superstring.BitCode.Program.Clean line 386

    Source documentation

    Unused higher counters may contain arbitrary data, for compositional use.

    def Clean (d : ℕ) (z : Store ℕ) : Prop := z 1 = [] ∧ ∀ j < d, z (j + 2) = []

    Mentions: OAI.Superstring.BitCode.Store

27. theorem OAI.Superstring.BitCode.Program.Clean.mono line 388
28. theorem OAI.Superstring.BitCode.Program.Clean.update_above line 391
29. theorem OAI.Superstring.BitCode.Program.sum_update_left line 399
30. theorem OAI.Superstring.BitCode.Program.sum_update_right line 406