Переписывание
В математике , информатике и логике переписывание охватывает широкий спектр методов замены подтерминов формулы другими терминами. Такие методы могут быть реализованы с помощью систем перезаписи (также известных как системы перезаписи , механизмы перезаписи [1] [2] или системы сокращения ). В своей самой простой форме они состоят из набора объектов, а также отношений о том, как преобразовать эти объекты.
Переписывание может быть недетерминированным . Одно правило перезаписи термина может быть применено к этому термину разными способами, или может быть применимо более одного правила. Таким образом, системы перезаписи предоставляют не алгоритм замены одного термина другим, а набор возможных приложений правил. Однако в сочетании с соответствующим алгоритмом системы перезаписи можно рассматривать как компьютерные программы , а некоторые средства доказательства теорем [3] и языки декларативного программирования основаны на переписывании терминов. [4] [5]
В логике процедура получения конъюнктивной нормальной формы (КСН) формулы может быть реализована в виде системы перезаписи. [6] Правилами примера такой системы могут быть:
где символ ( ) указывает, что выражение, соответствующее левой части правила, может быть переписано в выражение, образованное правой частью, а каждый символ обозначает подвыражение. В такой системе каждое правило выбирается таким образом, чтобы левая часть была эквивалентна правой части, и, следовательно, когда левая часть соответствует подвыражению, выполнение перезаписи этого подвыражения слева направо поддерживает логическую согласованность и значение всего выражения. .
Системы перезаписи терминов могут использоваться для вычисления арифметических операций над натуральными числами . Для этого каждое такое число должно быть закодировано как терм . Самая простая кодировка — та, что используется в аксиомах Пеано , основанная на константе 0 (нуле) и функции - преемнике S. например, числа 0, 1, 2 и 3 представлены терминами 0, S(0), S(S(0)) и S(S(S(0))) соответственно. Затем можно использовать следующий термин система перезаписи для вычисления суммы и произведения заданных натуральных чисел. [7]
В лингвистике правила построения фраз , также называемые правилами перезаписи , используются в некоторых системах порождающей грамматики [ 8] как средство создания грамматически правильных предложений языка. Такое правило обычно принимает форму , где А — метка синтаксической категории , такая как именное словосочетание или предложение , а Х — последовательность таких меток или морфем , выражающая тот факт, что А может быть заменена на Х при создании составной структуры слова. предложение. Например, правило означает, что предложение может состоять из именной фразы (NP), за которой следует глагольная фраза .(ВП); дальнейшие правила будут определять, из каких составных частей могут состоять именное и глагольное словосочетания, и так далее.
