Cтраница 2
Затем v растягивается с помощью новых помеченных неопределенных значений и становится частичной строкой v над U. Теперь необходима осторожность: после изменений в t имеем / ( Rt) и ( Rt) иву есть отличающиеся помеченные неопределенные значения на U - Rt. Согласно утверждению 2, можно удалить v из s, так как t ее заменяет. Удаляем t, чтобы обеспечить завершаемость процесса прогонки. [16]
С помощью таких же рассуждений, как и выше, можно показать, что рекурсивные вызовы процедуры Р2 не могут продолжаться бесконечно долго. Итак, мы доказали, что все вызовы процедур пустое, е и подмнож должны обрабатываться за конечное время. Отсюда вытекает, что вычисление Г обязано быть конечным. Этот вывод имеет место для всех вычислений Г, и, стало быть, полное пространство вычислений нашей программы конечно. Следовательно, исполнение программы 29 при стандартной стратегии управления или при любой другой исчерпывающей стратегии завершается. Доказательство завершаемости можно без труда провести более формально с помощью структурной индукции. [17]