3. Числа в теории строк
. К оглавлению . Показать весь текст .
То, что в теории строк мы опираемся в «конструировании» объектов не только на ноль, создаёт свойства для строк сверх тех свойств, которые есть у чисел в теории Пеано. У строк теперь есть собственная структура «цепочка символов». Вопрос - как эту же структуру придать числам, которые используются в теории строк? Это будет та структура, которой нет у чисел арифметики (арифметики Пеано, в частности), но есть у чисел в позиционном представлении.
Что касается чисел, которые использованы в аксиомах теории строк, то они подчиняются обычным свойствам арифметики, и тут мы имеем (в неявном виде пока) ещё аксиомы теории Пеано или её арифметического расширения. Запишем явным образом аксиомы теории Q, достаточной для представления рекурсивных функций, а затем и её расширение до теории Пеано.
Дж. Булос, P. Джеффри «Вычислимость и логика» Глава 14. Представимость в Q. Аксиомы теории Q.
(Q_1) ∀ i ∀ j (i ′ = j ′ ⇒ i = j)
(Q_2) ∀ i 0 ≠ i ′
(Q_3) ∀ i ( i ≠ 0 ⇒ ∃ j i = j ′ )
(Q_4) ∀ i i + 0 = i
(Q_5) ∀ i ∀ j ( i + j ′= (i + j) ′ )
(Q_6) ∀ i i × 0 = 0
(Q_7) ∀ i ∀ j ( i × (j ′ ) = (i × j) + i )
Замечу, что для знака умножения использован символ «×», потому что символ «⋅» уже занят для обозначения конкатенации.
Глава 15 Неразрешимость, неопределимость и полнота. В той же книге. Добавление аксиом индукции к теории Q и переход к теории Пеано - «теории Z».
( ( A(0) ∧ ∀ i (A(i) ⇒ A(i ′ )) ) ⇒ ∀ i (A(i)) ) - все формулы такого вида на языке теории строк, но с навешиванием на такие формулы квантора общности ∀ i.
Разумеется, для теории строк формула A(i) понимается как формула, которая может зависеть и от разных строковых аргументов, которые не являются числами.
При этом аксиому Q_3 можно исключить, так как она выводится из аксиомы индукции и аксиомы Q_2.
До данного момента мы разделяли между собой просто строки и строки, которые являются ещё и числами. Вот аксиомы Пеано - это аксиомы, которые выполнены для не просто строк, но для строк со свойствами чисел. Теперь, сохраняя те же условности обозначения для строк, имеющих свойства чисел (для переменных со значением числа мы используем оговоренные ранее буквы) зададим связь между алфавитом для строк и числами.
Чтобы придать числам свойства строк, достаточно задать строку, которая будет 0 (нулём) и задать операцию добавления единицы (функцию следования). После этого остальные арифметические операции легко выводятся на основании свойств строк и аксиом арифметики Пеано.
Вот нужная для «превращения» некоторых строк ещё и в числа аксиома, которую можно при желании разбить на отдельные аксиомы - отдельная аксиома из каждого члена следующей конъюнкции:
( 0 ≤ l_NumBeg < l_NumLim ≤ l_ChrLim )
∧ 0 = Chr(l_NumBeg)
∧ ( l_NumBeg ≤ j < l_NumLim ⇒ (Chr(j)) ′ = Chr(j ′ ) )
∧ Chr(l_NumLim) ′ = (Chr(l_NumBeg) ′ ) ⋅ Chr(l_NumBeg)
∧ ( (k ≠ 0 ∧ l_NumBeg ≤ j < l_NumLim) ⇒ (k ⋅ Chr(j)) ′ = k ⋅ Chr(j ′ ) )
∧ ( k ≠ 0 ⇒ (k ⋅ Chr(l_NumLim)) ′ = (k ' ) ⋅ Chr(l_NumBeg) )
Пояснения:
1. Мы задаём «алфавит в алфавите» - для цифр.
2. Первая цифра в этом алфавите - символ «0». Вот его мы и объявляем числом 0 (ноль) в этой части из приведённой аксиомы:
0 = Chr(l_NumBeg)
Дальше идёт логика добавления 1 в разных случаях.
3. Сначала рассматриваем случай, когда у нас число состоит из любой цифры, кроме последней цифры «алфавита цифр»:
l_NumBeg ≤ j < l_NumLim ⇒ (Chr(j)) ′ = Chr(j ′ )
При увеличении такого числа на 1 происходит просто замена прежней цифры на следующую. Например, для десятичной системы:
5 ′ = 6 или 5 + 1 = 6
4. Затем рассматриваем случай, когда у нас число состоит из последней цифры «алфавита цифр». В десятичной системе это - 9:
Chr(l_NumLim) ′ = (Chr(l_NumBeg) ′ ) ⋅ Chr(l_NumBeg)
На примере 9 это правило выглядит так:
9 ′ = 10 или 9 + 1 = 10
Заметим, что тут мы используем строковую операцию конкатенации, соединяя в правой части равенства следующую цифру после 0 (так как 1 = 0 ′ ) и сам 0, который возник вместо 9.
5. Затем рассматриваем случай, когда последняя цифра - не 9 (если разбирать на примере десятичной системы) и она не единственная в числе (усложнение пункта 3). Тогда последняя цифра просто заменяется на следующую в алфавите цифру, когда число увеличено на 1:
23345 ′ = 23346
В данном примере k = «2334» и он соединён (конкатенация) с цифрой «5». Условие
k ≠ 0
понятно, потому что числа у нас не имеют вида «05», например. Поэтому разбираемая часть аксиомы имеет вид:
(k ≠ 0 ∧ l_NumBeg ≤ j < l_NumLim) ⇒ (k ⋅ Chr(j)) ′ = k ⋅ Chr(j ′ )
6. И в заключение рассматриваем случай, когда последняя цифра в числе является последней цифрой ещё и в алфавите цифр:
( k ≠ 0 ⇒ (k ⋅ Chr(l_NumLim)) ′ = (k ' ) ⋅ Chr(l_NumBeg) )
Тогда последняя цифра заменяется на 0 (ноль), а вся предыдущая часть числа заменяется на число, которое больше этой предыдущей части на 1. На примере десятичного числа:
123799 ′ = 123800
Видно, что число у нас из двух соединённых строк - «12379» и «9». При увеличении такого числа на 1 получается соединение из 2 новых строк - «12380» и «0».
Этой аксиоматизации достаточно для задания всех чисел - от 0 и до бесконечности. Из этой аксиомы и остальных аксиом для строк и арифметики можно уже вывести правила сложения, умножения, вычитания и деления «в столбик» и любые другие правила для операций с числами в позиционном представлении, записанных при помощи строк.
Замечу, что в аксиоме использованы для обозначения чисел те буквы, которые были оговорены для этого в начале предыдущего раздела: i, j, k, l, m, n. Неявно это означает, что в каждой аксиоме имеется посылка о том, что используемый на месте числа объект - число (а не просто строка). Например, полная запись аксиомы (8.1) из предыдущего раздела будет:
a = b ⇔ ( ∀ i Num(i) ⇒ str(a, i, 1) = str(b, i, 1) )
Где одноместная предикатная буква Num(i) как раз «проверяет», является ли данная строка числом. Но раз мы условились об обозначении числа буквой i, то считаем это условие (про то, что тут число) исполненным и посылку с Num(i) пропускаем:
a = b ⇔ ∀ i str(a, i, 1) = str(b, i, 1)
Это обычная практика - как, например, в теории множеств принято изображать множества строчными, а классы - прописными буквами, а посылки с проверками на то, что объект - множество - типа M(x) - тогда не пишут.
Тем не менее, одноместная предикатная буква Num(i) о проверке строки на то, что она ещё и число - имеется в теории. И в связи с аксиомой о связи чисел и строк можно вывести:
Num(a) ⇔
len(a) ≠ ⊖ ∧ (str(a, 1, 1) = Chr(l_NumBeg) ⇒ a = str(a, 1, 1))
∧ ∀ i ≤ len(a): l_NumBeg ≤ Ach(str(a, i, 1)) ≤ l_NumLim
Пояснение: при вышеизложенной аксиоматизации о связи чисел и строк получается, что число представляет собой конечную строку из одних цифр, притом цифра «0» (ноль) может стоять на первом месте только в числе 0 (ноль).
Но представленная аксиоматизация для связи чисел и строк - совершенно не единственно возможная. Мы вполне можем написать аксиомы для представления чисел в духе «стандартной интерпретации». Вот так:
Аксиоматизация нуля:
0 = Chr(0)
Аксиоматизация увеличения на 1:
i ' = i ⋅ Chr(0)
Пояснение: Символы с номером 0 (ноль) мы используем как «счётные палочки». И их количество минус 1 и есть само число. А «кучи» этих «счётных палочек» мы организуем при помощи конкатенации.
При такой аксиоматизации можно вывести:
i + j = end(i ⋅ j, 0 ′′ )
i - j = end(i, len(j)), для i > j
Ну, а случай
i × j
Окажется конкатенацией из len(j) - 1 одинаковых строк end(i, 0 ′′ ) и конкатенация Chr(0) сверх того:
end(i, 0 ′′ ) ⋅ end(i, 0 ′′ ) … end(i, 0 ′′ ) ⋅ end(i, 0 ′′ ) ⋅ Chr(0)
Ну, или конкатенацией из len(i) - 1 строк end(j, 0 ′′ ) и конкатенация Chr(0) сверх того:
end(j, 0 ′′ ) ⋅ end(j, 0 ′′ ) … end(j, 0 ′′ ) ⋅ end(j, 0 ′′ ) ⋅ Chr(0)
Напоминаю, что для знака умножения использован символ «×», потому что символ «⋅» уже занят для обозначения конкатенации.
При таких аксиомах связи чисел и строк будет верно:
Num(a) ⇔ len(a) ≠ ⊖ ∧ len(a) ≠ 0 ∧ ( ∀ i 1 ≤ i ≤ len(a) ⇒ str(a, i, 1) = Chr(0) )
Как видим, одни и те же аксиомы арифметики допускают представление чисел и в таком виде, когда размер представления числа равен величине числа. Это совершенно не годится для правильной оценки размеров данных и времени работы с ними при рассмотрении алгоритмов, работающих со строками и числами в позиционном представлении. Впрочем, это уже было доказано в предыдущем разделе.