Введение
Замена подтерма в формуле другим термом
В математике, информатике и логике переписывание охватывает широкий спектр методов замены подтермов формулы другими термами. Такие методы могут быть реализованы с помощью систем переписывания (также известных как системы редуцирования, механизмы переписывания или системы сокращения). В своей простейшей форме они состоят из множества объектов и отношений, определяющих способы преобразования этих объектов. Переписывание может быть недетерминированным. Одно правило переписывания может быть применено к терму различными способами, или к терму может быть применимо несколько правил. Системы переписывания, таким образом, не предоставляют алгоритм для преобразования одного терма в другой, а представляют собой набор возможных применений правил. Однако, в сочетании с соответствующим алгоритмом, системы переписывания можно рассматривать как компьютерные программы, и ряд систем доказательства теорем и декларативных языков программирования основаны на переписывании термов.
Лингвистика
В лингвистике правила структуры фраз, также называемые правилами переписывания, используются в некоторых системах генеративной грамматики как средство для порождения грамматически правильных предложений языка. Такое правило обычно имеет вид , где A – это метка синтаксической категории, например, именная группа или предложение, а X – последовательность таких меток или морфем, выражающая тот факт, что A может быть заменена на X при построении структуры составляющих предложения. Например, правило означает, что предложение может состоять из именной группы (NP), за которой следует глагольная группа (VP); дальнейшие правила уточняют, из каких подгрупп могут состоять именная и глагольная группы, и так далее.
Системы рескрипции абстрактных данных
Из приведенных выше примеров ясно, что системы переписывания можно рассматривать в абстрактном виде. Необходимо определить множество объектов и правила, которые могут быть применены для их преобразования. Наиболее общая (одномерная) постановка этого понятия называется абстрактной системой редукции или абстрактной системой переписывания (сокращенно ARS). ARS – это просто множество объектов A вместе с бинарным отношением → на A, называемым отношением редукции, отношением переписывания или просто редукцией.
Системы переписывания терминов
Система переписывания терминов (TRS) — это система переписывания, объектами которой являются термины — выражения с вложенными подвыражениями. Например, система, показанная выше, является системой переписывания терминов. Термины в этой системе состоят из бинарных операторов и и унарного оператора. В правилах также присутствуют переменные, представляющие любой возможный термин (однако одна и та же переменная всегда обозначает один и тот же термин в рамках одного правила). В отличие от систем переписывания строк, объектами которых являются последовательности символов, объекты системы переписывания терминов образуют алгебру терминов. Термин можно представить в виде дерева символов, множество допустимых символов которого фиксируется заданной сигнатурой. Как формализм, системы переписывания терминов обладают вычислительной мощностью, эквивалентной машинам Тьюринга, то есть любую вычислимую функцию можно определить с помощью системы переписывания терминов.
Формальное определение
Правило переписывания — это пара термов, обычно записываемая как , указывающая, что левая часть l может быть заменена правой частью r. Система переписывания термов — это множество R таких правил. Правило может быть применено к терму s, если левый терм l соответствует некоторому подтерму s, то есть существует такая подстановка , что подтерм s, находящийся в позиции p, является результатом применения подстановки к терму l. Подтерм, соответствующий левой части правила, называется редексом или редуцируемым выражением. Результат t применения этого правила — это результат замены подтерма в позиции p в s термом с примененной подстановкой , см. рисунок 1. В этом случае говорят, что переписывается за один шаг, или переписывается непосредственно, в системой , что формально обозначается как , , или, по некоторым источникам, как . Если терм можно переписать за несколько шагов в терм , то есть если , то говорят, что переписывается в , что формально обозначается как . Другими словами, отношение является транзитивным замыканием отношения ; часто также используется обозначение для обозначения рефлексивного транзитивного замыкания , то есть если или . Переписывание терма, заданное набором правил , можно рассматривать как абстрактную систему переписывания, определенную выше, с термами в качестве объектов и в качестве отношения переписывания. Например, — это правило переписывания, обычно используемое для приведения к нормальной форме относительно ассоциативности. Это правило можно применить к числителю в терме с соответствующей подстановкой , см. рисунок 2. Применение этой подстановки к правой части правила дает терм , а замена числителя этим термом дает , который является результатом применения правила переписывания. В целом, применение правила переписывания достигло того, что в элементарной алгебре называется «применением закона ассоциативности для ». В качестве альтернативы, правило можно было бы применить к знаменателю исходного терма, получив .
Системы переписывания более высокого порядка
Системы переписывания высшего порядка являются обобщением систем переписывания термов первого порядка для лямбда-термов, допускающих функции высшего порядка и связанные переменные. Многие результаты, полученные для систем переписывания термов первого порядка, могут быть переформулированы и для систем переписывания высшего порядка.
Системы переписывания графиков
Системы переписывания графов — это ещё одно обобщение систем переписывания термов, оперирующих графами вместо (базовых) термов / их соответствующего древовидного представления.
Системы переписывания следов
Теория следов предоставляет способ обсуждения многопроцессорности в более формальных терминах, например, с помощью следового моноида и моноида истории. Перезапись также может быть выполнена в следовых системах.