Documentation

Acmoi.HydeTheorem

Hyde's Theorem #

source
def δ_of_path {A : Type u_1} {Q : Type u_2} {n : ℕ} (w : Fin n → A) (p : Fin (n + 1) → Q) :
A → Q → Set Q

The transition function δ generated by a labeled path. δ b r = {s | s is reachable in one step from r reading b}.

Equations
source
def khδ' {A : Type u_1} {k : ℕ} (w : Fin (2 * k + 1) → A) :
A → Fin (k + 1) → Set (Fin (k + 1))

Kayleigh Hyde's "Kayleigh graph" transition function δ.

Equations
source
def moves_slowly {k : ℕ} (p : Fin (2 * k + 1 + 1) → Fin (k + 1)) :
Prop
Equations
source
theorem khδ_moves_slowly {A : Type u_1} {k : ℕ} {w : Fin (2 * k + 1) → A} {p : Fin (2 * k + 1 + 1) → Fin (k + 1)} {final : Fin (k + 1)} (h : accepts_path (khδ' w) 0 final p) :
moves_slowly p

If a Kayleigh graph accepts a word then it never advances by more than one. NOTE: More is true, it is sufficient that ``khδ'` process the word.

source
theorem idBound_of_moves_slowly {k : ℕ} {p : Fin (2 * k + 1 + 1) → Fin (k + 1)} (h : p 0 = 0) (h₀ : moves_slowly p) (s : Fin (2 * k + 1 + 1)) :
↑(p s) ≤ ↑s
source
theorem kayleighBound {A : Type u_1} {k : ℕ} {w : Fin (2 * k + 1) → A} {p : Fin (2 * k + 1 + 1) → Fin (k + 1)} (h : accepts_path (khδ' w) 0 0 p) (s : Fin (2 * k + 1 + 1)) :
↑(p s) ≤ ↑s

If a Kayleigh graph accepts a word then its position is dominated by the identity.

source
def retreatSlow {k : ℕ} (p : Fin (2 * k + 1 + 1) → Fin (k + 1)) :
Prop
Equations
source
theorem kayleighBound_lower {A : Type u_1} {k : ℕ} (w : Fin (2 * k + 1) → A) (p : Fin (2 * k + 1 + 1) → Fin (k + 1)) (h : accepts_path (khδ' w) 0 0 p) :
retreatSlow p

A Kayleigh graph path does not retreat too fast.

source
theorem loop_when_of_retreat_slow {k : ℕ} (p : Fin (2 * (k + 1)) → Fin (k + 1)) {t : Fin (2 * k + 1)} (ht : p t.castSucc = Fin.last k ∧ p t.succ = Fin.last k) (h₀ : p 0 = 0) (h₁ : retreatSlow p) (h₂ : moves_slowly p) (h₃ : p (Fin.last (2 * k + 1)) = 0) :
t = ⟨k, ⋯⟩
source
theorem hyde_loop_when {A : Type u_1} {k : ℕ} (w : Fin (2 * k + 1) → A) (p : Fin (2 * (k + 1)) → Fin (k + 1)) (h : accepts_path (khδ' w) 0 0 p) (t : Fin (2 * k + 1)) (ht : p t.castSucc = Fin.last k ∧ p t.succ = Fin.last k) :
t = ⟨k, ⋯⟩

If the Kayleigh graph ever uses the loop, we know when! Same proof for khδ' as for khδ given earlier lemmas, so we could generalize this.

source
theorem general_parity {k : ℕ} {p : Fin (2 * (k + 1)) → Fin (k + 1)} (h₀ : p 0 = 0) (h₁ : retreatSlow p) (h₂ : moves_slowly p) (h₄ : ∀ (i : Fin (2 * k + 1)), p i.succ ≠ p i.castSucc) (t : Fin (2 * (k + 1))) :
↑(p t) % 2 = ↑t % 2
source
theorem khδ_not_still {A : Type u_1} {k : ℕ} {w : Fin (2 * k + 1) → A} {p : Fin (2 * (k + 1)) → Fin (k + 1)} (h : accepts_path (khδ' w) 0 0 p) (i : Fin (2 * k + 1)) (hi : p i.succ = p i.castSucc) :
p i.succ = Fin.last k
source
theorem hyde_parity {A : Type u_1} {k : ℕ} {w : Fin (2 * k + 1) → A} {p : Fin (2 * (k + 1)) → Fin (k + 1)} (h : accepts_path (khδ' w) 0 0 p) (H : ¬∃ (t : Fin (2 * k + 1)), p t.castSucc = Fin.last k ∧ p t.succ = Fin.last k) (t : Fin (2 * (k + 1))) :
↑(p t) % 2 = ↑t % 2

If a Kayleigh graph path never uses the loop, then it preserves parity.

source
theorem move_slowly_rev_aux' {k : ℕ} (p : Fin (2 * (k + 1)) → Fin (k + 1)) (h : retreatSlow p) (s : Fin k) :
k ≤ k - ↑(p ⟨↑s + k + 1, ⋯⟩) + 1 + ↑(p ⟨↑s + 1 + k + 1, ⋯⟩)

An auxiliary lemma about slow-retreating paths.

source
theorem general_unique_path {k : ℕ} (p : Fin (2 * (k + 1)) → Fin (k + 1)) (h₀ : p 0 = 0) (h₁ : p (Fin.last (2 * k + 1)) = 0) (h₂ : moves_slowly p) (h₃ : retreatSlow p) (h₄ : ∀ (i : Fin (2 * k + 1)), p i.succ = p i.castSucc → p i.succ = Fin.last k) :
p = fun (t : Fin (2 * (k + 1))) => if x : ↑t < k + 1 then ⟨↑t, x⟩ else ⟨2 * k + 1 - ↑t, ⋯⟩
source
theorem hyde_unique_path {A : Type u_1} {k : ℕ} (w : Fin (2 * k + 1) → A) (p : Fin (2 * (k + 1)) → Fin (k + 1)) (h : accepts_path (khδ' w) 0 0 p) :
p = fun (t : Fin (2 * (k + 1))) => if x : ↑t < k + 1 then ⟨↑t, x⟩ else ⟨2 * k + 1 - ↑t, ⋯⟩

The Kayleigh graph NFA for an odd-length word w accepts along only the intended path.

source
theorem hyde_unique_path_reading_word' {A : Type u_1} {k : ℕ} {w : Fin (2 * k + 1) → A} {v : Fin (2 * k + 1) → A} {p : Fin (2 * (k + 1)) → Fin (k + 1)} (h : accepts_word_path (khδ' w) v 0 0 p) :
p = fun (t : Fin (2 * (k + 1))) => if x : ↑t < k + 1 then ⟨↑t, x⟩ else ⟨2 * k + 1 - ↑t, ⋯⟩

The Kayleigh graph NFA for an odd-length word w accepts along only the intended path, no matter what word v with |v| = |w| is read.

source
theorem hyde_unique_word' {A : Type u_1} {k : ℕ} {w : Fin (2 * k + 1) → A} {v : Fin (2 * k + 1) → A} {p : Fin (2 * (k + 1)) → Fin (k + 1)} (ha : accepts_word_path (khδ' w) v 0 0 p) :
w = v

The Kayleigh graph NFA for w accepts no word of length |w| other than w.

source
theorem δ_of_path_works_as_intended' {A : Type u_1} {Q : Type u_2} {n : ℕ} (w : Fin n → A) (p : Fin (n + 1) → Q) :
accepts_word_path (δ_of_path w p) w (p 0) (p (Fin.last n)) p

δ_of_path works as intended.

source
theorem hyde_accepts {A : Type u_1} {k : ℕ} (w : Fin (2 * k + 1) → A) :
accepts_word_path (khδ' w) w 0 0 fun (t : Fin (2 * k + 1 + 1)) => if x : ↑t < k + 1 then ⟨↑t, x⟩ else ⟨2 * k + 1 - ↑t, ⋯⟩
source
theorem hydetheorem_odd' {A : Type u_1} {k : ℕ} (w : Fin (2 * k + 1) → A) :
A_N_at_most w (k + 1)

Hyde's theorem for odd-length words.

source
theorem hyde_pos_length {A : Type u_1} {n : ℕ} (hn : n ≠ 0) (w : Fin n → A) :
A_N_at_most w (n / 2 + 1)

Hyde's theorem for positive-length words.

source
theorem hyde_all_lengths {A : Type u_1} {n : ℕ} (w : Fin n → A) :
A_N_at_most w (n / 2 + 1)

Hyde's theorem in relational form.

source
theorem A_N_bounded {A : Type u_1} {n : ℕ} (w : Fin n → A) :
∃ (q : ℕ), A_N_at_most w q

A_N is well-defined.

source
noncomputable def A_N {A : Type u_1} {n : ℕ} :
(Fin n → A) → ℕ

Nondeterministic automatic complexity.

Equations
source
theorem A_N_bound {A : Type u_1} {n : ℕ} (w : Fin n → A) :
A_N w ≤ n / 2 + 1

Hyde's theorem (2013).

source
theorem A_Ne_bounded {A : Type} {n : ℕ} (w : Fin n → A) :
∃ (q : ℕ), A_Ne_at_most w q
source
noncomputable def A_Ne {A : Type} {n : ℕ} :
(Fin n → A) → ℕ

Exact nondeterministic automatic complexity.

Equations