HoTT вместо FOL как foundation ontology, математический псевдокод, аксиоматическая экономика

Склейка математики, онтологии (включая 4D экстенсиональную), естественных наук и computer science Наконец-то нашёл работы, которые склеивают математику, естественные (да и прочие) науки, компьютеры, онтологию (4D экстенсиональную), онтологию собственно математики (основания математики, foundational ontology) и намётки на то, как это всё развивать и почему нельзя этого делать с текущей математической классикой. Это работы уехавшего во Францию в ноябре 2022 Андрея Родина, прежде всего работа 2016 года "Venus Homotopically" (https://philomatica.org/wp-content/uploads/2013/01/vh3.pdf), а также его разбор естественнонаучной программы Воеводского "Voevodsky's Unachieved Project" https://arxiv.org/abs/2012.01150 (и вот тут слайды и видео рассказа от декабря 2022, https://philomatica.org/2022/12/univalent-foundations-and-applied-mathematics/). Там на пальцах объясняется довольно много интересных вещей: и что FOL не слишком хороша для онтологии, и как помирить геометрию с её интуицией (помним тут о неотвеченных вопросах про интеллект от Chollet, там интуиция отслеживания объекта, который спрятался за препятствием вроде как аппаратна, и это тот же вопрос, что про Утреннюю и Вечернюю звезду, рассматриваемую в Venus Homotopically"), и про важность цепочки "реальная проблема --> прикладная математика --> удобные для неё идеи чистой математики". В том числе там становится понятен стык математики, онтологии и типов из языков программирования, и проще разбираться с вопросами, на которые так и не ответили когда-то 420 участников чата про типы в языках программирования, моделирования, представления знаний и жизни (помним, что приписка "и жизни" -- это специально про физический мир написано было, чтобы не упустить), https://t.me/typeslife. Наводку на это всё дал Алекс Шкотин, который со мной сидит в попечительском совете Ontolog Forum: он кинул мне в личном письме ссылку на сайт Андрея Родина https://philomatica.org, я там ткнул в первую же презентацию -- и понял, что этого мне как раз и не хватало для ОдО2023. Началось всё с упоминания аксиоматического метода в экономике в Ontolog Forum, https://www.axiomaticeconomics.com/axioms.php (Victor Aguilar), который ещё и для деток учебник геометрии написал аксиоматический, с практическими приложениями -- и там даже нашёлся русский перевод: https://www.researchgate.net/profile/Victor-Aguilar-15/. Начало там такое: "Перед вами учебник школьного уровня, но написан он без налёта снисходительности, свойственного американским школьным учебникам. Он состоит из двух томов «Геометрия без умножения: пояса с белого по красный» и «Геометрия с умножением: синий и чёрный пояс». Наша цель познакомить учеников с логикой и риторикой, и это значит, что они научатся аргументировать свою точку зрения". Первая цель автора -- это вдохнуть новую жизнь в школьную геометрию, а вот вторая -- неожиданная, "цель — дать отпор экономистам, которые ненавидят дедуктивную логику". Ха, известный австрийский слоган про аксиоматический метод в экономике, с которым абсолютно не согласны все мейнстримщики. Экономика, говорят мейнстримщики, не математика, нет там никаких аксиом! Victor Aguilar говорит, что есть -- и их три штуки. Дальше он идёт к австрийцам, но не тут-то было: "Ludwig von Mises was not a mathematician – he actually despised us – but, in his own vague way, he made the same claim about money. Money is valued today because it had value yesterday and it had value yesterday because it had value the day before. In this way, Mises’ Regression Theorem traces the value of money back to when it had value primarily for its use. But that is as far as he got; not being a mathematician, he had no way of knowing that the distribution of people’s valuations of their first unit of the monetary unit is log-normally distributed. I went beyond Mises by recognizing that his Regression Theorem is not a theorem but an axiom and that it applies to all phenomena, not just money. When I wrote a letter of introduction to Murray Rothbard in 1993, I fully expected the Austrians to recognize that I was extending Mises’ rudimentary work and applaud me for doing so. How naïve! The Austrians have enough hatred in them to feed seven hells. To this day I am appalled by the ferocity of their attacks on me. Oderunt dum metuant!". Этот Victor Aguilar ярый защитник аксиоматического метода, и у него удивительно сочный ругательный язык. Это второе пересечение с математикой в этой истории. Почему всплыли Родин и Воеводский? А там же тоже аксиоматический метод! Онтология и гомотопическая теория типов: унифицировать всё против найти killer application В чате по типам и онтологиям мне уже накидали ещё некоторое количество работ по онтологии и гомотопической теории типов: https://ncatlab.org/schreiber/show/Modern+Physics+formalized+in+Modal+Homotopy+Type+Theory, https://ncatlab.org/schreiber/show/Some+thoughts+on+the+future+of+modal+homotopy+type+theory, https://disk.yandex.ru/i/B9RvP1YrUUEm9w. Моё представление о развитии математики, как оказалось, более-менее совпадает с представлением Воеводского (вот тут я беседовал об этом ровно 14 лет назад, в марте 2009: https://ailev.livejournal.com/668305.html и огромная дискуссия там в комментах, а потом https://ailev.livejournal.com/669463.html по поводу коммента vit_r "чем больше формализация, тем меньше люди обращают внимание на смысл". И ведь это крайне точно, замечал много раз: чем больше формализация, чем больше математики, тем мощнее решения и тем меньше вероятность доведения решений до какой-то практики. Это волновало и Воеводского, и волнует Родина, что математика не решает практических проблем и при этом подтухает. Нужна свежатинка в виде свежих научных проблем, для которых надо будет разработать новую прикладную математику, для которой нужно будет новая чистая математика, а правильные (в случае Воеводского -- так называемые унивалентные) основания математики позволят удержать всё это в рамках формальности (то есть оставят машинно вычислимым, а не интуитивно оцениваемым как в нейронных сетках). И там два варианта: либо пытаться воткнуть куда-то основания математики для переписывания старого не очень формального и разношёрстного legacy знания, или поддержать новой математикой решение новых проблем: то есть повторить ход изобретения разных исчислений по потребностям (типа как интегрирование и дифференцирование с механикой, а потом выход на поля), и только потом формализации этих новых исчислений, уж насколько это возможно (полностью вроде невозможно, Гёдель вроде как не пускает, поэтому аксиомы -- и желательно на пару уровней ниже, чем текущие "множества", что и было сделано). И да, там всё ещё и конструктивное, "понял, значит можешь сконструировать объект". Но пока отсутствует развитое распределённое представление (то есть не закрываются нейросети, распределённые онтологии -- то есть отдельные работы какие-то есть, но это "отдельные старинные работы"). Ничего, после выхода GPT-4 все бегом бросятся закрывать этот пробел, через год ждём множества работ по гомотопиям и нейросетям, а в них -- по распределённым представлениям и representation learning (https://ailev.livejournal.com/1045081.html). Что у нас с этим было раньше: крутая наука, но никаких killer application С доведением до практики, конечно, в этом направлении всё плохо: обычная проблема каких-то "оснований", когда с ними знакомо очень мало людей. А людей знакомо мало, ибо основная аксиома во всём этом -- аксиома унивалентности сформулирована в 2006-2007 годах. Это всего 16 лет назад, и вообще чудо, что про эту работу знает уже довольно много людей. Ну, и как всегда в стартапах: "это гипотеза, что весь этот матаппарат будет хоть как-то полезен, сэкономит время, даст невиданные результаты. Поглядим, что там будет killer application". Ибо когда мне говорят, что "доказательство правильности компьютерных программ", я только улыбаюсь. Когда получился математический результат с обучением глубокой нейронной сетки, на уши встал весь мир, весь мир начал бодро учить эту математику, а затем и ни разу не математики вдруг стали "экспертами в GPT" (после того, как их услуги как экспертов в климатологии, вирусологии и политологии перестали быть нужными). Вот тут с этими типами требуется что-то похожее: что-то должно стать существенно быстрее, дешевле, проще (но уж никак не дольше, дороже, сложнее). С этим пока проблемы. Интересно, что мы пробовали уже десяток лет назад рассматривать теорию категорий как язык для выражения онтологии, но не срослось: не было ни одного ответа на вопрос, чем же это поможет по сравнению с текущим выражением на FOL. Языка, на котором эти вопросы обсуждать, не было. Теория типов даёт машинку "исчисления" (вычислений) как синтаксис, а теория категорий придаёт смысл теории типов -- что и для чего вычислять, https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory, там дуализм синтаксиса и семантики). До этого мы не трогали теорию типов, пробовали теорию категорий в чистом виде, обсуждали семантику, но никакого "исчисления" не затрагивали. Как мы говорили, "в этих учебниках теории категорий сплошные страницы самых разных определений самых разных объектов, но что потом с ними делать, когда просто всё определил как категории?!". Ну, что делают с исчислениями? Вычисляют! Вот это как раз не рассматривалось. Ход Воеводского тут -- можно записать на хитромудром языке вроде Coq и Agda, и посчитать. Вот типичный пост того времени (2014, https://ailev.livejournal.com/1154791.html): "Главный вопрос тут, конечно -- "зачем" все эти теоркатегорные мэппинги между разными дисциплинами математики и инженерии. Есть ли что-нибудь такое, что раньше нельзя было посчитать, а сегодня посчитали? Похоже, ничего такого нет -- новых расчётов или повышения точности для старых расчётов не предложено (или я плохо читал?). Считать, что экономится человеческое знание, тоже нельзя: всё это "похожее" редко приходится рассматривать одним и тем же людям -- разные инженеры делают разные расчёты. Хотя я не знаю, как бы выглядело разделение труда, если бы стало понятно, что "разные расчёты" и "разные диаграммы" вдруг являются вариантами одного и того же расчёта, одной и той же диаграммы. Ну, и при таком подходе можно формально проверить: достаточно ли полна модель данных для выражения тех или иных инженерных диаграмм, достаточно ли данных для тех или иных солверов, достаточно ли алгоритмов для тех или иных солверов", и дальше в этом посту целый план работ -- как попасть в инженерный рай с помощью теории категорий. Но за десять лет никакого рая не случилось, зато появились нейронные сетки ещё в 2012 году, и сейчас GPT-4, и вся инженерия в этом плане будет как-то вместо формализмов внимательно глядеть в сторону этих нейросеток (а потом всё равно вернётся к формализмам, ибо эти нейросетки -- это ж всё равно как инженеры, а к инженерам нужно приложить расчёты на хотя бы логарифмической линейке, а не просто оценки в уме, хотя бы и с сухой нейронной сеткой). Ещё один ход тут на "онтологию всего", который идёт по линии active inference и работам Chris Fields и Glazebrook. Там всё базируется на выражении в пространствах Чу, это тоже шаги в направлении теории категорий, но теории типов там пока особо нет. И дотянуть тамошнюю математику до практики пока непонятно как. Чему учить в математике (написано в соавторстве с GPT-4) В предыдущих текстах мне помогла разобраться GPT-4. GPT-3.5 показала себя боле-менее бесполезной, а вот GPT-4 уже сэкономила пару дней: я задавал ей вопросы про гомотопические уровни, и она даже сортировала мне объекты по этим уровням. Удался следующий ход: взял список "важных объектов, которые придумали математики в последние годы, но которые почти не используются в естественных науках", это из статей Воеводского -- categories, sheaves, cohomology, simplicial sets. Затем я понял, что одна из главных идей -- это вместо "логик разных порядков" иметь "гомотопические уровни" объектов разных типов. Попросил рассортировать categories, sheaves, cohomology, simplicial sets по этим уровням. А потом попросил дополнить этот рассортированный список объектов другими важными объектами (уж какие GPT-4 сочла важными). Итог вот (и мне в чате по типам-онтологиям подсказали, ещё куда ставить разные порядки -- все эти кардинализмы-ординализмы для экономики -- я их туда поставил по-русски руками, но всё остальное порождено GPT-4 и я это не трогал): 1. h-level 0 (contractible types): - Point: A single point is a contractible space, as it can be continuously deformed into itself. 2. h-level 1 (propositions): - Cohomology: Cohomology theories usually involve abelian groups or modules, which are sets, but the actual cohomology groups can be seen as propositions when considering them up to isomorphism. - Equivalence relations: An equivalence relation on a set partitions the set into disjoint subsets, and can be seen as a proposition about the elements of the set. - Equations: Mathematical statements that assert the equality of two expressions can be seen as propositions. - вся теория порядков - предпорядки, решетки, соответствия Галуа и тд 3. h-level 2 (sets, и тут вычислимость, объекты стали различимы): - Chu spaces: A Chu space is a set-theoretic structure consisting of a set of states, a set of events, and a satisfaction relation between them. - Categories: A category consists of a set of objects and a set of morphisms, along with composition and identity operations satisfying certain axioms. - Simplicial sets: A simplicial set is a functor from the simplex category to the category of sets. The category of sets is an h-level 2 object, so simplicial sets can be considered at this level. - Topological spaces: A topological space is a set of points, along with a collection of open sets satisfying certain axioms. - Groups: A group is a set with a binary operation satisfying certain axioms, such as associativity, identity, and inverses. - Functions: A function is a relation between a set of inputs and a set of possible outputs with the property that each input is related to exactly one output. - Matrices: A matrix is a rectangular array of numbers, symbols, or expressions, arranged in rows and columns. - Vectors: A vector is an element of a vector space, which is a set of objects that can be added together and multiplied by scalars. - Sequences and Series: A sequence is an ordered list of elements, while a series is the sum of the terms of a sequence. - Graphs: A graph is a mathematical structure consisting of a set of vertices and a set of edges connecting pairs of vertices. - Probability Distributions: A probability distribution is a function that describes the likelihood of obtaining the possible values of a random variable. 4. h-level 3 (groupoids): - Sheaves: A sheaf is a functor from a category (usually a topological space or a site) to the category of sets or groupoids, satisfying certain axioms. Since groupoids are at h-level 3, sheaves taking values in groupoids can be considered at this level. - Lie groups: A Lie group is a group that is also a smooth manifold, with the group operations being smooth maps. Since groups are h-level 2 objects and manifolds are h-level 3 objects, Lie groups can be considered at this level. - Fractals: A fractal is a complex geometric shape that exhibits self-similarity and has a non-integer dimension. Fractals can be considered at h-level 3 as they often involve groupoid structures. Что мы с этим будем делать? Мы поправим наши курсы, учтём SoTA математику для нашей мета-мета-модели понятий из трансдисциплин Проблема в том, что переформулирование онтологии предметной области в терминах теории типов и теории категорий как объектов с хорошо изученным поведением -- это тяжкий труд. Но что потом можно будет сделать легче, или вообще сделать? Ответы обычно не слишком внятны. Работы по первым ссылкам в этом посте дают намёки, что становится проще понимать и объяснять. Мой ход пока: в учебных программах мы используем эти материалы как поправки к нашей мета-мета-модели. Это неформальная онтология, которая позволяет точнее и быстрее думать (но не вычислять формально). Мы давно уже поняли, что проблема не столько в отсутствии формальности в мышлении, сколько в плохих объектах для мышления на среднем уровне формальности. Вот это изложение мы и хотим сделать. Тут надо будет ещё поглядеть на материалы по неформальной теории типов: https://planetmath.org/informaltypetheory, и там в том числе такие тексты, как "свобода от логики", https://golem.ph.utexas.edu/category/2012/11/freedom_from_logic.html, traditional mathematics is usually written in natural language (with some additional helpful symbols), but in a way that all mathematicians can nevertheless recognize as “sufficiently rigorous” — and it’s generally understood that anyone willing to undertake the tedium could fully formalize it in a formal system like material set theory, structural set theory, or extensional type theory. By analogy, therefore, we would like an “informal” way to write mathematics in natural language which we can all agree could be fully formalized in homotopy type theory, by anyone willing to undertake the tedium. При этом даже не обсуждается, зачем нужно формализовывать "до дна": нужно, и всё тут. Но признаётся, что это только если очень-очень надо! Нормальные люди работают на уровне псевдокода! Вообще, мы поставили задачу массовой постановки онтологического мышления где-то в 2010-2013 (когда поняли, что никакой инженерии без этого, никакого системного мышления). Решили с тех пор довольно много проблем, и продолжаем решать до сих пор (скажем, курсы онтологики и собранности мы объединили сейчас — там общая программа, ибо не удерживают длинные рассуждения, не умеют записывать модели, надо этому специально учить). Вопрос, можем ли мы поднять качество мышления, если перетолкуем онтологию на гомотопии. С одной стороны — геометрические интуиции пространств, путей (траекторий), типизация вроде как вся остаётся (хотя её нужно будет перетолковывать). С другой — непонятно, насколько это поможет в мышлении "вот прямо сейчас" (и с учётом того, что у нас уже есть GPT-4, которая поможет в мышлении с "классикой", там же куча наработанного legacy). У меня такое впечатление, что если впрямую научить рассуждать про всё вот это про обычный мир вокруг (там где-то 70 понятий обычно бывает в таких ситуациях), то это будет самое то. Мы научились делать это с классическими онтологиями, и это существенно добавляет к мозгам студентов. А дальше там развилка: чистая философия как у Kit Fine (вот вам объекты, думайте в этих терминах) или таки просматривается выход на цифирьки и возможность "посчитать", как у физиков и прочих естественнонаучников (вот вам объекты, думайте в этих терминах, результаты в мире можно померять и сравнить с результатами размышлений). Так что пишу некоторый текст в ОдО2023 (грубо говоря, переписываю этот десяток страниц текущего поста -- он длинный, десять страниц книжки A5), а затем мы начинаем потихоньку вносить изменения в наши учебные программы. Тут можно дальше много чего писать, но мне надо срочно закончить раздел по математике и переходить уже к физике. Итого из интересного: -- HoTT вместо FOL как foundation ontology как классической онтологии "объектов и отношений", так и математики как онтологии физики и естественных наук -- обсуждение "среднего уровня формальности" (informal type theory), то есть ходы на деформализацию, изучение псевдокодов -- ходы к аксиоматической экономике Картинка Stable Diffusion 2.1 от you.com -- Math teacher in a garden of math symbols. Picture in colorful art nouveau style.