Дудаков С.М. Математическое введение в информатику
Подождите немного. Документ загружается.
6.5.
∗
Доказательство корректности подпрограмм 181
Пример 6.18. Рассмотрим подпрограмму:
Sub S;
arg x, y, z;
if x < succ (y) then
S = z;
else
S = S (x, succ (y) , succ (z)) ;
end;
end;
Пусть L ∼ bx − yc. Рассмотрим произвольный вызов
δ = (S, a, b, c)
и рекурсивный для него вызов
ε = (S, d, e, f) .
Очевидно, что a > b (иначе Fc δ = ()). Пусть ζ = (S, a, b + 1, c + 1),
тогда
Fc δ = (ζ) = ((S, a, b + 1, c + 1)) ,
σ
ζ
(L) = ba − b − 1c < ba − b − 1c = σ
δ
(L) .
По индукции получаем, что
σ
ε
(L) < σ
δ
(L) .
Для подпрограмм у нас будет два правила вывода.
ЗП Замена переменной (для присваиваний) Пусть x не входит в вы-
ражение e и условие ϕ. Пусть x обязательно входит в выражение d,
если e содержит имена подпрограмм. Тогда из частичной (полной)
корректности троек
{ϕ}x = e; {ψ} {ψ}y = d; {θ}
следует частичная (полная) корректность тройки
{ϕ}y = (d)
x
e
; {∃x (θ ∧ ∃yψ)}.
182 Глава 6. Подпрогра ммы, функциональное программирование
ЗП Замена переменной (для тестов) Будем использовать три разно-
видности этого правила. Пусть x не входит в условия ϕ и ψ, про-
граммы Π
1
и Π
2
. Пусть x обязательно входит в тест T . Тогда из
частичной (полной) корректности каждой из троек
{ϕ}x = e; if T then Π
1
end; {ψ}
{ϕ}x = e; if T then Π
1
else Π
2
end; {ψ}
{ϕ}x = e; while T do Π
1
x = e; end; {ψ}
следует частичная (полная) корректность троек
{ϕ} if (T )
x
e
then Π
1
end; {ψ}
{ϕ} if (T )
x
e
then Π
1
else Π
2
end; {ψ}
{ϕ} while (T )
x
e
do Π
1
end; {ψ}
соответственно.
ВП Вызов подпрограммы Тройка
{ϕ}x = f (z
1
, . . . , z
n
) ;
n
(ψ)
f
x
o
выводима, если
1. x не встречается среди z
1
, . . . , z
n
;
2. z
1
, . . . , z
n
— аргументы подпрограммы f;
3.
{ϕ}x = f (z
1
, . . . , z
n
)
n
(ψ)
f
x
o
B
IH
{ϕ
0
}Π
f
{ψ
0
}
Здесь
ϕ
0
∼ ˆϕ ∧ z
1
= ˆz
1
∧ ··· ∧ z
n
= ˆz
n
;
ψ
0
∼
ˆ
ψ.
ˆϕ и
ˆ
ψ получаются из ϕ и ψ заменой каждой переменной u (кроме
f) на переменную ˆu, не встречающуюся в Π
f
.
4. для полной корректности требуется существование ограничите-
ля вызова L
ϕ
0
.
6.5.
∗
Доказательство корректности подпрограмм 183
Пункты 3 и 4 можно объединить в один: потребовать, чтобы
{ϕ ∧ L < u}x = f (z
1
, . . . , z
n
)
n
(ψ)
f
x
o
B
IH
n
ϕ
0
∧
ˆ
L = u
o
Π
f
{ψ
0
},
где u — новая переменная.
Пункт 3 в правиле ВП означает следующее: мы берем
{ϕ}x = f (z
1
, . . . , z
n
)
n
(ψ)
f
x
o
в качестве новой аксиомы, используя ее и другие аксиомы и правила
вывода доказываем тройку {ϕ
0
}Π
f
{ψ
0
}, и если это удается, то тройку
{ϕ}x = f (z
1
, . . . , z
n
) ;
n
(ψ)
f
x
o
мы считаем доказанной.
∗∗
Задача 6.24. Докажите, что с помощью каждого из правил ЗП из
частично (полностью) корректных троек получаются частично (пол-
ностью) корректные.
Доказательство аналогичного утверждения для правила ВП является
технически сложной задачей и оно вынесено в отдельный параграф.
Рассмотрим некоторые правила, которые допустимы в нашем исчис-
лении.
ДОБ Докажем допустимость правила ДОБ в новом исчислении. Точ-
но так же заменим в доказательстве переменные, которые использу-
ются в правилах ЗП, ВП и ЦП на новые, которые не встречаются ни
доказательстве ни в θ.
Доказательство будет проводиться такой же индукцией, как и раньше.
Только базисом индукции кроме аксиом АКС будут применения прави-
ла ВП, а также аксиомы, которые используются для этого правила.
Пусть доказуема тройка {ϕ}x = f (z) ; {ψ}. Пусть u, v — новые пере-
менные. Тройка
{ϕ ∧ θ}u = v; {ϕ ∧ θ}
является аксиомой АКС. Тройка
{ϕ ∧ θ}x = f (z) ; {ψ}
получается по правилу УПР. По правилу ЗП получаем
{ϕ ∧ θ}x = f (z) ; {∃u (ψ ∧ ∃x (ϕ ∧ θ))}.
184 Глава 6. Подпрогра ммы, функциональное программирование
Так как u не входит в ψ ∧ ∃x (ϕ ∧ θ), а x не входит в θ, то формула
∃u (ψ ∧ ∃x (ϕ ∧ θ)) → ψ ∧ θ
истинна. По правилу ОП получаем
{ϕ ∧ θ}x = f (z) ; {ψ ∧ θ}.
ВП* Пусть ϕ из переменных содержит только z
1
, . . . , z
n
, ψ —
z
1
, . . . , z
n
, f, и z
1
, . . . , z
n
6∈ LVar (Π
f
). Тогда для доказуемости трой-
ки
{ϕ}x = f (z
1
, . . . , z
n
) ;
n
(ψ)
f
x
o
достаточно потребовать, чтобы
{ϕ}x = f (z
1
, . . . , z
n
)
n
(ψ)
f
x
o
B
IH
{ϕ}Π
f
{ψ}.
Доказательство. Пусть
{ϕ}x = f (z
1
, . . . , z
n
)
n
(ψ)
f
x
o
B
IH
{ϕ}Π
f
{ψ}.
Пусть
θ ∼ z
1
= ˆz
1
∧ ··· ∧ z
n
= ˆz
n
.
Так как
Var (θ) ∩ LVar (Π
f
) = ∅,
то по правилу ДОБ получаем:
{ϕ}x = f (z
1
, . . . , z
n
)
n
(ψ)
f
x
o
B
IH
{ϕ ∧ θ}Π
f
{ψ ∧ θ}.
Так как ϕ не содержит переменных кроме z, а ψ кроме z содержит лишь
f, то
ϕ
0
∼ ˆϕ ∧ θ; ˆϕ ∧ θ ≡ ϕ ∧ θ;
ψ
0
∼
ˆ
ψ;
ˆ
ψ ⇐
ˆ
ψ ∧ θ;
ˆ
ψ ∧ θ ≡ ψ ∧ θ.
По правилам УПР и ОП получаем:
{ϕ}x = f (z
1
, . . . , z
n
)
n
(ψ)
f
x
o
B
IH
{ϕ
0
}Π
f
{ψ
0
},
что и требовалось.
ЗАМ Пусть
B
IH
{ϕ}x = e; {ψ},
6.5.
∗
Доказательство корректности подпрограмм 185
y не входит ни в ψ, ни в одно из выражений e, все выражения e не со-
держат подпрограмм,
z — набор не совпадающих с x попарно различных
переменныx. Тогда
B
IH
n
(ϕ)
xz
ye
o
y = (e)
xz
ye
;
n
(ψ)
xz
ye
o
.
Доказательство. Пусть u — новая переменная и
B
IH
{ϕ}x = e; {ψ}.
Сначала докажем, что
B
IH
{(ϕ)
z
u
}x = (e)
z
u
; {(ψ)
z
u
},
где z — любая переменная, отличная от x. Аксиома ПРИСВ*:
B
IH
{(ϕ)
z
u
}z = u; {(ϕ)
z
u
∧ z = u},
по правилу ОП:
B
IH
{(ϕ)
z
u
}z = u; {ϕ ∧ z = u},
по правилу УПР:
B
IH
{ϕ ∧ z = u}x = e; {ψ}.
По правилу ЗП:
B
IH
{(ϕ)
z
u
}x = (e)
z
u
; {∃z (∃x (ϕ ∧ z = u) ∧ ψ)},
Формула
∃z (∃x (ϕ ∧ z = u) ∧ ψ) → (ψ)
z
u
истинна, следовательно, по правилу ОП:
B
IH
{(ϕ)
z
u
}x = (e)
z
u
; {(ψ)
z
u
}.
Применив эту процедуру несколько раз мы докажем, что
B
IH
n
(ϕ)
z
u
o
x = (e)
z
u
;
n
(ψ)
z
u
o
.
Так как ψ не содержит y, то
(ψ)
xz
yu
y
x
∼ (ψ)
z
u
. Согласно аксиоме АКС:
B
IH
n
(ψ)
z
u
o
y = x;
n
(ψ)
xz
yu
o
.
186 Глава 6. Подпрогра ммы, функциональное программирование
Теперь по правилу ЗП:
B
IH
n
(ϕ)
z
u
o
y = (e)
z
u
;
n
∃x
∃y
(ψ)
z
u
∧ (ψ)
xz
yu
o
.
Так как (ψ)
xz
yu
не содержит x, то по правилу ОП:
B
IH
n
(ϕ)
z
u
o
y = (e)
z
u
;
n
(ψ)
xz
yu
o
.
Далее АКС:
B
IH
n
(ϕ)
xz
yu
o
x = y;
n
(ϕ)
z
u
o
.
По правилу ЗП:
B
IH
n
(ϕ)
xz
yu
o
y = (e)
xz
yu
;
n
∃x
∃y
(ϕ)
z
u
∧ (ψ)
xz
yu
o
.
И снова по правилу ОП:
B
IH
n
(ϕ)
xz
yu
o
y = (e)
xz
yu
;
n
(ψ)
xz
yu
o
.
Теперь осталось только u заменить на e. Это делается точно так же, как
z на u.
∗
Задача 6.25. Завершите доказательство допустимости правила
ЗАМ.
Пример 6.19. Рассмотрим пример — подпрограмму для вычисления
наименьшего общего кратного, см. рис. 6.6 на стр. 187.
1. Предположим, что
{0 < z ≤ НОК (x, y) ∧ xy − z < u}
m = mcc
1
(x, y, z) ;
{m = НОК (x, y)}
2. ЗАМ : 1.
{0 < z + 1 ≤ НОК (x, y) ∧ xy − (z + 1) < u}
mcc
1
= mcc
1
(x, y, z + 1) ;
{mcc
1
= НОК (x, y)}
3. АКС. {z = НОК (x, y)}mcc
1
= z; {mcc
1
= НОК (x, y)}
6.5.
∗
Доказательство корректности подпрограмм 187
Alg mcc
1
;
arg x, y, z;
if z mod x = 0 then
if z mod y = 0 then
mcc
1
= z;
else
mcc
1
= mcc
1
(x, y, z + 1) ;
end;
Π
1
else
mcc
1
= mcc
1
(x, y, z + 1) ;
end;
end;
Alg mcc;
arg x, y;
mcc = mcc
1
(x, y, 1) ;
end;
Рис. 6.6: Наименьшее общее кратное.
4. УПР : 3.
0 < z ≤ НОК (x, y) ∧ z mod x = 0 ∧ z mod y = 0 ∧ xy − z = u →
→ z = НОК (x, y)
{0 < z ≤ НОК (x, y) ∧ z mod x = 0 ∧ z mod y = 0 ∧ xy − z = u}
mcc
1
= z;
{mcc
1
= НОК (x, y)}
5. УПР : 2.
0 < z ≤ НОК (x, y) ∧ z mod x = 0 ∧ ¬z mod y = 0 ∧ xy − z = u →
→ 0 < z + 1 ≤ НОК (x, y) ∧ xy − (z + 1) < u
{0 < z ≤ НОК (x, y) ∧ z mod x = 0 ∧ ¬z mod y = 0 ∧ xy − z = u}
mcc
1
= mcc
1
(x, y, z + 1) ;
{mcc
1
= НОК (x, y)}
6. ПВ : 4, 5.
{0 < z ≤ НОК (x, y) ∧ z mod x = 0 ∧ xy − z = u}
Π
1
{mcc
1
= НОК (x, y)}
7. УПР : 2.
0 < z ≤ НОК (x, y) ∧ ¬z mod x = 0 ∧ xy − z = u →
→ 0 < z + 1 ≤ НОК (x, y) ∧ xy − (z + 1) < u
188 Глава 6. Подпрогра ммы, функциональное программирование
Sub F ;
arg x;
if x < 2 then
F = 1;
else
F = F (x − 1) × x;
end;
end;
Рис. 6.7: Факториал.
{0 < z ≤ НОК (x, y) ∧ ¬z mod x = 0 ∧ xy − z = u}
mcc
1
= mcc
1
(x, y, z + 1) ;
{mcc
1
= НОК (x, y)}
8. ПВ : 6, 7.
{0 < z ≤ НОК (x, y) ∧ xy − z = u}
Π
mcc
1
{mcc
1
= НОК (x, y)}
9. ВП* : 1 − 8.
{0 < z ≤ НОК (x, y)}m = mcc
1
(x, y, z) ; {m = НОК (x, y)}
10. ЗАМ : 9.
{0 < 1 ≤ НОК (x, y)}m = mcc
1
(x, y, 1) ; {m = НОК (x, y)}
11. ВП* : 1 − 10.
{0 < 1 ≤ НОК (x, y)}m = mcc (x, y) ; {m = НОК (x, y)}
12. УПР : 11.
x 6= 0 ∧ y 6= 0 → 0 < 1 ≤ НОК (x, y)
{x 6= 0 ∧ y 6= 0}m = mcc (x, y) ; {m = НОК (x, y)}
Пример 6.20. Рассмотрим подпрограмму, вычисляющую факториал,
см. рис. 6.7.
1. Предположим, что
{ИСТИНА}y = F (x) ; {y = x!}
6.5.
∗
Доказательство корректности подпрограмм 189
Sub mcd;
arg x, y;
if x = y then
mcd = x;
else
if x < y then
mcd = mcd (x, y − x) ;
else
mcd = mcd (x − y, y) ;
end;
Π
1
end;
end;
Рис. 6.8: Алгоритм Евклида.
2. ПРИСВ*. {x < 2}F = 1; {x < 2 ∧ F = 1}
3. ОП : 2. {x < 2}F = 1; {F = x!}
4. ЗАМ : 1. {ИСТИНА}y = F (x − 1) ; {y = (x − 1)!}
5. ПРИСВ*. {y = (x − 1)!}F = y × x; {y = (x − 1)! ∧ F = yx}
6. ОП : 5. {y = (x − 1)!}F = y × x; {F = x!}
7. ЗП : 6, 4.
{ИСТИНА}
F = F (x − 1) × x;
{∃y (∃F (y = (x − 1)!) ∧ F = x!)}
8. ОП : 7. {ИСТИНА}F = F (x − 1) × x; {F = x!}
9. УПР : 8. {¬x < 2}F = F (x − 1) × x; {F = x!}
10. ПВ : 2, 8. {ИСТИНА}Π
F
{F = x!}
11. ВП* : 1 − 10. Ограничитель вызовов — x, следовательно, тройка
{ИСТИНА}y = F (x) ; {y = x!}
вполне корректна.
Пример 6.21. Рассмотрим алгоритм Евклида на рис. 6.8.
Чтобы каждый раз не переписывать x > 0∧y > 0, мы предполагаем,
что это всегда так.
190 Глава 6. Подпрогра ммы, функциональное программирование
1. Предположим, что
{ИСТИНА}z = mcd (x, y) ; {z = НОД (x, y)}.
2. ПРИСВ*. {x = y}mcd = x; {mcd = x ∧ x = y}
3. ОП : 2. {x = y}mcd = x; {mcd = НОД (x, y)}
4. ЗАМ, ДОБ : 1.
{¬x = y ∧ x < y}
mcd = mcd (x, y − x) ;
{¬x = y ∧ x < y ∧ mcd = НОД (x, y − x)}
5. ЗАМ, ДОБ : 1.
{¬x = y ∧ ¬x < y}
mcd = mcd (x − y, y) ;
{¬x = y ∧ ¬x < y ∧ mcd = НОД (x − y, y)}
6. ОП : 4.
{¬x = y ∧ x < y}
mcd = mcd (x, y − x) ;
{mcd = НОД (x, y)}
7. ОП : 5.
{¬x = y ∧ ¬x < y}
mcd = mcd (x − y, y) ;
{mcd = НОД (x, y)}
8. ПВ : 6, 7. {¬x = y}Π
1
{mcd = НОД (x, y)}.
9. ПВ : 3, 8. {ИСТИНА}Π
mcd
{mcd = НОД (x, y)}.
10. ВП* : 1 − 9. Ограничитель — |x − y|, следовательно
{ИСТИНА}z = mcd (x, y) ; {z = НОД (x, y)}.
6.6
∗∗
Корректность правила ВП
Чтобы доказать непротиворечивость ВП введем новое понятие.