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

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

Основные понятия[править | править код]

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

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

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

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

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

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

• Переписывающая система конфлюентна' если ${\displaystyle x\rightsquigarrow y}$ и ${\displaystyle x\rightsquigarrow z}$ то ${\displaystyle y\rightsquigarrow w}$ и ${\displaystyle z\rightsquigarrow w}$ для некоторого ${\displaystyle 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".

Внешние ссылки[править | править код]

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