Counting on the configuration graph
Lax362205.ConfigurationCounting · concepts/Lax362205/ConfigurationCounting.lean · lax-362205
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 Lax362205.ConfigurationGraph |
| 2 | import Lax362205.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 Lax362205.ConfigurationCounting |
| 15 | |
| 16 | open Lax434930.PolynomialTime Lax434930.SpaceMachines |
| 17 | open Lax362205.BoundedConfigurations Lax362205.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 Lax362205.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