Finite inverse automata and subgroup membership

A finite graph with inverse-labelled edges and at most one outgoing edge of each label from each vertex is represented by its partial transition map. This file proves that the labels of loops at a chosen basepoint form a subgroup of the free group, and that membership in this subgroup is exactly a finite traversal test on the canonical reduced word.

@[reducible, inline]

abbrev Stallings.Letter : Type

A letter in the rank-two free group, with a Boolean recording orientation.

Equations

• Stallings.Letter = (Fin 2 × Bool)

@[reducible, inline]

abbrev Stallings.Word : Type

A word in the signed generators a, b, a⁻¹, and b⁻¹.

Equations

• Stallings.Word = List Stallings.Letter

@[reducible, inline]

abbrev Stallings.Free : Type

The free group on two generators.

Equations

• Stallings.Free = FreeGroup (Fin 2)

def Stallings.letterInv (x : Letter) : Letter

Reverse the orientation of a letter.

Equations

• Stallings.letterInv x = (x.1, !x.2)

@[simp]

theorem Stallings.letterInv_letterInv (x : Letter) : letterInv (letterInv x) = x

def Stallings.wordInv (w : Word) : Word

The inverse word, obtained by reversing and inverting its letters.

Equations

• Stallings.wordInv w = FreeGroup.invRev w

def Stallings.wordEval (w : Word) : Free

Interpret a signed word as an element of the free group.

Equations

• Stallings.wordEval w = FreeGroup.mk w

def Stallings.letterEval (x : Letter) : Free

Interpret one signed generator as an element of the free group.

Equations

• Stallings.letterEval x = if x.2 = true then FreeGroup.of x.1 else (FreeGroup.of x.1)⁻¹

@[simp]

theorem Stallings.wordEval_nil : wordEval [] = 1

@[simp]

theorem Stallings.wordEval_append (u v : Word) : wordEval (u ++ v) = wordEval u * wordEval v

theorem Stallings.wordEval_singleton (x : Letter) : wordEval [x] = letterEval x

@[simp]

theorem Stallings.wordEval_cons (x : Letter) (w : Word) : wordEval (x :: w) = letterEval x * wordEval w

@[simp]

theorem Stallings.letterEval_inv (x : Letter) : letterEval (letterInv x) = (letterEval x)⁻¹

@[simp]

theorem Stallings.wordEval_wordInv (w : Word) : wordEval (wordInv w) = (wordEval w)⁻¹

structure Stallings.InverseAutomaton (V : Type u_1) : Type u_1

A deterministic graph whose edges come in inverse-labelled pairs.

The transition function is partial: none means that no edge with that label leaves the given vertex.

• base : V

  The vertex at which accepted loops start and end.

• next : V → Letter → Option V

  The target of a labelled edge, when that edge exists.

• inverse_next {v : V} {x : Letter} {w : V} : self.next v x = some w → self.next w (letterInv x) = some v

def Stallings.InverseAutomaton.run {V : Type u_1} (G : InverseAutomaton V) (v : V) : Word → Option V

Execute a word from a starting state, stopping if a required edge is absent.

Equations

• G.run v [] = some v
• G.run v (x_1 :: w) = (G.next v x_1).bind fun (u : V) => G.run u w

@[simp]

theorem Stallings.InverseAutomaton.run_nil {V : Type u_1} (G : InverseAutomaton V) (v : V) : G.run v [] = some v

inductive Stallings.InverseAutomaton.Walk {V : Type u_1} (G : InverseAutomaton V) : V → Word → V → Prop

A labelled path in an inverse automaton.

• nil {V : Type u_1} {G : InverseAutomaton V} (v : V) : G.Walk v [] v
• cons {V : Type u_1} {G : InverseAutomaton V} {v u z : V} {x : Letter} {w : Word} (edge : G.next v x = some u) (tail : G.Walk u w z) : G.Walk v (x :: w) z

theorem Stallings.InverseAutomaton.run_eq_some_iff_walk {V : Type u_1} (G : InverseAutomaton V) {v z : V} {w : Word} : G.run v w = some z ↔ G.Walk v w z

The executable traversal returns an endpoint exactly when the corresponding path exists.

theorem Stallings.InverseAutomaton.Walk.append {V : Type u_1} (G : InverseAutomaton V) {v u t : V} {w₁ w₂ : Word} (h₁ : G.Walk v w₁ u) (h₂ : G.Walk u w₂ t) : G.Walk v (w₁ ++ w₂) t

Concatenate two paths whose endpoints match.

theorem Stallings.InverseAutomaton.Walk.invRev {V : Type u_1} (G : InverseAutomaton V) {v u : V} {w : Word} (h : G.Walk v w u) : G.Walk u (wordInv w) v

Reversing a path and inverting every label gives the reverse path.

theorem Stallings.InverseAutomaton.run_append {V : Type u_1} (G : InverseAutomaton V) (v : V) (u z : Word) : G.run v (u ++ z) = (G.run v u).bind fun (t : V) => G.run t z

Traversal distributes over concatenation of words.

theorem Stallings.InverseAutomaton.run_success_cancel {V : Type u_1} (G : InverseAutomaton V) (v : V) (pre suffix : Word) (x : Letter) {z : V} (h : G.run v (pre ++ x :: letterInv x :: suffix) = some z) : G.run v (pre ++ suffix) = some z

A successful traversal remains successful after cancelling a letter pair.

theorem Stallings.InverseAutomaton.run_success_of_red_step {V : Type u_1} (G : InverseAutomaton V) (v : V) {w z : Word} (h : FreeGroup.Red.Step w z) {t : V} (hRun : G.run v w = some t) : G.run v z = some t

A successful traversal remains successful under one free-reduction step.

theorem Stallings.InverseAutomaton.run_success_of_red {V : Type u_1} (G : InverseAutomaton V) (v : V) {w z : Word} (h : FreeGroup.Red w z) {t : V} (hRun : G.run v w = some t) : G.run v z = some t

A successful traversal remains successful after any sequence of free reductions.

theorem Stallings.InverseAutomaton.run_success_of_reduction {V : Type u_1} (G : InverseAutomaton V) (v : V) (w : Word) {t : V} (hRun : G.run v w = some t) : G.run v (FreeGroup.reduce w) = some t

A successful traversal remains successful on the canonical reduced word.

def Stallings.InverseAutomaton.loopSubgroup {V : Type u_1} (G : InverseAutomaton V) : Subgroup Free

The subgroup represented by all loops at the basepoint.

Equations

• G.loopSubgroup = { carrier := {g : Stallings.Free | ∃ (w : Stallings.Word), Stallings.wordEval w = g ∧ G.Walk G.base w G.base}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def Stallings.InverseAutomaton.accepts {V : Type u_1} (G : InverseAutomaton V) (g : Free) : Prop

Membership in the loop subgroup is decided by traversing the canonical reduced word.

Equations

• G.accepts g = (G.run G.base (FreeGroup.toWord g) = some G.base)

theorem Stallings.InverseAutomaton.accepts_iff_mem_loopSubgroup {V : Type u_1} (G : InverseAutomaton V) (g : Free) : G.accepts g ↔ g ∈ G.loopSubgroup

def Stallings.InverseAutomaton.membershipTest {V : Type u_1} [DecidableEq V] (G : InverseAutomaton V) (g : Free) : Bool

Executable subgroup-membership test for a finite inverse automaton.

Equations

• G.membershipTest g = if G.run G.base (FreeGroup.toWord g) = some G.base then true else false

@[simp]

theorem Stallings.InverseAutomaton.membershipTest_eq_true_iff {V : Type u_1} [DecidableEq V] (G : InverseAutomaton V) (g : Free) : G.membershipTest g = true ↔ g ∈ G.loopSubgroup