DAG Isomorphism reduces to Digraph Isomorphism

The easy half of GI-completeness, and the half that pays for the design of DescriptiveComplexity.Problems.DagIso.Defs: since FirstOrder.Language.twoGraphs carries two arbitrary binary relations – nothing asks them to be symmetric – DescriptiveComplexity.DigraphIso is already isomorphism of two directed graphs, so a DAG instance only has to forget its two topological orders.

What it may not forget is well-formedness. The reduction is a one-dimensional, single-tag interpretation that first tests, first-order, that both order relations really are topological orders of their arcs (DescriptiveComplexity.TopoOn, the sentence DescriptiveComplexity.DagIso.topoSentence): if the test passes it copies the two marked arc relations over, and if it fails it emits a pattern with no vertices facing a host with all of them – no bijection, hence a no-instance, matching the no-instance the ill-formed input is. This test is the whole reason the instances carry their acyclicity witness: acyclicity itself is not first-order, so no interpretation could gate on it.

The well-formedness sentence

noncomputable def DescriptiveComplexity.DagIso.topoIrreflClause {α : Type} (V : FirstOrder.Language.twoDags.Relations 1) (Lt : FirstOrder.Language.twoDags.Relations 2) : FirstOrder.Language.twoDags.Formula α

Lt is a topological order of Arc on V, as a first-order sentence (over any variable type, so that it can be conjoined inside the defining formulas of an interpretation): irreflexive and transitive on the marked set, and containing the arcs.

Equations

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

noncomputable def DescriptiveComplexity.DagIso.topoTransClause {α : Type} (V : FirstOrder.Language.twoDags.Relations 1) (Lt : FirstOrder.Language.twoDags.Relations 2) : FirstOrder.Language.twoDags.Formula α

Lt is a topological order of Arc on V, as a first-order sentence (over any variable type, so that it can be conjoined inside the defining formulas of an interpretation): irreflexive and transitive on the marked set, and containing the arcs.

Equations

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

noncomputable def DescriptiveComplexity.DagIso.topoMonoClause {α : Type} (V : FirstOrder.Language.twoDags.Relations 1) (Lt Arc : FirstOrder.Language.twoDags.Relations 2) : FirstOrder.Language.twoDags.Formula α

Lt is a topological order of Arc on V, as a first-order sentence (over any variable type, so that it can be conjoined inside the defining formulas of an interpretation): irreflexive and transitive on the marked set, and containing the arcs.

Equations

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

noncomputable def DescriptiveComplexity.DagIso.topoSentence {α : Type} (V : FirstOrder.Language.twoDags.Relations 1) (Lt Arc : FirstOrder.Language.twoDags.Relations 2) : FirstOrder.Language.twoDags.Formula α

Lt is a topological order of Arc on V, as a first-order sentence (over any variable type, so that it can be conjoined inside the defining formulas of an interpretation): irreflexive and transitive on the marked set, and containing the arcs.

Equations

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

theorem DescriptiveComplexity.DagIso.realize_topoSentence {A : Type} [FirstOrder.Language.twoDags.Structure A] {α : Type} (v : α → A) (V : FirstOrder.Language.twoDags.Relations 1) (Lt Arc : FirstOrder.Language.twoDags.Relations 2) : (topoSentence V Lt Arc).Realize v ↔ TopoOn (fun (a : A) => FirstOrder.Language.Structure.RelMap V ![a]) (fun (a b : A) => FirstOrder.Language.Structure.RelMap Lt ![a, b]) fun (a b : A) => FirstOrder.Language.Structure.RelMap Arc ![a, b]

The sentence says what it is named after.

noncomputable def DescriptiveComplexity.DagIso.wfSentence {α : Type} : FirstOrder.Language.twoDags.Formula α

Both sides of the instance are well formed.

Equations

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

theorem DescriptiveComplexity.DagIso.realize_wfSentence {A : Type} [FirstOrder.Language.twoDags.Structure A] {α : Type} (v : α → A) : wfSentence.Realize v ↔ TopoOn TDPatV TDPatLt TDPatArc ∧ TopoOn TDHostV TDHostLt TDHostArc

The interpretation

noncomputable def DescriptiveComplexity.DagIso.dagInterp : FOInterpretation FirstOrder.Language.twoDags FirstOrder.Language.twoGraphs Unit 1

The interpretation of DAG Isomorphism into Digraph Isomorphism: one dimension, one tag. If the instance is well formed, the two marked arc relations are copied verbatim – FirstOrder.Language.twoGraphs holds arbitrary binary relations, so a DAG needs no encoding. If it is not, the pattern is emptied while the host keeps every element, so the two sides cannot be isomorphic.

Equations

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

def DescriptiveComplexity.DagIso.dagPt {A : Type} (v : A) : dagInterp.Map A

The unique copy of a vertex.

Equations

• DescriptiveComplexity.DagIso.dagPt v = ((), fun (x : Fin 1) => v)

theorem DescriptiveComplexity.DagIso.dagPt_eta {A : Type} (t : Unit) (w : Fin 1 → A) : (t, w) = dagPt (w 0)

def DescriptiveComplexity.DagIso.dagEquiv {A : Type} : dagInterp.Map A ≃ A

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

Equations

• DescriptiveComplexity.DagIso.dagEquiv = { toFun := fun (p : DescriptiveComplexity.DagIso.dagInterp.Map A) => p.2 0, invFun := DescriptiveComplexity.DagIso.dagPt, left_inv := ⋯, right_inv := ⋯ }

What the interpretation realizes

theorem DescriptiveComplexity.DagIso.patV_map {A : Type} [FirstOrder.Language.twoDags.Structure A] (hwf : TopoOn TDPatV TDPatLt TDPatArc ∧ TopoOn TDHostV TDHostLt TDHostArc) (p : dagInterp.Map A) : TGPatV p ↔ TDPatV (dagEquiv p)

theorem DescriptiveComplexity.DagIso.hostV_map {A : Type} [FirstOrder.Language.twoDags.Structure A] (hwf : TopoOn TDPatV TDPatLt TDPatArc ∧ TopoOn TDHostV TDHostLt TDHostArc) (p : dagInterp.Map A) : TGHostV p ↔ TDHostV (dagEquiv p)

theorem DescriptiveComplexity.DagIso.patE_map {A : Type} [FirstOrder.Language.twoDags.Structure A] (hwf : TopoOn TDPatV TDPatLt TDPatArc ∧ TopoOn TDHostV TDHostLt TDHostArc) (p q : dagInterp.Map A) : TGPatE p q ↔ TDPatArc (dagEquiv p) (dagEquiv q)

theorem DescriptiveComplexity.DagIso.hostE_map {A : Type} [FirstOrder.Language.twoDags.Structure A] (hwf : TopoOn TDPatV TDPatLt TDPatArc ∧ TopoOn TDHostV TDHostLt TDHostArc) (p q : dagInterp.Map A) : TGHostE p q ↔ TDHostArc (dagEquiv p) (dagEquiv q)

theorem DescriptiveComplexity.DagIso.not_patV_map_of_not_wf {A : Type} [FirstOrder.Language.twoDags.Structure A] (hwf : ¬(TopoOn TDPatV TDPatLt TDPatArc ∧ TopoOn TDHostV TDHostLt TDHostArc)) (p : dagInterp.Map A) : ¬TGPatV p

When the instance is ill formed, no element of the image is a pattern vertex.

theorem DescriptiveComplexity.DagIso.hostV_map_of_not_wf {A : Type} [FirstOrder.Language.twoDags.Structure A] (hwf : ¬(TopoOn TDPatV TDPatLt TDPatArc ∧ TopoOn TDHostV TDHostLt TDHostArc)) (p : dagInterp.Map A) : TGHostV p

When the instance is ill formed, every element of the image is a host vertex.

Correctness

theorem DescriptiveComplexity.DagIso.hasDagIso_iff_hasDigraphIso_map (A : Type) [FirstOrder.Language.twoDags.Structure A] [Finite A] [Nonempty A] : HasDagIso A ↔ HasDigraphIso (dagInterp.Map A)

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

noncomputable def DescriptiveComplexity.dagIso_fo_reduction_digraphIso : FOReduction DagIso DigraphIso

DAG Isomorphism FO-reduces to Digraph Isomorphism: forget the two topological orders, after checking first-order that they are ones. The reduction is order-free.

Equations

• DescriptiveComplexity.dagIso_fo_reduction_digraphIso = { Tag := Unit, tagFinite := ⋯, tagNonempty := ⋯, dim := 1, toInterpretation := DescriptiveComplexity.DagIso.dagInterp, correct := ⋯ }