II. Трудности в арифметике с тем, чтобы выразить работу алгоритмов

[dmitgu]

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

Чтобы почувствовать разницу между теорией компьютерных строк и арифметикой, рассмотрим вопрос - почему в арифметике операция сложения аксиоматизируется, а не определяется? Ведь с использованием техники «протокола исполнения» вполне можно (вроде бы) дать для суммы a + i_Step следующее определение:

∃ Tracing (

a + i_Step = IncStep(i_Step, Tracing)

∧ IncStep(0, Tracing) = a

∧ ∀ i < i_Step: IncStep(i′, Tracing) = IncStep(i, Tracing)′

)

Приведённое «определение» для сложения явно сводит сумму к последовательности операций увеличения на 1. Для теории Пеано такое определение невозможно. Без аксиом сложения (и аксиом умножения) теория оказывается недостаточно выразительной для формулировки подобного «определения». А вот вместе со сложением и умножением появляется возможность использовать числа как аналоги «контейнеров».

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



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

И есть функция (на базе β-функции Гёделя), которая даёт в зависимости от индекса и ещё пары «базовых» чисел (одно из которых - факториал от максимума «нужной» последовательности и количества членов в ней), результаты функции, равные членам простой конечной последовательности взаимно простых чисел. А при помощи двух «базовых» чисел можно «отрегулировать» количество членов в соответствующей последовательности и величину взаимно простых членов этой соответствующей последовательности.

И можно использовать эти 2 возможности вместе:

1. Использовать функцию (на базе β-функции Гёделя), которая по индексу даёт число, взаимно простое с результатами этой функции для других значений индекса.

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

3. Через «большое число» п.2 и одно из взаимно простых чисел, получаемое через индекс i п.1 - получить (используя китайскую теорему об остатках) значение i-го члена нужной последовательности.

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

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

Из-за того, что без аксиом сложения и умножения арифметика не позволяет использовать аналоги «протоколов исполнения» приходится не определять, а аксиоматизировать сложение (и умножение). Вот аксиомы теории Пеано для сложения:

(Q_4) ∀ i (i + 0 = i)

(Q_5) ∀ i ∀ j ( i + j ′= (i + j) ′ )

Как видим, сложение просто индуктивно сводится к операциям увеличения на 1. А умножение сводится к сложению. То есть - умножение тоже в итоге сводится к операциям увеличения на 1.

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

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

Кстати - это весьма типичный способ - искать подход к решению вопроса в одной теории с помощью другой - более выразительной. Но у нас тут более радикальный случай, который тоже имеет свои аналоги (следующий абзац - цитата из Э. Мендельсон, «Введение в математическую логику», после Предложение 3.11):

С другой стороны, некоторые классические результаты теории чисел, такие, как теорема Дирихле, доказаны с помощью теории функций комплексного переменного, причём зачастую неизвестно даже, можно ли получить элементарные доказательства (или вывод в S) для таких теорем.

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

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

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

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

Отсутствие общего доказательства для аналогов протокола исполнения внутри арифметики приводит к тому, что в арифметике невозможно определять функции, подобно тому, как это сделано (иллюстративно) в начале статьи для функции Run(var, i_Step, Program, Start). Чуть ниже я раскрою причины.

Поэтому подобные функции не определяются в арифметике, а «представимы» в ней. (Поэтому, кстати, в арифметике алгоритмы не «выразимы», а «представимы»). «Представимость» - это как если бы в определении, которое написано в начале данной статьи, для функции Run(var, i_Step, Program, Start) было вместо Run(var, i_Step, Program, Start) написана не данная функция со скобками и аргументами, а RunValue, например:

∃ Tracing (

RunValue = VarFrom(var, StartFrom(i_Step, Tracing))

∧ StartFrom(0, Tracing) = Start

∧ ∀ i < i_Step: VarFrom(var, StartFrom(i′, Tracing)) = DoIt(var, Program, StartFrom(i, Tracing))

)

А для всей этой формулы мы бы ввели обозначение:

RUN(var, i_Step, Program, Start, RunValue)

И эта формула была бы:

1. Доказана тогда, когда вместо RunValue подставлено правильное значение для заданных (тоже подставленных) значений остальных аргументов var, i_Step, Program, Start;

2. Доказано отрицание формулы тогда, когда вместо RunValue подставлено не правильное значение для заданных (тоже подставленных) значений остальных аргументов var, i_Step, Program, Start;

3. Для любого набора конкретных значений аргументов формулы RUN(var, i_Step, Program, Start, RunValue), исключая аргумент RunValue, существует только одно значение для аргумента RunValue, при котором данная формула истинна.

Для арифметики вместо строк в определении логической формулы RUN(var, i_Step, Program, Start, RunValue) должны пониматься в качестве значений аргументов гёделевы номера строк или их аналоги, конечно. И я упрощаю арифметические построения в данном примере определения - в арифметике в них будет более одного квантора существования, а сверх того ещё и конструкции типа β-функции Гёделя и подобные им.

Проблема с тем, чтобы заменить «представимость» функции Run(var, i_Step, Program, Start) на её определение («выразимость»), состоит в том, что пункт 3 - про конкретные значения аргументов, а не вот такой:

3-б) ∃_1 RunValue (RUN(var, i_Step, Program, Start, RunValue))

С таким доказанным третьим пунктом у нас была бы «строгая представимость», которая позволяет уже давать определение - см. в «Теория компьютерных строк» раздел 4, пункт IV.5 «Введение новых функциональных букв и предметных констант».

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

Всегда путаюсь в этих обозначениях для не однозначных конкретных значений - это может быть маленькая чёрточка наверху, готический шрифт, жирный шрифт и т.п. варианты, которые или трудно разглядеть, или они в других книгах понимаются иначе. Чтобы не присматриваться к обозначению конкретного, но не однозначного, значения хотя бы в своей статье, введу такое обозначение:

(∀_1 x), которое можно ставить в соответствующем месте формулы.

Квантор общности, «испорченный» конкретизацией.

Если у нас есть доказательства для формулы F(a, b), для каждого случая конкретных значений аргументов, когда они равны, то это можно записать так:

∀_1 a F(a, a). То есть - имеется доказательство для формулы, которая получается из F(a, a), если в эту формулу подставить на место a конкретное значение - притом любое. И доказательство данной формулы для одного конкретного значения не отменяет необходимости доказывать эту же формулу для другого конкретного значения.

Кстати, если необходимо одно неоднозначное конкретное значение, то можно и не «задваивать» связанную «квантором» ∀_1 переменную. И вместо ∀_1 a F(a) писать F((∀_1 a)).

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

Пункт 3 для не строгой представимости можно тогда записать так:

3) ∃_1 RunValue RUN((∀_1 var), (∀_1 i_Step), (∀_1 Program), (∀_1 Start), RunValue)

Понятно, что пункты 1 и 2 теперь тоже можно переписать в формальном виде, читатель сам представляет, как.

Так вот, доказательство формул-определений рекурсивных функций, записанных на языке арифметики, проводится для общего случая произвольных аргументов, но - вне рамок арифметики. Про это сказано выше - произведение членов последовательности (чуть сложнее, чем произведение членов последовательности на самом деле) и факториал от максимального члена нужной последовательности/количества членов используются до их определения внутри арифметики. Поэтому внутри арифметики мы имеем доказательства только для конкретных значений аргументов. Поэтому получается третий пункт - с не строгой представимостью. А поэтому формула-определение функции не становится определением внутри арифметики, а остаётся лишь формулой. А поэтому в арифметике мы имеем представимость (не строгую) привычных нам функций, а не сами функции.

А можно ли в арифметике как-то иначе строить формулы-определения функций, чтобы их можно было доказывать, как действительно определения в рамках арифметики? Не знаю, но предполагаю, что нельзя. Слишком хорошие математики занимались вопросом определения/представления функций в арифметике, чтобы они могли упустить возможность для строгой представимости (термин даже придумали!), если бы такая возможность была - как мне представляется. Но отсутствие таких возможностей в арифметике не доказано или я не знаю об имеющихся доказательствах.

А что же в теории компьютерных строк? А в ней нет никаких проблем с тем, чтобы определить конечную (да и бесконечную можно при необходимости) последовательность чисел или любые другие аналогичные контейнеры. Поэтому представимость - строгая, привычные функции (и алгоритмы) можно определять и доказывать корректность этих определений внутри теории. И не надо строить никаких дополнительный конструкций вроде β-функции Гёделя с факториалами, потому что логика для конструирования контейнеров из строк заложена в аксиомах теории компьютерных строк.

Из-за того, что строки обладают логикой контейнеров - не приходится выходить за рамки теории, чтобы использовать «внешнюю» логику для контейнеров. Поэтому доказательство можно провести в рамках теории для общего случая, а это даёт строгую представимость и определение для функции оказывается «внутренним». Я не могу сразу всё это сделать в одной статье, но, чтобы идти куда-то - надо иметь план и идеи - куда двигаться и зачем - для начала. К тому же - это работа не для одного человека, я не претендую делать всё один, и не мешаю никому быть самостоятельными авторами в этом направлении. Я с удовольствием многое почитаю, вместо того, чтобы писать всё самому.

Пример определения для конечной числовой последовательности в теории компьютерных строк (в не формальном виде):

Текст (строка с символами перевода строки), которая содержит только цифры и символы перевода строки. Притом:

1. Текст начинается с цифры, заканчивается переводом строки, и никакие символы перевода строки не расположены рядом друг с другом;

2. Любая подстрока, которая начинается с цифры в начале текста или сразу после символа перевода строки, а заканчивается сразу перед ближайшим от её начала символом перевода строки является числом.

Если кому-то больше нравится обычная запись последовательности, где числа разделены запятой и пробелом - то это тоже вариант, который можно сделать определением. И эти определения будут эквивалентны в плане теорем, доказанных с их помощью о конечных последовательностях. То есть, любое из них будет «без ограничения общности» в плане работы с последовательностями.

Кстати, теория компьютерных строк содержит теорию Пеано в качестве своей части. Но возможно, что можно обойтись лишь частью теории Пеано, а сложение и умножение определить, используя возможности строк в качестве «контейнеров», которые хранят «Протоколы исполнения». Но какие из аксиом Пеано можно «выбросить» (если это вообще возможно), чтобы логика строк сохранила возможность использования строк в качестве «контейнеров» - интересный вопрос для «чистой математики». Пришлось бы, конечно, рассматривать сразу аксиомы связи между числами и строками. Но данный вопрос не является приоритетным, на мой взгляд, поэтому «Не буду думать об этом сегодня», как говорила Скарлетт O′ Хара в фильме «Унесенные ветром».

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

Такая аксиоматизация чисел в духе «стандартной интерпретации арифметики» делается на базе аксиом:

0 = Chr(0)

i ‘ = i ⋅ Chr(0)

Остальное выводится - в том числе из аксиом Пеано.

Введём для удобства обозначение для символа (не пустого), который играет роль перевода строки, и не равен ни одной цифре (в нашем случае это всего лишь цифра Chr(0)):

ChrEnter

Конечная последовательность чисел - это конкатенация между собой «блоков» символов. Где каждый блок представляет собой конкатенацию нескольких символов Chr(0) подряд плюс в конце символ ChrEnter.

Определим функцию IsSequence(x) для проверки, является ли строка конечной последовательностью:

IsSequence(x) = 1

∧ (∀ i str(x, i, 1) = Chr(0) ∨ str(x, i, 1) = ChrEnter ∨ str(x, i, 1) = ⊖ )

∧ (∀ i str(x, i, 2) ≠ ChrEnter ⋅ ChrEnter)

∧ (len(x) ≠ ⊖ ∧ str(x, len(x), 1) = ChrEnter)

∨

IsSequence(x) = 0

∧ (

(∃ i str(x, i, 1) ≠ Chr(0) ∧ str(x, i, 1) ≠ ChrEnter ∧ str(x, i, 1) ≠ ⊖ )

∨ (∃ i str(x, i, 2) = ChrEnter ⋅ ChrEnter)

∨ (len(x) = ⊖ ∨ str(x, len(x), 1) ≠ ChrEnter)

)

Приоритет операций обычный для логики - сначала исполняются логические «и», затем - логические «или».

Очевидно, что приведённая формула является определением, то есть существование и единственность результата выводятся для произвольного аргумента (в данной формуле аргумент один - переменная x).

А какие объекты есть в арифметике, чтобы в терминах теории дать определение для последовательности чисел, если объектами арифметики являются только числа арифметики? Никакие, конечно.

В арифметике невозможно выделить какие-то числа, каждое из которых является последовательностью чисел. Все построения в духе «если посчитать вот эту функцию, подставив индекс» - это про наши операции с объектами теории, а не про объекты теории.

А именно - числа и последовательности не могут быть равны - это разные объекты. Но в рамках представления последовательностей их гёделевыми номерами, например, у нас будут равны между собой некоторые числа и последовательности (которые тоже в арифметике - числа). А это значит, что арифметика недостаточно выразительна - она не в состоянии полноценно выразить взаимные свойства между последовательностями чисел и самими числами.

Секундочку. Но мы же можем добиться, чтобы гёделевым номерам чисел соответствовали одни числа арифметики, а гёделевым номерам последовательностей чисел - другие?

Да, можем. Тогда возникает вопрос - числа арифметики и числа как гёделевы номера - это одно и то же или нет? Мы что извлекаем из «последовательности чисел» с i-го места - само число или гёделев номер этого числа?

Если мы извлекаем число, то справедлива первоначальная претензия - это число является в некоторых случаях последовательностью (выполнено равенство между ними). А это неправильно, потому что числа и последовательности - это разные объекты.

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

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

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

То, что подобная «двойственность» отношения к числам арифметики как к просто числам и как к гёделевым номерам (например), стала привычной, не отменяет того факта, что ошибка остаётся ошибкой - совершенно независимо от того, совершает эту ошибку один человек, многие, большинство или все.

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

Метатеорема (о меньшей выразительности арифметики в сравнении с теорией компьютерных строк при работе с последовательностями чисел):

Арифметика не в состоянии правильно выразить взаимные свойства чисел и числовых последовательностей между собой. Теория компьютерных строк, напротив - в состоянии это сделать, если в ней задана связь между числами и строками и имеется один непустой символ, который не является цифрой.

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

Может быть, есть альтернатива теории компьютерных строк в виде «комбинированной» теории вроде арифметика + теория множеств? Часто ссылаются на теорию множеств, используют язык теории множеств и, кажется, верят, что её можно «скомбинировать» с любой другой теорией и получить ту же теорию, но ещё и с «множествами» из её объектов. А «множества из её объектов» станут новыми объектами с нужными свойствами. Но я не вижу на практике ни построения, ни использования таких «комбинированных» теорий, формализованных в соответствии со стандартами для теории первого порядка с равенством.

Лично меня в теории множеств не устраивает аксиома объёмности. Считать, что объекты являются одинаковыми в том случае, если они состоят из одинаковых элементов - я не могу - после того, сколько в детстве собирал разных конструкций из одних и тех же элементов детского конструктора. Возможно, у кого-то есть для меня «хитрые» объяснения на этот счёт, но теория с такими «хитрыми» толкованиями представляется мне сомнительной альтернативой для прикладного применения вместо понятной и наглядной логики строк.

Теория компьютерных строк нужна хотя бы потому, что есть огромная практическая деятельность в сфере ИТ с массивами, базами данных и т.п., что можно на формальном уровне рассматривать, как последовательности (не только числовые) и давать соответствующие определения в теории компьютерных строк. А в арифметике - как было отмечено чуть выше - нельзя. Поэтому нам нужна в математике теория, возможности которой соответствуют огромной в наше время практике - притом практике в весьма интеллектуальной сфере, где систематизация и отработанные в математике методы исследования и обучения уместны, и необходимы.

В шутку говоря, теория компьютерных строк позволяет выстроить между математикой и программированием взаимовыгодный «фэншуй».

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

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

Немного подробней о «наших методах», отличающихся от формальной арифметики. Например, функция y=m^n, которую мы используем для геометрической прогрессии и суммы её членов. Я представляю себе определение этой функции примерно так:

m × m × … × m, где сомножители m повторятся n раз. А от этой последовательности (если смотреть дальше) я перехожу к (m × m) × … × m, к ((m × m) × m) × … × m, к …

Это определение вполне можно дать в рамках теории строк - включив в текст нужные арифметические знаки, дав формальное определение текстам числовых выражений и тому, какое числовое выражение считается шагом вычисления из предыдущего выражения. И можно тогда доказывать «цепочку вычислений» от произведения m × m × … × m до конкретного числа. То есть, определить функцию «Вычислить». И тогда y=m^n для конкретных чисел будет генерацией нужного текста числового выражения и применение к нему функции «Вычислить».

Есть нюанс - нам надо как-то перейти от текста вида 2^10 (только записанный в одну строку - как в Latex, например) к тексту вида m × m × … × m. Для этого могут быть такие шаги вычисления (каждый абзац - отдельный текст, являющийся шагом вычисления для предыдущего):

2^10

2^9 × 2

2^8 × 2 × 2

2^7 × 2 × 2 × 2

Хотя, вместо последнего текста может быть и такой шаг вычисления:

2^8 × 4

И т.д.

То есть - шагом вычисления может быть сведение «сложной» операции к простым операциям, либо к менее сложной (понижение степени в нашем случае) операции и простой операции.

Это тот способ (не самый оптимальный), который приходит мне в голову первым и который тоже можно реализовать в рамках теории строк. Или использовать для определения метод из начала статьи или какой-то другой способ.

Функцию Run из начала статьи можно использовать как весьма универсальный способ определения вычислимых функций в теории строк. А именно:

Можно придумывать тесты программ для программного аргумента Program, заносить «входные» аргументы определяемой функции в аргумент Start функции Run в качестве программных аргументов и задавать программный аргумент/переменную, откуда брать результат в конце вычисления в качестве результата определяемой функции.

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

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

А если бы мне предложили быстро найти способ получить функцию y=m^n без теории компьютерных строк? Я бы добавил пару аксиом к аксиомам Пеано - это первое, что приходит мне в голову. А придумать метод с аналогом «протокола исполнения» я бы сам едва ли смог без книг по логике с его изложением. Математики (видимо, Гёдель?) очень удачно придумали данный метод с аналогом «протокола исполнения».

Кстати, не следует и преуменьшать выразительные возможности арифметики. Разумеется в ней можно доказать (логически вывести) формулу, эквивалентную равенству функции прямого суммирования членов геометрической прогрессии (пусть Sgp(a_0, q, i)) и функции быстрого расчёта этой суммы (пусть Qsgp(a_0, q, i)). Просто в арифметике вместо равенства:

Sgp(a_0, q, i) = Qsgp(a_0, q, i)

Будет доказана (логически выведена) эквивалентность:

SGP(a_0, q, i, sum) ⇔ QSGP(a_0, q, i, sum)

Где SGP(a_0, q, i, sum) представляет функцию Sgp(a_0, q, i), а QSGP(a_0, q, i, sum) представляет функцию Qsgp(a_0, q, i).

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

Внутри арифметики остаётся другая проблема - невозможность доказать строгую представимость функции и корректно определить функцию внутри арифметики на базе формулы строгого представления. Функция - значит, должна сопоставлять каждому набору аргументов не более, чем 1 результат. И чтобы доказано это было внутри арифметики в общем виде, а не для каждого набора конкретных значений аргументов отдельно. Хотя «снаружи» арифметики у нас доказано именно это.

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

Итак, я предполагаю, что в арифметике можно определить формулу RUN(var, i_Step, Program, Start, RunValue), которая представляет (не строго) функцию исполнение алгоритма (для программной переменной с гёделевым номером её имени в аргументе var) с гёделевым номером программного текста Program и значениями (включая частичные) входных аргументов, «упакованных» в гёделев номер Start.

При этом свойство любого программного аргумента/переменной IsPerfect тоже доступно через RUN() и через гёделев номер имени этого свойства для соответствующего аргумента.

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

Однако, математики в процессе реализации программы Гильберта пошли иным путём - через представление в арифметике рекурсивных функций в качестве модели исполнения алгоритмов. Это ощутимо сложнее, притом рекурсивные функции - «не совсем правильная» модель. Причины для выбора такого пути интересны, на мой взгляд, и мы попытаемся с ними разобраться в IV разделе данной статьи.

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