Graph Isomorphism: vocabulary, semantics, and membership in the GI degree

GRAPH ISOMORPHISM, as the literature means it: are the two simple graphs of the instance isomorphic? DescriptiveComplexity.DigraphIso is the same question over FirstOrder.Language.twoGraphs with no condition on the two binary relations, hence for directed graphs; this problem is that one restricted to instances whose relations are symmetric and irreflexive.

Unlike acyclicity (DescriptiveComplexity.Problems.DagIso), that restriction is first-order, so nothing has to be carried by the instance: the reduction into DigraphIso simply tests it. This file also defines the GI degree (DescriptiveComplexity.GI), on this problem: it is what the literature means by graph isomorphism, so it is what the degree should be named after. The directed problem is complete for it too – the two are interreducible – but that needs the gadget of DescriptiveComplexity.Problems.GraphIso.Hardness, so it is proved there.

The generic property

def DescriptiveComplexity.SimpleOn {A : Type} (V : A → Prop) (E : A → A → Prop) : Prop

The relation E is symmetric and irreflexive on the marked set V: a simple graph, as opposed to an arbitrary binary relation.

Equations

• DescriptiveComplexity.SimpleOn V E = ((∀ (x y : A), V x → V y → E x y → E y x) ∧ ∀ (x : A), V x → ¬E x x)

theorem DescriptiveComplexity.SimpleOn.of_equiv {A B : Type} (u : B ≃ A) {VB : B → Prop} {EB : B → B → Prop} {VA : A → Prop} {EA : A → A → Prop} (hV : ∀ (b : B), VB b ↔ VA (u b)) (hE : ∀ (b b' : B), EB b b' ↔ EA (u b) (u b')) (h : SimpleOn VB EB) : SimpleOn VA EA

SimpleOn transports along an equivalence commuting with the two predicates.

theorem DescriptiveComplexity.SimpleOn.equiv_iff {A B : Type} (u : B ≃ A) {VB : B → Prop} {EB : B → B → Prop} {VA : A → Prop} {EA : A → A → Prop} (hV : ∀ (b : B), VB b ↔ VA (u b)) (hE : ∀ (b b' : B), EB b b' ↔ EA (u b) (u b')) : SimpleOn VB EB ↔ SimpleOn VA EA

SimpleOn transports along an equivalence, iff version.

The problem

def DescriptiveComplexity.HasGraphIso (A : Type) [FirstOrder.Language.twoGraphs.Structure A] : Prop

Both marked graphs are simple, and they are isomorphic.

Equations

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

theorem DescriptiveComplexity.hasGraphIso_iso {A B : Type} [FirstOrder.Language.twoGraphs.Structure A] [FirstOrder.Language.twoGraphs.Structure B] (e : FirstOrder.Language.twoGraphs.Equiv A B) : HasGraphIso A ↔ HasGraphIso B

The graph-isomorphism property is isomorphism-invariant. Registered in the Lax archive as Lax604544.IsomorphismInvariance.hasGraphIso_iso.

def DescriptiveComplexity.GraphIso : DecisionProblem FirstOrder.Language.twoGraphs

GRAPH ISOMORPHISM: are the two marked simple graphs isomorphic? Simplicity is part of the yes-condition, and is first-order, so a reduction can test it – unlike acyclicity in DescriptiveComplexity.DagIso, which has to be carried by the instance.

Equations

• DescriptiveComplexity.GraphIso = { Holds := fun (A : Type) (inst : FirstOrder.Language.twoGraphs.Structure A) => DescriptiveComplexity.HasGraphIso A, iso_invariant := ⋯ }

Membership: forget nothing, just check simplicity

noncomputable def DescriptiveComplexity.GraphIso.simpleSentence {α : Type} (V : FirstOrder.Language.twoGraphs.Relations 1) (E : FirstOrder.Language.twoGraphs.Relations 2) : FirstOrder.Language.twoGraphs.Formula α

E is symmetric and irreflexive on V, as a first-order sentence over any variable type, so that it can be conjoined inside the defining formulas of an interpretation.

Equations

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

noncomputable def DescriptiveComplexity.GraphIso.wfSentence {α : Type} : FirstOrder.Language.twoGraphs.Formula α

Both sides of the instance are simple graphs.

Equations

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

noncomputable def DescriptiveComplexity.GraphIso.simpleInterp : FOInterpretation FirstOrder.Language.twoGraphs FirstOrder.Language.twoGraphs Unit 1

The interpretation of Graph Isomorphism into Digraph Isomorphism: copy both marked graphs if they are simple, and otherwise emit a pattern with no vertices facing a host with all of them.

Equations

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

The degree

noncomputable def DescriptiveComplexity.GI : ComplexityClass

The GI degree: the problems that (ordered) first-order reduce to Graph Isomorphism, as a complexity class (DescriptiveComplexity.ComplexityClass.below). A problem is GI-complete – in this library's finer, first-order sense – when it is DescriptiveComplexity.ComplexityClass.Complete for GI.

The degree is named after the undirected problem, as the literature is: the directed one has the same degree (DescriptiveComplexity.GI_eq_below_digraphIso), but is not what “GI” means.

Equations

• DescriptiveComplexity.GI = DescriptiveComplexity.ComplexityClass.below DescriptiveComplexity.GraphIso

theorem DescriptiveComplexity.graphIso_mem_GI : GI.Mem GraphIso

Graph Isomorphism belongs to its own degree.

theorem DescriptiveComplexity.graphIso_mem_NP : NP.Mem GraphIso

Graph Isomorphism is in NP: it reduces to the directed problem, which is. Registered in the Lax archive as Lax604544.IsomorphismInNP.graphIso_mem_NP.

theorem DescriptiveComplexity.GI_subset_NP : GI ⊆ NP

The whole GI degree lies inside NP, since Graph Isomorphism does and membership travels backward along reductions. (Whether the inclusion is strict is the open question; the framework decides no such thing.) Registered in the Lax archive as Lax604544.IsomorphismInNP.GI_subset_NP.