Counting the accepting runs of a machine

The counting version of DescriptiveComplexity.NTMAccept, on the same vocabulary: the number of accepting runs of the machine an instance describes – the quantity #P was introduced to measure (Valiant 1979).

A run is counted through its layout along the positions, as in DescriptiveComplexity.TMData.IsWalk, with two more requirements that make the layout of a run unique (DescriptiveComplexity.TMData.IsHaltWalk):

• an accepting configuration is repeated, never left: a run is counted up to the first accepting configuration it reaches, as for a machine whose accepting states are halting;
• times that are not positions carry the initial configuration: the clock of a run is the positions, and a walk says something only there.

DescriptiveComplexity.SharpNTMAccept is the bundled counting problem; its support is machine acceptance (DescriptiveComplexity.sharpNtmAccept_support_iff), and it belongs to #P (DescriptiveComplexity.sharpNtmAccept_mem_sharpP): the tableau of Fagin's argument is functionally determined by the run, so its guesses are the runs, bijectively (DescriptiveComplexity.haltWalkEquiv). With the counting Cook–Levin theorem this gives its textbook form, DescriptiveComplexity.sharpNtmAccept_reduces_to_sharpSat: counting the accepting runs of a machine reduces parsimoniously to counting the models of a CNF formula.

The converse reduction is in DescriptiveComplexity.Problems.Machine.CountingHardness, which makes this problem parsimoniously #P-complete and #P the class of the problems reducing to it.

def DescriptiveComplexity.TMData.IsHaltWalk {A : Type} (M : TMData A) (conf : A → Config A) : Prop

A halting walk: a walk that repeats an accepting configuration once it has reached one, and carries the initial configuration at the times that are not positions. A run from an initial configuration to the first accepting one, within the budget, has exactly one such layout.

Equations

• One or more equations did not get rendered due to their size.

Halting walks of agreeing machines

theorem DescriptiveComplexity.Config.map_symm_map {A B : Type} (u : B ≃ A) (c : Config B) : map u.symm (map u c) = c

The relational form of a halting walk

def DescriptiveComplexity.TMData.RelSame {A : Type} (Q H : A → A → Prop) (T : A → A → A → Prop) (t t' : A) : Prop

The three relations describe the same configuration at t' as at t.

Equations

• DescriptiveComplexity.TMData.RelSame Q H T t t' = ((∀ (q : A), Q t' q ↔ Q t q) ∧ (∀ (p : A), H t' p ↔ H t p) ∧ ∀ (p a : A), T t' p a ↔ T t p a)

structure DescriptiveComplexity.TMData.RelHaltWalk {A : Type} (M : TMData A) (Q H : A → A → Prop) (T : A → A → A → Prop) : Prop

A halting walk, guessed as three relations.

• walk : M.RelWalk Q H T

  The relations are a walk.

• halt (t t' : A) : SuccPos M.Le M.Posn t t' → (∀ (q : A), Q t q → M.Acc q) → RelSame Q H T t t'

  An accepting configuration is repeated.

• off (t t₀ : A) : ¬M.Posn t → MinPos M.Le M.Posn t₀ → RelSame Q H T t₀ t

  Times that are not positions carry the initial configuration.

theorem DescriptiveComplexity.TMData.RelHaltWalk.isHaltWalk {A : Type} {M : TMData A} {Q H : A → A → Prop} {T : A → A → A → Prop} (h : M.RelHaltWalk Q H T) : M.IsHaltWalk ⋯.conf

A relational halting walk is a halting walk, through the configurations it describes.

theorem DescriptiveComplexity.TMData.IsHaltWalk.relHaltWalk {A : Type} {M : TMData A} {conf : A → Config A} (h : M.IsHaltWalk conf) : M.RelHaltWalk (fun (t q : A) => q = (conf t).state) (fun (t p : A) => p = (conf t).head) fun (t p a : A) => a = (conf t).tape p

A halting walk is a relational halting walk, through the graphs of its configurations.

The kernel

noncomputable def DescriptiveComplexity.tqAccAtF {α : Type} (t : α) : tqSOLang.Formula α

The state at t is accepting, as a formula.

Equations

• DescriptiveComplexity.tqAccAtF t = FirstOrder.Language.Formula.iAlls (Fin 1) ((DescriptiveComplexity.tqStateF (Sum.inl t) (Sum.inr 0)).imp (DescriptiveComplexity.tqAccF (Sum.inr 0)))

noncomputable def DescriptiveComplexity.tqSameF {α : Type} (t t' : α) : tqSOLang.Formula α

The configuration at t' is the one at t, as a formula.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.tqHaltClause : tqSOLang.Sentence

An accepting configuration is repeated.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.tqOffClause : tqSOLang.Sentence

Times that are not positions carry the initial configuration.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.sharpTqKernel : tqSOLang.Sentence

The kernel of the counting problem: the kernel of machine acceptance, and the two clauses that make the tableau of a run unique.

Equations

• DescriptiveComplexity.sharpTqKernel = DescriptiveComplexity.tqKernel ⊓ (DescriptiveComplexity.tqHaltClause ⊓ DescriptiveComplexity.tqOffClause)

Runs are the witnesses of the kernel

def DescriptiveComplexity.confAssign {A : Type} (conf : A → Config A) : tmGuessBlock.Assignment A

The guess of the block describing a family of configurations: the graphs of its state, head and tape.

Equations

• DescriptiveComplexity.confAssign conf DescriptiveComplexity.TMIdx.state = fun (w : Fin 2 → A) => w 1 = (conf (w 0)).state
• DescriptiveComplexity.confAssign conf DescriptiveComplexity.TMIdx.head = fun (w : Fin 2 → A) => w 1 = (conf (w 0)).head
• DescriptiveComplexity.confAssign conf DescriptiveComplexity.TMIdx.tape = fun (w : Fin 3 → A) => w 2 = (conf (w 0)).tape (w 1)

theorem DescriptiveComplexity.card_haltWalk_eq_witnessCount (A : Type) [FirstOrder.Language.turing.Structure A] : Nat.card { conf : A → Config A // (tmData A).WellFormed ∧ (tmData A).IsHaltWalk conf } = witnessCount tmGuessBlock sharpTqKernel A

The number of halting walks is the number of witnesses of the kernel.

The counting problem

noncomputable def DescriptiveComplexity.SharpNTMAccept : CountingProblem FirstOrder.Language.turing

Counting accepting runs: the number of runs of the machine described by the instance that reach an accepting state within as many steps as there are positions, each counted up to the first accepting configuration it reaches, through its layout along the positions (DescriptiveComplexity.TMData.IsHaltWalk). As for DescriptiveComplexity.NTMAccept, the well-formedness promises are folded in: an ill-formed instance has no run.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.sharpNtmAccept_support_iff (A : Type) [FirstOrder.Language.turing.Structure A] [Finite A] : SharpNTMAccept.support.Holds A ↔ NTMAccept.Holds A

The support of counting accepting runs is machine acceptance.

theorem DescriptiveComplexity.sharpNtmAccept_mem_sharpP : SharpP.Mem SharpNTMAccept

Counting accepting runs is in #P: the runs are the witnesses of an existential second-order sentence, the tableau of a run being determined by it.

theorem DescriptiveComplexity.sharpNtmAccept_reduces_to_sharpSat : Nonempty (OrderedParsimoniousReduction SharpNTMAccept SharpSAT)

The textbook counting Cook–Levin theorem: counting the accepting runs of a machine reduces, parsimoniously, to counting the models of a CNF formula. As on the decision side, no tableau-to-CNF encoding appears: the Σ₁ definition of a run feeds the generic parsimonious Tseitin reduction.