Переписывающая система (или ARS от ) — набор объектов вместе с правилами замены одного объекта на другой.
Основные понятия
Переписывающую систему обычно определяют как ориентированный граф (возможны петли и кратные рёбра). Однако вершины графа принято называть объектами. Наличие ребра из объекта на объект обычно обозначается как и интерпретируется как возможность заменить объект на объект .
В теории переписывающих систем интересуются отношением и его свойствами. При этом оказываются важными следующие понятия и отношения.
является рефлексивным транзитивным замыканием , то есть транзитивным замыканием . Эквивалентно, это наименьший предпорядок, содержащий . является рефлексивным транзитивным симметричным замыканием , то есть транзитивным замыканием .
Объект в переписывающей системе называется приводимым, если существует какой-либо другой в и ; в противном случае он называется неприводимым или нормальной формой. Объект называется нормальной формой , если и неприводим. Если имеет единственную нормальную форму, то она обычно обозначается . Если каждый объект имеет по крайней мере одну нормальную форму, то переписывающая система называется нормализующей.
Переписывающая система называется нётеровой если в ней не существует бесконечной цепи
Переписывающая система локально конфлюентна если и то и для некоторого .
Переписывающая система конфлюентна' если и то и для некоторого .
Свойства Лемма о ромбе утверждает, что нётерова локально конфлюентная система конфлюентна.
Литература
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".
Внешние ссылки Виктор Губа «Переписывающие системы»
Категория:Логика в информатике Категория:Теория формальных языков