Алгоритм завершения Кнута – Бендикса

Алгоритм завершения Кнута – Бендикса (названный в честь Дональда Кнута и Питера Бендикса). ) — полурешение алгоритм преобразования набора уравнений (над термовами ) в конфлюэнтную систему переписывания термов . Когда алгоритм успешен, он эффективно решает проблему слов для указанной алгебры .

Алгоритм Бухбергера для вычисления базисов Грёбнера — очень похожий алгоритм. Хотя он разработан независимо, его также можно рассматривать как реализацию алгоритма Кнута – Бендикса в теории колец полиномов .

Введение

Для набора E уравнений его дедуктивное замыкание ( ⁎ ⟷ E ) представляет собой набор всех уравнений, которые могут быть получены путем применения уравнений из E в любом порядке. Формально E считается бинарным отношением , ( ⟶ E ) — его замыканием перезаписи , а ( ⁎ ⟷ E ) — замыканием эквивалентности ( ⟶ E ). Для набора R правил перезаписи его дедуктивное замыкание ( ⁎ ⟶ R ∘ ⁎ ⟵ R ) представляет собой набор всех уравнений, которые можно подтвердить, применяя правила из R слева направо к обеим сторонам, пока они не станут буквально равными. Формально R снова рассматривается как бинарное отношение, ( ⟶ R ) — его переписывающее замыкание, ( ⟵ R ) — его обратное , и ( ⁎ ⟶ R ∘ ⁎ ⟵ R ) — композиция отношений их рефлексивных транзитивных замыканий ( ⁎ ⟶ Р и ⁎ ⟵ Р ).

Например, если E = {1⋅ x = x , x ⁻¹ ⋅ x = 1, ( x ⋅ y )⋅ z = x ⋅( y ⋅ z )} — аксиомы группы , цепочка вывода

а ⁻¹ ⋅( а ⋅ б ) ⁎ ⟷ Е ( а ⁻¹ ⋅ a )⋅ b   ⁎ ⟷ E   1⋅ b   ⁎ ⟷ E   b

демонстрирует, что ⁻¹ ⋅( a ⋅ b ) ⁎ ⟷ E b является членом E. дедуктивного замыкания Если R знак равно { 1⋅ Икс → Икс , Икс ⁻¹ ⋅ x → 1, ( x ⋅ y )⋅ z → x ⋅( y ⋅ z ) } — это версия E с «правилом перезаписи» , цепочки вывода

( а ⁻¹ ⋅ а )⋅ б   ⁎ ⟶ р 1⋅ б   ⁎ ⟶ р   б и б   ⁎ ⟵ р   б

продемонстрировать, что ( ⁻¹ ⋅ a )⋅ b ⁎ ⟶ R ∘ ⁎ ⟵ R b является членом R. дедуктивного замыкания Однако нет возможности получить ⁻¹ ⋅( a ⋅ b ) ⁎ ⟶ R ∘ ⁎ ⟵ R b аналогично предыдущему, поскольку применение правила справа налево ( x ⋅ y )⋅ z → x ⋅( y ⋅ z ) не допускается.

Алгоритм Кнута-Бендикса берет набор E уравнений между терминами и редукционный порядок (>) на множестве всех терминов и пытается построить конфлюэнтную и завершающую систему переписывания терминов R, которая имеет то же дедуктивное замыкание, что и E . В то время как доказательство последствий из E часто требует человеческой интуиции, доказательство последствий из R не требует. Для получения более подробной информации см. Confluence (абстрактное переписывание)#Мотивирующие примеры , где приводится пример доказательства из теории групп, выполненный как с использованием E так и с использованием R. ,

Правила

Учитывая набор E уравнений между терминами , следующие правила вывода могут быть использованы для преобразования его в эквивалентную сходящуюся систему перезаписи терминов (если возможно): Они основаны на заданном пользователем сокращении (>) набора всех терминов; его поднимают до обоснованного порядка (▻) на множестве правил перезаписи, определяя ( s → t ) ▻ ( l → r ), если

• s > e l в порядке охвата , или
• s и l похожи буквально и t > r .

Удалить	‹ E ∪{ s = s }	, Р ›	⊢	‹ Э	, Р ›
Сочинить	‹ Э	, р ∪{ s → t } ›	⊢	‹ Э	, р ∪{ s → ты } ›	если т ⟶ Р ты
Упрощать	‹ E ∪{ s знак равно т }	, Р ›	⊢	‹ E ∪{ s знак равно ты }	, Р ›	если т ⟶ Р ты
Восток	‹ E ∪{ s знак равно т }	, Р ›	⊢	‹ Э	, р ∪{ s → t } ›	если s > t
Крах	‹ Э	, р ∪{ s → t } ›	⊢	‹ E ∪{ ты знак равно т }	, Р ›	если s ⟶ р ты л ( → р с ( s → т ) ▻ л → р )
Делать вывод	‹ Э	, Р ›	⊢	‹ E ∪{ s знак равно т }	, Р ›	если ( s , t ) критическая пара R ​

Пример

Следующий пример, полученный с помощью средства доказательства теоремы E , вычисляет пополнение аксиом (аддитивной) группы, как в Knuth, Bendix (1970). Он начинается с трех исходных уравнений группы (нейтральный элемент 0, обратные элементы, ассоциативность), используя f(X,Y) для X + Y и i(X) для − X . 10 отмеченных звездочками уравнений образуют результирующую конвергентную систему перезаписи. «pm» — это сокращение от « парамодуляция », реализующее вывод . Вычисление критической пары - это пример парамодуляции для предложений эквациональных единиц. «rw» переписывает, реализует композицию , свертывание и упрощение . Ориентирование уравнений осуществляется неявно и не записывается.

Нет.		лев.		резус	Источник
1:	*	е(Х,0)	=	Х	начальный("GROUP.lop", at_line_9_column_1)
2:	*	f(X,i(X))	=	0	начальный("GROUP.lop", at_line_12_column_1)
3:	*	е(е(Х,Y),Z)	=	е(Х, е(Y,Z))	начальный("GROUP.lop", at_line_15_column_1)
5:		е(Х,Y)	=	е(Х, е(0,Y))	вечер(3,1)
6:		f(X,f(Y,i(f(X,Y))))	=	0	вечер(2,3)
7:		е(0,Y)	=	е(Х, е(я(Х),Y))	вечер(3,2)
27:		е(Х,0)	=	f(0,i(i(X)))	вечер(7,2)
36:		Х	=	f(0,i(i(X)))	рв(27,1)
46:		е(Х,Y)	=	f(X,i(i(Y)))	вечер(5,36)
52:	*	е(0,Х)	=	Х	рв(36,46)
60:	*	я (0)	=	0	вечер(2,52)
63:		я (я (Х))	=	е(0,Х)	вечер(46,52)
64:	*	е(Х, е(я(Х),Y))	=	И	рв(7,52)
67:	*	я (я (Х))	=	Х	рв(63,52)
74:	*	е(я(Х),Х)	=	0	вечера(2,67)
79:		е(0,Y)	=	е(я(Х),е(Х,Y))	вечер(3,74)
83:	*	И	=	е(я(Х),е(Х,Y))	рв(79,52)
134:		е(я(Х),0)	=	f(Y,i(f(X,Y)))	вечера(83,6)
151:		я (Х)	=	f(Y,i(f(X,Y)))	рв(134,1)
165:	*	е(я(Х),я(Y))	=	я(е(Y,X))	вечер(83,151)

См. также «Задача Word (математика)» для другого представления этого примера.

Системы переписывания строк в теории групп

Важным случаем в вычислительной теории групп являются системы переписывания строк, которые можно использовать для присвоения канонических меток элементам или смежным классам конечно представленной группы как продуктам генераторов . Этот особый случай находится в центре внимания данного раздела.

Мотивация в теории групп

Лемма о критической паре утверждает, что система переписывания терминов локально конфлюэнтна (или слабо конфлюэнтна) тогда и только тогда, когда все ее критические пары сходятся. Более того, у нас есть лемма Ньюмана , которая утверждает, что если (абстрактная) система переписывания является сильно нормализующей и слабо конфлюэнтной, то система переписывания конфлюэнтна. Итак, если мы сможем добавить правила к системе переписывания терминов, чтобы заставить все критические пары сходиться, сохраняя при этом свойство сильной нормализации, то это заставит результирующую систему переписывания быть конфлюэнтной.

Рассмотрим конечно определенный моноид $M=\langle X\mid R\rangle$ где X — конечное множество образующих, а R — множество определяющих соотношений на X. Пусть X ^* — множество всех слов из X (т.е. свободный моноид, порожденный X). Поскольку отношения R порождают отношение эквивалентности на X*, элементы M можно рассматривать как классы эквивалентности X ^* под R. Для каждого класса {w ₁ , w ₂ , ... } желательно выбрать стандартного представителя w _k . Этот представитель называется канонической или нормальной формой для каждого слова w _k в классе. Если существует вычислимый метод определения для каждого w _k его нормальной формы w _i, то проблема слов легко решается. Конфлюэнтная система переписывания позволяет сделать именно это.

Хотя выбор канонической формы теоретически может быть сделан произвольным образом, этот подход, как правило, не вычислим. (Учтите, что отношение эквивалентности в языке может порождать бесконечное количество бесконечных классов.) Если язык хорошо упорядочен , то порядок < дает последовательный метод определения минимальных представителей, однако вычисление этих представителей все равно может оказаться невозможным. В частности, если для вычисления минимальных представителей используется система переписывания, то порядок < также должен обладать свойством:

A < B → XAY < XBY для всех слов A,B,X,Y

Это свойство называется трансляционной инвариантностью . Порядок, который одновременно является трансляционно-инвариантным и вполне упорядоченным, называется порядком редукции .

Из представления моноида можно определить систему переписывания, заданную отношениями R. Если A x B находится в R, то либо A < B, и в этом случае B → A является правилом в системе переписывания, в противном случае A > B и A → B. Поскольку < является порядком сокращения, данное слово W можно привести W > W_1 > ... > W_n, где W_n неприводимо в системе переписывания. Однако в зависимости от правил, которые применяются при каждом Wi _→ Wi _i+1, можно получить две разные неприводимые редукции W _n ≠ W' _m из W. Однако, если система переписывания, заданная отношениями, преобразуется к конфлюэнтной системе переписывания с помощью алгоритма Кнута – Бендикса, то все сокращения гарантированно дадут одно и то же несократимое слово, а именно нормальную форму для этого слова.

Описание алгоритма для конечно представленных моноидов

Предположим, нам дали презентацию $\langle X\mid R\rangle$, где $X$ представляет собой набор генераторов и $R$ представляет собой набор отношений, задающих систему переписывания. Предположим далее, что у нас есть редукционный порядок $<$ среди слов, созданных $X$(например, шортлексный заказ ). Для каждого отношения $P_{i}=Q_{i}$ в $R$, предполагать $Q_{i}<P_{i}$. Итак, начнем с набора сокращений $P_{i}\rightarrow Q_{i}$.

Во-первых, если какое-либо отношение $P_{i}=Q_{i}$ можно уменьшить, заменить $P_{i}$ и $Q_{i}$ с сокращениями.

Далее мы добавляем дополнительные сокращения (то есть переписываем правила), чтобы исключить возможные исключения слияния. Предположим, что $P_{i}$ и $P_{j}$ перекрывать.

1. Случай 1: либо префикс $P_{i}$ соответствует суффиксу $P_{j}$, или наоборот. В первом случае мы можем написать $P_{i}=BC$ и $P_{j}=AB$; в последнем случае $P_{i}=AB$ и $P_{j}=BC$.
2. Случай 2: либо $P_{i}$ полностью содержится в (окруженном) $P_{j}$, или наоборот. В первом случае мы можем написать $P_{i}=B$ и $P_{j}=ABC$; в последнем случае $P_{i}=ABC$ и $P_{j}=B$.

Сократите слово $ABC$ с использованием $P_{i}$ сначала, затем с помощью $P_{j}$ первый. Назовите результаты $r_{1},r_{2}$, соответственно. Если $r_{1}\neq r_{2}$, то у нас есть случай, когда слияние может завершиться неудачно. Следовательно, добавьте сокращение $\max r_{1},r_{2}\rightarrow \min r_{1},r_{2}$ к $R$.

После добавления правила в $R$, удалите все правила в $R$ которые могут иметь приводимые левые части (после проверки, есть ли у таких правил критические пары с другими правилами).

Повторяйте процедуру до тех пор, пока не будут проверены все перекрывающиеся левые стороны.

Примеры

Завершающий пример

Рассмотрим моноид:

$\langle x,y\mid x^{3}=y^{3}=(xy)^{3}=1\rangle$.

Мы используем порядок shortlex . Это бесконечный моноид, но, тем не менее, алгоритм Кнута – Бендикса способен решить проблему слов.

Таким образом, наши первые три сокращения таковы:

$x^{3}\rightarrow 1$ ( 1 )

$y^{3}\rightarrow 1$ ( 2 )

$(xy)^{3}\rightarrow 1$. ( 3 )

Суффикс $x^{3}$ (а именно $x$) является префиксом $(xy)^{3}=xyxyxy$, поэтому рассмотрим слово $x^{3}yxyxy$. Сокращая с помощью ( 1 ), получаем $yxyxy$. Сокращая с помощью ( 3 ), получаем $x^{2}$. Следовательно, мы получаем $yxyxy=x^{2}$, давая правило редукции

$yxyxy\rightarrow x^{2}$. ( 4 )

Аналогично, используя $xyxyxy^{3}$ и сокращая с помощью ( 2 ) и ( 3 ), получаем $xyxyx=y^{2}$. Отсюда и сокращение

$xyxyx\rightarrow y^{2}$. ( 5 )

Оба эти правила устарели ( 3 ), поэтому мы их удалим.

Далее рассмотрим $x^{3}yxyx$ путем перекрытия ( 1 ) и ( 5 ). Сокращая, мы получаем $yxyx=x^{2}y^{2}$, поэтому мы добавляем правило

$yxyx\rightarrow x^{2}y^{2}$. ( 6 )

Учитывая $xyxyx^{3}$ перекрывая ( 1 ) и ( 5 ), мы получаем $xyxy=y^{2}x^{2}$, поэтому мы добавляем правило

$y^{2}x^{2}\rightarrow xyxy$. ( 7 )

Это устаревшие правила ( 4 ) и ( 5 ), поэтому мы их удалим.

Теперь у нас осталась система переписывания

$x^{3}\rightarrow 1$ ( 1 )

$y^{3}\rightarrow 1$ ( 2 )

$yxyx\rightarrow x^{2}y^{2}$ ( 6 )

$y^{2}x^{2}\rightarrow xyxy$. ( 7 )

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

Незавершающийся пример

Порядок генераторов может решающим образом повлиять на то, завершится ли пополнение Кнута – Бендикса. В качестве примера рассмотрим свободную абелеву группу по представлению моноида:

$\langle x,y,x^{-1},y^{-1}\,|\,xy=yx,xx^{-1}=x^{-1}x=yy^{-1}=y^{-1}y=1\rangle .$

Пополнение Кнута – Бендикса относительно лексикографического порядка. $x<x^{-1}<y<y^{-1}$ заканчивается конвергентной системой, однако с учетом длины-лексикографического порядка $x<y<x^{-1}<y^{-1}$ он не завершается, поскольку не существует конечных сходящихся систем, совместимых с этим последним порядком.

Обобщения

Если Кнут-Бендикс не преуспеет, он либо будет работать вечно и производить последовательные приближения к бесконечной полной системе, либо потерпит неудачу, когда встретит неориентируемое уравнение (т. е. уравнение, которое он не сможет превратить в правило перезаписи). Расширенная версия не дает сбоев в неориентируемых уравнениях и создает основную конфлюэнтную систему, предоставляя полуалгоритм для решения словесной задачи.

Идея протоколируемого переписывания, обсуждаемая в статье Хейворта и Уэнсли, указанной ниже, позволяет некоторую запись или протоколирование процесса переписывания по мере его прохождения. Это полезно для вычисления тождеств между отношениями для представлений групп.

Ссылки

• Д. Кнут; П. Бендикс (1970). Дж. Лич (ред.). Простые задачи со словами в универсальных алгебрах (PDF) . Пергамон Пресс. стр. 263–297.
• Жерар Юэ (1981). «Полное доказательство правильности алгоритма завершения Кнута-Бендикса» (PDF) . Дж. Компьютер. Сист. Наука . 23 (1): 11–21. дои : 10.1016/0022-0000(81)90002-7 .
• К. Симс. «Вычисления с конечно представленными группами». Кембридж, 1994.
• Энн Хейворт и CD Уэнсли. « Зарегистрированные переписывания и идентичности среди родственников ». Группы Сент-Эндрюс 2001 в Оксфорде. Том. I, 256–276, Лондонский математический институт. Соц. Лекции Сер., 304, Кембриджский университет. Пресс, Кембридж, 2003.

Внешние ссылки

• Вайсштейн, Эрик В. «Алгоритм завершения Кнута – Бендикса» . Математический мир .
• Визуализатор завершения работ Кнут-Бендикса