fct f == ( nat n ) nat:
if n == 0 then 0
else f(n—l)
fi
является недетерминированным и при его вызове
f(m) для m Î N в качестве результата выдает любое число i Î N, такое, что 0£ i £ m.
Обратим внимание, что от недетерминированного выбора может также зависеть и завершаемость вычислений.
Пример (недетерминированный алгоритм с неопределенным завершением).
Предписание
fct f =( nat n ) nat:
n?f(n+1)
При вызове f(m) либо вычисляет такое число i Î N, что m £ i, либо вычисление выражения не завершается.
В дальнейшем мы хотим - в свете полиномиально-ограниченных Т-машин - сконцентрироваться на недетерминированных алгоритмах, при которых завершение вычислений всегда обеспечено. В таком случае завершаемость не зависит от недетерминированного выбора.
Пример (недетерминированное порождение перестановки). Алгоритм f, заданный описанием
fct f = ( nat n ) seq nat:
if n = 0 then
else nperm(f(n—l), n)
fi
fct nperm == ( seq nat s, nat n ) seqnat:
if s == e then append(n, s)
else
append(n, s) ?
append(first(s), nperm(rest(s), n))
fi
При вызове f(n) для заданного числа n порождает недетерминированным образом некоторую перестановку чисел {1, 2, ..., n} и всегда завершается. Докажем это по индукции.
(0) Для n > 0 утверждение тривиально.
(1) Предположение индукции: утверждение справедливо для заданного n Î N. Вызов f(n) дает перестановку s из {1, 2, ..., n}. Функция nperm(s, n+l) вставляет (n+l) в какую-нибудь позицию в s. Так можно породить любую перестановку.
Рассмотрение недетерминированных выражений приводит к ряду трудностей, поскольку классические правила преобразований логики не обязательно имеют место. Так, высказывание f(x)==f(x) для недетерминированного алгоритма f можно интерпретировать двояко:
· вычисления правой и левой частей приводят к одинаковому значению (если значений не больше одного);
· множества недетерминированно-возможных значений левой и правой частей совпадают.