May 15th, 2021

ёжик

Как "работает" программа в математической теории. Теория компьютерных строк выразительнее арифметики

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

Оглавление и введение

I. Как в теории выразить работу алгоритмов с бесконечными или слишком большими входными аргументами

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

III. Стандартная интерпретация арифметики и «не замеченная» логика строк

IV. Рекурсивные функции – удачный для своего времени паллиатив «правильной» модели исполнения алгоритмов

Введение

Подготовил вводную часть для одной статьи в мат. журнал (вчера отправил, пока ещё не ответили, но мало ли чем занят человек или подумать надо). Но материал интересный, выложу сюда, постепенно уберу в тексте ссылки на основную часть статьи, чтобы оставить вводную часть тут (в ЖЖ) как самостоятельную статью.

Аннотация 

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

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

В отношении доказательств теорем логики о неполноте, неразрешимости и т.п. приведены факты неформальной, но принципиальной для проведения доказательств опоры на логику строк. 

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


ёжик

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

)

Теперь разберём что, где и, почему записано в данной формуле.

Collapse )
ёжик

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

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

Чтобы почувствовать разницу между теорией компьютерных строк и арифметикой, рассмотрим вопрос – почему в арифметике операция сложения аксиоматизируется, а не определяется? Ведь с использованием техники «протокола исполнения» вполне можно (вроде бы) дать для суммы 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. Для теории Пеано такое определение невозможно. Без аксиом сложения (и аксиом умножения) теория оказывается недостаточно выразительной для формулировки подобного «определения». А вот вместе со сложением и умножением появляется возможность использовать числа как аналоги «контейнеров». 

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

Collapse )
ёжик

III. Стандартная интерпретация арифметики и «не замеченная» логика строк

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

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

Я немного детализирую стандартную интерпретацию (детализирую в сравнении с классическими «Основаниями математики» Гильберта и Бернайса, например), чтоб подчеркнуть слабые стороны в её выразительности.

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

Как работает тогда операция равенства a=b? Мы перебрасываем по одной единице в обеих коробочках одновременно. Если единицы в основной коробочке a закончатся одновременно с единицами в основной коробочке b, то числа равны. Иначе – не равны.

Collapse )
ёжик

IV. Рекурсивные функции-удачный для своего времени паллиатив правильной модели исполнения алгоритмов

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

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

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

Collapse )