Доказательство правила верификации рекурсивных процедур

💸 Как сделать бизнес проще, а карман толще?

Тот, кто работает в сфере услуг, знает — без ведения записи клиентов никуда. Мало того, что нужно видеть свое раписание, но и напоминать клиентам о визитах тоже. Проблема в том, что средняя цена по рынку за такой сервис — 800 руб/мес или почти 15 000 руб за год. И это минимальный функционал. Нашли самый бюджетный и оптимальный вариант: сервис VisitTime.
⚡️ Для новых пользователей первый месяц бесплатно. А далее 290 руб/мес, это в 3 раза дешевле аналогов. За эту цену доступен весь функционал: напоминание о визитах, чаевые, предоплаты, общение с клиентами, переносы записей и так далее.
✅ Уйма гибких настроек, которые помогут вам зарабатывать больше и забыть про чувство «что-то мне нужно было сделать».
Сомневаетесь? нажмите на текст, запустите чат-бота и убедитесь во всем сами!

Правило верификации применяется к процедурному оператору P процедуры без параметров и с одним рекурсивным вызовом, имея рекурсивное уравнение P = M (P). Функция f = P если и только если

2. f является решением рекурсивного уравнения.

Направление доказательства “только если” тривиально, потому что P удовлетворяет обоим условиям, следовательно, удовлетворяет и f = P.

Для другого направления примем условия 1) и 2). Рассмотрим любое s Î domain(P). Когда правая сторона рекурсивного уравнения применяется к s, к тому времени как будет применена собственно P, состояние выполнения может быть изменено (другими операторами в M(P)) в s’. При вычислении P(s’) снова используется правая часть рекурсивного уравнения и продолжается процесс вычисления частей M(P) и замены в правой части рекурсивного уравнения всякий раз, когда P применяется к измененному состоянию выполнения. Процесс не может продолжаться бесконечно, потому что P определено на s, рекурсия должна завершиться. То есть после (скажем, k) замен в правой части рекурсивного уравнения, часть M(P), включающая P не встретится, и вычисление результирующего состояния сможет быть вычислено. То есть, объединяя эти замены в k-местное применение модификации M,

где при получении состояния t не применялось P.

Теперь рассмотрим написание рекурсивного уравнения в терминах f вместо P. Поскольку f является решением рекурсивного уравнения по условию 2), выполнение k подстановок дает

то же состояние, что и полученное при использовании уравнения для P, потому что не зависит от применения к исходному состоянию f или P, а только других операторов из M(P).

Таким образом, P(s) = f(s), и поскольку s – определенная точка в их общей области определения, P=f, что и требовалось доказать.

Другой способ охарактеризовать функцию, которая фиксирует значение вызова рекурсивной процедуры, это то, что решение рекурсивного уравнения процедуры, определенно минимально. То есть, F – это функция удовлетворяющая уравнению, которое неопределено так часто как это возможно. (Не существует другой удовлетворяющей уравнению, которая была бы подмножеством F.) Чтобы увидеть, почему это выражение эквивалентно, отметим, что если F имело бы ту же область определения, что и P, F удовлетворял бы правилу верификации, следовательно F = P. Предположим далее, что domain(F) точно меньше, чем domain(P), что существует точка x, для которой P определено, а F нет. Произведем замены в рекурсивном уравнении для P до тех пор пока оно не исчезнет для аргумента x, как было показано выше,

где при получении состояния y не применялось P. Но поскольку F удовлетворяет тому же уравнению,

И потому F определено на x. Тот же аргумент применим к любой точке в domain(P), поэтому последнее решение F имеет эту область определения.

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

Значение процедурного оператора для рекурсивной процедуры должно, следовательно, получаться через нахождение пробной функции, потом верификации. Что это значение с помощью вышеописанного правила. Ситуация похожа на ситуацию с оператором WHILE, рассмотренную в разделе 8.4.2. Однако, правило верификации для оператора WHILE применялось в общем случае, а результат выше ограничен одной рекурсией без параметров. Технические подробности общего случая для рекурсии довольно объемны, поскольку в общем случае могут встречаться несколько рекурсивных выражений одновременно для множественных рекурсий и различные параметры для одной процедуры, если она встречается несколько раз в этих уравнениях.

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

Процедуры CF Pascal могут вызывать себя, рекурсивные процедуры являются механизмом для реализации решения задач с помощью рекурсии. Важным аспектом рекурсии в программировании является то, что каждый новый вызов создает экземпляры локальных переменных. Эта особенность является существенной для решения многих задач.

Сортировка и реверсирования с помощью рекурсии являются хорошими примерами использования этого приема. Задача Ханойские башни имеет особенно элегантное рекурсивное решение.

Математическая индукция может быть полезна при доказательстве свойств рекурсивных задач.

Правило верификации простых рекурсивных процедур очень похоже на правило верификации оператора WHILE, которое мы рассмотрели в главе 8.