English
A DFA can be built whose states are the left quotients of L, with transitions given by appending the input symbol to the representative word, the start state corresponding to L, and accepting states determined by whether the empty word lies in the corresponding left quotient. This automaton recognizes L.
Русский
Можно построить ДКА, чьи состояния являются левыми делителями языка L, переходы задаются добавлением входного символа к представителю слова, стартовое состояние соответствует L, а принимающие состояния определяются тем, принадлежит ли пустое слово соответствующему левому делителю. Такой ДКА распознаёт L.
LaTeX
$$$\text{toDFA} : DFA\; \alpha\; (\mathrm{Set.range}(L.leftQuotient)).\mathrm{Elem}$.$$
Lean4
/-- The left quotients of a language are the states of an automaton that accepts the language. -/
def toDFA : DFA α (Set.range L.leftQuotient)
where
step s
a := by
refine ⟨s.val.leftQuotient [a], ?_⟩
obtain ⟨y, hy⟩ := s.prop
exists y ++ [a]
rw [← hy, leftQuotient_append]
start := ⟨L, by exists []⟩
accept := {s | [] ∈ s.val}
