OAI/Computability/RationalHitting/ProcedureControl.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RationalHitting.StackLanguage.Procedure.toPort line 12

   Source documentation

   Give a procedure a single external input/output port. The two transfers are real stack programs; scratch registers remain clean.

   def toPort (p : Procedure ca cb f) : Procedure ca cb f where
   …

   Mentions: OAI.RationalHitting.StackLanguage.Procedure

2. def OAI.RationalHitting.StackLanguage.splitPair line 37
3. lemma OAI.RationalHitting.StackLanguage.eval_splitPair line 40
4. lemma OAI.RationalHitting.StackLanguage.extend_both line 60
5. def OAI.RationalHitting.StackLanguage.Procedure.fromBinary line 72

   Source documentation

   Package an independently proved two-input clean register routine as a serialized procedure. Its polynomial bound is not an operation oracle: the actual Eval proof is required.

   def fromBinary (p : Program K) (i j o : K) (hij : i≠j) (bnd : TimeBound)
       (hp : ∀ a b, ∃ t ≤ bnd.eval ((ca a).length+(cb b).length+1),
         Eval p (both i j (ca a) (cb b)) (single o (cc (f (a,b)))) t)
       (hs : ∀ a b, (cc (f (a,b))).length ≤ bnd.eval ((ca a).length+(cb b).length+1)) :
       Procedure (pairCode ca cb) cc f where
   …

   Mentions: OAI.RationalHitting.StackLanguage.Program, OAI.RationalHitting.TimeBound, OAI.RationalHitting.StackLanguage.Eval, OAI.RationalHitting.StackLanguage.both, OAI.RationalHitting.StackLanguage.single, OAI.RationalHitting.StackLanguage.Procedure, OAI.RationalHitting.StackLanguage.pairCode

6. def OAI.RationalHitting.StackLanguage.boolCode line 109
7. lemma OAI.RationalHitting.StackLanguage.boolCode_length line 110
8. def OAI.RationalHitting.StackLanguage.Procedure.rename line 116
9. def OAI.RationalHitting.StackLanguage.Procedure.branch line 131

   Source documentation

   Deterministic Boolean branching on a serialized pair. Only the selected finite subprogram runs; the tag is physically consumed.

   def branch (p : Procedure ca cb f) (q : Procedure ca cb g) :
       Procedure (pairCode boolCode ca) cb (fun a => if a.1 then f a.2 else g a.2) := by
   …

   Mentions: OAI.RationalHitting.StackLanguage.Procedure, OAI.RationalHitting.StackLanguage.pairCode, OAI.RationalHitting.StackLanguage.boolCode

10. def OAI.RationalHitting.StackLanguage.unaryCode line 209

    Source documentation

    Unary loop count. These symbols are explicitly popped by the loop body.

    def unaryCode (n : ℕ) : List Bool := List.replicate n true

11. lemma OAI.RationalHitting.StackLanguage.unaryCode_length line 210
12. lemma OAI.RationalHitting.StackLanguage.unaryCode_zero line 211
13. lemma OAI.RationalHitting.StackLanguage.unaryCode_succ line 212
14. def OAI.RationalHitting.StackLanguage.Procedure.iterateProgram line 217
15. lemma OAI.RationalHitting.StackLanguage.Procedure.eval_iterateProgram line 220
16. def OAI.RationalHitting.StackLanguage.Procedure.iterate line 257

    Source documentation

    Bounded iteration is compiled to a real finite loop. The semantic size invariant is a proof obligation, not a loop oracle or added main hypothesis.

    def iterate (p : Procedure ca ca f) (Q : TimeBound)
        (hQ : ∀ (n : ℕ) (a : A) (i : ℕ), i≤n →
          (ca (f^[i] a)).length≤Q.eval ((pairCode unaryCode ca (n,a)).length+1)) :
        Procedure (pairCode unaryCode ca) ca (fun a => f^[a.1] a.2) := by
    …

    Mentions: OAI.RationalHitting.StackLanguage.Procedure, OAI.RationalHitting.TimeBound, OAI.RationalHitting.StackLanguage.pairCode, OAI.RationalHitting.StackLanguage.unaryCode