English
The subset construction yields a DFA whose states are sets of NFA states, the start state is the set of NFA start states, and a set S of NFA-states is accepting exactly when some state in S is accepting in the NFA.
Русский
Подмножество конструирование строит детерминированный конечный автомат, чьи состояния – множества состояний НКА, стартовое состояние — множество стартовых состояний НКА, а множество принимающих состояний детерминированного автомата состоит из всех множеств, содержащих хотя бы одно принимающее состояние НКА.
LaTeX
$$$\text{toDFA}(M) = \mathrm{DFA}\; \alpha\; (\mathrm{Set}\; \sigma)\;\text{where }\text{step}=M.stepSet,\; \text{start}=M.start,\; \text{accept} = \{S \mid \exists s \in S,\; s \in M.accept\}.$$$
Lean4
/-- `M.toDFA` is a `DFA` constructed from an `NFA` `M` using the subset construction. The
states is the type of `Set`s of `M.state` and the step function is `M.stepSet`. -/
def toDFA : DFA α (Set σ) where
step := M.stepSet
start := M.start
accept := {S | ∃ s ∈ S, s ∈ M.accept}
