2.IV. Равенство строк
. К оглавлению . Показать весь текст .
Аксиома о равенстве строк:
(8.1) a = b ⇔ ∀ i str(a, i, 1) = str(b, i, 1)
Пояснения.
Аксиома равенства строк – независима от предыдущих. Так как функции взятия подстроки могут сохранять «ссылку» на исходный объект и этим отличаться от «нового» (возникшего в результате конкатенации, например) объекта – это опять опыт из программирования. И без данной аксиомы теорию, составленную из предыдущих аксиом (до 8.1, не включая) можно расширить таким образом, что будет верным:
str(«строка», 1, 3) ≠ «стр», при этом никаких противоречий не возникнет.
Действительно, результат «строка».str(«строка», 1, 3) может допускать возможность выяснить – с какой позиции была получена данная подстрока и из какой строки. И получать эти значения можно при помощи свойств i_{in}(a) и parent(a) соответственно. И тогда будет верно:
«строка».str(1, 3).i_{in} = 1
«строка».str(1, 3).parent = «строка».
В то время как у подстроки, содержащей все символы, свойство parent может возвращать (если так запрограммировать) результат «стр»:
«стр».parent = «стр»
Получается, что НЕ верно:
«строка».str(1, 3) = «стр»
Так как, в соответствии с аксиомами равенства (см. Раздел 4 Приложение):
(J_1) a = a
(J_2) a = b ⇒ ( A(a) ⇒ A(b) )
И в случае равенства должно было быть:
«строка».str(1, 3). parent = «стр». parent, что неверно в разбираемом примере.
А это значит, что без аксиомы (8.1), а только на основе изложенных ранее аксиом, невозможно доказать, что:
str(«строка», 1, 3) = «стр», потому что у нас есть непротиворечивое расширение теории, в которой доказывается отрицание данного равенства.
Тут есть нюанс: до аксиомы алфавита (не включая аксиому алфавита) все строки (аргументы, которые находятся на месте для произвольных строк в функциях) являются одной и той же строкой, либо её производной (результатом некоторых функций от общей произвольной строки-предка) . Для таких аксиом все равенства подразумевают одинаковые дополнительные свойства (i_{in}(a) и parent(a)).
Но аксиома алфавита и аксиома о результате конкатенации являются единственными аксиомами перед аксиомой о равенстве строк, где присутствуют произвольные строки, которые не являются производными (через некоторые функции) от общей строки-предка. Однако, в обоих этих аксиомах с обеих сторон равенства всегда находятся строки из единственного элемента алфавита каждая.
Поэтому для непротиворечивого построения теории со свойствами i_{in}(a) и parent(a) надо считать, что они сохраняются лишь для строк, длина которых больше 1. Как только из строки получена пустая строка или подстрока длиной 1 – эти свойства меняются на «базовые». Например, имеется аксиома:
a.str(i, 1).parent = a.str(i, 1)
То есть, строка из одного символа и пустая строки всегда – «независимы» и имеют в качестве «предков» самих себя.
А это значит, что всё же можно построить непротиворечивую теорию, расширяющую аксиомы перед аксиомой равенства строк, если считать, что равенство имеется только тогда, когда у равных строк не только последовательность символов a.str(i, 1) одинакова по i, но одинакова последовательность символов по i и в a.parent.str(i, 1).
Таким образом, доказана следующая метатеорема:
(м.8.1) Аксиома (8.1) независима от предыдущих аксиом, так как есть пример из ООП (объектно-ориентированного программирования), когда функции beg() и end() создают «детей» у «независимых» строк. И между «независимыми» строками и «детьми» есть разница помимо последовательности символов. Такие объекты ООП соответствуют всем аксиомам перед аксиомой (8.1), но не соответствуют аксиоме (8.1).
Как уже упоминалось, доказательство у метатеорем всегда неформально и в силу этого есть риск пропустить в рассуждениях важный нюанс, из-за пропуска которого доказательство окажется ошибочным. Например, в последней метатеореме можно было упустить нюанс с «независимостью» элементов алфавита. Поэтому к доказательствам метатеорем надо относиться с особой осторожностью.
Впрочем, метатеоремы не влияет на внутреннюю логику теории, к которой они относятся, даже если метатеорема ошибочна. Но в случае ошибочности метатеоремы будет не совсем верным наше неформальное понимание «внутренней логики» теории – что всё равно не создаёт риска построения ошибочных логических выводов средствами самой теории.
Для того, чтобы мы могли использовать знак равенства в нашей теории «обычным» образом (а мы именно это и делали) необходимо, чтобы для теории были истинны 2 следующих аксиомы теории первого порядка с равенством (см. Раздел 4. Приложение):
(J_1) a = a
(J_2) a = b ⇒ ( A(a) ⇒ A(b) )
Где A(a) представляет собой любую логически корректную формулу, построенную из функциональных букв, предикатных букв теории, кванторов (в область действия которых не попадают a, b) и логических связок.
Но на самом деле – тут тонкий момент, чтобы то, что ты понимаешь под знаком равенства, действительно обладало свойствами равенства. И пояснения к аксиоме (8.1) – тому пример. Просто написание знака «=» в некоторых аксиомах не делает предикаты на его основе соответствующим утверждениям (J_1) и (J_2).
Однако у нас есть критерий, который позволяет отнести теорию первого порядка в категорию теории первого порядка с равенством – см. Раздел 4. Приложение, пункт VI.4. Вот в соответствии с этим пунктом мы и допишем необходимые нам для получения теории первого порядка с равенством утверждения. И допишем их в качестве аксиом:
a. Для каждой функциональной буквы f_n() с аргументами x_1, … x_m (где m – количество аргументов функции f_n(x_1, … x_m)) должно быть истинно:
(x_1=y_1 ∧ … ∧ x_m=y_m) ⇒ (f_n(x_1, … x_m) = f_n(y_1, … y_m))
Поэтому:
(8.2) (x_1 = y_1 ∧ x_2 = y_2) ⇒ x_1 ⋅ x_2 = y_1 ⋅ y_2
(8.3) (x = y ∧ i = j) ⇒ beg(x, i) = beg(y, j)
(8.3) (x = y ∧ i = j) ⇒ end(x, i) = beg(y, j)
Тут, вроде, надо было бы написать ещё аксиому для функции следования (i ′ ). Но для неё всё нужное уже доказано в теории Пеано – как и для других арифметических операций (сравнения чисел определяются в арифметике, поэтому тоже соответствуют). А теория Пеано тоже является частью нашей теории и будет явно включена в теорию строк в следующем разделе.
(8.4) (i = j) ⇒ Chr(i) = Chr(j)
Заметим, что для тех функций, которые были определены – мы аксиом равенства не пишем, так как соответствующие утверждения выводятся из других аксиом, которые не являются определениями.
b. Для знака равенства должна быть истинна рефлексивность x = x. Поэтому:
(8.5) x = x
В теории Пеано данное равенство не аксиоматизируется, так как оно следует для натуральных чисел из аксиомы x + 0 = x. Но в теории строк я это утверждение аксиоматизирую.
c. Для знака равенства должна быть истинна транзитивность x = y ⇒ (z=x ⇒ z=y). Поэтому:
(8.6) x = y ⇒ (z = x ⇒ z = y)
Возможно, что некоторые (или даже все) из аксиом равенства (8.2)-(8.6) можно вывести из предыдущих аксиом. Но это уже второстепенная задача, а у любителя математики (я про себя) нет возможности заниматься ещё и этим исследованием. К тому же задача по аккуратному построению теории строк является задачей для математического сообщества, и неправильно взваливать её на одного человека – даже если бы речь шла о профессионале.
Кстати, в учебнике Э. Мендельсона «Введение в математическую логику» доказательство того, что теория Пеано – теория первого порядка с равенством – занимает несколько страниц в Главе 3. Формальная арифметика. Раздел 1. Система аксиом. От леммы 3.1. до следствия 3.3 включительно. Боюсь, что в теории строк аналогичные доказательства заняли бы значительно больше места – а придумать их намного труднее, чем прочитать.
В учебнике А. С. Герасимова «Курс математической логики и теории вычислимости» нужные для равенства утверждения не доказываются, а аксиоматизируются для теории Пеано. Что никаких противоречий не создаёт и тоже вполне возможно. Занятно, что в отличном учебнике Дж. Булос, Р Джеффри – «Вычислимость и логика» вопрос о равенстве для теории Пеано оказывается упущенным из вида, и среди аксиом теории Пеано нет необходимой аксиомы о транзитивности равенства.
Можно сказать, что вопрос о равенстве для теории строк в данной статье не упущен, но до идеала не «отполирован», чего едва ли можно требовать от статьи.
Ассоциативность конкатенации:
(т.8.1) (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)
Очевидная теорема, следует из аксиом (7) и (8.1). Если бы вместо аксиом (7) у нас была аксиома для слияния упорядоченных массивов символов в упорядоченный массив символов, то помимо ассоциативности была доказана ещё и коммутативность. Но конкатенация строк не обладает таким свойством, разумеется.
(т.8.2) len(a) ≠ ⊖ ⇒ a = str(a, 1, len(a)), в силу чего в отношении конечной строки a, в виде str(a, 1, len(a)), можно применять теоремы (т.4.4) и от (т.4.6) до (т.4.9) включительно.
Доказательство.
Исходим из предположения len(a) ≠ ⊖.
Будем использовать (т.4.6) str(a, 1, j) = beg(a, j).
При len(a) = 0 теорема истинна, так как тогда a = ⊖ и str(a, 1, len(a)) = str(a, 1, 0) = ⊖, поэтому:
a = str(a, 1, len(a))
Поэтому нам осталось рассмотреть случай len(a) = 0 ∧ len(a) ≠ ⊖.
Из (т.4.2) (i ≠ 0 ∧ j ≠ 0) ⇒ str(a, i, j) = end(beg(a, i + j - 1), i) при j = 1 получим:
str(beg(a, len(a)), i, 1) = end(beg(beg(a, len(a)), i), i)
При i ≤ len(a), из (т.3.1) beg(a, min(i, j)) = beg(beg(a, i), j) получим:
end(beg(beg(a, len(a)), i), i) = end(beg(a, i), i)
По (4.2) end(beg(a, i), i) = beg(end(a, i), 1) и определению (4.1) для str() получим:
end(beg(a, i), i) = str(a, i, 1)
Таким образом (раз доказано для случая i ≠ 0 ∧ i ≤ len(a)):
0 < i ≤ len(a) ⇒ str(beg(a, len(a)), i, 1) = str(a, i, 1)
При len(a) < i из (т.4.4) j < k ⇒ str(str(a, i, j), k, 1) = ⊖ получим:
str(str(a, 1, len(a)), i, 1) = ⊖
Так как, (т.4.6) str(a, 1, len(a)) = beg(a, len(a)) то доказано:
len(a) < i ⇒ str(beg(a, len(a)), i, 1) = ⊖
С другой стороны, (т.6.3) len(a) ≠ ⊖ ⇒ (len(a) < i ⇒ str(a, 1, i) = ⊖), поэтому при данных условиях
len(a) < i ⇒ str(a, 1, i) = ⊖
Из последних 2 равенств получаем:
len(a) < i ⇒ str(beg(a, len(a)), i, 1) = str(a, 1, i)
Таким образом, у нас при сделанном предположении len(a) ≠ ⊖ доказаны 2 импликации:
0 < i ≤ len(a) ⇒ str(beg(a, len(a)), i, 1) = str(a, i, 1)
len(a) < i ⇒ str(beg(a, len(a)), i, 1) = str(a, 1, i)
Добавляем очевидную третью импликацию, где в заключении стоит равенство, в которой обе стороны равны пустой строке ⊖:
i = 0 ⇒ str(beg(a, len(a)), i, 1) = str(a, i, 1)
Объединяя их в одну импликацию по аксиоме логики III.3 (см. Раздел 4. Приложение) получим:
(0 < i ≤ len(a) ∨ len(a) < i ∨ i = 0) ⇒ str(beg(a, len(a)), i, 1) = str(a, i, 1)
В посылке стоит истинное утверждение, поэтому отбрасываем его по правилу вывода MP. Получаем утверждение:
str(beg(a, len(a)), i, 1) = str(a, i, 1)
По аксиоме равенства строк (8.1) получаем:
a = beg(a, len(a))
То же самое иными обозначениями:
a = str(a, 1, len(a))
оно истинно при истинности предположения нашего доказательства:
len(a) ≠ ⊖
Поэтому по теореме дедукции получаем:
len(a) ≠ ⊖ ⇒ str(a, 1, len(a))
Что и требовалось доказать.
(с.8.2) len(a) ≠ ⊖ ⇒ (len(a) ≤ i ⇒ a = str(a, 1, i))
Очевидное следствие теорем (т.8.2) и (т.4.7) j ≤ k ⇒ str(str(a, 1, j), 1, k) = str(a, 1, j)
(т.8.3) a = a ⋅ ⊖ = ⊖ ⋅ a
Очевидные равенства – из свойств пустой строки ⊖, аксиом для конкатенации и для равенства строк.
(т.8.4) a = b ⇔ ∀ i (0 < i ⇒ str(a, i, 1) = str(b, i, 1))
Очевидное следствие из аксиомы для равенства строк (8.1), так как для случая i = 0 равенство функций:
str(a, 0, 1) = str(b, 0, 1)
выполнено по (4.1) – определению str(), по (2.2) end(a, 0) = ⊖ и (2.4) beg(⊖, q) = ⊖.
(т.8.5) len(a)≠⊖ ⇒ [ a = b ⇔ ∀ i ((len(a) = len(b) ∧ 0 < i ∧ i ≤ len(a)) ⇒ str(a, i, 1) = str(b, i, 1)) ]
Тоже очевидное следствие – уже из (т.8.4) для равенства конечных строк. Если их длины не равны, то для более короткой (пусть b) будет str(b, len(b) ′, 1) = ⊖ при str(a, len(b) ′, 1) ≠ ⊖, то есть – строки не равны тогда. Если же длины равны, а внутри своих длин строки тоже равны, то за пределами своей длины (одинаковой для них) str() для каждой такой позиции в этих строках возвращает пустую строку и они равны там тоже:
len(a) < i ⇒ str(a, i, 1) = ⊖, что верно и для строки b из (т.6.3) которая (напоминание):
len(a) ≠ ⊖ ⇒ (len(a) < i ⇒ str(a, 1, i) = ⊖).
(т.8.6) len(a) ≠ ⊖ ⇒ a = beg(a ⋅ u, len(a))
Доказательство. Предположение дедукции - len(a) ≠ ⊖.
Сравним beg(a ⋅ u, len(a)) и beg(a, len(a)). Про последнее мы знаем, что
beg(a, len(a)) = a, из-за (т.8.2) len(a) ≠ ⊖ ⇒ a = str(a, 1, len(a)) и (т.4.6) str(a, 1, j) = beg(a, j).
Случай 1. i ≤ len(a)
Из-за теоремы (т.6.4) j ≤ i ⇒ str(beg(a, i), j, 1) = str(a, j, 1) получаем:
str(beg(a ⋅ u, len(a)), i , 1) = str(a ⋅ u, i, 1)
По аксиоме (7.1) которая (напоминание):
len(a) ≠ ⊖
⇒ (i ≤ len(a) ⇒ str(a ⋅ b, i, 1) = str(a, i, 1)) ∧ ( i > len(a) ⇒ str(a ⋅ b, i, 1) = str(b, i - len(a), 1))
Получаем с учётом i ≤ len(a):
str(a ⋅ u, i, 1) = str(a, i, 1)
str(beg(a ⋅ u, len(a)), i , 1) = str(a, i, 1)
Устраняя условие Случая 1, получим:
i ≤ len(a) ⇒ str(a, i, 1) = str(beg(a ⋅ u, len(a)), i , 1)
Случай 2. len(a) < i
str(beg(a ⋅ u, len(a)), i, 1) = str(str(a ⋅ u, 1, len(a)), i, 1)
Из теоремы (т.4.4) j < k ⇒ str(str(a, i, j), k, 1) = ⊖ получаем:
str(str(a ⋅ u, 1, len(a)), i, 1) = ⊖
Аналогично:
str(a, i, 1) = str((str(a, 1, len(a)), i, 1) = ⊖
Из двух последних предложений:
str(a, i, 1) = str(beg(a ⋅ u, len(a)), i , 1)
Устраняя условие Случая 2, получим:
len(a) < i ⇒ str(a, i, 1) = str(beg(a ⋅ u, len(a)), i , 1)
Объединяя Случай 1 и Случай 2 по III.3 из раздела 4. Приложение, получим:
(i ≤ len(a) ∨ len(a) < i) ⇒ str(a, i, 1) = str(beg(a ⋅ u, len(a)), i , 1)
Посылка истинная, поэтому отбрасываем её по MP и получаем:
str(a, i, 1) = str(beg(a ⋅ u, len(a)), i , 1)
В соответствии с аксиомой (8.1) равенства строк получаем:
a = beg(a ⋅ u, len(a))
Устраняя предположение дедукции, завершаем доказательство:
len(a) ≠ ⊖ ⇒ a = beg(a ⋅ u, len(a)), что и требовалось доказать.
(т.8.7) len(a) ≠ ⊖ ⇒ u = end(a ⋅ u, len(a) ′ )
Доказательство. Предположение дедукции - len(a) ≠ ⊖
Если len(a) = 0, то a ⋅ u = ⊖ ⋅ u = u. Откуда end(a ⋅ u, len(a) ′ ) = end(u, 1) = u.
Если len(u) = 0, то a ⋅ u = a ⋅ ⊖ = a. Откуда end(a ⋅ u, len(a) ′ ) = end(a, len(a) ′) = ⊖ = u.
Поэтому для len(a) = 0 ∨ len(u) = 0 теорема истинна и исходим из «внутреннего предположения дедукции №1» (len(a) ≠ 0 ∧ len(u) ≠ 0), будем пропускать эту посылку при использовании аксиом (она выполнена).
str(end(a ⋅ u, len(a) ′ ), i, 1) = beg(end(end(a ⋅ u, len(a) ′ ), i), 1), по (4.1) – определению str()
beg(end(end(a ⋅ u, len(a) ′), i), 1) = beg(end(a ⋅ u, len(a) + i), 1),
Из (т.3.2) (i ≠ 0 ∧ j ≠ 0) ⇒ end(a, i + j - 1) = end(end(a, i), j), но только при i ≠ 0 или эквивалентном 0 < i («внутреннее предположение дедукции №2»):
beg(end(a ⋅ u, len(a) + i), 1) = str(a ⋅ u, len(a) + i, 1), по (4.1) – определению str()
str(a ⋅ u, len(a) + i, 1) = str(u, len(a) + i - len(a), 1), по (7.1) о конкатенации с конечной строкой и того, что i > 0.
Поэтому по всей цепочке предыдущих равенств приравниваем начало с концом:
str(end(a ⋅ u, len(a) ′ ), i, 1) = str(u, i, 1)
Устраняем «внутреннее предположение дедукции №2»:
0 < i ⇒ str(end(a ⋅ u, len(a) ′ ), i, 1) = str(u, i, 1)
Обобщаем данную формулу по i:
∀ i (0 < i ⇒ str(end(a ⋅ u, len(a) ′ ), i, 1) = str(u, i, 1))
И из (т.8.4) a = b ⇔ ∀ i (0 < i ⇒ str(a, i, 1) = str(b, i, 1)) получаем:
u = end(a ⋅ u, len(a) ′ )
Устраняем «внутреннее предположение дедукции №1»:
(len(a) ≠ 0 ∧ len(u) ≠ 0) ⇒ u = end(a ⋅ u, len(a) ′ )
Поскольку ранее было доказано:
(len(a) = 0 ∨ len(u) = 0) ⇒ u = end(a ⋅ u, len(a) ′ )
То соединение этих предложений даёт:
u = end(a ⋅ u, len(a) ′ )
Теперь устраняем предположение дедукции и получаем:
len(a) ≠ ⊖ ⇒ u = end(a ⋅ u, len(a) ′ ), что и требовалось доказать.
(т.8.8) a = ⊖ ⇔ len(a) = 0
В части a = ⊖ ⇒ len(a) = 0 эта эквивалентность выводится из определения для len(⊖), на основании дедуктивного предположения a = ⊖ и результата расчёта len(a) = 0. Но, так как в данном подразделе мы разбираем равенство для теории строк, то упомяну, на чём основывается возможность логического вывода a = ⊖ ⇒ len(a) = 0 для равенства на уровне свойств равенства.
В рамках свойств равенства (если обходиться без теоремы дедукции) выводится:
a = ⊖ ⇒ len(a) = len(⊖)
А затем надо воспользоваться выводимым свойством транзитивности для равенства:
len(⊖) = 0 ⇒ (len(a) = len(⊖) ⇒ len(a) = 0)
Посылка этой импликации истинная и она отбрасывается, после чего остаётся:
len(a) = len(⊖) ⇒ len(a) = 0
И из этого утверждения и ранее полученного a = ⊖ ⇒ len(a) = len(⊖) получаем по правилу силлогизма:
a = ⊖ ⇒ len(a) = 0
Все подробности вывода свойств для равенства можно прочитать в любом учебнике логики, но они и так самоочевидны для читателя с математической подготовкой уровня программиста, например.
Осталось доказать эквивалентность в части:
len(a) = 0 ⇒ a = ⊖
Гипотеза теоремы дедукции: len(a) = 0
Из определения (6.2) для len(a) при len(a) = 0 устраняем 2 ложных члена дизъюнкции, превратив их в истинные посылки. Вот по такой схеме:
A ∨ B ∨ C – исходное определение. Преобразуем его в эквивалентное:
¬ B ⇒ (A ∨ C), но B ложное, так как для него надо len(a) = i, а по условию len(a) = 0. Поэтому ¬ B истинное и его можно убрать по MP. Аналогично с C, где надо len(a) = ⊖, а имеем len(a) = 0 и по (2.6) i ≠ ⊖. После удаления по MP члена C остался член дизъюнкции A. В нашем случае это:
len(a) = 0 ∧ str(a, 1, 1) = ⊖
В истинной конъюнкции истинным является каждый член конъюнкции, поэтому получаем:
str(a, 1, 1) = ⊖
А это значит, что
str(a, i, 1) = ⊖, из-за (т.6.1) i ≤ j ⇒ (str(a, i, 1) = ⊖ ⇒ str(a, j, 1) = ⊖)
что совпадает с: str(⊖, i, 1) = ⊖
И по аксиоме равенства строк получаем: a = ⊖
Поэтому по теореме дедукции выведено: len(a) = 0 ⇒ a = ⊖
Вторая часть эквивалентности доказана, а вместе с ней доказана и эквивалентность (т.8.8).
(с.8.8) len(a) = ⊖ ⇔ len(len(a)) = 0
Очевидное следствие из теоремы (т.8.8), которое получается при подстановке в (т.8.8) выражения len(a) вместо a.
