Структуры данных и модели вычислений



             

Частично-рекурсивные функции - часть 2


после выполнения на ленте будет

после —

после —

и т.д.

После —

после —

и, наконец, после выполнения всей программы получим

Лемма 3 (о примитивной рекурсии).

Если функции , и вычислимы соответственно программами и , то функция , полученная по схеме примитивной рекурсии, вычислима программой

Доказательство.

Представим программу, предлагаемую для вычисления функции , блок-схемой, изображенной на рисунке.

Пунктирными стрелками показаны контрольные дуги, для которых будут сформированы соответствующие индуктивные утверждения .

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

Напомним, что основное требование, предъявляемое к утверждениям , заключается в том, чтобы была возможность доказательства индуктивных шагов:

Пусть , — исходные значения аргументов из множества , тогда требуемые утверждения можно сформулировать следующим образом:

P_1 — содержимое ленты равно

— существует

такие, что содержимое ленты равно

— содержимое ленты равно

Доказательство индуктивных шагов легко получить, выписывая содержимое ленты после каждого оператора в соответствующем пути. Читателю предоставляется возможность проделать это самостоятельно и убедиться в правильности программы, предлагаемой в формулировке леммы 3. Не забудьте доказать завершаемость исследуемой программы.

Лемма 4 (о минимизации).

Если функция вычислима программой , то функция , полученная из нее по схеме минимизации, вычисляется программой

Доказательство.

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

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

— содержимое ленты равно

— существуют , такие, что содержимое ленты равно

— содержимое ленты равно

Требуется доказать следующие индуктивные шаги.

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

Заметим, что в доказательствах лемм 3 и 4 при рисовании блок-схемы мы несущественно отступили от текстов программ, данных в их формулировках, а при доказательстве леммы 2 не выписывали индуктивных утверждений, так как в представлении программы блок-схемой нет циклов. Обращаем внимание на то, что правильность блоков, из которых составлены программы, мы не подвергаем сомнению.




Содержание  Назад  Вперед