6 Improving discovery without changing its meaning
On this page · Permalink · Source line 738
Removing redundant work is an improvement only when the removed work could not change the justified result.
On this page · Permalink · Source line 739
Let \(\mathcal G=(p_0,\ldots,p_{N-1})\) be a finite ordered grammar of pure, total candidate programs. Let \(D\) be a finite context set and \(t:D\to Y\) a fixed labeling. A teacher either accepts a candidate that agrees everywhere or returns a context where it disagrees. The teacher's work is part of the development account.
6.1 Finite counterexample-guided acquisition
On this page · Permalink · Source line 742
The learner retains every returned counterexample. It proposes the earliest candidate consistent with all retained examples, or reports exhaustion of the grammar when none remains.
Proposition 6.1: What finite counterexamples establish
The learner never submits the same rejected candidate twice. Within at most \(N\) teacher calls, it returns the earliest globally correct candidate in the declared grammar or exhausts that grammar. A timeout before this process finishes is neither acceptance nor exhaustion.
Read proof · Recorded Lean scope · Permalink · Source line 745
Proof
Each counterexample refutes the submitted program and remains a constraint forever. That program cannot be submitted again. A globally correct candidate never violates a truthful counterexample. With only \(N\) candidates, either an accepted one is found or all are ruled out. If the accepted candidate were preceded by a globally correct candidate, that earlier candidate would still be consistent and would have been selected first. This proves the ordering claim. Interruption changes none of these logical implications and cannot supply a completed search result.
Source relationship. [SII], Theorem 15.1. This is finite exact synthesis in a supplied language, not a statistical generalization guarantee.
Agreement on \(D\) is not validity outside \(D\). That distinction is especially important when a candidate is used to prune future searches. A wrong proposal can be rejected by a final checker. A wrong pruning rule may remove the only candidate the checker ought to see.
6.2 A learned search representation can preserve the exact investigation
On this page · Permalink · Source line 755
Suppose a deterministic normalizing map \(n\) is sound in the following direction:
The map need not detect every semantic equivalence or produce a mathematically canonical normal form. Each successful contextual rewrite must be justified under the actual pure, total semantics. Keep the earliest original AST for every attained normal form, not a replacement AST with an uncharged new interpreter.
Theorem 6.2: Ordered semantic compression preserves the teacher trace
Assume all counterexamples are retained, candidate and example orders are fixed, and the teacher is deterministic and extensional, returning the first disagreement in a fixed context order. Searching only the earliest representatives yields exactly the same submitted ASTs, counterexamples, and final acceptance or grammar exhaustion as the original learner. With the same AST interpreter it uses no more retained-example evaluations. Preparation, dispatch, and stored-index costs are separate.
Read proof · Recorded Lean scope · Permalink · Source line 762
Proof
A removed expression has an earlier representative with the same values on every admitted context. If that representative was accepted, the original search ended before reaching the removed expression. Otherwise an already retained example refuted the representative, either during a consistency test or from the teacher. Persistence of examples means that the same example refutes the later equivalent expression. The original learner therefore never submits that removed expression to the teacher.
Deleting only those unsuccessful consistency tests preserves the next submitted AST. A deterministic teacher then returns the same counterexample or acceptance. Induction over submissions proves equality of the complete trace, including exhaustion. Every deleted evaluation has nonnegative cost in the named evaluation count. The argument makes no claim that constructing or consulting the representative index is free.
Source relationship. [SII], Theorems 21.1 and 21.2. Sound equational replacement is the premise; empirical agreement on a few probe points does not supply it.
Counterexample 6.3: A probe-equivalent equation is not a general identity
The expressions \(\max(x,1)\) and \(x\) agree for probes \(x\in\{1,2,3\}\). At zero they differ. Grouping them by those probe values alone can remove a needed candidate. The identity \(\max(x,0)=x\) is valid over nonnegative integers, but not over all integers. The semantic domain is part of the equation's certificate.
The retained object may therefore improve later search without containing its answers. This is the precise process-level role of a checked equation library. The grammar, primitive semantics, teacher, and proof rules can still be supplied. Their presence must remain visible instead of being redescribed as discoveries.
6.3 A reusable rule for stopping an unpromising read
On this page · Permalink · Source line 778
A diagnostic compiler inspects a binary query on \(m\) immutable cases. In the prefix already read, \(a\) cases give zero and \(b\) give one. Each child is allowed at most \(C\) cases because the remaining binary depth has that leaf capacity. Assume integers
Proposition 6.4: A sound prefix exclusion
The unread reports can be completed with both final branch counts at most \(C\) if and only if \(\max(a,b)\le C\). A scan may therefore stop when one count first exceeds \(C\). In a fixed ordered depth-first compiler with identical scope, terminal, and fallback rules, replacing full root scans by this early rejection preserves the first returned tree or the completed depth-bounded failure result.
Read proof · Recorded Lean scope · Permalink · Source line 784
Proof
Counts only increase, so an overfull child cannot be rescued. Otherwise the two remaining capacities are \(C-a\) and \(C-b\), both nonnegative. Their sum \(2C-a-b\) is at least the number \(m-a-b\) of unread rows. Distributing the unread cases between those capacities gives a feasible completion.
Every root rejected early would also be rejected after its full scan. A root not rejected early is read completely and produces the same ordered child supports. Induction on the finite remaining depth therefore yields identical recursive searches, backtracking, and first completion. The same failure condition invokes the same fallback. The skipped rows are only suffixes whose contents could not change rejection. A resource timeout is excluded from the completed-failure claim.
Source relationship. [SII], Proposition 16.1 and Theorem 16.3. The conclusion concerns capacity feasibility, not the existence of a completing query in the installed language.
For \(C=4\), a fifth zero already closes a root. Reading more rows cannot reduce that branch. By contrast, a four-versus-four split merely survives this necessary test. If no remaining query distinguishes either child, the root still fails.
Counterexample 6.5: A changed repair defeats the old premise
Four cases previously required four different repairs. Admit one new repair successful in all four. No identifying query is now needed. The old singleton-leaf lower bound and its pruning interpretation are not applicable. The correct response is to recheck the repair scope, not to preserve an obsolete optimization because it once passed.
What is now available
On this page · Permalink · Source line 800
The resulting method is semantically justified only under its premises. We must still determine whether it saves total resources, and which proof records remain usable when a later revision changes those premises. Both questions belong to the next chapter rather than being inferred from a successful synthesis.