Система Semi-Thue - Semi-Thue system

В теоретическом информатики и математической логике строка переписывания системы ( SRS ), исторически называется полу- Thue системой , является переписыванием системы над строками из (обычно конечного ) алфавита . Учитывая бинарное отношение между фиксированными строками над алфавитом, называемых переписать правилами , обозначаемых , ВКР расширяет переписывания отношения ко всем строкам , в которых левая и правая часть правила появляются как подстроки , то есть , где , , , и являются строками. ${\ displaystyle R}$ ${\ displaystyle s \ rightarrow t}$ ${\ displaystyle usv \ rightarrow utv}$ ${\ displaystyle s}$ ${\ displaystyle t}$ ${\ displaystyle u}$ ${\ displaystyle v}$

Понятие полусистемы Туэ по существу совпадает с представлением моноида . Таким образом, они составляют естественную основу для решения проблемы слов для моноидов и групп.

SRS можно определить непосредственно как абстрактную систему перезаписи . Это также можно рассматривать как ограниченный вид системы переписывания терминов . Как формализм, системы перезаписи строк являются полными по Тьюрингу . Название полу-Туэ происходит от норвежского математика Акселя Туе , который представил систематическую трактовку систем переписывания строк в статье 1914 года. Туэ ввел это понятие в надежде решить проблему слов для конечно определенных полугрупп. Лишь в 1947 году была показана неразрешимость проблемы - этот результат независимо друг от друга получили Эмиль Пост и А.А. Марков-младший.

Определение

Система перезаписи строк или система полу-Туэ - это кортеж, в котором ${\ Displaystyle (\ Sigma, R)}$

$Σ$ - это алфавит, обычно предполагаемый конечным. Элементы множества (здесь * - звезда Клини ) - это конечные (возможно, пустые) строки на $Σ$ , иногда называемые словами в формальных языках ; мы будем называть их здесь просто строками. ${\ displaystyle \ Sigma ^ {*}}$
$R$ - это бинарное отношение на строках из $Σ$ , то есть каждый элемент называется правилом (перезаписи) и обычно записывается . ${\ Displaystyle R \ substeq \ Sigma ^ {*} \ times \ Sigma ^ {*}.}$ ${\ displaystyle (u, v) \ in R}$ ${\ displaystyle u \ rightarrow v}$

Если отношение $R$ является симметричным , то система называется системой Туэ- .

Переписывание правил в $R$ может быть естественным образом распространяется на другие строки в позволяя подстроки быть переписаны в соответствии с $R$ . Более формально, одноэтапное переписывающее отношение отношения, индуцированное $R$ on для любых строк : ${\ displaystyle \ Sigma ^ {*}}$ ${\ displaystyle {\ xrightarrow [{R}] {}}}$ ${\ displaystyle \ Sigma ^ {*}}$ ${\ displaystyle s, т \ in \ Sigma ^ {*}}$

{\ displaystyle s {\ xrightarrow [{R}] {}} t}

тогда и только тогда , когда существуют такие , что , , и .

{\ Displaystyle х, у, и, v \ in \ Sigma ^ {*}}

{\ displaystyle s = xuy}

{\ displaystyle t = xvy}

{\ displaystyle u \ rightarrow v}

Поскольку есть отношение on , эта пара соответствует определению абстрактной системы перезаписи . Очевидно, что $R$ является подмножеством . Некоторые авторы используют различные обозначения для стрелки в (например ) для того , чтобы отличить его от $R$ самого ( ) , потому что они потом хотят , чтобы иметь возможность опускать индекс и до сих пор избежать путаницы между $R$ и одностадийного переписывание индуцированного $R$ . ${\ displaystyle {\ xrightarrow [{R}] {}}}$ ${\ displaystyle \ Sigma ^ {*}}$ ${\ Displaystyle (\ Sigma ^ {*}, {\ xrightarrow [{R}] {}})}$ ${\ displaystyle {\ xrightarrow [{R}] {}}}$ ${\ displaystyle {\ xrightarrow [{R}] {}}}$ ${\ displaystyle {\ xrightarrow [{R}] {}}}$ ${\ displaystyle \ rightarrow}$

Ясно, что в системе полутуэ мы можем сформировать (конечную или бесконечную) последовательность строк, полученную, начиная с начальной строки и многократно переписывая ее, производя по одной замене подстроки за раз: ${\ displaystyle s_ {0} \ in \ Sigma ^ {*}}$

{\ Displaystyle s_ {0} \ {\ xrightarrow [{R}] {}} \ s_ {1} \ {\ xrightarrow [{R}] {}} \ s_ {2} \ {\ xrightarrow [{R}] {}} \ \ ldots}

Нулевой или-больше-шаги переписывания как это захватывается рефлексивным транзитивным замыканием на , обозначаемом (см абстрактной системы переписывания # Основных понятия ). Это называется переписыванием отношения или уменьшения отношения на индуцированный $R$ . ${\ displaystyle {\ xrightarrow [{R}] {}}}$ ${\ displaystyle {\ xrightarrow [{R}] {*}}}$ ${\ displaystyle \ Sigma ^ {*}}$

Thue congruence

В общем, множество строк на алфавите образует свободный моноид вместе с бинарной операцией из конкатенации (обозначаются как и мультипликативная запись, опуская символ). В SRS отношение сокращения совместимо с операцией моноида, что означает , что это подразумевается для всех строк . Поскольку по определению является предварительным заказом , образует моноидальный предварительный заказ . ${\ displaystyle \ Sigma ^ {*}}$ ${\ displaystyle \ cdot}$ ${\ displaystyle {\ xrightarrow [{R}] {*}}}$ ${\ displaystyle x {\ xrightarrow [{R}] {*}} y}$ ${\ displaystyle uxv {\ xrightarrow [{R}] {*}} uyv}$ ${\ Displaystyle х, у, и, v \ in \ Sigma ^ {*}}$ ${\ displaystyle {\ xrightarrow [{R}] {*}}}$ ${\ displaystyle \ left (\ Sigma ^ {*}, \ cdot, {\ xrightarrow [{R}] {*}} \ right)}$

Аналогичным образом , рефлексивный транзитивен симметричное замыкание из , обозначается (см система абстрактных переписывание # Основные понятия ), является конгруэнтность , а это означает , что это отношение эквивалентности (по определению) , и он также совместим с конкатенации. Соотношение называется Туэ конгруэнтность , порожденный $R$ . В системе Туэ, т. Е. Если $R$ симметрично, отношение переписывания совпадает с конгруэнцией Туэ . ${\ displaystyle {\ xrightarrow [{R}] {}}}$ ${\ displaystyle {\ overset {*} {\ underset {R} {\ leftrightarrow}}}}$ ${\ displaystyle {\ overset {*} {\ underset {R} {\ leftrightarrow}}}}$ ${\ displaystyle {\ xrightarrow [{R}] {*}}}$ ${\ displaystyle {\ overset {*} {\ underset {R} {\ leftrightarrow}}}}$

Факторные моноиды и представления моноидов

Так как это сравнение, мы можем определить коэффициент моноид в свободном моноиде по конгруэнции Туэ в обычном порядке . Если моноидом является изоморфными с , то система полу-Thue называется моноидное представление о . ${\ displaystyle {\ overset {*} {\ underset {R} {\ leftrightarrow}}}}$ ${\ displaystyle {\ mathcal {M}} _ {R} = \ Sigma ^ {*} / {\ overset {*} {\ underset {R} {\ leftrightarrow}}}}$ ${\ displaystyle \ Sigma ^ {*}}$ ${\ Displaystyle {\ mathcal {M}}}$ ${\ displaystyle {\ mathcal {M}} _ {R}}$ ${\ Displaystyle (\ Sigma, R)}$ ${\ Displaystyle {\ mathcal {M}}}$

Мы сразу получаем очень полезные связи с другими областями алгебры. Например, алфавит { a , b } с правилами { ab → ε, ba → ε}, где ε - пустая строка , представляет собой представление свободной группы на одном образующем. Если вместо этого правила просто { ab → ε}, то мы получаем представление бициклического моноида .

Важность систем полу-Туэ как представления моноидов усиливается следующим:

Теорема : каждый моноид имеет представление формы , таким образом, он всегда может быть представлен полусистемой Туэ, возможно, над бесконечным алфавитом. ${\ Displaystyle (\ Sigma, R)}$

В связи с этим, набор называется множество образующих в , и называется набор определяющих соотношений . Мы можем сразу классифицировать моноиды на основе их представления. называется ${\ displaystyle \ Sigma}$ ${\ Displaystyle {\ mathcal {M}}}$ ${\ displaystyle R}$ ${\ Displaystyle {\ mathcal {M}}}$ ${\ Displaystyle {\ mathcal {M}}}$

конечно порожденный, если конечно. ${\ displaystyle \ Sigma}$
конечно представленный, если оба и конечны. ${\ displaystyle \ Sigma}$ ${\ displaystyle R}$

Проблема слов для систем полу-Туэ

Проблема слов для систем полутуэ может быть сформулирована следующим образом: данная система полутуэ и два слова (строки) могут быть преобразованы в , применяя правила из ? Эта проблема неразрешима , т.е. нет общего алгоритма решения этой проблемы. Это справедливо даже в том случае, если мы ограничим ввод конечными системами. ${\ Displaystyle T: = (\ Sigma, R)}$ ${\ Displaystyle и, v \ in \ Sigma ^ {*}}$ ${\ displaystyle u}$ ${\ displaystyle v}$ ${\ displaystyle R}$

Мартин Дэвис предлагает обычному читателю двухстраничное доказательство в своей статье «Что такое вычисления?» С. 258–259 с комментарием с. 257. Дэвис приводит доказательство следующим образом: «Придумайте [словесную проблему], решение которой привело бы к решению проблемы остановки ».

Связи с другими понятиями

Система полу-Туэ также является системой перезаписи терминов , в которой есть монадические слова (функции), оканчивающиеся той же переменной, что и левые и правые части, например, правило термина эквивалентно правилу строки . ${\ displaystyle f_ {2} (f_ {1} (x)) \ rightarrow g (x)}$ ${\ displaystyle f_ {1} f_ {2} \ rightarrow g}$

Система полутхуэ также является особым типом канонической системы Post , но каждая каноническая система Post также может быть сведена к SRS. Оба формализма Тьюринг , и , таким образом эквивалентен Хомский «ы неограниченные грамматики , которые иногда называют пол-Туэ грамматик . Формальная грамматика только отличается от полу-Туэ системы путем разделения алфавита в терминалах и не-терминалов, а также фиксации исходного символа среди не-терминалов. Меньшая часть авторов фактически определяет систему полутуэ как тройку , которая называется набором аксиом . Согласно этому «порождающему» определению системы полу-Туэ, неограниченная грамматика - это просто система полу-Туэ с единственной аксиомой, в которой алфавит разбивается на терминальные и нетерминальные и делает аксиому нетерминальной. Простая уловка разделения алфавита на терминалы и нетерминалы - очень мощный прием; он позволяет определять иерархию Хомского на основе того, какую комбинацию терминалов и нетерминалов содержат правила. Это было решающим достижением в теории формальных языков . ${\ Displaystyle (\ Sigma, A, R)}$ ${\ Displaystyle А \ substeq \ Sigma ^ {*}}$

В квантовых вычислениях можно развить понятие квантовой системы Туэ. Поскольку квантовые вычисления по своей сути обратимы, правила перезаписи по алфавиту должны быть двунаправленными (т. Е. Лежащая в основе система является системой Туэ, а не полусистемой Туэ). На подмножестве символов алфавита можно присоединить гильбертово пространство , а правило перезаписи, переводящее одну подстроку в другую, может выполнять унитарную операцию над тензорным произведением гильбертова пространства, присоединенного к строкам; это означает, что они сохраняют количество символов из набора . Подобно классическому случаю, можно показать, что квантовая система Туэ представляет собой универсальную вычислительную модель для квантовых вычислений в том смысле, что выполняемые квантовые операции соответствуют унифицированным классам схем (например, в BQP, когда, например, гарантируется завершение правил перезаписи строки в пределах полиномиально большого количества шагов от входного размера) или, что то же самое, квантовой машины Тьюринга . ${\ displaystyle \ Sigma}$ ${\ Displaystyle Q \ substeq \ Sigma}$ ${\ Displaystyle \ mathbb {C} ^ {d}}$ ${\ displaystyle Q}$

История и значение

Системы Semi-Thue были разработаны как часть программы для добавления дополнительных конструкций в логику , чтобы создать такие системы, как логика высказываний , которые позволили бы выразить общие математические теоремы на формальном языке , а затем доказать и проверить их в автоматическом режиме. , механическая мода. Была надежда, что затем акт доказательства теорем можно свести к набору определенных манипуляций с набором строк. Впоследствии выяснилось, что системы полу-Туэ изоморфны неограниченным грамматикам , которые в свою очередь, как известно, изоморфны машинам Тьюринга . Этот метод исследования оказался успешным, и теперь компьютеры можно использовать для проверки доказательств математических и логических теорем.

По предложению Алонза Церковь , Emil Сообщение в статье , опубликованной в 1947 году, первый доказал «определенная проблема Туэ» неразрешимый, то , что Мартин Дэвис утверждает , как»... первое неразрешимости доказательства проблемы с классической математики - в данном случае слово «проблема» для полугрупп ».

Дэвис также утверждает, что доказательство было независимо предложено А. А. Марковым .

Смотрите также

Заметки

Ссылки

Монографии

Рональд В. Книга и Фридрих Отто, Системы перезаписи строк , 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 .

Landmark документы

Эмиль Пост (1947) Рекурсивная неразрешимость проблемы Туэ , Журнал символической логики 12: 1–11 через проект Евклид .

Languages

In other projects