Канонические системы

5.1. Канонические системы

Порождения — это в действительности грамматические правила манипулирования строками символов и потому их иногда называют правилами переписывания (rewrite rules). Пост изучал свойства систем правил, базирующихся на порождениях, которые он назвал каноническими системами [Post, 1943]. Каноническая система — это разновидность формальной системы, основанной на следующих компонентах:

• алфавит А, из символов которого формируются строки;
  
• некоторое множество строк, которые рассматриваются как аксиомы,
  
• множества порождений в форме
  

а1$1 ... am$m->b1$'1...bn$'1...bn$'n.

где

(I) каждое ai и bi; есть фиксированная строка;

(II) а1 и am, часто есть нуль;

(III) некоторые или все из ai или bi могут представлять собой нуль;

(IV) каждое $i является переменной строкой, которая также может быть нулем;

(V) каждое $i заменяется определенным $'i .

Определение канонической системы, возможно, станет более понятным, если привести пример. Пусть А — алфавит {а, b, с}, а аксиомы суть:

а, b, с, аа, bb, cc.

Тогда следующие порождения сгенерируют все палиндромы, базирующиеся на этом алфавите, приняв за отправную точку имеющиеся аксиомы:

(Р1)$->а$a (Р2) $ -> ab$ab (РЗ) $ -> с$с.

Более того, в данном случае можно проследить применение правил, которые должны привести к росту определенного палиндрома. Например, чтобы сгенерировать bacab, нужно применить Р1 к аксиоме с, а затем Р2 — к результату. Другими словами, приняв с в качестве аксиомы, можно вывести из нее теорему аса и добавить ее к имеющимся аксиомам. Затем из аса можно вывести новую теорему bacab. Обратите внимание, что эта последовательность порождений не обладает свойством коммутативности, т.е. если применять те же правила, но в ином порядке, получится совсем другой результат. Например, если к аксиоме с применить сначала правило Р2, а затем Р1, то получим abcba.

На первый взгляд канонические системы довольно тривиальны. Все, что можно сделать в рамках такой системы, — преобразовать одну строку символов в другую. Но если задуматься, то любое логическое или математическое исчисление в конце концов сводится к набору правил манипулирования символами. Мы упускаем это из виду, поскольку для нас часто важен определенный смысл логических и математических символов, чего не скажешь о строках типа abcba.

Отсюда следует, что любая формальная система может рассматриваться как каноническая (см., например, [Minsky, 1972, Chapter 12J). В действительности к этому нужно добавить тривиальную оговорку, что такая система может нуждаться еще в дополнительном алфавите, буквы которого будут использоваться в качестве знаков пунктуации в сложных доказательствах. Таким образом, для проверки доказательства в любой формальной системе или для того, чтобы выполнить любую эффективную процедуру, вполне достаточно способности прочесть строку символов, разделить ее на компоненты и переупорядочить (при этом, возможно, придется добавить еще какие-то символы или удалить существующие в исходной строке).