Myhill–Nerode theorem #

This file proves the Myhill–Nerode theorem using left quotients.

Given a language L and a word x, the left quotient of L by x is the set of suffixes y such that x ++ y is in L. The Myhill–Nerode theorem shows that each left quotient, in fact, corresponds to the state of an automaton that matches L, and that L is regular if and only if there are finitely many such states.

References #

https://en.wikipedia.org/wiki/Syntactic_monoid#Myhill%E2%80%93Nerode_theorem

source

def Language.leftQuotient {α : Type u} (L : Language α) (x : List α) :

Language α

The left quotient of x is the set of suffixes y such that x ++ y is in L.

Equations

L.leftQuotient x = {y : List α | x ++ y ∈ L}

Instances For

source

@[simp]

theorem Language.leftQuotient_nil {α : Type u} (L : Language α) :

L.leftQuotient [] = L

source

theorem Language.leftQuotient_append {α : Type u} (L : Language α) (x y : List α) :

L.leftQuotient (x ++ y) = (L.leftQuotient x).leftQuotient y

source

@[simp]

theorem Language.mem_leftQuotient {α : Type u} {L : Language α} (x y : List α) :

y ∈ L.leftQuotient x ↔ x ++ y ∈ L

source

theorem Language.leftQuotient_accepts_apply {α : Type u} {σ : Type v} (M : DFA α σ) (x : List α) :

M.accepts.leftQuotient x = M.acceptsFrom (M.eval x)

source

theorem Language.leftQuotient_accepts {α : Type u} {σ : Type v} (M : DFA α σ) :

M.accepts.leftQuotient = M.acceptsFrom ∘ M.eval

source

theorem Language.IsRegular.finite_range_leftQuotient {α : Type u} {L : Language α} (h : L.IsRegular) :

(Set.range L.leftQuotient).Finite

source

def Language.toDFA {α : Type u} (L : Language α) :

DFA α ↑(Set.range L.leftQuotient)

The left quotients of a language are the states of an automaton that accepts the language.

Equations

L.toDFA = { step := fun (s : ↑(Set.range L.leftQuotient)) (a : α) => ⟨(↑s).leftQuotient [a], ⋯⟩, start := ⟨L, ⋯⟩, accept := {s : ↑(Set.range L.leftQuotient) | [] ∈ ↑s} }