11.3.1. Пример решения задачи с помощью FDS

Проиллюстрируем метод FDS задачей из школьной алгебры. Допустимые операторы даны в табл. 11.4.

Таблица 11.4. Правила переписывания для упрощенной алгебры

Для удобства чтения эти правила написаны и в обычной, и в бесскобочной записи. Программа же, конечно, работает только с бесскобочной записью.

Задача, которую нужно решить, состоит в доказательстве того, что

— правильный вывод. Фактически, когда есть только семь правил из табл. 11.4, это очень трудная задача. Советуем читателю, прежде чем идти дальше, попытаться решить ее самостоятельно. Это будет весьма поучительным упражнением.

Для удобства иллюстрации применяемого здесь алгоритма исходное состояние и происходящие из него состояния будем записывать непосредственно над конечным целевым состоянием. Вначале было

Программа устанавливает, что второй знак минус следует заменить переменной. Это можно сделать, применив правило ко всему выражению:

Теперь X нужно перевести в В путем простой замены, так как X — свободная переменная:

Знак нужно перевести в переменную А, но у нас нет правила, делающего это непосредственно. Однако требуемая переменная А является последним символом. Это пример различия, возникающего „в контексте". Подзадача превращения цепочки, начинающейся с в (19), в цепочку, к которой применимо правило поставлена. (Заметим, что п. п. в. начинается с любого места в цепочке.) Это подзадача

где — снова свободные переменные. Знак в (20) можно преобразовать в Можно осуществить это с помощью правила но применимо ли оно? Не ранее, чем (20) будет представлено в необходимом для этого виде. Возникает новая подзадача:

Поскольку и — свободные переменные, можно пользоваться подстановкой. Если положить , то задача сведется к

Правило можно применить к (22) и затем осуществить подстановку в (20). Цепочка принимает вид

Это все еще не соответствует требуемой форме, но после подстановки получаем

Третье В в верхней цепочке следует перевести в Это можно сделать, непосредственно применив правило к подцепочке, начинающейся с Поскольку

и

согласуются, целесообразны замены Использование правой части и подстановка дают цепочку вида

Сделав подстановку сравниваем всю цепочку. Следовательно, нижнюю цепочку в (26) можно заменить ее правой частью, т. е. просто и замена на его определение, т. е. А, приводит к

Задача решена.