Лемма о ромбе

Лемма о ромбе (или лемма Ньюмана) даёт простой способ проверить сходимость переписывающей системы без убывающих бесконечных цепей. Доказана Максом Ньюманом в 1942 году. Стандартное доказательство использует нётерову индукцию.

Формулировка

схема доказательства леммы

Пусть $A$ — переписыващая система, то есть есть орграф. Наличие ребра из вершины $x$ в вершину $y$ будет обозначаться $x\to y$. Наличие направленного пути из $x$ в $y$ (включая путь нулевой длины) будет обозначаться $x⇝y$.

Предположим, что $A$

• нётерова, то есть не существует бесконечной цепи $x_0\to x_1\to \dots$
• локально конфлюентна, то есть если $x\to y$ и $x\to z$ то $y⇝w$ и $z⇝w$ для некоторого $w$.

Тогда система $A$ конфлюентна; то есть если $x⇝y$ и $x⇝z$ то $y⇝w$ и $z⇝w$ для некоторого $w$.

Литература

• M. H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43, Number 2, pages 223–243, 1942.
• Шаблон:Cite book
• Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003. (book weblink)
• Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998 (book weblink)
• John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009, Шаблон:ISBN, chapter 4 "Equality".

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

• Виктор Губа «Переписывающие системы»