Переписывающая система

Переписывающая система (или ARS от Шаблон:Lang-en) — набор объектов вместе с правилами замены одного объекта на другой.

Основные понятия

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

В теории переписывающих систем интересуются отношением $\to$ и его свойствами. При этом оказываются важными следующие понятия и отношения.

• $⇝$ является рефлексивным транзитивным замыканием $\to$, то есть транзитивным замыканием $(\to )\cup (=)$. Эквивалентно, $⇝$ это наименьший предпорядок, содержащий $\to$.
• $\sim$ является рефлексивным транзитивным симметричным замыканием $\to$, то есть транзитивным замыканием $(\leftrightarrow )\cup (=)$.

• Объект $x$ в переписывающей системе $A$ называется приводимым, если существует какой-либо другой $y$ в $A$ и $x\to y$; в противном случае он называется неприводимым или нормальной формой.
  • Объект $y$ называется нормальной формой $x$, если $x⇝y$ и $y$ неприводим.
  • Если $x$ имеет единственную нормальную форму, то она обычно обозначается $[x]$.
  • Если каждый объект имеет по крайней мере одну нормальную форму, то переписывающая система называется нормализующей.

• Переписывающая система называется нётеровой если в ней не существует бесконечной цепи $x_0\to x_1\to \dots$

Пример локально сонфлюентной, но не конфлюентной системы.

• Переписывающая система локально конфлюентна если $x\to y$ и $x\to z$ то $y⇝w$ и $z⇝w$ для некоторого $w$.

• Переписывающая система конфлюентна' если $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".

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

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