OAI/Computability/RationalHitting/Procedures.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.RationalHitting.TimeBound line 10

   Source documentation

   A concrete syntax for nonnegative polynomial bounds. This is only used to bound actual stack transitions, never as an additional machine instruction.

   inductive TimeBound where
   …

2. instance OAI.RationalHitting.TimeBound.(instance at line 18) line 18
3. instance OAI.RationalHitting.TimeBound.(instance at line 19) line 19
4. instance OAI.RationalHitting.TimeBound.(instance at line 20) line 20
5. def OAI.RationalHitting.TimeBound.eval line 22
6. lemma OAI.RationalHitting.TimeBound.eval_const line 28
7. lemma OAI.RationalHitting.TimeBound.eval_variable line 29
8. lemma OAI.RationalHitting.TimeBound.eval_add line 30
9. lemma OAI.RationalHitting.TimeBound.eval_mul line 31
10. lemma OAI.RationalHitting.TimeBound.eval_numeral line 32
11. lemma OAI.RationalHitting.TimeBound.monotone line 34
12. def OAI.RationalHitting.TimeBound.comp line 42

    Source documentation

    Substitution is again a polynomial with nonnegative coefficients.

    def comp : TimeBound → TimeBound → TimeBound
      | .const c, _ => .const c
      | .variable, q => q
      | .add a b, q => a.comp q + b.comp q
      | .mul a b, q => a.comp q * b.comp q

    Mentions: OAI.RationalHitting.TimeBound

13. lemma OAI.RationalHitting.TimeBound.eval_comp line 48
14. theorem OAI.RationalHitting.TimeBound.growth line 54

    Source documentation

    These certificates imply an ordinary fixed positive-coefficient, positive- degree power bound. This prevents any hidden superpolynomial time allowance.

    theorem growth (p : TimeBound) :
        ∃ C k : ℕ, 0<C ∧ 0<k ∧ ∀ n : ℕ, 1≤n → p.eval n≤C*n^k := by
    …

    Mentions: OAI.RationalHitting.TimeBound

15. def OAI.RationalHitting.StackLanguage.single line 92
16. lemma OAI.RationalHitting.StackLanguage.single_self line 94
17. lemma OAI.RationalHitting.StackLanguage.single_other line 96
18. lemma OAI.RationalHitting.StackLanguage.single_nil line 98
19. lemma OAI.RationalHitting.StackLanguage.extend_single line 101
20. lemma OAI.RationalHitting.StackLanguage.Eval.rename_single line 110
21. structure OAI.RationalHitting.StackLanguage.Procedure line 117

    Source documentation

    A quantitative implementation, with completely clean stack input and output. Both execution and result size are polynomially bounded.

    structure Procedure {A B : Type} (ca : A → List Bool) (cb : B → List Bool) (f : A → B) where
    …

22. def OAI.RationalHitting.StackLanguage.Feasible line 133

    Source documentation

    A compositional polynomial-time feasibility predicate.

    def Feasible {A B : Type} (ca : A → List Bool) (cb : B → List Bool) (f : A → B) : Prop :=
    …

23. def OAI.RationalHitting.StackLanguage.move line 138

    Source documentation

    Order-preserving transfer, implemented using two stack reversals.

    def move (a b tmp : K) : Program K := .seq (reverse a tmp) (reverse tmp b)

    Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.reverse

24. lemma OAI.RationalHitting.StackLanguage.eval_move line 140
25. lemma OAI.RationalHitting.StackLanguage.Eval.move_single line 156
26. lemma OAI.RationalHitting.StackLanguage.Eval.runAt line 165

    Source documentation

    Run in an embedded register bank, preserving every register outside it.

    lemma Eval.runAt {p : Program K} {i o : K} {x y : List Bool} {t : ℕ}
        (h : Eval p (single i x) (single o y) t) (f : K → L) (hf : Injective f)
        (s : Store L) (hs : ∀ k, s (f k)=single i x k) :
        Eval (p.rename f) s (update (update s (f i) []) (f o) y) t := by
    …

    Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.single, OAI.RationalHitting.StackLanguage.Store

27. def OAI.RationalHitting.StackLanguage.Procedure.identity line 188

    Source documentation

    Identity has no operation of unbounded cost.

    def identity (ca : A → List Bool) : Procedure ca ca id where
    …

    Mentions: OAI.RationalHitting.StackLanguage.Procedure

28. def OAI.RationalHitting.StackLanguage.Procedure.comp line 201

    Source documentation

    Composition uses disjoint scratch banks and an actual order-preserving stack transfer.

    def comp (q : Procedure cb cc g) (p : Procedure ca cb f) : Procedure ca cc (g ∘ f) where
    …

    Mentions: OAI.RationalHitting.StackLanguage.Procedure

29. def OAI.RationalHitting.StackLanguage.Procedure.recode line 228

    Source documentation

    Reinterpret equal input/output words, with no additional computation.

    def recode {A' B' : Type} (p : Procedure ca cb f) (ca' : A' → List Bool)
        (cb' : B' → List Bool) (f' : A' → B') (e : A' → A)
        (hi : ∀ a, ca (e a)=ca' a) (ho : ∀ a, cb (f (e a))=cb' (f' a)) :
        Procedure ca' cb' f' where
    …

    Mentions: OAI.RationalHitting.StackLanguage.Procedure