Переписывающая система (или 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. . — Warwick University, England : Springer, 1990. — Vol. 443. — ISBN 978-3-540-52826-5 .
• Term Rewriting Systems , Terese, Cambridge Tracts in Theoretical Computer Science, 2003.
• Term Rewriting and All That , Franz Baader and Tobias Nipkow, Cambridge University Press, 1998
• John Harrison, Handbook of Practical Logic and Automated Reasoning , Cambridge University Press, 2009, ISBN 978-0-521-89957-4 , chapter 4 "Equality".

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