Skip to content

v1.1.0 – for Mathlib v4.33.0-rc1

Latest
Latest

Choose a tag to compare

View all tags
@PierreSenellart PierreSenellart released this 07 Aug 08:17
v1.1.0
c789440

Requires Mathlib v4.33.0-rc1 and toolchain leanprover/lean4:v4.33.0-rc1.

Four new areas – the RE degree, the fixed-point logics and
Abiteboul–Vianu, inexpressibility by Ehrenfeucht–Fraïssé games, and the
Graph Isomorphism degree – together with a foundational restriction of
the library to relational vocabularies.

Undecidability, and the RE degree

  • HALT and PCP are RE-complete, and Post's correspondence problem is
    undecidable. Hardness stays machine-free on the source side: the program
    is carried by the instance rather than compiled into one.
  • This closes the bridge opened in v1.0.0 by CODEHALT and Trakhtenbrot: the
    RE degree now holds its classical members.

Fixed-point logics, and Abiteboul–Vianu

  • FO(IFP) and FO(PFP), with their captures of PTIME and PSPACE.
  • The Abiteboul–Vianu theorem: order-free FO(IFP) = FO(PFP) exactly when
    PTIME = PSPACE, with the ordered corollary.
  • Immerman–Vardi is now named, and discharged from the logic rather than
    restated.

Inexpressibility, by games

  • Ehrenfeucht–Fraïssé games, giving EVEN ∉ FO even in the presence of an
    order    , hence FO ⊊ FO(TC) unconditionally.
  • The two-structure k-pebble game: order-free FO(IFP) defines no order, and
    so does not capture PTIME.
  • First-order definability travels backward along reductions, so EVEN
    reduces to no FO-definable problem.

The Graph Isomorphism degree

  • ComplexityClass.below and Degree: completeness relative to a problem
    rather than to a class, with NP = below SAT as the sanity check.
  • Directed, undirected and DAG isomorphism, and the digraph-to-graph gadget
    that closes the degree on the undirected problem, as the literature states
    it.

Also new

  • CVP is PTIME-complete, both halves machine-free: hardness draws unit
    propagation as a monotone circuit inside a HORN-SAT instance.
  • The Cook–Levin interreducibility statement, both directions in one theorem.
  • Order-free SO(TC).
  • Honest encodings for weighted problems: the binary encoding of a list of
    weights and a target, faithful for Knapsack, and the computable decoder back
    – so knapsack_NP_complete is a statement about concrete lists of
    binary-written numbers in both directions.

Foundations

  • The library is now restricted to relational vocabularies: DecisionProblem
    takes an IsRelational instance. This is a breaking change for downstream
    users defining their own problems; it removed a whole relationalization layer
    and simplified the extended-structure machinery.
  • autoImplicit is disabled throughout.
  • A class now declares only its members: ComplexityClass.ofMem derives cofinal
    hardness once.
  • The integer-representation design is anchored in Numbers.lean.

Housekeeping

A CONTRIBUTING.md; a README rewritten around the three layers; citation
anchored on the concept DOI, with a Software Heritage badge beside it; CI
hardened (least-privilege token, path-guarded workflows, Dependabot on the
actions, a documentation cache) and the monthly Mathlib pin move driven from
scripts/release.sh.

Use

require "descriptive-complexity" from git
  "https://github.com/PierreSenellart/descriptive-complexity" @ "v1.1.0"

See the compatibility table
for which version to use with which Mathlib.

Assets 2
Loading