Дудаков С.М. Математическое введение в информатику
Подождите немного. Документ загружается.
6.4.
∗∗
Удаление подпрограмм 171
ложь — двухместная операция, возвращающая второй аргумент. То-
гда IF (x, y, z) можно записать в виде (x) (y, z). В самом деле, если
тест x истинен, то
(x) (y, z) = ИСТИНА (y, z) = y = IF (x, y, z) ,
а если ложен, то
(x) (y, z) = ЛОЖЬ (y, z) = z = IF (x, y, z) .
6.4
∗∗
Удалени е подпрограмм
Теперь докажем обратную теорему.
Теорема 6.2. (Об удалении подпрограмм) По к аждому алгорит-
му можно построить эквивалентный алгоритм без подпрограмм.
Доказательство. Докажем эту теорему для случая, когда нет ре-
курсии, а затем докажем, что каждый алгоритм можно преобразовать
к нерекурсивному. В этом случае должна быть подпрограмма f, в кото-
рой не встречаются никакие другие подпрограммы (в противном случае
имелась бы рекурсия). Пользуясь теоремой о подстановке можно удалить
подпрограмму f из всех остальных подпрограмм и основной программы.
Ввиду того, что внутри f другие подпрограммы не встречались, то по-
сле подстановки рекурсии не будет. Пользуясь этой процедурой можно
исключить по очереди все подпрограммы.
Такой метод не годится, если присутствует рекурсия, так подстав-
ляя вместо выражений вида f (e) тело подпрограммы f мы снова будем
получать выражения такого вида и никогда не сможем исключить их
полностью.
Прежде чем показывать, как удаляется рекурсия, докажем следую-
щую лемму.
Лемма 6.8. (О кодировании пар чисел) Существует вычислимая
двухместная функция ν такая, что
1. для всяких x, y, x
0
, y
0
:
ν (x, y) = ν (x
0
, y
0
) ⇐⇒ x = x
0
и y = y
0
;
172 Глава 6. Подпрогра ммы, функциональное программирование
2. существуют вычислимые функции ν
1
и ν
2
такие, что для всяких
x, y:
ν (ν
1
(x) , ν
2
(x)) = x; ν
1
(ν (x, y)) = x; ν
2
(ν (x, y)) = y.
Доказательство. В самом деле, рассмотрим функцию
ν (x, y) = (2x + 1) 2
y
.
Чтобы доказать справедливость обоих пунктов, заметим, что каждое
положительное натуральное число допускает единственное разложение
на простые множители: z = 2
i
2
3
i
3
. . . p
i
p
k
k
. Следовательно, для каждого
z > 0 существуют единственные числа a и b такие, что b — нечетное, a —
степень двойки и z = ab.
Пусть ν (x, y) = ν (x
0
, y
0
) = z. Тогда для z существуют a и b. Н о тогда
a = 2
y
= 2
y
0
. b = (2x + 1) = (2x
0
+ 1). То есть x = x
0
и y = y
0
. Аналогично
доказывается второй пункт.
∗
Задача 6.20. Завершите доказательство леммы.
Задача 6.21. Напишите подпрограммы для вычисления функций ν, ν
1
,
ν
2
из леммы без использования рекурсии.
Очевидными свойствами функции ν являются следующие:
Следствие 6.6. ν (x, y) > x, ν (x, y) > y, ν (x, y) > 0.
Следующий наш шаг — доказать, что всякую косвенную рекурсию
можно заменить прямой.
Лемма 6.9. (О косвенной рекурсии) Каждый алгоритм эквива-
лентен некоторому алгоритму, в котором присутствует только одна
подпрограмма.
Доказательство. Прежде всего, будем считать, что все подпрограм-
мы имеют одинаковое количество аргументов. Если это не так всегда
можно добавить фиктивные параметры, которые нигде не используют-
ся.
Пусть алгоритм содержит m подпрограмм f
1
, . . . , f
m
, каждая из ко-
торых имеет n аргументов. Можно считать, что все подпрограммы
6.4.
∗∗
Удаление подпрограмм 173
f
1
, . . . , f
m
имеют аргументы x
1
, . . . , x
n
. Рассмотрим следующую подпро-
грамму f:
Sub f;
arg x, x
1
, . . . , x
n
;
if x = 1 then
(Π
f
1
)
f
1
(·)
f(1, ·)
...
...
f
m
(·)
f(m, ·)
end;
.
.
.
if x = m then
(Π
f
m
)
f
1
(·)
f(1, ·)
...
...
f
m
(·)
f(m, ·)
end;
Здест x — новая переменная. Каждое выражение вида f
i
(e) мы заме-
няем выражением вида f (i, e). Для каждого состояния σ будем иметь
σ (f
i
(e)) = σ (f (i, e)) .
Проделав точно такую же замену f
i
(e) на f (i, e) в основной програм-
ме мы получим алгоритм, эквивалентный исходному. Так как теперь в
алгоритме присутствует только одна подпрограмма, то рекурсия может
быть только прямой.
∗
Задача 6.22. Докажите, что для любого состояния σ
σ (f
i
(e)) = σ (f (i, e))
для любого i = 1, . . . , m, и любых выражений e.
Теорема 6.3. (Об удалении рекурсии) По каждому алгоритму
можно построить эквивалентный алгоритм без рекурсии.
Доказательство. Итак, согласно предыдущим утверждениям, мы
можем считать, что у нас есть одна подпрограмма f с n аргументами.
Прежде всего, несколько модифицируем саму f.
Во-первых, перестроим тело f в простую программу. Это означает,
в частности, что каждый вызов подпрограммы f является отдельным
оператором присваивания вида
u = f (u
1
, . . . , u
n
) ;
174 Глава 6. Подпрогра ммы, функциональное программирование
Более того, можно считать, что переменная u во всех таких операторах
одна и та же.
Во-вторых, переделаем тело подпрограммы f в программу с метками.
Будем считать, что метки — натуральные положительные числа. γ —
заключительная метка. Заметим, что все проделанные преобразования
привели к эквивалентной подпрограмме.
Итак, подпрограмма f сейчас имеет вид
Sub f;
arg x;
o
1
o
2
.
.
.
o
N
end;
Каждый из операторов o
k
имеет один из видов:
1. o
k
∼ α
k
x
k
= e
k
; β
k
,
2. o
k
∼ α
k
if T
k
then β
k
else γ
k
,
3. o
k
∼ α
k
u = f (u
1
, . . . , u
n
) ; β
k
,
причем e
k
и T
k
не содержат f.
Приступим к построению по подпрограмме f подпрограммы f
1
без
рекурсивных вызовов. Будем делать это так же, как мы структуризиро-
вали программу с метками, см. доказательство теоремы 4.2 на стр. 98.
Добавим новые переменные w, y, s и R. Заменим всюду оператор при-
сваивания f = e; на R = e; По каждому o
k
определим соответствующую
программу ϕ (o
k
). Для операторов первых двух видов определение ϕ (o
k
)
6.4.
∗∗
Удаление подпрограмм 175
не изменится. Для операторов третьего вида:
ϕ (o
k
) ∼
if w = succ (0) then
if y =
α
k
then
s = ν (s, z
1
) ; . . . s = ν (s, z
m
) ;
s = ν (s, x
1
) ; . . . s = ν (s, x
n
) ;
s = ν
s, β
k
;
x
1
= u
1
; . . . x
n
= u
n
;
z
1
= 0; . . . z
m
= 0;
y = α
1
;
w = 0;
end;
end;
Здесь мы предполагаем, что z
1
, . . . , z
m
— все переменные программы Π
f
(исключая y, w, s, но включая R), которые не являются ее аргументами,
а x
1
, . . . , x
n
— аргументы f. Пусть
ϕ
1
∼
if w = succ (0) then
if 0 < s then
y = ν
2
(s) ; s = ν
1
(s) ;
x
n
= ν
2
(s) ; s = ν
1
(s) ;
.
.
.
x
1
= ν
2
(s) ; s = ν
1
(s) ;
z
m
= ν
2
(s) ; s = ν
1
(s) ;
.
.
.
z
1
= ν
2
(s) ; s = ν
1
(s) ;
u = R;
w = 0;
end;
end;
176 Глава 6. Подпрогра ммы, функциональное программирование
Теперь мы готовы построить нерекурсивную подпрограмму f
1
:
Sub f
1
;
arg x;
y = α
1
; w = 0; s = 0;
while w = 0 do
w = succ (0) ;
ϕ (o
1
)
.
.
.
ϕ (o
N
)
ϕ
1
end;
f
1
= R;
end;
Пусть Π
f
(σ) определено. Следовательно, последовательность расши-
ренных состояний
σ
i
, λ
i
i
конечна. Рассмотрим последовательность со-
стояний цикла Π
f
1
:
σ
j
1
j
, и последовательность расширенных состояний
Π
f
:
σ
i
, λ
i
i
. Пусть j
0
= 0. Индукцией по высоте леса вложенных вызовов
Ff (σ, Π
f
) мы докажем следующее утверждение:
Утверждение 6.2. Для всякого i существует j
i
такое, что
1. σ
j
i
1
s = σ
j
0
1
s,
2. σ
l
1
s ≥ σ
j
0
1
s для l ∈ [j
0
, j
i
],
3. σ
j
i
1
y = λ
i
,
4. σ
j
i
1
w = 0,
5. σ
j
i
1
R = σ
i
f,
6. σ
j
i
1
z = σ
i
z для остальных переменных z.
Базис индукции.
Если вложенные вызовы отсутствуют, то доказательство повторяет до-
казательство теоремы о структуризации.
Шаг индукции.
Пусть для лесов высоты не более h утверждение доказано, и предполо-
жим, что лес Ff (σ, Π
f
) имеет высоту h + 1. Используем индукцию по
6.4.
∗∗
Удаление подпрограмм 177
длине последовательности
σ
i
, λ
i
i
. Для операторов первых дву х видов
доказательство повторяет доказательство теоремы о структуризации.
Рассмотрим i-ый элемент последовательности:
σ
i
, λ
i
. Пусть λ
i
= α
k
,
а сам оператор имеет вид
α
k
u = f (u) ; β
k
.
Пусть δ — вызов, служащий, для вычисления σ
i
(f (u)).
В последовательности
σ
j
1
i
следующим за σ
j
i
1
будет состояние σ
j
i
+1
1
такое, что σ
j
i
+1
1
y = α
1
, σ
j
i
+1
1
w = 0,
σ
j
i
+1
1
s = ν
ν
j
i
ν
j
i
(s, z) , x
, β
k
,
и σ
j
i
+1
1
z = σ
δ
z для остальных переменных z.
Здесь мы обозначаем
ν
l
(s, w) = ν
ν
. . . ν
σ
l
1
s, σ
l
1
w
1
. . .
, σ
l
1
w
N
.
Заметим, что σ
j
i
+1
1
s > σ
j
i
1
s ≥ 0.
Высота леса Ff (σ
δ
, Π
f
) не больше h. Так как вызов δ определен, то
последовательность расширенных состояний для Π
f
(σ
δ
) конечна, и за-
канчивается она расширенным состоянием вида (σ
0
, γ). По индукцион-
ному предположению существует такое j
0
, что σ
j
0
1
s = σ
j
i
+1
1
s, σ
j
0
1
y = γ,
σ
j
0
1
w = 0, σ
j
0
1
R = σ
0
f, и σ
j
0
1
z = σ
0
z для остальных z. При следующем
выполнении тела цикла все тесты y = α
k
в операторах ϕ (o
k
) окажут-
ся ложными. Следовательно, тесты w = succ (0) и 0 < s в ϕ
1
будут
истинны. Пусть j
i+1
= j
0
+ 1. Тогда σ
j
i+1
1
z = σ
j
i
1
z для z 6∼ u,
σ
j
i+1
1
u = σ
j
0
1
R = σ
0
f,
σ
j
i+1
1
s = σ
j
i
1
s, σ
j
i+1
1
y = β
k
= λ
i+1
, σ
j
i+1
1
w = 0. Таким образом, σ
j
i+1
1
соот-
ветствует
σ
i+1
, λ
i+1
. Утверждение доказано.
Последовательность расширенных состояний
σ
i
, λ
i
i
оканчивается
расширенным состоянием (σ
n
, γ). Согласно утверждению существует j
n
такое, что σ
j
n
1
s = σ
0
1
s = 0, σ
j
n
1
y = γ, σ
j
n
1
w = 0, σ
j
n
1
R = σ
n
f. При сле-
дующем выполнении тела цикла, мы получим σ
j
n
+1
1
w = 1, а значение
остальных переменных не изменится. Следовательно,
Π
f
1
(σ) (f
1
) = σ
j
n
1
R = σ
n
f = Π
f
(f) .
Теперь докажем обратное, пусть Π
f
1
(σ
1
) определено.
178 Глава 6. Подпрогра ммы, функциональное программирование
Утверждение 6.3. Если k < l,
σ
k
1
s = σ
l
1
s,
σ
j
1
s ≥ σ
k
1
s для j ∈ [k, l],
то в последовательности расширенных состояний для Π
f
σ
0
, λ
0
где
λ
0
= σ
k
1
y, σ
0
f = σ
k
1
R и σ
0
z = σ
k
1
z для остальных переменных z, имеет-
ся элемент
σ
l
0
, λ
l
0
такой, что
1. σ
l
1
y = λ
l
0
,
2. σ
l
1
R = σ
l
0
f,
3. σ
l
1
z = l
0
z для остальных переменных z.
Индукция по количеству j ∈ [k, l] таких, что σ
j
1
s > σ
k
1
s.
Базис индукции.
Если таких j нет, то доказательство повторяет доказательство теоремы
о структуризации.
Шаг индукции.
Пусть для меньших количеств доказано. Рассмотрим самое первое j, для
которого σ
j−1
1
s < σ
j
1
s. Рассмотрим наибольшее из таких p, что σ
i
1
s ≥ σ
j
1
s
для всех i ∈ [j, p].
Последовательности состояний
σ
k
, . . . , σ
j−1
;
σ
j
, . . . , σ
p
;
σ
p+1
, . . . , σ
l
удовлетворяют условиям индукционного предположения. Применим его
к этим трем случаям.
В последовательности расширенных состояний для Π
f
σ
0
, λ
0
где
λ
0
= σ
k
1
y, σ
0
f = σ
k
1
R и σ
0
z = σ
k
1
z для остальных переменных z, име-
ется элемент
σ
j
0
, λ
j
0
такой, что
1. σ
j−1
1
y = λ
j
0
,
2. σ
j−1
1
R = σ
j
0
f,
3. σ
j−1
1
z = j
0
z для остальных переменных z.
6.4.
∗∗
Удаление подпрограмм 179
Так как σ
j−1
1
s < σ
j
1
s, то σ
j−1
1
y = λ
j
0
и в программе Π
f
имеется опера-
тор вида
λ
j
0
u = f (u) ; λ
j
0
+1
.
Для вычисления σ
j
0
(f (u)) используется вызов
δ =
f, σ
j
0
u
1
, . . . , σ
j
0
u
n
.
Заметим, что σ
δ
f = σ
j
1
R, σ
δ
z = σ
j
1
z для остальных переменных z про-
граммы Π
f
.
При переходе от p к p + 1 значение переменной s уменьшилось, что
могло произойти, только при выполнении фрагмента ϕ
1
. Это означает,
что все тесты y = α являются ложными на состоянии σ
p
. Это означает,
что σ
p
y = γ — заключительная метка.
Таким образом, в последовательности расширенных состояний для
Π
f
σ
0
, λ
0
где λ
0
= σ
j
1
y = α
1
, σ
0
f = σ
j
1
R = 0 и σ
0
z = σ
j
1
z для остальных
переменных z, имеется элемент
σ
p
0
, λ
p
0
такой, что
1. γ = λ
p
0
,
2. σ
p
1
R = σ
p
0
f,
Из этого следует, что
Res δ = σ
p
1
R.
Заметим, что σ
p+1
1
совпадает с σ
j−1
1
кроме того, что
σ
p+1
1
u = σ
1
p
R = Res δ = σ
j
0
(f (u)) .
Это означает, что σ
p+1
1
соответствует
σ
j
0
+1
, λ
j
0
+1
в последовательности
расширенных состояний.
В последовательности расширенных состояний для Π
f
σ
j
0
+1
, λ
j
0
+1
где λ
j
0
+1
= σ
p+1
1
y, σ
j
0
+1
f = σ
p+1
1
R и σ
j
0
+1
z = σ
p+1
1
z для остальных пере-
менных z, имеется элемент
σ
l
0
, λ
l
0
такой, что
1. σ
l
1
y = λ
l
0
,
2. σ
l
1
R = σ
l
0
f,
3. σ
l
1
z = l
0
z для остальных переменных z.
180 Глава 6. Подпрогра ммы, функциональное программирование
Так как Π
f
1
(σ
1
) определено, то последовательность
σ
i
1
i
конечна. То
есть для некоторого N выполняется
σ
n
6|= w = 0.
Из этого следует, что σ
n−1
y = γ — заключительная метка и σ
n−1
s = 0.
Согласно утверждению, в последовательности расширенных состояний
для Π
f
σ
0
, λ
0
, где λ
0
= α
1
, σ
0
f = 0 и σ
0
z = σ
δ
z для остальных пе-
ременных z, имеется элемент
σ
l
, λ
l
такой, что λ
l
= γ. То есть Π
f
(σ)
определено.
Задача 6.23. Пользуясь предложенным методом удалите рекурсию
из программы из примера 6.17 на стр. 161.
6.5
∗
Доказательство корректности подпрограмм
Очевидно, что для доказательства корректности алгоритмов с подпро-
граммами правил, которые мы изучали раньше, недостаточно. В самом
деле, если f — подпрограмма, то мы не можем использовать аксиому
n
(ϕ)
x
f(y)
o
x = f (y) ; {ϕ},
потому что мы не можем сказать, что означает f (y) в условии. Истин-
ность условия на состоянии должна определяться самим условием и со-
стоянием, но не программой, для которой это условие написано.
Определение 6.18. (Ограничитель вызовов) Ограничитель вызо-
вов подпрограммы f при условии ϕ — выражение L
ϕ
такое, что
1. σ (L
ϕ
) ∈ ω для любого состояния σ;
2. Для любого вызова δ и рекурсивного для δ вызова ε, если σ
δ
|= ϕ,
то
σ
ε
(L
ϕ
) < σ
δ
(L
ϕ
) .