dmitgu

Category:

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

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

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

Для предметных переменных типа строка буду использовать все переменные, кроме i, j, k, l, m, n – которые оставлю для натуральных чисел. Увеличение числа i на 1 буду обозначать так:

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

Теперь запишем аксиомы теории строк.

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

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

Пояснение: строки одинаковы, если на всех одинаковых местах в строках стоят одинаковые символы.

Аксиома о границе слова, если она есть:

str(a, i, 1) = ⊖ ⇒ str(a, i + 1, 1) = ⊖ 

Пояснение: попытка извлечь из строки очередной символ после того, как не удалось извлечь символ с предыдущего места – тоже ничего не даёт. Точнее – даёт пустую строку ⊖.

Аксиома об отсутствии символов нулевой длины:

str(a, i, 0) = ⊖ 

Пояснение: попытка извлечь из строки с произвольного её места подстроку нулевой длины даёт только пустую строку ⊖.

1-я аксиома «рекурсии» для str(): 

∀ a: str(a, 0, 1) = ⊖ ∧ ∀ i ∃ j: str(a, i, 1) = Chr(j)

Пояснение: Место с номером ноль не используется, символы в строке начинаются с места номер 1 (если это не пустая строка, но это видно в других аксиомах). И каждый символ соответствует символу из алфавита или символа вообще нет (пустая строка). «Алфавит или пустая строка» - потому, что функция Chr(j) ничего другого не возвращает. Но это будет в аксиомах ниже.

Можно, конечно, нумеровать символы (символы не равны пустой строке) в строке с 0 места, но ноль удобен для технических нужд, да и ошибок делаешь меньше, когда длина строки равна номеру места её последнего символа (не пустого), поэтому нумерация – с 1.

2-я аксиома «рекурсии» для str() и одновременно – 1-я аксиома конкатенации:

str(a, i, j’) = str(a, i, j) ⋅ str(a, (i + j ’ ), 1)

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

Теперь напишем аксиомы «алфавита». То есть, аксиомы для функции получения символов по их номеру Chr(i) и для функции сравнения символов Comp(). Функция Comp() позволяет, например, перейти к нужной строке программы, но программы в данной статье мы ещё не будем рассматривать. 

В аксиомах ниже используются знаки неравенства, которые, вообще-то, определяются для чисел в арифметике на базе сложения («найдётся дельта, сложение с которым меньшего числа даст большее число» — так словами можно описать про «меньшее» и «большее»). Мы помним, что сложение в арифметике в исходном виде – последовательность увеличений на 1, но определению алфавита с ограниченным числом символов это никак не мешает. А в следующем разделе будет обозначен способ, как определить метод сложения «в столбик».

∃ I_ChrLim:  

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

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

∧ ( ∀ i ≤ I_ChrLim ∀ j ≤ I_ChrLim: (Comp(Chr(i), Chr(j)) = 0 ⇔ i = j)  )

∧ ( ∀ i ≤ I_ChrLim ∀ j ≤ I_ChrLim: (Comp(Chr(i), Chr(j)) = 1 ⇔ i < j)  )

∧ ( ∀ i ≤ I_ChrLim ∀ j ≤ I_ChrLim: (Comp(Chr(i), Chr(j)) = 2 ⇔ i > j)  )

∧ ( ∀ i ≤ I_ChrLim: Chr(i) ≠ ⊖ ∧ Chr(i) = Str(Chr(i), 1, 1) ∧ Str(Chr(i), 2, 1) = ⊖ )

Пояснение: данная аксиома описывает «алфавит», из которого строятся строки. Символы нумеруются от 0 до I_ChrLim включительно. При этом все символы отличаются друг от друга, если их номера отличаются. Речь пока только о номерах, не превышают число I_ChrLim. Функция Comp(Simb_1, Simb_2) сравнивает символы и для одинаковых – возвращает 0. А если номер Simb_1 меньше номера Simb_2, то Comp(Simb_1, Simb_2) = 1, а если наоборот, то Comp(Simb_1, Simb_2) = 2. 

Для всех номеров i > I_ChrLim функция Chr(i) возвращают пустую строку ⊖. Пустая строка – это не символ, у неё даже длина равна 0. У символов длина равна 1. 

Аксиомы для функции Comp() с аргументом/аргументами, равным(и) пустой строке:

Comp(⊖, ⊖) = 0

∀ a ≠ ⊖: Comp(⊖, a) = 1 ∧ Comp(a, ⊖) = 2

Функция Comp() для строк, состоящих из нескольких символов (это избыточные аксиомы, аналог такого расширения функции Comp() можно определить из предыдущих аксиом, но – аксиоматизируем для удобства):

Comp(a ⋅ b, a ⋅ c) = Comp(b, c)

∀ Сhr(i) ≠ ⊖ ∀ Сhr(j) ≠ ⊖: i ≠ j ⇒ Comp(Сhr(i) ⋅ a, Сhr(j) ⋅ b) = Comp(Chr(i), Chr(j))

Пояснение: обычное правило сравнения строк. Если первые символы отличаются, то меньше та строка, чей первый символ стоит в алфавите раньше. Если первые символы равны, то сравниваем вторые символы и т.д. Если все символы совпали – строки равны.

Аксиомы для len(a):

1. len(⊖) = 0

2. ( ∃ i: str(a, i, 1) ≠ ⊖ ∧ str(a, i + 1, 1) = ⊖ ) ⇒ len(a) = i

3. len(a) не определено в ином случае. 

В принципе, функцию len(a) можно определить, а не аксиоматизировать – её результат совпадает с тем наименьшим числом i, для которого верно: str(a, i’, 1) = ⊖. Поэтому при желании можно считать, что тут не аксиомы для len(a), а приведённое определение.

Просто функция len(a) часто используется при работе со строками, поэтому её надо было внести в теорию строк – так или иначе.

В аксиомах (или определении) для len(a) предполагается, что возможны строки, которые имеют начало, но не имеют конца – бесконечная цепочка символов после своего начала. Возможно, это избыточная возможность и нужна аксиома о конечности произвольной строки:

∀ a ∃ i: str(a, i, 1) = ⊖

Тогда среди аксиом для функции len(a) пункт 3 не нужен, а в следующей аксиоме конкатенации посылка импликации выполнена, и тоже не нужна.

2-я Аксиома конкатенации:

(∃ i: str(a, i, 1) = ⊖ ) ⇒

( ∃ c = a ⋅ b )

∧ ( i ≤ len(a) ⇒ str(c, i, 1) = str(a, i, 1) )

∧ ( i > len(a) ⇒ str(c, i, 1) = str(b, i - len(a), 1) )

Пояснение: при соединении двух строк длина полученной строки равна сумме длин 2-х соединённых строк. При этом первые символы полученной строки совпадают с символами первой строки, а после них идут такие же символы, как во второй строке.

3-я Аксиома конкатенации:

a = str(b, 1, i) ⇒ ∃ c (b = a ⋅ c)

Пояснение: Строки бывают и бесконечные в данной версии теории строк. Поэтому нужна аксиома, которая гарантировала бы, что если у данной строки b (возможно, бесконечной) имеется начало, равное строке a, то и продолжение строки b (после начала, совпадающего со строкой a) – тоже строка (некоторая строка c). Поэтому строка b может быть представлена как конкатенация этих строк a ⋅ c.

Заметим, что раз соответствующая строка c существует, то она – единственная для данной строки b и числа i. Потому, что любая другая строка d, удовлетворяющая данной аксиоме, будет равна строке c на основании аксиомы равенства – все символы после (не включая) символа на месте i в строке b совпадают как с символами строки c, так и с символами строки d.

А для такого значения, которое «существуют и притом единственное» всегда можно вводить новую функциональную букву – см. например Э. Мендельсон – «Введение в математическую логику», Глава 2. Теории первого порядка. Раздел 9. Введение новых функциональных букв и предметных констант. Предложение 2.29.

В соответствии с данным Предложением 2.29 введение такой функциональной буквы не добавляет никакой новой логики (помимо нового обозначения) в теорию. И то, что можно доказать с новым определением (аксиомой) – можно доказать (в эквивалентной форме) и в исходной теории. Поэтому введём новую функциональную букву right(b, i) посредством определения (аксиомы для данного обозначения):

( a = str(b, 1, i) ⇒ b = a ⋅ right(b, i ′ ) ) ∧ right(b, 0) = ⊖ 

Пояснение: второй аргумент в функции right(b, i ′ ) – это номер того символа, который из строки b попадает на первое место в строку right(b, i ′ ). Именно поэтому он на 1 больше, чем номер последнего символа (i), который попал из переменной b в переменную a. 

Случай, когда 2-й аргумент равен 0 (нулю) в функции right(…) – добавлен дополнительно, чтобы сделать работу функции совпадающей с работой str(…) при данном значении 2-го аргумента.

Заметим, что данное определение не является конструктивным в общем случае. Потому что мы не можем получить «бесконечную подстроку» в реальности. Но эта функциональная буква будет играть важную роль в третьей статье данного цикла при доказательстве «полиномиальной представимости» алгоритмов в теории строк. А для конечных строк легко доказывается следующее равенство:

right(b, i) = str(b, i, len(b))

Аксиома для поиска и его однозначности (найденная строка what оказывается самой близкой к началу исследуемой строки in, среди всех возможных вариантов совпадения строки what с некой подстрокой в строке in, начиная с позиции j+1):

find(in, what, j) = i ∧ i ≠ 0 ⇔ 

str(in, i, len(what)) = what 

∧ ∀ a ( (a ⋅ what = str(in, 1, len(a ⋅ what)) ∧ len(a)+1 ≠ i) ⇒ (len(a)<j ∨ len(a)+1>i)  )

Пояснение: если в строке in пропустить j первых символов и искать дальше подстроку what, то если найдёшь – она будет самой первой – после пропущенных j символов – из равных ей (если они есть) в строке in. А именно, начало любой такой же подстроки в строке in (такой же в той же строке – a ⋅ what = str(in, 1, len(a ⋅ what) то есть), но в другом месте ( len(a)+1 ≠ i – то есть) будет либо среди пропущенных j первых символов (len(a) < j), либо после начала найденной подстроки (len(a)+1 > i). 

Случай равенства нулю – отдельно, потому что кроме нуля у нас иначе могла бы быть и какая-то строка, которая не является числом:

find(in, what, j) = 0 ⇔ ∀ a ( a ⋅ what = str(in, 1, len(a ⋅ what)) ⇒ len(a) < j  )

Последние две аксиомы для функции find(in, what, j) тоже является избыточными. Функцию поиска можно определить как алгоритм сравнения строк str(in, i, len(a)) для разных i > j со строкой what. Как только равенство будет обнаружено (если оно может быть обнаружено), так нужное i будет результатом поиска. Иначе результатом будет 0. 

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.