dmitgu

Category:

2. Теория строк

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

0. Общая информация и свод результатов

Математики называют объекты теории алгоритмов термином «слово», программисты используют для того же термин «строка». Далее буду использовать термин программистов, потому что аксиомы построены именно в соответствии с общеизвестной практикой программирования.

Для предметных переменных типа строка буду использовать все переменные, кроме i, j, k, l, m, n – которые оставим для натуральных чисел. И кроме переменной q, которую оставим для числовых значений и пустой строки ⊖. Впрочем, натуральные числа тоже являются строками особого вида, и форма представления чисел внутри теории строк будет рассмотрена в разделе 3. Но обратное (что всякая строка является числом) не верно. 

Увеличение числа i на 1 буду обозначать так:

i ′ – такое обозначение увеличения числа на 1 является аксиоматизированной операцией в арифметике (и в её кратком варианте в виде теории Пеано), поэтому сохраним тут это стандартное обозначение.

Кроме того, вместо специального обозначения для арифметического вычитания от числа i числа j (результат которого равен i - j, когда i > j, и нулю в противном случае) буду использовать обозначение:

max(i, j) - j

Результат приведенной формулы совпадает с результатом арифметического вычитания и более привычен людям, особенно если они программисты, например.

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

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

Сразу дам сводку всех результатов данного раздела в данном его подразделе. Это удобно для того, чтобы проверять доказательства – сразу видеть все предыдущие утверждения теории, на которые опираются доказательства. Разумеется, не все смотрят доказательства – тогда им вполне хватит этого подраздела вместо того, чтобы читать все остальные подразделы данного раздела.

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

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

Итак, ключевые результаты построения теории строк – кроме аксиом арифметики и аксиомы индукции, расширенной на формулы теории строк, следующие:

Аксиомы, определения и метатеоремы (теоремы о теории)

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

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

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

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

(2.1)  beg(a, 0) = ⊖ 

(2.2)  end(a, 0) = ⊖

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

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

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

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

(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.4) a = end(a, 0 ′ ) 

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

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

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

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

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

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

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

II. Алфавит строк

Аксиомы об «атомах», из которых образованы строки:

(5.1) ∀ a ∀ i ∃ j str(a, i, 1) = Chr(j) 

(5.2) Аксиома об «алфавите»:

( ∀ i > l_ChrLim: Chr(i) = ⊖ ) 

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

∧ ( ∀ i ≤ l_ChrLim ∀ j ≤ l_ChrLim: Chr(i) = Chr(j) ⇒ i = j )

(м.5.1) Аксиома алфавита (5.2) независима от предыдущих аксиом, так как массивы произвольных натуральных чисел удовлетворяют предыдущим аксиомам, но не удовлетворяют аксиоме (5.2).

(5.3) Определение функции Ach(u), обратной к функции Chr(i):

( Ach(u) = l_ChrLim ′ ∧ u = ⊖ ) 

∨ ( Ach(u) = i ∧ u ≠ ⊖ ∧ Chr(i) = u ) 

∨ ( Ach(u) = ⊖ ∧ ∀ i Chr(i) ≠ u )

(5.4) Определение функции Comp(Chr(i), Chr(j)), сравнивающей произвольные элементы алфавита Chr(i) и Chr(j)):

( Comp(Chr(i), Chr(j)) = 0 ∧ i > l_ChrLim ∧ j > l_ChrLim )

∨ ( Comp(Chr(i), Chr(j)) = 0 ∧ i ≤ l_ChrLim ∧ j ≤ l_ChrLim ∧ i=j )

∨ ( Comp(Chr(i), Chr(j)) = 1 ∧ i ≤ l_ChrLim ∧ j ≤ l_ChrLim ∧ i < j) )

∨ ( Comp(Chr(i), Chr(j)) = 1 ∧ i > l_ChrLim ∧ j ≤ l_ChrLim )

∨ ( Comp(Chr(i), Chr(j)) = 2 ∧ i ≤ l_ChrLim ∧ j ≤ l_ChrLim ∧ i > j )

∨ ( Comp(Chr(i), Chr(j)) = 2 ∧ i ≤ l_ChrLim ∧ j > l_ChrLim )

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

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

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

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

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

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

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

∨ ( len(u) = ⊖ ∧ ∀ i str(u, 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))

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

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

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

IV. Равенство строк

Аксиома о равенстве строк:

(8.1) a = b ⇔ ∀ i str(a, i, 1) = str(b, i, 1)

(м.8.1) Аксиома (8.1) независима от предыдущих аксиом, так как есть пример из ООП (объектно-ориентированного программирования), когда функции beg() и end() создают «детей» у «независимых» строк. И между «независимыми» строками и «детьми» есть разница помимо последовательности символов. Такие объекты ООП соответствуют всем аксиомам перед аксиомой (8.1), но не соответствует аксиоме (8.1).

(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)

(8.4) (i = j) ⇒ Chr(i) = Chr(j)

(8.5) x = x

(8.6) x = y ⇒ (z = x ⇒ z = y)

V. Сравнение, поиск, вставка

(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 )

(9.2) Определение для Comp(a, b):

Comp(a, b) = Comp(str(a, CompIn(a, b), 1), str(b, CompIn(a, b), 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) )

(9.4) Определение для find(in, what, i):

find(in, what, i) = find(end(in, i ′ ), what, 0)

(9.5) Определение для if_0(a, b, c):

(if_0(a, b, c) = b ∧ a = 0) ∨ (if_0(a, b, c) = c ∧ a ≠ 0)

(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.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)) )

(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.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.

VI. Алгоритмы, не сводимые к (частично) рекурсивным функциям и арифметике

(м.9.1) В теории строк с односимвольным алфавитом (l_ChrLim = 0) невозможно в общем случае представить работу алгоритмов со строками многосимвольного алфавита таким образом, чтобы размер логического вывода для результата работы такого алгоритма был в полиномиальных (или любых иных) пределах относительно времени работы этого алгоритма.

(м.9.2) В арифметике невозможно в общем случае представить работу алгоритмов со строками многосимвольного алфавита таким образом, чтобы размер логического вывода для результата работы такого алгоритма был в полиномиальных (или любых иных) пределах относительно времени работы этого алгоритма.

Теоремы, леммы и следствия

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

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

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

(т.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) = ⊖

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

(т.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)

(т.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.3) str(a, i, j ′ ) = str(a, i, j) ⋅ str(a, i + j, 1)

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

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

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

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

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

(т.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)

(т.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)

(т.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)

II. Алфавит строк

(т.5.1) Ach(Chr(i)) = min(i, l_ChrLim ′) 

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

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

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

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

(т.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)

(т.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)

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

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

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

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

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

(с.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)

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

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

IV. Равенство строк

Ассоциативность конкатенации:

(т.8.1) (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)

(т.8.2) len(a) ≠ ⊖ ⇒ a = str(a, 1, len(a)), в силу чего в отношении конечной строки a, в виде str(a, 1, len(a)), можно применять теоремы (т.4.4) и от (т.4.6) до (т.4.9) включительно

(с.8.2) len(a) ≠ ⊖ ⇒ (len(a) ≤ i ⇒ a = str(a, 1, i))

(т.8.3) a = a ⋅ ⊖ = ⊖ ⋅ a

(т.8.4) a = b ⇔ ∀ i (0 < i ⇒ str(a, i, 1) = str(b, i, 1))

(т.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.6) len(a) ≠ ⊖ ⇒ a = beg(a ⋅ u, len(a))

(т.8.7) len(a) ≠ ⊖ ⇒ u = end(a ⋅ u, len(a) ′ )

(т.8.8) a = ⊖ ⇔ len(a) = 0

(с.8.8) len(a) = ⊖ ⇔ len(len(a)) = 0

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)))

Лемма об эквивалентном добавлении дизъюнктивных членов:

(л.9.2) A ⇒ ( (A ⇒ ¬ C) ⇒ (B ⇔ (B ∨ C)) ) 

(с.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) соответственно.

Критерий локального сравнения данных:

(с.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) соответственно.

(л.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))

(л.9.4) a ≠ a ⋅ Chr(0) ⇔ len(a) ≠ ⊖

VII. Критерий локального изменения данных

(т.9.1) len(a) ≠ ⊖ ∧ len(b) ≠ ⊖ ⇒ str(a ⋅ b ⋅ u, len(a) ′, len(b)) = b

(т.9.2) len(a) ≠ ⊖ ∧ len(b) ≠ ⊖ ⇒ end(a ⋅ b ⋅ u, len(a) ′) = b ⋅ u

(т.9.3) IsIns(len(a), i, len(b)) = 1 ⇒ len(Ins(a, i, b)) = len(a) 

(т.9.4) Критерий локальной вставки:

(len(a) ≠ ⊖ ∧ len(b) ≠ ⊖) ⇒ 

( IsIns(len(a), i, len(b)) = 1 ⇔ ∀ u Ins(a ⋅ u, i, b) = Ins(a, i, b) ⋅ u )

VIII. Критерий локального извлечения данных

(т.9.5) len(a) ≠ ⊖ ⇒ ( IsStr(len(a), i, j) = 1 ⇔ ∀ u str(a ⋅ u, i, j) = str(a, i, j) ) 

Теперь будем записывать аксиомы и определения теории строк, разбирать их семантику и доказывать теоремы.

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.