Counting on the configuration graph
Lax733996.ConfigurationCounting · concepts/Lax733996/ConfigurationCounting.lean · lax-733996
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
For every terminal accepting configuration, certify that it cannot be reached from the initial configuration. The implementation must generate the witnesses sequentially; this predicate alone makes no space claim.
Concept map
In the paper
- page 2 of this submission's paper
Lean source view on GitHub
| 1 | import Lax733996.ConfigurationGraph |
| 2 | import Lax733996.Counting |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Counting on the configuration graph |
| 7 | type: definition |
| 8 | --- |
| 9 | For every terminal accepting configuration, certify that it cannot be |
| 10 | reached from the initial configuration. The implementation must generate |
| 11 | the witnesses sequentially; this predicate alone makes no space claim. |
| 12 | -/ |
| 13 | |
| 14 | namespace Lax733996.ConfigurationCounting |
| 15 | |
| 16 | open Lax434930.PolynomialTime Lax434930.SpaceMachines |
| 17 | open Lax733996.BoundedConfigurations Lax733996.ConfigurationGraph Counting |
| 18 | |
| 19 | def RejectsByCounting (M : Machine) (w : Word) (s : ℕ) : Prop := |
| 20 | ∀ a b : Config M w.length s, expand a = M.initial → |
| 21 | M.Terminal w (expand b) → M.accept b.state = true → |
| 22 | NonreachCertificate (graph M w s) (numbering M w.length s a) (numbering M w.length s b) |
| 23 | |
| 24 | end Lax733996.ConfigurationCounting |
| 25 |
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments