Лемма о ромбе (также лемма Нью́мана) даёт простой способ проверить сходимость переписывающей системы без убывающих бесконечных цепей. Доказана Максом Ньюманом в 1942 году. Стандартное доказательство использует нётерову индукцию.
Формулировка
Пусть — переписыващая система, то есть ориентированный граф. Наличие ребра из вершины в вершину будет обозначаться . Наличие направленного пути из в (включая путь нулевой длины) будет обозначаться .
Предположим, что нётерова, то есть не существует бесконечной цепи локально конфлюентна, то есть если и то и для некоторого . Тогда система конфлюентна; то есть если и то и для некоторого .
Литература
M. H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43, Number 2, pages 223–243, 1942.
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, , chapter 4 "Equality".
Внешние ссылки Виктор Губа «Переписывающие системы»
Категория:Леммы Категория:Теория графов Категория:Теория формальных языков