#P by counting the accepting runs of a Turing machine
Lax366625.CountingRunsComplete · concepts/Lax366625/CountingRunsComplete.lean · lax-366625
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Counting accepting runs is parsimoniously #P-complete, and a counting problem is in #P if and only if it reduces to it by an ordered parsimonious reduction: #P is the class of the numbers of accepting runs of nondeterministic polynomial-time machines. Membership counts the tableaux of the runs, which the runs determine; hardness builds the machine of the Cook–Levin theorem, which guesses only at the variables of a formula, so that its accepting runs are the models.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax904597.Problems |
| 2 | import Lax904597.Interpretations |
| 3 | import Lax904597.Relativized |
| 4 | import Lax904597.SecondOrder |
| 5 | import Lax904597.Classes |
| 6 | import Lax904597.Sat |
| 7 | import Lax904597.Machines |
| 8 | import Lax535992.HornSat |
| 9 | import Lax535992.CircuitValue |
| 10 | import Lax535992.DeterministicMachines |
| 11 | import Lax535992.ClassPTIME |
| 12 | import Lax366625.CountingProblems |
| 13 | import Lax366625.CountingClasses |
| 14 | import Lax366625.WitnessCounting |
| 15 | import Lax366625.SecondOrderCounting |
| 16 | import Lax366625.QuantitativeLogic |
| 17 | import Lax366625.CountingSat |
| 18 | import Lax366625.MachineNumbers |
| 19 | import Lax366625.CountingRuns |
| 20 | import Lax366625.NumberedCircuits |
| 21 | import Lax366625.HornNumbers |
| 22 | |
| 23 | /-! |
| 24 | --- |
| 25 | title: #P by counting the accepting runs of a Turing machine |
| 26 | type: theorem |
| 27 | --- |
| 28 | Counting accepting runs is parsimoniously #P-complete, and a counting problem |
| 29 | is in #P if and only if it reduces to it by an ordered parsimonious |
| 30 | reduction: #P is the class of the numbers of accepting runs of |
| 31 | nondeterministic polynomial-time machines. Membership counts the tableaux of |
| 32 | the runs, which the runs determine; hardness builds the machine of the |
| 33 | Cook–Levin theorem, which guesses only at the variables of a formula, so |
| 34 | that its accepting runs are the models. |
| 35 | -/ |
| 36 | |
| 37 | namespace Lax366625.CountingRunsComplete |
| 38 | |
| 39 | open FirstOrder FirstOrder.Language |
| 40 | open Lax904597.Problems Lax904597.Interpretations Lax904597.Relativized Lax904597.SecondOrder |
| 41 | open Lax904597.Classes Lax904597.Sat Lax904597.Machines |
| 42 | open Lax535992.ClassPTIME |
| 43 | open Lax366625.CountingProblems Lax366625.CountingClasses Lax366625.WitnessCounting |
| 44 | open Lax366625.SecondOrderCounting |
| 45 | open Lax366625.QuantitativeLogic Lax366625.CountingSat Lax366625.MachineNumbers |
| 46 | open Lax366625.CountingRuns |
| 47 | open Lax366625.NumberedCircuits Lax366625.HornNumbers |
| 48 | |
| 49 | /-- Counting accepting runs is parsimoniously #P-complete. -/ |
| 50 | axiom sharpNtmAccept_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpNTMAccept |
| 51 | |
| 52 | /-- #P is reducibility to counting accepting runs. -/ |
| 53 | axiom mem_sharpP_iff_le_sharpNtmAccept : |
| 54 | ∀ {L : Language.{0, 0}} [L.IsRelational] (C : CountingProblem L), |
| 55 | SharpP.Mem C ↔ Nonempty (OrderedParsimoniousReduction C SharpNTMAccept) |
| 56 | |
| 57 | end Lax366625.CountingRunsComplete |
| 58 |
Builds on
Lax366625.CountingClassesLax366625.CountingProblemsLax366625.CountingRunsLax366625.CountingSatLax366625.HornNumbersLax366625.MachineNumbersLax366625.NumberedCircuitsLax366625.QuantitativeLogicLax366625.SecondOrderCountingLax366625.WitnessCountingLax535992.CircuitValueLax535992.ClassPTIMELax535992.DeterministicMachinesLax535992.HornSatLax904597.ClassesLax904597.InterpretationsLax904597.MachinesLax904597.ProblemsLax904597.RelativizedLax904597.SatLax904597.SecondOrder
Used by
none
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments