DAG Isomorphism reduces to Digraph Isomorphism

The easy half of GI-completeness, and the half that pays for the design of DescriptiveComplexity.Problems.DagIso.Defs: since FirstOrder.Language.twoGraphs carries two arbitrary binary relations – nothing asks them to be symmetric – DescriptiveComplexity.DigraphIso is already isomorphism of two directed graphs, so a DAG instance only has to forget its two topological orders.

What it may not forget is well-formedness. The reduction is a one-dimensional, single-tag interpretation that first tests, first-order, that both order relations really are topological orders of their arcs (DescriptiveComplexity.TopoOn, the sentence DescriptiveComplexity.DagIso.topoSentence): if the test passes it copies the two marked arc relations over, and if it fails it emits a pattern with no vertices facing a host with all of them – no bijection, hence a no-instance, matching the no-instance the ill-formed input is. This test is the whole reason the instances carry their acyclicity witness: acyclicity itself is not first-order, so no interpretation could gate on it.

The well-formedness sentence

noncomputable def DescriptiveComplexity.DagIso.topoIrreflClause {α : Type} (V : FirstOrder.Language.twoDags.Relations 1) (Lt : FirstOrder.Language.twoDags.Relations 2) : FirstOrder.Language.twoDags.Formula α

Lt is a topological order of Arc on V, as a first-order sentence (over any variable type, so that it can be conjoined inside the defining formulas of an interpretation): irreflexive and transitive on the marked set, and containing the arcs.

Equations

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

noncomputable def DescriptiveComplexity.DagIso.topoTransClause {α : Type} (V : FirstOrder.Language.twoDags.Relations 1) (Lt : FirstOrder.Language.twoDags.Relations 2) : FirstOrder.Language.twoDags.Formula α

Lt is a topological order of Arc on V, as a first-order sentence (over any variable type, so that it can be conjoined inside the defining formulas of an interpretation): irreflexive and transitive on the marked set, and containing the arcs.

Equations

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

noncomputable def DescriptiveComplexity.DagIso.topoMonoClause {α : Type} (V : FirstOrder.Language.twoDags.Relations 1) (Lt Arc : FirstOrder.Language.twoDags.Relations 2) : FirstOrder.Language.twoDags.Formula α

Lt is a topological order of Arc on V, as a first-order sentence (over any variable type, so that it can be conjoined inside the defining formulas of an interpretation): irreflexive and transitive on the marked set, and containing the arcs.

Equations

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

noncomputable def DescriptiveComplexity.DagIso.topoSentence {α : Type} (V : FirstOrder.Language.twoDags.Relations 1) (Lt Arc : FirstOrder.Language.twoDags.Relations 2) : FirstOrder.Language.twoDags.Formula α

Lt is a topological order of Arc on V, as a first-order sentence (over any variable type, so that it can be conjoined inside the defining formulas of an interpretation): irreflexive and transitive on the marked set, and containing the arcs.

Equations

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

noncomputable def DescriptiveComplexity.DagIso.wfSentence {α : Type} : FirstOrder.Language.twoDags.Formula α

Both sides of the instance are well formed.

Equations

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

The interpretation

noncomputable def DescriptiveComplexity.DagIso.dagInterp : FOInterpretation FirstOrder.Language.twoDags FirstOrder.Language.twoGraphs Unit 1

The interpretation of DAG Isomorphism into Digraph Isomorphism: one dimension, one tag. If the instance is well formed, the two marked arc relations are copied verbatim – FirstOrder.Language.twoGraphs holds arbitrary binary relations, so a DAG needs no encoding. If it is not, the pattern is emptied while the host keeps every element, so the two sides cannot be isomorphic.

Equations

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

What the interpretation realizes

Correctness