Изменения

Пусть язык содержит слово <tex>w</tex>. Любой автомат <tex>A</tex>, задающий этот язык, должен допускать <tex>w</tex>. Тогда при переходе из стартового состояния <tex>A</tex> по символам <tex>w</tex> получится путь, оканчивающийся в одной одном из терминальных вершинсостояний.

Пусть в автомате существует путь из стартового состояния в одно из допускающих. Рассмотрим последовательность символов на рёбрахпереходах, образующих этот путь. Строка из этой последовательности допускается автоматом, а значит, принадлежит языку.

Пусть <tex>A_{1}</tex> и <tex>A_{2}</tex> - — детерминированные конечные автоматы, соответствующие языкам <tex>L_{1}</tex> и <tex>L_{2}</tex> над одним алфавитом <tex>\Sigma</tex>, соответственно. Совпадение языков на языке конечных автоматов (''эквивалентность'') означает, что любое слово, допустимое одним автоматом, допускается и другим. Назовём состояния <tex>p_{1} \in A_{1}</tex> и <tex>p_{2} \in A_{2}</tex> '''различимыми''', если существует строка <tex>w</tex> из символов <tex>\Sigma</tex>, для которой выполняется

где <tex>s_{1}</tex>, <tex>s_{2}</tex> - — стартовые состояния, <tex>t_{1}</tex>, <tex>t_{2}</tex> - — допускающие состояния, <tex>u_{1}</tex>, <tex>u_{2}</tex> - — недопускающие.

Все ''бесполезные'' состояния, из которых не достигаются допускающие, не влияют на множество слов, допускаемых автоматами, поэтому далее они рассматриваться не будут; назовём их '''бесполезными'''. Введём '''сток'' - ' — специальное недопускающее состояние, переходы по всем символам из которого ведут в него самого. Все переходы исходного автомата, которые отсутствовали или вели в бесполезные состояния, направим в сток.

Пусть <tex>eq(u, v)</tex> - — функция, принимающая пару состояний из первого и второго автоматов и возвращающая некоторое значение булевского типа. Второй шаг алгоритма - — установка <tex>eq(u, v)</tex> в <tex>false</tex> для всех пар <tex>\langle u, v \rangle</tex>, кроме <tex>\langle s_{1}, s_{2} \rangle</tex>. Также создаётся очередь, в которую помещается пара <tex>\langle s_{1}, s_{2} \rangle</tex>.

Третий шаг алгоритма - — [[Обход в ширину|обход в ширину]]. Пусть на текущем шаге из очереди получена пара <tex>\langle u \in A_{1}, v \in A_{2} \rangle</tex>. Тогда для всех символов <tex>c \in \Sigma</tex> рассматриваются пары <tex>\langle u', v' \rangle : \delta_{1} (u, c) = u', \delta_{2} (v, c) = v'</tex>. Если <tex>eq(u', v')</tex> возвращает <tex>false</tex>, данное значение устанавливается в <tex>true</tex>, а в очередь добавляется пара <tex>\langle u', v' \rangle</tex>.

Пусть такая пара <tex>\langle u, v \rangle</tex> существует. Для определённости скажем, что <tex>u \in A_{1}</tex> - — допускающее. Рассмотрим строку <tex>w</tex>, состоящую из символов, в результате переходов по которым из <tex>\langle s_{1}, s_{2} \rangle</tex> в процессе обхода в ширину <tex>eq(u, v)</tex> было установлено в <tex>true</tex>. Строка <tex>w</tex> допускается первым автоматом, но не допускается вторым, значит, автоматы не эквивалентны.

Алгоритм проверки <tex>L_{1}</tex> на включение в <tex>L_{2}</tex> идентичен алгоритму проверки их совпадения, кроме одной особенности. Могут существовать слова из <tex>L_{2}</tex>, не входящие в <tex>L_{1}</tex>, поэтому существование пар <tex>\langle v \in L_{1}, u \in L_{2} \rangle : eq(v, u) == true, v \notin T_{1}, u \in T_{2}</tex>, где <tex>T_{i}</tex> - — множества допускающих состояний, не нарушает факт вхождения <tex>L_{1}</tex> в <tex>L_{2}</tex>. Таким образом, <tex>L_{1}</tex> не входит в <tex>L_{2}</tex> тогда и только тогда, когда после окончания работы алгоритма, идентичного алгоритму проверки на совпадение, не существует такой пары <tex>\langle v, u \rangle</tex>, что <tex>eq(v, u)</tex> возвращает <tex>true</tex>, <tex>v \in T_{1}, u \notin T_{2}</tex>.

Пусть такое состояние <tex>v</tex> существует, а строки <tex>x, y, z</tex> таковы, что <tex>\langle s, xyz \rangle \vdash ^{*} \langle v, yz \rangle \vdash ^{*} \langle v, z \rangle \vdash ^{*} \langle t, \epsilon \rangle</tex>, <tex>t</tex> - — допускающее, <tex>y</tex> - — непустая. Рассмотрим строки вида <tex>xy^{k}z, k \in \mathbb{N}</tex>. Их бесконечное количество, и все они, как легко увидеть, допускаются автоматом. Значит, язык бесконечен.

Пусть такого состояния не существует. Тогда любой путь из стартового состояния в какое-либо из допускающих является простым. Количество слов в языке равно количеству таких путей; количество путей, в свою очередь, ограничено <tex>n! (n-1)^{| \Sigma |^{n-1}</tex>, где <tex>n</tex> - — количество состояний автомата: <tex>n!</tex> - — количество перестановок состояний, <tex>(n-1)^{| \Sigma |^{n-1}</tex> - — количество совокупностей переходов по символам между ними. Таким образом, язык конечен.

Доказанное утверждение позволяет свести задачу поиска числа слов в языке к поиску количества различных путей в ациклическом графе. Сначала с помощью [[Обход в глубину, цвета вершин|обхода в глубину]] по обратным рёбрам определим '''полезные''' состояния, из которых достижимо хотя бы одно допускающее. Затем найдём любой цикл, состояния которого полезны, достижимый из старта; при нахождении констатируем бесконечность языка. Пусть язык конечен; тогда отсортируем автомат [[Использование обхода в глубину для топологической сортировки|топологически]]. Введём функцию <tex>paths(v)</tex>, задающую число различных путей из <tex>s</tex> в <tex>v</tex>; <tex>paths(s) = 1</tex>. Заметим, что если известны значения <tex>paths(u)</tex> для всех <tex>u</tex>, из которых существует переход в <tex>v</tex>, то <tex>paths(v) = \sum\limits_{u}paths(u)</tex>. Количеством слов в языке будет сумма <tex>paths(t)</tex> для всех допускающих <tex>t</tex>.