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)) – доказано.
