DAG Isomorphism: vocabulary and semantics

DAG ISOMORPHISM: are the two directed acyclic graphs of the instance isomorphic? This file fixes the vocabulary and the yes-instance predicate; the two halves of GI-completeness live in DescriptiveComplexity.Problems.DagIso.ToDigraphIso and DescriptiveComplexity.Problems.DagIso.FromDigraphIso.

Why the instances carry a topological order

Acyclicity is not first-order definable, so a problem whose yes-instances are “both sides acyclic and isomorphic” could not be reduced back to DescriptiveComplexity.DigraphIso: the reduction would have to decide acyclicity first-order, and no first-order interpretation can (a directed cycle is a reachability question). A classical polynomial-time reduction simply tests acyclicity and maps a cyclic instance to a fixed no-instance; an FO reduction, computable in AC⁰, cannot.

The instances therefore carry their acyclicity witness: besides the two arc relations, each side has a relation asked to be a strict partial order containing its arcs (DescriptiveComplexity.TopoOn) – a topological order of the DAG, in the partial-order form, which is exactly what DescriptiveComplexity.acyclicRel_iff_exists_order certifies acyclicity by. Being a strict partial order containing the arcs is first-order, so a reduction can test it, and the well-formed instances are precisely the pairs of DAGs (DescriptiveComplexity.acyclicOn_iff_exists_topoOn: a finite relation admits such a witness exactly when it is acyclic). The witness is data of the instance, not of the problem: the isomorphism asked for by DescriptiveComplexity.HasDagIso relates the arcs only and may ignore the two orders entirely, so this is DAG isomorphism and not isomorphism of ordered DAGs.

This is the same “junk is ignorable” discipline as everywhere in the catalog, one level up: elements outside both marks are junk, and instances whose order relation is not a witness are no-instances.

@[reducible, inline]

abbrev FirstOrder.Language.tdHostV : Language.twoDags.Relations 1

hostV a: a is a vertex of the host DAG.

Equations

• FirstOrder.Language.tdHostV = FirstOrder.Language.twoDagsRel.hostV

def FirstOrder.Language.instDecidableEqTwoDagsRel.decEq {a✝ : ℕ} (x✝ x✝¹ : twoDagsRel a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.instDecidableEqTwoDagsRel.decEq FirstOrder.Language.twoDagsRel.patV FirstOrder.Language.twoDagsRel.patV = isTrue FirstOrder.Language.instDecidableEqTwoDagsRel.decEq._proof_1

@[reducible, inline]

abbrev FirstOrder.Language.tdPatV : Language.twoDags.Relations 1

patV a: a is a vertex of the pattern DAG.

Equations

• FirstOrder.Language.tdPatV = FirstOrder.Language.twoDagsRel.patV

@[reducible, inline]

abbrev FirstOrder.Language.tdPatLt : Language.twoDags.Relations 2

patLt a b: a precedes b in the pattern's topological order.

Equations

• FirstOrder.Language.tdPatLt = FirstOrder.Language.twoDagsRel.patLt

def FirstOrder.Language.twoDags : Language

The relational language of two directed acyclic graphs: two arc relations sharing a universe, each with its own vertex mark and its own topological order.

Equations

• FirstOrder.Language.twoDags = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.twoDagsRel }

instance FirstOrder.Language.instIsRelationalTwoDags : Language.twoDags.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.tdPatArc : Language.twoDags.Relations 2

patArc a b: there is an arc of the pattern DAG from a to b.

Equations

• FirstOrder.Language.tdPatArc = FirstOrder.Language.twoDagsRel.patArc

@[reducible, inline]

abbrev FirstOrder.Language.tdHostLt : Language.twoDags.Relations 2

hostLt a b: a precedes b in the host's topological order.

Equations

• FirstOrder.Language.tdHostLt = FirstOrder.Language.twoDagsRel.hostLt

inductive FirstOrder.Language.twoDagsRel : ℕ → Type

The relation symbols of the language.

• patV : twoDagsRel 1

  patV a: a is a vertex of the pattern DAG.

• hostV : twoDagsRel 1

  hostV a: a is a vertex of the host DAG.

• patArc : twoDagsRel 2

  patArc a b: there is an arc of the pattern DAG from a to b.

• hostArc : twoDagsRel 2

  hostArc a b: there is an arc of the host DAG from a to b.

• patLt : twoDagsRel 2

  patLt a b: a precedes b in the pattern's topological order.

• hostLt : twoDagsRel 2

  hostLt a b: a precedes b in the host's topological order.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqTwoDagsRel {a✝ : ℕ} : DecidableEq (twoDagsRel a✝)

Equations

• FirstOrder.Language.instDecidableEqTwoDagsRel = FirstOrder.Language.instDecidableEqTwoDagsRel.decEq

@[reducible, inline]

abbrev FirstOrder.Language.tdHostArc : Language.twoDags.Relations 2

hostArc a b: there is an arc of the host DAG from a to b.

Equations

• FirstOrder.Language.tdHostArc = FirstOrder.Language.twoDagsRel.hostArc

The acyclicity witness

def DescriptiveComplexity.TopoOn {A : Type} (V : A → Prop) (Lt Arc : A → A → Prop) : Prop

Lt is a topological order for the arcs Arc on the marked set V: a strict partial order (on V) containing the arcs. Its existence is exactly the acyclicity of the arcs (DescriptiveComplexity.acyclicOn_iff_exists_topoOn), and it is first-order checkable, which acyclicity itself is not.

Equations

• DescriptiveComplexity.TopoOn V Lt Arc = ((∀ (x : A), V x → ¬Lt x x) ∧ (∀ (x y z : A), V x → V y → V z → Lt x y → Lt y z → Lt x z) ∧ ∀ (x y : A), V x → V y → Arc x y → Lt x y)

theorem DescriptiveComplexity.TopoOn.of_equiv {A B : Type} (u : B ≃ A) {VB : B → Prop} {LtB ArcB : B → B → Prop} {VA : A → Prop} {LtA ArcA : A → A → Prop} (hV : ∀ (b : B), VB b ↔ VA (u b)) (hLt : ∀ (b b' : B), LtB b b' ↔ LtA (u b) (u b')) (hArc : ∀ (b b' : B), ArcB b b' ↔ ArcA (u b) (u b')) (h : TopoOn VB LtB ArcB) : TopoOn VA LtA ArcA

TopoOn transports along an equivalence commuting with the three predicates.

theorem DescriptiveComplexity.TopoOn.equiv_iff {A B : Type} (u : B ≃ A) {VB : B → Prop} {LtB ArcB : B → B → Prop} {VA : A → Prop} {LtA ArcA : A → A → Prop} (hV : ∀ (b : B), VB b ↔ VA (u b)) (hLt : ∀ (b b' : B), LtB b b' ↔ LtA (u b) (u b')) (hArc : ∀ (b b' : B), ArcB b b' ↔ ArcA (u b) (u b')) : TopoOn VB LtB ArcB ↔ TopoOn VA LtA ArcA

TopoOn transports along an equivalence, iff version.

theorem DescriptiveComplexity.acyclicOn_iff_exists_topoOn {A : Type} (V : A → Prop) (Arc : A → A → Prop) : (AcyclicRel fun (x y : { x : A // V x }) => Arc ↑x ↑y) ↔ ∃ (Lt : A → A → Prop), TopoOn V Lt Arc

The well-formed instances are exactly the DAGs: the arcs of a marked set admit a topological order precisely when they are acyclic on it. Left to right a cycle would give Lt x x; right to left the transitive closure is the order (DescriptiveComplexity.acyclicRel_iff_exists_order, on the subtype of marked elements).

This is why carrying the witness costs no generality: every DAG is a yes-instance-shaped instance, and no other structure is.

The problem

def DescriptiveComplexity.TDHostArc {A : Type} [FirstOrder.Language.twoDags.Structure A] (a0 a1 : A) : Prop

hostArc a b: there is an arc of the host DAG from a to b.

Equations

• DescriptiveComplexity.TDHostArc a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tdHostArc ![a0, a1]

def DescriptiveComplexity.TDHostV {A : Type} [FirstOrder.Language.twoDags.Structure A] (a0 : A) : Prop

hostV a: a is a vertex of the host DAG.

Equations

• DescriptiveComplexity.TDHostV a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tdHostV ![a0]

def DescriptiveComplexity.TDPatArc {A : Type} [FirstOrder.Language.twoDags.Structure A] (a0 a1 : A) : Prop

patArc a b: there is an arc of the pattern DAG from a to b.

Equations

• DescriptiveComplexity.TDPatArc a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tdPatArc ![a0, a1]

def DescriptiveComplexity.TDPatV {A : Type} [FirstOrder.Language.twoDags.Structure A] (a0 : A) : Prop

patV a: a is a vertex of the pattern DAG.

Equations

• DescriptiveComplexity.TDPatV a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tdPatV ![a0]

def DescriptiveComplexity.TDHostLt {A : Type} [FirstOrder.Language.twoDags.Structure A] (a0 a1 : A) : Prop

hostLt a b: a precedes b in the host's topological order.

Equations

• DescriptiveComplexity.TDHostLt a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tdHostLt ![a0, a1]

def DescriptiveComplexity.TDPatLt {A : Type} [FirstOrder.Language.twoDags.Structure A] (a0 a1 : A) : Prop

patLt a b: a precedes b in the pattern's topological order.

Equations

• DescriptiveComplexity.TDPatLt a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.tdPatLt ![a0, a1]

def DescriptiveComplexity.HasDagIso (A : Type) [FirstOrder.Language.twoDags.Structure A] : Prop

Both sides are well-formed – each order relation is a topological order of its arcs, so both marked arc relations are acyclic – and the two DAGs are isomorphic. The isomorphism relates the arcs only: the two orders are the instance's acyclicity witnesses, not part of the structure being matched.

Equations

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

theorem DescriptiveComplexity.hasDagIso_iso {A B : Type} [FirstOrder.Language.twoDags.Structure A] [FirstOrder.Language.twoDags.Structure B] (e : FirstOrder.Language.twoDags.Equiv A B) : HasDagIso A ↔ HasDagIso B

The DAG-isomorphism property is isomorphism-invariant.

def DescriptiveComplexity.DagIso : DecisionProblem FirstOrder.Language.twoDags

DAG ISOMORPHISM, as a problem on two-DAG structures: are the two marked DAGs isomorphic? Well-formedness – each side's order relation being a topological order of its arcs – is part of the yes-condition, and is first-order, unlike acyclicity itself.

Equations

• DescriptiveComplexity.DagIso = { Holds := fun (A : Type) (inst : FirstOrder.Language.twoDags.Structure A) => DescriptiveComplexity.HasDagIso A, iso_invariant := ⋯ }