dmitgu

Category:

2.I. Разбиение строк

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

Аксиома о делении строки на начальную и конечную части в произвольной позиции i:

(1)  a = beg(a, i) ⋅ end(a, i ′ )

Пояснение. Разумеется, если длина строки 6 символов, то деление с 8 позиции приведет к конкатенации исходной строки и пустой строки, обозначаемой значком ⊖:

«строка» = beg(«строка», 8) ⋅ end(«строка», 9) = «строка» ⋅ ⊖ 

Если же то же самое делать с 3 позиции, то получится обычное:

«строка» = beg(«строка», 3) ⋅ end(«строка», 4) = «стр» ⋅ «ока»

Впрочем, всё это будет понятно из дальнейших аксиом.

Кстати, «конкатенация» – это операция соединения строк. В данной аксиоме – соединение «начала» и «конца» строки, разбитой по границе между местом строки i и i ′. Конкатенация в данном цикле статей будет обозначаться значком «⋅» – отняв это обозначение у умножения чисел. Для умножения мы будем использовать значок «×». 

В данной группе аксиом («I. Разбиение строк») мы рассматриваем только соединение частей одной строки между собой. Эти аксиомы не могут решить вопрос о соединении (конкатенации) разных строк между собой – как будет показано в группе аксиом «IV. Соединение строк».

Нумерация символов в строке начинается с 1, чтобы использовать место номер «0» для «технических нужд» - что будет видно в этой и следующих статьях цикла. И длина строки при такой нумерации совпадает с номером последнего символа в ней.

Аксиомы пустых строк:

(2.1)  beg(a, 0) = ⊖ - если пытаемся взять начало до 1-го символа(не включая 1й символ), то получаем пустую строку; 

(2.2)  end(a, 0) = ⊖ - если пытаемся брать окончание строки с позиции перед первой позицией, то ничего не обнаруживаем, потому что перед 1-м местом нет символа, который можно вернуть со всей цепочкой символов после него;

(2.3)  end(beg(a, i), i ′) = ⊖ - если мы взяли в качестве новой строки начало старой строки до i-го символа включительно, то после этого символа в новой строке нет символов.

Альтернативное обозначение: a.beg(i).end(i ′) = ⊖

«Альтернативное обозначение» – из объектно-ориентированного программирования (ООП), когда у объектов есть свойства, а чтобы узнать значение свойства – надо задать после имени объекта через точку имя свойства со списком аргументов. Вот так:

object.property(Arg_1, …, Arg_n)

В данной аксиоме объектом является строка, а свойством – подстрока в начале данной строки. А затем объектом становится полученная строка (подстрока тоже является строкой) и его свойство – подстрока в конце этой строки. А аргумент задаёт границу, до которого нас интересует подстрока в начале, а затем граница, от которой берём подстроку в конце. И результатом тоже является строка, что снова позволяет обратиться к свойству этой новой строки. И так – с любой глубиной композиции свойств. 

Такое обозначение гораздо удобней для композиций глубокой вложенности, чем традиционное. Потому что обычное обозначение приводит к необходимости читать исполнение вложенных функций справа налево, а аргументы – слева направо, при этом разрыв нарастает и всё это – с трудно уловимым вложенным соответствием скобок.

Понимая, что новые обозначения не все быстро осваивают, будем придерживаться в основном традиционного обозначения. Кроме случаев слишком большой вложенности, по крайней мере. 

(2.4)  beg(⊖, x) = ⊖, начало пустой строки – пустая строка, независимо от того, является второй аргумент числом или нет.

(2.5)  end(⊖, x) = ⊖, то же самое можно сказать про конец пустой строки.

(2.6)  i ≠ ⊖, никакое число (включая ноль) не является пустой строкой. Тут выясняется, что в теории строк есть объект (хотя бы один), отличающийся от любого числа.

Аксиомы уменьшения вложенности:

(3.1) beg(a, i) = beg(beg(a, i), i)

Альтернативное обозначение: a.beg(i) = a.beg(i).beg(i)

(3.2) beg(a, i) = beg(beg(a, i), i ′)

Альтернативное обозначение: a.beg(i) = a.beg(i).beg(i ′)

(3.3) beg(a, i) = beg(beg(a, i ′), i)

Альтернативное обозначение: a.beg(i) = a.beg(i ′).beg(i)

Пояснение для аксиом (3.1)-(3.3). Если отбрасывать все символы в строке 2 раза – после i-го и i+1-го символов, то независимо от последовательности этих 2 операций останется только i начальных символов после отбрасывания.

По индукции легко доказать, что

(т.3.1)  beg(a, min(i, j)) = beg(beg(a, i), j)

Альтернативное обозначение: a.beg(min(i, j)) = a.beg(i).beg(j)

Нюанс: «легко доказать» - если использовать обычные правила работы с равенством. Вопрос о равенстве в данном разделе будет обсуждаться особо в подразделе IV.

Основные моменты доказательства (т.3.1) на примере. Из предположения истинности для i < j предложения beg(a, min(i, j)) = beg(beg(a, i), j) получим:

beg(beg(a, i), j ′ ) = beg(beg(beg(a, i), j), j ′ ) = beg(beg(a, i), j) = beg(a, min(i, j)) = beg(a, min(i, j ′ )) 

(3.4) a = end(a, 0 ′ ) 

Пояснение: если брать всю цепочку символов, начиная с 1-го, то получим всю исходную строку.

(3.5) i ≠ 0 ⇒ end(a, i ′ ) = end(end(a, i), 0 ′′ )

Альтернативное обозначение: i ≠ 0 ⇒ a.end(i ′ ) = a.end(i).end(0 ′′ )

Пояснение. Удаление первых i символов в строке – это то же самое, что удалить i-1 первых символов, а затем удалить ещё 1-й символ в оставшейся строке. Отсюда легко доказывается по индукции, как и для (т.3.1) и с той же оговоркой про равенство:

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

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

(т.3.3) i < k ⇒ end(beg(a, i), k) = ⊖

Альтернативное обозначение: i < k ⇒ a.beg(i).end(k) = ⊖

Выводится из (2.3) end(beg(a, i), i ′) = ⊖, (2.5) end(⊖, i) = ⊖ и (3.5)

Доказывается индукцией по k от k = i ′, что совпадает с (2.3). Допустим 

end(beg(a, i), k) = ⊖ и докажем из этого, что end(beg(a, i), k ′) = ⊖.

end(beg(a, i), k ′) = end(end(beg(a, i), k), 0 ′′ ), по (3.5)

end(end(beg(a, i), k), 0 ′′ ) = end(⊖, 0 ′′ ), по предположению индукции

end(⊖, 0 ′′ ) = ⊖, по (2.5). Это завершает доказательство по индукции.

Определение функции str() и аксиома перестановки в композиции beg() с end():

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

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

Пояснение. Это обычная для программирования функция взятие подстроки в строке. В теории оказалось удобнее разбить логику её работы на 2 этапа: удаление начальной части строки до i-1 символа включительно (функция end()) и, затем, удаление в оставшейся части строки всех символов от j+1-го включительно и всех символов после него (функция beg()).

Функция str() чрезвычайно важна для логики строк, так как раскрывает структуру строк до уровня их «атомов» через str(a, i, 1). На любом месте в строке находится либо символ, либо пустая строка. Но сначала нам необходима аксиома, на базе которой выводится способ построения подстроки из её минимальных «атомов». Речь пока не про произвольную строку, а только про результат применения функции str() к произвольной строке.

После аксиом понижения вложенности и следующей аксиомы перестановки можно любую композицию из вложенных функций str() с конкретными числами свести либо к одной функции str(), либо к пустой строке ⊖. 

Если дело сведётся к одной функции str() вместо их композиции, то на месте 2-го и 3-го аргументов этой единственной функции str() будут некие арифметические результаты из всех чисел в исходной композиции. И следующая аксиома перестановки – вместе с изложенными выше аксиомами – делает это возможным: 

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

Альтернативное обозначение: a.beg(i).end(i) = a.end(i).beg(1)

Пояснение. У нас есть 3 способа получить одинаковый результат:

1. Взять в качестве результата то (символ или пустую строку), что находится на i-м месте в исходной строке (способ, производный для данной теории от 2-х следующих); 

2. Удалить все символы после (не включая) i-го символа и затем удалить в оставшейся строке все символы до (не включая) i-го символа;

3. Удалить в исходной строке все символы до (не включая) i-го символа и затем удалить в оставшейся строке все символы после (не включая) 1-го.

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

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

Доказывать будем в виде 

∀ x beg(end(x, i ′ ), j ′) = end(beg(x, i ′ + j), i ′) – квантор общности тут, чтоб подчеркнуть, что доказательство по индукции ведётся для всех строк сразу, а не для некоторой фиксированной строки a. И переменные тут в сравнении с (т.4.1) имеют вид i ′ вместо i и j ′ вместо j. Это сделано для устранения из формулы посылки (i ≠ 0 ∧ j ≠ 0). Потому что любое натуральное число m, не равное нулю, может быть представлено как n ′ для некоторого n. И, обратно, любое число вида n ′ – не равно нулю.

Доказывать будем, отталкиваясь от (4.2)

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

Допустим, у нас доказано «предположение индукции»

∀ x beg(end(x, i ′ ), j ′) = end(beg(x, i ′ + j), i ′), что для j = 0 верно из-за (4.2)

Нам надо доказать

∀ x beg(end(x, i ′ ), j ′′) = end(beg(x, i ′ + j ′), i ′)

То, что у нас квантор общности – подчёркивает, что доказательство идёт сразу для всех строк, потому что в процессе вывода мы будем использовать предположение индукции не только для одной конкретной строки a. Но, фактически, мы будем исходить из «вторичного» предположения индукции: 

beg(end(a, i ′ ), j ′) = end(beg(a, i ′ + j), i ′)

А доказывать будем искомое следствие индукции без квантора общности:

beg(end(a, i ′ ), j ′′) = end(beg(a, i ′ + j ′), i ′)

Обоснованием такого способа действия является аксиома логики (см. раздел 4):

(a) ∀ x A(x, j) ⇒ A(a, j) 

Что позволяет нам перейти от предположения индукции к вторичному предположения индукции.

Точнее, мы воспользуемся этим предположением два раза, и получим результат вида:

∀ x A(x, j) ⇒ A(a, j) ∧ A(b, j)

Затем мы получим искомое следствие без квантора общности, то есть – докажем импликацию вида: 

A(a, j) ∧ A(b, j) ⇒ A(a, j ′)

На основании силлогизма по последним двум импликациям будем иметь:

∀ x A(x, j) ⇒ A(a, j ′)

по правилу вывода логики (см. раздел 4):

(α) Если верно U ⇒ B(a), то верно U ⇒ ∀ x B(x) 

Получим результат вида:

∀ x A(x, j) ⇒ ∀ x A(a, j ′)

И, таким образом, завершим доказательство индукции. Начнём же его:

Для этого надо рассмотреть 2 ветки для 2 сторон данного равенства. Каждая ветка будет построена на основании (1)

a = beg(a, i) ⋅ end(a, i ′ )

1-я ветка: beg(end(a, i ′ ), j ′′) = beg(beg(end(a, i ′ ), j ′′), j ′) ⋅ end(beg(end(a, i ′ ), j ′′), j ′′)

2-я ветка: end(beg(a, i ′ + j ′), i ′) = beg(end(beg(a, i ′ + j ′), i ′), j ′) ⋅ end(end(beg(a, i ′ + j ′), i ′), j ′′)

И теперь надо доказать их равенство на основании предположения индукции. 

1-я ветка 1-й член конкатенации:

beg(beg(end(a, i ′ ), j ′′), j ′) = beg(end(a, i ′ ), j ′), по (3.3)

1-я ветка 2-й член конкатенации:

end(beg(end(a, i ′ ), j ′′), j ′′) = beg(end(end(a, i ′ ), j ′′), 1), по (4.2) для «внешней» композиции

beg(end(end(a, i ′ ), j ′′), 1) = beg(end(a, i ′ + j ′), 1), из (т.3.2) для «внутренней» композиции

2-я ветка 1-й член конкатенации:

beg(end(beg(a, i ′ + j ′), i ′), j ′) = end(beg(beg(a, i ′ + j ′), i ′ + j), i ′), по предположению индукции, где вместо a подставлено beg(a, i ′ + j ′)

end(beg(beg(a, i ′ + j ′), i ′ + j), i ′) = end(beg(a, i ′ + j), i ′), по (3.3) для внутренней композиции

end(beg(a, i ′ + j), i ′) = beg(end(a, i ′ ), j ′), по предположению индукции. 

Совпадение с 1-й веткой 1-м членом конкатенации

2-я ветка 2-й член конкатенации:

end(end(beg(a, i ′ + j ′), i ′), j ′′) = end(beg(a, i ′ + j ′), i ′+ j ′), из (т.3.2) для «внешней» композиции

end(beg(a, i ′ + j ′), i ′+ j ′) = beg(end(a, i ′ + j ′), 1), по (4.2)

Совпадение с 1-й веткой 2-м членом конкатенации

Поскольку в обеих конкатенациях совпали 1-е члены с 1-ми и 2-е со 2-ми, то обе конкатенации одинаковы и доказано beg(end(a, i ′ ), j ′′) = end(beg(a, i ′ + j ′), i ′) на основании индуктивного предположения. Это завершает доказательство по индукции.

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

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

Пояснение. Это та же теорема (т.4.1), переписанная с учётом определения (4.1).

У теоремы (т.4.2) есть практическое значение – если у нас имеется очень длинная (даже бесконечная) строка a, то на практике для получения подстроки str(a, i, j) нужно поступить иначе, чем beg(end(a, i), j). Потому что делать буквально по определению (4.1) – это значит, в промежуточном вычислении end(a, i) создавать значение из «хвоста» значения a от символа i включительно. А «хвост» значения a может быть как угодно велик, и там может быть сколько угодно символов, не нужных для окончательного результата. Поэтому лучше исполнить промежуточное вычисление beg(a, i+j-1), создав значение из «начала» значения a до i+j-1 символа включительно, и лишь затем сформировать результата из «хвоста» этого промежуточного значения. При втором методе «хвост» промежуточного значения целиком попадает в окончательный результат без обработки ненужных символов.

(т.4.3) str(a, i, j ′ ) = str(a, i, j) ⋅ str(a, i + j, 1)

Пояснение. Это простое следствие из анализа доказательства (т.4.1). Конкатенация тут состоит из 1-го и 2-го членов конкатенации ветки 1 (Или ветки 2 – без разницы). 

Теорема (т.4.3) раскрывает нам то, как подстрока «построена» из своих «атомов». Всё начинается с «атома» str(a, i, 1), а дальше «атомы» добавляются к самому концу строки по одному, до j-го «атома» из строки a, если речь у нас о подстроке str(a, i, j)

(т.4.4) j < k ⇒ str(str(a, i, j), k, 1) = ⊖ 

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

Вытекает из (т.3.3) i < k ⇒ end(beg(a, i), k) = ⊖. Действительно:

str(str(a, i, j), k, 1) = beg(end(beg(end(a, i), j), k), 1), по определению для str();

beg(end(beg(end(a, i), j), k), 1) = end(beg(beg(end(a, i), j), k), k), по (4.2) для «внешней» композиции;

end(beg(beg(end(a, i), j), k), k) = end(beg(end(a, i), j), k), из (т.3.1) для «средней» композиции, так как k > j;

end(beg(end(a, i), j), k) = ⊖, из (т.3.3) для «внешней» композиции, так как k > j. Это завершает доказательство.

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

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

Очевидное следствие из (т.4.4), которое показывает, что подстрока, полученная с одного (i-го) места строки, не имеет продолжения со 2-й своей позиции включительно.

Следующие далее теоремы для подстроки str(a, 1, j) будут позже перенесены и на любые конечные строки, потому, что мы докажем, что для конечных строк верно a = str(a, 1, len(a))

(т.4.6) str(a, 1, j) = beg(a, j)

Действительно:

str(a, 1, j) = beg(end(a, 1), j) по определению str(a, 1, j)

beg(end(a, 1), j) = beg(a, j) по (3.4).

(т.4.7) j ≤ k ⇒ str(str(a, 1, j), 1, k) = str(a, 1, j)

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

Очевидное следствие теоремы (т.3.1) beg(a, min(i, j)) = beg(beg(a, i), j) и предыдущей теоремы.

(т.4.8) end(str(a, 1, j), k) = str(str(a, 1, j), k, j), притом вместо одного данного end() может быть композиция из подобных end() сколь угодно большой глубины вложенности.

Альтернативное обозначение: a.str(1, j).end(1, k) = a.str(1, j).str(k, j)

В отношении «сколь угодно большой глубины вложенности» – это очевидно из (т.3.2):

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

Понятно, что для случая равенства 0 второго аргумента в хотя бы одном из end() равенство в (т.4.8) будет выполнено. Так как обе его стороны будут равны ⊖ в силу аксиом пустых строк (2) и определения str(). Если же числовые аргументы не равны 0, то любая вложенность end() сводится к одному end(). Поэтому, если (т.4.8) истинна для одного end(), то если

b = str(str(a, 1, j), k, j)

тогда и дальше можно использовать прежнее число j для дальнейшей замены функции end() на функцию str():

end(b, n) = str(b, n, j)

Поэтому нам достаточно рассмотреть единственную функцию end(), а не их композицию, при этом k ≠ 0 в (т.4.8).

end(str(a, 1, j), k) = end(beg(a, j), k), по (т.4.6) – 1-я ветка для левой части равенства (т.4.8)

Теперь разберём 2-ю ветку для правой части равенства (т.4.8)

str(str(a, 1, j), k, j) = str(beg(a, j), k, j), из (т.4.6)

str(beg(a, j), k, j) = end(beg(beg(a, j), k + j - 1), k), из (т.4.3)

end(beg(beg(a, j), k + j - 1), k) = end(beg(a, j), k), из (т.3.1) и k ≠ 0 

Первая и вторая ветка совпали, поэтому (т.4.8) доказана.

(т.4.9) str(a, 1, j) = str(str(a, 1, j), 1, k) ⋅ str(str(a, 1, j), k ′, j)

Альтернативное обозначение: a.str(1, j) = a.str(1, j).str(1, k) ⋅ a.str(1, j).str(k ′, j)

Действительно:

str(a, 1, j) = beg(str(a, 1, j), k) ⋅ end(str(a, 1, j), k ′ ), по (1)

1-я ветка для 1-го члена конкатенации:

beg(str(a, 1, j), k) = str(str(a, 1, j), 1, k), из (т.4.6)

2-я ветка для 2-го члена конкатенации:

end(str(a, 1, j), k ′ ) = str(str(a, 1, j), k ′, j), из (т.4.8) 

Обе ветки совпали с соответствующими членами конкатенации в (т.4.9). Теорема доказана.

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.