Counting the accepting runs of a Turing machine
Lax366625.CountingRuns · concepts/Lax366625/CountingRuns.lean · lax-366625
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
On a machine instance of the NP core, a walk lays a run out along the positions: a configuration for each position, initial at the least one, related to the next one by a step, or kept unchanged in an accepting state, and accepting at the greatest. A halting walk moreover repeats an accepting configuration once it has reached one, and carries the initial configuration at the elements that are not positions, so that every run reaching an accepting state within the bound has exactly one halting walk. Counting accepting runs is the number of halting walks of a well-formed instance, and for an ill-formed one.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Tactic.FinCases |
| 2 | import Mathlib.Order.PiLex |
| 3 | import Mathlib.Data.Prod.Lex |
| 4 | import Mathlib.Data.Fintype.EquivFin |
| 5 | import Mathlib.ModelTheory.Order |
| 6 | import Mathlib.ModelTheory.Semantics |
| 7 | import Mathlib.ModelTheory.Complexity |
| 8 | import Mathlib.Logic.Equiv.Fin.Basic |
| 9 | import Mathlib.Data.Fintype.Lattice |
| 10 | import Mathlib.Data.Finite.Sigma |
| 11 | import Mathlib.Order.Lattice.Nat |
| 12 | import Mathlib.Data.Set.Card |
| 13 | import Mathlib.Data.Fintype.Pigeonhole |
| 14 | import Mathlib.Dynamics.FixedPoints.Basic |
| 15 | import Mathlib.ModelTheory.Syntax |
| 16 | import Mathlib.Algebra.Order.BigOperators.Group.Finset |
| 17 | import Mathlib.Data.Fintype.Card |
| 18 | import Mathlib.SetTheory.Cardinal.Finite |
| 19 | import Mathlib.Algebra.BigOperators.Finprod |
| 20 | import Mathlib.Data.Set.Finite.Lemmas |
| 21 | import Mathlib.Logic.Equiv.Prod |
| 22 | import Lax366625.MachineNumbers |
| 23 | import Lax904597.Machines |
| 24 | import Lax366625.CountingProblems |
| 25 | import Lax904597.SecondOrder |
| 26 | |
| 27 | /-! |
| 28 | --- |
| 29 | title: Counting the accepting runs of a Turing machine |
| 30 | type: definition |
| 31 | --- |
| 32 | On a machine instance of the NP core, a walk lays a run out along the |
| 33 | positions: a configuration for each position, initial at the least one, |
| 34 | related to the next one by a step, or kept unchanged in an accepting state, |
| 35 | and accepting at the greatest. A halting walk moreover repeats an accepting |
| 36 | configuration once it has reached one, and carries the initial configuration |
| 37 | at the elements that are not positions, so that every run reaching an |
| 38 | accepting state within the bound has exactly one halting walk. Counting |
| 39 | accepting runs is the number of halting walks of a well-formed instance, and |
| 40 | for an ill-formed one. |
| 41 | -/ |
| 42 | |
| 43 | namespace Lax366625.CountingRuns |
| 44 | |
| 45 | open Lax366625.MachineNumbers Lax904597.Machines |
| 46 | |
| 47 | open FirstOrder |
| 48 | |
| 49 | open Language Structure Lax904597.SecondOrder.SOBlock |
| 50 | |
| 51 | namespace TMData |
| 52 | |
| 53 | variable {A : Type} (M : TMData A) |
| 54 | |
| 55 | /-- **A run laid out along the positions**: a configuration for each position, |
| 56 | initial at the lowest, related by a step – or by a stutter in an accepting |
| 57 | state, for a machine that has already accepted – at each immediate successor, |
| 58 | and accepting at the highest. -/ |
| 59 | def IsWalk (conf : A → Config A) : Prop := |
| 60 | (∀ p, MinPos M.Le M.Posn p → M.IsInit (conf p)) ∧ |
| 61 | (∀ p q, SuccPos M.Le M.Posn p q → |
| 62 | M.Step (conf p) (conf q) ∨ (M.Acc (conf p).state ∧ conf q = conf p)) ∧ |
| 63 | ∀ p, MaxPos M.Le M.Posn p → M.Acc (conf p).state |
| 64 | |
| 65 | |
| 66 | /-- **A halting walk**: a walk that repeats an accepting configuration once it |
| 67 | has reached one, and carries the initial configuration at the times that are |
| 68 | not positions. A run from an initial configuration to the first accepting one, |
| 69 | within the budget, has exactly one such layout. -/ |
| 70 | def IsHaltWalk (conf : A → Config A) : Prop := |
| 71 | TMData.IsWalk M conf ∧ |
| 72 | (∀ p q, SuccPos M.Le M.Posn p q → M.Acc (conf p).state → conf q = conf p) ∧ |
| 73 | ∀ t p₀, ¬ M.Posn t → MinPos M.Le M.Posn p₀ → conf t = conf p₀ |
| 74 | |
| 75 | end TMData |
| 76 | |
| 77 | open Lax366625.CountingProblems |
| 78 | |
| 79 | /-- **Counting accepting runs**: the number of halting walks of the machine |
| 80 | described by the instance, an ill-formed instance having none. -/ |
| 81 | noncomputable def SharpNTMAccept : CountingProblem turing := |
| 82 | CountingProblem.ofFun fun A _ => |
| 83 | Nat.card {conf : A → Config A // (tmData A).WellFormed ∧ TMData.IsHaltWalk (tmData A) conf} |
| 84 | |
| 85 | end Lax366625.CountingRuns |
| 86 |
Used by
From Mathlib
Mathlib.Algebra.BigOperators.FinprodMathlib.Algebra.Order.BigOperators.Group.FinsetMathlib.Data.Finite.SigmaMathlib.Data.Fintype.CardMathlib.Data.Fintype.EquivFinMathlib.Data.Fintype.LatticeMathlib.Data.Fintype.PigeonholeMathlib.Data.Prod.LexMathlib.Data.Set.CardMathlib.Data.Set.Finite.LemmasMathlib.Dynamics.FixedPoints.BasicMathlib.Logic.Equiv.Fin.BasicMathlib.Logic.Equiv.ProdMathlib.ModelTheory.ComplexityMathlib.ModelTheory.OrderMathlib.ModelTheory.SemanticsMathlib.ModelTheory.SyntaxMathlib.Order.Lattice.NatMathlib.Order.PiLexMathlib.SetTheory.Cardinal.FiniteMathlib.Tactic.FinCases
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments