SynthesisBudget.lean

1 import MachineTheory.SynthesisTrace
2 
3 /-!
4 # Explicit suspension is not acceptance or exhaustion
5 
6 Fuel bounds candidate inspections, not CPU instructions, teacher calls, or the
7 cost of a candidate evaluation. Suspensions retain the pending ordered grammar,
8 all counterexamples, the actual transcript and accumulated comparison counters.
9 Resumption has the same result as an uninterrupted scan.
10 -/
11 
12 namespace Komorebi.MachineTheory.Synthesis
13 
14 universe u v w
15 variable {P : Type u} {D : Type v} {Y : Type w} [DecidableEq Y]
16 
17 structure Suspension (P : Type u) (D : Type v) where
18   pending : List P
19   retained : List D
20   transcript : List (P × Option D)
21   comparisons : Nat
22   visits : Nat
23   deriving Repr, DecidableEq
24 
25 inductive Progress (P : Type u) (D : Type v) where
26   | complete : Result P D → Progress P D
27   | suspended : Suspension P D → Progress P D
28   deriving Repr, DecidableEq
29 
30 def prependWork (cost : Nat) : Progress P D → Progress P D
31   | .complete r => .complete {r with comparisons := cost + r.comparisons, visits := 1 + r.visits}
32   | .suspended s => .suspended {s with comparisons := cost + s.comparisons, visits := 1 + s.visits}
33 
34 def prependCall (p : P) (x : D) (cost : Nat) : Progress P D → Progress P D
35   | .complete r => .complete {r with transcript := (p, some x) :: r.transcript, comparisons := cost + r.comparisons, visits := 1 + r.visits}
36   | .suspended s => .suspended {s with transcript := (p, some x) :: s.transcript, comparisons := cost + s.comparisons, visits := 1 + s.visits}
37 
38 /-- No teacher is consulted when the candidate-inspection allowance is exhausted. -/
39 def boundedScan (T : Task P D Y) : Nat → List P → List D → Progress P D
40   | _, [], E => .complete ⟨none, [], E, 0, 0⟩
41   | 0, G, E => .suspended ⟨G, E, [], 0, 0⟩
42   | n + 1, p :: ps, E =>
43     let c := inspect T p E
44     match c.1 with
45     | some _ => prependWork c.2 (boundedScan T n ps E)
46     | none =>
47       match teacher T p with
48       | none => .complete ⟨some p, [(p, none)], E, c.2, 1⟩
49       | some x => prependCall p x c.2 (boundedScan T n ps (x :: E))
50 
51 /-- Finish the stored pending computation, preserving the emitted prefix. -/
52 def resume (T : Task P D Y) : Progress P D → Result P D
53   | .complete r => r
54   | .suspended s =>
55     let r := scan T s.pending s.retained
56     ⟨r.answer, s.transcript ++ r.transcript, r.retained,
57       s.comparisons + r.comparisons, s.visits + r.visits⟩
58 
59 theorem resume_prependWork (T : Task P D Y) (c : Nat) (q : Progress P D) :
60     resume T (prependWork c q) =
61       {resume T q with comparisons := c + (resume T q).comparisons, visits := 1 + (resume T q).visits} := by
62   cases q <;> simp [resume, prependWork, Nat.add_assoc]
63 
64 theorem resume_prependCall (T : Task P D Y) (p : P) (x : D) (c : Nat) (q : Progress P D) :
65     resume T (prependCall p x c q) =
66       {resume T q with transcript := (p, some x) :: (resume T q).transcript, comparisons := c + (resume T q).comparisons, visits := 1 + (resume T q).visits} := by
67   cases q <;> simp [resume, prependCall, Nat.add_assoc]
68 
69 /-- Completed calls, counterexamples, answer and measured work all survive suspension. -/
70 theorem resume_bounded (T : Task P D Y) (n : Nat) (G : List P) (E : List D) :
71     resume T (boundedScan T n G E) = scan T G E := by
72   induction n generalizing G E with
73   | zero =>
74     cases G <;> simp [boundedScan, resume, scan]
75   | succ n ih =>
76     cases G with
77     | nil => rfl
78     | cons p ps =>
79       cases hc : (inspect T p E).1 with
80       | some x => simp [boundedScan, scan, hc, resume_prependWork, ih]
81       | none =>
82         cases ht : teacher T p with
83         | none => simp [boundedScan, scan, hc, ht, resume]
84         | some x => simp [boundedScan, scan, hc, ht, resume_prependCall, ih]
85 
86 /-- A completion returned within a partial allowance is still the full exact result. -/
87 theorem bounded_completion_sound (T : Task P D Y) {n : Nat} {G : List P} {E : List D}
88     {r : Result P D} (h : boundedScan T n G E = .complete r) : r = scan T G E := by
89   have he := resume_bounded T n G E
90   rw [h] at he
91   exact he
92 
93 /-- There is no assumption that one inspection has constant physical execution cost. -/
94 theorem enough_inspections (T : Task P D Y) (n : Nat) (G : List P) (E : List D)
95     (h : G.length ≤ n) : boundedScan T n G E = .complete (scan T G E) := by
96   induction n generalizing G E with
97   | zero =>
98     have hg : G = [] := by simpa using h
99     subst G
100     rfl
101   | succ n ih =>
102     cases G with
103     | nil => rfl
104     | cons p ps =>
105       have htail : ps.length ≤ n := by simpa using h
106       cases hc : (inspect T p E).1 with
107       | some x => simp [boundedScan, scan, hc, ih ps E htail, prependWork]
108       | none =>
109         cases ht : teacher T p with
110         | none => simp [boundedScan, scan, hc, ht]
111         | some x => simp [boundedScan, scan, hc, ht, ih ps (x :: E) htail, prependCall]
112 
113 end Komorebi.MachineTheory.Synthesis

Back to source controls