Изменения
Нет описания правки
Более формально:
{{Определение
|definition = '''Линейно ограниченный автомат''' (англ. ''linear bounded automata'', ''lba'') — формальная система <tex>M = \langle Q, \Sigma, \Gamma, \delta, q_0, F \rangle</tex>, в которой
*<tex>Q</tex> — множество состояний,
*<tex>q_0 \in Q</tex> — начальное состояние,
Если <tex>L</tex> — [[Иерархия Хомского формальных грамматик#Класс 1|контекстно-зависимый язык]], то язык <tex>L</tex> принимается некоторым линейно ограниченным автоматом.
|proof=
Пусть <tex>G = \langle V_N , V_T, P, S\rangle</tex> — контекстно-зависимая грамматика. Мы построим lba линейный ограниченный автомат <tex>M</tex>, такой, что язык, принимаемый lba <tex>M</tex>, есть <tex>L(G)</tex>.
Входная лента будет иметь две дорожки. Первая дорожка будет содержать входную строку <tex>x (x \ne \epsilon)</tex> с концевыми маркерами. Вторая дорожка будет использоваться для работы.
На первом шаге lba <tex>M</tex> помещает символ <tex>S</tex> в крайнюю левую ячейку второй дорожки. Затем автомат входит в порождающую подпрограмму, которая выполняет следующие шаги:
'''1.''' Подпрограмма выбирает последовательные подстроки символов <tex>\alpha</tex> на второй дорожке, такие, что <tex>\alpha \rightarrow \beta \in P</tex>.
'''4.''' При выходе из подпрограммы первая дорожка все еще будет содержать строку <tex>x</tex>, в то время как вторая дорожка будет содержать некоторую строку <tex>y</tex>, такую, что <tex>S \Rightarrow^*_M y</tex>.
Автомат <tex>M</tex> сравнивает посимвольно цепочки <tex>x</tex> и <tex>y</tex>. Если окажется, что <tex>x \ne y</tex>, то автомат останавливается, не принимая, если же окажется, что <tex>x = y</tex>, то он останавливается, принимая входную цепочку. Ясно, что если <tex>x \in L(G)</tex>, то найдется такая последовательность движений lba <tex>M</tex>, которая сгенерирует цепочку <tex>x</tex> на второй дорожке, и тогда автомат остановится, принимая. Аналогично, если lba <tex>M</tex> принимает цепочку <tex>x</tex>, то должна существовать последовательность движений, генерирующих цепочку <tex>x</tex> на второй дорожке. Только при таком условии lba <tex>M</tex> принимает цепочку <tex>x</tex>. Но, по построению, процесс генерации <tex>x</tex> воспроизводит вывод этой цепочки из <tex>S</tex>. Следовательно, <tex>S \Rightarrow^*_M x</tex>.
}}
Для доказательства этой теоремы построим контекстно-зависимую грамматику, которая моделирует линейно ограниченный автомат.
Нетерминалы контекстно-зависимой грамматики должны указывать не только первоначальное содержание некоторой ячейки ленты lbaлинейно ограниченного автомата, но также и то, является ли эта ячейка смежной с концевым маркером слева или справа. Такие ячейки в обозначении нетерминалов мы будем снабжать маркерами <tex>\#</tex> и <tex>\$</tex>, обозначающими, что ячейка граничит соответственно с левым, правым или обоими концевыми маркерами. В обозначении нетерминала состояние lba линейно ограниченного автомата должно также комбинироваться с символом, находящимся под головкой ленты. Контекстно-зависимая грамматика не может иметь отдельных символов для концевых маркеров и состояния линейно ограниченного автомата, потому что эти символы должны были бы заменяться на пустые цепочки, когда строка превращается в терминальную, а <tex>\epsilon</tex>-порождения в контекстно-зависимой грамматике запрещены.
В грамматике необходимо поддерживать три типа операций:
* Операции, которые генерирую две копии строки, наряду с некоторыми символами, которые выполняют роль маркеров, чтобы разделять эти копии.
* Операции, которые симулируют некоторую последовательность действий lba линейно ограниченного автомата <tex>M</tex>. Во время их выполнения, одна из двух копий оригинальной строки остается неизменной, другая же представляет из себя входную ленту <tex>M</tex> и соответствующе изменяется.* Операции, которые могут удалить всё кроме не измененной копии строки. Применяются, когда, симулированная на другой копии исходной строки, последовательность действий lba <tex>M</tex> привела к принимающему состоянию.
Более подробное доказательство приведено в книге Мартыненко Б.К. Языки и трансляции.
