Documentation

DescriptiveComplexity.Problems.GraphIso.Hardness

Graph Isomorphism is GI-complete #

The last step: the gadget of DescriptiveComplexity.Problems.GraphIso.Gadget, doubled by DescriptiveComplexity.GadgetDouble and read through the renaming of DescriptiveComplexity.Problems.DigraphIso.Bridge, reduces Digraph Isomorphism to Graph Isomorphism. Since simplicity is first-order the converse reduction is a gated copy (DescriptiveComplexity.Problems.GraphIso.Defs), so the two problems are interreducible and the degree they define is the same.

The one thing the doubling does not carry by itself is simplicity: its target is the unrestricted DescriptiveComplexity.TwoCopiesIso, while DescriptiveComplexity.GraphIso asks its instances to be simple graphs. That is discharged here, by transporting the gadget's symmetry and irreflexivity (DescriptiveComplexity.GraphGadget.edge_symm, DescriptiveComplexity.GraphGadget.edge_irrefl) along the identification of the sides of a doubled construction with the gadget's values (DescriptiveComplexity.patSideDoubleEquiv).

The doubled gadget builds simple graphs #

source
theorem DescriptiveComplexity.GraphHard.simpleOn_pat {Z : Type} [FirstOrder.Language.graph.twoCopies.Structure Z] :
SimpleOn TCPatMark DigraphBridge.TCPatAdj

The pattern side of the doubled gadget is a simple graph: its adjacency is the gadget's, which is symmetric and loopless.

Dependency graph
source
theorem DescriptiveComplexity.GraphHard.simpleOn_host {Z : Type} [FirstOrder.Language.graph.twoCopies.Structure Z] :
SimpleOn TCHostMark DigraphBridge.TCHostAdj

The host side of the doubled gadget is a simple graph.

Dependency graph

Reading the result in the hand-rolled vocabulary #

source
theorem DescriptiveComplexity.GraphHard.simpleOn_ofTC_pat {Y : Type} [FirstOrder.Language.graph.twoCopies.Structure Y] (h : SimpleOn TCPatMark DigraphBridge.TCPatAdj) :
SimpleOn TGPatV TGPatE

If the two sides of a generic instance are simple, so are the two sides of its renaming into FirstOrder.Language.twoGraphs.

Dependency graph
source
theorem DescriptiveComplexity.GraphHard.simpleOn_ofTC_host {Y : Type} [FirstOrder.Language.graph.twoCopies.Structure Y] (h : SimpleOn TCHostMark DigraphBridge.TCHostAdj) :
SimpleOn TGHostV TGHostE

If the two sides of a generic instance are simple, so are the two sides of its renaming into FirstOrder.Language.twoGraphs.

Dependency graph

Correctness of the composite #

source
theorem DescriptiveComplexity.GraphHard.twoCopiesIso_iff_graphIso_map {Z : Type} [FirstOrder.Language.graph.twoCopies.Structure Z] [Finite Z] :
(TwoCopiesIso FirstOrder.Language.graph).Holds Z ↔ GraphIso.Holds (DigraphBridge.ofTC.Map (GraphGadget.gadget.double.Map Z))

The doubled gadget, renamed, reduces the generic isomorphism problem to Graph Isomorphism. Simplicity of the image is what upgrades the target from the unrestricted problem to the simple-graph one.

Dependency graph

The reduction and the completeness theorem #

source
noncomputable def DescriptiveComplexity.twoCopiesIso_fo_reduction_graphIso :
FOReduction (TwoCopiesIso FirstOrder.Language.graph) GraphIso

The generic isomorphism problem reduces to Graph Isomorphism: subdivide every arc three times, mark each vertex with a lollipop and each tail with a pendant, then read the result as a pair of simple graphs.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    noncomputable def DescriptiveComplexity.digraphIso_fo_reduction_graphIso :
    FOReduction DigraphIso GraphIso

    Digraph Isomorphism reduces to Graph Isomorphism: the classical digraph-to-graph construction, through the renaming into the generic vocabulary.

    Equations
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.graphIso_GI_complete :
      GI.Complete GraphIso

      Graph Isomorphism is GI-complete, the degree being defined on it.

      Dependency graph
      source
      theorem DescriptiveComplexity.digraphIso_GI_complete :
      GI.Complete DigraphIso

      Digraph Isomorphism is GI-complete too: it reduces to the undirected problem by the gadget – every arc subdivided three times, each vertex carrying a lollipop and each tail a pendant – and the undirected problem reduces back to it by testing simplicity. The directed problem is not what the literature calls GI, which is why the degree is named after the other one; this theorem is what says the choice costs nothing.

      Dependency graph
      source
      theorem DescriptiveComplexity.GI_eq_below_digraphIso :
      GI = ComplexityClass.below DigraphIso

      The directed and undirected problems have the same degree.

      Dependency graph
      source
      theorem DescriptiveComplexity.GI_eq_below_twoCopiesIso :
      GI = ComplexityClass.below (TwoCopiesIso FirstOrder.Language.graph)

      And the same as the degree of the generic isomorphism problem of the graph vocabulary, which is what a new entry stated over twoCopies reduces to.

      Dependency graph