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 : Type

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

@[instance_reducible]

instance DescriptiveComplexity.DagIso.instDecidableEqNodeTag : DecidableEq NodeTag

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.DagIso.instFintypeNodeTag : Fintype NodeTag

Equations

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

instance DescriptiveComplexity.DagIso.instNonemptyNodeTag : Nonempty NodeTag

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)

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₁ = ⊥

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

• DescriptiveComplexity.DagIso.ltF DescriptiveComplexity.DagIso.NodeTag.vtx DescriptiveComplexity.DagIso.NodeTag.arcMid = ⊤
• DescriptiveComplexity.DagIso.ltF DescriptiveComplexity.DagIso.NodeTag.vtx DescriptiveComplexity.DagIso.NodeTag.arcEnd = ⊤
• DescriptiveComplexity.DagIso.ltF DescriptiveComplexity.DagIso.NodeTag.arcMid DescriptiveComplexity.DagIso.NodeTag.arcEnd = ⊤
• DescriptiveComplexity.DagIso.ltF t s = ⊥

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.

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

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

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

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

theorem DescriptiveComplexity.DagIso.two_eta {A : Type} (w : Fin 2 → A) : w = ![w 0, w 1]

theorem DescriptiveComplexity.DagIso.vtx_eta {A : Type} (w : Fin 2 → A) : (NodeTag.vtx, w) = vPt2 (w 0) (w 1)

A point of the vertex level, in named form.

theorem DescriptiveComplexity.DagIso.mid_eta {A : Type} (w : Fin 2 → A) : (NodeTag.arcMid, w) = midPt (w 0) (w 1)

A point of the middle level, in named form.

theorem DescriptiveComplexity.DagIso.end_eta {A : Type} (w : Fin 2 → A) : (NodeTag.arcEnd, w) = endPt (w 0) (w 1)

A point of the end level, in named form.

theorem DescriptiveComplexity.DagIso.vPt_injective {A : Type} : Function.Injective vPt

theorem DescriptiveComplexity.DagIso.midPt_inj {A : Type} {u v u' v' : A} (h : midPt u v = midPt u' v') : u = u' ∧ v = v'

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

@[simp]

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

@[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

@[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

theorem DescriptiveComplexity.DagIso.patV_cases {A : Type} [FirstOrder.Language.twoGraphs.Structure A] {p : incInterp.Map A} (h : TDPatV p) : (∃ (v : A), TGPatV v ∧ p = vPt v) ∨ (∃ (u : A) (v : A), (TGPatV u ∧ TGPatV v ∧ TGPatE u v) ∧ p = midPt u v) ∨ ∃ (u : A) (v : A), (TGPatV u ∧ TGPatV v ∧ TGPatE u v) ∧ p = endPt u v

A pattern node is a vertex node, a middle node or an end node. The hypothesis is unfolded by rcases rather than by rw: the defining formula's realization is definitionally a conjunction, and a pair literal at FOInterpretation.Map type does not match at rewriting transparency.

theorem DescriptiveComplexity.DagIso.pat_arc_tag {A : Type} [FirstOrder.Language.twoGraphs.Structure A] {p q : incInterp.Map A} (h : TDPatArc p q) : p.1 = NodeTag.vtx ∧ q.1 = NodeTag.arcMid ∨ p.1 = NodeTag.vtx ∧ q.1 = NodeTag.arcEnd ∨ p.1 = NodeTag.arcMid ∧ q.1 = NodeTag.arcEnd

The only arcs are the three of the gadget: the tags of an arc's endpoints climb the three levels. The six forbidden tag combinations need no argument – their defining formula is ⊥, so the hypothesis is False.

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.

theorem DescriptiveComplexity.DagIso.pat_no_out_endPt {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (u v : A) (q : incInterp.Map A) : ¬TDPatArc (endPt u v) q

An end node points at nothing: level 2 is the top.

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

Two middle nodes are never joined: they sit at the same level.

@[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

@[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

@[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'

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

@[simp]

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

@[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

@[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

theorem DescriptiveComplexity.DagIso.hostV_cases {A : Type} [FirstOrder.Language.twoGraphs.Structure A] {p : incInterp.Map A} (h : TDHostV p) : (∃ (v : A), TGHostV v ∧ p = vPt v) ∨ (∃ (u : A) (v : A), (TGHostV u ∧ TGHostV v ∧ TGHostE u v) ∧ p = midPt u v) ∨ ∃ (u : A) (v : A), (TGHostV u ∧ TGHostV v ∧ TGHostE u v) ∧ p = endPt u v

A host node is a vertex node, a middle node or an end node. The hypothesis is unfolded by rcases rather than by rw: the defining formula's realization is definitionally a conjunction, and a pair literal at FOInterpretation.Map type does not match at rewriting transparency.

theorem DescriptiveComplexity.DagIso.host_arc_tag {A : Type} [FirstOrder.Language.twoGraphs.Structure A] {p q : incInterp.Map A} (h : TDHostArc p q) : p.1 = NodeTag.vtx ∧ q.1 = NodeTag.arcMid ∨ p.1 = NodeTag.vtx ∧ q.1 = NodeTag.arcEnd ∨ p.1 = NodeTag.arcMid ∧ q.1 = NodeTag.arcEnd

The only arcs are the three of the gadget: the tags of an arc's endpoints climb the three levels. The six forbidden tag combinations need no argument – their defining formula is ⊥, so the hypothesis is False.

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

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

theorem DescriptiveComplexity.DagIso.host_no_out_endPt {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (u v : A) (q : incInterp.Map A) : ¬TDHostArc (endPt u v) q

An end node points at nothing: level 2 is the top.

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

Two middle nodes are never joined: they sit at the same level.

@[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

@[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

@[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'

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

• DescriptiveComplexity.DagIso.level DescriptiveComplexity.DagIso.NodeTag.vtx = 0
• DescriptiveComplexity.DagIso.level DescriptiveComplexity.DagIso.NodeTag.arcMid = 1
• DescriptiveComplexity.DagIso.level DescriptiveComplexity.DagIso.NodeTag.arcEnd = 2

@[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

@[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

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

Arcs climb the levels, on the pattern side.

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

Arcs climb the levels, on the host side.

theorem DescriptiveComplexity.DagIso.topoOn_pat {A : Type} [FirstOrder.Language.twoGraphs.Structure A] : TopoOn TDPatV TDPatLt TDPatArc

The pattern side of the image is a DAG, with the carried order as witness: the order is the level comparison, so irreflexivity and transitivity are those of < on ℕ, and every arc climbs a level.

theorem DescriptiveComplexity.DagIso.topoOn_host {A : Type} [FirstOrder.Language.twoGraphs.Structure A] : TopoOn TDHostV TDHostLt TDHostArc

The host side of the image is a DAG, likewise.

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem DescriptiveComplexity.DagIso.liftMap_tag {A : Type} (g : A → A) (p : incInterp.Map A) : (liftMap g p).1 = p.1

theorem DescriptiveComplexity.DagIso.patV_coords {A : Type} [FirstOrder.Language.twoGraphs.Structure A] {p : incInterp.Map A} (h : TDPatV p) : TGPatV (p.2 0) ∧ TGPatV (p.2 1)

Both coordinates of a pattern node are marked vertices.

theorem DescriptiveComplexity.DagIso.relIsoOn_map {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (g : A → A) (hmaps : ∀ (x : A), TGPatV x → TGHostV (g x)) (hinj : ∀ (x y : A), TGPatV x → TGPatV y → g x = g y → x = y) (hsurj : ∀ (y : A), TGHostV y → ∃ (x : A), TGPatV x ∧ g x = y) (hedge : ∀ (x y : A), TGPatV x → TGPatV y → (TGPatE x y ↔ TGHostE (g x) (g y))) : RelIsoOn TDPatV TDHostV TDPatArc TDHostArc

The gadget is functorial and faithful: an isomorphism of the two marked graphs lifts, level by level, to an isomorphism of the two DAGs. The six combinations of levels that carry no arc are dispatched by the level lemmas, the three that do by the corresponding characterizations.

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

theorem DescriptiveComplexity.DagIso.image_vPt {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (F : incInterp.Map A → incInterp.Map A) (hmaps : ∀ (p : incInterp.Map A), TDPatV p → TDHostV (F p)) (hsurj : ∀ (q : incInterp.Map A), TDHostV q → ∃ (p : incInterp.Map A), TDPatV p ∧ F p = q) (hedge : ∀ (p q : incInterp.Map A), TDPatV p → TDPatV q → (TDPatArc p q ↔ TDHostArc (F p) (F q))) {v : A} (hv : TGPatV v) : ∃ (w : A), TGHostV w ∧ F (vPt v) = vPt w

An isomorphism of the DAGs sends vertex nodes to vertex nodes: they are the nodes nothing points at, and that is preserved because every host node is the image of a pattern node.

theorem DescriptiveComplexity.DagIso.image_endPt_no_out {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (F : incInterp.Map A → incInterp.Map A) (hsurj : ∀ (q : incInterp.Map A), TDHostV q → ∃ (p : incInterp.Map A), TDPatV p ∧ F p = q) (hedge : ∀ (p q : incInterp.Map A), TDPatV p → TDPatV q → (TDPatArc p q ↔ TDHostArc (F p) (F q))) {x y : A} (he : TDPatV (endPt x y)) (q : incInterp.Map A) (hq : TDHostV q) : ¬TDHostArc (F (endPt x y)) q

Nothing follows the image of an end node: end nodes are the nodes with no outgoing arc, and that too is preserved.

theorem DescriptiveComplexity.DagIso.image_midPt_shape {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (F : incInterp.Map A → incInterp.Map A) (hmaps : ∀ (p : incInterp.Map A), TDPatV p → TDHostV (F p)) (hedge : ∀ (p q : incInterp.Map A), TDPatV p → TDPatV q → (TDPatArc p q ↔ TDHostArc (F p) (F q))) {x y : A} (hx : TGPatV x) (hy : TGPatV y) (hxy : TGPatE x y) : ∃ (x' : A) (y' : A), (TGHostV x' ∧ TGHostV y' ∧ TGHostE x' y') ∧ F (midPt x y) = midPt x' y'

The image of a middle node is a middle node: it has both an incoming and an outgoing arc, which no other level has.

theorem DescriptiveComplexity.DagIso.image_endPt_shape {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (F : incInterp.Map A → incInterp.Map A) (hmaps : ∀ (p : incInterp.Map A), TDPatV p → TDHostV (F p)) (hsurj : ∀ (q : incInterp.Map A), TDHostV q → ∃ (p : incInterp.Map A), TDPatV p ∧ F p = q) (hedge : ∀ (p q : incInterp.Map A), TDPatV p → TDPatV q → (TDPatArc p q ↔ TDHostArc (F p) (F q))) {x y : A} (hx : TGPatV x) (hy : TGPatV y) (hxy : TGPatE x y) : ∃ (x' : A) (y' : A), (TGHostV x' ∧ TGHostV y' ∧ TGHostE x' y') ∧ F (endPt x y) = endPt x' y'

The image of an end node is an end node.

theorem DescriptiveComplexity.DagIso.image_midPt_eq {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (F : incInterp.Map A → incInterp.Map A) (hmaps : ∀ (p : incInterp.Map A), TDPatV p → TDHostV (F p)) (hsurj : ∀ (q : incInterp.Map A), TDHostV q → ∃ (p : incInterp.Map A), TDPatV p ∧ F p = q) (hedge : ∀ (p q : incInterp.Map A), TDPatV p → TDPatV q → (TDPatArc p q ↔ TDHostArc (F p) (F q))) (g : A → A) (hg : ∀ (v : A), TGPatV v → TGHostV (g v) ∧ F (vPt v) = vPt (g v)) {x y : A} (hx : TGPatV x) (hy : TGPatV y) (hxy : TGPatE x y) : F (midPt x y) = midPt (g x) (g y) ∧ F (endPt x y) = endPt (g x) (g y)

The image of the middle node of an arc is the middle node of the image arc: the tail is pinned by the arc from the tail's vertex node, the head by the arc from the head's vertex node through the end node.

Correctness of the reduction

theorem DescriptiveComplexity.DagIso.relIsoOn_of_dagIso {A : Type} [FirstOrder.Language.twoGraphs.Structure A] (h : RelIsoOn TDPatV TDHostV TDPatArc TDHostArc) : RelIsoOn TGPatV TGHostV TGPatE TGHostE

Reading an isomorphism of the DAGs on level 0: it maps vertex nodes to vertex nodes, so it restricts to a bijection of the marked vertices, and the arcs of the graphs are recovered from the arcs of the gadget through the middle and end nodes.

theorem DescriptiveComplexity.DagIso.hasDigraphIso_iff_hasDagIso_map (A : Type) [FirstOrder.Language.twoGraphs.Structure A] [Finite A] : HasDigraphIso A ↔ HasDagIso (incInterp.Map A)

Correctness of the reduction: the two graphs are isomorphic exactly when the two DAGs built from them are.

def DescriptiveComplexity.digraphIso_fo_reduction_dagIso : FOReduction DigraphIso DagIso

Digraph Isomorphism FO-reduces to DAG Isomorphism: subdivide every arc twice, and carry the level comparison as the topological order. Two dimensions, three tags, and no order on the input – the reduction is order-free, as every reduction between isomorphism problems must be.

Equations

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