AC⁰ definability: first-order logic with the numeric predicates #

The class AC⁰, as a logic: a problem is AC⁰ definable when a single sentence over the arithmetic expansion of its vocabulary decides it on nonempty finite ordered structures – first-order logic with ≤, + and × on the ranks of the elements (DescriptiveComplexity.AC0Definable). Classically this is FO(≤, +, ×) = FO(≤, BIT), and (DLOGTIME-)uniform AC⁰ (Immerman 1999, Thm 1.17; Barrington, Immerman & Straubing 1990; in textbook form, Vollmer 1999 Thm 4.73, with Thm 4.69 for the non-uniform class); here, as everywhere in this library, the logic is the definition, and the identification with a circuit model is a bridge that is not built – see below.

Why `+` and `×` rather than `BIT` #

Expressively it makes no difference (the two are classically interdefinable – a fact the literature states rather than proves: Vollmer 1999 p. 163 attributes it to a 1994 e-mail of Lindell and to Immerman 1999 §1.2.1, and DescriptiveComplexity.LogTime proves it), so the choice is made by a proof obligation elsewhere: the closure of the class under first-order reductions must define the numeric predicates of the interpreted universe – lexicographically ordered tagged tuples, hence base-n digits – from those of the base. For + and × that is schoolbook arithmetic on a constant number of digits; for BIT it is base-n-to-base-2 conversion, whose only route is to define + and × on the tuples first. So BIT is a later addition, not the primitive.

Order-invariance, and the absence of an order-free variant #

The definition quantifies over structures carrying a LinearOrder, and requires the equivalence for every linear order: the sentence sees ≤, +, ×, the problem does not. This is verbatim the convention of DescriptiveComplexity.FODefinable, and it is not a convenience here but a necessity: the numeric predicates are functions of the order (DescriptiveComplexity.Arithmetic), so there is no order-free reading of this logic to state, and no AC0DefinableFree in this file. Together with DescriptiveComplexity.LOGSPACE, whose logic is an operator rather than a fragment, this is the second place where the bottom of the ladder breaks the pattern of the classes above it.

What is proved here, and what is not #

FO(≤) ⊆ AC⁰ (DescriptiveComplexity.FODefinable.ac0Definable), by transport along DescriptiveComplexity.sumOrderToArith; the inclusion is strict (DescriptiveComplexity.exists_ac0Definable_not_foDefinable, in DescriptiveComplexity.Problems.Even), so the numeric predicates genuinely add power, unconditionally and with no complexity assumption.
Closure under complement (DescriptiveComplexity.AC0Definable.compl) – free, since the defining object is a sentence, where every class above needed an argument (Immerman–Szelepcsényi for NL, a determinized walk for LOGSPACE).
Not here: that AC⁰ definability is closed under first-order reductions (the arithmetic of an interpreted universe, as above), and therefore no DescriptiveComplexity.ComplexityClass yet; and no circuit model, so no capture theorem. The inclusion in DescriptiveComplexity.LOGSPACE is proved separately, through the multi-head automaton, and gives every consumer that the missing closure lemma would.

The definition #

source

def DescriptiveComplexity.AC0Definable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) :

Prop

A decision problem is AC⁰ definable if a single sentence over the arithmetic expansion of its vocabulary decides it on nonempty finite ordered structures. The equivalence is required for every linear order, so the notion is order-invariant: the sentence sees ≤, + and ×, the problem does not.

There is deliberately no order-free variant: the numeric predicates are computed from the order (DescriptiveComplexity.arithStructure), so without one there is nothing for them to mean.

Equations

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

Instances For

Dependency graph

source

theorem DescriptiveComplexity.ac0Definable_congr {L : FirstOrder.Language} [L.IsRelational] {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) :

AC0Definable P ↔ AC0Definable Q

AC⁰ definability only depends on the finite instances of a problem – the hypothesis a DescriptiveComplexity.ComplexityClass demands of its membership predicate.

Dependency graph

First-order definability, read arithmetically #

source

theorem DescriptiveComplexity.FODefinable.ac0Definable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : FODefinable P) :

AC0Definable P

FO(≤) ⊆ AC⁰: an order-invariant first-order definition is an arithmetic one, by transport along DescriptiveComplexity.sumOrderToArith – the numeric predicates are simply not used. The inclusion is strict (DescriptiveComplexity.exists_ac0Definable_not_foDefinable).

Dependency graph

source

theorem DescriptiveComplexity.FODefinableFree.ac0Definable {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : FODefinableFree P) :

AC0Definable P

An order-free first-order definition is in particular an arithmetic one.

Dependency graph

Boolean closure #

source

theorem DescriptiveComplexity.AC0Definable.compl {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : AC0Definable P) :

AC0Definable Pᶜ

AC⁰ is closed under complement: negate the sentence. Nothing like Immerman–Szelepcsényi is needed at this level – the defining object is a sentence, not a walk.

Dependency graph

Terms of a relational language #

Every vocabulary in this library is relational, and so is FirstOrder.Language.arith: a term is a variable and nothing else. Two consumers need to say so – the evaluator of an arithmetic formula (DescriptiveComplexity.HeadEvalArith) and the translation of one into the bit logic – so it is said here, below both.