dmitgu

Category:

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

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

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

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

Пояснение. У нас есть «алфавит» (в следующей аксиоме (5.2)) и на произвольном месте i в произвольной строке a находится некоторый вариант значения (из конечного набора значений) этого алфавита. И рассматриваем мы при этом только одну позицию в строке, поэтому третий аргумент в функции str(a, i, 1) равен 1. 

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

Пояснение: 

Данная аксиома описывает «алфавит», из символов и пустой строки, из которого строятся строки. Символы нумеруются от 0 до l_ChrLim включительно, а пустая строка соответствует любому номеру, большему, чем l_ChrLim. Будем называть «элементом алфавита» как любой символ, так и пустую строку. Символом будем называть любой элемент алфавита, отличный от пустой строки.

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

smb, smb_1, smb_2, … для переменных, имеющих в качестве своего значения символ;

abc, abc_1, abc_2, … для переменных, имеющих в качестве своего значения элемент алфавита.

Теперь разберём аксиому (5.2).

Если число i больше, чем l_ChrLim то функция Chr(i) возвращает пустую строку:

∀ i > l_ChrLim: Chr(i) = ⊖ 

Как мы увидим ниже, у пустой строки даже длина равна 0, а у символа длина равна 1 в теории строк. Но из всех аксиом выше, включая аксиому алфавита, такой вывод получить невозможно, как будет показано далее.

Если же число i не превышает l_ChrLim, то результат функция Chr(i) – символ. При этом символ по свойствам совпадает со своей собственной подстрокой из единственной первой позиции:

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

Кстати, пустая строка тоже равна подстроке из своей первой позиции – но это можно вывести из аксиом (2.2), (2.4) и определения (4.1) для str().

При этом все символы отличаются друг от друга, если их номера отличаются: 

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

Данная аксиома вводит предметную константу – некоторое число l_ChrLim. Первоначально я записывал аксиому с квантором существования по l_ChrLim, но, по сути, l_ChrLim может быть любым натуральным числом (даже нулём), чтобы в алфавите был хотя бы один символ, отличный от пустой строки. 

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

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

Поэтому сформулируем метатеорему – то есть, теорему о теории:

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

Функция Ach(u) не «идеально» обратная к функции Chr(i) – для пустой строки она возвращает минимально возможный номер i, при котором Chr(i) = ⊖. Для символа же (то есть – не пустой строки) номер вполне однозначный в силу 

( ∀ i ≤ l_ChrLim ∀ j ≤ l_ChrLim: Chr(i) = Chr(j) ⇒ i = j ), из (5.2)

Поэтому легко доказать, что 

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

Кроме того, если аргумент u в Ach(u) не является элементом алфавита, то Ach(u) = ⊖. 

Формула (5.3) является определением – то есть, в (5.3) аксиоматизируется лишь обозначение, но никакой дополнительной логики в теории данная формула не создаёт. 

Это следует из метода «введения новых функциональных букв и предметных констант». Подробнее смотри раздел 4, пункт VI.5 данной статьи, там имеется и ссылка на источник.

В частности, данное определение опирается на теорему:

∃_1 q ( ( q = l_ChrLim ′ ∧ u = ⊖ ) ∨ ( q = i ∧ u ≠ ⊖ ∧ Chr(i) = u) ∨ ( q = ⊖ ∧ ∀ i Chr(i) ≠ u ) )

Её доказательство и является обоснованием того, что (5.3) является всего лишь определением. И данное доказательство нужно «всего лишь» для того, чтобы не вводить аксиому для равенства, применительно к функции Ach(u). Потому что раз функция не имеет дополнительной относительно остальных аксиом логики, то аксиомы равенства будут для неё автоматически выполнены, раз они выполнены для теории, в которой она определена. 

Доказательство данной теоремы о существовании и единственности интересно только с точки зрения минимизации количества исходных утверждений теории – её аксиом. В противном случае достаточно просто дописать ещё одну аксиому равенства – пусть она и избыточна, но никакого противоречия в этом нет. Кому же доказательство всё же интересно, то вот какая у него примерная схема:

Дадим обозначение C(q, u) для формулы:

( q = l_ChrLim ′ ∧ u = ⊖ ) ∨ ( q = i ∧ u ≠ ⊖ ∧ Chr(i) = u) ∨ ( q = ⊖ ∧ ∀ j Chr(j) ≠ u )

Сначала докажем существование q для произвольного u.

Допустим, истинно u = ⊖, тогда истинно

C(l_ChrLim ′, u) 

Это очевидно по первому члену дизъюнкции в C(l_ChrLim ′, u).

На основании теоремы дедукции делаем вывод об истинности импликации

u = ⊖ ⇒ C(l_ChrLim ′, u)

По аксиоме логики (см. Раздел 4. Приложение):

(b) A(a) ⇒ ∃ x A(x)

Получаем

C(l_ChrLim ′, u) ⇒ ∃ q C(q, u)

По правилу силлогизма из последней формулы и предыдущей u = ⊖ ⇒ C(l_ChrLim ′, u) имеем:

u = ⊖ ⇒ ∃ q C(q, u)

Аналогичным образом доказываем ещё 2 формулы:

(u ≠ ⊖ ∧ Chr(i) = u) ⇒ ∃ q C(q, u)

( ∀ j Chr(j) ≠ u ) ⇒ ∃ q C(q, u)

Из предпоследней формулы на основании правила вывода логики (см. Раздел 4. Приложение):

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

получим: 

(∃ j (u ≠ ⊖ ∧ Chr(j) = u)) ⇒ ∃ q C(q, u)

Перепишем в эквивалентном виде (эквивалентность – см. Раздел 4. Приложение, в VI.8 поменять стороны в эквивалентности на их отрицания и применить VI.7):

(u ≠ ⊖ ∧ ∃ j Chr(j) = u) ⇒ ∃ q C(q, u)

Теперь у нас доказаны 3 формулы:

u = ⊖ ⇒ ∃ q C(q, u) 

(u ≠ ⊖ ∧ ∃ j Chr(j) = u) ⇒ ∃ q C(q, u) 

( ∀ j Chr(j) ≠ u ) ⇒ ∃ q C(q, u) 

Из этих трёх формул и аксиомы (см. Раздел 4. Приложение)

III.3) (A ⇒ C) ⇒ ((B ⇒ C) ⇒ (A ∨ B ⇒ C)) 

Применив её 2 раза, получим:

( (u = ⊖) ∨ (u ≠ ⊖ ∧ ∃ j Chr(j) = u) ∨ ( ∀ j Chr(j) ≠ u ) ) ⇒ ∃ q C(q, u) 

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

Насчёт истинной посылки обоснование такое –

Раскроем по закону дистрибутивности часть дизъюнкции

(u = ⊖) ∨ (u ≠ ⊖ ∧ ∃ j Chr(j) = u) 

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

(u = ⊖ ∨ u ≠ ⊖) ∧ (u = ⊖ ∨ ∃ j Chr(j) = u)

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

(u = ⊖ ∨ ∃ j Chr(j) = u)

Так как верно

u = ⊖ ⇒ ∃ j Chr(j) = u, по аксиоме (5.1) ∀ a ∀ i ∃ j str(a, i, 1) = Chr(j) при i=0, то предыдущая дизъюнкция может быть переписана в эквивалентном виде:

∃ j Chr(j) = u 

Теперь вся посылка

( (u = ⊖) ∨ (u ≠ ⊖ ∧ ∃ j Chr(j) = u) ∨ ( ∀ j Chr(j) ≠ u ) ) 

Приобрела вид:

(∃ j Chr(j) = u) ∨ (∀ j Chr(j) ≠ u) 

Истинность последнего утверждения очевидна и легко выводится. Поэтому мы её сокращаем по правилу MP и существование ∃ q C(q, u) доказано.

Теперь надо доказать единственность, то есть, надо доказать, что

C(q_1, u) ∧ C(q_2, u) ⇒ q_1 = q_2 

Доказывать будем аналогично тому, как для существования – перебирая возможные посылки. Начнём с u = ⊖ 

Так как все члены дизъюнкции в C(q_1, ⊖) ложные, кроме первой, то верно:

q_1 = l_ChrLim ′ ∧ u = ⊖ 

Отсюда:

q_1 = l_ChrLim ′

Аналогично:

q_2 = l_ChrLim ′

Из этих 2-х равенств получаем:

q_1 = q_2

Поэтому по теореме дедукции имеем:

u = ⊖ ⇒ ( C(q_1, u) ∧ C(q_2, u) ⇒ q_1 = q_2 )

Перебрав оставшиеся 2 посылки и соединив их дизъюнкцией в единую истинную посылку по аналогии с доказательством существования, сократим эту истинную посылку и получим:

C(q_1, u) ∧ C(q_2, u) ⇒ q_1 = q_2.

Единственность тоже доказана. Поэтому (5.3) является определением функции Ach(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 )

Функция Comp(abc_1, abc_2) здесь сравнивает между собой символы/пустые строки, которые представлены в 1-м и 2-м аргументах. И для одинаковых – возвращает 0. А для разных возвращает 1, когда значение 1-го аргумента меньше второго из-за его меньшего номера в алфавите, либо того, что в первом аргументе – пустая строка, в отличие от второго аргумента. В остальных случаях (2ой аргумент «меньше» 1-го) функция возвращает 2. 

Заметим, что функция определена пока только для элементов алфавита, а не для произвольных строк, как Ach(u). Дело в том, что для произвольных строк функция Comp(a, b) будет доопределена после формулировки аксиомы равенства для строк. 

Пока же, как видно из (5.4), формула строится даже не на элементах алфавита, а на числах. И ещё желательно доказать корректность такого построения. Ведь даже сама формулировка Comp(Chr(i), Chr(j)) – это композиция функций, «на входе» которой два числа i, j и результат – тоже число. Но вопрос, разве функция Chr(i) никогда не уничтожает какие-то необходимые для работы функции Comp(Chr(i), Chr(j)) подробности о числе i?

Перечислим детали определения.

Если оба аргумента являются пустыми строками – то функция равна 0. А если оба аргумента – символы (не пустые строки) и при этом имеют один номер в алфавите – то функция тоже возвращает 0: 

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

Если аргументы являются символами и номер первого символа в алфавите меньше номера второго, то функция возвращает 1. Если же значением первого аргумента является пустая строка, а значением второго является символ (не пустая строка), то функция тоже возвращает 1: 

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

Если аргументы являются символами и номер первого символа в алфавите больше номера второго, то функция возвращает 2. Если же значением первого аргумента является символом, а значением второго является пустая строка, то функция тоже возвращает 2: 

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

Для тех, кому интересна минимизация количества аксиом равенства, приведу схему доказательства того, что (5.4) является определением для Comp(Chr(i), Chr(j)).

Докажем это в два этапа. 

Первый этап – доказательство 

∃_1 n C(n, i, j)

где C(n, i, j) служит обозначением для формулы

( n = 0 ∧ i > l_ChrLim ∧ j > l_ChrLim ) 

∨ ( n = 0 ∧ i ≤ l_ChrLim ∧ j ≤ l_ChrLim ∧ i=j )

∨ ( n = 1 ∧ i ≤ l_ChrLim ∧ j ≤ l_ChrLim ∧ i < j) )

∨ ( n = 1 ∧ i > l_ChrLim ∧ j ≤ l_ChrLim )

∨ ( n = 2 ∧ i ≤ l_ChrLim ∧ j ≤ l_ChrLim ∧ i > j )

∨ ( n = 2 ∧ i ≤ l_ChrLim ∧ j > l_ChrLim )

Доказательство существования и единственности для n тут проводится аналогично со случаем (5.3). Только вариантов посылок тут будет шесть, а не три. Но очевидно, что они охватят все варианты возможных значений для i, j и дизъюнкция посылок в итоге станет истинной и будет отброшена по правилу вывода MP как при доказательстве существования, так и при доказательстве единственности. Поэтому

∃_1 n C(n, i, j) доказано.

Второй этап – перейти от чисел к элементам алфавита. 

Можно вывести в рамках арифметики и достаточно очевидно, что:

C(u, i, j) ⇔ C(u, min(i, l_ChrLim ′ ), min(j, l_ChrLim ′ ) ) 

Доказывается данная эквивалентность на основе эквивалентности каждого члена дизъюнкции в C(u, i, j) и C(u, min(i, l_ChrLim ′ ), min(j, l_ChrLim ′ ) ) соответственно.

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

min(i, l_ChrLim ′ ) = Ach(Chr(i)), из-за (т.5.1)

Таким образом:

C(u, i, j) ⇔ C(u, Ach(Chr(i)), Ach(Chr(j)))

Поэтому:

C(u, i, j) ⇔ C(u, Ach(abc_1), Ach(abc_2))

Мы построили формулу, эквивалентную C(u, i, j) для которой в силу эквивалентности выполнено:

∃_1 n C(u, Ach(abc_1), Ach(abc_2))

И эта формула представляет собой основу для определения (5.4), так как зависит уже от элементов алфавита, а не от их номеров. Поэтому то, что (5.4) является определением для Comp(Chr(i), Chr(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.