Потеряем общность, но получим легкость преобразований

[EminentVictorians]

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

$$\int\limits_{a}^{b} f + g = \int\limits_{a}^{b} f + \int\limits_{a}^{b} g$$

работает далеко не по щелчку пальцев и требует проверять разные условия: нужно чтобы функции $f$ и $g$ были интегрируемы по Риману, т.е. надо проверять их ограниченность, проверять меру множества их точек разрыва на этом отрезке (чтобы удовлетворлся критерий Лебега). И это нам еще повезло: здесь хотя бы не надо контролировать области определения: при "расщеплении" функции $f+g$ на функции $f$ и $g$ область определения может только расшириться, но не сузиться.

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

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

Да, получится так, что средствами такого языка не получится определить какую-нибудь канторову лестницу или даже функцию Дирихле. Да и пофигу, не больно и хотелось. А вот что хочется - так это чтобы в качестве базовой числовой системы было не $\mathbb R$. Я сомневаюсь, что подойдет какое-то топорное решение типа вычислимых чисел - это было бы довольно грустно. Хочется, чтобы числовая система была сильно интереснее: можно, например, пожертвовать существованием или алгоритмическим определением нуля (а иметь вместо него "монаду" околонулевых чисел). Вероятно, операции с числами должны быть всюду определенными или по крайней мере с алгоритмической разрешимостью (чтобы компилятор бил по рукам, если пытаешься сделать запрещенную операцию). Можно пожертвовать неограниченностью чисел.

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

[dgwuqtj]

А чем $\mathbb R$ не устраивает? Вообще сейчас популярно пробовать использовать что-то вроде локалей. Там, в отличие от вычислимых чисел, и локальная компактность есть.

[Cnupm]

EminentVictorians
Хочется стремиться к конструктивности во всём. Ну хотя бы избавиться от большей части доказательств от противного. Есть разделы, где ну почти всё от противного. Ну не безобразие ли?

[EminentVictorians]

dgwuqtj в сообщении #1649813 писал(а):

А чем $\mathbb R$ не устраивает?

Плохо с алгоритмизируемостью, базовая операция деления - частичная (откуда, к слову, растут ноги того, что не бывает свободных полей), нету бесконечно малых. $\mathbb R$ же нужны в основном ради анализа, но мне кажется, что фрэймворк пределов - не лучшая основа для анализа. То, что получается в результате компактификации (любой - хоть одноточечной, хоть двухточечной) не ведет себя как число (но все же ведет себя довольно близко к этому, что наталкивает на мысль, что если отказаться от чего-нибудь типа неограниченности, то бесконечности можно было бы нативно ввести в анализ как числа). Еще момент, связанный с теоретико-множественной основой: мы имеем право определять функции, определенные на любом подмножестве $M \subset \mathbb R$. Имхо, это плохо. Язык должен ограничивать произвол. Т.е. одна из претензий к $\mathbb R$, грубо говоря, в том, что они слишком "теоретико-множественные".

Из альтернатив прикольная - Fermat real numbers (работы Paolo Giordano). С точки зрения алгоритмики интересный вариант - поле Леви-Чивита. Но они все какие-то теоретико-множественные, так что все равно не то. Есть еще "alpha-theory" (Vieri Benci and Mauro Di Nasso), но я пока не очень понял, о чем там речь.

[Anton_Peplov]

EminentVictorians в сообщении #1649807 писал(а):

можно, например, пожертвовать существованием или алгоритмическим определением нуля

Вам не нравится ноль, потому что результат операции $a/0$ не определен. Если Вы выбросите ноль, как будет определен результат операции $a-a$?

[drzewo]

EminentVictorians в сообщении #1649807 писал(а):

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

Это еще Пуанкаре заметил, что общность теории обратно пропорциональна ее содержательности.
Только банальные высказывания верны всегда и безусловно

-- 13.08.2024, 22:08 --

EminentVictorians в сообщении #1649807 писал(а):

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

Ровно наоборот.

[EminentVictorians]

Anton_Peplov в сообщении #1649839 писал(а):

Если Вы выбросите ноль, как будет определен результат операции $a-a$?

Операция разности не обязана быть однозначной, вместо нуля может быть монада околонулевых чисел. Или, например, разность двух одинаковых чисел писать можно, но считать нельзя (ну, гипотетически, если у нас это все происходит в языке с ленивой (или похожей на ленивую) моделью вычислений, который $a-a$ вычислять не будет, но Вы так писать можете; просто эта разность будет не числом, а "синтаксическим сахаром"). Мне сложно вот так сходу накидать вариантов, потому что хотелось бы посмотреть на уже существующие теории.

[drzewo]

(Оффтоп)

Anton_Peplov я сожалею, что влез в эту ветку и вам не советую.Надо просто понимать только одно: что EminentVictorians, что Cnupm это не профессиональные математики, а любители-самоучки. И реагировать на их общематиматические заявления, ну это смешно просто. Много чести.

[dgwuqtj]

EminentVictorians в сообщении #1649834 писал(а):

базовая операция деления - частичная (откуда, к слову, растут ноги того, что не бывает свободных полей)

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

Вас как будто правда может заинтересовать бесточечная топология, для неё интуиционистской логики достаточно и алгоритмизуемость можно прикрутить. А так и над обычным $\mathbb R$ придумали кучу пространств функций, в каждом из которых свои операции всегда определены и хорошо считаются. Скажем, $\mathrm C^\infty(\mathbb R)$ является дифференциальной алгеброй, а в пространстве обобщённых функций зато есть разрывные функции и производные всё ещё определены. Просто надо в зависимости от потребностей явно указывать пространства функций, с которыми работаете. И это даже легко формализуется. Если не нравится теоретико-множественный язык как слишком мощный — берите понравившуюся теорию типов (хоть с интуиционистской логикой, хоть с классической, хоть вообще с когерентной, хоть старших порядков).

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

[Anton_Peplov]

EminentVictorians в сообщении #1649807 писал(а):

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

И получать результаты только в том множестве математических объектов, к которым применима эта техника. Элементарные функции - хороший пример. Их можно подставлять друг в друга, можно дифференцировать, но уже интегрирование выводит нас из класса элементарных функций. Если ампутировать из матана интегрирование, кому будет нужен оставшийся обрубок? Наоборот, развитие математики идет в сторону все большего обобщения. Взять ту же общую топологию: свойства, которыми $\mathbb R^n$ обладает из коробки, теперь нужно проверять на каждом шагу. Зато какая содержательная теория получилась, показавшая, что непрерывность есть даже там, где нет расстояний.

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

[EminentVictorians]

dgwuqtj в сообщении #1649850 писал(а):

А так и над обычным $\mathbb R$ придумали кучу пространств функций, в каждом из которых свои операции всегда определены и хорошо считаются. Скажем, $\mathrm C^\infty(\mathbb R)$ является дифференциальной алгеброй

Да, но проверять принадлежность $\mathrm C^\infty(\mathbb R)$ все равно приходится руками.

dgwuqtj в сообщении #1649850 писал(а):

Просто надо в зависимости от потребностей явно указывать пространства функций, с которыми работаете.

И это мне не нравится. Хочется, чтобы был "вывод пространств" (по аналогии с выводом типов в функциональных языках программирования). Взамен я готов ограничиться примитивами языка и не иметь возмножность определять всякие канторовы лестницы.

dgwuqtj в сообщении #1649850 писал(а):

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

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

dgwuqtj в сообщении #1649850 писал(а):

Может, какую-нибудь конкретную задачу рассмотреть, а то сейчас это какое-то философствование?

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

[Anton_Peplov]

(drzewo)

drzewo в сообщении #1649848 писал(а):

EminentVictorians, что Cnupm это не профессиональные математики, а любители-самоучки

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

[mihaild]

EminentVictorians в сообщении #1649807 писал(а):

Даже банальное преобразование $\int\limits_{a}^{b} f + g = \int\limits_{a}^{b} f + \int\limits_{a}^{b} g$ работает далеко не по щелчку пальцев

Оно, как и большая часть классического анализа, работает всегда когда его можно записать. Куда уж всегдатее?

[EminentVictorians]

Anton_Peplov в сообщении #1649855 писал(а):

Элементарные функции - хороший пример. Их можно подставлять друг в друга, можно дифференцировать, но уже интегрирование выводит нас из класса элементарных функций. Если ампутировать из матана интегрирование, кому будет нужен оставшийся обрубок?

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

mihaild в сообщении #1649861 писал(а):

Оно, как и большая часть классического анализа, работает всегда когда его можно записать. Куда уж всегдатее?

Хочется чтобы проверку на корректность делал компилятор, а не руки. А в обычной версии матанализа такое невозможно.

[dgwuqtj]

EminentVictorians в сообщении #1649858 писал(а):

проверять принадлежность $\mathrm C^\infty(\mathbb R)$ все равно приходится руками.

Вы руками, по определению, проверяете существование и непрерывность всех производных у функций типа $e^{e^{-1 / x^2}}$? Обычно же пользуются прямо замкнутостью пространства функций относительно каких-то операций, ну и набором примитивов, из которых всё собирается. В исключительных случаях типа $e^{-1 / x^2}$ да, руками. А ещё можно строить функции через последовательность приближений пользуясь полнотой, это во всякой дифференциальной топологии полезно.

EminentVictorians в сообщении #1649858 писал(а):

А вообще, существуют варианты функционального анализа в теориях типов?

Есть статья Formalizing functional analysis structures in dependent type theory в открытом доступе. Этим обычно занимаются для пруфчекеров, где язык достаточно богатый (мощнее ZFC), но приходится много сил уделять аккуратным определениям. Вряд ли вещи типа интерполяции пространств $\mathrm L_p(\mathbb R)$ можно как-то магически вытащить прямо из формализма без доказательства неравенств и неканонических конструкций типа вложения всего этого в пространство измеримых функций.