2.V. Сравнение, поиск, вставка
. К оглавлению . Показать весь текст .
Лемма о минимальной позиции отличия в строках:
(л.9.1) str(a, n, 1) ≠ str(b, n, 1) ⇒ ∃_1 m (str(a, m, 1) ≠ str(b, m, 1) ∧ (∀ i < m: str(a, i, 1) = str(b, i, 1)))
Пояснение: Очевидная лемма о том, что если строки не равны, то есть такой номер m позиции в этих строках, что именно на нем встречается самое первое отличие в строках, а до него (если есть позиции раньше) у строк одинаковые элементы алфавита на соответствующих местах.
Существование m доказывается по индукции для n ′. Рассматриваются 2 варианта: при первом варианте имеется i:
i ≤ n, такой что str(a, i, 1) ≠ str(b, i, 1),
а при втором варианте для каждого i:
i ≤ n означает str(a, i, 1) = str(b, i, 1).
При первом варианте для n ′ теорема верна в силу предположения индукции, а во втором - сама позиция n ′ является искомым решением. Это завершает доказательство по индукции для существования.
Единственность m тоже очевидна: если бы были два отличных m_1 и m_2, то для меньшего - пусть m_1 - было бы верно:
str(a, m_1, 1) ≠ str(b, m_1, 1)
А для второго было бы верно:
i < m_2 ⇒ str(a, i, 1) = str(b, i, 1), в частности, для i = m_1 получается (так как m_1 < m_2):
str(a, m_1, 1) = str(b, m_1, 1)
Что противоречит написанному чуть выше неравенству. Поэтому единственность тоже доказана.
Лемма об эквивалентном добавлении дизъюнктивных членов:
(л.9.2) A ⇒ ( (A ⇒ ¬ C) ⇒ (B ⇔ (B ∨ C)) )
Это тавтология, что легко выявить прямой проверкой, но приведу схему вывода ради демонстрации некоторых технических приёмов.
Для доказательства леммы (л.9.2) достаточно доказать, что:
¬ C ⇒ (B ⇔ (B ∨ C)), так как лемма (л.9.2) следует по правилу силлогизма из данного предложения и тавтологии:
A ⇒ ( (A ⇒ ¬ C) ⇒ ¬ C).
Поэтому сводим эквивалентность к эквивалентной эквивалентности отрицаний:
¬ C ⇒ (¬ B ⇔ (¬ B ∧ ¬ C))
А последнее предложение очевидно - при дедуктивном предположении ¬ C из очевидных тавтологий:
¬ B ⇒ ¬ B
¬ C ⇒ (¬ B ⇒ ¬ B)
¬ C ⇒ (¬ B ⇒ ¬ C)
¬ C ⇒ (¬ B ⇒ ¬ B ∧ ¬ C)
¬ B ∧ ¬ C ⇒ ¬ B
¬ C ⇒ (¬ B ∧ ¬ C ⇒ ¬ B)
¬ C ⇒ (¬ B ⇔ (¬ B ∧ ¬ C))
Теорема доказана.
(9.1) Определение для CompIn(a, b):
( str(a, CompIn(a, b), 1) ≠ str(b, CompIn(a, b), 1) ∧ ∀ i (i < CompIn(a, b) ⇒ str(a, i, 1) = str(b, i, 1)) )
∨ ( CompIn(a, b) = 0 ∧ a = b )
Пояснение. Эта функция возвращает первое место, на котором в строке a и строке b находятся разные элементы алфавита. А если такого места нет, то CompIn(a, b) возвращает 0.
Для доказательства того, что (9.1) является определением, будем рассматривать следующую формулу, которую обозначим как C(m, a, b):
( str(a, m, 1) ≠ str(b, m, 1) ∧ (∀ i < m: str(a, i, 1) = str(b, i, 1)) ) ∨ ( m = 0 ∧ a = b )
И надо доказать:
∃_1 m C(m, a, b)
Ветка 1.
Докажем данную формулу при условии
str(a, n, 1) ≠ str(b, n, 1)
Тогда у нас уже доказано по (л.9.1):
∃_1 m (str(a, m, 1) ≠ str(b, m, 1) ∧ (∀ i < m: str(a, i, 1) = str(b, i, 1)))
Верной является следующее предложение:
1.1. str(a, n, 1) ≠ str(b, n, 1) ⇒ ¬ ( m = 0 ∧ a = b )
Это следует из
a = b ⇒ (∀ i str(a, i, 1) = str(b, i, 1))
(∀ i str(a, i, 1) = str(b, i, 1)) ⇒ str(a, n, 1) = str(b, n, 1)
И, применяя контрапозицию к краям этой короткой цепочки импликаций, получим:
str(a, n, 1) ≠ str(b, n, 1) ⇒ ¬ ( a = b )
К заключению импликации мы можем добавлять любой дизъюнктивный член по аксиоме III.1 раздела 4. Приложение. И по правилу силлогизма получим:
str(a, n, 1) ≠ str(b, n, 1) ⇒ ( ¬ ( a = b ) ∨ ¬ ( m = 0) )
Если вынести знак отрицания за скобки в заключении данной импликации, то получим (докажем) нужное нам предложение:
1.1. str(a, n, 1) ≠ str(b, n, 1) ⇒ ¬ ( m = 0 ∧ a = b ).
Кроме того, в соответствии с леммой (л.9.2) имеем:
str(a, n, 1) ≠ str(b, n, 1) ⇒
( (str(a, n, 1) ≠ str(b, n, 1) ⇒ ¬ (m = 0 ∧ a = b))
⇒ [ ( str(a, m, 1) ≠ str(b, m, 1) ∧ (∀ i < m: str(a, i, 1) = str(b, i, 1)) ) ⇔ C(m, a, b) ]
)
Посылки можно переставлять местами, поэтому предложение 1.1 на первое место и убираем её по правилу MP, так как оно истинна. Получим:
str(a, n, 1) ≠ str(b, n, 1)
⇒ [ ( str(a, m, 1) ≠ str(b, m, 1) ∧ (∀ i < m: str(a, i, 1) = str(b, i, 1)) ) ⇔ C(m, a, b) ]
В силу леммы (л.9.1) и последней эквивалентности имеем (заменяя в лемме (л.9.1) формулу под квантором ∃_1 на эквивалентную формулу):
str(a, n, 1) ≠ str(b, n, 1) ⇒ ∃_1 m C(m, a, b). Ветка 1 доказана.
Ветка 2.
Докажем ∃_1 m C(m, a, b) при условии
a = b
Очевидно, что
a = b ⇒ ∃_1 m (m = 0 ∧ a = b)
Теперь аналогично предложению 1.1 в ветке 1 получаем предложение:
2.1. a = b ⇒ ¬ ( str(a, m, 1) ≠ str(b, m, 1) ∧ (∀ i < m: str(a, i, 1) = str(b, i, 1)) )
Действительно:
a = b ⇒ (∀ i str(a, i, 1) = str(b, i, 1))
А далее по цепочке силлогизмов (многоточие в посылке - это заключение предыдущей импликации):
… ⇒ str(a, m, 1) = str(b, m, 1)
… ⇒ str(a, m, 1) = str(b, m, 1) ∨ ¬ (∀ i < m: str(a, i, 1) = str(b, i, 1))
… ⇒ ¬ ( str(a, m, 1) ≠ str(b, m, 1) ∧ (∀ i < m: str(a, i, 1) = str(b, i, 1)) )
Истинность импликации 2.1 очевидна, так как неравенство элементов алфавита на местах m невозможно для равных строк. И данный вывод не требует правил вывода помимо MP, так как опирается на силлогизм и аксиому (a) ∀ x A(x) ⇒ A(a) из Раздела 4. Приложение.
Это предложение 2.1 истинно, и мы точно так же сокращаем его после применения леммы (л.9.2), как и в ветке 1. Получим:
a = b ⇒ [ (m = 0 ∧ a = b) ⇔ C(m, a, b) ]
Поэтому из последней формулы и написанного выше предложения
a = b ⇒ ∃_1 m (m = 0 ∧ a = b), получим (заменяя в данном предложении формулу под квантором ∃_1 на эквивалентную формулу):
a = b ⇒ ∃_1 m C(m, a, b). Ветка 2 доказана.
Объединяя ветки 1 и 2, получим:
( str(a, n, 1) ≠ str(b, n, 1) ∨ a = b ) ⇒ ∃_1 m C (m, a, b)
По правилу вывода из раздела 4. Приложение:
(β) Если верно B(a) ⇒ U, то верно ∃ x B(x) ⇒ U
Получим:
(∃ n str(a, n, 1) ≠ str(b, n, 1) ∨ a = b ) ⇒ ∃_1 m C(m, a, b)
Теперь, чтобы доказать, что ∃_1 m C(m, a, b), достаточно доказать посылку последней импликации и отбросить её по правилу MP. Итак, осталось доказать:
∃ n ( str(a, n, 1) ≠ str(b, n, 1) ∨ a = b )
По пункту VI.9 из раздела 4. Приложение:
∃ n ( str(a, n, 1) ≠ str(b, n, 1) ∨ a = b ) ⇔ ( a = b ∨ ∃ n str(a, n, 1) ≠ str(b, n, 1))
По (8.1) a = b ⇔ ∀ i str(a, i, 1) = str(b, i, 1) и по VI.7 из раздела 4. Приложение:
a = b ⇔ ¬ (∃ n str(a, n, 1) ≠ str(b, n, 1)), поэтому:
∃ n ( str(a, n, 1) ≠ str(b, n, 1) ∨ a = b ) ⇔ ( a = b ∨ ¬ (a = b) )
Правая часть эквивалентности доказана из-за тавтологии
A ∨ ¬ A
Таким образом,
∃ n ( str(a, n, 1) ≠ str(b, n, 1) ∨ a = b ) доказано, а с ним доказано и ∃_1 m C(m, a, b), в силу чего (9.1) является определением.
(с.9.1) len(a) ≠ ⊖ ⇒ [ 0 < CompIn(a, b) ≤ len(a) ⇔ ∀ u CompIn(a ⋅ u, b) = CompIn(a, b) ], и то же верно, если в этом следствии заменить CompIn(a, b) и CompIn(a ⋅ u, b) на CompIn(b, a) и CompIn(b, a ⋅ u) соответственно.
Пояснение: если строка a конечна (len(a) ≠ ⊖) и отличие от строки b есть (0 < CompIn(a, b)) и находится в пределах строки a (CompIn(a, b) ≤ len(a)), то это тот и только тот случай, когда для любой строки a ⋅ u, начало которой равно конечной строке a, имеется первое отличие от строки b в той же позиции, в которой в строке a находится первое отличается от строки b.
Тут мы впервые доказываем возможность игнорировать в строке всё, кроме её ограниченного начала, но при этом получить интересующий нас результат для всей строки при определённых условиях.
Доказательство.
Предполагаем, что len(a) ≠ ⊖ и в условиях этой гипотезы дедукции нам для доказательства (с.9.1) достаточно доказать эквивалентность:
0 < CompIn(a, b) ≤ len(a) ⇔ ∀ u CompIn(a ⋅ u, b) = CompIn(a, b)
Для доказательства данной эквивалентности надо доказать две импликации:
Ветка 1: 0 < CompIn(a, b) ≤ len(a) ⇒ ∀ u CompIn(a ⋅ u, b) = CompIn(a, b)
Ветка 2: ∀ u CompIn(a ⋅ u, b) = CompIn(a, b) ⇒ 0 < CompIn(a, b) ≤ len(a)
Ветка 1.
Определение (9.1) для CompIn(a, b), когда CompIn(a, b) ≠ 0, и CompIn(a, b) ≤ len(a) (наши дедуктивные гипотезы):
( str(a, CompIn(a, b), 1) ≠ str(b, CompIn(a, b), 1) ∧ (∀ i i < CompIn(a, b) ⇒ str(a, i, 1) = str(b, i, 1)) )
Так как для всех i (под квантором общности) в данном предложении верно i ≤ len(a), то будет верно в силу аксиомы (7.1) о результате конкатенации при конечной 1-й строке:
str(a ⋅ u, i, 1) = str(a, i, 1)
И то же самое можно сказать про
str(a ⋅ u, CompIn(a, b), 1) = str(a, CompIn(a, b), 1)
Поэтому, по аксиомам для равенства можно заменить в первом предложении Ветки 1 все str(a, i, 1) на str(a ⋅ u, i, 1), а str(a, CompIn(a, b), 1) можно заменить на str(a ⋅ u, CompIn(a, b), 1).
И тогда выяснится, что число CompIn(a, b) полностью удовлетворяет определению для CompIn(a ⋅ u, b).
Таким образом, доказано:
0 < CompIn(a, b) ≤ len(a) ⇒ CompIn(a ⋅ u, b) = CompIn(a, b)
И по схеме вывода из Раздела 4. Приложение
(α) Если верно U ⇒ B(a), то верно U ⇒ ∀ x B(x)
Получим:
0 < CompIn(a, b) ≤ len(a) ⇒ ∀ u CompIn(a ⋅ u, b) = CompIn(a, b), ветка 1 доказана.
Ветка 2.
Возьмём контрапозицию, эквивалентную доказываемой импликации:
[ CompIn(a, b) = 0 ∨ len(a) < CompIn(a, b)] ⇒ ¬ ∀ u CompIn(a ⋅ u, b) = CompIn(a, b)
Правую часть перепишем в соответствии с п. VI.7 Раздела 4. Приложение. И разобьём доказательство полученной импликации на доказательство 2-х импликаций:
Ветка 2.1: CompIn(a, b) = 0 ⇒ ∃ u CompIn(a ⋅ u, b) ≠ CompIn(a, b)
Ветка 2.2: len(a) < CompIn(a, b) ⇒ ∃ u CompIn(a ⋅ u, b) ≠ CompIn(a, b)
После того, как Ветки 2.1 и 2.2 будут доказаны, из них выводится исходная Ветку 2 в силу тавтологии:
(A ⇒ C) ⇒ ((B ⇒ C) ⇒ ((A ∨ B )⇒ C)), п.III.3 Раздела 4. Приложение.
Ветка 2.1. CompIn(a, b) = 0 - предположение дедукции.
Так как CompIn(a, b) = 0, то из определения (9.1) получаем:
a = b
Положим:
u = Chr(0)
Очевидно (легко выводится из a = b и len(a) ≠ ⊖):
CompIn(a ⋅ Chr(0), b) ≠ CompIn(a, b)
Так как левая часть неравенства (CompIn(a ⋅ Chr(0), b)) имеет значение len(a) ′, а правая (CompIn(a, b)) - имеет значение 0 (ноль).
Из аксиомы (b) Раздела 4. Приложение:
CompIn(a ⋅ u, b) ≠ CompIn(a, b) ⇒ ∃ u CompIn(a ⋅ u, b) ≠ CompIn(a, b)
А, значит, верно, при подстановке в свободную (не под квантором) переменную u:
CompIn(a ⋅ Chr(0), b) ≠ CompIn(a, b) ⇒ ∃ u CompIn(a ⋅ u, b) ≠ CompIn(a, b)
Так как посылка импликации истинна, то получаем:
∃ u CompIn(a ⋅ u, b) ≠ CompIn(a, b), вспоминая предположение дедукции ветки 2.1 - получаем её доказательство.
Ветка 2.2. len(a) < CompIn(a, b) - предположение дедукции.
Так как len(a) < CompIn(a, b), то из определения (9.1) получаем:
∀ i ≤ len(a): str(a, i, 1) = str(b, i, 1)
Поэтому, из (т.8.5) получаем
beg(b, len(a)) = a
Положим:
u = end(b, len(a) ′)
Тогда по (1) получаем:
b = a ⋅ end(b, len(a) ′ )
Поэтому:
CompIn(a ⋅ end(b, len(a) ′), b) ≠ CompIn(a, b)
Последнее неравенство истинное, потому что слева - 0 (ноль), а справа CompIn(a, b) > 0.
Дальше вывод аналогичен ветке 2.1, поэтому ветка 2.2. доказана.
Следствие (с.9.1) доказано.
(9.2) Определение для Comp(a, b):
Comp(a, b) = Comp(str(a, CompIn(a, b), 1), str(b, CompIn(a, b), 1))
Очевидно, что это определение.
1. Если строки не равны, то результат Comp(a, b) совпадает с результатом сравнения элементов алфавита на том месте (в обоих строках), где это отличие возникло впервые от 1 места и до данного, Вопрос сводится к сравнению элементов алфавита в силу аксиомы (5.1) ∀ a ∀ i ∃ j str(a, i, 1) = Chr(j). А сравнение для элементов алфавита было определено в аксиоме (5.4).
2. Если строки равны, то результат сравнения будет равен нулю, потому что
CompIn(a, b) = 0 для равных строк, в силу чего
Comp(str(a, 0, 1), str(b, 0, 1)) = Comp(⊖, ⊖) = 0
В последней строке вывода были использованы определение (4.1) str(a, i, j) = beg(end(a, i), j) и аксиома (2.2) end(a, 0) = ⊖, и ещё аксиома (2.4) beg(⊖, i) = ⊖.
Критерий локального сравнения данных:
(с.9.2) len(a) ≠ ⊖ ⇒ [ 0 < CompIn(a, b) ≤ len(a) ⇔ ∀ u Comp(a ⋅ u, b) = Comp(a, b) ], и то же верно, если в этом следствии заменить CompIn(a, b), Comp(a ⋅ u, b) и Comp(a, b) на CompIn(b, a), Comp(b, a ⋅ u) и Comp(b, a) соответственно.
Заметим, что в левой и правой частях эквивалентностей используются разные функции. В левой - CompIn(a, b), как в следствии (с.9.1), а в правой - Comp(a, b), которая определена в последней аксиоме (9.2).
Доказательство.
По аналогии с доказательством (с.9.1) рассмотрим две импликации при гипотезе дедукции len(a) ≠ ⊖.
Ветка 1.
Из доказательства Ветки 1 в (с.9.1) знаем, что когда CompIn(a, b) ≠ 0, и CompIn(a, b) ≤ len(a), то
CompIn(a ⋅ u, b) = CompIn(a, b)
И из доказательства (с.9.1) для всех i < len(a) верно
str(a ⋅ u, i, 1) = str(a, i, 1)
Поэтому из определения (9.2) - заменяя сразу CompIn(a ⋅ u, b) и str(a ⋅ u, …, 1) на равные им CompIn(a, b) и str(a, …, 1):
Comp(a ⋅ u, b) = Comp(str(a, CompIn(a, b), 1), str(b, CompIn(a, b), 1)) = Comp(a, b)
Поэтому Ветка 1 доказана.
Ветка 2.1: CompIn(a, b) = 0 ⇒ ∃ u Comp(a ⋅ u, b) ≠ Comp(a, b)
Как и в доказательстве Ветки 2.1 следствия (с.9.1) рассматриваем
u = Chr(0) и выводим заключение импликации из
Comp(a ⋅ Chr(0), b) = Comp(str(a ⋅ Chr(0), CompIn(a ⋅ Chr(0), b), 1), str(b, CompIn(a ⋅ Chr(0), b), 1))
= Comp(str(a ⋅ Chr(0), len(a) ′, 1), str(b, len(a) ′, 1)) = Comp(Chr(0), ⊖) = 2
Результат 2 отличается от Comp(a, b) = 0.
Завершение доказательства - по аналогии с Веткой 2.1 из доказательства для (с.9.1).
Ветка 2.2: len(a) < CompIn(a, b) ⇒ ∃ u Comp(a ⋅ u, b) ≠ Comp(a, b)
В качестве предположения дедукции-2 возьмем не просто len(a) < CompIn(a, b), но:
CompIn(a, b) ≠ 0 ∧ len(a) < CompIn(a, b), в соответствии с теоремой VI.10 из раздела 4. Приложение.
Как и в Ветке 2.2 доказательства (с.9.1) рассматриваем
u = end(b, len(a) ′ ) и выводим
Comp(a ⋅ u, b) = 0, так как мы добились равенства a ⋅ u = b.
И этот результат 0 (ноль) отличается от Comp(a, b) ≠ 0 из предположения дедукции-2.
Завершение доказательства - по аналогии с Веткой 2.1
Следствие (с.9.2) доказано.
(л.9.3) Лемма о минимальной позиции совпадения в строке:
what ≠ ⊖ ∧ len(what) ≠ ⊖ ∧ str(in, n, len(what)) = what ⇒
∃_1 m (str(in, m, len(what)) = what ∧ (∀ i < m: str(in, i, len(what)) ≠ what))
Пояснение. Это лемма о том, что если в строке in имеется подстрока (не пустая и не бесконечная), равная строке what, то можно найти такую подстроку, равную what, которая начиналась бы в строке in раньше (на позиции с самым маленьким номером), чем любые другие такие строки.
Логика данной формулы идентична логике формулы (л.9.1) - меняется только способ сравнения: вместо поиска самого раннего отличия в данной позиции у данной строки ищется самое раннее совпадение начиная с данной позиции у данной строки. Доказательство аналогичное доказательству (л.9.1).
(9.3) Определение для find(in, what, 0):
( what ≠ ⊖ ∧ len(what) ≠ ⊖ ∧ str(in, find(in, what, 0), len(what)) = what
∧ ∀ j (j < find(in, what, 0) ⇒ str(in, j, len(what)) ≠ what)
) ∨ ( find(in, what, 0) = 0 ∧ (what = ⊖ ∨ len(what) = ⊖ ∨ ∀ j str(in, j, len(what)) ≠ what) )
Пояснение.
Первый член дизъюнкции соответствует случаю, когда найдена позиция в строке in, с которой начинается такая подстрока в строке in, которая равна строке what. Притом раньше найденной позиции нет никакой другой позиции с таким же совпадением со строкой what, а строка what не является ни пустой, ни бесконечной.
Второй член дизъюнкции - это случай равенства нулю: это случай, когда строка what является либо пустой, либо бесконечной, либо ни на каких местах в строке in не начинается подстрока, равная строке what.
В принципе, можно было бы включить в состав находимых и варианты с бесконечной подстрокой, но не вижу в этом необходимости с практической точки зрения. Если же необходимость возникнет, то можно будет тогда определить функцию расширенного поиска бесконечной подстроки.
Сейчас же логика функции find(in, what, 0) почти совпадает с логикой функции CompIn(a, b). Даже проще, так как случай what = ⊖ сразу попадет в «прочие» для find(in, what, 0), в отличие от b = ⊖ для CompIn(a, b).
Так как логика формулы (9.3) аналогична логике формулы (9.1), как логика леммы (л.9.3) аналогична логике леммы (л.9.1), то:
Доказательство на основе леммы (л.9.3) того, что аксиома (9.3) является определением - проводится почти идентично тому (с учетом разницы в способе признания результата в данной строке в данной позиции - искомым), как доказывалось на основе леммы (л.9.1) то, что аксиома (9.1) является определением.
Поэтому считаем доказанным то, что аксиома (9.3) является определением для
find(in, what, 0).
(9.4) Определение для find(in, what, i):
find(in, what, i) = find(end(in, i ′ ), what, 0)
Очевидно, что аксиома (9.4) является определением для функции find(in, what, i).
От функции find(in, what, 0) она отличается тем, что ищет позицию совпадения со строкой what в строке in не с первой позиции строки in, а только c (i ′ ) позиции включительно, пропустив первые i символов в строке in.
(9.5) Определение для if_0(a, b, c):
(if_0(a, b, c) = b ∧ a = 0) ∨ (if_0(a, b, c) = c ∧ a ≠ 0)
Пояснение. Если первый аргумент в данной функции равен нулю, то функция принимает значение второго аргумента. В противном случае функция принимает значение третьего аргумента.
Очевидно, что данная аксиома является определением, то есть, предложение:
∃_1 u (u = b ∧ a = 0) ∨ (u = c ∧ a ≠ 0) легко выводится.
(л.9.4) a ≠ a ⋅ Chr(0) ⇔ len(a) ≠ ⊖
Действительно, если верно a ≠ a ⋅ Chr(0), то для бесконечной строки это не так, в силу применив к аксиоме о конкатенации с бесконечной строкой (7.2) контрапозиции и подстановки:
a ≠ a ⋅ Chr(0) ⇒ len(a) ≠ ⊖
В обратную сторону эта импликация доказывается из (т.7.1) которая (напоминание):
len(a_1) ≠ ⊖ ∧ … ∧ len(a_n) ≠ ⊖ ⇒ len(a_1 ⋅ … ⋅ a_n) = len(a_1) + … + len(a_n), так как len(a) ≠ ⊖:
len(a ⋅ Chr(0)) = len(a) + len(Chr(0))
Но из (т.7.2) которая (напоминание):
i ≤ l_ChrLim ⇒ len(Chr(i)) = 1
Получаем:
len(Chr(0)) = 1, и находим:
len(a ⋅ Chr(0)) = len(a) ′
Из арифметики известно - так как len(a) число - что:
len(a) ′ ≠ len(a)
откуда
len(a ⋅ Chr(0)) ≠ len(a)
А из теоремы (т.8.5)
len(a)≠⊖ ⇒ [ a = b ⇔ ∀ i ((len(a) = len(b) ∧ 0 < i ∧ i ≤ len(a)) ⇒ str(a, i, 1) = str(b, i, 1)) ]
Получаем поэтому (из len(a ⋅ Chr(0)) ≠ len(a) и из (т.8.5), меняя обе стороны в эквивалентности на свои отрицания):
a ≠ a ⋅ Chr(0)
Значит, эквивалентность
a ≠ a ⋅ Chr(0) ⇔ len(a) ≠ ⊖
доказана по теореме дедукции и в «обратную» сторону.
Принципиальная необходимость следующих трёх определений будет понятна после трёх подразделов, которые следуют за текущим подразделом.
(9.6) Определение для функции Ins(a, i, b):
Ins(a, i, b) = beg(a, max(i, 1) - 1) ⋅ b ⋅ end(a, if_0(min(len(len(b)), i), 0, len(b) + i))
Данная функция представляет собой композицию аксиоматизированных и определённых ранее или в арифметике функций, поэтому нет нужды в доказательстве того, что (9.6) - определение.
Пояснение. Функция Ins(a, i, b) «вставляет» строку b внутрь строки a, заменяя своими символами все те символы строки a, номера мест которых в строке a начинаются с i-го (включительно) и заканчиваются i+ len(b)-1-м. По крайней мере, так происходит, когда значение переменной a имеет достаточно большой размер. То есть, когда в строке a на местах номер с i-го по i+len(b)-1 находятся символы.
Если же размер len(a) < i, то строка b просто допишется (при помощи конкатенации) к концу строки a.
Если же размер len(a) ≥ i, но при этом вся строка b не может «влезть» в исходные пределы строки a (потому что len(a) < i + len(b) - 1), то от строки a останется только beg(a, i-1), а дальше будет дописана строка b.
Но всё сказанное о значении функции Ins(a, i, b) верно лишь в том случае, если i ≠ 0. Потому что если i = 0, то значением функции Ins(a, i, b) будет b.
Для чего нам нужна эта функция? Для того, чтобы наша теория была способна выразить такую работу алгоритма, при которой алгоритм изменяет лишь часть данных (то, что у нас в теории будет «в начале» переменной). И чтобы получить результат этой работы, алгоритму не требуется ни чтения «лишней» части данных, ни изменения этих «лишних» данных. И, как мы увидим дальше, такая выразительность не может быть достигнута ни рекурсивными функциями, ни в рамках арифметики.
Более формально говоря, нам необходимо сформулировать такие «корректные» условия для «локальной вставки», при которых будет верно:
∀ u Ins(a ⋅ u, i, b) = Ins(a, i, b) ⋅ u
При этом «хвост» u не должен «сдвинуться» в строке Ins(a, i, b) ⋅ u, если сравнивать его положение с положением в строке a ⋅ u:
len(a) = len(Ins(a, i, b))
Теперь мы приступим к реализации всей этой программы.
Определим следующую функцию проверки выполнения комплекса условий для локальной вставки:
(9.7) Определение для функции IsIns(q_a, i, q_b):
( IsIns(q_a, i, q_b) = 1 ∧ i ≠ 0 ∧ q_a ≠ ⊖ ∧ q_b ≠ ⊖ ∧ (q_b = 0 ∨ q_a ≥ i + q_b - 1) )
∨ ( IsIns(q_a, i, q_b) = 0 ∧ (i=0 ∨ q_a = ⊖ ∨ q_b = ⊖ ∨ (q_b ≠ 0 ∧ q_a < i + q_b - 1)) )
Очевидно, что это определение, потому что первый член дизъюнкции описывает набор всех «корректных» условий (пока «корректность» не доказана - пишу кавычки), а второй член дизъюнкции описывает случай отрицания первого набора. И для «корректного» набора условий есть единственное значение функции - равное 1. А для любого «некорректного» набора тоже единственный результат функции - равный 0. И эти результаты не равны (1≠0).
Но не только «вставку» новой строки b в старую строку a можно сделать так, что при любом продолжении старой строки a строкой u не было никаких изменений в строке u ни в содержании, ни в положении строки u внутри a ⋅ u после изменения:
∀ u Ins(a ⋅ u, i, b) = Ins(a, i, b) ⋅ u
Точно так же и получать значения из строки можно независимо от того, началом в какой строке a ⋅ u является строка a:
∀ u str(a ⋅ u, i, j) = str(a, i, j)
И для вычисления того, когда данное выражение истинно, мы определим соответствующую функцию.
(9.8) Определение для функции IsStr(q_a, i, j):
( IsStr(q_a, i, j) = 1 ∧ q_a ≠ ⊖ ∧ (i = 0 ∨ j = 0 ∨ q_a ≥ i + j - 1) )
∨ ( IsStr(q_a, i, j) = 0 ∧ (q_a = ⊖ ∨ (i ≠ 0 ∧ j ≠ 0 ∧ q_a < i + j - 1)) )
Очевидно, что это определение, по тем же причинам, что были написаны для определения (9.7).
Пояснение. Разница между извлечением подстроки и вставкой в строку состоит в том, что при вставке с нулевого символа - всё заменяется новым значением. А при извлечении с нулевого места в качестве результата получается пустая строка. И такое значение результата не зависит от того, какая строка u продолжает строку a в строке a ⋅ u. Поэтому данная функция IsStr(q_a, i, j) возвращает 1 (в отличие от нуля функции IsIns(q_a, i, q_b) при аналогичных условиях), если подстроку пытаются получить с нулевого места строки a (или строки a ⋅ u). А в остальном функции IsIns(q_a, i, q_b) и IsStr(q_a, i, j) работают схожим образом.
Только функция IsIns(q_a, i, q_b) делает дополнительную проверку по аргументу q_b - не соответствует ли его значение строке с бесконечной длиной, а в функции IsStr(q_a, i, j) изначально используется j для извлечения конечной строки длины j (или меньше, если в строке с длиной q_a не хватит символов).
(9.9) Определение для ss(i) и ss_k(i):
len(ss(i)) = i ∧ ∀ j ≤ i: str(ss(i), j, 1) = Chr(0). Функция ss_k(i) определяется так же, но только вместо Chr(0) используется Chr(k), где k ≤ l_ChrLim.
То, что (9.9) является определением - очевидно. Формально существование ss(i) можно вывести по индукции из ss(0) = ⊖ и ss(i ′ ) = ss(i) ⋅ Chr(0). А единственность этого существования следует из (т.8.5):
len(a) ≠ ⊖ ⇒ [ a = b ⇔ ∀ i ((len(a) = len(b) ∧ 0 < i ∧ i ≤ len(a)) ⇒ str(a, i, 1) = str(b, i, 1)) ]