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

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

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

Вступление

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

Например, если $E = {1\cdot x = x, x -1 \cdot x = 1, (x \cdot y) \cdot z = x \cdot (y \cdot z)}$ - аксиомы группы , цепочка вывода

а -1 \cdot (а \cdot б) ⁎ ⟷ E (a -1 \cdot a) \cdot b ⁎ ⟷ E 1\cdot б ⁎ ⟷ E б

показывает, что a ⁻¹ ⋅ ( a ⋅ b ) ⁎⟷E b является членом дедуктивного замыкания E. Если $R = {1\cdot x \to x, x -1 \cdot x \to 1, (x \cdot y) \cdot z \to x \cdot (y \cdot z)}$ является версией E «правила перезаписи» , цепочки вывода

(a -1 \cdot a) \cdot b ⁎ ⟶ р 1\cdot б ⁎ ⟶ р б и б ⁎ ⟵ р б

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

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

Правила

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

$s > е л$ , или
$с$ и $л$ в буквальном смысле похожи и $т > г$ .

Удалить	‹ E ∪ { s = s }	, R ›	⊢	‹ E	, R ›
Сочинять	‹ E	, R ∪ { s → t } ›	⊢	‹ E	, R ∪ { s → u } ›	если $т ⟶ р ты$
Упрощать	‹ E ∪ { s = t }	, R ›	⊢	‹ E ∪ { s = u }	, R ›	если $т ⟶ р ты$
Ориент	‹ E ∪ { s = t }	, R ›	⊢	‹ E	, R ∪ { s → t } ›	если $s > t$
Крах	‹ E	, R ∪ { s → t } ›	⊢	‹ E ∪ { u = t }	, R ›	если $с ⟶ р u$ на $l \to r$ с $(s \to t) ▻ (l \to r)$
Вывести	‹ E	, R ›	⊢	‹ E ∪ { s = t }	, R ›	если $(х, т)$ является критическим паром из R

Пример

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

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

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

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

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

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

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

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

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

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 неприводимо по системе перезаписи. Однако, в зависимости от правил, которые применяются при каждом W _i → W _{i + 1,} можно получить два разных неприводимых сокращения W _n ≠ W ' _m W. Однако, если система перезаписи, заданная отношениями, преобразуется к конфлюентной системе перезаписи с помощью алгоритма Кнута – Бендикса, то все сокращения гарантированно дают одно и то же несократимое слово, а именно нормальную форму этого слова.

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

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

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

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

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

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

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

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

Примеры

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

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

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

.

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

Таким образом, наши начальные три сокращения

{\ displaystyle x ^ {3} \ rightarrow 1}

( 1 )

{\ displaystyle y ^ {3} \ rightarrow 1}

( 2 )

{\ Displaystyle (ху) ^ {3} \ rightarrow 1}

.

( 3 )

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

{\ displaystyle yxyxy \ rightarrow x ^ {2}}

.

( 4 )

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

{\ displaystyle xyxyx \ rightarrow y ^ {2}}

.

( 5 )

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

Затем рассмотрим , совмещая ( 1 ) и ( 5 ). Уменьшение получаем , поэтому добавляем правило ${\ displaystyle x ^ {3} yxyx}$ ${\ Displaystyle yxyx = х ^ {2} у ^ {2}}$

{\ displaystyle yxyx \ rightarrow x ^ {2} y ^ {2}}

.

( 6 )

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

{\ Displaystyle у ^ {2} х ^ {2} \ rightarrow xyxy}

.

( 7 )

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

Теперь у нас осталась система перезаписи

{\ displaystyle x ^ {3} \ rightarrow 1}

( 1 )

{\ displaystyle y ^ {3} \ rightarrow 1}

( 2 )

{\ displaystyle yxyx \ rightarrow x ^ {2} y ^ {2}}

( 6 )

{\ Displaystyle у ^ {2} х ^ {2} \ rightarrow xyxy}

.

( 7 )

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

Непрерывный пример

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

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

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

Обобщения

Если Кнут – Бендикс не добьется успеха, он либо будет работать вечно, либо потерпит неудачу, когда встретит неориентируемое уравнение (т. Е. Уравнение, которое оно не может превратить в правило перезаписи). Улучшенное завершение без сбоев не приведет к отказу в неориентируемых уравнениях и обеспечивает процедуру полурешения для проблемы слов.

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

использованная литература

Д. Кнут; П. Бендикс (1970). Дж. Пиявка (ред.). Простые задачи со словами в универсальных алгебрах (PDF) . Pergamon Press. С. 263–297.
Жерар Юэ (1981). «Полное доказательство правильности алгоритма завершения Кнута-Бендикса» (PDF) . J. Comput. Syst. Sci . 23 (1): 11–21. DOI : 10.1016 / 0022-0000 (81) 90002-7 .
С. Симс. «Вычисления с конечно определенными группами». Кембридж, 1994.
Энн Хейворт и К.Д. Венсли. « Переписывание протоколов и идентификация родственников ». Группы Сент-Эндрюс 2001 г. в Оксфорде. Vol. I, 256–276, London Math. Soc. Lecture Note Ser., 304, Cambridge Univ. Press, Кембридж, 2003.

Languages

In other projects