2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу 1, 2  След.
 
 Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 19:25 


22/10/20
1185
Меня довольно сильно напрягают те части математики, в которых чтобы сделать какое-то преобразование, нужно проверить 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$. Я сомневаюсь, что подойдет какое-то топорное решение типа вычислимых чисел - это было бы довольно грустно. Хочется, чтобы числовая система была сильно интереснее: можно, например, пожертвовать существованием или алгоритмическим определением нуля (а иметь вместо него "монаду" околонулевых чисел). Вероятно, операции с числами должны быть всюду определенными или по крайней мере с алгоритмической разрешимостью (чтобы компилятор бил по рукам, если пытаешься сделать запрещенную операцию). Можно пожертвовать неограниченностью чисел.

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

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 19:48 
Заслуженный участник


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

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 20:05 


26/07/24

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

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 20:54 


22/10/20
1185
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), но я пока не очень понял, о чем там речь.

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 21:03 
Заслуженный участник
Аватара пользователя


20/08/14
8484
EminentVictorians в сообщении #1649807 писал(а):
можно, например, пожертвовать существованием или алгоритмическим определением нуля
Вам не нравится ноль, потому что результат операции $a/0$ не определен. Если Вы выбросите ноль, как будет определен результат операции $a-a$?

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 21:06 


21/12/16
721
EminentVictorians в сообщении #1649807 писал(а):
Меня довольно сильно напрягают те части математики, в которых чтобы сделать какое-то преобразование, нужно проверить 10 разных условий.

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

-- 13.08.2024, 22:08 --

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

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

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 21:12 


22/10/20
1185
Anton_Peplov в сообщении #1649839 писал(а):
Если Вы выбросите ноль, как будет определен результат операции $a-a$?
Операция разности не обязана быть однозначной, вместо нуля может быть монада околонулевых чисел. Или, например, разность двух одинаковых чисел писать можно, но считать нельзя (ну, гипотетически, если у нас это все происходит в языке с ленивой (или похожей на ленивую) моделью вычислений, который $a-a$ вычислять не будет, но Вы так писать можете; просто эта разность будет не числом, а "синтаксическим сахаром"). Мне сложно вот так сходу накидать вариантов, потому что хотелось бы посмотреть на уже существующие теории.

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 21:28 


21/12/16
721

(Оффтоп)

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

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 21:31 
Заслуженный участник


07/08/23
1055
EminentVictorians в сообщении #1649834 писал(а):
базовая операция деления - частичная (откуда, к слову, растут ноги того, что не бывает свободных полей)

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

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

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

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 21:45 
Заслуженный участник
Аватара пользователя


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

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

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 21:55 


22/10/20
1185
dgwuqtj в сообщении #1649850 писал(а):
А так и над обычным $\mathbb R$ придумали кучу пространств функций, в каждом из которых свои операции всегда определены и хорошо считаются. Скажем, $\mathrm C^\infty(\mathbb R)$ является дифференциальной алгеброй
Да, но проверять принадлежность $\mathrm C^\infty(\mathbb R)$ все равно приходится руками.

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

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

dgwuqtj в сообщении #1649850 писал(а):
Может, какую-нибудь конкретную задачу рассмотреть, а то сейчас это какое-то философствование?
Я хочу в первую очередь развитую теорию. Не люблю решать задачи, пока нету в распоряжении хорошей теории.

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 22:05 
Заслуженный участник
Аватара пользователя


20/08/14
8484

(drzewo)

drzewo в сообщении #1649848 писал(а):
EminentVictorians, что Cnupm это не профессиональные математики, а любители-самоучки
Так и я любитель-самоучка. Мне перед ними гордиться нечем. Мои мысли о путях развития математики - точно такой же дилетантский треп.
У меня, конечно, нет юношеских мечтаний взять да и реформировать всю математику, потому что она-де неправильно устроена. Если кто и придумает, как глобально улучшить математику, то точно не я. Ну так и юность моя давно позади. "Кто в юности не был революционером..."

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 22:06 
Заслуженный участник
Аватара пользователя


16/07/14
9090
Цюрих
EminentVictorians в сообщении #1649807 писал(а):
Даже банальное преобразование $\int\limits_{a}^{b} f + g = \int\limits_{a}^{b} f + \int\limits_{a}^{b} g$ работает далеко не по щелчку пальцев
Оно, как и большая часть классического анализа, работает всегда когда его можно записать. Куда уж всегдатее?

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 22:13 


22/10/20
1185
Anton_Peplov в сообщении #1649855 писал(а):
Элементарные функции - хороший пример. Их можно подставлять друг в друга, можно дифференцировать, но уже интегрирование выводит нас из класса элементарных функций. Если ампутировать из матана интегрирование, кому будет нужен оставшийся обрубок?
Да я просто ради иллюстрации идеи привел эти элементарные функции. Разумеется, должна быть гораздо более широкая поляна с многими классами функций (но не такая широкая, как в обычном теоретико-множественном матане).

mihaild в сообщении #1649861 писал(а):
Оно, как и большая часть классического анализа, работает всегда когда его можно записать. Куда уж всегдатее?
Хочется чтобы проверку на корректность делал компилятор, а не руки. А в обычной версии матанализа такое невозможно.

 Профиль  
                  
 
 Re: Потеряем общность, но получим легкость преобразований
Сообщение13.08.2024, 22:14 
Заслуженный участник


07/08/23
1055
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)$ можно как-то магически вытащить прямо из формализма без доказательства неравенств и неканонических конструкций типа вложения всего этого в пространство измеримых функций.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 28 ]  На страницу 1, 2  След.

Модератор: Модераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group