Subgraph Isomorphism on concrete graphs: encoding and decoding

DescriptiveComplexity.SubgraphIso is a problem on FirstOrder.Language.twoGraphs-structures. A user starts from two concrete graphs – a pattern on p vertices and a host on h vertices, each a finite set of directed edges – and the textbook question, DescriptiveComplexity.ConcreteSubgraphIsoHolds: is there an injective map from the pattern's vertices to the host's carrying every edge of the pattern to an edge of the host? This file ties the two together in both directions, with the machinery of DescriptiveComplexity.Encoding and DescriptiveComplexity.Decoding, the way the two tutorials (DescriptiveComplexity.Examples.ConjunctiveQueries, DescriptiveComplexity.Examples.GraphCrawling) do for their domains.

• DescriptiveComplexity.subgraphIsoEncoding: the pattern's vertices to the left of a sum, the host's to the right, the marks reading the side and the two adjacency relations reading the two edge sets. The size bounds are discharged at construction: the universe is the vertex set, and an edge set has at most quadratically many elements.
• DescriptiveComplexity.subgraphIsoEncoding_faithful: the abstract problem computes the textbook one on every encoded instance.
• DescriptiveComplexity.subgraphIsoDecoding: the decoder, which needs no well-formedness condition. The semantics of SubgraphIso ignores the elements in neither mark, and never relates the pattern role and the host role of one element – the guessed map sends pattern vertices to host vertices, and a vertex may be its own image – so a structure marking an element as both is the same instance as one where that element is split in two. The decoder therefore reads every presented structure back: pattern vertices are the pattern-marked elements, host vertices the host-marked ones, each enumerated in order, and the edges are read off the tables. Contrast the crawling tutorial, where the decoder exists only on single-root websites, and compare DescriptiveComplexity.bwDecoding, the other decoder of the library whose condition is ⊤.

Both directions go through one lemma, DescriptiveComplexity.subgraphIsoOn_iff_concrete: against an enumeration of the pattern vertices and one of the host vertices, the generic property DescriptiveComplexity.SubgraphIsoOn is the textbook predicate. The encoding enumerates them by the two injections of the sum, the decoding by Finset.orderIsoOfFin on the two marked sets.

The concrete problem

structure DescriptiveComplexity.SubgraphIsoInstance : Type

A concrete instance of Subgraph Isomorphism: a pattern graph on Fin pat and a host graph on Fin host, each given by its set of directed edges.

• pat : ℕ

  The number of pattern vertices.

• host : ℕ

  The number of host vertices.

• patEdges : Finset (Fin self.pat × Fin self.pat)

  The edges of the pattern.

• hostEdges : Finset (Fin self.host × Fin self.host)

  The edges of the host.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqSubgraphIsoInstance : DecidableEq SubgraphIsoInstance

Equations

• DescriptiveComplexity.instDecidableEqSubgraphIsoInstance = DescriptiveComplexity.instDecidableEqSubgraphIsoInstance.decEq

def DescriptiveComplexity.instDecidableEqSubgraphIsoInstance.decEq (x✝ x✝¹ : SubgraphIsoInstance) : Decidable (x✝ = x✝¹)

Equations

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

def DescriptiveComplexity.sgSize (i : SubgraphIsoInstance) : ℕ

The textbook size of a concrete instance: vertices and edges of both graphs. The one audited line of the encoding.

Equations

• DescriptiveComplexity.sgSize i = i.pat + i.host + i.patEdges.card + i.hostEdges.card

def DescriptiveComplexity.ConcreteSubgraphIsoHolds (i : SubgraphIsoInstance) : Prop

The textbook semantics of a concrete instance: an injective map from the pattern's vertices to the host's carrying every edge of the pattern to an edge of the host.

Equations

• DescriptiveComplexity.ConcreteSubgraphIsoHolds i = ∃ (f : Fin i.pat → Fin i.host), Function.Injective f ∧ ∀ (a b : Fin i.pat), (a, b) ∈ i.patEdges → (f a, f b) ∈ i.hostEdges

The generic property, against enumerations of the two vertex sets

theorem DescriptiveComplexity.subgraphIsoOn_iff_subtype {A : Type} (PV HV : A → Prop) (PE HE : A → A → Prop) : SubgraphIsoOn PV HV PE HE ↔ ∃ (f : { x : A // PV x } → { y : A // HV y }), Function.Injective f ∧ ∀ (x y : { x : A // PV x }), PE ↑x ↑y → HE ↑(f x) ↑(f y)

SubgraphIsoOn as an injective map between the two subtypes: the guessed map of the definition, restricted to the pattern, and back.

theorem DescriptiveComplexity.subgraphIsoOn_iff_concrete {A : Type} (i : SubgraphIsoInstance) (PV HV : A → Prop) (PE HE : A → A → Prop) (eP : Fin i.pat ≃ { x : A // PV x }) (eH : Fin i.host ≃ { y : A // HV y }) (hEP : ∀ (a b : Fin i.pat), (a, b) ∈ i.patEdges ↔ PE ↑(eP a) ↑(eP b)) (hEH : ∀ (a b : Fin i.host), (a, b) ∈ i.hostEdges ↔ HE ↑(eH a) ↑(eH b)) : ConcreteSubgraphIsoHolds i ↔ SubgraphIsoOn PV HV PE HE

The generic property is the textbook predicate, once the pattern and host vertices are enumerated (eP, eH) and the two edge sets are read through the enumerations (hEP, hEH). The encoding and the decoding below each supply one pair of enumerations.

The encoding

def DescriptiveComplexity.sgRelBool (i : SubgraphIsoInstance) {n : ℕ} (R : FirstOrder.Language.twoGraphs.Relations n) : (Fin n → Fin i.pat ⊕ Fin i.host) → Bool

The encoder, standalone and auditable: a plain def, so the compiler vouches that it computes. Pattern vertices are the left injections, host vertices the right ones, and the two adjacency relations decide membership in the two edge sets on their own side.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.sgRelBool i FirstOrder.Language.twoGraphsRel.patV = fun (x : Fin 1 → Fin i.pat ⊕ Fin i.host) => (x 0).isLeft
• DescriptiveComplexity.sgRelBool i FirstOrder.Language.twoGraphsRel.hostV = fun (x : Fin 1 → Fin i.pat ⊕ Fin i.host) => (x 0).isRight

def DescriptiveComplexity.subgraphIsoEncoding : Encoding FirstOrder.Language.twoGraphs SubgraphIsoInstance

The encoding of concrete instances by Language.twoGraphs-structures: universe Fin pat ⊕ Fin host, relations by sgRelBool. The universe is the vertex set, so nothing is padded, and an edge set has at most quadratically many elements, so nothing is compressed.

Equations

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

theorem DescriptiveComplexity.sgEnc_patV (i : SubgraphIsoInstance) (x : subgraphIsoEncoding.Univ i) : TGPatV x ↔ Sum.isLeft x = true

On an encoded instance, being a pattern vertex is being a left injection.

theorem DescriptiveComplexity.sgEnc_hostV (i : SubgraphIsoInstance) (x : subgraphIsoEncoding.Univ i) : TGHostV x ↔ Sum.isRight x = true

On an encoded instance, being a host vertex is being a right injection.

theorem DescriptiveComplexity.sgEnc_patE (i : SubgraphIsoInstance) (a b : Fin i.pat) : TGPatE (Sum.inl a) (Sum.inl b) ↔ (a, b) ∈ i.patEdges

Pattern adjacency on an encoded instance, at two left injections.

theorem DescriptiveComplexity.sgEnc_hostE (i : SubgraphIsoInstance) (a b : Fin i.host) : TGHostE (Sum.inr a) (Sum.inr b) ↔ (a, b) ∈ i.hostEdges

Host adjacency on an encoded instance, at two right injections.

def DescriptiveComplexity.sgEncPatEquiv (i : SubgraphIsoInstance) : Fin i.pat ≃ { x : subgraphIsoEncoding.Univ i // TGPatV x }

The pattern vertices of an encoded instance, enumerated by the left injection.

Equations

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

def DescriptiveComplexity.sgEncHostEquiv (i : SubgraphIsoInstance) : Fin i.host ≃ { y : subgraphIsoEncoding.Univ i // TGHostV y }

The host vertices of an encoded instance, enumerated by the right injection.

Equations

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

theorem DescriptiveComplexity.subgraphIsoEncoding_faithful : subgraphIsoEncoding.Faithful ConcreteSubgraphIsoHolds SubgraphIso

The encoding is faithful: SubgraphIso computes the textbook predicate on every encoded instance.

A worked instance, run

def DescriptiveComplexity.sgExample : SubgraphIsoInstance

A concrete instance: the directed triangle as pattern, the complete directed graph on four vertices as host.

Equations

• DescriptiveComplexity.sgExample = { pat := 3, host := 4, patEdges := {(0, 1), (1, 2), (2, 0)}, hostEdges := {q : Fin 4 × Fin 4 | q.1 ≠ q.2} }

The decoding

def DescriptiveComplexity.sgPatVs (S : FinPresentation FirstOrder.Language.twoGraphs) : Finset (Fin S.card)

The pattern vertices of a presented structure.

Equations

• DescriptiveComplexity.sgPatVs S = {x : Fin S.card | S.relBool FirstOrder.Language.tgPatV ![x] = true}

def DescriptiveComplexity.sgHostVs (S : FinPresentation FirstOrder.Language.twoGraphs) : Finset (Fin S.card)

The host vertices of a presented structure.

Equations

• DescriptiveComplexity.sgHostVs S = {x : Fin S.card | S.relBool FirstOrder.Language.tgHostV ![x] = true}

theorem DescriptiveComplexity.mem_sgPatVs (S : FinPresentation FirstOrder.Language.twoGraphs) (x : Fin S.card) : x ∈ sgPatVs S ↔ TGPatV x

theorem DescriptiveComplexity.mem_sgHostVs (S : FinPresentation FirstOrder.Language.twoGraphs) (x : Fin S.card) : x ∈ sgHostVs S ↔ TGHostV x

def DescriptiveComplexity.sgDecode (S : FinPresentation FirstOrder.Language.twoGraphs) : Option SubgraphIsoInstance

The decoder: enumerate the pattern vertices and the host vertices, in order, and read the two edge sets off the tables through the enumerations. Total: every presented structure is an instance.

Equations

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

noncomputable def DescriptiveComplexity.sgDecPatEquiv (S : FinPresentation FirstOrder.Language.twoGraphs) : Fin (sgPatVs S).card ≃ { x : Fin S.card // TGPatV x }

The pattern vertices of a presented structure, enumerated in order.

Equations

• DescriptiveComplexity.sgDecPatEquiv S = ((DescriptiveComplexity.sgPatVs S).orderIsoOfFin ⋯).trans (Equiv.subtypeEquivRight ⋯)

noncomputable def DescriptiveComplexity.sgDecHostEquiv (S : FinPresentation FirstOrder.Language.twoGraphs) : Fin (sgHostVs S).card ≃ { y : Fin S.card // TGHostV y }

The host vertices of a presented structure, enumerated in order.

Equations

• DescriptiveComplexity.sgDecHostEquiv S = ((DescriptiveComplexity.sgHostVs S).orderIsoOfFin ⋯).trans (Equiv.subtypeEquivRight ⋯)

theorem DescriptiveComplexity.sgDecode_sound (S : FinPresentation FirstOrder.Language.twoGraphs) (i : SubgraphIsoInstance) (hi : i ∈ sgDecode S) : ConcreteSubgraphIsoHolds i ↔ SubgraphIso.Holds (Fin S.card)

theorem DescriptiveComplexity.sgDecode_total (S : FinPresentation FirstOrder.Language.twoGraphs) (_hpos : 0 < S.card) (_hW : (DecisionProblem.ofSentence ⊤).Holds (Fin S.card)) : (sgDecode S).isSome = true

def DescriptiveComplexity.subgraphIsoDecoding : Decoding FirstOrder.Language.twoGraphs (DecisionProblem.ofSentence ⊤) ConcreteSubgraphIsoHolds SubgraphIso

The computable decoding of presented structures, with no well-formedness condition. Together with subgraphIsoEncoding_faithful it closes the loop: encoded instances are equidecided, and every nonempty finite structure decodes to an equidecided concrete instance, so SubgraphIso is nowhere hard only on junk.

Equations

• DescriptiveComplexity.subgraphIsoDecoding = { dec := DescriptiveComplexity.sgDecode, sound := DescriptiveComplexity.sgDecode_sound, total := DescriptiveComplexity.sgDecode_total }

def DescriptiveComplexity.sgPres : FinPresentation FirstOrder.Language.twoGraphs

A presented four-element structure: element 0 a pattern vertex, 1 and 2 host vertices, 3 in both roles, with the pattern edge 0 → 3 and the host edges 3 → 1 and 1 → 2. The decoder runs on it: the pattern has two vertices and one edge, the host three vertices and two edges.

Equations

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

theorem DescriptiveComplexity.exists_concreteSubgraphIso_iff (A : Type) [FirstOrder.Language.twoGraphs.Structure A] [Finite A] [Nonempty A] : ∃ (i : SubgraphIsoInstance), ConcreteSubgraphIsoHolds i ↔ SubgraphIso.Holds A

Hardness reads back to concrete data: every nonempty finite twoGraphs-structure is decided by SubgraphIso exactly as some pair of concrete graphs is by the textbook predicate.