I. Как в теории выразить работу алгоритмов с бесконечными или слишком большими входными аргументами
. К оглавлению . Показать весь текст .
Данная статья опирается на теорию компьютерных строк, аксиомы которой были изложены и обсуждались в предыдущей статье «Теория компьютерных строк».
Сейчас в математической теории (пока что для этих целей используется арифметика) алгоритмы в теории «представлены» для модели рекурсивных (aka общерекурсивных) функций. Нюансы этой «представимости» мы неформально разберём в следующем (II) разделе, но начнём с того, как «надо» определять в теории (а в качестве теории мы возьмём теорию компьютерных строк) функцию Run(…), соответствующую шагам выполнению алгоритма в модели Машина исполнения компьютерных алгоритмов.
В этой статье мы не будем давать доказательства того, что следующее определение функции Run(…) действительно является определением, нам пока что нужен неформальный разбор функции Run(…), чтобы наметить направление исследования в теории компьютерных строк и увидеть одну из перспективных целей данного исследования. А затем в данной статье мы сделаем первые шаги в теоретическом формализме в выбранном направлении.
Существует и единственное Run(var, i_Step, Program, Start), такое что:
∃ Tracing (
Run(var, i_Step, Program, Start) = 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) - данная определяемая функция возвращает значение программной переменной, а имя этой программной переменной является значением аргумента var в данной функции теории. При этом:
1. Программный текст исполняемой программы является значением аргумента Program;
2. Начальные значения «входных» аргументов программы являются значением аргумента Start (они там «упакованы» и значение переменной Start выступает в роли «контейнера», об этом будет написано ниже);
3. Шаг исполнения очередной команды программы, для которого (после исполнения которого) функция Run(…) возвращает значение программной переменной с именем из аргумента var, равен значению аргумента i_Step.
Что касается «контейнера» для входных аргументов Start, то это легко делается разными способами со строками - способы можно брать у программистов, ниже мы лишь немного коснёмся деталей этого вопроса. Но нам обязательно надо решить вопрос о бесконечных строках, с которыми практики дел не имеют.
Заметим, что если программа работает конечное количество шагов, то любой входной аргумент используется программой лишь в некоторой своей начальной конечной части (которая может совпадать и со всем значением конечного аргумента, разумеется). Поэтому бесконечные или не полностью используемые программой входные данные в теории можно условно записать так, например:
Arg_1 = «Нужная часть строки» ⋅ Unknown_1
И предусмотреть для таких «частичных» входных значений способ записи в аргументе Start функции Run(…).
IsPerfect(var, Start) - вот что нужно для работы с «частичными аргументами». Нужна «отметка» - получены данные о строке в полном объёме (тогда значение данной функции будет 1), либо же у нас имеется только начальная часть значения данного программного аргумента (тогда значение данной функции будет 0). В переменной Start значение каждого программного аргумента/переменной может быть записано в таком формате:
MyVar 1 29 это строка длиной 29 символов
Где данные о значении аргумента/переменной начинаются с имени программного аргумента/переменной (MyVar здесь), затем через пробел идёт указание на то - полностью (1 здесь) или только в начальной части (0) записано далее значение данного аргумента/переменной. А далее (через пробел) - количество символов значения (29 здесь) строки или начальной части строки (в зависимости от предыдущего параметра). И в конце (через пробел) - сама строка («это строка длиной 29 символов» здесь) или её начальная часть - с ровно таким количеством символов, которое указано в предыдущем параметре.
Если у программного аргумента свойство IsPerfect равно 1, то он не может измениться в процессе работы программы на 0 (Ноль), потому что программа не создаёт значений, которые хоть в какой-то части ей не известны (не прочитаны и/или не созданы). Но если аргумент имел свойство IsPerfect равное 0, то оно может измениться (уже необратимо) на свойство IsPerfect равное 1. Такое происходит в случае присваивания данному аргументу нового значения со стиранием прежнего.
Программные переменные никогда не записаны частично (условимся об этом - разделять входные аргументы и создаваемые в процессе работы программы переменные). Но будем считать формат их записи в «контейнерах» одинаковым с форматом записи программных аргументов для единообразия.
Поэтому нам нужно, всё же, иметь свойство IsPerfect в процессе его изменения для каждого программного аргумента/переменной. То есть - можно для любых шагов программы получать это свойство программных аргументов/переменных посредством той же функции:
Run(var, i_Step, Program, Start), где var содержит уже не имя программного аргумента/переменной, а имя условной программной переменной для свойства IsPerfect соответствующего программного аргумента/переменной.
Имя для этой вводимой нами условной «программной переменной» пусть будет таким:
MyVar is perfect
Где «MyVar» - имя программного аргумента/переменной (может быть и другим), свойство IsPerfect которого нам нужно. То есть, имя для свойства IsPerfect данного программного аргумента/переменной получается конкатенацией имени данного программного аргумента/переменной со строкой « is perfect» (с ведущим пробелом).
Мы можем гарантировать, что никакого конфликта с именами других программных аргументов/переменных не возникнет, потому что эти имена, используемые в нашей модели и программных текстах, не содержат в себе знаков пробела. А на уровне теории в качестве значения 1-го аргумента функции Run(var, i_Step, Program, Start) мы можем использовать строки с пробелами.
Таким образом, мы выяснили (немного опережая пояснения про StartFrom(i, Tracing)), что:
IsPerfect(var, StartFrom(i, Tracing)) = VarFrom(var ⋅ « is perfect», StartFrom(i, Tracing))
Но нужно, конечно, понимать, что хранится значение для условных программных аргументов/переменных с именами вида «MyVar is perfect» в том же блоке данных, что и для основного программного аргумента/переменной с именем «MyVar». Вот так приблизительно (пример уже приводился):
MyVar 1 29 это строка длиной 29 символов
Это качается и начальных данных в переменной Start, и протокола исполнения в связанной квантором существования переменной Tracing.
Признак IsPerfect(var, Start) - это именно тот «нюанс», который делает выразимость алгоритмов в теории компьютерных строк полной. И этого признака, или его аналога, нет ни в рекурсивных функциях, ни в нынешнем «представлении» рекурсивных функций в арифметике. Хотя, на самом деле, можно ввести свойство IsPerfect и при рассмотрении алгоритмов в рамках арифметики.
Возникает вопрос о примате целостности и частичном чтении данных, раз они уже получены частично. Напоминаю (из «Теория компьютерных строк»), что в соответствии с гипотезой о примате целостности арифметики невозможно заменить частичное чтение начальной части строки на чтение начальной части числа арифметики, если числа и строки поставлены во взаимно-однозначное соответствие. Но, вроде бы, решать этот вопрос и не приходится, раз начальные части аргументов и без того имеются в аргументе Start функции Run. И в арифметики при таком подходе, уже есть число, соответствующее начальной части строки «частичного аргумента» - если мы работает с, например, гёделевыми номерами строк (и подстрок), вместо работы со строками (и подстроками).
Но теория нам нужна не только для того, чтобы «жить» в её рамках. Нам надо получать данные из реальности об объектах, соответствующих логике теории, чтобы исследовать их средствами теории. И, кроме того, нам надо применять результаты из теории именно к тем объектам реального мира, в отношении которых они сделаны. И если частичное чтение - не проблема для строк, но проблема для чисел в реальном мире, то нет смысла определять время и «доказывать» внутри арифметики скорость работы алгоритма с опорой на представления о скорости чтения строк. Потому что результат будет ложный, когда он будет применяться к тому, что является числами, но не строками. А отличить одно от другого на базе арифметики мы не можем. Рассмотрим пример.
Пусть у нас есть склад и текст инвентаризационной ведомости о количества товаров на нём. Данный текст начинается следующими строками текста:
Пиво Аксиоматическое - 50 бутылок
Пиво Не формальное - 60 бутылок
Текила Конкистадорская - 70 бутылок
…
Если мы в рамках теории можем доказать, что в первых 33 символах мы получаем информацию о количестве бутылок пива «Аксиоматическое», то это касается именно текста, но не бутылок нужной марки в виде их «натурального числа» на складе. Где (пусть склад одномерный) бутылки стоят так (тоже только часть склада):
11321231133212311123212223111231234312341211332212321232322331212132132211321…
Где 1 - «Аксиоматическое», 2 - «Не формальное», 3 - «Конкистадорская». Было бы ошибочно считать, что достав со склада 33 бутылки и пересчитав количество «Аксиоматического» среди них, мы узнаем этим своим «частичным чтением» сколько бутылок «Аксиоматического» на складе.
С гёделевыми номерами такая же история, как в приведённом примере, если верен примат целостности чисел арифметики относительно строк. Пока не прочитано число целиком - невозможно узнать начальную часть соответствующей строки. И время на это чтение может потребоваться неограниченно больше, чем то, что потребуется для работы программы с полученной частью входных данных.
В предыдущей статье был приведён пример «квазистрок», которые являются вариантом зашифрованных строк, и для которых выполнены аксиомы теории компьютерных строк, хотя строковые функции конкатенации и взятия подстроки у них своеобразные. Там был приведён пример:
«f» ⋅ «a» ⋅ «t» ⋅ «h» ⋅ «e» ⋅ «r» = «joseph», и при этом
«jos» = «l» ⋅ «o» ⋅ «l»
Но мы легко можем отличить «квазистроки» от «нормальных» строк, допускающих «частичное чтение» своего начала в модели Машина исполнения компьютерных алгоритмов, например. Для этого надо всего лишь, чтобы их вид совпадал с конкатенацией их символов. Как в примере:
«f» ⋅ «a» ⋅ «t» ⋅ «h» ⋅ «e» ⋅ «r» = «father»
Но, как видим, даже для того, чтобы отличить «квазистроки» от «нормальных» строк, нам нужна теория компьютерных строк и сравнение проверяемых реальных строк с «теоретическим форматом». Конечно, в жизни мы зачастую можем отличить зашифрованный текст от нормального и не формально, но если подходить к проверке с математическими стандартами, то нам следует опираться на теорию первого порядка с равенством.
А в теории компьютерных строк нам нужно, конечно, доказать соответствующие критерии «локальности», которые позволят в некоторых случаях гарантировать, что работа с данной начальной частью строки даёт тот же результат работы алгоритма, что и работа с полным значением строки. Видимо, аналогичные критерии можно использовать (и даже доказать) и в арифметике, даже если речь о числах, поставленных в соответствие строкам (или начальным частям строковых входных аргументов). Но это уже вопросы, которые возникают после чтения данных.
Доказательство соответствующих критериев локальности будет означать, что теория компьютерных строк в состоянии обосновать, и выразить работу тех алгоритмов, которые выдают результат даже при бесконечных строках на «входе» - чего невозможно добиться посредством рекурсивных функций и их «представлений».
И дело не только в решении вопроса с бесконечными строками на «входе», но и в «слишком больших» входных данных. Так, например, в теории алгоритмов могут быть чрезмерно большие сертификаты, которые должны быть отвергнуты в силу своего чрезмерного размера. И в теории компьютерных строк у нас есть возможность (будет, после доказательства соответствующих критериев локальности) выражать работу соответствующего алгоритма лишь при частичном значении (начальной части) для сертификата. Необходимо лишь, чтобы эта начальная часть была достаточна для того, чтобы алгоритм мог признать сертификат чрезмерно большим.
Разумеется, теория не может сама получать данные из реального мира. На границе между теорией и реальностью находимся мы, и это мы должны «частично прочитать» данные реального мира и записать в рамках теории такое представление для прочитанных данных, с которыми можно разбираться при помощи инструментов теории. Но мы должны отдавать себе отчёт, что именно мы «частично читаем» и к чему именно мы применяем результаты, полученные из теории. По крайней мере, в случае, если частичное чтение чисел не может заменить частичное чтение строк.
Конечно, мы можем слишком «урезать» нужную часть входного аргумента в аргументе-контейнере Start, что сделает невозможным правильный расчёт, мы можем получить «зацикливание» программы и другие случаи, которые отличаются от нормальной ситуации: «Программа имеет доступ ко всем нужным данным, работает, и завершает свою работу за конечное время».
Но для всех этих исключительных случаев мы можем предусмотреть те условности в определении функций DoIt(…) и FinishStep(Program, Start), которые всё равно дадут нам «существующий и единственный» результат - и для функции Run(…), и для функции FinishStep(…). Пусть даже для практиков подобный результат невозможен - это как наше определение для функции len(…), где предусмотрен результат (равный ⊖) даже для бесконечных строк.
И для выявления проблем, возникающих в теории при вычислении очередного шага работы алгоритма, нам потребуются критерии локальности. Потому что одна из возможных проблем - недостаточная полнота входных данных при разборе работы программы.
Кстати, FinishStep(Program, Start) - это тот шаг работы программы, в котором она достигла команды остановки. Либо, если программа не останавливается, результат будет равен ⊖. Либо, если возник форс-мажор из-за слишком короткой известной части входного аргумента или что-то подобное - номер последнего шага перед форс-мажором или ноль - если ошибка в начальных данных. Так можно определить FinishStep(Program, Start), что даст нам всегда «существование и единственность» для данного определения, но в детали реализации (реализации могут быть самые разные) в данной статье вдаваться не будем.
Итак, Start - это «контейнер» для входных аргументов, а Tracing - это «контейнер контейнеров» для состояний всех аргументов и переменных для каждого шага i_Step. Не обязательно, кстати, чтобы значение каждой переменной (или аргумента) повторялось внутри Tracing столько раз, сколько шагов работы программы хранит данная «упаковка» Tracing.
Каждая команда может менять не больше 2 программных переменных/аргументов при исполнении одной команды, чтобы Машина исполнения компьютерных алгоритмов успешно работала. И ещё при присваивании будет меняться, возможно, свойство IsPerfect, соответствующее программному аргументу/переменной присваивания. И если для данного шага значение переменной/аргумента в Tracing не приведено, то нужное значение равно самому позднему шагу, в котором это значение есть, но только до текущего шага.
Вот часть формулы:
StartFrom(i, Tracing)
Эта часть формулы извлекает из протокола исполнения (назовём так значение переменной Tracing) тот набор всех данных (состояние данных), который соответствует шагу i (после исполнения шага i) работы программы. И это состояние данных имеет тот же формат, что и формат стартовых данных в аргументе Start. Кстати, набор данных нулевого шага из Tracing равен набору стартовых данных Start, и это отражено в формуле вот здесь:
StartFrom(0, Tracing) = Start
Есть переменная и одновременно аргумент i_Program, которая указывает номер места начального символа текущей команды в программе Program. В стартовых данных Start значение этой переменной всегда равно 1.
Чтобы извлечь из состояния данных на шаге (после исполнения шага) i значение нужной программной переменной, используем функцию:
VarFrom(var, StartFrom(i, Tracing))
От шага к шагу значения программных переменных и аргументов меняются из-за работы программы и это отражено в следующей части разбираемого определения:
VarFrom(var, StartFrom(i′, Tracing)) = DoIt(var, Program, StartFrom(i, Tracing))
Функция DoIt() как раз и занята исполнением той команды, которая расположена в Program начиная с места i_Program после исполнения шага i (при состоянии программных аргументов/переменных, соответствующих StartFrom(i, Tracing)).
Почти все значения программных переменных и аргументов при выполнении одной команды программы остаются прежними, но меняется (если программа не остановилась или не завершилась аварийно) программная переменная i_Program (если только программа не достигла команды остановки) - во-первых. А, во-вторых, меняется тот программный аргумент/переменная, в отношении которой была исполнена команда присваивания (если текущая команда была командой присваивания). Притом изменяется (возможно) и свойство IsPerfect данного программного аргумента.
Вот именно в отношении этих программных аргументов/переменных функция DoIt выдаёт новые значения. Например, на 996 шаге происходило присваивание программной переменной с именем MyVar значения «Test», а номер символа следующей команды в программе стал 100234. Тогда будет верно:
VarFrom(«i_Program», StartFrom(996, Tracing)) =
= DoIt(«i_Program», Program, StartFrom(995, Tracing)) = 100234
VarFrom(«MyVar», StartFrom(996, Tracing)) =
= DoIt(«MyVar», Program, StartFrom(995, Tracing)) = «Test»
VarFrom(«MyVar is perfect», StartFrom(996, Tracing)) =
= DoIt(«MyVar is perfect», Program, StartFrom(995, Tracing)) = 1
Разумеется, в теории могут возникать исключительные ситуации не алгоритмического характера. Вроде нарушения критерия локальности, когда программа обращается к той части частичного программного аргумента, которой нет в аргументе теории Start. Тогда можно, например, выдавать в качестве нового значения программной переменой i_Program пустую строку ⊖, например, и не менять после данного шага работы программы никакие значения программных переменных. Это будет означать, что нам нужен другой набор частичных аргументов, чтобы выразить работу данного алгоритма в теории - если данный алгоритм вообще заканчивает свою работу в реальности.
При этом все собственно программные «хитрости» исполнения определены в функции DoIt(). Она просто делает один шаг работы программы при заданном состоянии данных - включая номер первого символа исполняемой программы, который содержит программная переменная с именем i_Program. В принципиальном отношении это весьма простое «одношаговое» определение для данной функции, но оно довольно громоздкое и требует прописать все команды для нашей модели Машина исполнения компьютерных алгоритмов в данном определении. Но в данной статье мы не будем этого делать.
Вот и всё - в принципиальном отношении - объяснение того как и из чего строится определение функции Run(var, i_Step, Program, Start), играющей в теории компьютерных строк роль Машины исполнения компьютерных алгоритмов.
Теперь у нас есть «эталон» для сравнения с тем, что было сделано, и используется сейчас в арифметике в качестве «компьютера». «Эталон», кстати, гораздо проще (если не учитывать свойства IsPerfect) чем то, что используется сейчас, поэтому для удобства взят именно он в качестве «отправной точки» рассмотрения. К тому же «эталон» выразительнее своих нынешних арифметических аналогов за счёт возможности определить, обосновать и использовать в теории компьютерных строк частичные программные аргументы и их свойство IsPerfect.
Во-первых, должен отметить, что «протокол исполнения» и способ строить функцию с его помощью (точнее, с помощью аналога протокола исполнения) изобрёл вовсе не я, а логики периода великих логических открытий. Идея та же, что использована для β-функции Гёделя. Смотри, например, «Введение в математическую логику» Э. Мендельсон, Предложение 3.21. К тому же мы неформально рассмотрим в следующем разделе принципиальные особенности «представимости» алгоритмов в арифметике.
Во-вторых, в арифметике нет той лёгкости операций с аналогами строк (в арифметике нет строк), которая есть в теории компьютерных строк и, которая использована при неформальном рассмотрении определения функции Run(var, i_Step, Program, Start). И в арифметике нет «контейнеров», так как число арифметики не может иметь никакой структуры (что будет разобрано в III разделе), есть только величина числа.
В-третьих, если смотреть имеющиеся сейчас доказательства о неполноте, неразрешимости и т.п., то там неявно, но очень существенно использована логика работы с формулами (что можно свести к логике строк), выходящая за рамки арифметики, но математики не заметили этого - или просто забыли это упомянуть. Этот «невидимый» и при этом «лежащий на поверхности» факт мы рассмотрим в следующем разделе.