dmitgu

Category:

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.

Error

default userpic

Your reply will be screened

Your IP address will be recorded 

When you submit the form an invisible reCAPTCHA check will be performed.
You must follow the Privacy Policy and Google Terms of use.