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

Переписывающая система (или ARS от англ. Abstract rewriting system) — набор объектов вместе с правилами замены одного объекта на другой.

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

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

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

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

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

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

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

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

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

Свойства

• Лемма о ромбе утверждает, что нётерова локально конфлюентная система конфлюентна.

Литература

• M. H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43, Number 2, pages 223–243, 1942.
• Paterson, Michael S. Automata, languages, and programming: 17th international colloquium. — Warwick University, England : Springer, 1990. — Vol. 443. — ISBN 978-3-540-52826-5.
• 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 978-0-521-89957-4, chapter 4 "Equality".

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

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