Graph isomorphism and the class GI
Lax604544.GraphIsomorphism · concepts/Lax604544/GraphIsomorphism.lean · lax-604544
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An instance is a pair of graphs on one universe, as for the subgraph isomorphism problem of the catalog of NP-complete problems: a structure with two unary marks, the vertices of the pattern and of the host, and two binary relations, their edges. It is a yes-instance of Digraph Isomorphism when it is finite and the two marked relations are isomorphic. It is a yes-instance of Graph Isomorphism when moreover both relations are simple graphs on their vertices, symmetric and irreflexive. Each problem is the decision problem of the structures isomorphic to such an instance.
GI is the degree of Graph Isomorphism: the class of the problems that reduce to it by an ordered first-order reduction. The degree is defined on the undirected problem, the one the literature calls GI.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Semantics |
| 2 | import Lax904597.Problems |
| 3 | import Lax485149.Problems |
| 4 | import Lax904597.Classes |
| 5 | import Lax799700.SubgraphIso |
| 6 | import Lax604544.RelationIsomorphism |
| 7 | import Lax604544.Degrees |
| 8 | |
| 9 | /-! |
| 10 | --- |
| 11 | title: Graph isomorphism and the class GI |
| 12 | type: definition |
| 13 | --- |
| 14 | An instance is a pair of graphs on one universe, as for the subgraph |
| 15 | isomorphism problem of the catalog of NP-complete problems: a structure |
| 16 | with two unary marks, the vertices of the pattern and of the host, and two |
| 17 | binary relations, their edges. It is a yes-instance of Digraph Isomorphism |
| 18 | when it is finite and the two marked relations are isomorphic. It is a |
| 19 | yes-instance of Graph Isomorphism when moreover both relations are simple |
| 20 | graphs on their vertices, symmetric and irreflexive. Each problem is the |
| 21 | decision problem of the structures isomorphic to such an instance. |
| 22 | |
| 23 | GI is the degree of Graph Isomorphism: the class of the problems that |
| 24 | reduce to it by an ordered first-order reduction. The degree is defined on |
| 25 | the undirected problem, the one the literature calls GI. |
| 26 | -/ |
| 27 | |
| 28 | namespace Lax604544.GraphIsomorphism |
| 29 | |
| 30 | open FirstOrder FirstOrder.Language |
| 31 | open Lax904597.Problems Lax904597.Classes Lax485149.Problems Lax799700.SubgraphIso |
| 32 | open Lax604544.RelationIsomorphism Lax604544.Degrees |
| 33 | |
| 34 | section Problem |
| 35 | |
| 36 | variable (A : Type) [twoGraphs.Structure A] |
| 37 | |
| 38 | /-- The two marked graphs of the instance are isomorphic. -/ |
| 39 | def HasDigraphIso : Prop := |
| 40 | Finite A ∧ RelIsoOn (TGPatV (A := A)) TGHostV TGPatE TGHostE |
| 41 | |
| 42 | end Problem |
| 43 | |
| 44 | section Generic |
| 45 | |
| 46 | variable {A : Type} |
| 47 | |
| 48 | /-- The relation `E` is symmetric and irreflexive on the marked set `V`: a |
| 49 | simple graph, as opposed to an arbitrary binary relation. -/ |
| 50 | def SimpleOn (V : A → Prop) (E : A → A → Prop) : Prop := |
| 51 | (∀ x y, V x → V y → E x y → E y x) ∧ ∀ x, V x → ¬E x x |
| 52 | |
| 53 | end Generic |
| 54 | |
| 55 | section Problem |
| 56 | |
| 57 | variable (A : Type) [twoGraphs.Structure A] |
| 58 | |
| 59 | /-- Both marked graphs are simple, and they are isomorphic. -/ |
| 60 | def HasGraphIso : Prop := |
| 61 | Finite A ∧ SimpleOn (TGPatV (A := A)) TGPatE ∧ SimpleOn (TGHostV (A := A)) TGHostE ∧ |
| 62 | RelIsoOn (TGPatV (A := A)) TGHostV TGPatE TGHostE |
| 63 | |
| 64 | end Problem |
| 65 | |
| 66 | /-- Digraph Isomorphism: are the two marked directed graphs of the instance |
| 67 | isomorphic? -/ |
| 68 | def DigraphIso : DecisionProblem twoGraphs := |
| 69 | DecisionProblem.ofPred fun A _ => HasDigraphIso A |
| 70 | |
| 71 | /-- Graph Isomorphism: are the two marked graphs simple and isomorphic? -/ |
| 72 | def GraphIso : DecisionProblem twoGraphs := |
| 73 | DecisionProblem.ofPred fun A _ => HasGraphIso A |
| 74 | |
| 75 | /-- **GI**: the degree of Graph Isomorphism. -/ |
| 76 | def GI : ComplexityClass := below GraphIso |
| 77 | |
| 78 | end Lax604544.GraphIsomorphism |
| 79 |
Builds on
Used by
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments