Documentation

DescriptiveComplexity.Problems.DigraphIso.Bridge

Digraph Isomorphism is the generic isomorphism problem of the graph vocabulary #

DescriptiveComplexity.DigraphIso was stated over the hand-rolled FirstOrder.Language.twoGraphs before the generic FirstOrder.Language.twoCopies existed. The two vocabularies are the same up to renaming – patV/patE against the pattern mark and the pattern copy of adj – and this file proves the problems are FO-interreducible, in both directions, by the interpretation that renames the symbols.

The payoff is DescriptiveComplexity.below_digraphIso_eq_below_twoCopiesIso: the degree of DescriptiveComplexity.DigraphIso is the degree of DescriptiveComplexity.TwoCopiesIso FirstOrder.Language.graph, and hence the GI degree. A problem stated over twoCopies – as every entry added from here on is meant to be – therefore reaches the degree through DescriptiveComplexity.isoReflecting_fo_reduction and this bridge, with no further vocabulary bookkeeping.

Renaming the hand-rolled vocabulary to the generic one #

source
def DescriptiveComplexity.DigraphBridge.toTC :
FOInterpretation FirstOrder.Language.twoGraphs FirstOrder.Language.graph.twoCopies Unit 1

The interpretation renaming twoGraphs to twoCopies graph: one tag, one dimension, each symbol to its counterpart.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    def DescriptiveComplexity.DigraphBridge.ofTC :
    FOInterpretation FirstOrder.Language.graph.twoCopies FirstOrder.Language.twoGraphs Unit 1

    The interpretation renaming twoCopies graph back to twoGraphs.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph

      The one-dimensional universe #

      What the renamings realize #

      The generic side condition, as a relation isomorphism #

      Correctness of the two renamings #

      source
      theorem DescriptiveComplexity.DigraphBridge.toTC_correct (A : Type) [FirstOrder.Language.twoGraphs.Structure A] [Finite A] :
      DigraphIso.Holds A ↔ (TwoCopiesIso FirstOrder.Language.graph).Holds (toTC.Map A)

      Going to the generic vocabulary preserves the answer.

      Dependency graph
      source
      theorem DescriptiveComplexity.DigraphBridge.ofTC_correct (A : Type) [FirstOrder.Language.graph.twoCopies.Structure A] [Finite A] :
      (TwoCopiesIso FirstOrder.Language.graph).Holds A ↔ DigraphIso.Holds (ofTC.Map A)

      Coming back preserves the answer.

      Dependency graph

      The two reductions, and the degree #

      source
      def DescriptiveComplexity.digraphIso_fo_reduction_twoCopiesIso :
      FOReduction DigraphIso (TwoCopiesIso FirstOrder.Language.graph)

      Digraph Isomorphism reduces to the generic isomorphism problem of the graph vocabulary, by renaming the symbols.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Dependency graph
        source
        def DescriptiveComplexity.twoCopiesIso_fo_reduction_digraphIso :
        FOReduction (TwoCopiesIso FirstOrder.Language.graph) DigraphIso

        And back.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Dependency graph
          source
          theorem DescriptiveComplexity.below_digraphIso_eq_below_twoCopiesIso :
          ComplexityClass.below DigraphIso = ComplexityClass.below (TwoCopiesIso FirstOrder.Language.graph)

          Digraph Isomorphism and the generic isomorphism problem of the graph vocabulary have the same degree. A problem stated over twoCopies reaches the GI degree through this equality, so DescriptiveComplexity.isoReflecting_fo_reduction – a gadget on single structures – is all a new entry needs.

          Dependency graph