В теоретическом информатики и математической логике строка переписывания системы ( SRS ), исторически называется полу- Thue системой , является переписыванием системы над строками из (обычно конечного ) алфавита . Учитывая бинарное отношение между фиксированными строками в алфавите, называемыми правилами перезаписи , обозначаемыми, SRS расширяет отношение перезаписи на все строки, в которых левая и правая части правил появляются как подстроки , т. е., где , , , а также струны.
Понятие полусистемы Туэ по существу совпадает с представлением моноида . Таким образом, они составляют естественную основу для решения проблемы слов для моноидов и групп.
SRS можно определить непосредственно как абстрактную систему перезаписи . Это также можно рассматривать как ограниченный вид системы переписывания терминов . Как формализм, системы перезаписи строк являются полными по Тьюрингу . [ необходимая цитата ] Имя полу-Туэ происходит от норвежского математика Акселя Туэ , который представил систематическую трактовку систем перезаписи строк в статье 1914 года. [1] Туэ ввел это понятие в надежде решить проблему слов для конечно определенных полугрупп. Только в 1947 г. была показана неразрешимость проблемы - этот результат независимо друг от друга получили Эмиль Пост и А.А. Марков-младший [2] [3]
Определение
Система переписывания строк или система полу-Туэ - это кортеж где
- Σ - это алфавит, обычно предполагаемый конечным. [4] Элементы множества(* здесь звезда Клини ) - конечные (возможно, пустые) строки на Σ , иногда называемые словами в формальных языках ; мы будем называть их здесь просто строками.
- R - бинарное отношение на строках из Σ , т. Е. Каждый элемент называется правилом (перезаписи) и обычно записывается.
Если отношение R является симметричным , то система называется системой Туэ- .
Правила перезаписи в R могут быть естественным образом распространены на другие строки впозволяя подстроки быть переписаны в соответствии с R . Более формально отношение отношения одношаговой перезаписииндуцированный R на для любых струн :
- тогда и только тогда, когда существуют такой, что , , а также .
С это отношение на , пара соответствует определению абстрактной системы перезаписи . Очевидно, R является подмножеством. Некоторые авторы используют другое обозначение стрелки в (например ), чтобы отличить его от самого R () , Потому что они потом хотят , чтобы иметь возможность опускать индекс и до сих пор избежать путаницы между R и одностадийного переписывание индуцированного R .
Ясно, что в системе полутуэ мы можем сформировать (конечную или бесконечную) последовательность струн, образованную, начиная с начальной строки и многократно переписывая его, заменяя по одной подстроке за раз:
Нулевой или-больше-шаги переписывания как это захватывается рефлексивном транзитивного замыкания из, обозначаемый (см. абстрактную систему переписывания # Основные понятия ). Это называется отношением переписывания или редукционным отношением наиндуцированный R .
Thue congruence
В общем, набор строк на алфавите образует свободный моноид вместе с бинарной операцией в конкатенации (обозначается каки записывается мультипликативно, отбрасывая символ). В SRS редукционное отношение совместим с операцией моноида, что означает, что подразумевает для всех струн . Спо определению является предварительным заказом ,образует моноидальный предзаказ .
Аналогичным образом , рефлексивный транзитивен симметричное замыкание из, обозначенный (см. абстрактную систему переписывания # Основные понятия ), является конгруэнцией , что означает, что это отношение эквивалентности (по определению), и оно также совместимо с конкатенацией строк. Соотношениеназывается Туэ конгруэнтность , порожденный R . В системе Туэ, т. Е. Если R симметрично, соотношение перезаписи совпадает с конгруэнцией Туэ .
Факторные моноиды и моноидные представления
С является конгруэнцией, мы можем определить фактор-моноид от свободного моноида путем сравнения Туэ обычным способом . Если моноидявляется изоморфными с, то система полутуэ называется моноид представление о.
Мы сразу получаем очень полезные связи с другими областями алгебры. Например, алфавит { a , b } с правилами { ab → ε, ba → ε}, где ε - пустая строка , представляет собой представление свободной группы на одном образующем. Если вместо этого правила просто { ab → ε}, то мы получаем представление бициклического моноида .
Важность систем полутуэ как представления моноидов усиливается следующим:
Теорема : каждый моноид имеет представление в виде, таким образом, он всегда может быть представлен полу-системой Туэ, возможно, над бесконечным алфавитом. [5]
В этом контексте набор называется множество генераторов из, а также называется набором определяющих соотношений . Мы можем сразу классифицировать моноиды на основе их представления. называется
- конечно порожденный, если конечно.
- конечно представлены, если оба а также конечны.
Проблема слов для систем полу-Туэ
Проблема слов для систем полутуэ может быть сформулирована следующим образом: для данной системы полутуэ и два слова (строки) , может превратиться в применяя правила из ? Эта проблема неразрешима , т. Е. Нет общего алгоритма решения этой проблемы. Это справедливо даже в том случае, если мы ограничиваем ввод конечными системами [ требуется определение ] .
Мартин Дэвис предлагает рядовым читателям двухстраничное доказательство в своей статье «Что такое вычисления?» С. 258–259 с комментарием с. 257. Дэвис формулирует доказательство следующим образом: «Придумайте [словесную проблему], решение которой привело бы к решению проблемы остановки ».
Связи с другими понятиями
Система полу-Туэ также является системой переписывания терминов , в которой есть монадические слова (функции), оканчивающиеся той же переменной, что и левые и правые члены, [6] например, правило термина эквивалентно строковому правилу .
Система полутхуэ также является особым типом канонической системы Post , но каждая каноническая система Post также может быть сведена к SRS. Оба формализма Тьюринг , и , таким образом эквивалентен Хомский «ы неограниченные грамматики , которые иногда называют пол-Туэ грамматик . [7] Формальная грамматика только отличается от полу-Туэ системы путем разделения алфавита в терминалах и не-терминалов, а также фиксации исходного символа среди не-терминалов. Меньшая часть авторов фактически определяет систему полутуэ как тройную систему., где называется набором аксиом . Согласно этому «порождающему» определению системы полу-Туэ, неограниченная грамматика - это просто система полу-Туэ с единственной аксиомой, в которой алфавит разбивается на терминальные и нетерминальные и делает аксиому нетерминальной. [8] Простая уловка разделения алфавита на терминалы и нетерминалы - очень мощный прием; он позволяет определять иерархию Хомского на основе того, какую комбинацию терминалов и нетерминалов содержат правила. Это было решающим достижением в теории формальных языков .
В квантовых вычислениях можно развить понятие квантовой системы Туэ. [9] Поскольку квантовые вычисления по своей сути обратимы, перезапись правила по алфавитудолжны быть двунаправленными (т. е. лежащая в основе система является системой Туэ, а не системой полу-Туэ). На подмножестве букв алфавита можно присоединить гильбертово пространство , и правило перезаписи, переводящее одну подстроку в другую, может выполнять унитарную операцию над тензорным произведением гильбертова пространства, присоединенного к строкам; это означает, что они сохраняют количество символов из набора. Подобно классическому случаю, можно показать, что квантовая система Туэ является универсальной вычислительной моделью для квантовых вычислений в том смысле, что выполняемые квантовые операции соответствуют унифицированным классам схем (например, в BQP, когда, например, гарантируется завершение правил перезаписи строки в пределах полиномиально большого количества шагов от входного размера), или, что то же самое, квантовой машины Тьюринга .
История и значение
Системы Semi-Thue были разработаны как часть программы для добавления дополнительных конструкций в логику , чтобы создать такие системы, как логика высказываний , которые позволяли бы выражать общие математические теоремы на формальном языке , а затем доказывать и проверять их в автоматическом режиме. , механическая мода. Была надежда, что затем акт доказательства теорем можно свести к набору определенных манипуляций с набором строк. Впоследствии выяснилось, что системы полу-Туэ изоморфны неограниченным грамматикам , которые в свою очередь, как известно, изоморфны машинам Тьюринга . Этот метод исследования оказался успешным, и теперь компьютеры можно использовать для проверки доказательств математических и логических теорем.
По предложению Алонза Церковь , Emil Сообщение в статье , опубликованной в 1947 году, первый доказал «определенная проблема Туэ» неразрешимый, то , что Мартин Дэвис утверждает , как»... первое неразрешимости доказательства проблемы с классической математики - в данном случае слово «проблема» для полугрупп ». [10]
Дэвис также утверждает, что доказательство было независимо предложено А. А. Марковым . [11]
Смотрите также
- L-система
- MU головоломка
Заметки
- ^ Книга и Отто, стр. 36
- ^ Abramsky et al. п. 416
- ^ Саломаадр., P.444
- ^ В Книге и Отто система полутуэ определена над конечным алфавитом на протяжении большей части книги, за исключением главы 7, когда вводится моноидное представление, когда это предположение незаметно отбрасывается.
- ^ Книга и Отто, теорема 7.1.7, стр. 149
- ^ Нахум Дершовиц и Жан-Пьер Жуанно . Rewrite Systems (1990) стр. 6
- ^ DIA Cohen , Введение в теорию компьютеров, 2-е изд., Wiley-India, 2007, ISBN 81-265-1334-9 , стр.572
- ^ Дэн А. Симовичи, Ричард Л. Тенни, Теория формальных языков с приложениями , World Scientific, 1999 ISBN 981-02-3729-4 , глава 4
- ^ Дж. Бауш, Т. Кубитт, М. Озолс, Сложность трансляционно-инвариантных спиновых цепочек с низкой локальной размерностью , Ann. Анри Пуанкаре 18 (11), 2017 doi : 10.1007 / s00023-017-0609-7 стр. 3449-3513
- ^ Мартин Дэвис (редактор) (1965), Неразрешимое: Основные статьи о неразрешимых предложениях, неразрешимых проблемах и вычислимых функциях , после страницы 292, Raven Press , New York
- ↑ А. А. Марков (1947) Доклады Академии Наук СССР (НС) 55: 583–586.
Рекомендации
Монографии
- Рональд В. Бук и Фридрих Отто, Системы перезаписи строк , Springer, 1993, ISBN 0-387-97965-4 .
- Маттиас Янцен, Переписывание сливающихся строк , Birkhäuser, 1988, ISBN 0-387-13715-7 .
Учебники
- Мартин Дэвис , Рон Сигал, Элейн Дж. Вейкер, Вычислимость, сложность и языки: основы теоретической информатики , 2-е изд., Academic Press, 1994, ISBN 0-12-206382-1 , глава 7
- Элейн Рич, Автоматы, вычислимость и сложность: теория и приложения , Prentice Hall, 2007, ISBN 0-13-228806-0 , глава 23.5.
Обзоры
- Самсон Абрамски, Дов М. Габбей, Томас С.Е. Майбаум (редактор), Справочник по логике в компьютерных науках: семантическое моделирование , Oxford University Press, 1995, ISBN 0-19-853780-8 .
- Гжегож Розенберг, Арто Саломаа (редактор), Справочник по формальным языкам: слово, язык, грамматика , Springer, 1997, ISBN 3-540-60420-0 .
Ориентирные документы
- Эмиль Пост (1947) Рекурсивная неразрешимость проблемы Туэ , Журнал символической логики 12: 1–11 через проект Евклид .