Введение
Система переписывания строк В теоретической информатике и математической логике система переписывания строк (SRS), исторически называемая системой Полу-Тью, является системой переписывания строк из (обычно конечного) алфавита. При заданном бинарном отношении между фиксированными строками над алфавитом, называемом правилами переписывания и обозначаемым , SRS расширяет отношение переписывания на все строки, в которых левая и правая части правил появляются как подстроки, то есть , где , , и являются строками. Понятие системы Полу-Тью по существу совпадает с представлением моноида. Таким образом, они составляют естественную основу для решения проблемы слов для моноидов и групп. SRS может быть определена непосредственно как абстрактная система переписывания. Её также можно рассматривать как ограниченный вид системы переписывания термов, в которой все функциональные символы имеют арность не более 1. Как формализм, системы переписывания строк являются Тьюринг-полными. Название Полу-Тью происходит от норвежского математика Акселя Тью, который ввёл систематическое изучение систем переписывания строк в статье 1914 года. Тью ввёл это понятие, надеясь решить проблему слов для конечно представленных полугрупп. Лишь в 1947 году было показано, что эта проблема неразрешима — этот результат был получен независимо Эмилем Постом и А. А. Марковым-младшим.
In theoretical computer science and mathematical logic a string rewriting system (SRS), historically called a semi Thue system, is a rewriting system over strings from a (usually finite) alphabet. Given a binary relation between fixed strings over the alphabet, called rewrite rules, denoted by , an SRS extends the rewriting relation to all strings in which the left and right hand side of the rules appear as substrings, that is , where , , , and are strings. The notion of a semi Thue system essentially coincides with the presentation of a monoid. Thus they constitute a natural framework for solving the word problem for monoids and groups. An SRS can be defined directly as an abstract rewriting system. It can also be seen as a restricted kind of a term rewriting system, in which all function symbols have an arity of at most 1. As a formalism, string rewriting systems are Turing complete. The semi Thue name comes from the Norwegian mathematician Axel Thue, who introduced systematic treatment of string rewriting systems in a 1914 paper. Thue introduced this notion hoping to solve the word problem for finitely presented semigroups. Only in 1947 was the problem shown to be undecidable— this result was obtained independently by Emil Post and A. A. Markov Jr.
Конгруэнтность
В целом, множество строк над алфавитом образует свободный моноид вместе с бинарной операцией конкатенации строк (обозначается как и записывается мультипликативно, опуская символ). В SRS отношение редукции совместимо с моноидной операцией, что означает, что для всех строк. Поскольку по определению является предпорядком, образует моноидальный предпорядок. Аналогично, рефлексивно-транзитивное симметричное замыкание , обозначаемое (см. абстрактная система переписывания#Основные понятия), является конгруэнтностью, то есть это отношение эквивалентности (по определению) и оно также совместимо с конкатенацией строк. Отношение называется конгруэнтностью Тью, порожденной R. В системе Тью, то есть если R симметрична, отношение переписывания совпадает с конгруэнтностью Тью.
Связи с другими понятиями
Система полу-Тьюэ также является системой переписывания термов, которая оперирует монадическими словами (функциями), заканчивающимися одной и той же переменной, что и левая и правая части правила, например, правило для термов эквивалентно правилу для строк. Система полу-Тьюэ также представляет собой особый тип пост-канонической системы, однако любая пост-каноническая система может быть сведена к SRS. Оба формализма являются Тьюринг-полными и, следовательно, эквивалентны неограниченным грамматикам Ноама Хомского, которые иногда называют грамматиками полу-Тьюэ. Формальная грамматика отличается от системы полу-Тьюэ лишь разделением алфавита на терминальные и нетерминальные символы, а также выделением начального символа среди нетерминальных. Небольшое число авторов фактически определяет систему полу-Тьюэ как тройку, где называется множеством аксиом. Согласно этому "генеративному" определению системы полу-Тьюэ, неограниченная грамматика – это просто система полу-Тьюэ с единственной аксиомой, в которой алфавит разделен на терминальные и нетерминальные символы, а аксиома является нетерминальным символом. Простое разделение алфавита на терминальные и нетерминальные символы – мощный инструмент, позволяющий определить иерархию Хомского в зависимости от комбинации терминальных и нетерминальных символов, используемых в правилах. Это стало важным достижением в теории формальных языков. В квантовых вычислениях можно разработать понятие квантовой системы Тьюэ. Поскольку квантовые вычисления по своей природе обратимы, правила переписывания по алфавиту должны быть двунаправленными (то есть, базовая система является системой Тьюэ, а не полу-Тьюэ). К подмножеству символов алфавита можно присоединить гильбертово пространство, и правило переписывания, преобразующее одну подстроку в другую, может выполнять унитарную операцию над тензорным произведением гильбертовых пространств, присоединенных к строкам; это означает, что оно сохраняет количество символов из этого множества. Аналогично классическому случаю, можно показать, что квантовая система Тьюэ является универсальной вычислительной моделью для квантовых вычислений, в том смысле, что выполняемые квантовые операции соответствуют однородным классам схем (например, классам в BQP, когда, например, гарантируется завершение правил переписывания строк за полиномиальное число шагов относительно размера входных данных), или, эквивалентно, квантовой машине Тьюринга.
A semi Thue system is also a special type of Post canonical system, but every Post canonical system can also be reduced to an SRS. Both formalisms are Turing complete, and thus equivalent to Noam Chomsky's unrestricted grammars, which are sometimes called semi Thue grammars. A formal grammar only differs from a semi Thue system by the separation of the alphabet into terminals and non terminals, and the fixation of a starting symbol amongst non terminals. A minority of authors actually define a semi Thue system as a triple , where is called the set of axioms. Under this "generative" definition of semi Thue system, an unrestricted grammar is just a semi Thue system with a single axiom in which one partitions the alphabet into terminals and non terminals, and makes the axiom a nonterminal. The simple artifice of partitioning the alphabet into terminals and non terminals is a powerful one; it allows the definition of the Chomsky hierarchy based on what combination of terminals and non terminals the rules contain. This was a crucial development in the theory of formal languages. In quantum computing, the notion of a quantum Thue system can be developed. Since quantum computation is intrinsically reversible, the rewriting rules over the alphabet are required to be bidirectional (i. e. the underlying system is a Thue system, not a semi Thue system). On a subset of alphabet characters one can attach a Hilbert space , and a rewriting rule taking a substring to another one can carry out a unitary operation on the tensor product of the Hilbert space attached to the strings; this implies that they preserve the number of characters from the set Similar to the classical case one can show that a quantum Thue system is a universal computational model for quantum computation, in the sense that the executed quantum operations correspond to uniform circuit classes (such as those in BQP when e. g. guaranteeing termination of the string rewriting rules within polynomially many steps in the input size), or equivalently a Quantum Turing machine.
История и значение
Системы Полу-Тью были разработаны в рамках программы по добавлению дополнительных конструкций в логику, с целью создания систем, таких как логика высказываний, которые позволили бы выражать общие математические теоремы на формальном языке, а затем доказывать и верифицировать их автоматическим, механическим способом. Возлагалась надежда на то, что процесс доказательства теорем можно было бы свести к набору определенных манипуляций со строками. Впоследствии было установлено, что системы Полу-Тью изоморфны неограниченным грамматикам, которые, в свою очередь, известны как изоморфные машинам Тьюринга. Этот исследовательский подход оказался успешным, и теперь компьютеры могут использоваться для проверки доказательств математических и логических теорем. По предложению Алонзо Чёрча, Эмиль Пост в статье, опубликованной в 1947 году, впервые доказал неразрешимость "определенной проблемы Тью", что Мартин Дэвис определяет как "первое доказательство неразрешимости задачи из классической математики – в данном случае, задачи о слове для полугрупп". Дэвис также утверждает, что доказательство было независимо предложено А. А. Марковым.
Монографии
Рональд В. Бук и Фридрих Отто, Системы переписывания строк, Springer, 1993, Маттиас Янтцен, Конфлюэнтное переписывание строк, Birkhäuser, 1988.
Учебники
Мартин Дэвис, Рон Сигал, Элейн Дж. Вейукер, Вычислимость, сложность и языки: основы теоретической информатики, 2-е изд., Academic Press, 1994, глава 7.
Элейн Рич, Автоматы, вычислимость и сложность: теория и приложения, Prentice Hall, 2007, глава 23.5.
Elaine Rich, Automata, computability and complexity: theory and applications, Prentice Hall, 2007, , chapter 23.5.
Опросы
Самсон Абрамский, Дов М. Габбай, Томас С. Э. Майбаум (ред.), "Справочник по логике в информатике: семантическое моделирование", Oxford University Press, 1995, Гжегож Розенберг, Арто Саломаа (ред.), "Справочник по формальным языкам: слова, языки, грамматики", Springer, 1997.