WikiDer > Лемма Ньюмана - Википедия

В математика, в теории переписывание системы, Ньюмана лемма, также обычно называемый алмазная лемма, заявляет, что прекращение (или сильно нормализующий) абстрактная система переписывания (ARS), то есть та, в которой нет бесконечных редукционных последовательностей, является сливаться если это локально сливной. На самом деле завершающийся ARS сливается именно когда он локально сливается.^[1]

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

Сегодня это рассматривается как чисто комбинаторный результат, основанный на обоснованность из-за доказательства Жерар Юэ в 1980 г.^[2] Первоначальное доказательство Ньюмана было значительно сложнее.^[3]

Алмазная лемма

Доказательство идеи (прямые и волнистые линии обозначают → и ∗→, соответственно):
Данный т₁ ∗←т∗→т₂, произведем индукцию по длине вывода. Получать т′ от местного слияния, и т′′ из предположения индукции; аналогично для т′′′.

В общем, лемму Ньюмана можно рассматривать как комбинаторный результат о бинарных отношениях → на множестве А (написано наоборот, чтобы а → б Значит это б ниже а) со следующими двумя свойствами:

• → это обоснованные отношения: каждое непустое подмножество Икс из А имеет минимальный элемент (элемент а из Икс такой, что а → б нет б в Икс). Эквивалентно не существует бесконечной цепочки а₀ → а₁ → а₂ → а₃ → .... В терминологии систем перезаписи → означает завершение.
• Каждое покрытие ограничено снизу. То есть, если элемент а в А покрывает элементы б и c в А в том смысле, что а → б и а → c, то есть элемент d в А такой, что б ∗→ d и c ∗→ d, куда ∗→ обозначает рефлексивный переходное закрытие из →. В терминологии систем перезаписи → является локально сливающимся.

Если два вышеуказанных условия выполнены, то лемма утверждает, что → конфлюэнтно: всякий раз, когда а ∗→ б и а ∗→ c, есть элемент d такой, что б ∗→ d и c ∗→ d. Ввиду прекращения действия → это означает, что каждая связная компонента → как графа содержит единственный минимальный элемент а, более того б ∗→ а для каждого элемента б компонента.^[4]

Примечания

Рекомендации

• М. Х. А. Ньюман. О теориях с комбинаторным определением «эквивалентности». Анналы математики, 43, номер 2, страницы 223–243, 1942.
• Патерсон, Майкл С. (1990). Автоматы, языки и программирование: 17-й международный коллоквиум. Конспект лекций по информатике. 443. Уорикский университет, Англия: Springer. ISBN 978-3-540-52826-5.

Учебники

• Системы перезаписи терминов, Тереза, Кембриджский трактат по теоретической информатике, 2003. (ссылка на книгу)
• Перезапись терминов и все такое, Франц Баадер и Тобиас Нипков, Cambridge University Press, 1998 г. (ссылка на книгу)
• Джон Харрисон, Справочник по практической логике и автоматизированному мышлению, Издательство Кембриджского университета, 2009 г., ISBN 978-0-521-89957-4, глава 4 «Равенство».

внешняя ссылка

• Алмазная лемма в PlanetMath.
• PDF на исходной пробе, В архиве 6 июля 2017 г. Wayback Machine[Позиционные параметры игнорируются]