dmitgu

Category:

3. Числа в теории строк

. К оглавлению . Показать весь текст .
То, что в теории строк мы опираемся в «конструировании» объектов не только на ноль, создаёт свойства для строк сверх тех свойств, которые есть у чисел в теории Пеано. У строк теперь есть собственная структура «цепочка символов. Вопрос – как эту же структуру придать числам, которые используются в теории строк? Это будет та структура, которой нет у чисел арифметики (арифметики Пеано, в частности), но есть у чисел в позиционном представлении.

 Что касается чисел, которые использованы в аксиомах теории строк, то они подчиняются обычным свойствам арифметики, и тут мы имеем (в неявном виде пока) ещё аксиомы теории Пеано или её арифметического расширения. Запишем явным образом аксиомы теории Q, достаточной для представления рекурсивных функций, а затем и её расширение до теории Пеано.

Дж. Булос, P. Джеффри «Вычислимость и логика» Глава 14. Представимость в Q. Аксиомы теории Q. 

Q_1  ∀x ∀y (x ′ = y ′ ⇒ x = y)

Q_2  ∀x 0 ≠ x ′

Q_3  ∀x ( x ≠ 0 ⇒ ∃ y x = y ′ )

Q_4  ∀x x+0=x

Q_5  ∀x ∀y ( x + y ′= (x + y) ′ )

Q_6  ∀x x×0=0

Q_7  ∀x ∀y ( x×(y ′ ) = (x×y) + x )

Замечу, что для знака умножения использован символ «×», потому что символ «⋅» уже занят для обозначения конкатенации.

Глава 15 Неразрешимость, неопределимость и полнота. В той же книге. Добавление аксиом индукции к теории Q и переход к теории Пеано – «теории Z».

( ( A(0) ∧ ∀x (A(x) ⇒ A(x ′ )) ) ⇒ ∀x (A(x)) ) – все формулы такого вида на языке арифметики, но с навешиванием на такие формулы квантора общности ∀x. 

При этом аксиому Q_3 можно исключить, так как она выводится из аксиомы индукции и аксиомы Q_2. 

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

Вот нужные для «превращения» некоторых строк ещё и в числа аксиомы:

∃ l_NumBeg ∃ l_NumLim: 

( 0 ≤ l_NumBeg < l_NumLim ≤ I_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. Неявно это означает, что в каждой аксиоме имеется посылка о том, что используемый на месте числа объект – число (а не просто строка). Например, полная запись первой аксиомы из предыдущего раздела будет:

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

(∃ l: str(a, l ’, 1) = ⊖) ∧ ( str(a, 1, 1) = Chr(NumBeg) ⇒ a = str(a, 1, 1))

∧ ( str(a, i, 1) = Chr(j) ∧ 1 ≤ i ≤ len(a) ⇒ NumBeg ≤ j ≤ NumLim ).

Пояснение: При вышеизложенной аксиоматизации о связи чисел и строк получается, что число представляет собой конечную строку из одних цифр, притом цифра «0» (ноль) может стоять на первом месте только в числе 0 (ноль).

Но представленная аксиоматизация для связи чисел и строк – совершенно не единственно возможная. Мы вполне можем написать аксиомы для представления чисел в духе «стандартной интерпретации». Вот так:

Аксиоматизация нуля:

0 = ⊖

Аксиоматизация увеличения на 1:

i ' = i ⋅ Chr(0)

Пояснение: Символы с номером 0 (ноль) мы используем как «счётные палочки». И их количество и есть само число. А «кучи» этих «счётных палочек» мы организуем при помощи конкатенации.

После такой аксиоматизации можно вывести:

i + j = i ⋅ j  

i - j = str(i, len(j)’, len(i))

Ну, а случай 

i × j

Окажется конкатенацией из len(j) следующих одинаковых строк:

i ⋅ i … i ⋅ i 

Ну, или конкатенацией из len(i) таких одинаковых строк:

j ⋅ j … j ⋅ j

Напоминаю, что для знака умножения использован символ «×», потому что символ «⋅» уже занят для обозначения конкатенации.

При таких аксиомах связи чисел и строк будет верно:

Num(a) ⇔ ( ∃ l: str(a, l ’, 1) = ⊖ ) ∧ ( 1 ≤ i ≤ len(a) ⇒ str(a, i, 1) = Chr(0) )

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

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

И, разумеется, «гёделевы номера» тоже не подходят для задач теории алгоритмов по тем же причинам. Но на базе теории строк можно использовать для представления формул теории строк сами строки. Строки обладают необходимыми свойствами для теории алгоритмов, к тому же они полностью соответствуют практике программирования. 

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

Сформулированные аксиомы теории строк являются лишь первым шагом на пути реализации программы Гильберта в отношении теории алгоритмов. А реализация программы Гильберта для теории алгоритмов совершенно необходима, иначе даже формализация понятия сложности оказывается невозможной, что было отмечено в данной статье во Введении. Но рассмотрение следующих вопросов оставим для следующих статей. А данная статья на этом закончена.

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.