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.

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.

theorem DescriptiveComplexity.GraphIso.realize_simpleSentence {A : Type} [FirstOrder.Language.twoGraphs.Structure A] {α : Type} (v : α → A) (V : FirstOrder.Language.twoGraphs.Relations 1) (E : FirstOrder.Language.twoGraphs.Relations 2) : (simpleSentence V E).Realize v ↔ SimpleOn (fun (a : A) => FirstOrder.Language.Structure.RelMap V ![a]) fun (a b : A) => FirstOrder.Language.Structure.RelMap E ![a, b]

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.

theorem DescriptiveComplexity.GraphIso.realize_wfSentence {A : Type} [FirstOrder.Language.twoGraphs.Structure A] {α : Type} (v : α → A) : wfSentence.Realize v ↔ SimpleOn TGPatV TGPatE ∧ SimpleOn TGHostV TGHostE

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.

def DescriptiveComplexity.GraphIso.uPt {A : Type} (v : A) : simpleInterp.Map A

The unique copy of a vertex.

Equations

• DescriptiveComplexity.GraphIso.uPt v = ((), fun (x : Fin 1) => v)

theorem DescriptiveComplexity.GraphIso.uPt_eta {A : Type} (t : Unit) (w : Fin 1 → A) : (t, w) = uPt (w 0)

def DescriptiveComplexity.GraphIso.uEquiv {A : Type} : simpleInterp.Map A ≃ A

The map is a copy of the universe: dimension one, one tag.

Equations

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

theorem DescriptiveComplexity.GraphIso.patV_map {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (hwf : SimpleOn TGPatV TGPatE ∧ SimpleOn TGHostV TGHostE) (p : simpleInterp.Map A) : TGPatV p ↔ TGPatV (uEquiv p)

theorem DescriptiveComplexity.GraphIso.hostV_map {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (hwf : SimpleOn TGPatV TGPatE ∧ SimpleOn TGHostV TGHostE) (p : simpleInterp.Map A) : TGHostV p ↔ TGHostV (uEquiv p)

theorem DescriptiveComplexity.GraphIso.patE_map {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (hwf : SimpleOn TGPatV TGPatE ∧ SimpleOn TGHostV TGHostE) (p q : simpleInterp.Map A) : TGPatE p q ↔ TGPatE (uEquiv p) (uEquiv q)

theorem DescriptiveComplexity.GraphIso.hostE_map {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (hwf : SimpleOn TGPatV TGPatE ∧ SimpleOn TGHostV TGHostE) (p q : simpleInterp.Map A) : TGHostE p q ↔ TGHostE (uEquiv p) (uEquiv q)

theorem DescriptiveComplexity.GraphIso.not_patV_map_of_not_wf {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (hwf : ¬(SimpleOn TGPatV TGPatE ∧ SimpleOn TGHostV TGHostE)) (p : simpleInterp.Map A) : ¬TGPatV p

theorem DescriptiveComplexity.GraphIso.hostV_map_of_not_wf {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (hwf : ¬(SimpleOn TGPatV TGPatE ∧ SimpleOn TGHostV TGHostE)) (p : simpleInterp.Map A) : TGHostV p

theorem DescriptiveComplexity.GraphIso.hasGraphIso_iff_hasDigraphIso_map (A : Type) [FirstOrder.Language.twoGraphs.Structure A] [Finite A] [Nonempty A] : HasGraphIso A ↔ HasDigraphIso (simpleInterp.Map A)

Correctness: the image is a yes-instance of Digraph Isomorphism exactly when the input is one of Graph Isomorphism.

noncomputable def DescriptiveComplexity.graphIso_fo_reduction_digraphIso : FOReduction GraphIso DigraphIso

Graph Isomorphism FO-reduces to Digraph Isomorphism: check simplicity first-order, then copy.

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.

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.)