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 #

Reading the result in the hand-rolled vocabulary #

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
    theorem DescriptiveComplexity.graphIso_GI_complete :
    GI.Complete GraphIso

    Graph Isomorphism is GI-complete, the degree being defined on it. Registered in the Lax archive as Lax604544.GraphIsomorphismDegree.graphIso_GI_complete.

    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. Registered in the Lax archive as Lax604544.GraphIsomorphismDegree.digraphIso_GI_complete.

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

    The directed and undirected problems have the same degree. Registered in the Lax archive as Lax604544.GraphIsomorphismDegree.GI_eq_below_digraphIso.

    Dependency graph