Hamilton circuits: definitions

DIRECTED HAMILTON CIRCUIT and (undirected) HAMILTON CIRCUIT (Karp 1972): does a graph have a circuit visiting every vertex exactly once? Both live on the same vocabulary FirstOrder.Language.digraph, a single binary relation arc; the undirected problem reads that relation symmetrically (DescriptiveComplexity.DGEdge), which is the honest reading of an undirected graph presented by a possibly asymmetric edge relation.

A circuit is a linear order

A Hamilton circuit is a cyclic enumeration of the universe, and cutting it anywhere turns it into a linear order whose consecutive elements are adjacent and whose last element is adjacent to its first (DescriptiveComplexity.TourOn). That reading is what makes the problem Σ₁: a relation is what an existential second-order block can guess, and “being a linear order”, “being the immediate successor” and the two adjacency demands are first-order. It is the same device the job-sequencing certificate uses for its schedule, one dimension down: there the order is a sequence of the universe, here it is a cycle of it.

On the empty universe every condition is vacuous, so the empty graph counts as a yes-instance; on a one-element universe the wrap-around demand becomes a self-loop, which is the usual convention.

inductive FirstOrder.Language.digraphRel : ℕ → Type

Relation symbols of the language of digraphs.

• arc : digraphRel 2

  arc a b: there is an arc from a to b.

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

Equations

• FirstOrder.Language.instDecidableEqDigraphRel.decEq FirstOrder.Language.digraphRel.arc FirstOrder.Language.digraphRel.arc = isTrue FirstOrder.Language.instDecidableEqDigraphRel.decEq._proof_1

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqDigraphRel {a✝ : ℕ} : DecidableEq (digraphRel a✝)

Equations

• FirstOrder.Language.instDecidableEqDigraphRel = FirstOrder.Language.instDecidableEqDigraphRel.decEq

def FirstOrder.Language.digraph : Language

The relational language of digraphs: one binary relation. The undirected problem reads it symmetrically rather than on a vocabulary of its own.

Equations

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

instance FirstOrder.Language.instIsRelationalDigraph : Language.digraph.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.dgArc : Language.digraph.Relations 2

The arc symbol of digraphs.

Equations

• FirstOrder.Language.dgArc = FirstOrder.Language.digraphRel.arc

Tours of a relation

def DescriptiveComplexity.SuccOf {A : Type} (Le : A → A → Prop) (x y : A) : Prop

y is the immediate Le-successor of x: above it, distinct from it, and with nothing strictly in between.

Equations

• DescriptiveComplexity.SuccOf Le x y = (Le x y ∧ x ≠ y ∧ ∀ (z : A), Le x z → Le z y → z = x ∨ z = y)

def DescriptiveComplexity.TourOn {A : Type} (R : A → A → Prop) : Prop

A tour of a relation: a linear order of the universe whose consecutive elements are related and whose last element is related to its first. On a finite universe this is exactly a Hamilton circuit, cut open at one place.

Equations

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

theorem DescriptiveComplexity.succOf_equiv {A B : Type} (u : A ≃ B) {Le : A → A → Prop} {x y : A} : SuccOf (fun (b b' : B) => Le (u.symm b) (u.symm b')) (u x) (u y) ↔ SuccOf Le x y

Being the immediate successor transports along an equivalence.

theorem DescriptiveComplexity.tourOn_of_equiv {A B : Type} (u : A ≃ B) {RA : A → A → Prop} {RB : B → B → Prop} (hR : ∀ (a a' : A), RA a a' ↔ RB (u a) (u a')) (h : TourOn RA) : TourOn RB

Having a tour transports along an equivalence commuting with the two relations.

The two problems

def DescriptiveComplexity.DGArc {A : Type} [FirstOrder.Language.digraph.Structure A] (a b : A) : Prop

There is an arc from a to b.

Equations

• DescriptiveComplexity.DGArc a b = FirstOrder.Language.Structure.RelMap FirstOrder.Language.dgArc ![a, b]

def DescriptiveComplexity.DGEdge {A : Type} [FirstOrder.Language.digraph.Structure A] (a b : A) : Prop

There is an edge between a and b: the arc relation read symmetrically, which is how the undirected problem reads its instance.

Equations

• DescriptiveComplexity.DGEdge a b = (DescriptiveComplexity.DGArc a b ∨ DescriptiveComplexity.DGArc b a)

def DescriptiveComplexity.HasDirHamCircuit (A : Type) [FirstOrder.Language.digraph.Structure A] : Prop

A digraph is a yes-instance of DIRECTED HAMILTON CIRCUIT when its arcs carry a tour of the universe.

Equations

• DescriptiveComplexity.HasDirHamCircuit A = (Finite A ∧ DescriptiveComplexity.TourOn DescriptiveComplexity.DGArc)

def DescriptiveComplexity.HasHamCircuit (A : Type) [FirstOrder.Language.digraph.Structure A] : Prop

A graph is a yes-instance of HAMILTON CIRCUIT when its edges – the arcs read symmetrically – carry a tour of the universe.

Equations

• DescriptiveComplexity.HasHamCircuit A = (Finite A ∧ DescriptiveComplexity.TourOn DescriptiveComplexity.DGEdge)

theorem DescriptiveComplexity.hasDirHamCircuit_iso {A B : Type} [FirstOrder.Language.digraph.Structure A] [FirstOrder.Language.digraph.Structure B] (e : FirstOrder.Language.digraph.Equiv A B) : HasDirHamCircuit A ↔ HasDirHamCircuit B

Having a directed Hamilton circuit is isomorphism-invariant.

theorem DescriptiveComplexity.hasHamCircuit_iso {A B : Type} [FirstOrder.Language.digraph.Structure A] [FirstOrder.Language.digraph.Structure B] (e : FirstOrder.Language.digraph.Equiv A B) : HasHamCircuit A ↔ HasHamCircuit B

Having a Hamilton circuit is isomorphism-invariant.

def DescriptiveComplexity.DirHamCircuit : DecisionProblem FirstOrder.Language.digraph

DIRECTED HAMILTON CIRCUIT, as a problem on digraphs: is there a circuit following the arcs and visiting every vertex exactly once?

Equations

• DescriptiveComplexity.DirHamCircuit = { Holds := fun (A : Type) (inst : FirstOrder.Language.digraph.Structure A) => DescriptiveComplexity.HasDirHamCircuit A, iso_invariant := ⋯ }

def DescriptiveComplexity.HamCircuit : DecisionProblem FirstOrder.Language.digraph

HAMILTON CIRCUIT, as a problem on digraphs read symmetrically: is there a circuit following the edges and visiting every vertex exactly once?

Equations

• DescriptiveComplexity.HamCircuit = { Holds := fun (A : Type) (inst : FirstOrder.Language.digraph.Structure A) => DescriptiveComplexity.HasHamCircuit A, iso_invariant := ⋯ }