Isomorphism of directed acyclic graphs
Lax604544.DagIsomorphism · concepts/Lax604544/DagIsomorphism.lean · lax-604544
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance is a pair of directed graphs on one universe, each with a mark on its vertices, a relation of arcs and a further binary relation given as a witness of acyclicity. That relation is a topological order of the arcs when it is a strict partial order on the marked vertices containing the arcs; the instance carries one because acyclicity is not first-order definable, so a first-order reduction could not test it. The instance is a yes-instance of DAG Isomorphism when it is finite, both witnesses are topological orders, and the two marked arc relations are isomorphic; the isomorphism is not required to respect the witnesses. DAG Isomorphism is the decision problem of the structures isomorphic to such an instance.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Semantics |
| 2 | import Lax904597.Problems |
| 3 | import Lax485149.Problems |
| 4 | import Lax604544.RelationIsomorphism |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Isomorphism of directed acyclic graphs |
| 9 | type: definition |
| 10 | --- |
| 11 | An instance is a pair of directed graphs on one universe, each with a mark |
| 12 | on its vertices, a relation of arcs and a further binary relation given as a |
| 13 | witness of acyclicity. That relation is a topological order of the arcs |
| 14 | when it is a strict partial order on the marked vertices containing the |
| 15 | arcs; the instance carries one because acyclicity is not first-order |
| 16 | definable, so a first-order reduction could not test it. The instance is a |
| 17 | yes-instance of DAG Isomorphism when it is finite, both witnesses are |
| 18 | topological orders, and the two marked arc relations are isomorphic; the |
| 19 | isomorphism is not required to respect the witnesses. DAG Isomorphism is the |
| 20 | decision problem of the structures isomorphic to such an instance. |
| 21 | -/ |
| 22 | |
| 23 | namespace Lax604544.DagIsomorphism |
| 24 | |
| 25 | open Lax904597.Problems Lax485149.Problems Lax604544.RelationIsomorphism |
| 26 | |
| 27 | open FirstOrder |
| 28 | |
| 29 | open FirstOrder.Language |
| 30 | |
| 31 | /-- The relation symbols of the language. -/ |
| 32 | inductive twoDagsRel : ℕ → Type where |
| 33 | /-- `patV a`: `a` is a vertex of the pattern DAG. -/ |
| 34 | | patV : twoDagsRel 1 |
| 35 | /-- `hostV a`: `a` is a vertex of the host DAG. -/ |
| 36 | | hostV : twoDagsRel 1 |
| 37 | /-- `patArc a b`: there is an arc of the pattern DAG from `a` to `b`. -/ |
| 38 | | patArc : twoDagsRel 2 |
| 39 | /-- `hostArc a b`: there is an arc of the host DAG from `a` to `b`. -/ |
| 40 | | hostArc : twoDagsRel 2 |
| 41 | /-- `patLt a b`: `a` precedes `b` in the pattern's topological order. -/ |
| 42 | | patLt : twoDagsRel 2 |
| 43 | /-- `hostLt a b`: `a` precedes `b` in the host's topological order. -/ |
| 44 | | hostLt : twoDagsRel 2 |
| 45 | deriving DecidableEq |
| 46 | |
| 47 | /-- The relational language of two directed acyclic graphs: two arc relations |
| 48 | sharing a universe, each with its own vertex mark and its own topological |
| 49 | order. -/ |
| 50 | def twoDags : FirstOrder.Language := |
| 51 | ⟨fun _ => Empty, twoDagsRel⟩ |
| 52 | |
| 53 | instance instIsRelationalTwoDags : FirstOrder.Language.IsRelational twoDags := fun _ => |
| 54 | (inferInstance : IsEmpty Empty) |
| 55 | |
| 56 | /-- `patV a`: `a` is a vertex of the pattern DAG. -/ |
| 57 | abbrev tdPatV : twoDags.Relations 1 := |
| 58 | .patV |
| 59 | |
| 60 | /-- `hostV a`: `a` is a vertex of the host DAG. -/ |
| 61 | abbrev tdHostV : twoDags.Relations 1 := |
| 62 | .hostV |
| 63 | |
| 64 | /-- `patArc a b`: there is an arc of the pattern DAG from `a` to `b`. -/ |
| 65 | abbrev tdPatArc : twoDags.Relations 2 := |
| 66 | .patArc |
| 67 | |
| 68 | /-- `hostArc a b`: there is an arc of the host DAG from `a` to `b`. -/ |
| 69 | abbrev tdHostArc : twoDags.Relations 2 := |
| 70 | .hostArc |
| 71 | |
| 72 | /-- `patLt a b`: `a` precedes `b` in the pattern's topological order. -/ |
| 73 | abbrev tdPatLt : twoDags.Relations 2 := |
| 74 | .patLt |
| 75 | |
| 76 | /-- `hostLt a b`: `a` precedes `b` in the host's topological order. -/ |
| 77 | abbrev tdHostLt : twoDags.Relations 2 := |
| 78 | .hostLt |
| 79 | |
| 80 | open FirstOrder |
| 81 | |
| 82 | open Language Structure |
| 83 | |
| 84 | section Topo |
| 85 | |
| 86 | variable {A : Type} |
| 87 | |
| 88 | /-- `Lt` is a topological order for the arcs `Arc` on the marked set `V`: a |
| 89 | strict partial order (on `V`) containing the arcs. Its existence is exactly the |
| 90 | acyclicity of the arcs, and it is first-order checkable, which acyclicity |
| 91 | itself is not. -/ |
| 92 | def TopoOn (V : A → Prop) (Lt Arc : A → A → Prop) : Prop := |
| 93 | (∀ x, V x → ¬Lt x x) ∧ |
| 94 | (∀ x y z, V x → V y → V z → Lt x y → Lt y z → Lt x z) ∧ |
| 95 | ∀ x y, V x → V y → Arc x y → Lt x y |
| 96 | |
| 97 | end Topo |
| 98 | |
| 99 | section Shorthands |
| 100 | |
| 101 | variable {A : Type} [twoDags.Structure A] |
| 102 | |
| 103 | /-- `patV a`: `a` is a vertex of the pattern DAG. -/ |
| 104 | def TDPatV {A : Type} [twoDags.Structure A] (a0 : A) : Prop := |
| 105 | FirstOrder.Language.Structure.RelMap tdPatV ![a0] |
| 106 | |
| 107 | /-- `hostV a`: `a` is a vertex of the host DAG. -/ |
| 108 | def TDHostV {A : Type} [twoDags.Structure A] (a0 : A) : Prop := |
| 109 | FirstOrder.Language.Structure.RelMap tdHostV ![a0] |
| 110 | |
| 111 | /-- `patArc a b`: there is an arc of the pattern DAG from `a` to `b`. -/ |
| 112 | def TDPatArc {A : Type} [twoDags.Structure A] (a0 : A) (a1 : A) : Prop := |
| 113 | FirstOrder.Language.Structure.RelMap tdPatArc ![a0, a1] |
| 114 | |
| 115 | /-- `hostArc a b`: there is an arc of the host DAG from `a` to `b`. -/ |
| 116 | def TDHostArc {A : Type} [twoDags.Structure A] (a0 : A) (a1 : A) : Prop := |
| 117 | FirstOrder.Language.Structure.RelMap tdHostArc ![a0, a1] |
| 118 | |
| 119 | /-- `patLt a b`: `a` precedes `b` in the pattern's topological order. -/ |
| 120 | def TDPatLt {A : Type} [twoDags.Structure A] (a0 : A) (a1 : A) : Prop := |
| 121 | FirstOrder.Language.Structure.RelMap tdPatLt ![a0, a1] |
| 122 | |
| 123 | /-- `hostLt a b`: `a` precedes `b` in the host's topological order. -/ |
| 124 | def TDHostLt {A : Type} [twoDags.Structure A] (a0 : A) (a1 : A) : Prop := |
| 125 | FirstOrder.Language.Structure.RelMap tdHostLt ![a0, a1] |
| 126 | |
| 127 | end Shorthands |
| 128 | |
| 129 | section Problem |
| 130 | |
| 131 | variable (A : Type) [twoDags.Structure A] |
| 132 | |
| 133 | /-- Both sides are well-formed – each order relation is a topological order of |
| 134 | its arcs, so both marked arc relations are acyclic – and the two DAGs are |
| 135 | isomorphic. The isomorphism relates the arcs only: the two orders are the |
| 136 | instance's acyclicity witnesses, not part of the structure being matched. -/ |
| 137 | def HasDagIso : Prop := |
| 138 | Finite A ∧ TopoOn (TDPatV (A := A)) TDPatLt TDPatArc ∧ |
| 139 | TopoOn (TDHostV (A := A)) TDHostLt TDHostArc ∧ |
| 140 | RelIsoOn (TDPatV (A := A)) TDHostV TDPatArc TDHostArc |
| 141 | |
| 142 | end Problem |
| 143 | |
| 144 | /-- DAG Isomorphism: are the two marked acyclic graphs of the instance, given |
| 145 | with topological orders, isomorphic? -/ |
| 146 | def DagIso : DecisionProblem twoDags := |
| 147 | DecisionProblem.ofPred fun A _ => HasDagIso A |
| 148 | |
| 149 | end Lax604544.DagIsomorphism |
| 150 |
Used by
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments