Documentation

DescriptiveComplexity.Problems.DagIso.FromDigraphIso

Digraph Isomorphism reduces to DAG Isomorphism #

The substantial half of GI-completeness: an arbitrary directed graph is turned into a DAG whose isomorphisms are exactly the isomorphisms of the graph. Every arc is subdivided twice,

  u  ⟶  a(u,v)  ⟶  b(u,v)  ⟵  v

so that the arc u ⟶ v becomes a three-level pattern: the tail u points at the middle node a(u,v), which points at the end node b(u,v), which the head v also points at. Subdividing once would not do – with a single node per arc the two endpoints would be interchangeable and the direction of the arc lost; here the tail is the vertex pointing at a middle node and the head the vertex pointing at an end node.

The construction is acyclic by inspection: every arc goes from level 0 (vertices) to level 1 (middle nodes) or level 2 (end nodes), or from level 1 to level 2. That is also the topological order the instance must carry, and it needs no formula at all – it is read off the tags (DescriptiveComplexity.DagIso.ltF), which is why the reduction stays order-free: FirstOrder.Language.twoGraphs carries its own vertex marks, so the same gadget runs on the pattern side and on the host side inside a single interpretation, junk staying unmarked.

The three levels are recovered from the arcs alone, without any counting: a vertex node is one with no incoming arc, an end node one with an incoming but no outgoing arc, and a middle node has both (DescriptiveComplexity.DagIso.pat_no_in_vPt and its siblings). An isomorphism of the two DAGs therefore preserves the levels, and reading it on level 0 gives the isomorphism of the graphs.

The tags: the three levels of the construction #

inductive DescriptiveComplexity.DagIso.NodeTag :

The three kinds of node of the gadget: a vertex, the middle node of an arc, the end node of an arc.

vtx : NodeTag
A copy of a vertex of the input graph (level 0).
arcMid : NodeTag
The middle node a(u,v) of an arc u ⟶ v (level 1).
arcEnd : NodeTag
The end node b(u,v) of an arc u ⟶ v (level 2).

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.DagIso.instDecidableEqNodeTag :

DecidableEq NodeTag

Equations

DescriptiveComplexity.DagIso.instDecidableEqNodeTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.DagIso.instFintypeNodeTag :

Fintype NodeTag

Equations

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

Dependency graph

instance DescriptiveComplexity.DagIso.instNonemptyNodeTag :

Nonempty NodeTag

Dependency graph

The defining formulas #

def DescriptiveComplexity.DagIso.nodeF {α : Type} (mark : FirstOrder.Language.twoGraphs.Relations 1) (adj : FirstOrder.Language.twoGraphs.Relations 2) (t : NodeTag) (x y : α) :

FirstOrder.Language.twoGraphs.Formula α

Being a node of the gadget, for one side of the instance: a vertex node is a diagonal pair whose entry is a marked vertex, and an arc node is a pair that is an arc between two marked vertices.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.DagIso.nodeF mark adj DescriptiveComplexity.DagIso.NodeTag.vtx x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y) ⊓ mark.formula₁ (FirstOrder.Language.var x)

Instances For

Dependency graph

def DescriptiveComplexity.DagIso.arcF {α : Type} (mark : FirstOrder.Language.twoGraphs.Relations 1) (adj : FirstOrder.Language.twoGraphs.Relations 2) (t s : NodeTag) (x₀ x₁ y₀ y₁ : α) :

FirstOrder.Language.twoGraphs.Formula α

The arcs of the gadget: u ⟶ a(u,v), a(u,v) ⟶ b(u,v) and v ⟶ b(u,v), and nothing else.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.DagIso.arcF mark adj t s x₀ x₁ y₀ y₁ = ⊥

Instances For

Dependency graph

def DescriptiveComplexity.DagIso.ltF {α : Type} (t s : NodeTag) :

FirstOrder.Language.twoGraphs.Formula α

The topological order of the gadget: the level of the tag strictly increases. It mentions no variable at all – the whole point of the three-level layout.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.DagIso.incInterp :

FOInterpretation FirstOrder.Language.twoGraphs FirstOrder.Language.twoDags NodeTag 2

The interpretation of Digraph Isomorphism into DAG Isomorphism: two dimensions (an arc is a pair), three tags (the three levels), the same gadget run on the pattern side and on the host side.

Equations

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

Instances For

Dependency graph

The points of the gadget #

def DescriptiveComplexity.DagIso.vPt2 {A : Type} (u v : A) :

incInterp.Map A

A point at the vertex level; it is a node only when its two coordinates agree (DescriptiveComplexity.DagIso.pat_vPt2).

Equations

DescriptiveComplexity.DagIso.vPt2 u v = (DescriptiveComplexity.DagIso.NodeTag.vtx , ![u, v])

Instances For

Dependency graph

def DescriptiveComplexity.DagIso.vPt {A : Type} (v : A) :

incInterp.Map A

The vertex node of a vertex.

Equations

DescriptiveComplexity.DagIso.vPt v = DescriptiveComplexity.DagIso.vPt2 v v

Instances For

Dependency graph

def DescriptiveComplexity.DagIso.midPt {A : Type} (u v : A) :

incInterp.Map A

The middle node of an arc.

Equations

DescriptiveComplexity.DagIso.midPt u v = (DescriptiveComplexity.DagIso.NodeTag.arcMid , ![u, v])

Instances For

Dependency graph

def DescriptiveComplexity.DagIso.endPt {A : Type} (u v : A) :

incInterp.Map A

The end node of an arc.

Equations

DescriptiveComplexity.DagIso.endPt u v = (DescriptiveComplexity.DagIso.NodeTag.arcEnd , ![u, v])

Instances For

Dependency graph

What the gadget builds, on the pattern side #

@[simp]

theorem DescriptiveComplexity.DagIso.pat_vPt2 {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (u v : A) :

TDPatV (vPt2 u v) ↔ u = v ∧ TGPatV u

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.pat_vPt {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (v : A) :

TDPatV (vPt v) ↔ TGPatV v

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.pat_midPt {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (u v : A) :

TDPatV (midPt u v) ↔ TGPatV u ∧ TGPatV v ∧ TGPatE u v

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.pat_endPt {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (u v : A) :

TDPatV (endPt u v) ↔ TGPatV u ∧ TGPatV v ∧ TGPatE u v

Dependency graph

theorem DescriptiveComplexity.DagIso.pat_no_in_vPt {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (q : incInterp.Map A) (v : A) :

¬TDPatArc q (vPt v)

Nothing points at a vertex node: level 0 is the bottom.

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.pat_arc_v_mid {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (x u v : A) :

TDPatArc (vPt x) (midPt u v) ↔ TGPatV x ∧ (TGPatV u ∧ TGPatV v ∧ TGPatE u v) ∧ x = u

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.pat_arc_v_end {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (x u v : A) :

TDPatArc (vPt x) (endPt u v) ↔ TGPatV x ∧ (TGPatV u ∧ TGPatV v ∧ TGPatE u v) ∧ x = v

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.pat_arc_mid_end {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (u v u' v' : A) :

TDPatArc (midPt u v) (endPt u' v') ↔ (TGPatV u ∧ TGPatV v ∧ TGPatE u v) ∧ (TGPatV u' ∧ TGPatV v' ∧ TGPatE u' v') ∧ u = u' ∧ v = v'

Dependency graph

What the gadget builds, on the host side #

@[simp]

theorem DescriptiveComplexity.DagIso.host_vPt2 {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (u v : A) :

TDHostV (vPt2 u v) ↔ u = v ∧ TGHostV u

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.host_vPt {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (v : A) :

TDHostV (vPt v) ↔ TGHostV v

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.host_midPt {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (u v : A) :

TDHostV (midPt u v) ↔ TGHostV u ∧ TGHostV v ∧ TGHostE u v

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.host_endPt {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (u v : A) :

TDHostV (endPt u v) ↔ TGHostV u ∧ TGHostV v ∧ TGHostE u v

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.host_arc_v_mid {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (x u v : A) :

TDHostArc (vPt x) (midPt u v) ↔ TGHostV x ∧ (TGHostV u ∧ TGHostV v ∧ TGHostE u v) ∧ x = u

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.host_arc_v_end {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (x u v : A) :

TDHostArc (vPt x) (endPt u v) ↔ TGHostV x ∧ (TGHostV u ∧ TGHostV v ∧ TGHostE u v) ∧ x = v

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.host_arc_mid_end {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (u v u' v' : A) :

TDHostArc (midPt u v) (endPt u' v') ↔ (TGHostV u ∧ TGHostV v ∧ TGHostE u v) ∧ (TGHostV u' ∧ TGHostV v' ∧ TGHostE u' v') ∧ u = u' ∧ v = v'

Dependency graph

The gadget is acyclic: the levels #

def DescriptiveComplexity.DagIso.level :

NodeTag → ℕ

The level of a node: vertices at 0, middle nodes at 1, end nodes at 2. The carried topological order is exactly the comparison of levels.

Equations

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.patLt_iff {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (p q : incInterp.Map A) :

TDPatLt p q ↔ level p.1 < level q.1

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.hostLt_iff {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (p q : incInterp.Map A) :

TDHostLt p q ↔ level p.1 < level q.1

Dependency graph

From an isomorphism of the graphs to one of the DAGs #

def DescriptiveComplexity.DagIso.liftMap {A : Type} (g : A → A) (p : incInterp.Map A) :

incInterp.Map A

A map of the universe, lifted to the nodes of the gadget: it keeps the level and acts on both coordinates.

Equations

DescriptiveComplexity.DagIso.liftMap g p = (p.1, fun (i : Fin 2) => g (p.2 i))

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.liftMap_vPt {A : Type} (g : A → A) (v : A) :

liftMap g (vPt v) = vPt (g v)

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.liftMap_midPt {A : Type} (g : A → A) (u v : A) :

liftMap g (midPt u v) = midPt (g u) (g v)

Dependency graph

@[simp]

theorem DescriptiveComplexity.DagIso.liftMap_endPt {A : Type} (g : A → A) (u v : A) :

liftMap g (endPt u v) = endPt (g u) (g v)

Dependency graph

From an isomorphism of the DAGs back to one of the graphs #

Correctness of the reduction #