Трансформация замены хвостовой рекурсии циклом является весьма эффективной, поскольку устранение рекурсии позволяет провести подстановку определения на место вызова, после чего открывается возможность применения серии других оптимизирующих преобразований. Однако рекурсия в наиболее простом решении задачи обычно не является хвостовой. Существует ряд подходов по приведению рекурсии к хвостовому виду, как правило, автоматическими преобразованиями. Однако автоматическое приведение определения предиката к виду хвостовой рекурсии может быть оправдано лишь в том случае, когда все дальнейшие преобразования совершаются в автоматическом режиме. По нашей точке зрения, неправильно считать приведение к виду хвостовой рекурсии оптимизирующим преобразованием, реализуемым в процессе трансляции. Данное преобразование меняет алгоритм решения задачи, и поэтому должно применяться на стадии выбора алгоритма и программирования.
В качестве адекватной техники программирования предлагается универсальный метод обобщения исходной задачи для получения решения с хвостовой формой рекурсии. Этот метод часто оказывается ключевым для эффективной реализации предикатных программ.
Дадим иллюстрацию метода на примере 5.1 программы умножения через сложение. Как отмечено выше, рекурсия в программе (7.2) не является хвостовой, поскольку после рекурсивного вызова Умн(a – 1, b) в операторе c = b + Умн(a – 1, b) реализуется сложение с b. Чтобы сделать рекурсию хвостовой, необходимо внести сложение с b в рекурсивный вызов. Типичный прием - использование дополнительного параметра d в качестве накопителя при суммировании. Рассмотрим обобщенную задачу реализации умножения a * b через сложение с использованием накопителя d. Представим задачу следующим предикатом:
УмнO(nat a, b, d:nat c) prea ≥ 0 & b ≥ 0 & d ≥ 0 postc = a * b + d;
Тогда Умн(a, b: c) º УмнO(a, b, 0: c), и поэтому корректным является следующее определение предиката:
Умн(nat a, b: nat c) (7.3)
prea ≥ 0 & b ≥ 0
{ УмнO(a, b, 0: c) }
postc = a * b;
Формальное доказательство корректности (при очевидной однозначности и реализуемости) проводится доказательством истинности следующих правил, являющихся упрощенными аналогами правил LS8 и LS9.
Правило LSУ8. PУмн(a, b) ├ true (в качестве предусловия константы 0).
Правило LSУ9. PУмн(a, b) & QУмн(a, b, c)├ PУмнO(a, b, 0) & QУмнO(a, b, 0, c). □
Предикат УмнO имеет следующее определение:
УмнO(nat a, b, d: nat c) (7.4)
prea ≥ 0 & b ≥ 0 & d ≥ 0
{ if (a = 0) c = d else УмнO(a – 1, b, d + b: c) }
postc = a * b + d;
Доказательство корректности определения проводится так же, как и для определения Умн в примере 5.1 (см. разд. 5.5). □
Проиллюстрируем технику трансформации программы умножения, представленную определениями предикатов Умн и УмнO. На первом этапе применяется трансформация склеивания переменных. Аргумент d склеивается с результатом c, поскольку c информационно связан с d в обеих альтернативах условного оператора. Отметим, что дополнительная переменная, введенная при обобщении задачи, обычно подлежит склеиванию с некоторым результатом. Склеивание d с c будем обозначать c ¬ d. В результате склеивания получим следующее определение:
УмнO(nat a, b, c: nat c) { if (a = 0) c = c else УмнO(a – 1, b, с + b: c) } .
Далее применяется трансформация замены хвостовой рекурсии циклом
УмнO(nat a, b, c: nat c) {M: if (a = 0) else |a, b, c| = |a – 1, b, с + b|; goto M } .
После раскрытия группового оператора и оформления цикла получим
УмнO(nat a, b, c: nat c) {for (; a <> 0 ;) {a = a – 1; c = с + b} } . (7.5)
Последней является трансформация подстановки определения (7.5) на место вызова в (7.3). В соответствии с определением подстановки (7.1) получим:
|a, b, c| = | a, b, 0 |; for (; a <> 0 ;) {a = a – 1; c = с + b} .
Раскрывая групповой оператор, получим итоговую программу:
c = 0; for (; a <> 0 ;) {a = a – 1; c = с + b} .
Результатом проведенной серии трансформаций предикатной программы (7.3), (7.4) является представленная императивная программа, по качеству не хуже запрограммированной вручную. Разумеется, данная программа далеко не самая эффективная. В процессорах ЭВМ применяются более изощренные алгоритмы, использующие особенности двоичного представления чисел a и b. В предикатном программировании эффективность конечной программы в значительной степени зависит от выбора эффективного алгоритма, превращаемого в эффективную программу применением последовательности трансформаций.