dmitgu

Category:

2.III. Концы строк, соединение строк

. К оглавлению . Показать весь текст .

Аксиома о конце строки, для случая, когда у строки есть конец:

(6.1)  (i ≠ 0 ∧ str(a, i, 1) = ⊖) ⇒ str(a, i ′, 1) = ⊖ 

Пояснение. 

Аксиома конца строк не может быть выведена из предыдущих аксиом. Действительно, рассмотрим случай, когда все «цепочки» элементов алфавита бесконечны, а после ⊖ в «цепочке» может идти любой другой элемент алфавита. А функция beg() (и str() соответственно) возвращает тоже бесконечные «цепочки» элементов алфавита – добавляя после последнего элемента алфавита, извлеченному из исходной «цепочки», ещё и бесконечную «цепочку» из ⊖. 

Изложенная в предыдущем абзаце интерпретация может быть построена в реальности, поэтому не противоречива и эти «цепочки» соответствуют всем изложенным до аксиомы (6.1) аксиомам – не включая аксиому (6.1). 

Поэтому доказана метатеорема:

(м.6.1) Аксиома (6.1) независима от предыдущих аксиом, так как случай, когда пустая строка может чередоваться с другими элементами алфавита внутри «строки», соответствует всем аксиомам перед аксиомой (6.1), а аксиоме (6.1) – не соответствует. 

Именно аксиома (6.1) придаёт символу ⊖ особый смысл, превращая его наличие в строке – на первом месте или после любого символа (не равного пустой строке ⊖, разумеется) строки – в критерий окончания строки.

Очевидно (доказывается по индукции), что:

(т.6.1) 0 < i ≤ j ⇒ (str(a, i, 1) = ⊖ ⇒ str(a, j, 1) = ⊖)

(6.2)  Определение для len(a):

( len(a) = 0 ∧ str(a, 1, 1) = ⊖) 

∨ ( len(a) = i ∧ str(a, i, 1) ≠ ⊖ ∧ str(a, i ′, 1) = ⊖ ) 

∨ ( len(a) = ⊖ ∧ ∀ i str(a, i, 1) ≠ ⊖)

Пояснение.

Если на первом же месте строки стоит пустая строка (то есть, если str(a, 1, 1) = ⊖), то длина строки считается нулевой:

len(a) = 0 ∧ str(a, 1, 1) = ⊖

Если же в строке есть символ (отличный от пустой строки элемент алфавита), то номер места последнего такого символа в строке считается длиной строки:

len(a) = i ∧ str(a, i, 1) ≠ ⊖ ∧ str(a, i ′, 1) = ⊖

А то, что после такого символа уже нет символов – обеспечено из-за (т.6.1). 

Если же строка a вообще нигде не кончается – то есть, на каждом её месте имеется символ (отличный от пустой строки элемент алфавита), то значением функции len(a) является пустая строка ⊖: 

len(a) = ⊖ ∧ ∀ i str(a, i, 1) ≠ ⊖

Случай len(a) = i отличается от случая len(a) = ⊖ из-за того, что i ≠ ⊖ по (2.6).

Доказательство того, что (6.2) является определением, проводится аналогично доказательству для (5.3). 

(т.6.2) len(a) ≠ ⊖ ⇒ str(a, len(a) ′, 1) = ⊖ ∧ (len(a) = 0 ∨ str(a, len(a), 1) ≠ ⊖)

Следует из определения (6.2). Вариант посылки

( len(a) = i ∧ str(a, i, 1) ≠ ⊖ ∧ str(a, i ′, 1) = ⊖ )

Очевидно соответствует (т.6.2). 

Вариант посылки: 

( len(a) = 0 ∧ str(a, 1, 1) = ⊖) 

Тоже соответствует в силу того, что в нём и записано

str(a, len(a) ′, 1) = ⊖, так как 1 = len(a) ′ в данном случае.

К полученным импликациям добавляем «лишнюю» посылку, что не меняет истинности, и получим 2 истинных импликации:

len(a) ≠ ⊖ 

⇒ (( len(u) = i ∧ str(a, i, 1) ≠ ⊖ ∧ str(a, i ′, 1) = ⊖ ) ⇒ str(a, len(a) ′, 1) = ⊖) ∧ (len(a) = 0 ∨ str(a, len(a), 1) ≠ ⊖)

len(a) ≠ ⊖ 

⇒ (( len(u) = 0 ∧ str(a, 1, 1) = ⊖) ⇒ str(a, len(a) ′, 1) = ⊖ ∧ (len(a) = 0 ∨ str(a, len(a), 1) ≠ ⊖)) 

Заодно добавим истинное:

len(a) ≠ ⊖ 

⇒ (( len(u) = ⊖ ∧ ∀ i str(a, i, 1) ≠ ⊖) ⇒ str(a, len(a) ′, 1) = ⊖ ∧ (len(a) = 0 ∨ str(a, len(a), 1) ≠ ⊖))

Последнее верно потому, что вложенные импликации эквивалентны импликации с конъюнкцией посылок, а в данном случае у нас противоречие в конъюнкции посылок: 

len(a) ≠ ⊖ ∧ len(u) = ⊖
А из противоречия следует всё.

Теперь во всех 3 импликациях меняем местами вторую посылку с первой (это даёт эквивалентное утверждение) и получим:

Part_1 ⇒ (len(a) ≠ ⊖ ⇒ str(a, len(a) ′, 1) = ⊖ ∧ (len(a) = 0 ∨ str(a, len(a), 1) ≠ ⊖))

Part _2 ⇒ (len(a) ≠ ⊖ ⇒ str(a, len(a) ′, 1) = ⊖ ∧ (len(a) = 0 ∨ str(a, len(a), 1) ≠ ⊖))

Part_3 ⇒ (len(a) ≠ ⊖ ⇒ str(a, len(a) ′, 1) = ⊖ ∧ (len(a) = 0 ∨ str(a, len(a), 1) ≠ ⊖))

Понятно, что понимается под Part_1, Part_2, Part_3. Из этих 3 импликаций получим по аксиоме логики III.3 из Раздела 4. Приложение, применив её 2 раза:

Part_1 ∨ Part_2 ∨ Part_3 ⇒ (len(a) ≠ ⊖ ⇒ str(a, len(a) ′, 1) = ⊖ ∧ (len(a) = 0 ∨ str(a, len(a), 1) ≠ ⊖))

Но посылка в данной импликации – это определение (6.2), то есть – истинное утверждение. Отбрасываем её по правилу MP. Теорема доказана. 

(т.6.3) len(a) ≠ ⊖ ⇒ ( len(a) < i ⇒ str(a, i, 1) = ⊖ )

Доказательство – из (т.6.1) 0 < i ≤ j ⇒ (str(a, i, 1) = ⊖ ⇒ str(a, j, 1) = ⊖) и (т.6.2) len(a) ≠ ⊖ ⇒ str(a, len(a) ′, 1) = ⊖.

Следующие 2 теоремы позволяют «поглощать» функции end() и beg() – а, значит, и str() – во вложенной композиции тем str(), который применяется к ним в композиции и извлекает элемент алфавита только из одной позиции строки.

Данные теоремы уместно было бы разместить в подразделе «I. Разбиение строк», но они нужны сейчас, после определения функции len() длины строки. Так как с их помощью будут доказаны следующие за ними теоремы о длине подстрок.

(т.6.4) j ≤ i ⇒ str(beg(a, i), j, 1) = str(a, j, 1)

Альтернативное обозначение: 0 < j ≤ i ⇒ a.beg(i).str(j, 1) = a.str(j, 1)

Доказательство при гипотезе дедукции 0 < j ≤ i:

str(beg(a, i), j, 1) = end(beg(beg(a, i), j), j) = end(beg(a, j), j) = str(a, j, 1)

Осталось рассмотреть случай j = 0:

str(beg(a, i), j, 1) = str(beg(a, i), 0, 1) = beg(end(beg(a, i), 0), 1) = beg(⊖, 1) = ⊖

str(a, j, 1) = str(a, 0, 1) = beg(end(a, 0), 1) = beg(⊖, 1) = ⊖

Поэтому и для случая j = 0 доказано:

str(beg(a, i), j, 1) = str(a, j, 1)

Теорема (т.6.4) доказана.

(т.6.5) i ≠ 0 ∧ j ≠ 0 ⇒ str(end(a, i), j, 1) = str(a, i + j - 1, 1)

Альтернативное обозначение: i ≠ 0 ∧ j ≠ 0 ⇒ a.end(i).str(j, 1) = a.str(i + j - 1, 1)

Доказательство при гипотезе дедукции i ≠ 0 ∧ j ≠ 0:

str(end(a, i), j, 1) = beg(end(end(a, i), j), 1) = beg(end(i + j -1), 1) = str(a, i + j - 1, 1)

Теорема (т.6.5) доказана.

(т.6.6) len(a) ≠ ⊖ ∧ 0 < i ≤ len(a) ⇒ str(a, i, 1) ≠ ⊖

Доказательство при дедуктивном предположении len(a) ≠ ⊖ ∧ 0 < i ≤ len(a):

Допустим, имеется такой i, что: 

str(a, i, 1) = ⊖

Тогда в силу (т.6.1) имеем:

0 < i ≤ len(a) ⇒ (str(a, i, 1) = ⊖ ⇒ str(a, len(a), 1) = ⊖)

В силу чего доказано:

str(a, len(a), 1) = ⊖

Но это противоречит (т.6.2)

len(a) ≠ ⊖ ⇒ str(a, len(a) ′, 1) = ⊖ ∧ (len(a) = 0 ∨ str(a, len(a), 1) ≠ ⊖)

Так как при имеющимся дедуктивном предположении верно:

str(a, len(a), 1) ≠ ⊖

Полученное противоречие завершает доказательство.

(т.6.7) len(a) ≠ ⊖ ∧ i ≤ len(a) ⇒ len(beg(a, i)) = i ∧ (len(end(a, i)) = len(a) - i +1 ∨ i = 0) 

Доказательство.

Для случая i = 0 очевидно, так как len(beg(a, 0)) = 0 ∧ i = 0.

Поэтому докажем заключение предложения (т.6.7) при дедуктивном предположении:

len(a) ≠ ⊖ ∧ 0 < i ≤ len(a)

Тогда 

str(beg(a, i), i, 1) = str(a, i, 1), из-за (т.6.4)

str(a, i, 1) ≠ ⊖, из-за (т.6.6)

Поэтому

str(beg(a, i), i, 1) ≠ ⊖

С другой стороны:

str(beg(a, i), i ′, 1) = ⊖, из-за (т.4.4) j < k ⇒ str(str(a, i, j), k, 1) = ⊖ при i = 1 и равенстве (т.4.6) str(a, 1, j) = beg(a, j).

Два доказанных утверждения дают в силу определение (6.2) для len(u):

len(beg(a, i)) = i, теорема (т.6.7) доказана для первого члена конъюнкции заключения.

str(end(a, i), len(a) - i +1, 1) = str(a, i + (len(a) - i +1) - 1, 1), из-за (т.6.5).

Поэтому:

str(end(a, i), len(a) - i +1, 1) = str(a, len(a), 1)

str(a, len(a), 1) ≠ ⊖, из-за (т.6.2) len(a) ≠ ⊖ ⇒ … ∧ (len(a) = 0 ∨ str(a, len(a), 1) ≠ ⊖).

Получили:

str(end(a, i), len(a) - i +1, 1) ≠ ⊖

Аналогично:

str(end(a, i), (len(a) - i +1) ′, 1) = str(a, len(a) ′, 1) = ⊖

Два последних утверждения доказывают:

len(end(a, i)) = len(a) - i +1

Теорема (т.6.7) доказана теперь и для второго члена конъюнкции заключения при i ≠ 0.

Поэтому теорема доказана для случаев i = 0 и i ≠ 0. Доказана полностью.

(с.6.7) len(a) ≠ ⊖ ∧ i ≠ 0 ∧ i + j - 1 ≤ len(a) ⇒ len(str(a, i, j)) = j

Доказательство при предположении дедукции len(a) ≠ ⊖ ∧ i ≠ 0 ∧ j ≠ 0 ∧ i + j - 1 ≤ len(a).

Случай 1. j = 0

На основании определения str() имеем:

str(a, i, j) = beg(end(a, i), 0)

На основании аксиомы (2.1)  beg(a, 0) = ⊖ получаем:

str(a, i, j) = ⊖

На основании определения len() и предыдущего равенства получаем:

len(str(a, i, 0)) = 0

То есть, для Случая 1 (j = 0) следствие (с.6.7) доказано:

len(str(a, i, j)) = j

Случай 2. j ≠ 0

На основании предположении дедукции, Случая 2 и теоремы (т.4.2) которая (напоминание):

(i ≠ 0 ∧ j ≠ 0) ⇒ str(a, i, j) = end(beg(a, i+j-1), i)

Получаем:

str(a, i, j) = end(beg(a, i + j - 1), i)

На основании теоремы (т.6.7) которая (напоминание): 

len(a) ≠ ⊖ ∧ i ≤ len(a) ⇒ len(beg(a, i)) = i ∧ (len(end(a, i)) = len(a) - i +1 ∨ i = 0) 

Получаем:

len(beg(a, i + j - 1)) = i + j - 1

Применяя теорему (т.6.7) ещё раз – теперь к beg(a, i + j - 1), получаем:

len(end(beg(a, i+j-1), i)) = len(beg(a, i+j-1)) - i + 1 = (i + j – 1) - i + 1 = j

То есть, для Случая 2 (j ≠ 0) следствие (с.6.7) тоже доказано.

Следствие доказано.

(т.6.8) len(a) = ⊖ ⇒ len(beg(a, i)) = i ∧ (len(end(a, i)) = ⊖ ∨ i = 0) 

Доказательство.

Для случая i = 0 теорема очевидно выполнена. Рассмотрим случай i ≠ 0.

При len(a) = ⊖ все str(a, i, 1) ≠ ⊖ при i ≠ 0.

Поэтому для beg(a, i) в доказательстве ничего не меняется, в сравнении с (т.6.7), поэтому:

len(beg(a, i)) = i

А для end(a, i) все символы оказываются из a, то есть – для любого j ≠ 0 верно:

str(end(a, i), i, 1) ≠ ⊖.

Поэтому, по определению (6.2) для len() получаем:

len(end(a, i)) = ⊖

Теорема доказана.

(т.6.9) len(a) ≠ ⊖ ∧ len(a) < i ⇒ len(beg(a, i)) = len(a) ∧ len(end(a, i)) = 0

Доказательство при дедуктивном предположении len(a) ≠ ⊖ ∧ len(a) < i.

Случай 1. len(a) = 0 

На основании (4.1) которая (напоминание):

str(a, i, j) = beg(end(a, i), j) 

Запишем:

str(beg(a, i), 1, 1) = beg(end(beg(a, i), 1), 1)

На основании (3.4) которая (напоминание):

a = end(a, 0 ′ ) 

убираем end():

str(beg(a, i), 1, 1) = beg(beg(a, 1), 1)

На основании (т.3.1) beg(a, min(i, j)) = beg(beg(a, i), j) получим:

str(beg(a, i), 1, 1) = beg(a, 1)

На основании (т.4.6) str(a, 1, j) = beg(a, j) получим:

str(beg(a, i), 1, 1) = str(a, 1, 1)

Но так как len(a) = 0, то по определению len() имеем:

str(a, 1, 1) = ⊖

Поэтому:

str(beg(a, i), 1, 1) = ⊖

И по определению len() получаем:

len(beg(a, i)) = 0

len(beg(a, i)) = len(a)

Теорема (т.6.9) для beg(a, i) и Случая 1 доказана.

Теперь рассмотрим str(end(a, i), 1, 1), тоже раскрывая str() по определению (4.1):

str(end(a, i), 1, 1) = beg(end(end(a, i), 1), 1)

На основании (3.4) которая (напоминание):

a = end(a, 0 ′ ) 

убираем тот end(), где второй аргумент равен 1:

str(end(a, i), 1, 1) = beg(end(a, i), 1)

На основании (4.1) (см. тут чуть выше) получим:

str(end(a, i), 1, 1) = str(a, i, 1)

Но для рассматриваемого Случая 1 мы уже получили при рассмотрении str(beg(a, i), 1, 1):

str(a, 1, 1) = ⊖

На основании (т.6.1) которая (напоминание):

0 < i ≤ j ⇒ (str(a, i, 1) = ⊖ ⇒ str(a, j, 1) = ⊖)

Получаем:

str(a, i, 1) = ⊖

Поэтому 

str(end(a, i), 1, 1) = ⊖

Из определения для len() из последнего равенства получаем:

len(end(a, i)) = 0

Теорема (т.6.9) для end(a, i) и Случая 1 доказана.

Теорема (т.6.9) для Случая 1 доказана.

Случай 2. len(a) ≠ 0 

Так как из-за (т.4.2) (i ≠ 0 ∧ j ≠ 0) ⇒ str(a, i, j) = end(beg(a, i+j-1), i), то:

str(beg(a, i), len(a), 1) = end(beg(beg(a, i), len(a)), 1)

Так как (т.3.1) beg(a, min(i, j)) = beg(beg(a, i), j), то:

str(beg(a, i), len(a), 1) = end(beg(a, len(a)), 1)

И используя снова (т.4.2), но теперь «в другую сторону», получаем:

str(beg(a, i), len(a), 1) = str(a, len(a), 1)

Аналогично доказывается

str(beg(a, i), len(a) ′, 1) = str(a, len(a) ′, 1)

Так как len(a) ≠ 0, то по определению имеем:

str(a, len(a), 1) ≠ ⊖ 

str(a, len(a) ′, 1) = ⊖ 

Но раз для beg(a, i) выполнены те же 2 соотношения, что для a, то верно:

len(beg(a, i)) = len(a)

Теорема (т.6.9) для beg(a, i) и Случая 2 доказана.

str(end(a, i), 1, 1) = beg(end(a, i), 1)

На основании (4.1) (см. тут чуть выше) получим:

str(end(a, i), 1, 1) = str(a, i, 1)

Но для рассматриваемого Случая 2 мы уже получили при рассмотрении str(beg(a, i), len(a) ′, 1):

str(a, len(a) ′, 1) = ⊖

На основании (т.6.1) которая (напоминание):

0 < i ≤ j ⇒ (str(a, i, 1) = ⊖ ⇒ str(a, j, 1) = ⊖)

Получаем, так как len(a) ′ ≤ i из-за дедуктивного предположения len(a) < i:

str(a, i, 1) = ⊖

Поэтому 

str(end(a, i), 1, 1) = ⊖

Из определения для len() из последнего равенства получаем:

len(end(a, i)) = 0

Теорема (т.6.9) для end(a, i) и Случая 2 доказана.

Теорема (т.6.9) для Случая 2 доказана.

Теорема (т.6.9) доказана.

(с.6.9) len(a)≠⊖ ⇒ len(beg(a, i))=min(i, len(a)) ∧ (len(end(a, i))=max(len(a), i -1) - i +1 ∨ i = 0)

Это следствие очевидно из предыдущих теорем - (т.6.7), которая (напоминание):

len(a) ≠ ⊖ ∧ i ≤ len(a) ⇒ len(beg(a, i)) = i ∧ (len(end(a, i)) = len(a) - i +1 ∨ i = 0) 

И теоремы (т.6.9), которая (напоминание):

len(a) ≠ ⊖ ∧ len(a) < i ⇒ len(beg(a, i)) = len(a) ∧ (len(end(a, i)) = 0)

Как видим из этих теорем: 

Значение len(beg(a, i)) всегда совпадает с тем, что меньше среди двух вариантов: i и len(a). То есть – равно min(i, len(a)).

И

Значение len(end(a, i)) либо 0 при i = 0, либо от len(a) отнимается (i -1), когда есть от чего отнимать (в (т.6.7), i -1 < len(a)), либо от уменьшаемого len(a) ничего не остаётся (в (т.6.9) , len(a) ≤ i -1), когда уменьшаемое меньше вычитаемого. То есть, len(end(a, i)) оказывается равным арифметической разности между len(a) и (i -1). А арифметическая разница записывается, например, формулой max(len(a), i -1) - i +1. 

Следствие доказано.

(7.1) Аксиома о результате конкатенации при конечной 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))

Пояснение.

Аксиома о результате конкатенации для произвольных строк декларирует сохранении прежнего порядка (как в исходных строках) элементов алфавита на своих новых местах в новой строке относительно «соседей». То есть – начало второй «цепочки» символов «цепляется» к концу первой «цепочки» символов, но исходные «цепочки» не разрываются при создании новой строки. 

Аксиома о порядке символов в конкатенации необходима: иначе слияние может быть, например, слиянием 2-х упорядоченных массивов в упорядоченный массив. И все предыдущие аксиомы будут соответствовать такой интерпретации. 

При интерпретации «упорядоченные массивы символов» бесконечный 2-й массив полностью «вытесняет» первый массив при их конкатенации, если символы 2-го упорядоченного массива символов идут раньше в алфавите, чем 1-ого. И все аксиомы для упорядоченных массивов символов при разбиении строк остаются в силе – потому что такое извлечение части из массива упорядоченных символов – тоже даёт упорядоченный массив.

Кстати, видимо, можно включить в рассмотрение и случай бесконечной первой строки в конкатенации:

(7.2) Аксиома о результате конкатенации при бесконечной 1-й строке:

len(a) = ⊖ ⇒ a = a ⋅ b

(м.7.1) Аксиомы (7.1) и (7.2) независимы от предыдущих аксиом, так как случай упорядоченных массивов символов соответствует всем аксиомам перед аксиомами (7.1) и (7.2), но не соответствует аксиомам (7.1) и (7.2).

Данная теорема доказана чуть выше. Разумеется, доказательство метатеорем не может быт формализовано в рамках теории, о которой проведено данное доказательство, так как касается вопросов, выходящих за рамки самой теории, о которой сформулированы метатеоремы.

(т.7.1) len(a_1) ≠ ⊖ ∧ … ∧ len(a_n) ≠ ⊖ ⇒ len(a_1 ⋅ … ⋅ a_n) = len(a_1) + … + len(a_n)

Очевидное следствие для n = 2 из аксиомы конкатенации и определения len(). Доказывается по индукции, так как len(a_1 ⋅ … ⋅ a_{n ‘}) = len((a_1 ⋅ … ⋅ a_n) ⋅ a_{n ‘}), поэтому вопрос для n ‘ сводится к предыдущему n и случаю n = 2.

(т.7.2) i ≤ l_ChrLim ⇒ len(Chr(i)) = 1

Очень удобная теорема вместе с предыдущей – так как не пустая строка равна конкатенации собственных символов. Впрочем, утверждение про «равна конкатенации своих символов» невозможно доказать без теоремы о равенстве строк в следующем разделе.

Но сейчас мы уже можем доказать, что длина конечной строки равна количеству этих символов. Доказательство теоремы (т.7.2) не требует аксиом (7), поэтому её можно было бы доказать перед аксиомой (7.1), но она удобна в связке с предыдущей теоремой (т.7.1), поэтому расположил эти теоремы рядом.

Доказательство при предположении дедукции i ≤ l_ChrLim.

Так как в аксиоме (5.2) есть конъюнктивный член:

∀ i ≤ l_ChrLim: Chr(i) ≠ ⊖ ∧ Chr(i) = str(Chr(i), 1, 1) 

То верно:

str(Chr(i), 1, 1) = Chr(i) ≠ ⊖.

С другой стороны, из-за (т.4.5) которая (напоминание):

1 < k ⇒ str(str(a, i, 1), k, 1) = ⊖

Получим:

str(Chr(i), 2, 1) = str(str(Chr(i), 1, 1), 2, 1) = ⊖

Таким образом у нас выполнено:

str(Chr(i), 1, 1) ≠ ⊖ ∧ str(Chr(i), 2, 1) = ⊖

В соответствии с определением (6.2) для len(a) это соответствует 2-му члену в дизъюнкции этого определения при i=1:

len(a) = i ∧ str(a, i, 1) ≠ ⊖ ∧ str(a, i ′, 1) = ⊖

Поэтому при сделанном дедуктивном предположении i ≤ l_ChrLim верно: 

len(Chr(i)) = 1 

Теорема доказана.

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.