Комментарии 331
А я в меру своего скромного ума, понял, что теория категорий - это следующий уровень абстракции над теорией множеств.
Как думаете, есть ли смысл в ней разобраться (как она в coq формализуется) и через нее работать? Т.е. выводить теорию множеств из теории категорий, а теорию категорий из теории типов?
Я еще видел учебник "An Invitation to Applied Category Theory. Seven Sketches in Compositionality", вроде неплохое введение
Не знаю. Я - не разобрался. Как уже сказал, в силу своего скромного ума, я так понял, что она нужна математикам для выведения теорем, которые потом используются в теории множеств и иже с ней. А для прямого практического применения - не уверен.
Я, конечно, математику люблю, но я - не профессиональный математик, и тратить много времени на настолько высокие абстракции - не готов.
есть ли смысл
Не очень применимый к чистой математике вопрос. Лучше спрашивать «весело ли это» и «что получится».
В прикладных задачах ничего особо интересного не получится. Весело ли это? Кому как.
Т.е. выводить теорию множеств из теории категорий
Сделано в ETCS. Полезна тем, что можно обобщать над аксиоматикой теории множеств.
а теорию категорий из теории типов?
Я бы не стал, получится неудобная и неизящная конструкция.
Да, у нас есть системы типов, и есть классы категорий, реализующие внутреннюю логику этих систем типов, но формулировать эти вещи лучше по отдельности и строить соответствие пропозиционально, а не дефиниционально, так сказать.
Не очень применимый к чистой математике вопрос.
Почему? Многие разделы чистой математики вполне себе имеют практическую пользу в обучении и могут сильно помочь в глубоком понимании прикладной математики и ее практическом применении. Нужно смотреть шире, у нас всегда много неявных (неочевидных) связей.
Про ETCS интересно, спасибо.
Я бы не стал, получится неудобная и неизящная конструкция.
А как мы ее тогда в теорем-прувере формализовать будем?
Почему? Многие разделы чистой математики вполне себе имеют практическую пользу в обучении и могут сильно помочь в глубоком понимании прикладной математики и ее практическом применении. Нужно смотреть шире, у нас всегда много неявных (неочевидных) связей.
Если вкратце, то потому что чистые математики редко этим руководствуются, и польза вне самой чистой математики оказывается скорее случайным побочным эффектом, чем результатом целенаправленной работы.
А как мы ее тогда в теорем-прувере формализовать будем?
Как обычно и как любую другую теорию, просто используя прувер как метаязык.
∃b. ∀x. ((x ∈ b) ⇔ (x = a ∨ x = b ∨ x = c)))
А это правильно что используется одна и та же буква 'b' и для множества и для одного из его элементов?
> Натуральная Дедукция.
Естественный вывод.
Martin-Löf type theory (MLTT) и Calculus of Construction (CoC)
Он всё таки различаются. К примеру, MLTT предикативна (вроде бы?). А в CoC (в смысле Coq) есть импредикативный Prop. На сколько я понимаю раньше и Set был импредикативен.
По поводу "натуральной дедукции" - кажется, что вы правы, но возникают проблемы, если копнуть глубже. Например, если мы переведем дедукцию как "вывод", то надо будет переводить и индукцию как "ввод", но в русском языке уже принятно слово "индукция" везде. А если мы переведем "натуральный" как "ествественный", то нужно и натуральные числа переводить как "естественные числа", но так не принято в русском языке. Итог - возникают противоречия.
Про импредикативность Coq вы все правильно написали. Да, MLTT предикативна, а CoC и Coq - как правило, нет (но есть чит-опция). Какие это имеет последствия - я пока не ощутил.
> По поводу "натуральной дедукции" - кажется, что вы правы, но возникают проблемы, если копнуть глубже. Например, если мы переведем дедукцию как "вывод", то надо будет переводить и индукцию как "ввод", но в русском языке уже принятно слово "индукция" везде. А если мы переведем "натуральный" как "ествественный", то нужно и натуральные числа переводить как "естественные числа", но так не принято в русском языке. Итог - возникают противоречия.
В целом вы правы. Но по неправильной причине :). Не то что бы дело в противоречиях. Дело в принятых терминах. Я человек к логике отношение имеющий постольку поскольку и думал что верный термин "естественный вывод". И он верный. Но "натуральная дедукция" тоже легко гуглится и по всей видимости это вполне устоявшийся термин. Ещё встретил "Натуральный вывод".
Так что я поторопился с поправкой.
Coq - как правило, нет (но есть чит-опция)
Coq имеет предикативную систему для Type и импредикативную для Prop. (Ещё можно сделать Set импредикативным с помощью опции).
Насчёт чит-опции я не в курсе, поясните, пожалуйста.
В целом очень интересный обзор (и личная история успеха). Просмотрел пока, думаю вернусь к чтению, любопытно побольше узнать про опыт, похожий на собственный (лет 6 назад).
Приятно видеть, что есть люди, видящие настоящую красоту математики.
Сразу скажу, что у меня только общие представления. Насчёт теории категорий, то насколько я знаю это удел алгебры. Т.е. в категориях акцент ставится именно на изучение операций между объектами, а не самими объектами (складывать можно и матрицы и числа - значит фундаментальнее рассматривать сложение, а не разные объекты).
По поводу ZFC, то мне как-то не верится, что она может вывести аксиомы геометрии Гильберта, топологии и теории чисел. Если из нее можно выразить алгебру, матанализ, логику, теорвер, то это и вправду фундаментальная вещь (правда, если она выражает арифметику/ аксиомы Пеано (она тьюринг-полна), то проблема остановки и теорема о неполноте (почему Вы ее как-то обделили) говорят, что не выйдет построить машину выводящую все теоремы. Это можно будет сделать только для довольно маломощных систем аксиом (например евклидова геометрия)).
Кстати кто-то даже пытался свести все аксиомы математики в одну универсальную (тут).
По поводу ZFC, то мне как-то не верится, что она может вывести аксиомы геометрии Гильберта, топологии и теории чисел
Вот я тоже не верил, что аксиомы Пиано на натуральных числах можно вывести, а потом взял и вывел (по учебнику). Мне кажется, что теория чисел должна очень даже хорошо и чисто формализоваться, т.к. нам осталось вывести множество Z и это хорошо решаемая задача, когда представляем каждое число в виде класса из пар двух натуральных чисел (a, b).
По поводу топологии и геометрии Гильберта, я поговорил с ChatGPT, он утверждает, что классическая часть этих областей без проблем выводиться из ZFC, а глубокие штуки на стыке с теорией множеств, связанные с гипотезой континуума или большими кардинальностями - нет. Собственно, что и следовало ожидать.
https://chatgpt.com/share/6775381f-9424-800e-b161-938164dde4d9
я поговорил с ChatGPT
А с помощью чего Вы валидировали его ответ?
А никак не валидировал, принял на веру =). Если кто-то глубоко шарит в топологии или геометрии Гильберта, просьба прокомментировать.
Но по теории чисел - я зуб даю, что прокатит ее очень чисто формализовать
Вы когда-нибудь пробовали поговорить с ним, например, о генеалогии монархов Европы? Или о художественной литературе?
ГПТ может запросто написать неправду. В смысле 100%-ый вымысел. Поэтому его обязательно нужно валидировать.
А никак не валидировал, принял на веру =).
Ну как-то это дико после всех рассказов про доказанные выводы, аксиоматику и пр.
Нашел перевод одной из упомянутых книг
Посмотрел. Да, перевод есть, но он 7-ми летней давности (книга много обновлялась) и не все главы переведены, например IndPrinciples.v только заголовки переведены. Впрочем, это не проблема - можно скормить эти исходники какому-нибудь переводчику и он должен легко справиться с переводом, так как исходники книги - доступны
Строгая типизация (с нормальной системой типов) заменяет юнит тесты и эта замена равносильна 100% покрытию. Если вы тесты не писали то разница будет не так очевидна.
Вы же видите что я про юнит тесты говорю - зачем вы мне интеграционные в пример приводите?
Ну если для Вас это не работает - не пользуйтесь, какие проблемы?
А во-вторых, далеко не все функции сводятся к чистым (моё эмпирическое мнение - не более 1% в реальном мире)
Это просто вы так пишете код, что у вас нечистота и общение с внешним миром лежат там же, где и бизнес-логика. Не надо так делать. Надо выделять получение и отправку данных во внешний мир отдельно (м… м… мон…) и рассматривать получившуюся чистую функцию.
Ну либо решаемые задачи — «принять жсон отсюда и переложить как есть туда». Не знаю, что в таком случае тестировать или обкладывать типами (хотя параметризм мог бы помочь).
Тест для функции, сохраняющей данные в файл
Эта функия называется Data.ByteString.Lazy.writeFile. Что вы там тестировать собрались? Она уже протестирована авторами библиотеки bytestring.
Ну и по предыдущему комментарию:
Я просил, чтобы мне показали http-сервер без тестов, но мне не показали.
Когда-то давно писал тестовым заданием на прикладного хаскелиста маленькую http api-шку, которая получает картинку, распознает там объекты и складывает в БД (а потом возвращает обратно, если что).
Сервер — поверх servant. Там (в самом сервере) просто нечего было тестировать, все типами описано и компилятором проверяется.
А тесты были только уровня интеграционных и только для «бизнес-логики», которая вполне себе реализуется чистыми функциями, и которую так писать даже удобнее, опять же. В более выразительном языке и это можно было бы покрыть типами.
Это просто вы так пишете код, что у вас нечистота и общение с внешним миром лежат там же, где и бизнес-логика. Не надо так делать. Надо выделять получение и отправку данных во внешний мир отдельно (м… м… мон…) и рассматривать получившуюся чистую функцию.
Бешено плюсую
Начал сильно обращать на это внимание только после работы с системами типа Temporal/Azure Durable Function где фреймворк форсит тебя разделять decision-making и грязные дествия.
Мысль кажется очевидной когда осознаешь её, но как же в обычных языках типа C#/Java блин проще не задумываясь, в потоке, написать всё в одном классе, максимум в приватные функции выделив обращение во внешний мир. И получить непокрываемую юнит-тестами логику :(
Выносить сайд-эффекты в отдельный класс, прятать за интерфесом, чтобы в тестах замокать. Ещё придумывать какие типы будут в интерфейсе, тупо брать модели из используемого клиента внешнего сервиса из реальной имплементации или создавать отдельные модели и делать конвертацию между ними. Оно в целом недолго делается, но ментально это настолько больше шагов что порой проще сказать "да интеграционными тестаи проверится за компанию". Может есть какой-то более простой рецепт как всё это разделять, который я не вижу?
Бизнес-логика часто максимально тривиальная, типа
votes[voteId]++;
Тесты на это делать как-то смешно.
А всё остальное - обвесы с эффектами: чтение из хранилища, запись в хранилище, синхронизация между потоками, сериализация/десериализация.
Если в бизнес-логику начинает вклиниваться какой-то нетривиальный алгоритм, типа вычисления необычной контрольной суммы, или поиска кратчайшего пути, его надо выносить в библиотеку и её покрывать тестами.
блин проще не задумываясь, в потоке, написать всё в одном классе
Так делать точно не нужно. Это будет страшный спагетти-код. Помимо простого деления на бизнес логику и работу с вводом\выводом, есть еще и другие слои, например работу с БД принято выносить в DAO-классы. Интеграции с внешними системами - тоже в отдельные классы и отдельные пакеты. Иногда даже в отдельные библиотеки. А еще, принято использовать паттерны проектирования, и они, как правило, тоже выносятся в отдельные классы
Не, я имел в виду "всё" одного уровня абстракции. Ну то есть условно код, который по бизнес-логике должен составить запросы в сервис1 и сервис2 и по данным от них либо вызвать одно действие в сервисе3 либо ещё забрать данные из сервиса4 и уже с ними вызвать сервис3.
Клиенты к сервисам естественно отдельные классы/модули. Иногда это можно разделить так, что вначале сделать все внешние запросы и потом вызвать чистую логику принятия решения что отправлять в сервис3. Но если вызов в сервис4 дорогой, то его надо делать только если действительно нужно. А определение нужности уже часть бизнес-логики. И тут либо мокать клиенты к сервисам, получая связанность теста с конкретными деталями взаимодейтсвия с сервисами и меняя его если бизнес логика какой-нибудь FindById сменит на вызов FindByUsername. Либо абстрагировать всех клиентов за специальным интерфейсом созданным специально для этой части бизнес-логики. Тогда бизнес логика вызывает только этот специальный интерфейс, который можно замокать в тестах и изменения лишь особенностей взаимодействия с внешним миром (поменять имплементацию interface.FindUser c client1.FindById на client1.FindByUsername) не приведет к изменениям тестов.
Но пилить отдельный интерфейс для каждого workflow такого вида - выглядит громоздко
Можете, пожалуйста, на каком-нибудь маленьком конкретном примере показать, что имеется в виду. Три раза перечитал, не могу понять
Аргументы по существу кончились (вернее, их и не было изначально), и пошёл спердоб/адхом? Ну как хотите.
это не я живу в нечистом мире, это Вы пытаетесь от него абстрагироваться
Да, потому что, ещё раз, тогда проще и разрабатывать, и тестировать, и рассуждать о коде. Это (более частными терминами и с большими костылями) пишут в каждой первой книжке по архитектуре ПО — dependency injection, SRP, какая-нибудь там гексагональная архитектура, и прочая ерунда.
Короче, не вижу в этом ничего плохого. А вот так патологически бороться за говнокодинг, как вы это делаете — это я не очень понимаю. Зачем так делать?
вот тем, к чему я руку приложил, вы точно скорее всего пользовались: яндекс. такси, яндекс.лавка.
А, понятно, зачем. Просто вы — из того сорта яндексистов, которые наслаждаются своей элитарностью, которая им даруется местом, где они просиживают штаны и говнокодят (ведь они же прошли все литкод-интервью в Яшечку!). Притом, что говнокодинг в Яндексе — это тоже притча во языцех (фокус на литкодинге к другим результатам и не приводит). Я бы не хотел идти работать в Яндекс.
И нет, не пользовался ни одним из них.
но там вообще и запаха типов и иммутабельности нет, уж извините.
Здесь мы обсуждаем чистоту. И расчёт путей и цен — не чистая задача? Поиск ближайших таксистов и соотнесение их с заказчиками — не чистая задача?
а что сделали Вы?
Ничего, конечно же. Я ж только языком трепать могу, сорьки, куда мне до Маэстро Литкода.
я просил аргументов, а что получил?
Нет, вы не просили аргументов. Вы сказали, что ваше эмпирическое мнение — что всего лишь 1% функций чистые. На это я ответил, что либо вы неправильно декомпозируете задачу, либо просто у вас такие задачи, где бизнес-логики толком нет, а есть только перекладывание жсонов.
В ответ на это можно было бы рассказать, например, подробности про решаемые задачи, а вы зачем-то стали пускать пыль в глаза про Яндекс.Лавку.Такси.Алису.
высокомерное
Лол, с такой чувствительностью к критике картина становится всё более цельной.
знаете, как, например, появилась Яндекс-лавка?
Не знаю и не очень интересно, потому что дальше снова какое-то непроверяемое пускание пыли в глаза, которое вообще не имеет никакого отношения к долгосрочной поддерживаемости кода (как вам расскажет любой эффективный менеджер, срезающий косты и рапортующий об успехах, а после него — хоть потоп).
а сейчас в лавке НЕговнокодит уже около 100 человек. Но клиент не видит результатов их труда, увы
Подчищают за вами, видимо.
У меня тоже такой пример перед глазами есть. Был на одной моей работе чувак, и начал он разрабатывать одну, скажем, фичу. Пре-MVP выкатился очень быстро, потому что чувак максимально срезал углы. Про это написали в анонсе новой версии, бизнес пипл что-то там оценили, что это привлекло 100500 новых клиентов и денег и вызвало энтузиазм, и все радостно получили бонусы.
Проблема в том, что чувак срезал углы. Поддерживать и развивать эту кодовую базу за пределами пре-MVP было очень больно: добавляешь что-то в одном месте, так в другом разваливается. С этого проекта за моё время там ушло трое других людей потому, что над ним невозможно работать, не удалось найти никого другого, кто хотел бы им заниматься, бизнес пипл пришлось всё время придумывать, почему обещанные фичи не реализуются, исходный чувак с бонусом и красивой строчкой резюме упорхал в следующую компанию, а исходные менеджеры, выписавшие ему и себе бонусы, тоже куда-то там упорхали.
Но да, в глазах общественности чувак молодец и гений, а все остальные — туповатые лентяи, раз ничего не могут после него сделать.
прибыли, понимаете, похрен: говнокод там или нет
Ещё выгоднее веществами барыжить или там, не знаю, pump & dump на шиткоинах. Может, ну его нафиг это программирование?
но если интересны подробности, то в такси был большой картографический блок (с нуля написанный) плюс система сбора/хранения координат/треков водителей, при том, что по ней нужно быстро искать понятие "ближайший".
Звучит как чистые функции.
Некоторым боком там была задача комивояжёра.
И это тоже.
которую мы решали методом "х-к х-к и в продакшен"
Не ожидал другого.
Знаете какой самый козырный и самый масштабируемый способ её решать? Если конечно плевать на перфекционизм? И, главное, не лезть во всякие градиентные спуски и прочую псевдоматематическую ненужность.
Да конечно не нужно. Это всё вообще никогда не нужно.
Я недавно форму заполнял на 6 экранов и примерно сотню полей суммарно, и к концу её валидация занимала минуты две при каждом изменении формы. Почему? Потому, что литкод-маэстро нечистых функций, её писавшие, тоже сделяли х-к х-к и в продакшен, и в итоге у них там алгоритм Шлемиеля, ведущий к тому, что первое поле проверяется при проверке первого, второго и последующих, второе — при проверке второго и последующих, и так далее, и в итоге O(n²) на ровном месте. И на каждое поле они отправляли запрос на сервер и обратно.
Зачем? Почему? Потому, что на их игрушечных данных всё работало, можно релизить MVP!
точно-точно! переписывают на микросервисы
Какое отношение микросервисы имеют к обсуждаемому вопросу?
Покрытие тестами около 80%.
До сих пор не понимаю, зачем тесты писать. Только замедляют работу :shrug:
почему так? а потому что чтобы упростить код, писатели "на чистых функциях" стоят перед развилкой: либо написать независимый чекер к каждому элементу, либо тупо пересчитывать весь список целиком.
С чего это? Не упрощает это код и нет такой необхоидмости.
затем на её изменение сработал триггер из чистой функции и пересчитал DOM-дерево вашего браузера. Целиком.
Нет, это не на изменение. Это на нажатие специальной кнопочки «check for errors».
А, я понял! У вас типизация и разделение обязанностей просто ответственны за все смертные грехи. На улице гололёд — тоже хаскелисты виноваты полюбас.
Какой то умник который сказал что goto плохо - на секунду Дейкстра, и такие же альтернативно одаренные как и вы его пытались за это втоптать, но нифига не вышло. Он свою позицию доказал и этот подход прошел проверку временем и развил программирование как дисциплину управления сложностью. Я обычно стараюсь выбирать выражения, но в этом случае - вы выглядите крайне жалко в своих потугах.
goto - это настолько плохо, что даже на уровне самих языков программирования его не стали добавлять. В Java его нет, например. Есть только очень узкий случай break LABEL; для выхода из многомерного цикла и все.
А в Lua - есть, причём у метки блочная область видимости, что исключает все недостатки goto.
Хотя, справедливости ради, я ни разу не писал ничего с использованием goto. Как-то не требовалось...
Вы правы. Дело в том, что я JavaScript-ер, и даже парсеры со стейт-машинами мне приходилось писать без goto. А на других языках пэт-проекты с парсерами мне писать пока что не случалось.
Ну, это вряд ли. Я в пэт-проектах использую и парсеры и стейт-машины, почитай, лет пятнадцать. Просто, мне приходится для этого гемороиться с циклом и ветвлением по номеру состояния.
И, конечно, я прекрасно представляю, как бы я написал это, будь у меня goto.
Я в пэт-проектах использую и парсеры и стейт-машины, почитай, лет пятнадцать. Просто, мне приходится для этого гемороиться с циклом и ветвлением по номеру состояния.
А могли бы взять комбинаторы для парсеров, и не пришлось бы геморроиться.
Причём тут комбинаторы? Мы же про более низкий уровень реализации.
Не понимаю, как «использую парсеры» означает «более низкий уровень реализации [чем библиотека комбинаторов]».
Это было сказано в контексте РАЗРАБОТКИ парсеров. Читать надо ветку, а не последний комментарий.
Это уже терминология какая-то.
Когда я пишу
parseFloat = do
sign <- fromMaybe Positive <$> optional (char '-' $> Negative)
intPart <- digits
fracPart <- optional $ char '.' >> digits
expPart <- optional $ char 'e' >> digits
pure $ makeFloat sign intPart fracPart expPart
where
digits = some digitто я разрабатываю парсер в ваших терминах?
Я писал эффективные стейтмашины и парсеры. goto в целевом коде всё ещё не нужен. Для парсеров у меня есть attoparsec (которого хватает для 99% задач), для стейтмашин обычный простой код на data State = Foo SomeFooData | Bar SomeOtherData | Baz YouGotItMoreData тоже в 99% задач даёт более чем достаточную эффективность. В 1% задач, когда этого не хватает, я сажусь и пишу DSL с кодогенерацией, а не обмазываю логику goto .
Эффективное зависимое выделение/освобождение — это оксюморон, потому что сам процесс выделения/освобождения на порядки больше любой экономии на подобных вещах.
а не обмазываю логику
goto.
Это Вы что-то странное написали. Вы вообще представляете, как выглядит код стейт-машины на goto? Изящнее, разве что, голая таблица переходов.
Ассемблерный код или тот, что я пишу? Тот, что я пишу — например, что-то в таком духе
data State
= Init String
| Foo Int
| Done ResultType
step (Init s) = Foo (length s)
step (Foo 0) = Done someResult
step (Foo n) = Foo (n - 1)
run = go . Init
where
go state = case step state of
Done r -> r
state' -> go state'ну, значит, на эффективность Вам было плевать.
Нет, не плевать, и я бенчмаркал и сравнивал с ragel'ем, например (который генерирует код в том числе с goto, и который писали совсем неглупые люди). Моя хренота была на 3-5% медленнее притом, что умела больше, чем ragel (потому что у меня был не совсем классический регулярный язык, и мне нужно было поддерживать больше вещей, чем умел ragel).
Впрочем, например, программистам JS эффективность интересна в последнем случае.
Я не джаваскриптер.
goto в таких случаях именно улучшает читабельность и лаконичность.
RAII в C++? bracket/with в функциональщине? Да это всё ерунда!
Я не джаваскриптер.
Маска, я тебя знаю?
сравнивал с ragel'ем
В процессе написания аналога wc?
Для RAII надо классы зафигачивать. А тут всё проще и понятнее.
Для RAII надо классы зафигачивать. А тут всё проще и понятнее.
Не обязательно, достаточно:
Foo foo;
oldCApiInit(&foo);
auto releaseGuard = Scoped([&] { oldCApiDestroy(&foo); });Вам лишь бы с кем поругаться? JS-еры-то Вас чем задели, чтобы бочку на нас катить?
Значит, вы ни разу в жизни не пробовали писать эффективные
стейтмашины
Стейт-машина не может быть конечной целью. Разве что, универсальная стейт-машина, без заранее заданной таблицы переходов (интерпретатор/эмулятор). Но тогда паттерн с goto (состояние = указатель инструкций CPU) не применим, нужен switch.
А если у вас фиксированная стейт-машина, её всегда можно переписать в виде обычного традиционного алгоритма, который будет работать быстрее, потому что скомпилируется под нативную архитектуру, а не будет абстракцией поверх машины состояний.
Реализовывая фиксированную стейт-машину вручную, вы стреляете себе в ногу, мешая компилятору разворачивать циклы, векторизовать вычисления и т.п.
парсеры
См. выше. Правильнее описать парсер декларативно и отдать на выполнение специальной библиотеке (которая может и машинный код сгенерировать под грамматику), чем пытаться вручную оптимизировать goto.
зависимое выделение/освобождение ресурсов
RAII в стиле C++ надёжнее, чем "goto finish", в котором могут заводиться ошибки, причём эти ошибки могут годами не обнаруживаться.
Значит, вы ни разу в жизни не пробовали писать эффективные
стейтмашины
парсеры
Как-то выходит без этого. И да, в парсерах для эффективности стоит переходить с написания отдельного лексера и собственно парсера на паерсер, который меняет состояние по отдельным байтам, но руками писать такое сродни безумию.
зависимое выделение/освобождение ресурсов
А вот использование goto для освобождения ресурсов - это так костыль в сишечке. В практически всех языках для этого есть более вменяемые инструменты: RAII в C++/D/Rust, try-with-resources в Java, using в C#, context managers в Python, bracket pattern в StandardML/Ocaml/Haskell. Причём конкретно RAII напишет ровно такой же код, что и сишник руками, только без ошибок.
что даже на уровне самих языков программирования его не стали добавлять
GOTO существует как высокоуровневая абстракция, J-operator. Вот например работа с подробностями http://www.math.bas.bg/bantchev/place/iswim/j.pdf
Из абстракта оттуда: «It is independent of assignment, i.e., it can be added to a “purely-functional” (“non-imperative”) system (such as lisp without pseudo-functions or program feature). Experiments in purely functional programming suggest that its main use will be in success/failure situations, and failure actions.»
Не только. Есть ещё вариант ступенчатой деинициализации, который применяется в ядре NT. Такой аналог RAII или вложенных with.
По моему опыту, 90% сайтов работает быстро и отзывчиво. Может это у вас старая ОС\железо или плохой интернет или роутер старый?
Просто вы — из того сорта яндексистов, которые наслаждаются своей элитарностью, которая им даруется местом, где они просиживают штаны и говнокодят
Да они просто бесплатны для Яндекса, поэтому можно их заставлять писать тесты вместо использования автоматики. Тут же пробегала масса статей про зарплаты.
но там вообще и запаха типов и иммутабельности нет, уж извините.
Ну мы знаем, что программисты в Яндексе более-менее бесплатны, и время их не ценится. Поэтому их можно заставлять писать тесты на каждый чих.
Статическая типизация - это же автоматизирование программирования, когда на специально приспособленном декларативном языке вы описываете некоторые свойства программы, которые проверяются при каждой компиляции.
Соответственно, отказ от использования развитых систем статической типизации аналогичне солдатам из стройбата вместо экскаватора. Ну можно, а на мелких масштабах даже оправдано. Но на крупных это используется когда солдаты дёшевы.
ага. когда вы на декларации записываете 1000 строк, там где могли бы написать на императивке
a += b
Вы сейчас выступаете как чатГПТ - вместо обдумывания реплики, выдёргиваете случайное слово, и пишете на него ответ, не вдаваясь в контекст.
Речь шла о декларативном языке типов, на котором вы пишете, что a : int, b : int для вашей ситуации. И то, если эти типы не выводятся. Ну и вы одновременно путаете императивность/декларативность и статическую/динамическую типизации. Это разные координаты.
вот например был широко распространён императивный bash.
Он не очень-то императивный, там дофига элементов функциональщины. Более того, конвейеры в bash - это вообще ленивые вычисления.
далее пришёл чувак который сказал "это сложно" и запили взамен bash'у systemd.
Это единичный пример работящего идиота, который вместо гибкой системы стал делать кубик-рубик-монолит.
ага. когда вы на декларации записываете 1000 строк, там где могли бы написать на императивке
a += b
Вы не поверите, но я тоже пишу a += b даже в чистой функциональщине. При этом это работает композабельно и универсально, для куда большего спектра выражений, чем это ваше a в императивщине. Можно этим же выражением обновить каждый нечётный элемент массива, например.
далее пришёл чувак который сказал "это сложно" и запили взамен bash'у systemd.
взамен bash'у systemd.
I can't even
Пришёл чувак и впилил взамен брейнфаку (восемь операторов) Go (дофига операторов и ключевых слов), ага.
Считать systemd заменой bash'у — это какой-то бред. systemd — это замена bash'у + всему набору команд, которые тащатся вместе с ним и так, и в вашей системе инициализации.
Лично мне нет существенной разницы, писать скрипты под openrc (в генте, которой я пользуюсь) или под systemd — они оба одинаково сложные, я их оба одинаково не знаю.
Спасибо за интересное обсуждение. Про мир реальных приложений (запрос к веб-приложению и микросервисы) - это как раз то, чем я профессионально занимаюсь на основной работе как Java-разработчик уже много-много лет. Хочу вам сказать, что строгая типизация для высоконагруженных бэкенд-приложений просто жизненного необходима, она очень много ошибок предотвращает. Например, мы на работе очень часто задаем, что запрос пользователя должен быть строго по спецификации (ООП иерархия объектов) и некоторые поля обязательно должны присутствовать, другие должны иметь минимальную длину и так далее. Например, аннотации javax.validation используются.
но всё же, откуда взято, что теория типов якобы удобна для компьютера?
Да из личного опыта программирования этой теории типов - 11 правил выведения типов довольно легко запрограммировать. А вот если вы теорию множеств захотите запрограммировать - все не так просто, там придется теорию типов вводить\придумывать к ней.
Нет, она не может заменить, а только дополнить. Тесты позволяют выразить какие-то свойства, которых не хватает подъязыку типов (той части вашего ЯП, что описывает типы).
С другой стороны, глупо отрицать, что "обычная система типов" позволяет выразить многие полезные свойства программы так, что тестами это писать очень тяжело. Ну банальная сигнатура оператора "+".
Поэтому, если идти с точки зрения подхода "программирование = фильтрация от ошибок", то типы - это всего лишь более грубое сито по сравнению с тестами.
Все Вами сказанное справедливо если у вас номинативная типизация. Ну там где у вас на входе int а в процессе используется деление и вам надо ручками проверять - прилетел к вам ноль или нет. И тут да, надо писать тесты и проверять как ваш код эту ситуацию отрабатывает, потому что вы просто не можете через тип выразить с какими именно данными вы работаете. Почему? Потому что у вас тип аргумента функции не совпадает с областью определения функции. У вас функция деления определена не на int а на NonZero фактически. И вот если ваша система типов позволяет описать это - то тесты (юнит тесты) вам не нужны, за вас все сделает тайпчекер. А если ваша система типов не позволяет этого описать - то вы тайп чекаете ручками через тесты.
> И вот если ваша система типов позволяет описать это - то тесты (юнит тесты) вам не нужны, за вас все сделает тайпчекер.
Понимаете, в конечном итоге проверки программ, что типами, что тестами получаются в результате определённого дублирования свойств программы. Соответственно, если система типов настолько выразительна, чтобы полностью описать свойства программы, то писать надо на ней, а не на основном ЯВУ.
Соответственно, где-то проходит граница разумной выразительности системы типов, а значит, в практически применимых системах всегда остаётся место для других методов проверки программ.
Соответственно, если система типов настолько выразительна, чтобы полностью описать свойства программы, то писать надо на ней, а не на основном ЯВУ.
Не совсем, потому что типами вы выражаете свойства, а термами, имеющими эти типы, вы показываете, почему эти свойства выполняются.
Тут нет того дублирования, о котором вы говорите.
Не совсем, потому что типами вы выражаете свойства, а термами, имеющими эти типы, вы показываете, почему эти свойства выполняются.
Если эти свойства полностью выражают, скажем, денотационную семантику программы, то для значительной доли программ достаточно будет свойств - основную программу можно будет не писать. Ну просто вы будете программировать типах, а достаточно проработанный компилятор выведет основную программу.
Картина выше абсурдна, соответственно, подъязык типов у каждого ЯВУ имеет естественные ограничения - он должен быть менее выразителен, чем основной язык.
Тут нет того дублирования, о котором вы говорите.
Когда мы статически типизируем программу, мы вносим определённое дублирование. Представьте, что у вас вообще никакого дублирования нет, любой символ в программе уникален. Ну тогда вы просто не сможете проверить программу ну никак.
Если эти свойства полностью выражают, скажем, денотационную семантику программы, то для значительной доли программ достаточно будет свойств - основную программу можно будет не писать.
Утверждаю, что нет, ни в теории, ни даже на практике. Term finding — неразрешимая задача, и эффективных полуалгоритмов нахождения доказательств нет.
Ну да, если у вас там, условно, семантика сводится к равенству двух выражений в полукольце, то это разрешимая задача. Но подавляющее большинство интересных программ к этому не сводится.
Когда мы статически типизируем программу, мы вносим определённое дублирование. Представьте, что у вас вообще никакого дублирования нет, любой символ в программе уникален. Ну тогда вы просто не сможете проверить программу ну никак.
Мы ведь оба можем построить ЯП, в котором это утверждение формально не выполняется? :)
Мы ведь оба можем построить ЯП, в котором это утверждение формально не выполняется? :)
Будут внешние правила вывода типов, которые соблюдаются, а значит неявно выписаны в программе (их можно до какой-то степени извлечь из достаточно длинной программы).
В любом случае, любая проверка сводится к тому, что вы приходите к одному и тому же результату с двух сторон. Не с одной, а хотя бы с двух.
Окей.
inc (x : Int) = x + 2 : (Σr:Int. r > x)Где здесь дублирование из-за типов?
: Int
Вернее, что это тип, у которого определено сложение. Если взять в качестве йазыга OcaML, то аннотация выводится из кода. Впрочем, из-за двойки это же выводится и в SML.
Ну невозможна проверка без частичного повтора. Меня можно упрекнуть в том, что я очень широко употребляю слово "дублирование", ну и ладно.
Кстати, из типов и области видимости можно вывести, что там в качестве оператора стоит + или *.
: Int
Это какое-то новое определение дублирования.
Вернее, что это тип, у которого определено сложение.
Нет.
У меня здесь Int бесконечно точный (как хаскельный Integer), а для других типов (например, машинного целого) эта функция не тайпчекается: x + 2 может быть меньше x.
По термуλx. x + 2 вы не сможете вывести тип, а по типу (x : Int) → (Σr:Int. r > x) вы не сможете вывести терм (особенно единственным образом).
где на бестиповом языке писали 1-2 строки, на типовом теперь пишут 1-2 экрана да и ещё иммутабельность пропагандируют, с которой 1-2 экрана превращается в 5-10.
А почему не 50-100?
Аннотации типов в большинстве мейнстримных языков с продвинутой системой типов нужны мало где, поэтому оверхед по писанине от типизации сильно меньше (а при чтении он из оверхеда превращается во благо, кстати), и он существенно меньше, чем выигрыш на становящихся ненужными тестах.
с типами компиляторы писать проще
И снова нет. Тайпчекер — весьма нетривиальная часть компилятора, и куда проще просто забить и напихать рантайм-проверки.
но всё же, откуда взято, что теория типов якобы удобна для компьютера?
Чем больше классов ошибок проверено и исключено на этапе компиляции, тем меньше нужно делать на этапе выполнения, тем быстрее при прочих равных будет ваша программа.
Чем больше классов ошибок проверено и исключено на этапе компиляции, тем меньше нужно делать на этапе выполнения,
Плюсую, языки программирования именно этим путем развиваются. C++ -> Java -> Kotlin все больше и больше проверяют на этапе компиляции. Дошло до того, что Kotlin банально заставляет вас прорабатывать все null-типы через if, чтобы потом на проде не словить NPE
плевать на ошибки в коде, отлавливая их где-нибудь "наверху": грохнулось — перезапустили, а потом на статистику ошибок поглядели и что-то поправили, или даже оставили так
Потом, правда, Алиса кладёт весь NTP, с диска C: всё удаляется, и так далее, но это ничего страшного, просто посмотрим статистику ошибок и что-то поправим.
А если не секрет, зачем вообще с таким подходом тесты писать? Написали код, запустили-потыкали пару раз, вроде работает ⇒ деплоим в прод. Если что-то навернётся — тоже перезапустили, статистика ошибок, оставили так.
Как они помогают прийти к нужному результату? Они только мешают, их обновлять надо, поддерживать, все дела. А так нафигачил и го в прод. Я вот на одном проекте без тестов фигачил и очень быстро всё сделал, триллионы долларов заработали.
Что не так?
Даже когда систему пишешь в одиночку, чертовски полезно зафиксировать поведение в тестах, чтобы потом иметь возможность автоматизированного контроля, изменилось оно или нет.
Абсолютно та же логика работает с типами.
И обратно, абсолютно так же все пока что упомянутые вами возражения против типизации работают и как возражения против тестов. И экранов кода там больше, и бро из соседнего комментария с MVP тестами не пользовался.
Это у вас где количество кода радикально растёт от введения статической типизации?
Ну чисто для прикола, вот простыня https://github.com/ocaml/ocaml/blob/trunk/middle_end/printclambda_primitives.ml , расскажите пожалуйста, как там аннотации типов раздули код...
вижу внедрение вопросиков в раст
Так это они Хаскель косплеят, монада Either по-сути https://hackage.haskell.org/package/ghc-internal-9.1201.0/docs/src/GHC.Internal.Data.Either.html#line-157 с оптимизацией быстрого выхода. Ошибка - это строка с Left.
То, на что вы намекаете - это unwrap.
Большой молодец, пишите еще, спасибо! Lean4 нравится тем, что готов к употреблению как ЯП с завтипами, а как пруф-ассистант мила Изабелла: AFP и seL4 весьма хороши и полезны
Она (HoTT) настолько не готова, что даже в начале учебника по гомотопической теории типов написано, что теория в процессе изменений и все может поменяться
Книжке много лет, Воеводский умер, к сожалению, и движения там и правда особо не наблюдается. Тем не менее, прочитать книжку стóит – горизонты понимания что такое тип она точно расширит, особенно если у вас геометрическая/топологическая интуиция прокачана.
По применимости – открытый вопрос, вот недавнее обсуждение https://mathoverflow.net/questions/480656/hott-for-the-working-mathematician-especially-the-homotopy-geometer-what-is
Пиано
Сейчас так уже не принято, чаще пишут Пеано.
у вас геометрическая/топологическая интуиция прокачана
Ох не люблю я эту геометрическую интуицию, всегда ее ненавидел еще со школы... Бррррр
Спасибо за замечание, мб прочитать первые пару-тройку глав действительно стоит, прочтение книги занимает в 4-5 раз меньше усилий, чем прочтение + выполнение упражнений + их формализация
К сожалению (я тоже не люблю топологию), похоже, без этого никуда. Лучше всего взять какую-нибудь лайтовую книжку по топологии и просто по ней пробежаться-прорешать задачи, чтобы развить топологическую интуицию. Introduction to Topology: Pure and Applied, например, меня порадовала (и там в конце главы с прикольными прикладными задачами, что хороший отдых от всей этой фундаментальной абстрактщины). Только заранее рекомендую открыть её errata и держать рядом — там есть ошибки и опечатки.
особенно если у вас геометрическая/топологическая интуиция прокачана.
По моему мнению, геометрическая интуиция особо не поможет. Точнее, она поможет ровно в той части, где используется геометрическая интерпретация. А поскольку большую часть книги проще понять, используя логические и вычислительные аналогии, а за пределами используются ∞-категорные построения, которые фиг нарисуешь, кроме как диаграммой, на геометрическую интуицию надеяться не стоит.
ИМХО, слово «гомотопическая» в названии — это больше пиар-ход, чем характеристика теории. Хотя Роберт Харпер высказывался, что HoTT можно читать как «(некая) теория гомотопических типов» (ввиду упомянутой геометрической интерпретации типов) и как «гомотопическая теория (неких) типов» (ввиду синтетичного характера построений внутри теории).
движения там и правда особо не наблюдается
В 2023-2024гг. я наблюдал сильное желание втащить в HoTT модальность в разных вариациях: формализация на HoTT модальных теорий, теория модальных типов, модальная теория зависимых типов и т.д. и т.п.
Сомнительный прогресс, конечно, но чем богаты.
ровно в той части, где используется геометрическая интерпретация
То-есть как минимум чтобы вообще начать читать ) Я начал читать после пролистывания до вот этой таблички, правую колонку которой как-то сразу и хорошо представил – и мне стало любопытно, куда такой взгляд на ландшафт вообще может привести.
слово «гомотопическая» в названии — это больше пиар-ход
Ну, времена такие. Из аббревиатуры HoTT тоже явно маркетинговые уши торчат )
Кстати большинство (и я в том числе) проголосовали за постижение Тайн Мироздания:)
Увы, в моем ВУЗе все эти основания математики не изучали (из математики была линейная алгебра, матан, дискретка, тервер, численные методы). Но тема очень интересная, всегда хотелось погрузиться в нее поглубже.
Поэтому вопрос к тем кто глубоко в теме: что вы можете сказать о том, как устроен реальный мир на низком уровне, опираясь на знания оснований математики?
Кстати большинство (и я в том числе) проголосовали за постижение Тайн Мироздания:)
Вот тут для меня была неожиданность, действительно этот пункт оказался очень популярен и сейчас лидирует. Мне тоже интересно =) Но ML в большем приоритете у меня
Увы, в моем ВУЗе все эти основания математики не изучали
А у кого их изучали?) Ладно, у нас был профессор Лагодинский, который давал математическую логику довольно глубоко. Но не конструктивным путем (через таблицы истинности) и без опоры на формализацию и теорем-пруверы.
что вы можете сказать о том, как устроен реальный мир на низком уровне, опираясь на знания оснований математики?
Например, можно формализовать и вывести уравнения Максвелла. Понимания оснований математики даст вам 100%-й уровень комфорта и понимании в том, что вы выводите.
Например, можно формализовать и вывести уравнения Максвелла. Понимания оснований математики даст вам 100%-й уровень комфорта и понимании в том, что вы выводите.
Вот не поверю, что можно математически вывести отстутствие магнитных зарядов в природе.
Но ML в большем приоритете у меня
Непонятно при чем тут ML. Это же по сути самые обычные (и вообще говоря приближенные) вычисления, но в ОЧЕНЬ большом количестве. Никакими основаниями математики там и не пахнет (ИМХО конечно), это просто почти школьная математика, а весь вау-эффект достигается за счет перехода количества в качество.
Вот здесь статья о реверс-инжиниринге простейшей нейросети, которую обучили для сложения двоичных чисел. Ожидалось что она воспроизведет внутри себя что-то вроде "двоичного сумматора", применяемого во всех микропроцессорах, по оказалось что сеть пошла по принципиально иному пути... И в некотором смысле этот другой путь гораздо ближе к природе, чем двоичные сумматоры.
Поэтому вопрос к тем кто глубоко в теме: что вы можете сказать о том, как устроен реальный мир на низком уровне, опираясь на знания оснований математики?
Ничего не могу сказать, к сожалению (но я ненастоящий сварщик).
Математика — это просто наука о том, как обращаться с закорючками по правилам, а основания математики — это кусочек этой науки, в котором закорючками являются правила обращения с другими закорючками.
Насколько я могу судить, физикам вся эта глубокая муть не нужна: они счастливо работают с наивной математикой по большому счёту 19-го века, и им норм. Я по разным причинам наиболее интересуюсь теорией топосов, и если смотреть на работы теоретических физиков по их применению, например, в качестве оснований (а не языка для выражения), то там дело ограничивается очень узким множеством статей вроде таких — https://arxiv.org/pdf/2110.06793 или https://arxiv.org/pdf/1106.5660 , у которых цитирований по десятку-другому максимум (то есть, физикам эта тема не очень интересна, а ИМХО если уж что из оснований и может претендовать на прорывные результаты, так это топосы).
И, например, не придумано экспериментов, способных фальсифицировать наличие или отсутствие C в ZF+C-аксиоматике нашего мира (я склонен считать, что парадокс Банаха-Тарского ближе к нереализуемым бесконечностям, чем к отсутствию C, и если для вас он что-то опровергает, то в вашем мире не должно существовать и, скажем, всего множества вещественных чисел), или отличить ZF+C от других аксиоматик, или сказать, описывается наш мир классической или конструктивной логикой.
Но это всё, конечно, не значит, что таких экспериментов не может быть. И даже если вдруг окажется, что в нашем мире C нет, или логика классическая, то это не делает ZF+C и классическую логику более плохой математикой.
Основания математики по определению замкнуты на себя самих.
А теперь поговорим о списке практических применений фундаментальной математики.
Извините за "диагноз по фотографии", но по-моему вы просто искренне и бескорыстно тащитесь от всего, что написано до приведенной фразы. И это прекрасно и не нуждается в притягивании за уши применений. Целую цивилизацию отгрохали, чтобы можно делать то, что хочется, а не только необходимое зачем-нибудь.
Сомнительны применения, связанные со статистикой и линейной алгеброй. Абстракция — мощнейший инструмент мышления. Скорее всего, принять на веру те начала мат. стиатистики и т. п., которые фундаментальной математикой можно вывести, ничуть не помешает изучению, зато позволит [вашим конкурентам] начать его раньше.
Формализация ПО и баз данных для обычного бизнеса запретительно дорога. Но! Рекомендую посмотреть в сторону безопасных (secure, safe) и доверенных систем (trustworthy). Именно там востребованы строгие доказательства и то, чтобы поменьше принимать за данность.
Раз интересна 3D-графика, рядом есть более серьезное направление — вычислительные методы. С точки зрения работы реального ИИ они, скорее всего, не менее релевантны, чем линейная алгебра, да и в 3D-графике о погрешностях надо думать.
Глубоко понять, как устроен реальный мир на низком уровне.
учился в аспирантуре [...], сдал академический минимум
Вы же сдавали философию...
ничуть не помешает изучению, зато позволит [вашим конкурентам] начать его раньше.
Да у нас вроде нету спешки проходить настолько базовые предметы. Они же проходятся один раз и на всю жизнь, и лучше это сделать более качественно и глубоко (на мой взгляд). Еще можно разбить на 2 этапа, в первом этапе вы проходите эти предметы по какому-нибудь поверхностному курсу, а потом возвращаетесь и проходите по более глубокому курсу с более глубоким покрытием фундамента. Собственно, я пошел именно таким путем почти по всем предметам.
Вы же сдавали философию...
Так вот, как раз философия и заставляет двигаться глубже. В общих чертах этот пункт я понимаю уже давно, уровни организации материи всякие (стандартная модель -> физика -> химия -> биология -> астрофизика -> теория большого взрыва). Но хочется больше деталей и формальной верификации, так как очень много дыр в понимании.
Поддерживаю. Мне попытки автора изучать все исключительно через теорию типов, да еще и склонять к этому нормальных людей во первых напомнили анекдот про математика и инженера. А во вторых вызывают сомнения в способности автора решать именно практические задачи, а не заниматься теоретизированием.
Анекдот:
Математика и инженера заперли в комнате с одной дверью. Голос скомандовал: вас будут тестировать. Постройтесь вдоль линии напротив двери. Сейчас через нее введут голую женщину. Она достанется тому, кто первый до нее доберется. Но есть правила: Прозвучит звуковой сигнал. После каждого сигнала вы можете делать шаг, но на расстояние не больше половины оставшегося. Голос замолк и раздался гудок. Инженер сразу сделал прыжок в половину комнаты. На следующий гудок - еще четверть комнаты. А математик стоит и приговаривает: прыгай милок, прыгай - ты все равно ее никогда не достигнешь, это знать надо! На что инженер отвечает - да и бог с ним, за то уже через два прыжка буду от нее на расстоянии, позволяющим любые практические действия.
Теория - это конечно замечательно, но практика - критерий истинности! Жила математика без теории типов долго и как то студенты изучали и тервер и мат. статистику И могли всë это не только понять, но и осмыслить. И для этого вовсе не нужно начинать с таких глубин.
Что бы быть чемпионом формулы 1 , обязательно знать все процессы происходящие в двигателе, на фундаментальном уровне?
И не обязательно знать математику на таком "царском", уровне, как Вы описываете, что бы быть хорошим инженером в ml. Достаточно базового , университетского уровня.
А еще важней, для програмиста/ разработчика, уметь понимать специфику бизнес задач, умение "нырнуть" в предметную область.
что бы быть хорошим програмистом
Ну это очень мутное понятие, каждый его по-разному интерпретирует. Как вы формально определите критерии "хорошего программиста"?
Для некоторых хороший программист - это тот, кто просто умеет писать чистый код. Для других - тот, кто умеет нужные библиотеки и фреймворки подключать\соединять. Для третьих это тот, кто удобен бизнесу и понимает требования\решает проблемы в адекватный срок. Для четвертых это тот, кто хорошо знает алгоритмы и структуры данных, сердце компьютерных наук.
Все это я уже проходил и хочется двигаться дальше.
Что бы быть чемпионом формулы 1 , обязательно знать все процессы происходящие в двигателе, на фундаментальном уровне?
Сильно подозреваю, что таки знают.
Про подобную "французскую математику" очень остроумно рассказывал покойный Арнольд. По моему опыту общения с современными французскими промышленными инженерами, с таким подходом непостижимая математика начинает где-то в таблице умножения.
Дальше цитируем Арнольда:
Оказывается, нуль - положительное число. Действительно, для Бурбаки все общие понятия важнее их частных случаев, поэтому все нестрогие неравенства являются фундаментальными, а строгие - маловажными специальными случаями, примерами. В соответствии с этим во Франции слово "больше" в математике означает то, что мы называем "больше или равно". Например, каждое вещественное число больше самого себя, а значит, нуль больше нуля и, следовательно, положителен!
...
Кроме положительности нуля, то же рассуждение устанавливает и его отрицательность (ибо нуль меньше нуля по французско-бурбакистской терминологии). Мои коллеги и ученики разъяснили мне, что нуль входит также и в множество неположительных чисел, а заодно и в множество неотрицательных чисел. Но Серр, кроме указанных неравенств, доказал еще одно свойство нуля: он оказывается вдобавок числом натуральным.
...
В уже упомянутом руководстве для первокурсников все это используется для определения факториала. Вот это определение: во-первых, 0! = 1; во-вторых, для любого натурального числа n имеет место равенство (n + 1)! = (n + 1)n!.
Если не знать, что нуль - натуральное число, то ни одного факториала невозможно ни определить, ни понять, ни вычислить. Кстати, обычное определение n! = 1• 2 • ... • n, во-первых, не фигурирует в этом тексте нигде, и, во-вторых, считается ошибочным. А именно: во-первых, участвующие в этом определении три точки не определены, а во-вторых, определение не годится ни для n = 0, ни для n = 1.
Раз уж я стал разбирать это руководство, процитирую из него еще одно место. Речь идет теперь об определении науки математики, чтобы студенты знали, что им предстоит:
"Математика есть наука о доказательствах, доказательства это цепочки импликаций: (из А вытекает В, из В вытекает С) - цепочка; вывод: доказано, что из А вытекает С. Итак, самое главное - понять, что такое одна импликация. Вот ее определение. Пусть А и В - два произвольных высказывания. Если оба они верны, то говорят, что из А вытекает В".
На мой непросвещенный взгляд, такая точка зрения на импликации (а следовательно, и на доказательства, и на математику) - чистое мракобесие. При таком определении из того, что дважды два четыре, следует, что Земля вращается вокруг Солнца.
Студента, понимающего выводы и доказательства подобным образом, уже бесполезно учить какой-либо естественной науке: мракобесие уничтожает естествознание как таковое. По этой мракобесной логике Галилея поделом наказывали: он ведь говорил о своих доказательствах вращения Земли и других подобных фактов совсем в другом смысле.
...
Из других бурбакистских принципов, упомянутых Серром, назову еще утверждение о полной независимости математики от физики. В одном своем письме ко мне Серр уже заявил, что "у математики и физики нет ничего общего", но он добавил тогда, что "не станет публиковать этого утверждения, потому что нам, математикам, не следует высказываться по философским вопросам, ибо самые лучшие из нас способны высказать здесь совершеннейшую чушь".
...
Антифизические идеи в математике давно популяризируются самыми разными ее представителями. Г. Харди, например, объяснял (в недавно изданной по-русски "Апологии математика") слова Гаусса "теория чисел - королева математики" сходством теории чисел с королевой: это сходство заключается, согласно Харди, в полной бесполезности обеих.
...
В середине двадцатого века была предпринята попытка разделить математику и физику. Последствия оказались катастрофическими. Выросли целые поколения математиков, незнакомых с половиной своей науки и, естественно, не имеющих никакого представления ни о каких других науках. Они начали учить своей уродливой схоластической псевдоматематике сначала студентов, а потом и школьников (забыв о предупреждении Харди, что для уродливой математики нет постоянного места под Солнцем).
Поскольку ни для преподавания, ни для приложений в каких-либо других науках схоластическая, отрезанная от физики, математика не приспособлена, результатом оказалась всеобщая ненависть к математикам — и со стороны несчастных школьников (некоторые из которых со временем стали министрами), и со стороны пользователей.
Уродливое здание, построенное замученными комплексом неполноценности математиками-недоучками, не сумевшими своевременно познакомиться с физикой, напоминает стройную аксиоматическую теорию нечётных чисел. Ясно, что такую теорию можно создать и заставить учеников восхищаться совершенством и внутренней непротиворечивостью возникающей структуры (в которой определена, например, сумма нечётного числа слагаемых и произведение любого числа сомножителей). Чётные же числа с этой сектантской точки зрения можно либо объявить ересью, либо со временем ввести в теорию, пополнив её (уступая потребностям физики и реального мира) некоторыми «идеальными» объектами.
К сожалению, именно подобное уродливое извращённое построение математики господствовало в преподавании математики в течение десятилетий. Возникнув первоначально во Франции, это извращение быстро распространилось на обучение основам математики сперва студентов, а потом и школьников всех специальностей (сперва во Франции, а потом и в других странах, включая Россию).
Ученик французской начальной школы на вопрос «сколько будет 2+3» ответил: «3+2, так как сложение коммутативно». Он не знал, чему равна эта сумма, и даже не понимал, о чем его спрашивают!
Другой французский школьник (на мой взгляд, вполне разумный) определил математику так: «там есть квадрат, но это нужно ещё доказать».
По моему преподавательскому опыту во Франции, представление о математике у студентов (вплоть даже до обучающихся математике в École Normale Supérieure — этих явно неглупых, но изуродованных ребят мне жалко больше всего) — столь же убого, как у этого школьника.
...
Попытки создания «чистой» дедуктивно-аксиоматической математики привели к отказу от обычной в физике схемы (наблюдение — модель — исследование модели — выводы — проверка наблюдениями) и замена её схемой: определение — теорема — доказательство. Понять немотивированное определение невозможно, но это не останавливает преступных алгебраистов-аксиоматизаторов. Например, они были бы готовы определить произведение натуральных чисел при помощи правила умножения «столбиком». Коммутативность умножения становится при этом трудно доказываемой, но все же выводимой из аксиом теоремой. Эту теорему и её доказательство можно затем заставить учить несчастных студентов (с целью повысить авторитет как самой науки, так и обучающих ей лиц). Понятно, что ни такие определения, ни такие доказательства, ни для целей преподавания, ни для практической деятельности, ничего, кроме вреда, принести не могут.
...
Если математики не обучаются сами, то потребители, сохранившие как нужду в современной в лучшем смысле слова математической теории, так и свойственный каждому здравомыслящему человеку иммунитет к бесполезной аксиоматической болтовне, в конце концов откажутся от услуг схоластов-недоучек и в университетах, и в школах.
он был большой шутник
Много пропаганды, мало сути.
Суть хорошо изложена в исходной статье. Математика исторически развивалась сначала параллельно землемерию (геометрия), а потом физике (интегральное счисление для ньютоновой, тензорный анализ для ОТО). Вся эта формализация (которую Фреге делал - не доделал, потом Рассел и Уайтхед делали - не доделали, потом группа Бурбаки делала - не доделала, теперь вот Воеводский делал - не доделал) не просто избыточно сложна и по большому счёту бесполезна, но ещё и совершенно непонятна посторонним. Отсюда сектантский апломб адептов, потому что адекватному человеку совершенно непонятно, зачем погружаться в это бесконечное определение определений, абстракции над ещё большими абстракциями и сомнительные утверждения, которые невозможно ни доказать, ни опровергнуть, ни даже понять.
Как быть с исследованиями Гёделя о том, что невыводимые теоремы всё равно существуют и их бесконечно много? С работами Лакотоса (который показал, что доказательство - по большому счёту конструкт и результат консенсуса)? С математическими объектами, состояние которых на определённой итерации в принципе непредсказуемо без вычисления предыдущих (игра Жизнь так устроена, и тот же Стивен Вольфрам вообще считает, что в этом и есть будущее математики)?
А никак. Этому не учили.
не просто избыточно сложна и по большому счёту бесполезна, но ещё и совершенно непонятна посторонним. Отсюда сектантский апломб адептов, потому что адекватному человеку совершенно непонятно, зачем погружаться в это бесконечное определение определений, абстракции над ещё большими абстракциями и сомнительные утверждения, которые невозможно ни доказать, ни опровергнуть, ни даже понять.
Это, вообще говоря, и к обычной, прикладной математике применимо как псевдоаргумент. А то придумали там какие-то парадоксы дней рождения, тоже мне. 183 человека нужно, чтобы вероятность совпадения днюхи была ½, и всё тут.
Как быть с исследованиями Гёделя о том, что невыводимые теоремы всё равно существуют и их бесконечно много?
Так с ними и быть. Не понимаю проблем.
С работами Лакотоса (который показал, что доказательство - по большому счёту конструкт и результат консенсуса)?
Консенсуально доказали с пацанами, что от вышек 5G случается ВИЧ, как с этим быть?
И «183 человека» тоже консенсуально объявили правильным ответом.
Надо закопать конкретно эти работы Лакатоса.
С математическими объектами, состояние которых на определённой итерации в принципе непредсказуемо без вычисления предыдущих
А в чём с ними проблема? Берёте и вычисляете.
(игра Жизнь так устроена, и тот же Стивен Вольфрам вообще считает, что в этом и есть будущее математики)?
Если говорить о ненужности оснований математики могут разные люди с разными взглядами (включая, скажем, прикладных математиков, которым это всё не нужно для их работы в прямом смысле), то при этом упоминать Вольфрама с его new kind of science в положительном ключе могут только фоменковцы от математики.
к обычной, прикладной математике применимо как псевдоаргумент.
Как раз к прикладной математике оно отлично применимо. Многие математические объекты вроде комплексных чисел как раз и появились для описания моделей природных процессов.
Так с ними и быть. Не понимаю проблем.
Действительно: существует бесконечное количество истинных теорем, которые невозможно доказать с помощью системы для доказательства теорем. Казалось бы, что тут может быть не так?
Надо закопать конкретно эти работы Лакатоса.
Для начала вам было полезно их хотя бы прочитать.
Достаточно начать с "Доказательства и опровержения". 152 страницы последовательно разворачивается история доказательства теоремы Эйлера для многогранников. В принципе, доказал её ещё Эйлер - но каждое новое поколение математиков добавляет уточнения и конца этому процессу не видно.
На какой же странице этой книги теорема Эйлера становится доказанной? На 5-ой (где приведено доказательство Эйлера)? На 152 - где признаётся, что на момент написания книги "она верна для многогранников, топологически эквивалентных сфере"? Но топология продолжает развиваться и скорее всего, и это определение неточно.
А в чём с ними проблема? Берёте и вычисляете.
В том, что из аксиом, без вычислений, это значение получить нельзя.
при этом упоминать Вольфрама с его new kind of science в положительном ключе могут только фоменковцы от математики
Ну, у Вольфрама есть заслуги перед наукой - его Mathematica имеет широчайшее применение.
Где применяются мощнейшие исследования Вопенки и Воеводоского? Нигде. Возникает ощущение, что их адепты просто больше ничего не умеют.
Как раз к прикладной математике оно отлично применимо. Многие математические объекты вроде комплексных чисел как раз и появились для описания моделей природных процессов.
И где мне их увидеть? Вот передо мной стол, стул и окно. Где там комплексные числа потрогать?
По-моему, это просто какое-то переусложнение ради переусложнения. Например, не зря великий Декарт называл их «воображаемыми» числами, а Гаусс сомневался в осмысленности их метафизики.
И это мы ещё всяких греков и иррациональные числа не вспоминали.
Действительно: существует бесконечное количество истинных теорем, которые невозможно доказать с помощью системы для доказательства теорем. Казалось бы, что тут может быть не так?
Их вообще невозможно доказать (во вкладываемом вами смысле), даже ручкой на бумажке, пруверы тут ни при чём.
Но таки да, что же тут не так? Давайте, доводите мысли до конца, чтобы не пришлось за вас додумывать.
Для начала вам было полезно их хотя бы прочитать.
Так я их читал.
Как там дела с количеством людей для парадокса дня рождения? Вы согласны, что нужно 183 человека? Если не согласны, то вон Росатый стоит, он в 90-ые очень авторитетным авторитетом был, и сейчас быстро вас убедит.
В том, что из аксиом, без вычислений, это значение получить нельзя.
Не понял, откуда тут взялась дихотомия между аксиомами и вычислениями?
Ну, у Вольфрама есть заслуги перед наукой - его Mathematica имеет широчайшее применение.
У Фоменко тоже есть заслуги в математике, но это не делает его авторитетом в истории. Точно так же с Вольфрамом: заслуги в софтварной инженерии не делают его авторитетом в основаниях математики.
И где мне их увидеть? Вот передо мной стол, стул и окно. Где там комплексные числа потрогать?
Переменный ток, который это всё освещает? Почти вся теория электрических цепей описывается комплексными числами.
Вот ещё пара примеров из Арнольда:
Когда я учился на первом курсе мех.-мата МГУ, лекции по анализу читал теоретико-множественный тополог Л. А. Тумаркин, добросовестно пересказывающий старый классический курс анализа французского образца, типа Гурса. Он сообщил нам, что интегралы от рациональных функций вдоль алгебраической кривой берутся, если соответствующая риманова поверхность — сфера, и, вообще говоря, не берутся, если род её выше, и что для сферичности достаточно существования на кривой данной степени достаточно большого числа двойных точек (вынуждающих кривую быть уникурсальной: её вещественные точки можно нарисовать на проективной плоскости единым росчерком пера).
Эти факты настолько поражают воображение, что (даже сообщённые без всяких доказательств) дают большее и более правильное понятие о современной математике, чем целые тома трактата Бурбаки. Ведь мы узнаем здесь о существовании замечательной связи между вещами на вид совершенно различными: существованием явного выражения для интегралов и топологией соответствующей римановой поверхности, с одной стороны, а с другой стороны — между числом двойных точек и родом соответствующей римановой поверхности, проявляющемся вдобавок в вещественной области в виде уникурсальности.
Уже Якоби заметил, как самое восхитительное свойство математики, что в ней одна и та же функция управляет и представлениями целого числа в виде суммы четырёх квадратов, и истинным движением маятника.
Эти открытия связей между разнородными математическими объектами можно сравнить с открытием связи электричества и магнетизма в физике или сходства восточного берега Америки с западным берегом Африки в геологии.
Понять коммутативность умножения можно, только либо пересчитывая выстроенных солдат по рядам и по шеренгам, либо вычисляя двумя способами площадь прямоугольника. Попытки обойтись без этого вмешательства физики и реальности в математику — сектанство и изоляционизм, разрушающие образ математики как полезной человеческой деятельности в глазах всех разумных людей.
Определитель матрицы — это (ориентированный) объём параллелепипеда, рёбра которого — её столбцы. Если сообщить студентам эту тайну (тщательно скрываемую в выхолощенном алгебраическом преподавании), то вся теория детерминантов становится понятной главой теории полилинейных форм. Если же определять детерминанты иначе, то у каждого разумного человека на всю жизнь останется отвращение и к определителям, и к якобианам, и к теореме о неявной функции.
Что такое группа? Алгебраисты учат, будто это множество с двумя операциями, удовлетворяющими куче легко забываемых аксиом. Это определение вызывает естественный протест: зачем разумному человеку такие пары операций? «Да пропади она пропадом, эта математика» — заключает студент (делающийся в будущем, возможно, министром науки).
Положение становится совершенно иным, если начать не с группы, а с понятия преобразования (взаимно-однозначного отображения множества в себя), как это и было исторически. Набор преобразований какого-либо множества называется группой, если вместе с любыми двумя преобразованиями он содержит результат их последовательного применения, а вместе с каждым преобразованием — обратное преобразование.
Их вообще невозможно доказать (во вкладываемом вами смысле), даже ручкой на бумажке, пруверы тут ни при чём.
Снова Арнольд:
"«Тонкий яд математического образования» (по выражению Ф. Клейна) для физика состоит именно в том, что абсолютизируемая модель отрывается от реальности и перестаёт с нею сравниваться. Вот самый простой пример: математика учит нас, что решение уравнения Мальтуса dx/dt = x однозначно определяется начальными условиями (т.е. что соответствующие интегральные кривые на плоскости (t, x) не пересекают друг друга). Этот вывод математической модели имеет мало отношения к реальности. Компьютерный эксперимент показывает, что все эти интегральные кривые имеют общие точки на отрицательной полуоси t. И действительно, скажем, кривые с начальными условиями x(0) = 0 и x(0) = 1 при t = –10 практически пересекаются, а при t = –100 между ними нельзя вставить и атома. Свойства пространства на столь малых расстояниях вовсе не описываются евклидовой геометрией. Применение теоремы единственности в этой ситуации — явное превышение точности модели. При практическом применении модели это надо иметь в виду, иначе можно столкнуться с серьёзными неприятностями."
Так я их читал.
Обманывать нехорошо.
Как там дела с количеством людей для парадокса дня рождения? Вы согласны, что нужно 183 человека?
Вы путаете недоказуемость с контринтуитивностью. Можно (и нетрудно, те же диаграммы Эйлера в помощь) вывести основные формулы теории вероятности, подставить исходные числа и подсчитать. "парадокс заключается лишь в различиях между интуитивным восприятием ситуации человеком и результатами математического расчёта."
Не понял, откуда тут взялась дихотомия между аксиомами и вычислениями?
Ну как же, логические операции не позволяют ничего вычислять. Они позволяют только определить тавтологию.
То есть они могут определить, что если у нас есть состояние b, то применяя операцию F мы получим состояние b. F(a) = b
Но как доказать, что состояние x получается из a путём конечного количества применений функции F? Только выстроив цепочку преобразований, т.е. перебором.
У Фоменко тоже есть заслуги в математике, но это не делает его авторитетом в истории. Точно так же с Вольфрамом: заслуги в софтварной инженерии не делают его авторитетом в основаниях математики.
В том и дело, что у new kind of science есть практические результаты - вся книга их ему посвящена.
Какие результаты у Вопенки с Воеводским? «Там есть квадрат, но это нужно ещё доказать».
Вы упустили уточнение вопроса про невыводимые теоремы. Вопрос снят, или вы решили проигнорировать эту ветвь?
Переменный ток, который это всё освещает? Почти вся теория электрических цепей описывается комплексными числами.
Считал в школе задачки на переменный ток без комплексных чисел, нормально жил. Утверждаю, что это всё ненужные, воображаемые вещи.
Обманывать нехорошо.
Знаю, поэтому и не обманываю.
Вы путаете недоказуемость с контринтуитивностью.
Нет. Я вам наглядно показываю, насколько бредово определение доказательства как конструкта и социального феномена.
Можно (и нетрудно, те же диаграммы Эйлера в помощь) вывести основные формулы теории вероятности
Ненужное переусложнение ради интеллектуальной мастурбации, разве нет?
Ну как же, логические операции не позволяют ничего вычислять. Они позволяют только определить тавтологию.
Вычисление в данном случае — это приведение терма в нормальную форму, в чём вопрос-то? Или вы застряли где-то на уровне исчисления высказываний?
Но как доказать, что состояние x получается из a путём конечного количества применений функции F?
Конечного, но не заданного наперёд? Это уже совсем другой вопрос, с которым у вас будут проблемы даже в вашем подходе.
В том и дело, что у new kind of science есть практические результаты - вся книга их ему посвящена.
Нет, он там занимается в основном глубоким философствованием о сути бытия, и о том, что экспериментальная проверка вселенной-как-клеточного-автомата может быть выполнена, если упрощать. Практических результатов там абсолютный ноль.
Я был бы готов записать тьюринг-полноту правила 110 в практические результаты, конечно, но, учитывая вашу позицию, не уверен, что это будет для вас сколь угодно практичным.
Я не могу тратить силы на объяснение, почему у вас всё никак не получается пошутить. Даже Лакотос (которого вы не читали), понятный неглупому старшекласснику, для вас слишком сложный.
Поэтому вот вам вопрос на вашем уровне:
Комплексные числа позволяют достаточно просто описать и решить многие задачи электродинамики (более сложные, чем те, которые вы решали в школе).
Формулы теории вероятности позволяют достаточно просто подсчитать вероятность совпадения дня рождений (что невозможно сделать наугад).
Клеточные автоматы очень активно применяются в моделировании физических процессов ещё годов с 1970-х. Они быстрее и проще аналогов.
Даже Тьюринг свою модель машины строил как раз для того, чтобы сделать более наглядным и понятным решение задач, которые другим способом требовали бы огромных вычислений, в которых было бы невозможно разобраться.
Какие физические (или вычислительные) задачи позволяет короче и яснее решить вся это болтовня об основаниях математики, в которой уже 100 лет назад во всём мире могли разобраться 12 человек? Ну кроме задачи защиты ещё одной кандидатской диссертации.
Я не могу тратить силы на объяснение, почему у вас всё никак не получается пошутить.
Неужели нужно так много сил на высказывание «потому что пошутить нет цели»? Ведь у меня действительно нет цели пошутить, а есть цель показать, что ваш метод рассуждений приводит к очевидно бредовым результатам в более близким вам областям.
Впрочем, это требует от вас некоторых навыков абстрактного мышления, и, возможно, моя ошибка — априори ожидать этих навыков.
Комплексные числа позволяют достаточно просто описать и решить многие задачи электродинамики (более сложные, чем те, которые вы решали в школе).
Отвечу цитатой великих:
«Вся эта формализация [...] совершенно непонятна посторонним. Адекватному человеку совершенно непонятно, зачем погружаться во взятие интегралов вычетами, чтобы просто рассчитать цепь.»
И правда, кстати, посторонним относительно электродинамики формализация цепей через комплексные выражения совершенно непонятна.
Формулы теории вероятности позволяют достаточно просто подсчитать вероятность совпадения дня рождений (что невозможно сделать наугад).
Отвечу цитатой великих:
Вся эта формализация [...] совершенно непонятна посторонним. Адекватному человеку совершенно непонятно, зачем погружаться в эти формализации и разложения Хана ради конечно аддитивных сигма-алгебр, чтобы просто посчитать дни рождения.
И правда, кстати, ведь если бы это было понятно посторонним, то парадокс дней рождения не был бы парадоксом.
Клеточные автоматы очень активно применяются в моделировании физических процессов ещё годов с 1970-х. Они быстрее и проще аналогов.
Отвечу ци… пажжите, с 1970-х? Вольфрам свой интерес к клеточным автоматам начал с 80-х (зайдя с козырей и патентования правила 110 — очень научный подход). Вы походу сами себя переспорили.
И, кстати, с 50-х, ещё с фон Неймана.
Даже Тьюринг свою модель машины строил как раз для того, чтобы сделать более наглядным и понятным решение задач, которые другим способом требовали бы огромных вычислений, в которых было бы невозможно разобраться.
Такое сказать может только человек, знакомый с машиной Тьюринга только по первому абзацу википедии. Формализм Тьюринга не делает ничего ни понятным, ни наглядным, потому что программирование МТ — это ад.
Тоже вычёркиваем из практических применений.
Какие физические (или вычислительные) задачи позволяет короче и яснее решить вся это болтовня об основаниях математики, в которой уже 100 лет назад во всём мире могли разобраться 12 человек?
Мне даже далеко ходить не надо — теоркат даёт основания для Giry monad, что даёт вычислительные основания для сэмплирования и байесовского вывода в том же monad-bayes, которой я пользуюсь вот прямо сейчас.
Но давайте с другой стороны. Какие практические результаты дала теоретическая физика за последние, скажем, 50 лет? Какие продвижения были в вычислительной математике? Рунге-Кутте лет 120. Закрываем физику и математику и раздаём освободившиеся деньги бездомным?
зачем погружаться в эти формализации и разложения Хана ради конечно аддитивных сигма-алгебр, чтобы просто посчитать дни рождения.
Действительно, аддитивных сигма-алгебр тут не нужно, достаточно оснований математике, известных ещё древним шумерам.
Вероятность того, что у одного день рождения не совпадёт с днем рождения другого человека, равна 1 - 1/365. Дальше проверяем по несовпадение третьего и т.д. По индукции легко выводится общая формула.
Зачем здесь разложение Хана? Зачем алгебры подмножеств? А 2 + 2 сложить можно, если не знаешь, что ноль больше самого себя?
Формализм Тьюринга не делает ничего ни понятным, ни наглядным, потому что программирование МТ — это ад.
Если бы вы прочли исходную статью Тьюринга, то убедились бы, что никакого "программирование" там и нет.
теоркат даёт основания для Giry monad, что даёт вычислительные основания для сэмплирования и байесовского вывода в том же monad-bayes, которой я пользуюсь вот прямо сейчас.
С тем же успехом можно сказать, что до работ Пеано люди не умели считать, потому что не было оснований для арифметики.
Хотя вот когда французов начали учить по принципу "надо просто выучить определения" - проблемы начались уже и с арифметикой...
Основания могут быть очень разными, на то они и основания, чтобы доказывать то, что уже есть. Да вот только Giry monad появились задолго до формализации - а именно, в 1962, как метод решений конкретных задач: https://ncatlab.org/nlab/show/Giry+monad#history
Прямо так и написано:
I’d like to say that the idea of the category of probabilistic mappings, the document corresponding to that was not part of a seminar, as some of the circulations say, essentially it was the document submitted to the arms control and disarmament agency after suitable checking that the Pentagon didn’t disagree with it. Because of the fact that for arms control agencies as a side responsibility the forming of arms control agreements and part of these agreements must involve agreed upon protocols of verification. So the idea of that paper did not provide such protocols, but it purported to provide reasonable framework within which such protocol can be formulated.
Действительно, аддитивных сигма-алгебр тут не нужно, достаточно оснований математике, известных ещё древним шумерам.
Ура! Осталось понять, что и вам не обязательно доводить всё до абсурда в описании оснований математики.
Вероятность того, что у одного день рождения не совпадёт с днем рождения другого человека, равна 1 - 1/365. Дальше проверяем по несовпадение третьего и т.д. По индукции легко выводится общая формула.
Фигня какая-то, да и индукция пошла, а это уже основания математики. Не могу в этом разобраться, и все мои знакомые не могут. Придумки академиков, чтобы написать ещё один диссер.
У меня в «5В» классе вот меньше 183 человек, и дни рожденья ни у кого не совпадают. В соседнем «5Г» то же.
Если бы вы прочли исходную статью Тьюринга, то убедились бы, что никакого "программирование" там и нет.
Вы ранее написали:
строил как раз для того, чтобы сделать более наглядным и понятным решение задач
Исходная статья в этой формулировке не является ни необходимым, ни достаточным источником.
Или давайте по-другому: какие задачи стали более наглядны и понятны с машиной Тьюринга?
С тем же успехом можно сказать, что до работ Пеано люди не умели считать, потому что не было оснований для арифметики.
До работ Пеано (а также Пресбургера, и всех прочих, кто анализировал эту область) не было понятно, какие задачи имеет смысл пытаться решать, а какие — нет (потому что арифметика Пеано неразрешима, а Пресбургера — разрешима).
Да вот только Giry monad появились задолго до формализации
Это и есть формализация. Она появилась задолго до самой себя?
Какие физические (или вычислительные) задачи позволяет короче и яснее решить вся это болтовня об основаниях математики, в которой уже 100 лет назад во всём мире могли разобраться 12 человек?
Ну основная польза для физиков в том, что можно не переживать, что используя наши замечательные комплексные числа для электрических цепей мы не придём к двум разным решениям в одной цепи.
Это же в некотором смысле очковато писать физические модели с помощью уравнений, в которых мы оперируем с не очень хорошо проработанными объектами. Вдруг мы там что-то нарешали, диоды уже практически в производство отправили, а достаточно написать ещё 2-3 страницы, и спектр по уравнениям будет другим?
А уже суровые практики нам матумбу обеспечат.
Ну основная польза для физиков в том, что можно не переживать, что используя наши замечательные комплексные числа для электрических цепей мы не придём к двум разным решениям в одной цепи.
Да мы и так не переживаем... Добавили мнимую часть, решили линейную систему, выкинули мнимую часть ответа. Все.
Это же в некотором смысле очковато писать физические модели с помощью уравнений, в которых мы оперируем с не очень хорошо проработанными объектами.
Любая физическая модель неточна. Но математика тут совсем ни при чем.
Да мы и так не переживаем... Добавили мнимую часть, решили линейную систему, выкинули мнимую часть ответа. Все.
Это безответственность. Нельзя так работать. Впрочем, вы, кажется, даже не поняли моей реплики.
Любая физическая модель неточна. Но математика тут совсем ни при чем.
Это у вас безответственное отношение к работе. Настоящие физики, разумеется, знают, где их модель неточна и как уточнить, если потребуется.
Это безответственность.
В чем? Я сейчас про линейные электрические схемы.
Далее вторая часть марлезонского балета. Сначала мое высказывание:
Любая физическая модель неточна. Но математика тут совсем ни при чем.
Потом ваш ответ:
Это у вас безответственное отношение к работе. Настоящие физики, разумеется, знают, где их модель неточна и как уточнить, если потребуется.
Обидеть хотите? Вот с чего вы взяли, что я не знаю, где "мои" модели неточны? При том, что меня M&S R&D вот уже 25 лет очень хорошо кормит.
Ну и если вы утверждаете, что вот эти основы математики могут помочь в M&S, покажите хоть один конкретный пример, когда без них никак. А пока - не верю :)
В чем? Я сейчас про линейные электрические схемы.
И про них тоже.
Обидеть хотите? Вот с чего вы взяли, что я не знаю, где "мои" модели неточны?
Как не сложно догадаться, я вижу то, что написано. И контекстом о вас, скорее всего, не обладаю.
При том, что меня M&S R&D вот уже 25 лет очень хорошо кормит.
А полотна Ван Гога, как известно, прекрасно кормили массу людей, но не их автора.
И где мне их увидеть? Вот передо мной стол, стул и окно. Где там комплексные числа потрогать?
Риторический вопрос - разве можно увидеть даже не отрицательные, а обычные натуральные числа? Вот у меня на столе сейчас лежит один брелок от автосигналки и 3 батарейки 3А. Я их вижу и могу потрогать, а где можно потрогать число три или единицу?
Ну вы их посчитали, хотя бы, и можно сказать, что число «три» — это такой же концепт и так же относится к трём батарейкам, как концепт «собака» относится к вашей конкретной Жучке.
А вот отрицательные числа уже тоже проделки дьявола.
число «три» — это такой же концепт
Какая-никакая, а все же абстракция, руками не потрогаешь.
Не больше, чем абстракция концепта собаки, с чем умеют работать не только люди.
А вот с отрицательными числами, невычислимыми (в алгоритмическом смысле) вещественными, или уж тем более комплексными так не получится — у них нет прямых реализаций в реальном мире.
нет прямых реализаций в реальном мире
А электрический заряд?
А скорость вдоль координатной оси?
невычислимыми (в алгоритмическом смысле) вещественными
А диагональ квадрата?
А электрический заряд?
Не могу на ощупь отличить положительный от отрицательного.
А скорость вдоль координатной оси?
Испытываю только её (заведомо неотрицательный) модуль. Объективных координатных осей не существует в природе (чё-то там про принцип относительности Галилея), это человеческая абстракция.
А диагональ квадрата?
Я специально написал про «невычислимые вещественные» — это для которых не существует алгоритма вычисления. Диагональ квадрата вычислима, поэтому таких диагоналей счётное число (так как алгоритмов счётное число, очевидно). Следовательно, подавляющего большинства вещественных чисел (всё несчётное ℝ минус какое-то счётное множество) не существует.
А электрический заряд? Не могу на ощупь отличить положительный от отрицательного.
Тут можно привести пример столкновения электрона и позитрона, которые несут положительный и отрицательный заряд и просто исчезают при столкновении, высвобождая энергию, которую можно почувствовать.
Но насколько это хороший пример - не знаю. Вообще, никакие числа нельзя пощупать в природе, но можно делать вычисления с их учетом и пощупать много-много применений этих вычислений.
Тут можно привести пример столкновения электрона и позитрона, которые несут положительный и отрицательный заряд и просто исчезают при столкновении, высвобождая энергию, которую можно почувствовать.
Написал про это рядом.
Но насколько это хороший пример - не знаю. Вообще, никакие числа нельзя пощупать в природе, но можно делать вычисления с их учетом и пощупать много-много применений этих вычислений.
Мой поинт в том, что утверждение «эти ваши категории не нужны, потому что где их пощупать в природе», с которым я спорю в том или ином виде примерно с начала ветки — довольно странное, и такой логикой можно дойти до ненужности почти всей математики, кроме доступной трёхлетним детям.
А если, опять же, вспомнить ещё более странное утверждение о том, что доказательство — это социальный феномен, то всё становится ещё веселее.
Не могу на ощупь отличить положительный от отрицательного.
Не различаете на ощупь притяжение от отталкивания?
У Вас, похоже, беда с фантазией.
А если я ощущаю отталкивание, то у меня в руке положительный или отрицательный заряд?
Утверждаю, что отрицательных зарядов не бывает, а бывают заряды двух разных видов, которые, если зажмуриться, вместе образуют группу Гротендика поверх моноида натуральных чисел (которая единственна с точностью до изоморфизма, соответствующего переобозначению + ↔ -). Но зажмуриваться надо очень сильно, потому что даже объединение мюона⁺ и электрона не приводит к пустоте и нулю, а даёт мюоний, у которого есть очень нетривиальная квантовая структура, физически, измеримо отличная от таковой у объединения протона и электрона. А если предположить, что отрицательные числа имеют смысл, то и там, и там — ноль, и получаем, что 0 ≠ 0.
А если я ощущаю отталкивание, то у меня в руке положительный или отрицательный заряд?
А какая разница? Главное, что Вы можете их различить, и назначить один положительным, а другой - отрицательным.
Так это прямо означает, что отрицательность — это просто метка, как «лево и право». Лево и право существует объективно в природе в доступных человеку ситуациях?
Объективно существуют ситуации, когда необходимо различать "лево и право" и присваивать им удобные метки. Об одной из них мы только что поговорили.
Произвольность выбора (и особенно в случае бинарного лево/право в трёхмерном или даже двухмерном пространстве) показывает, что их не существует в реальности.
А в одномерном - не показывает. И там два направления объективно существуют.
В мире, где можно потрогать объективное отсутствие яблока, эквивалентное яблоку, только наоборот, отрицательные числа тоже «существуют».
А электрические заряды вы уже старательно забыли. Ясно-понятно.
Только отрицательный заряд — это не «отсутствие положительного».
В том и дело, что не отсутствие! Потому и приходится пользоваться для его обозначение отрицательным числом. Отрицательные числа - это не отсутствие положительных, а числа, отсчитанные в другую сторону от нуля.
Было бы "отсутствие" - можно было бы просто от этого "отсутствия" шкалу начать, как это сделали с абсолютной температурой.
Да, я неаккуратно выразился в прошлом комментарии.
Отрицательный заряд — это не обратный к положительному в математическом смысле. Я привёл пример выше со всякими там мюониями и обычными водородами, почему это не работает.
Термин "обратный" в математике значит совсем другое.
А электрический заряд положительный и отрицательный - противоположны друг другу именно в математическом смысле. И мы это видим непосредственно в законе Кулона и в правилах расчёта общего заряда группы частиц.
Термин "обратный" в математике значит совсем другое.
Обратный — это дающий единицу соответствующей операции. Обратный по сложению к x — это -x, обратный по умножению к x — это 1/x. Обратная матрица — это которая при умножении на данную даёт единичную.
А электрический заряд положительный и отрицательный - противоположны друг другу именно в математическом смысле.
А что такое «противоположны»?
И мы это видим непосредственно в законе Кулона и в правилах расчёта общего заряда группы частиц.
И что разваливается, как только вы начинаете рассматривать более тонкие характеристики системы вроде дипольного момента, и о чём я тоже писал выше про зажмуривание глаз.
как только вы начинаете рассматривать более тонкие характеристики системы вроде дипольного момента
А эти тонкие характеристики на электростатическое взаимодействие влияют?
Обратный - это 1/x (что может быть обобщено на матрицы). "Обратный к сложению" - пусть остаётся в верхних уровнях абстракции в вместе с "мультипликативным нулём". Для физики нужны более прикладные разделы математики.
А эти тонкие характеристики на электростатическое взаимодействие влияют?
Ну вообще-то да, и та же поляризация в общем незаряженного тела вылезает даже в школьных задачах.
Да и это неважно: сам ваш вопрос подразумевает, что вы согласны, что отрицательный заряд как обратный к положительному — это лишь человеческая абстракция (arguendo в рамках электростатики), не существующая в природе и призванная упростить какой-то класс вычислений.
"Обратный к сложению" - пусть остаётся в верхних уровнях абстракции в вместе с "мультипликативным нулём".
Вы же чуть ранее:
Термин "обратный" в математике значит совсем другое.
Вы же теперь:
Для физики нужны более прикладные разделы математики.
для физики
в математике
Ну лан.
Ну и, глядя на современную физику, я бы не был бы в этом так уверен, ну да ладно.
Ну вы их посчитали, хотя бы,
И что? Как потрогать число три? - никак.
Вы можете посчитать деньги которые вы отдали кому-то в долг- посчитать в обратную сторону и так вы посчитали отрицательные цифры. И что?
Ни положительные ни отрицательные ни иррациональные цифры потрогать нельзя. А что можно? - а можно всего ничего- использовать их в расчётах, то есть считать!
Это звучит как «собака — это кошка, только наоборот». Я не могу представить себе наличие денег и потом его инвертировать.
Я думаю, многие, кто взял кредит, ощущают на себе силу знака "минус" =)
Я не могу представить себе наличие денег и потом его инвертировать
Это понятно. Про "представление". Например пиво - берёшь ящик пива, там 20 бутылок. Можно потрогать. Посчитать. Тут и представлять не надо то. Ящик пива.
А когда пиво выпили, то представить то ноль как отсутствие пива уже трудно. Ни пощупать ни посчитать.
А если пришло 25 человек на вечеринку и пятерым пиво не досталось, то представить эти "минус пять" бутылок вообще немыслимо, поди.
P. S. Я вот и представить себе не мог, что в 21 веке на Хабре буду убеждать человека в реальности отрицательных (и иных "нереальных") чисел. Я думал что эту "проблему", - "проблему реальности любых чисел" математики решили по крайней мере 100 или даже 200 лет назад.
Я вот и представить себе не мог, что в 21 веке на Хабре буду убеждать человека в реальности отрицательных (и иных "нереальных") чисел.
Попробуйте перечитать ветку с начала и представить контекст, в котором вам приходится убеждать человека в реальности/осмысленности/применимости тех или иных инструментов математики.
Ладно, ветка далеко началась, так что я помогу: там началось с того, что вопросы оснований, фундамента математики не нужны на практике, не имеют смысла и всё такое. Я лишь показываю (как уже написал рядом), что в такой логике всё не нужно и не имеет смысла.
Я думал что эту "проблему", - "проблему реальности любых чисел" математики решили по крайней мере 100 или даже 200 лет назад.
Я не думаю, что математика вообще занимается проблемой реальности чисел. Это к тем, кому и ластики не нужны.
Я не думаю, что математика вообще занимается проблемой реальности чисел.
Было бы странно чтобы в 21 веке математики не перестали заниматься реальностью чисел, даже если до этого все века они этим вполне занимались. - я тоже так думал.
Но недавно в СМИ прошла инфа, что некие математики открыли (всегда мне интересно когда математики не "придумывают", а "открывают" типа что-то) аж ДВА новых типа бесконечности. - но, ок. - Но, другие математики НЕ признают это открытие их.
Причина не признания? - А типа из-за того что "Никому не нужны эти ваши ДВА новых типа бесконечности".
И тогда начинаешь понимать Почему Нобель не включил математику в своё завещание!
Но недавно в СМИ прошла инфа
Опять «учёный изнасиловал журналиста»?
Нет, опять @taujavarob читает жопой.
Математика ему - не в коня корм. Он тупо не понимает прочитанного.
Опять «учёный изнасиловал журналиста»?
В эпоху ChatGPT вы можете запросто сами дойти до исходника. Убедиться в правильности и попросить ИИ разжевать вам суть открытия. Поди.
Но тут мысль то главная иная - несмотря ни на что, математики по-прежнему ведут себя как люди, применяя "тяжёлую" артиллериию виде споров о "реальности " или "полезности" чего-то нового в математике.
А вот отрицательные числа уже тоже проделки дьявола.
Да не, шаг вперёд, шаг назад. Комплексные, очевидным образом, показываются просто шагом в бок. Я, конечно, читерю — это всего лишь векторные пр-ва, ведь умножение на шагах объяснять замудохаешься уже с отрицательными.
Тем не менее, отрицательные числа детям объясняются на числовой прямой, на шагах вперёд-назад (опыт двухмесячной давности). По крайней мере, становится понятно, зачем вводить эти минусы.
На ёрничание по-поводу существования чисел исключительно в голове отвечать не готов — много раз искал всякое в лесу, грибы были, чисел пока не довелось найти. Надежду не теряю, но пока не находил.
И где мне их увидеть? Вот передо мной стол, стул и окно. Где там комплексные числа потрогать?
Скорей всего, математика это такая же часть реальности, как и материя, время, пространство. .... Возможно она более мета-часть, чем другие. Но смысл в том. что она не зависит напрямую от ощущаемой нами реальности, а наоборот - является законами, по которым эта реальность существует.
Скорей всего, математика это такая же часть реальности, как и материя, время, пространство
Спор о том что такое математика не утихает. Я вот думал что 21 веке учёные пришли к мнению, что математика есть не более чем фантазии, типа сказки.
Но похоже до сих пор многие ищут в математике что-то иное.
Что касается "реальности чисел", то если под "реальностью чисел" понимать способность решать какие-то уравнения, в истории кстати и ноль и отрицательные сила и мнимые числа возникли не в размышлениях о том, а какие могут быть числа вообще, а из "возникновения числел" в решении конкретного типа уравнений.
А зачем математики решали свои уравнения?- спросите вы, поди.
Математики в те времена были подобно цирковым артистам, бродячим факирам, которые получали деньги за обучение математике других людей и за участие в математических дуэлях друг с другом.
Математическая дуэль заключалась а том, что один математик посылал другому математику с десяток задач.
Другой математик, если принимал эту математическую дуэль, то в ответ посылал свой десяток задач противнику.
Потом они сходились на людях где-то в залах университетов и показывали свои решения противнику на публике. - победитель получал денежный приз и простиж, - престиж, который использовал при претензиях на место профессора в универах.
Размышлять о математике ВНЕ решения уравнений никому в те времена и в голову не приходило.
Если же кому и приходило, то он молча писал свои работы в стол, как Гаусс или же запирался в актовом зале универа и мерил там углы в надежде что параллельные прямые на большом расстоянии всё же сходятся в реальности (этим занимался Лобачевский, за что его и гнобили и хотели признать сумасшедшим).
Я вот думал что 21 веке учёные пришли к мнению, что математика есть не более чем фантазии, типа сказки
Тогда, по аналогии, придётся признать, что любая другая наука "не более чем фантазии, типа сказки".
математики страдают вот такой вот хернёй
Не вижу в этом большой проблемы. Большинство людей большую часть времени страдает какой-нибудь хернёй.
Почему пресловутому оппоненту не угодили именно математики, а не, скажем, футболисты?
и за деньги
Крайне сомневаюсь, что кто-то где-то платит за никому не нужные задачи. Такими вещами люди в свободное время и за свой счёт развлекаются.
Россия оплачивает строительство пары храмов в день для РПЦ
Храмы - приносят деньги. Причём, потенциально - сколь угодно большие. Развивать тему не буду, чтобы не нарваться на "оскорбление".
США оплачивает публичные ЛГБТ оргии
Значит у этого есть выгодоприобретатель
Все подряд оплачивают так называемую деятельность так называемых математиков
Можете привести хоть один реальный пример, когда кто-то заплатил математику за ерунду, а не за практически полезную работу?
и те, кто ходят не жертвуют много.
А отчетность ведут? Как проверить сколько храм получил пожертвований?
тысячи математиков во всём мире бьются, получают на этой херне учёные степени.
Так я про деньги спрашивал, а не про усталость и учёные степени. Есть пример, когда они за это деньги получали?
Учёные степени даются не за сделанную работу, а за подтверждённую квалификацию. В этом смысл степени.
Для подтверждения же квалификации - традиционно используется какая-нибудь избыточно сложная ерунда.
Даже сварщик - на зачёт варит какую нибудь абстрактную геометрию, содержащую одновременно элементы всех практически полезных изделий, которые ему положено варить по квалификационным требованиям.
Не, полагаю, ваш оппонент о математике, как вещи в себе говорит.
"Страдания", на которые вы ссылаетесь, это такое развлечение, как и разложение чисел на множители. Однако ж, из этого выросли "простые числа" и большое количество их приложений. Наверняка за этими таблицами скрывается какая-то мощная и полезная теория. Возможно, непостижимая для современных мозгов, но постижимая через тысячу лет мозгами с аугментациями. И вопросы про эти таблицы будут тривиальными, на уровне школьной математики.
Я же, впрочем, не то подразумевал в своём комменте. А то, что раз "число" нельзя пощупать, и оно нереально, то придётся признать, что и физические величины тоже нереальны. Вот та куча камней - реальна, а абстрактных "5 килограмм" не существует. А так в каждой науке, потому что наука оперирует абстрактным, а не конкретным.
то придётся признать, что и физические величины тоже нереальны
В целом я с Вами согласен, с той поправкой, что физическая величина существует независимо от нашей способности её измерить. Две абстракции: числа и единицы измерения - не существуют за пределами нашего разума, но позволяют кодировать наблюдаемую величину.
Тогда, по аналогии, придётся признать, что любая другая наука "не более чем фантазии, типа сказки".
Нет. Аналоги не возникает.
Недаром Нобель не включил фантазии математикоа в номинацию на свою премию. Он понимал что такое математика и чем она отличается от других.
Математики обиделись и ввели свою премию. Кому и за что она присуждается вы можете спросить у ChatGPT. И возможно вы тогда поймёте что вашей аналогии нет.
параллельные прямые на большом расстоянии всё же сходятся в реальности (этим занимался Лобачевский, за что его и гнобили и хотели признать сумасшедшим).
Не надо пересказывать сказки. Не занимался Лобачевский ничем подобным.
А зачем математики решали свои уравнения?- спросите вы, поди.
Математики в те времена были подобно цирковым артистам, бродячим факирам, которые получали деньги за обучение математике других людей и за участие в математических дуэлях друг с другом.
Снова не выдумывайте. Математики решали уравнения в основном ради астрономических расчётов. Реже - в интересах артиллерии.
Все те уравнения, ради которых появились новые виды чисел, были либо из геометрии (геодезии, маркшейдерства), либо из небесной механики, либо из баллистики.
Математики решали уравнения в основном ради астрономических расчётов.
Верно. Были астрологами.
Но корень из отрицательного числа появился в результате решения кубических уравнений на математической дуэли.
"стали проводиться математические состязания, некое подобие дуэлей. Два математика посылали друг другу определённое число задач, кто больше решит, тот и победитель. И этот победитель не только получал звание великого математика, но и вполне мог занять весьма привлекательное в материальном отношении место математика при дворе герцога, короля, а то и самого Папы Римского. Так что сражаться было за что."
Вопрос был в том, почему математика так хорошо описывает мир, если она зародилась в сознании человека разумного? Тут могут быть разные версии, свою я высказал: то есть она сама по себе является реальностью, но просто реальностью другого типа, нами пока не познанной.
Я с Вами не согласен. Моя версия: Математика разработана людьми для того, чтобы описывать мир. Было бы странно, если бы она не делала того, для чего её создали.
Стоп стоп стоп.... Вопрос такой - почему этот мир хорошо описывается нашей математикой? Неужели это просто наша фантазия, удачно подогнанная под реальность? Но даже если так, то что тогда управляет процессами в реальном мире?
Потому что НАША математика специально РАЗРАБОТАНА НАМИ для того, чтобы хорошо описывать ЭТОТ МИР.
Вас же не удивляет, что программа, написанная, допустим, для управления станком, хорошо управляет станком? Что файловая система хорошо подходит для организации информации в виде файлов на носителе? Ничего удивительного, правда?
Математика - это тоже продукт человеческого разума. И она хорошо делает то, для чего её сделали.
удачно подогнанная под реальность
Я полагаю (хотя, могу и ошибаться), что не "удачно", а вполне целенаправленно подогнанная.
то что тогда управляет процессами в реальном мире?
А почему Вы думаете, что ими что-то должно управлять?
А почему Вы думаете, что ими что-то должно управлять?
Ну вы же не хотите сказать, что мир это Хаос? А если нет, то каковы его законы, какова его структура и взаимосвязи? Не надо уходить в метафизику, я говорю о том, какие реальные законы описывает наша математика? И не проще ли сказать (привет Оккаму), что они и есть математика?
Ну вы же не хотите сказать, что мир это Хаос?
Нет, я этого не хочу сказать.
А если нет, то каковы его законы, какова его структура и взаимосвязи?
Изучайте естественные науки. Они все на эту тему.
Вот только
Не надо уходить в метафизику
т.е. не надо притягивать за уши, что
они и есть математика?
Изучайте естественные науки. Они все на эту тему
Нет. Они описывают реальность на основе (грубо говоря) математики. Но они не изучают сам наш обсуждаемый инструмент познания. Более того, такой науки вообще еще нет! чувствую себя коперником Как не было раньше и других наук...
Они описывают реальность на основе (грубо говоря) математики.
Именно. Они математически описывают законы реальности (с известной точностью).
обсуждаемый инструмент познания
Это Вы про математику? Так я уже высказал: её придумали люди, причём, намеренно придумали её такую, какая нужна для см.выше.
Прежде, чем чувствовать себя коперником, может докажете, что вопрос, на который Вы ищете ответ, вообще правомерно ставить?
Они математически описывают законы реальности
Так про то и речь, чтобы дать этим законам право быть отдельной сущностью мироздания (наряду с материей, пространством, временем, ...).
может докажете, что вопрос, на который Вы ищете ответ, вообще правомерно ставить?
Не уверен, что смогу именно что доказать это. Но, раз Вы уже спросили, предоставьте, пожалуйста, формализм доказательств в этой области.
чтобы дать этим законам право быть отдельной сущностью мироздания
Не Вы ли просили не уходить в метафизику? Выходите из неё.
Вещество, поле, энергия, пространство, время.... Это разве метафизика? Хотя несколько тысяч лет назад так наверное и думали...
Не скажу на счёт вещества, пространства и времени (хотя, возможно, и они тоже), но поле и энергия - это абстракции, удобные для описания физических процессов.
Но физические процессы это ведь реальность? На что они опираются? Не на наши же закорючки.
Физические процессы - не опираются. Они просто происходят.
Происходят без каких либо закономерностей? С совершенно случайным выбросом значений?
С закономерностями. Но эти закономерности - это часть самих процессов. Они не хранятся нигде отдельно.
эти закономерности - это часть самих процессов. Они не хранятся нигде отдельно.
Какая именно часть? Откуда это известно? Что-то в школе нам таких подробностей не рассказывали.
Не уходите в метафизику. Покажите хоть один эксперимент, в котором закономерности существуют отдельно от процессов.
Они математически описывают законы реальности
В этом и загвоздка. Коммутативность сложения, которую проявляет например закон сложения сил, это закон реальности?
Очевидно, да. Сложение сил - коммутативно, насколько вообще реальны силы. Реальность, как говорится, дана нам в ощущениях.
Ну так, коммутативность - закон природы или выдумка?
Коммутативность ЧЕГО? Коммутативность сложения сил - реальна настолько, насколько реальны силы. Если считать силы реальностью, конечно, а не абстракцией, введённой для удобства записи законов динамики.
Других языков описания мира у нас нет, и здесь видно ошибку отбора: те вещи, которые описываются плохо, мы просто не рассматриваем (потому что, опять же, других языков описания у нас нет).
Других языков описания мира у нас нет
Вот именно, несколько тысяч лет человечество старается, а альтернативы пока нет и не предвидится. Значит дело не в наших стараниях?
те вещи, которые описываются плохо
Что вы имеете в виду? что-то не научное?
Вот именно, несколько тысяч лет человечество старается, а альтернативы пока нет и не предвидится. Значит дело не в наших стараниях?
Нет, просто все такие языки становятся куском математики, потому что математика — это про любые обращения с закорючками по правилам. Описание мира — это подмножество обращений с закорючками.
Что вы имеете в виду?
что-то не научное?
Поведение света до проработки математической теории за квантовой механикой, например, невозможно было описать математикой, равно как и поведение очень массивных или очень быстрых штуковин до проработки всей этой ерунды с пространствами Минковского и прочим. Гипотетический автор гипотетической статьи про unreasonable effectiveness из 18-го века просто проигнорировал бы соответствующий спектр явлений.
просто проигнорировал бы соответствующий спектр явлений.
Если бы это было так, соответствующие разделы математики не появились бы.
Нет, просто все такие языки становятся куском математики, потому что математика — это про любые обращения с закорючками по правилам. Описание мира — это подмножество обращений с закорючками
Согласен. Но вы говорите про человеческое описание мира закорючками, а я про то, как и где сам мир хранит свои правила (где они у него записаны). Ведь как то он их считывает-учитывает.
Поведение света до проработки математической теории за квантовой механикой...
Иногда математика будет опережать физику, иногда наоборот. Тут как повезет...
сам мир хранит свои правила (где они у него записаны). Ведь как то он их считывает-учитывает.
Это было бы верно, если бы мир был субъектом.
Но поскольку мир не субъект - сама формулировка, что он что-то делает - неправомерна.
Если убрать некоторую одушевленность из моих слов, то по смыслу ничего не изменится.
Вы предполагаете, что правила - это самостоятельная сущность, отдельная от самих процессов.
Нет ни одной причины так считать.
Эти правила имеют более общую природу, чем каждый отдельный процесс сам по себе. Что и дает возможность для предположений.
мем 27 кб
Предполагать можно только то, что можно когда-нибудь проверить.
В данном случае, сходство формул происходит из-за трёхмерности пространства.
Предполагать можно только то, что можно когда-нибудь проверить.
Да ладно! Неужели греки говорили об атомизме, надеясь проверить его вот-вот скоро?
В данном случае, сходство формул происходит из-за трёхмерности пространства
Это не сходство, это полная идентичность. И никакого отношения к размерности пространства она не имеет.
Неужели греки говорили об атомизме, надеясь проверить его вот-вот скоро?
Так они и правы не были.
Это не сходство, это полная идентичность. И никакого отношения к размерности пространства она не имеет.
Что, тоже в школе не рассказывали? Квадрат в знаменателе, по вашему, откуда?
А числитель идентичен - только до погрешности.
Выше вы писали
Математика разработана людьми для того, чтобы описывать мир
А законы Кулона/Ньютона не для того ли придуманы?
В 3-мерном пространстве, площадь сферы - R^2, и поэтому он в знаменателе.
Мало чем отличается от правил абстрактной алгебры, где у умножения и сложения такие свойства, которые постулируются в математике, чтобы работала физика.
Так они и правы не были
Ну, в таком случае, тогда вообще никто и никогда не был прав и не будет прав, так как все знание со временем устаревает. Но это же получается бессмысленный подход.
Квадрат в знаменателе, по вашему, откуда?
А, вы про это, ок. Тогда в одномерном знаменателя не будет, в двумерном будет первая степень расстояния и т.д. А в числителе произведение характерных величин. Но я не про размерность пространства (хотя эту тему, если постараться, можно и там развить).
Я про саму формулу (для нашей мерности пространства), которая универсальна для любого подобного взаимодействия. Вот эта универсальность (а еще и универсальность по мерности пространства) и дает почву для соответственных предположений.
Я про саму формулу (для нашей мерности пространства), которая универсальна для любого подобного взаимодействия.
Какого «подобного»? Какая там формула у слабого и сильного взаимодействий, кстати?
Ну так там же разный характер взаимодействующих величин: количество (масса, заряд), качество (цвет), наличие( е+) - все трое принципиально разнотипные, поэтому и формулы разные. Ведь слово "взаимодействие" это неправильная абстракция (слишком общая) для моего примера.
У меня есть чувство, что вы пытаетесь сказать «взаимодействия, описываемые этой формулой, почему-то описываются этой формулой».
Да, а что не так?
Скорее так : здесь, здесь и здесь работает одна и та-же формула - почему? Что их объединяет?
Да, а что не так?
И это труизм, а труизмы скучные.
Скорее так : здесь, здесь и здесь работает одна и та-же формула - почему? Что их объединяет?
Отсутствие эффектов вроде конфайнмента.
Но это вопрос уровня «почему видов взаимодействий четыре», ИМХО, особенно учитывая их объединение. Собственно, есть шанс, что в GUT это просто будет разными близкими проявлениями одной сущности, но я о GUT знаю так, по популярным рассказам, поэтому не смогу поддержать этот разговор.
И это труизм, а труизмы скучные
Вопрос "почему яблоко падает на землю" тоже может выглядеть скучно.
Отсутствие эффектов вроде конфайнмента
Так весь вопрос в том, как происходит переход от отсутствия эффектов к их наличию. Где и как храниться безэффектовая составляющая. А ведь она есть (вы сейчас это сказали)!
Но это вопрос уровня «почему видов взаимодействий четыре»
Смотря на каком уровне отвечать на этот вопрос. Если на физическом, то это GUT. Если чисто на математическом, то это просто закорючки (с их внутренней логикой). Может есть еще другой уровень ответов? И пока неважно, это будет новая абстракция или реальная часть мироздания. Ведь, как минимум, это интересно. Как максимум....
Вопрос "почему яблоко падает на землю" тоже может выглядеть скучно.
Вопрос «почему яблоко падает туда, куда оно в итоге упало» действительно скучный. Почему — по определению.
Так весь вопрос в том, как происходит переход от отсутствия эффектов к их наличию. Где и как храниться безэффектовая составляющая. А ведь она есть (вы сейчас это сказали)!
GUT покажет.
Может есть еще другой уровень ответов?
Как проверить? ;)
Вопрос «почему яблоко падает туда, куда оно в итоге упало» действительно скучный. Почему — по определению
Векторы вышли из чата.
GUT покажет
Вангую, что Теория всеобщего объединения не будет открыта в рамках современных физики и математики (привет Эйнштену). Скорее сработает подход Макса Тегмарка. Делаем ставки...
Как проверить? ;)
Более точный вопрос - кто проверит? Ну не я же)) Я больше по инфоцыганству в этой области.
Более точный вопрос - кто проверит? Ну не я же)) Я больше по инфоцыганству в этой области.
А кто ж ещё? Тебе надо - ты и проверяй. А мы примем по умолчанию гипотезу, что ты не прав.
А кто ж ещё? Тебе надо - ты и проверяй. А мы примем по умолчанию гипотезу, что ты не прав.
Я так понимаю, что какой-то процесс в этой области идет. Если интересно, ознакомься, присоединяйся. Ну или оппонируй, это тоже полезно.
Дело не в том, что знания устаревают. А в том, что даже если греки случайно угадали - это не является правотой. Потому что они никак не проверили свои утверждения, а просто сказали наобум
Возвращаемся к вопросу, с какого момента математика становится "научной". Мне, кстати, это не очень интересно (даже не знаю почему), поэтому эту линию беседы поддержать не смогу.
А что если эта формула - просто первый член ряда, которым аппроксимируется настоящий закон взаимодействия?
Вау, так ты на моей стороне? Приветствую тебя, товарисч!
Никого же не удивляет, что для любой формулы её аппроксимация рядом из заданного числа членов отличается только коэффициентами
Пиши статью, обсудим.
Возвращаемся к вопросу, с какого момента математика становится "научной".
Дело в том, что не бывает "научности в целом". Есть два принципиально различных класса наук, которые не пересекаются. Естественные науки, которые описывают окружающую реальность, и абстрактные науки, которые сам по себе от реальности абстрагированы, а занимаются разработкой инструментов для естественных наук.
Если попростому, то физика отвечает на вопрос "что", а математика на вопрос "что, если".
Вау, так ты на моей стороне?
Не могу ответить, потому что пока что твоя "сторона" выглядит как-то по наркомански.
Ты хотя бы понял, что такое "ряд" и что такое "первый член"?
Есть два принципиально различных класса наук, которые не пересекаются
Речь, конечно, шла не про структуру научных знаний, но тут соглашусь.
Не могу ответить, потому что пока что твоя "сторона" выглядит как-то по наркомански
Забей. Наркоманов надо избегать.
Ты хотя бы понял, что такое "ряд" и что такое "первый член"?
Какой учебник 9-го класса посоветуешь?
Дело не в том, что знания устаревают. А в том, что даже если греки случайно угадали - это не является правотой. Потому что они никак не проверили свои утверждения, а просто сказали наобум.
Знаете что такое брутфорс? Допустим, мне надо подобрать пароль из семи букв. Если я просто сгенерирую все комбинации этой длины, я всё равно не буду знать, какая из них верна, пока не начну проверять их на том, для чего пароль подбирается.
Греки в своё время нагенерировали достаточно идей, чтобы хоть одна да подошла. Это невеликая заслуга, как и генерация всех комбинаций выше.
С античных времён до наших дней прослеживаются только те идеи, которые проверили сами авторы. А другие идеи - такие, как атомизм, - по сути пришлось открывать заново.
Я про саму формулу (для нашей мерности пространства), которая универсальна для любого подобного взаимодействия
А что если эта формула - просто первый член ряда, которым аппроксимируется настоящий закон взаимодействия? :)
Никого же не удивляет, что для любой формулы её аппроксимация рядом из заданного числа членов отличается только коэффициентами.
Но вы говорите про человеческое описание мира закорючками, а я про то, как и где сам мир хранит свои правила (где они у него записаны). Ведь как то он их считывает-учитывает.
Я склонен считать сегодняшние гипотезы и рассуждения на эту тему фундаментально ненаучными, потому что они ни на что не влияют.
А вообще вам в математическую мультивселенную Тегмарка и ко, где это у него финальный, четвёртый уровень иерархии мультивселенной, и где разные вселенные в этой мультивселенной отличаются управляющими (порождающими?) их математическими законами.
Я склонен считать сегодняшние гипотезы и рассуждения на эту тему фундаментально ненаучными, потому что они ни на что не влияют
Сейчас не влияют. Ну так и теория струн ни на что не влияла (но еще не вечер). Да и куча современной (и не только) математики ту да же. Разве не так? А про какой-нибудь Вояджер я вообще молчу. А Коперник?
А вообще вам в математическую мультивселенную Тегмарка
Все уже отрыто до нас Спасибо за наводку! Даже статья на Хабре есть.
Сейчас не влияют.
Я говорю о влиянии в контексте обсуждаемой ветви науки. И да, «сегодняшние» там было не просто так.
Ну так и теория струн ни на что не влияла (но еще не вечер). Да и куча современной (и не только) математики ту да же.
Истинность (или ложность) математических утверждений вполне себе имеет влияние на математику как науку о закорючках.
Теория струн не влияет как физическая теория (слишком много свободных параметров, можно подогнать к более-менее любым результатам экспериментов, нулевая физическая предсказательная сила), но это интересная математическая теория (где экспериментом является не проверка соответствия наблюдаемым физическим данным, а проверка соответствия дерева вывода логического утверждения правилам логики).
Разве не так? А про какой-нибудь Вояджер я вообще молчу.
Вояджер уж тем более даёт наблюдаемые данные.
Математическая мультивселенная же непроверяема и (пока что) не даёт предсказаний как физическая теория.
которые невозможно ни доказать, ни опровергнуть, ни даже понять.
Почему? В книге по теории типов, вполне четко объясняется параллель между теорией типов и реальной математикой, и дается конкретный пример теоремы Безу. И сама теория типов тоже довольно четко выстроена (на уровне метатеории).
Как быть с математическими объектами, состояние которых на определённой итерации в принципе непредсказуемо без вычисления предыдущих
Можете взять любой учебник по теории автоматов и ознакомиться. Игра жизни - это клеточный автомат. Отлично она формализуется, как и Машина Тьюринга. Они все довольно четко выражены в теории множеств. Трудность может быть только в том, чтобы конфигурацию машины Тьюринга в конкретный момент времени, и потом задать правило перехода от предыдущей к последующей
А никак. Этому не учили.
Обучение и развитие человека намного шире и может выходить за рамки того, что "учили".
Можно же обучаться самостоятельно (по книге или курсу), а также внутри IDE или симулятора. А еще можно проводить исследовательскую работу.
Вы боретесь с ветряными мельницами.
Абстракция над абстракцией нужна для поиска более общих инструментов работы с абстракциями. Всего навсего.
Если у кого-то там сектантский апломб - Вам-то что за беда? Отвечать сектантским апломбом на сектантский апломб - нездоровая манера.
Собственно, я уже итак довольно глубоко проработал эту область и прошел 2/4 курса из специализации на Курсере по дизайну и анализу алгоритмов от Стендфордского университета в 2022 году. Моя главная цель — это не только комфортное прохождение алгоритмических собесов и сильная позиция на рынке, но еще и возможность брать более крутые и интересные задачи.
Если вы закончили университет в 15 году (примерно 10 лет назад), то примерно к 40 годам вы такими темпами станете стажёром в Яндексе. (именно на тамошних собеседованиях, которых станет к тому времени где-то 7-8 подряд, вам и может пригодиться знание дизайна и анализа алгоритмов)
20 лет я учился недаром,
Пыль наук не напрасно глотал.
Есть теперь у меня, чем гордиться -
Мой оклад, как у дворника стал!
На стажера спрашивают совсем-совсем простые алгоритмы вроде цикла for по массиву.
Ваше сообщение составлено без опыта собеседований и понимания реальной ситуации на рынке, а также без знаний ситуации с алгоритмическими собеседованиями. Например, в некоторые команды Яндекса принимают по сокращенной программе собеседований, в которой только 2 технических (алгоритмических) собеседования. По личному опыту, я проходил в команду Яндекс.Медиасервисы в 2021 году на 17-й грейд (это эквивалент Синьера). И там не было чего-то особо сложного, среднего уровня типовые задачи.
Расскажите больше о вашем "понимании реальной ситуации на рынке". Где и когда срочно стали требоваться специалисты по Coq и эндофункторам?
В некоей отечественной финтех-конторе технари аппрувят кандидата после слова "Coq" (умение или готовность его изучить и применить). Если добавить "Rust" (лучше - реальный скилл) - Вы приняты (если не запорете интервью с менеджментом) :)
Но название этой конторы никто не знает
Знают, и очень хорошо. Начинается на "Ex... "
Видимо знают в неких очень узких кругах.
Да вот же она: https://career.habr.com/companies/excorp
Там так и написано: "для нас твои 5000+ часов в CS являются конкурентным преимуществом"
В каждом втором блокчейне. IOHK (которые cardano), например, много чего на агде делают. Кое-какие другие блокчейны имеют или разрабатывают формализации на coq/isabelle/etc.
Как выглядит доказательство правила Де-Моргана (¬(A ∧ B) ⇒ (¬A ∨ ¬B)) на самом низком уровне
Прежде всего, спасибо за статью. Тут очень много всего, не мало интересного и есть даже что-то полезное)))
Теория множеств - это больше про классификацию объектов, в частности, про отношение таких классификаций. Из неё пытались соорудить фундамент всея математики, но получилось не очень.
Поэтому попробовали развить теорию типов - у каждого терма есть свой тип, что позволяет проверять корректность алгоритмов, опираясь на утверждения об отношениях типов. И это, конечно здорово, но пришлось расширять теорию вселенными типов, включать в неё и значения... В общем, выяснилось, что "обычных" типов маловато, чтобы свести концы с концами.
Теория категорий - раздел топологи, позволяющий формализовать различные утверждения о путях. Между множествами, классами, типами, значениями и практически всем, что можно вообразить. Для программистов и других физиков прежде всего важны пути вычислений, в частности, задача о нахождении оптимального алгоритма. До сих пор идут исследования о роли множеств в теории категорий... Но ИМХО тема всё равно интересная.
В связи с этим вопрос: зачем вообще пытаться реализовать теорию множеств в теории типов, с её аксиомами выбора и проч.? Например, для тех же действительных чисел куда полезнее понятие типа, чем множества. И вообще зачем заморачиваться с неконструктивной математикой, если априори известно, что это бесполезный математический онанизм?
но получилось не очень.
Почему не очень? Вроде неплохо получилось, технически все сходится и выводится. Иногда очень долго и не всегда красиво, но все равно оно работает и адекватной замены аксиоматической теории множеств я пока не вижу. Ну разве что, coq вроде неплохо через индуктивные типы многие штуки представляет.
зачем заморачиваться с неконструктивной математикой, если априори известно, что это бесполезный математический онанизм?
А все классические учебники по анализу\теории вероятности, они же сильно неконструктивные, там каждая третья теорема использует аксиому исключения среднего в явной или неявной форме. Если только конструктивный подход использовать, есть учебник по конструктивной теории множеств и конструктивному анализу, но мне они показались весьма экспериментальными...
На сколько помню, появление теории типов было обусловлено тем, что теория множеств приводила к парадоксам, которые не позволяли считать её надёжным фундаментом. Требовался другой язык для целей формализации корректности алгоритмов.
Получается, что неконструктивная математика важна только потому, что на неё опираются старые учебники?)) Выглядит так, что любые неконструктивные теоремы попросту бесполезны, потому что... неконструктивны! Это просто демагогия, когда в фундаменте всех рассуждений лежит аксиома "потому что можем и всё тут!" Проверка каких-либо условий для частных случаев не даёт алгоритмов получения таких результатов, что обесценивает эту проверку.
Прощу прощения за наивность суждений, я дилетант в математике) Но надеюсь, что меня или переубедят, или согласятся со мной (или пошлют в правильном направлении)))
появление теории типов было обусловлено тем, что теория множеств приводила к парадоксам
Это было самым-самым началом. Потом теорию множеств пофиксили и сейчас в ZFC нет парадоксов
что обесценивает эту проверку.
Я бы не сказал, что обесценивает. Но тут надо уточнить, что вы имеете в виду под неконструктивной математикой? Вы не признаете аксиому исключения третьего, или шире понимаете неконструктивность?
Я понимаю конструктивное доказательство так: это последовательный вывод утверждения по правилам на основании начальных условий и базовых аксиом. Например, доказательством обитаемости типа является только предоставление его экземпляра (корректный алгоритм его вывода, завершающийся за конечное время), а не какое-то иное доказательство того, что тип НЕ необитаем. Аксиома выбора также бесполезна с практической точки зрения - если нет универсального (для любого множества) алгоритма выбора его элемента, то тут и говорить не о чем.
А можете раскрыть более подробно пункт про практическое применение конструктивной математики по сравнению с неконструктивной? Единственный пример что я знаю, это то, что из конструктивных доказательств можно потом в Coq синтезировать программы. Но если я доказываю всякие штуки из теории чисел, например? Какой там плюс?
"Доказать", и "вывести" (получить алгоритм вывода) - это разные цели. Они совпадают только в случае конструктивного доказательства. Алгоритмы полезны тем, что их можно переиспользовать - они помогают в решении целого класса задач с разными начальными условиями. Неконструктивные доказательства бесполезны. От слова "совсем". Вы можете "доказать всякие штуки из теории чисел", но в этом не будет никакого смысла, если вы при этом опираетесь на аксиому "потому что!" и не получите алгоритмов для решения каких-либо практических задач.
Каждая статически-типизированная компьютерная программа представляет собой доказательство выводимости значения типа-результата, если есть значение (утверждение истинности!) типа-начального-условия. Т.е. корректная с точки зрения синтаксиса языка программа по факту является конструктивным доказательством своей корректности. Доказать такую программу-теорему можно ещё до её исполнения.
А вот иное доказательство того, что тип программы A => B не является пустым типом, но при этом сама реализация (значение типа A => B) не предоставляется - неконструктивно. Это просто бесполезное доказательство.
Про аксиому выбора - да, все верно, она неконструктивна
Я пытаюсь найти мотивацию, чтобы полностью отказаться от неконструктивной математики, но пока что не получается...
А у меня курс матанализа начинался с теории множеств и CFT (там лемма Цорна страшна), из нее легко выводятся натуральные числа и их аксиомы
Глубоко понять, как устроен реальный мир на низком уровне. У меня еще со школы сохранилась мечта — написать программу, которая из законов квантовой физики выводит таблицу Менделеева и предсказывает химические реакции, а также закладывает фундамент химии.
Про таблицу Менделеева вроде еще в школе рассказывают, электронные орбитали, валентные электроны, принцип запрета Паули и вот это вот все.
в ближайшем будущем я могу попробовать освоить и формализовать дифференциальные уравнения
Что значит освоить дифференциальные уравнения?
Развитие в менеджмент. У меня сложилось впечатление, что хорошие менеджеры (особенно топ‑менеджеры) — это весьма образованные люди и они максимально используют математику в работе. Речь идет не только о простом статистическом анализе данных, но еще и о построении и проверке гипотез, использовании инструментов Data Science, а также применении всяких интересных штук типа Теории Игр/Теории оптимизации/Линейного программирования для принятия крупных стратегических решений.
А на основании чего у вас сложилось такое впечатление? Что-то не верится что топ-менеджеры рассказывают вам как они принимают "крупные стратегические решения".
Собственно, можно попробовать развиваться по этому пути и заработать очень много денег
Воротилы бизнеса уже держат мешки с деньгами наготове для математического менеджера.
электронные орбитали, валентные электроны, принцип запрета Паули и вот это вот все
Хотелось бы разобраться, откуда это все следует
А на основании чего у вас сложилось такое впечатление?
Личный опыт и общение с такими людьми, а также чтение их статей и истории их жизни\карьеры
Воротилы бизнеса уже держат мешки с деньгами наготове
Ну вообще для DataScience-спецов держат, а это оно и есть
Большое спасибо за статью! Я даже восстановил доступ к Хабру впервые за 10 лет, что бы оставить комментарий.
Получив диплом Математика-Программиста я должен с сожалением признать что не доказал сам ни одной теоремы и ни разу не использовал фундаментальные знания за 15 лет работы FullStack разработчиком.
Хотя я помню свое потрясение на семинаре по уравнениям мат. физики (удивительно, но там стоит "хорошо") когда понял что каждая точка реальности может быть формально определенна во всех смыслах.
Но при этом вынужден увидеть себя скорее в категории "менеджеров которые не очень сильны в алгоритмах" и больше получают удовольствия от использования софт скилов и настройки процессов команды для работы с клиентами, и построения грамотной архитектуры при существующих ресурсах.
При этом я отношу себя к тем самым фанатикам которые будут ночью кодить пет-проект на LLM с агентами, потому что это круто, интересно и вообще.
Но опустим)
Если позволите добавить еще одно возможное применение, тк хотелось бы услышать ваше мнение на этот счет.
Мне кажется что сейчас все еще очень слаба программная база для работы с квантовыми компьютерами.
И если бы получилось создать систему, которая при заданных параметрах компьютера (кол-во кубитов, методы работы с ошибками, и тд.) и заданных критериях инференса (время работы) смогла бы доказательно найти оптимальную архитектуру ML модели (для решения заданной задачи (например MNIST), то это могло бы действительно фундаментально изменить всю область ИИ.
Звучит, как интересная алгоритмическая задача, решаемая при глубоком понимании математической модели квантовых вычислений, а также предметной области ML. Но я не погружался в эту область, так как пока квантовые компьютеры сидят в очень узких лабораториях.
Если ML действительно будут запускать на квантовых компьютерах, то я 100% буду осваивать эту область. Но пока (насколько я понял) ML запускают на процессорах с архитектурой видеокарты типа NVIDIA, так что я бы скорее почитал про что-то типа CUDA
Кстати, есть еще квантовая машина Тьюринга =)
мощный обзор
Вот тут неточность
Также, есть комбинаторная логика, в которой всего 3 символа (комбинатора) S, K и I. Было доказано, что любые правила выведения типов можно свести с этим 3-м
к 2-м, 3 - избыточно
Интересно, спасибо. Может стоит разобраться как это работает и вывести правила мат. логики полностью на комбинаторах
Ох ты, и 1-го оказывается достаточно (спасибо ermouth)
Если вы знаете среду (или язык программирования), которые совместимы с не типизированным лямбда исчислением и позволят формализовать содержимое главы в них и проводить вычисления\проверки, то обязательно напишите об этом в комментариях.
А чем типизированная не годится? Y-комбинатор просто вводится дополнительно.
Да и вроде в хаскеле довольно легко делается обвязка для интерпретации. (в учебнике была)
Достаточно одного, iota combinator. https://en.m.wikipedia.org/wiki/Iota_and_Jot
совет автору. Математика, это инструмент. И как от всякого инструмента, от нее тогда будет польза, когда имеются обстоятельства, в которых он полезен. И тут важны практика и опыт. Собственно сам совет, поставьте перед собой задачу, решение которой имеет конкетную (материальную) пользу, например, ускорить в несколько раз (скажем, на порядок) некие важные вычисления. И решайте ее используя все возможные знания и подходы. И самое главное, не бросайте искать ответ при наличии трудностей.
Я думаю, что скорее восстание машин начнется, чем я успею защитить диссертацию...
Зависит от - если выбрать целью именно диссертацию, то успеете. Нужно только понимать, что а) все описанные цели, скорее всего, недостижимы, а распыляться очень не советую и б) фундаментальные знания математики в прикладной сфере малоприменимы, так что есть шанс потратить время впустую. Но свой мозг точно разовьете, это однозначно, так что успехов.
На данный момент его библиотека самая большая
а есть пруф? хотелось бы понимать как сравниваются разные солверы.
Онлайн-библиотеки типа MML, смотреть\сравнивать можно
Подозревая, что MML это не michigan/missisipi municipal league, не Martin Monsen Regiona Library и не Miller Memorial Library хотелось бы получить более развернутый ответ про сравнение. Пока что "100 теорем" единственное, где имеется хоть какое-то сравнение, но это не сказать чтобы всеобъемлющее сравнение для вышеупомянутого утверждения.
Статья шикарна!
Скажите, а я правильно понимаю, что в ZFC за счёт аксиомы регулярности не может существовать Универсального множества?
Фундаментальная математика — теория всего в IT и не только. Теория типов и формализация в Coq