Цитата:
Алгоритм всегда решает какую-то задачу. Вы же пока рассуждаете о каких-то абстрактных алгоритмах без привязки к задаче. Сформулируйте свою задачу чётче: что именно вам дано, что вы хотите получить, каким свойствам должно удовлетворять решение (алгоритм) и т.д.
Хорошо. Начну с общей постановки проблемы, а затем постепенно перейду к частным задачам.
Конечная цель состоит в том, чтобы язык математической логики сделать предметом (адекватного) математического исследования.
В литературе можно найти три способа отношения к этой задаче.
1. Язык математической логики существует в виде записи на бумаге и не является предметом математического исследования. Все свойства и закономерности языка очевидны для тех, кто им пользуется.
2. Язык математической логики определятся рекурсивно в рамках теории множеств исходя из данного бесконечного алфавита. Все свойства и закономерности языка доказываются как теоремы теории множеств. В частности, доказывается существования функций (определенных на множестве всех выражений), которые осуществляют те или иные преобразования, подстановки или замены.
3. Язык математической логики, или близкий ему язык моделируется на компьютере, например, на языке C++ для создания математических пакетов символьных вычислений, подобных Mathematica. Или же в самой Mathematica на языке программирования высокого порядка пишутся алгоритмы формульных преобразований.
Перечисленные подходы я считаю неадекватными. На мой взгляд, адекватным методом исследования формального языка должна быть конструктивная математика, в которой алгоритмами являются или машины Тьюринга, или нормальные алогорифмы Маркова, или канонические системы Поста. Для определенности выберем машины Тьюринга с двухбуквенным алфавитом. Таким образом, первое условие нашей задачи: представляем выражения формального языка линейной последовательностью, состоящей из двух символов 0 и |, а все свойства и преобразования выражений осуществляется путем построения соответствующих машин Тьюринга: 1)разрешающих это свойство (или выражения относительно этого свойства); 2) преобразующие выражения.
Вторым условием будет требование отсутствия в формальном языке символов пунктуации, а именно скобок и запятых.
Для еще большей конкретизации рассмотрим следующий формальный язык. Алфавит состоит из счетного числа символов, обозначающих предметные переменные, и счетного числа функциональных символов для каждого ранга, принимающего счетное число значений, начиная с единицы. Рекурсивное определение формальных выражений в этом языке очевидно. На нулевом шаге это все переменные. На следующем шаге это последовательности, начинающиеся с функционального символа, за которым стоят столько выражений из уже определенных выражений на предыдущих шагах, каков ранг этого функционального символа.
То, что было сказано в предыдущем абзаце, это интуитивное понимание. Мы должны это понимание воплотить в конструктивной математике. Введем сокращения для упрощения изложения. Последовательность 0| будем обозначать 1, последовательность 0|| будем обозначать 2, последовательность 0||| будем обозначать 3 и так далее. Будем использовать переменные m и n для обозначения произвольной последовательности вида 0|||...
Последовательность 0|0||0||| будем обозначать 1, 2, 3.
Последовательность 00|0||0||| будем обозначать (1, 2, 3).
Предметные переменные исходного алфавита в конструктивной математике будем представлять последовательностью вида (m) .
Функциональные символы ранга n будем обозначать последовательностью вида (n,m). В частности, правильным выражением будет последовательности вида (2,1)(1)(1), (3,1)(3)(2)(1).
Итак, возникает первая конкретная задача. Построить машину Тьюринга, которая перечисляет все правильные выражения. Возникает вторая задача. Построить машину Тьюринга, которая для любой последовательности дает |, если последовательность представляет правильное выражение, и 0 — в противном случае.
Далее очевидно возникает задача построения машин Тьюринга, которая по данному правильному выражению выдают ее древовидную структуру, представленную в виде определенного дерева. Затем возникает задача построения машины Тьюринга, которая по данной последовательности, представляющей правильное выражение, и последовательности, представляющей место в ее древовидной структуре, и другого выражения выдает новое выражение, в котором произошла замена подвыаржения, стоящего на указанном месте, данным выражением. И так далее и тому подобное.
Хотелось бы прежде всего узнать, в каких книгах эти или близкие им задачи рассматриваются. Буду также рад любым комментариям.