Complexity theory using combinators based on fold and some other prim… - #183
Draft
crei wants to merge 8 commits into
Draft
Complexity theory using combinators based on fold and some other prim…#183crei wants to merge 8 commits into
crei wants to merge 8 commits into
Conversation
Bounds.depthRec certifies functions defined by recursion whose depth
depends on the input. This is the shape behind Savitch's theorem, and it
is genuinely new: fold and while reuse tapes across iterations, so their
space is the max over iterations, whereas a recursive call must keep its
own frame live while the call beneath it runs. Space is therefore
additive down the depth and max across the breadth.
It adds no `sorry` — the primitive count stays at 18. The recursion is
compiled to a while loop over an explicit stack, which is the
algorithmic content of Savitch's theorem, so it gets proved rather than
assumed. Four lemmas carry it:
* complete the stack machine implements the recursion
* complete_le/steps_le a step-count measure bounds the halting time (N)
* stack_length_le strictly decreasing levels bound the stack (D)
* frame_inv a schema-level invariant transfers to every
reachable state (F, B)
The last two exist because the first draft stated F and B over
mstep^[j], which would have forced every caller to reason about the
machine; and because Nat.find alone gives no bound, leaving N
unprovable in practice. Both gaps only showed up on instantiation.
Algorithms are presented as a RecSchema: a resumable state machine that
either returns or asks one sub-question. Enumeration by counting and
several calls per step are then just states, so nothing of the size of
the search space is ever materialised.
Examples/Reach.lean instantiates it with the double recursion behind
Savitch's theorem and proves heval — the schema computes reach — by
induction on the level, with no machine reasoning. The resource bounds
(D, F, B, N and the field certificates) are not done yet.
Also adds, both free of new assumptions:
* DataEncode.ofInjection — encode a structure through an injection
* Bounds.recode — a certificate for any encoding-preserving map,
derived from Bounds.id, since DataComputableInTimeAndSpace mentions
only encodings. Together these make `structure`s usable: field
accessors become ordinary fst/snd chains.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
All five RecSchema fields now have Bounds certificates, which is what
the resumable-strategy shape was for: each field is first-order, so each
is certified separately with the ordinary combinators.
`answer` is synthesised by the `bounds` tactic. The tactic fails on
`isDone` — it tries `Function.uncurry List.isEmpty` when a disjunction
has an `isEmpty` application as an argument — so that one is built by
hand; worth a look when the tactic is next touched.
Two things worth noting for later readers:
* Field access goes through `Activation.toProd`, certified by
`Bounds.recode`, so accessors are ordinary fst/snd chains. The
chains are positional and easy to miscount; `mkActivation` wraps the
seven-fold fan-out so the assembling direction is named rather than
positional.
* `enter` is the only place the graph is consulted, so certificates
for vertex equality and for the edge relation are this example's
only hypotheses. They depend on how the graph is represented, which
`reach` deliberately leaves open.
Still to do: the D, F, B and N obligations and the final assembly into
Bounds.depthRec.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`level_enter_le` discharges depthRec's D: the opening level is bounded by the input size. `FrameOK` is the schema-level invariant that `frame_inv` transfers to every reachable machine state — the level only shrinks, the midpoint list is always a suffix of `verts`, and both endpoints come from the original question or from `verts`. It is proved closed under entering a sub-question and under resumption, which is all `frame_inv` asks for; no reasoning about `mstep^[j]` appears. Stating `enter`'s fields as three separate equations (enter_level, enter_remaining, enter_endpoints) rather than casing on the level test inside each proof is what made these go through cleanly. Still to do: turning FrameOK into the numeric F, the step measure for N, and the final assembly. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
…itives.