Сука, картинку распидорасило.
На /матх, небыдло!
освятил
Что они делают, автоматически доказывают математические теоремы? Как это выглядит на практике?
Они автоматически не доказывают, это уже скорее область всяких https://github.com/FStarLang/FStar и https://github.com/Microsoft/dafny. Но в общем случае доказательство за конечное время сгенерировать нельзя, поэтому даже этим двум надо постоянно подсказывать.
Это пруверы же лишь проверяют корректность доказательств. Что, впрочем, очень и очень неплохо.
Можно ещё доказывать свойства программ, если язык формализовать https://en.wikipedia.org/wiki/Formal_verification#Software
На практике выглядит как текстовый редактор с "кодом" на особом языке, который строит доказательство определённых утверждений о формальной системе. Можешь глянуть книжку Software Foundations для простого введения.
Примеры верификации программ: https://en.wikipedia.org/wiki/Formal_verification#Industry_use
Продвинутое тестирование, значит?
Я какое-то время назад делал свой мета-язык, goviaji. На нем можно определять свой язык программирования, писать на этом новом языке программы, проверять корректность их синтаксиса и типизации, и выполнять их. Все это определяется на простой мета-логической системе (похожей на упрощенный Пролог), а операции выполняются с помощью простого поиска доказательств в глубину. На пиках примеры goviaji-кода.
https://github.com/sorrge/goviaji
Сейчас пересмотрел код свежим взглядом. Во-первых, хотелось бы сделать отдельный пруфчекер, чтобы можно было записывать и проверять отчеты о корректности исполнения. Но самое главное - адски медленно. Для вычисления некоторых простых выражений на Church Numerals требуются минуты. Нотя там всего несколько тысяч шагов в выводе. Унификация, по-видимому, очень медленная. Вот думаю как это улучшить. На кресты можно переделать, там кода мало, будет наверное раз в 1000 быстрее. Но мне нравится Питон, прежде всего его легкая кроссплатформенность. Может, можно как-то радикально улучшить производительность алгоритмически? Я уже запоминаю хеши всех доказанных утверждений, чтобы не доказывать многократно. Но все равно медленно.
И хотелось бы комментариев уважаемого борщекоммьюнити по поводу проекта.
https://github.com/sorrge/goviaji
Сейчас пересмотрел код свежим взглядом. Во-первых, хотелось бы сделать отдельный пруфчекер, чтобы можно было записывать и проверять отчеты о корректности исполнения. Но самое главное - адски медленно. Для вычисления некоторых простых выражений на Church Numerals требуются минуты. Нотя там всего несколько тысяч шагов в выводе. Унификация, по-видимому, очень медленная. Вот думаю как это улучшить. На кресты можно переделать, там кода мало, будет наверное раз в 1000 быстрее. Но мне нравится Питон, прежде всего его легкая кроссплатформенность. Может, можно как-то радикально улучшить производительность алгоритмически? Я уже запоминаю хеши всех доказанных утверждений, чтобы не доказывать многократно. Но все равно медленно.
И хотелось бы комментариев уважаемого борщекоммьюнити по поводу проекта.
Эх помню были времена гонял конструктивного петушка в самом его логове можно сказать. Тред этот не взлетит, как и прошлый в сущности, инфа соточка. Надо было пилить в math, там бы хотя бы были шансы треду продержаться неограниченное количество времени за счет того что активность там на несколько порядков меньше. Если только конструшок не заглянет на огонек и не разразится немереный срач; но думаю в этот раз не будет этого.
Пройдусь немного по пруверам и расскажу разных морозных, может кому-нибудь будет интересно.
Отмечу что каждый язычок на перебой соревнуется с другими какую бы похитрожопее систему модулей придумать.
fstar
Сложилось впечатление что проект уже мертв и даже начал разлагаться и пованивать. Неслабо наебался с его установкой. Не помню уже деталей, но дошло даже до того что я под прыщами скачал докер-образ и запускал его из докера. Самая мякотка в том что приложенные примеры выдают ошибки. И я не знаю дело ли в том что они просто забили на эти примеры (что плохо) или еще нужны какие то неведомые настройки которых я не понимаю (что тоже плохо)
Очень смешной пример комьюнити в котором жизнь бьет ключом
https://www.reddit.com/r/fstar/
lean
Ощущения примерно как от fstar, хотя проект поживее наверное за счет того что где то внутри MS некоторая небольшая группка еще подкидывает дровишки, но ставить на него мне совсем не хочется.
Тоже долго с ним ебался чтобы завести. Сначала я по собственному недоумению открывал в vscode папку в которой у меня лежит несколько проектов. А оказывается делать этого ни в коем случае нельзя, а надо открывать по принципу одна папка - один проект, чтобы все что нужно автоматически подгрузилось.
Хотел побаловаться с проектами xena и mathlib. Вываливается куча ошибок о том что такой-то модуль (на деле практически вообще каждый модуль) использует sorry. Хотя я заглядываю в сорс и вижу что никаким sorry там не пахнет. Следовательно мелкокогении решили таким образом информативно свалить все ошибки в одну корзину. Ну что ж бравО.
Самый пиздец - оно ТОРМОЗИТ и ебет процессор вообще не переставая. И жрет дохуищи памяти. Хотя задумка же была написать все на плюсах чтобы летало. Я даже собрал уже проект mathlib. И оно бздело ошибками несколько часов. Но работать быстрее в итоге ничего не стало почему то. Может дело в моей криворукости. Хотя видел комментарии что мол проблемы с производительностью у людей действительно есть.
agda
Самый главный подводный камень агды - это конечно же ебаный кусок гнилого кала под названием emacs. Как же у меня бомбит от того что для каждого элементарного действия нужно сыграть целое соло на клавиатуре. Диды во времена телетайпов напридумывали какой то невероятной поебени, поэтому хуй тебе а не адекватные шорткаты вроде ctrl+c ctrl+v которыми пользуется весь мир. Выход по ctrl+c ctrl+x - блядь серьезно? Или ctrl+p ctrl+n для перемещения - я просто хочу чтобы мне как в том кинце с Джимом Керри выжгли тот нейрон в который попала эта информация из самого тупорылого туториала на свете.
Хотя я понимаю что у имакса есть свои преданные фанаты. И что их даже не беспокоит гарантированный туннельный синдром. Или что имакс можно настроить вообще совершенно как угодно если только разобраться. Но у меня просто нет вообще никакого желания ебаться еще и с этим в дополнение ко всему прочему.
Так же мысль про модули тут особенно актуальна. Потому что в агде в сущности как я понял нет стандартной библиотеки и сразу с порога нужно поебстись чтобы ее "воссоздать".
Прошел несколько глав Стампа. Потом пробовал запустить их же в другом линуксе где стоит версия агды поновее и они нихуя не запускаются. Остается теперь держать старую версию пока не покончу с этой книгой наверное.
Еще осилил где то треть лекций макБрайда. Была там забавная история. В конце лекции, которая идет перед лекцией, которая называется чтото типа "комедия непреднамеренных ошибок", он доказывает один кейс и оставляет другой по аналогии. И когда я стал пере-проходить эти упражнения и дошел до этого кейса жестко на нем встал. Для меня стало делом чести его забороть ведь вроде совсем ничего сложного. Тут еще не помогало что в агде то я разбираюсь далеко не так хорошо как хотелось бы. Ну и как то все наложилось. Ебался целый день. Уже блядь выть начал как животное и головой биться. Думал вообще с ума сойду нахуй.
А следущую лекцию он начал с того что этот кейс далеко нихуя просто так не доказывается. И все дело в том что там очень важен порядок паттернов при определении функции. Он его поменял и все заработало как часики. Он потом объяснил что к чему подробно. Но честно скажу вот так в голове провернуть какой нужен порядок паттернов в нетривиальных конструкциях чтобы доказывалось все как надо я не смогу. В целом вышел весьма поучительный экспириенс, но и довольно болезненный.
coq
Пока мой самый любимый петушок. Устанавливается за пять секунд, в руке лежит как влитой, быдло очень боится (тест на олдфага). Никаких особых проблем с ним не было. Правда и никаких больших проектов я с ним не пробовал запускать. Только прошел курс SF. Курс btw вообще заебок, в какой то степени изменил мое мироощущение, можно сказать.
Поглядывал на NuPRL. Рыскал по сайту полчаса, не меньше. Вроде раньше можно было скачать виртуалку гигов в 20 с ним. А сейчас они вместо этого предлагают использовать их сервера по инвайтам. Короче, отложил я тогда знакомство до лучших времен.
>Как же у меня бомбит от того что для каждого элементарного действия нужно сыграть целое соло на клавиатуре.
Пользоваться evil религия не позволяет?
>Выход по ctrl+c ctrl+x - блядь серьезно?
Вообще-то C-x C-c но зачем выходить из имакса, бака?
>Или ctrl+p ctrl+n для перемещения
Это стандартные кнопки для перемещения курсора в консоли Unix. Ты терминалом пользуешься вообще?
Вся суть борщетредов. Расписал стену текста про пруверы, в ответ три камента про то какие кнопки надо нажимать в редакторе. Причем советы, скорее всего, неверные, т.к. комментаторы, очевидно, никогда не пользовались обсуждаемыми программами и даже не знают, для чего они предназначены. Да и сам постер стен текста только запустил примеры и, поглазев на ошибки, удалил.
Да. Если совсем на языке тестов, то фишка в том, что такое тестирование позволяет покрыть все случаи.
Только те, на которые есть спецификации, и, как правило, лишь с довольно узкой точки зрения корректности результата. Например, спецификация может определять, что результат функции, вычисляющей длину списка, не может быть отрицательным. Если функция не завершается, то обычно верификатор этого не заметит и скажет что все ок. Не говоря уже о том, что вычислительную сложность пока вроде ни один верификатор не осиливает, и реально не работающий из-за конской сложности код пройдет все проверки.
>F*
Там же вроде только refinement types, не? Оно тогда не совсем прувер.
Помню, что у него очень кривой режим для Emacs, который в одном случае выдаст ошибку, а в другом скажет, что всё чекнулось.
Ещё помню, что экстракт в F# работает через жопу.
>Тоже долго с ним ебался чтобы завести. Сначала я по собственному недоумению открывал в vscode папку в которой у меня лежит несколько проектов. А оказывается делать этого ни в коем случае нельзя, а надо открывать по принципу одна папка - один проект, чтобы все что нужно автоматически подгрузилось.
Там совершенно черезжопная система пакетов. Потыкай https://github.com/Kha/elan, может понравится. Но я не тыкал, я ебусь через LEAN_PATH и прочие костыли.
>Хотел побаловаться с проектами xena и mathlib. Вываливается куча ошибок о том что такой-то модуль (на деле практически вообще каждый модуль) использует sorry. Хотя я заглядываю в сорс и вижу что никаким sorry там не пахнет. Следовательно мелкокогении решили таким образом информативно свалить все ошибки в одну корзину. Ну что ж бравО.
sorry собственно может и не являться им, а быть тактикой admit или незакрытым hole.
>Самый пиздец - оно ТОРМОЗИТ и ебет процессор вообще не переставая. И жрет дохуищи памяти.
Да, это пиздец, и разработчики не отрицают. Почему писанный на плюсах прувер так тормозит и жрёт память — загадка.
>Если функция не завершается, то обычно верификатор этого не заметит и скажет что все ок.
Сейчас в каждом втором прувере эвристики проверяют завершимость.
>Так же мысль про модули тут особенно актуальна. Потому что в агде в сущности как я понял нет стандартной библиотеки и сразу с порога нужно поебстись чтобы ее "воссоздать".
Там чуть ли ни каждый сделал себе по стандартной библиотеке.
Есть вроде как стандартная (https://github.com/agda/agda-stdlib), но нет гарантий, что рандомно взятый туториал будет использовать другую.
Эвристиками и корректность можно проверить. Тесты называется. Весь поинт верификации в доказательствах, если их нет то и никакой верификации нет. А их нет.
Ты хочешь, чтобы компьютер за тебя пруфы писал что ли?
А чем
> ctrl+p ctrl+n
лучше вот этих клавиш: ↑, ↓?
>борщетредов
>хлебателей борщей
> борщекоммьюнити
А при чем здесь борщ? Помогите знать мемы, чтобы не быть батхертом
Так как работы по этой хуйне нет и не будет, зарплатой у тебя будет мамин борщ
Если я все правильно понял, это больше для профессиональных математиков тема, а не разработчиков ПО, хотя тут пишут, что можно для улучшения качества тестирования использовать эти штуки.
Было бы неплохо.
> Почему писанный на плюсах прувер так тормозит и жрёт память — загадка.
Как раз таки ничего удивительного, плюсы - это кобол 21 века.
Тем, что не нужно двигать предплечье и убирать руки с homerow, а значит можно пользоваться слепой десятипальцевой печатью.
+
>И что их даже не беспокоит гарантированный туннельный синдром.
Надвно смотрел серию видосиков по погромированию, где чувак писал в каком-то непопулярном редакторе, и иногда открывал емакс. А в одном видосе он сидел в каких-то ортопедических перчах и тут я заржал знаю, грешно Хороший мем, кароче
Да что-то как-то неубедительно, мне не нужно смотреть на клавиатуру, чтобы найти стрелки.
Еще докину немножко
Idris
К системе как к софту нареканий нет, как минимум чтобы поиграться - устанавливается без проблем, ресурсов как не в себя не жрет. Поддерживаются официально vim и atom. Так что можно как белый человек с ней поиграться. Не помню что там с модулями, но думаю что у Бреди и тут все схвачено.
Но как прувер ее использовать это довольно отчаянная затея. Хотя, какие то умельцы перевели часть курса SF на сабж. Помню пробовал поиграться с тактиками и был весьма расстроен. Вроде бы rewrite не поддерживал обратного направления или указания места или еще что. Но это уже все не важно, т.к. тактики теперь депрекейтед и веместо них элаборатор. Думаю, интересная штука, надо бы с ней поиграться.
Еще я собрал всю волю в кулак и за 10 часов осилил "Type-driven Development with Idris - Edwin Brady". Но в целом экспириенс вышел так себе. Элементарное ФП я и раньше знал, а вот с более продвинутыми конструкциями вроде коиндукции не уверен что до конца разобрался.
Не могу себе представить чтобы я или вообще любой человек не начинающий день с размышлений об устройстве теории типов увидев проблему в виде конечного автомата набросал бы первым делом этот автомат на уровне типов (а не на уровне значений), набросал бы на изичах что то на подобии пикрелейтед и вообще регулярно использовал методологию описанную в книге.
Isabelle
Отмечу что сам редактор на жабе отжирает гиг памяти при запуске и ML ядро отжирает еще гиг. Вообще систему компактной не назовешь. Но при этом работает все более-менее отзывчиво, прямо летает по сравнению со связкой vscode+lean. Во времена когда чатик может отжирать несколько гигов это наверное пустяки.
После петуха такие ощущения, простите уж за странную аналогию, как если после своей уютной и по уму обставленной простенькой квартирки попадаешь в роскошные пестрые хоромы. Вроде бы гораздо бохаче. Но нахуй это все надо - не понятно.
Еще у меня полный диссонанс вызвает обилие кавычек расставленных как будто случайно.
Думаю надо бы пройти concrete semantics, но все руки не доходят.
Metamath
А вот это довольно компактненькая системка. Этим она подкупает. И нестандартным подходом к доказательствам через рерайтинг. На сайте у них все как то свалено в кучу. Немного потыкался и так и не придумал куда двигаться дальше.
Решил что попробую чтобы набить руку просто повторить все манипуляции из этого видео
https://www.youtube.com/watch?v=Rst2hZpWUbU
И я почти добрался до qed, но их горюшко редактор на жабе выбросил эксепшон и был таков. Сил начинать заново у меня уже не было.
>Metamath
Я вдохновлялся этой системой при создании goviaji. Автор и его сподвижники немного двинутые на некоторых вещах. Например, основной целью своей деятельности они видят переписывание учебников матана на свою систему, причем в их представлении записи в их системе должны быть максимально похожи на то, что в книгах. Вроде как чтобы студенты могли учить матан по их системе вместно книг. Получается, мягко говоря, не оче, и, естественно, ни один человек в здравом уме не начнет учить матан по их системе и не посоветует это делать другим. Еще мелочи вроде фиксации на сжатом текстовом виде представления доказательств. Изначальный автор вроде был категорически против пруф ассистантов, тактик и тому подобного, все надо было писать руками, так ему казалось более духовно будет. Зацикливались на поиске кратчайших доказательств. Ну кароч сильно своя атмосфера там, хотя люди с виду умные.
Самое интересное там для меня это базовая система. Там даже скобки не встроены в синтаксис, система лишь манипулирует последовательностью символов. Скобки определяются как и все остальное, правилами. Но если копнуть поглубже, тоже есть подводные камни, вроде связанных переменных, какой-то системы типов не очень внятного толка. Я уже сейчас не очень помню деталей, но мне не понравилось. Я сделал goviaji на более стандартной и гораздо более понятной базе деревьев и унификации. Если бы можно было выкинуть из их системы эту неочевидную муть, я бы перешел на нее, но она вроде бы необходима и в конечном счете является костылями для ручной реализации унификации.
Пацаны, а чем эта ваша хуерга лучше wolfram mathematica?
Наверное, тем что математика и доказательство теорем символьной алгеброй (причем, прибитой гвоздями к проприетарному языку и со своими багулями) не ограничивается.
Равно как не ограничивается нерадивой школотой, использующей её что бы домашку аналитически с выкладками порешать, чтобы училка одобряе и ленивыми инженеграми, использующими символьную алгебру для того же.
Сохацкий, це ті?
>goviaji
Говяжий?
А есть доказательство корректности реализации goviaji ?
Да, анус.
Нет. Как и нет доказательства корректности реализации чего бы то ни было еще. Так если подумать, вообще никаких доказательств нет. Что могут доказать лысые обезьяны с помощью своих животных звуков?
Увы, мы можем лишь уповать на то, что в более простой программе меньше вероятность ошибок. Вот, например, в metamath ядро парсера и пруфчекера довольно маленькое и, что важно, простое. Но, на мой взгляд, не настолько простое, как могло бы быть, хотя тут уже возможны разные мнения: простоту трудно точно определить. goviaji это попытка сделать по-другому, по возможности еще проще.
С этой т.з. другие пруверы проигрывают: там в качестве базовой логики выбирается, как правило, очень богатая система, с кучей правил (еще попробуй найди точное определение), каких-то тонких моментов (авторы обычно их замалчивают для ясности - чего людей техническими деталями пугать?), и довольно трудной и запутанной реализацией.
Что за "курс SF", который ты всё время упоминаешь?
Software foundations чтоле?
Да, конечно, он самый.
Единственный его недостаток, на мой взгляд, это то что уж больно там дохуя всего. Проходил я его ну очень долго, в основном из-за собственного распиздяйства, не буду даже писать сколько чтобы никого не пугать. Пока дошел до середины, зашел глянуть на их сайт, они все переворошили и несколько глав добавили. Когда я проходил было около 40 глав.
Вообще я считаю что совершенство - это когда нечего убрать. Но они придерживаются похоже противоположной философии и курс постоянно разрастается как раковая опухоль. Уже на четыре книги разбили.
Еще есть похожий (но явно покороче) курс от Вадлера на агде:
https://plfa.github.io/
> не буду даже писать сколько чтобы никого не пугать
После того, как я на SICP потратил год с хуем, меня уже ничего не напугает.
Пересматривая код, внезапно нашел еще одну проблему в своей реализации простых языков на goviaji. Если рассмотреть термы
lambda x. y
lambda x. false
то с т.з. простого синтаксического анализа y и false это одна и та же категория, т.е. у меня это "переменные". На самом деле false может быть константой языка, для него могут быть определены какие-то правила, а может и не быть. Но, например, предикат для определения свободных переменных в терме никак не сможет узнать, есть ли что-нибудь особенное у false или нет. В моем коде false всегда будет считаться переменной. Сейчас там все работает и так, но реально внутри программы полная чушь происходит из-за этого. В metamath сделали типы "переменная" и "константа", и заставляют пользователя определять тип для каждого используемого имени.
Альтернативно, можно всегда переменные оборачивать в специальный функтор, например:
lambda (var x). (var y)
или делать это специальным префиксом, как в пхп каком-нибудь. Но по сути это то же самое, разве что локальный синтаксис.
Сейчас у меня есть список того, что не может быть переменной, туда всякие ключевые слова занесены. Можно в этот список внести все константы. Проблема в том, что этот список принципиально нельзя расширить: он определяется один раз, одним предикатом. Это из-за того, что в моей монотонной металогике добавлением новых правил нельзя сделать ложными какие-то утверждения, которые были истинными до этого. Например, если variable false было истинным, то оно всегда останется истинным, какие правила ни добавляй.
А это значит, что нельзя по-простому расширить язык, добавив новые правила. Например, я (неправильно) расширял лямбда-исчисление типом bool и конструкцией if-then-else, добавив правила для нового синтаксиса и семантики. По идее нужно сделать так, чтобы bool, true, false, if, then, else больше не считались переменными. Но это невозможно из-за монотонности. Получается, что определение языка не может быть полностью реюзабельным: по крайней мере список констант придется каждый раз декларировать заново. Мне от этого неуютно.
lambda x. y
lambda x. false
то с т.з. простого синтаксического анализа y и false это одна и та же категория, т.е. у меня это "переменные". На самом деле false может быть константой языка, для него могут быть определены какие-то правила, а может и не быть. Но, например, предикат для определения свободных переменных в терме никак не сможет узнать, есть ли что-нибудь особенное у false или нет. В моем коде false всегда будет считаться переменной. Сейчас там все работает и так, но реально внутри программы полная чушь происходит из-за этого. В metamath сделали типы "переменная" и "константа", и заставляют пользователя определять тип для каждого используемого имени.
Альтернативно, можно всегда переменные оборачивать в специальный функтор, например:
lambda (var x). (var y)
или делать это специальным префиксом, как в пхп каком-нибудь. Но по сути это то же самое, разве что локальный синтаксис.
Сейчас у меня есть список того, что не может быть переменной, туда всякие ключевые слова занесены. Можно в этот список внести все константы. Проблема в том, что этот список принципиально нельзя расширить: он определяется один раз, одним предикатом. Это из-за того, что в моей монотонной металогике добавлением новых правил нельзя сделать ложными какие-то утверждения, которые были истинными до этого. Например, если variable false было истинным, то оно всегда останется истинным, какие правила ни добавляй.
А это значит, что нельзя по-простому расширить язык, добавив новые правила. Например, я (неправильно) расширял лямбда-исчисление типом bool и конструкцией if-then-else, добавив правила для нового синтаксиса и семантики. По идее нужно сделать так, чтобы bool, true, false, if, then, else больше не считались переменными. Но это невозможно из-за монотонности. Получается, что определение языка не может быть полностью реюзабельным: по крайней мере список констант придется каждый раз декларировать заново. Мне от этого неуютно.
>Потому что в агде в сущности как я понял нет стандартной библиотеки и сразу с порога нужно поебстись чтобы ее "воссоздать".
Ну здраститя. Их аж две - agda-prelude https://github.com/UlfNorell/agda-prelude и standard-library https://github.com/agda/agda-stdlib и даже три, еще iowa agda library, но установка несколько аутичная с неочевидными моментами (мне даже Норелла пришлось трясти на предмет почему его поделие (prelude) ошибки выдает, оказалось, для агды 2.5.4.2 нужно использовать бранч 2.5.4.2-compat). Как по мне, в агде и идрисе интереснее всего т.н. "дыры", в коке чего-то такого очень не хватает.
>Самый главный подводный камень агды - это конечно же ебаный кусок гнилого кала под названием emacs
Ну она и без емакса работает, в атоме. Но клавиатурные комбинации там те же, так что формально - обмен шила на мыло.
>Пока мой самый любимый петушок. Устанавливается за пять секунд, в руке лежит как влитой, быдло очень боится
Кок в виде установщика под винду малополезен, хотя там с ним и ставится полторы либы. Вся петушиная сила доступна только под линуксом, где можно и стандартные либы ставить и конпелять нестандартные.
>Нет. Как и нет доказательства корректности реализации чего бы то ни было еще. Так если подумать, вообще никаких доказательств нет. Что могут доказать лысые обезьяны с помощью своих животных звуков?
Нафига тогда тебе вообще пруверы, если конструктивизм, на котором все они основаны, начинается с признания математики подмножеством животных звуков лысых обезьян? Без антиплатонизма в этой теме вообще делать нечего.
Ну все верно. y и false - свободные переменные. Хочешь, чтобы они стали связанными - пили окружение, или абстрагируйся.
Посоны, как сделать, чтобы Coq экстрактил в тупль из прелюдии, а не создавал data Prod a b = Pair a b?
Мне нужно сделать так, чтобы некоторые имена не были свободными переменными. Связать их тоже не с чем, это должна быть константа сама по себе, определенная с помощью правил вывода, например
eval (if false then T2 else T3) T3
То есть все отличие false от y в том, что для false есть такие правила, а для y нет. Ну и это не работает, вот.
>или абстрагируйся
Вот этого не понял.
Вообще я уже придумал, как это решить с помощью derived forms. Все константы заменяются на термы с маркером, что это константа:
false = (constant c_false)
Тогда константы легко отличить от переменных, не зная конкретных имен. Так же и с ключевыми словами вроде if. Теперь расширения языка можно делать, добавляя новые derived forms и правила. В выражение lambda x. false в чистом лямбда-исчислении false будет переменной. А если доопределить язык булами, то оно будет преобразовано в lambda x. (constant c_false) и будет иметь другую семантику, как лямбда всегда возвращающая константу false.
> символьной алгеброй
А обсуждаемые системы для этого подходят?
>Их аж две .. и даже три
Получается они не такие уж стандартные
>но установка несколько аутичная
О чем и речь.
По поводу атома - не понимаю как я мог его пропустить. Возможно, что когда я смотрел, примерно год назад, там не было полной функциональности вроде кейс-сплита. Или даже более вероятно, что перебирая разные сочетания пруверов и редакторов я просто проскочил этот вариант. Но, спасибо за наводку.
>Но клавиатурные комбинации там те же
Да имхо лучше бы было хотя бы ctrl+alt+X как в идрисе-атоме.
>Кок в виде установщика под винду малополезен, хотя там с ним и ставится полторы либы. Вся петушиная сила доступна только под линуксом, где можно и стандартные либы ставить и конпелять нестандартные.
По мне так сложности возникающие под виндой весьма преувеличены. В основном они возникают когда требуется запустить нечто слепленное из говна и палок баш скриптами или заточенной под какую то чисто линуксовую функциональность. И от того что разрабы совершенно кладут на винду хуй, конечно же.
Вот например установка агды под винду это еще тот цирк. Можно либо через кабал установить, либо инсталлером. Я конечно же не ищу легких путей и попробовал оба варианта и могу сказать что они оба в принципе работают. Для меня только великая загадка почему разрабы сделали инсталятор все-в-одном с хаскелл-платформой и всем-всем-всем, но не сделали отдельный блядь инсталятор агды под винду т.е. такой в котором были бы только нужные бинарники. Я "в ручную" извлек с помощью msi-экстрактора нужные файлы из их огромного инсталятора и получил вроде бы работоспособный вариант.
Правда в итоге возник затык в самом неожиданном месте - со шрифтами. И я плюнув на все запустил бубнту в виртуалке.
Я тут отхожу от темы треда, но уже не могу остановиться. Современное положение с установкой софта вообще никуда не годится. Совершенно неприемлемо что любая программка может писать и читать вообще куда угодно на диске и размазывается тонким слоем по всей системе.
Так же меня весьма раздражают дот-файлы. Очень порадовал недавний пост на реддите, а то я реально думал что я один такой у кого люто бомбит со всей это точечковой хуиты.
https://www.reddit.com/r/programming/comments/amp06h/dotfile_madness/
Мак купи себе, там прям как ты хочешь.
Но я ведь не пидор.
К тому же традиция дристать дот-файлами идет явно из юникс-вея и для макбучных хипстерков тоже является нормой.
>К тому же традиция дристать дот-файлами идет явно из юникс-вея
Щито ты несешь. XDG_xxx давным-давно есть. То что криворукие нехорошие девелоперы кладут на это хуй и хуячат куда попало - это проблема криворуких нехороших девелоперов.
>любая программка может писать и читать вообще куда угодно на диске
Не может.
1 Идея здравая, более чем. Реализовано все через сраку, как обычно.
>LibreOffice Windows x64 MSI: 238 MB
>LibreOffice snap: 1.1 GB
Но может еще получше сделают
>Snappy Is Finally Doing Something About Super Large App Sizes
2. Нет не заебусь. Чистейший фад.
>XDG_xxx
Только всем насрать.
>Не может.
Нет, может. Ты наверняка намекаешь на модель "безопасности" которой прыщеглазики так гордятся. Эта модель чистейшей воды безумный манямирок и профанация. См. пикрелейтед.
Ну ты можешь радоваться что программа спрашивает у тебя разрешения чтобы раздристаться по диску. Ты можешь его не давать и не устанавливать программу. Такая то швабодка.
Не угадал, попробуй ещё раз.
> Вот например установка агды под винду это еще тот цирк. Можно либо через кабал установить, либо инсталлером.
Через stack все ставится в одну команду. Главное, чтобы учетка винды была без русских букв. В инсталлере старая версия, а кабал вообще для наркоманов. Но да, Идрис вот на винде правильно сделали, распаковываешь архив и все сразу работает.
> По мне так сложности возникающие под виндой весьма преувеличены. В основном они возникают когда требуется запустить нечто слепленное из говна и палок баш скриптами или заточенной под какую то чисто линуксовую функциональность.
Ну и как из виндовского установщика кока поставить хотя бы либы из opam репозитория? В бубунте opam install vst и вуаля, а как тот же vst в винде накатить?
opam на винде хуже cabal’а.
>Мне нужно сделать так, чтобы некоторые имена не были свободными переменными.
Это достигается созданием окружения, например, где-то в division в коболе, лол описываешь все возможные константы языка. Либо твоим способом с синтаксической заменой, но в твоем способе нельзя использовать constant как часть языка.
Сохацкий, це ті?
Опять не угадал.
Сохацкий, це не ті?
Я не Сохацкий.
А вот в goviaji прувер бы запомнил, что ОП не Сохацкий, и не доказывал бы больше одного раза.
Кстати, на тему корректности реализации: отладил неочевидный баг в прувере недавно, который раньше не проявлялся. Наверное, там еще есть.
Кстати, на тему корректности реализации: отладил неочевидный баг в прувере недавно, который раньше не проявлялся. Наверное, там еще есть.
Этот Сохацкий говорит, что он не Сохацкий.
Это не Сохацкий
Нет, это Сохацкий.
А вы ведь знаете про Эйфель?
Он вообще не про это.
Там рядом есть интересные разработки как AutoProof, AutoFix
Мне‐то лучше знать.
Агда интересна ещё тем, что в следующем релизе (а в нынешней девелопмент версии уже есть) будет cubicaltt искаропки. В кок, Идрис и остальные пруверы это завозить вроде пока вообще не собираются (?).
...потому что тi Сохацкий?
Нет.
я сохацкий
Трипл хуйни не скажет.
>Идрис
В это говно точно нет, там и HoTT никогда не будет.
Шидрис же как язык для «хуяк‐хуяк и впродакшон» позиционируется.
Он и как "хуяк-хяук" - говно полное.
Лучше сразу Coq взять и в Haskell его экстрактить.
Можете в двух словах сказать зачем все это нужно? Вы тут все ученые, что ли?
говно для академиков, не обращай внимания.
в проде здоровые люди это использовать никогда не будут
> в проде здоровые люди это использовать никогда не будут
Будут. Лет через 30. Не как отдельный прувер, конечно, а как фичу продакшн- быдлоязыка типа той же джябы или что там будет в моде.
и через тридцать лет не будут. нахуй не нужна корректность, нужно фичи пилить - быстро, дёшево, и чтобы хоть как-то работало
>нахуй не нужны ваши циклы и функции, нужно фичи пилить, чтобы хоть как-то работало
>нахуй не нужна ваша портабельность, нужно фичи пилить, чтобы хотя бы как-то на той же системе работало
>нахуй не нужен ваш сборщик мусора, нужно фичи пилить, чтобы быстро и хоть как-то работало
>нахуй не нужны ваши модули, текстовых инклюдов хватит всем и вообще нужно фичи пилить, чтобы хоть как-то работало
>нахуй не нужны ваши лямбды, нужно форичи пилить, чтобы хоть как-то работало
>нахуй не нужны ваши тайпклассы, нужно фичи пилить, чтобы хоть как-то одним классом реализовать интерфейс и все как-то работало
>нахуй не нужна ваша иммутабельность, нужно фичи пилить, чтобы на одном ядре хоть как-то работало
>нахуй не нужны ваши монады, нужно фичи пилить, чтобы копипастить код и рассказывать на собесах про паттерны и чтобы хоть как-то работало
...
>нахуй не нужна корректность, нужно фичи пилить - быстро, дёшево, и чтобы хоть как-то работало
всё что нужно - это циклы, функции, простые структуры данных + что-то реально полезное, как например в го сделано. поэтому он и популярен. хотя смысл расписывать "элитарию" вообще, ему же шашечки нужны, а не ехать
Я Сосацкий и я создал этот тред.
> всё что нужно - это циклы, функции, простые структуры данных + что-то реально полезное
Т.е, кроме С вообще ничего не нужно, я тебя понял. Однако, куча всего есть и активно используется в продакшене. Я к чему, даже не сомневайся, что на яп с корректностью, тактиками, автозаполнениями дыр итд, хипстеры налетят только в путь. Ещё и наперебой орать будут "ебаный бабай, как жи мы без всего этого раньше жили?!". Дело только в том, чтобы сделать все это доступным любой макаке с соевыми мозгами. Тот же Идрис нихуя не для широких масс и уж тем более не для продакшена, хуй там даже хеловорлд напишешь и поймешь написанное без минимальных познаний в теории типов.
Этот пиздит.
А ты докажи.
Как? Отправить sup‐коммит в мою репу на жидхабе и сдиванониться?
>Как?
Откуда мне знать? Это ты тусуешься в пруф-треде!
>Откуда мне знать?
Так и иди нахуй, раз не знаешь.
Нет, ты!
А вот Сохацкий наверняка знает.
Ну так спроси у него.
Мдауш, в любом треде про пруверы от половины постов - про Сохацкого. Знатно он дегродам дупы разворотил, долго его ещё анальные погорельцы помнить будут.
Я знаю про Сохацкого только то, что написано ИТТ. Но черт возьми, мне этот парень уже нравится!
Сохацкий, это же ты, да?
Нет, Сохацкий это я.
>Знатно он дегродам дупы разворотил, долго его ещё анальные погорельцы помнить будут.
А что было то, напомни?
А кто такой Сохацкий?
Профессиональный гуру?
Зачем мне твиттер? Я знаю, что такое твиттер; я спрашиваю, кто такой Сохацкий?
Ты по твиттеру не можешь информацию разыскать что ли?
Так мне не нужна информация по твиттеру, с твиттером я знаком (а с Сохацким - нет).
Он, типо, просто хачкель хуесосит?
Кто?
Сохацкий, це тi?
Единственная проблема с пруверами - никто не знает теорию типов достаточно для того, чтобы придумать ей хоть какое-то практическое применение. Всякая быдлота уровня местных тыжпрограммистов максимум на что способна в плане теории типов - гореть от Сохацкого, который на них ссать не хотел. Какие-то практические идеи даже обсудить не с кем. Вы хоть сами осознаете, какое вы дно?
А ты кто?
Ты какой-то булшит пишешь. По делу есть чо?
Тебе никто ничего не собирается доказывать, научись думать своей головой и не строй обиженку.
>придумать ей хоть какое-то практическое применение
А зачем ей практическое применение? Или это специфика /pr?
>гореть от Сохацкого
Зачем обращать на него внимание? Вся его активность в теории типов -- создание собственного бренда. Ничего полезного он не сделал.
>Какие-то практические идеи даже обсудить не с кем.
А что ты можешь предложить, кроме оскорблений?
> Тебе никто ничего не собирается доказывать,
А где я прошу мне что-то доказать? Я просто факты констатирую.
> А зачем ей практическое применение?
Затем что вычислительные теории типов - MLTT, UTT итд для этого и создавались. Вон, Брэди для Идриса целую парадигму программирования придумал, type-driven development. Чтобы это использовать, даже познаний особых в теории типов не нужно, хватит примеров из самой книжки. Нет, не хотим. Хотим с сохацького гореть.
> Вся его активность в теории типов -- создание собственного бренда. Ничего полезного он не сделал.
Ну он не Барендрегт или Мартин-Леф, чтобы что-то выдающееся сделать в теории типов. Но с точки зрения практической реализации чисто теоретических идей он сделал побольше, чем любой другой житель СНГ, это факт. В расеюшке вообще никто прувер сделать не в состоянии.
>Затем что вычислительные теории типов - MLTT, UTT итд для этого и создавались.
Мм, вообще-то нет. Не было в мыслях у Мартин-Лефа, что на компьютерах будут ПО верифицировать. Практические применения для математиков /= практические применения разработчиков, что, как мне кажется, ты имеешь ввиду упоминая Брэди. Это только последние 20-30 лет type theory пытаются использовать для software verification, а раньше это было про математику и логику. Даже сейчас пруверы на основе HoTT в первую очередь создаются в контексте оснований математики, а не для факториалов. Практически ориентированный только Idris.
>Но с точки зрения практической реализации чисто теоретических идей он сделал побольше, чем любой другой житель СНГ, это факт.
Это лишь говорит о твоей малой осведомленности в теме и подтверждает, что Сохацкий в первую очередь громче всех о себе кричит.
>В расеюшке вообще никто прувер сделать не в состоянии.
Ну что за глупости. Ты бы хоть в шапку посмотрел, заметил Arend. Валерий Исаев в отличии от Сохацкого занят делом и пишет папиры и пруверы, а не строчит в твиттер о своей охуенности и не создает сайты с лендингами.
И поверь, есть другие люди, способные создавать пруверы, просто они заняты своим делом.
Да так со многими областями знаний.
>А где я прошу мне что-то доказать?
Если ты не понял мысль в посте, я объяснять ее не буду. Твой бред начинает надоедать.
>в отличии от Сохацкого занят делом
Сильное утверждение. Проверять его на соответствие действительности мы, конечно, не будем.
Нейрончиков тред перекатывать не хочете, возобновили вновь старую тенденцию с пруверами. Не кажется ли вам, что всё это устарело уже? Нужен новый подход.
>Он и как "хуяк-хяук" - говно полное.
>Лучше сразу Coq взять и в Haskell его экстрактить.
Как на Coq хуяк-хуяк сделать partial функцию или не примитивно рекурсивную? E.g. head или mergesort. Так чтобы не сойти с ума в процессе.
Так что там за история, кто-нибудь?
Это не он пилил прувер на эрланге? Немного я припустил подливы с этого выбора языка.
Достаточно просто посмотреть на список публикаций и открыть их. Ну камон.
> сделать partial функцию
А зачем тебе верификация, если ты partial функции хуячишь?
> или не примитивно рекурсивную
Сам бы хотел знать, с радостью готов быть обоссаным Coq-боярами.
Беда всех этих языков это инфраструктура, решил было туториал по агде пройти, полдня прикручивал ее к виму, получилось хуево, бросил эту затею. А Coq вообще себе на уме, хоть и установить легко, после хачкелля вообще не идет. И, конечно, я не могу представить себе математика в здравом уме, ебущимся с кейбандами, емакса, зависимостями, совместимостями версий, фп- заморочками и прочим, чтобы велосипедить целые теории, в надежде дойти хоть до результатов 60х годов. Энтузиазм выше крыши нужен.
>Валерий Исаев в отличии от Сохацкого занят делом
однокурсник твой? Единственный человек из СНГ который что-то сделал для теории типов поехал крышей и умер 2 года назад, а остальное исаевы акуклевы какие-то ебланы-программисты, статей много, а импакта никакого.
Алсо раз тред возродили написали бы хотя бы жене сохацкого
> Беда всех этих языков это инфраструктура, решил было туториал по агде пройти, полдня прикручивал ее к виму,
Это твоя беда. Агда к емаксу прикручивается одной командой а к атому - несколькими кликами мышкой. Мартин-Леф тебе чтоли виноват, что ты не можешь даже установить то, чем собрался пользоваться?
В чем вообще заключается это прикручивание? Это же просто редакторы. Что вам там надо-то? Автодополнение? РЕПЛ какой-то продвинутый? Зачем?
> В чем вообще заключается это прикручивание? Это же просто редакторы. Что вам там надо-то?
В случае агды без редактора вообще можно только компилировать, интерактивного взаимодействия с голой агдой не существует. А там вся философия во взаимодействии пользователя с агдой через последовательно усложняющуюся типизацию и дыры. Ну ещё некое подобие тактик есть. Для всего этого нужен редактор. В идрисе изначально репл есть, но опять-таки что-то посложнее сделать - нужен редактор, у того же Брэди все примеры с атомом.
>говно сумасшедшего поедателя мозолек на диалекте лиспа
>говно на электроне выжирающее все память на старте
Нет, спасибо, все что начинается с "установите емакс" должно лежать под землей, как достояние узкого кружка сумасшедших. И еще удивляются, чей-то их язык непопулярен.
> И еще удивляются, чей-то их язык непопулярен.
С больной головы на здоровую. Кок без емакса и атома работает и существует 30+ лет и что, дохуя он популярен? Проблема в вас.
А вот эту хрень видел?
https://try.imandra.ai/
Стал ReasonML учить -- всплывала в реддите несколько раз.
> As a programming language, Imandra is a subset of the functional language OCaml. We call this subset of OCaml
Обрезанный окамл с нескучными обоями. Уноси.
> как достояние узкого кружка сумасшедших
Ну так сами пруверы - это достояние узкого кружка сумасшедших. Не для ерохиных тема.
Ну так приходят математики: слишком сложна, уходят набирать "очевидно" в latex. Приходят программисты: сложна, уходят писать идрисы свои.
Если человек не ученый, то он по определению ничего не делает, ок.
Да при чем тут эрланг, ноль информации в твоих каментах.
Такое ощущение что ты перед кем-то выйобуешься.
Передо мной не нужно, для меня ты никто.
Шиве?
Шива же вроде мужик
>Кок без емакса и атома работает и существует 30+ лет и что
Отмечу что при этом не более чем год назад появилась в coqide убойная фича - при переносе строки учитываются табы на предыдущей строке - доступная чуть ли не в любом редакторе размером от нескольких килобайт. Такими темпами они выйдут на паритет по функциональности с такими редакторами как sublime или vscode (или черт его дери emacs) лет через сто.
Если уж к поделкам MS я отношусь со скепсисом, то к этому поделию непонятной мутной конторки, вполне возможно состоящей из единственного хипстерка - почти как к червю пидору. Возможно я ошибаюсь, из нескольких минут наблюдений
1) один пост на реддите в r/imandra - переплюнули fstar
2) НЕТ СОРЦОВ?
3) вместо установщика - говно из курлпайпа плюс несколько часов компиляний
4) не работает под шиндовс
Главное - как и с большинством васяноподелок языков, регулярно всплывающих раз месяц с нескучными заимствованиями разных синтаксических конструкций, непонятно нахуя вообще нужно это чудо, для чего? В чем его фишка?
Ты про Воеводского?
>А зачем тебе верификация, если ты partial функции хуячишь?
прост))))) Можно например в месте вызова аргументы проверять чтобы не терять корректность. В агде вроде бы даже можно код с дырками запускать, правда не знаю на сколько это на практике полезно и что будет если такой код экстрактить.
Как что-то плохое. Ты что, гомофоб?
Не знал что этот ваш Сохацкий из этих любителей помесить глину.
Кто-кто?
Ну из этих, любителей стрельбы из кожаного пистолета на своём заднем дворе.
> Отмечу что при этом не более чем год назад появилась в coqide убойная фича - при переносе строки учитываются табы на предыдущей строке - доступная чуть ли не в любом редакторе размером от нескольких килобайт.
А это очень нужно для коковского кода?
Так он женат, не?
Кто?
Сохацкий, це тi?
>нахуй не нужен ваш сборщик мусора
С линейными и uniqueness типами действительно не нужен.
Го популярен из-за того, что у него няшный логотип и его пиарит гугл. Все. Его, кстати, переписывают (привет слоупокам) ломая обратную совместимость, и во второй версии добавляют и дженерики, и обработку ошибок, и все остальное, о чем Пайку талдычили с самого начала.
Алсо, сборщик мусора и модули - это "шашечки", я тебя услышал. Иди дальше laba1.cpp дописывай.
Нужен, ибо без нормальной реализации персистентных структур в наше время никуда rc - это один из вариантов gc, напоминаю.
Мне вообщем-то всё не похуй, везде сую свой нос, как-то так..
Что такое rc?
>А это очень нужно для коковского кода?
Ну как бы да - не все же ебошут все в одну строчку. Хотя и такие черти бывают, чего уж там.
Вообще интересно почему так - код надо хитровыебно выравнивать, а с обычным текстом никто так никогда не делает.
>Его, кстати, переписывают (привет слоупокам)
>и во второй версии добавляют и дженерики, и обработку ошибок, и все остальное, о чем Пайку талдычили с самого начала.
Врети! Линк?
>ломая обратную совместимость
Будет обсер гарантия миллион процентов. Гарантирую тот же исход хипстерков с ангуляра на реакт 2.0 - т.е. с го на еще какую нибудь новомодную поебень. Может даже typescript. Или еще чего придумают новенького.
>С линейными и uniqueness типами
Какое положение этих штук с точки зрения зависимых типов, доказательств и прочего Карри-Ховарда?
Какое место эти типы занимают на лямбда-кубе?
>Какое место эти типы занимают на лямбда-кубе?
Любое. Зависит от того, как calculus построишь.
В лямбда-кубе три плоскости, а substructural типы это совсем другая плоскость. То есть, ты выбираешь любую точку на лямбда кубе - это какое-то семейство исчислений, и уже его расширяешь линейными, аффинными, whatever типами.
>Какое положение этих штук с точки зрения зависимых типов, доказательств и прочего Карри-Ховарда?
Ортогональное. Это тоже про доказательства, но в другую сторону. А как оно все вместе взаимодействует - предмет bleeding edge research последних минимум лет двадцати.
Так ведь хохма этого куба в том что местные петухи его притаскивают чтобы всем доказать что депендент-калькулус самая-самая вершина эволюции и выше его уже ничего не может быть. А тут вона оно как получается.
А как, кстати, новомодные кубические типы сочетаются с линейными, кто-нибудь брался за такое?
Мое увожение треду, откуда вы все это знаете?
>Врети! Линк?
https://github.com/golang/go/wiki/Go2 не?
>новомодную поебень
>typescript
Ну такое.
У гугла кстати то же самое ведь уже было с дартом, один в один. Только там язык еще хуевее го был, ну то есть вообще кроме нескучных обоев от гугла ничего не было. Некоторые хипстерки заглотили, через некоторое время стало понятно, что он нихуя не взлетел, ну гугель их и кинул, потом вот вторую версию точно также выкатили, все попутно сломав, ну и опять маховик маркетинговой машины разгоняют. Переписывай код своего стартапа, хипстерок, код сам себя не перепишет.
> Так ведь хохма этого куба в том что местные петухи его притаскивают чтобы всем доказать что депендент-калькулус самая-самая вершина эволюции и выше его уже ничего не может быть. А тут вона оно как получается.
Че получается-то, мань? Ты хоть разберись в вопросе, потом называй петухом кого-то кроме отражения в зеркале. Самая упакованная вершина куба это СоС, calculus of construction. CIC - исчисление индуктивных построений, на чем основан тот же кок, уже выше. А зависимые типы начинаются вообще с лямбды пи. Этот куб вообще касается только лямбда исчислений по Черчу, лямбды а-ля Карри к нему вообще не относятся. И так далее. Двоечка тебе, уроки иди делай.
О а вот и порваный петух прилетел. Ну я рад что ты все таки разобрался что там к чему, может теперь поменьше будешь насаться с этим кубом как с писаной торбой
>Двоечка тебе, уроки иди делай.
Сначала сдай норматив чтобы тут указания раздавать. Первый вопрос норматива
>Перечислить все аксиомы CIC
время пошло.
>ломая обратную совместимость
>We do not want to break the ecosystem. Go 1 and Go 2 code must be able to interoperate in programs with ease.
Что то тут не сходится
>>новомодную поебень
>>typescript
>Ну такое.
Какое?
Долбаеб, блядь. О чем говорить с дегродом, который не отличает лямбда исчислений от вспомогательных построений на их основе.
>Go 1 and Go 2 code must be able to interoperate in programs with ease.
Подумай еще раз.
Назвать тайпскрипт новомодным язык не поворачивается. Он же и не новый, и не модный.
Подумал. Ты - пиздаболка.
Снова обсер.
Можно обсудить как хорошо ебсти твою мамку.
Представьте себе пространство всех языков программирования — понятно дело все знают про лямбда исчисление. Но не многие же рубисты или ПХП программисты задумываются, что они пишут на языке пространства — которое с точностью до битов моделируется теорией типов Мартина Лефа (надо только вселенные правильно отконфигурировать, это научились делать в 2001 году, когда Coq все дружно писали). Конечно я сам в это по началу не верил, и думал что есть все-таки ограничения и что Данила Мастер, который вручную все сам делает вместо того чтобы экстрактить это из Инфинити Топоса делает ненапрасный труд. Мне пришлось написать прувер чтобы понять — таки да, каждый Данила Мастер, который считает себя инженером — производит временный и бесполезный труд, давая ярлыки феноменам не видя их сути.
Пространство типов безгранично и все типы одновременно живут в этом бесконечномерном пространстве — где каждое его измерение наслаивается друг на друга, а сами типы образуют паттерны, похожие на гомотопические группы. Так как изоморфных типов в пространстве бесконечного топоса хватает, то в MLTT тоже есть что-то похожее на матрицу гомотопических групп. Они имеют разные имена и могут в принципе не проходить чеканье на равенство и т.д., но при компиляции в нетимизированную лямбду изоморфные типы будут генерировать совместимый код.
У всех типов есть четкая логика заселения пространства бесконечного топоса, подобно тому как жители самсары заселяют шесть лок. Начинается все с нижнего дна ада — Bottom типа. И потом по кирпичику начиная с Unit (), потом A -> A, потом Nat, потом Stream, потом List, потом ... и так далее вплоть до инфинити-групоида, потом все начинает повторятся и узор начинает меняться. Где у этого узора дырки я пока не вижу, и какая у него структура, но как бы чувствую немного дыхание этой мандалы. Эта мандала доступна впринципе всем программистам, которые могут писать циклы, складывать числа, больше уровня не нужно. Всю эту математику можно переформулировать так, чтобы MLTT преподавать 11 летним детям — считайте, что эксперимент начат.
Пространство типов безгранично и все типы одновременно живут в этом бесконечномерном пространстве — где каждое его измерение наслаивается друг на друга, а сами типы образуют паттерны, похожие на гомотопические группы. Так как изоморфных типов в пространстве бесконечного топоса хватает, то в MLTT тоже есть что-то похожее на матрицу гомотопических групп. Они имеют разные имена и могут в принципе не проходить чеканье на равенство и т.д., но при компиляции в нетимизированную лямбду изоморфные типы будут генерировать совместимый код.
У всех типов есть четкая логика заселения пространства бесконечного топоса, подобно тому как жители самсары заселяют шесть лок. Начинается все с нижнего дна ада — Bottom типа. И потом по кирпичику начиная с Unit (), потом A -> A, потом Nat, потом Stream, потом List, потом ... и так далее вплоть до инфинити-групоида, потом все начинает повторятся и узор начинает меняться. Где у этого узора дырки я пока не вижу, и какая у него структура, но как бы чувствую немного дыхание этой мандалы. Эта мандала доступна впринципе всем программистам, которые могут писать циклы, складывать числа, больше уровня не нужно. Всю эту математику можно переформулировать так, чтобы MLTT преподавать 11 летним детям — считайте, что эксперимент начат.
>эксперимент начат
Держи в курсе
Ясно, этот опущ прохудился, замените по гарантии.
Охуенная паста, никто кроме Сохацкого так не напишет.
Сохацкий, ето ты?
Говно без задач, не нужное ни программистам, ни математикам. Вторая культура и там и тут.
Вообщем если есть вопросы я отвечу, высмеяли меня хорошо, я люблю анонимусов они дают взгляд на себя долбоеба со стороны!
> Говно без задач, не нужное ни программистам, ни математикам. Вторая культура и там и тут.
MLTT это самая что ни на есть первая культура, основания. Не нужна она только дегенератам, для программистов и математиков польза есть, дело в том что средний пидор в узкачах с поворотами, с бородкой и петушиным гребнем из барбишопа - это не программист и не математик, а простое быдло.
О! Узнаю почерк конструктивиста с /math/.
Добро пожаловать в тред.
>основания
Основаниедрочер - не человек. Это такие байтоебы от математики.
Держи в курсе, только делай это в другом треде.
У меня от этой пасты кровь приливает к мандале и сразу хочется преподавать математику 11-летним детям, все правильно?
Найс обоссали основаниебыдло.
>Держи в курсе, только делай это в другом треде.
Лучше уж ты предупреждай когда снова соберешься запиздеться, чтобы время на твои охуительные истории не тратить.
>У меня от этой пасты кровь приливает к мандале и сразу хочется преподавать математику 11-летним детям, все правильно?
Главное чтобы к кое чему другому не приливало, а так норм.
>опущ прохудился
>Ни слова про норматив
Нет, маня, прохудилась тут только ты.
Где ответы на норматив? Часики то тикают.
Кто-нибудь может пояснить чем занимался Воеводский и ко?
Я так понял они хотели создать основания для математики такие что их принимало бы большинство математиков, типа в них можно было бы выстраивать эти ваши ебалогии. И так же удобные для работы на компьютере.
Но я вижу только два артефакта их деятельности. Первый - библиотека на коке/агде. Для чего она вообще нужна мне не понятно. Она кем-нибудь используется вообще? Второе - конференции. Устроены они по принципу - каждый желающий приходит и рассказывает свои охуительные истории хотя бы по касательной касающиеся темы оснований. Как то все совсем мутно.
Я так понял они хотели создать основания для математики такие что их принимало бы большинство математиков, типа в них можно было бы выстраивать эти ваши ебалогии. И так же удобные для работы на компьютере.
Но я вижу только два артефакта их деятельности. Первый - библиотека на коке/агде. Для чего она вообще нужна мне не понятно. Она кем-нибудь используется вообще? Второе - конференции. Устроены они по принципу - каждый желающий приходит и рассказывает свои охуительные истории хотя бы по касательной касающиеся темы оснований. Как то все совсем мутно.
Бля, вот только что зашёл в тред первый раз, начал читать и думаю интересно, взлетела ли та хуита, которую Воеводский мутил и тут твой пост. Вот как это объяснить? Может я ебанулся и подменил себе воспоминания, а твой пост был раньше? Или это просто мир волнами информационными хуячит и мы на одной волне зашли? А?
> Кто-нибудь может пояснить чем занимался Воеводский и ко?
В двух словах - конструктивные основания.
> - библиотека на коке/агде. Для чего она вообще нужна мне не понятно. Она кем-нибудь используется вообще?
Попытка реализации конструктивных оснований. Она никем не используется, потому что в MLTT могут единицы, в её дальнейшее развитие - HoTT могут ещё меньше, а в cubicaltt, где аксиома унивалентности Воеводского это уже не аксиома, а доказуемая теорема, со всего снг может вообще один сохацкий. Так и живём, сладкий хлеб жуем. Ибо папуасы.
Это все проделки "существ" не иначе, етпочя.
>Сохацкий совсем не палится
>а в cubicaltt, где аксиома унивалентности Воеводского это уже не аксиома, а доказуемая теорема, со всего снг может вообще один сохацкий
Слишком громкое заявление.
Верните нейроночки
Тоже интересно откуда они всё это знают
По моим тредам можно теорию типов учить.
Покинь тред, не трать время. Не пиши мне больше.
> Слишком громкое заявление.
А кто ещё? Автор того прувера, arend? Ну ок, двое.
Как доказать единственность без доказательства от противного?
> а в cubicaltt, где аксиома унивалентности Воеводского это уже не аксиома, а доказуемая теорема, со всего снг может вообще один сохацкий.
Ору
>Покинь тред, не трать время.
Нет, ты.
>Не пиши мне больше.
Хуй соси, губой тряси.
> Ору
Сохацкий, це тi?
Если P a и P b, то a = b?
isContr : ∀ {i} (A : U i) → U i
isContr A = Σ A λ x → (y : A) → x ⟿ y
Кто-нибудь может объяснить что означает этот дрист?
> Кто-нибудь может объяснить что означает этот дрист?
Дрист у тебя в голове, походу. Что ты забыл в этом треде, если простую типизацию читать не можешь? "Сохацький, це тi?" писать сюда пришёл? Иди лучше уроки пиши.
Но ведь это доказательство от противного.
Cам ты противный.
Стягиваемость.
Что за
>⟿
Это на той самой поебени которую могут полтора Сохацких?
Ну замени «⟿» на «=».
Все, я разобрался. Просто беседа в духе
> как доказывается ..?
> доказательством
Ну ОК тут не поспоришь.
А много тут таких, кто разбирается в кубических пруверах?
Один семен
Ещё Сохацький, но это неточно
> Однажды создатели Coq с удивлением обнаружили, что если в него добавить закон исключенного третьего, то аксиома выбора опровергается. После доработки напильником она больше не опровергается. А мораль этой истории в том, что попытки скрестить слона с китом (ZFC с лямбдами) могут привести к неожиданным результатам.
Есть у кого нибудь подробности этой истории?
Есть у кого нибудь подробности этой истории?
А откуда цитата?
Покажите, что предикат y = x+1 невыразим в интерпретации (Z, =, f), где f — одноместная функция x -> (x + 2). Не получается автоморфизм построить, автоморфизмы вида x -> kx не подходят, так как f неустойчива относительно них, так же всякие x -> xk и тд. А автоморфизмы вида x -> x +k ничего не дают, так как предикат y = x + 1 устойчив относительно них. И чё делать?
Отбой, разобрался, автоморфизм будет x -> x, если x нечётное и x -> x+2, если x чётное.
На чем основывается математика
На том, что она работает ИРЛ.
Дебил
Ты не в то поле подпись ввел. Недавно здесь?
Поясните за Blodwen. Это типа Idris 2?
Это просто поигрушки.
Но он активно пилится. И Брэди говорил, что в идрисе не все так однозначно и исправимо. А тут вроде как работа над ошибками.
Это каким мегачванливым чмом надо быть, чтобы:
1) Обосрать единственный православный редактор
2) Посчитать свои поверхностные заметки достойными рецензии (или восхищения?)
3) Предполагать, что анонимус не знает, про что говорит, и поэтому несёт чушь
>это больше для профессиональных математиков тема, а не разработчиков ПО
Да только вот труъ-математикам поебать, а программистам интересно, потому что они пишут свои привычные термы, но вроде бы при этом и математику делают (на самом деле нет).
>можно для улучшения качества тестирования использовать эти штуки
Это ну очень оптимистичный взгляд на положение дел. Можно прикрутить рефайнменты с моделчекером или экстрактить из завтипового языка незавтиповой, но корректный код. Что хуже - не знаю, но и то, и другое пока тяжело и долго.
Нет, подожди, ты хочешь сказать, что в этом емакс виноват?
>3) Предполагать, что анонимус не знает, про что говорит, и поэтому несёт чушь
Естественно. Это так в 100% случаев. И чем более чванливый и безапелляционный тон у высказывания, тем меньше говорящий знает о предмете. Это азы анонимного общения, ти вапще с кокой плонети?
Ну на самом деле нет. Бывает, что анонимус может спиздануть, но он это не стесняется признать, если оно так. Картину портят полтора безголовых уёбка, которые находятся в каждом треде и там гадят дико ополоумевши (от них постов больше всего, поэтому кажется, что других нет). А ещё от эффекта разбитых окон вменяемый анон лишний раз склонен промолчать, а то и тоже насрать просто так.
Idris - это говно, которое уже никак не исправить. Просто даже не прикасайся к нему.
> Idris - это говно, которое уже никак не исправить. Просто даже не прикасайся к нему.
А что так? Мне он наоборот понравился. Начиная с установки, просто распаковываешь архив и все работает, без всякой дрочьбы вприсядку.
Заебал ныть, тебе сложность установки - главный критерий успеха? А пруфы не пробовал писать?
Ну, чувак говорит, что иде хуйня, а языки должны стремиться быть такими, чтобы ими можно было легко и просто пользоваться без иде, одним обыкновенным редактором (вместо кодогенерации - более лучшие абстракции, например). В принципе это правильно.
А описание имакса тупо устарело - не знаю, может когда-то так и было, но нынче для тех, кто не хочет ничего настраивать, есть спейсмакс.
Не хочешь играться - не играйся, чём проблема-то?
Видел у одного чела который пытался прикрутить агду к вим похожие рассуждения, что кейс-сплиты и подобное не нужны на самом деле при должном уровне просветления. С одной стороны очень похоже на рационализацию, а с другой - довольно любопытная мысль. Может действительно когда есть инструмент начинаешь акцентироваться не на том что действительно важно, а на всякой вторичной поебени.
Для меня это очевидно. Вон вкатывальщик написал простыни в начале треда: там только и разговоров про то, как иде работает или не работает. До собственно работы с системами он так и не дошел. Он не понял ни чем они отличаются, ни зачем это все нужно. И все туториалы и проч. тоже на этой чепухе зациклены.
>До собственно работы с системами он так и не дошел. Он не понял ни чем они отличаются, ни зачем это все нужно.
У тебя какие то болезненные маняпроекции, впрочем, далеко не первый раз вижу тут такое. С каких хуев ты вообще это взял совершенно не понятно. Но да представь себе - перед тем как начать работать с системой ее нужно предварительно установить и настроить, както само-собой чистой силой воли это не делается, приходится поебаться.
Ну если бы ты покодировал пруфы и понял, в чём разница, ты бы про это и писал. А поскольку ни до чего интересного не дошёл, то остаётся только изливать анальную боль от того, что не умеешь пользоваться компьютером.
>Ну если бы ты покодировал пруфы и понял, в чём разница, ты бы про это и писал.
Фантазеры-фантазерчики. Ты сам то чьих будешь - их тех кто расписал весь тред фундаментальными отличиями пруверов (в своем манямирке) или из тех кто даже на пол-шишечки вкатиться не может но воооот задал бы тут всем жару толька ленива чет.
Я только Logical Foundations прорешал. Но я и не выйобуюсь )))
Попробуй не выйобывоться получше, пока не очень. Или хуйни уж чего-нибудь интересного.
>попробовал я недавно работать в вашем линуксе. Скачал какой-то .iso файл убунты, че с ним делать дальше непонятно. Поискал в гугле, там по-английски чет написано, ниче не понял. Говно этот ваш линукс, удалил.
>может вообще один сохацкий
Все, что может сохацкий - это написать элементарный терм из книжки по математике. Ну и еще выложить в инстаграм фоточку с книжкой по алг топологии, иногда открытой на рандомной странице. При это нихрена не понимая материала, естессно.
> При это нихрена не понимая материала, естессно.
Тыскозал? Ну покажи свой прувер тогда.
Сохацкий, пидор, вот я крестьянин. Объясни мне, пожалуйста, почему группа точек эллиптической кривой изоморфна комплексному тору.
Сохацкий тупая вниманиеблядь.
Ох, кто это к нам пожаловал? ;)
>Ну покажи свой прувер тогда
Очередной аргумент в стиле "сперва добейся".
Несмотря на очевидную фриковость всей этой HoTT-компании, у большинства известных участников есть приличное образование, зачастую математическое, и публикации во вменяемых журналах, в том числе по математике и логике. У того же Исаева есть публикации и препринты на архиве.
Что там с публикациями у Сохацкого? Тру-математики вообще не знают о существовании такого человека. Все, что он может, это только фоткаться с книжечками, писать простые определения и тригериться на Каледина в твиторе.
Еще одного пидора притащили. Уебывайте с моего кодача, подсосы вниманиеблядей.
>Что там с публикациями у Сохацкого?
Видел одну (правда в паре ещё с одним человеком); но уже не найду, к сожалению.
https://link.springer.com/chapter/10.1007%2F978-3-319-97885-7_30
>Recent Developments in Data Science and Intelligent Analysis of Information
>Cubical Type Theory
лiл
> Несмотря на очевидную фриковость всей этой HoTT-компании,
Тыскозал? Ты ж даже не понимаешь что это и зачем, а своё школьное мнение не только имеешь, что ещё полбеды, но и выдаешь за истину, что уже полное школьничество. Сохацкий вас лямбдами обидел, или с чего весь этот хейт?
Сохацкий, ну хватит уже
Нит.
> Мам, у меня Сохацкий под кроватью!
Каледин, перелогинься.
Почему от Каледина горят булки?
А кто такой Каледин?
Любитель пошерудить гиперкэлеровы многообразия.
А Сохацкий?
Ну и как можно сравнивать фриковатого Максимку, который может только копипастить чужие пруфы себе в либу, и хорошего, успешного математика.
Каледин выёбывайся в /math/
> А Сохацкий?
А Сохацкий предложил придумать вопросы, которые он задаст Мортбергу. Только вы даже не знаете кто это, а единственный вопрос, который смогли бы придумать - "Сохацький, це ти?".
>Мортбергу
Хуи сосёшь? Бочку делаешь?
Ага, а ты бы что спросил, если такой умный?
>а ты бы что спросил
Ты тупой или слепой -
> Хуи сосёшь? Бочку делаешь?
Вот это и есть ваш уровень, дегенераты. И ещё на Сохацкого гоните.
Судя по линкедину, максимка просидел больше 10 лет в кровавом энтерпрайзе, но так и не научился говорить без элементарных ошибок. "I am just interesting", "was came" и тому подобное, и все это украшено постоянным ебанутым смешком.
тоже жутко кринжую с этого, не могу даже досмотреть
Ну он в принципе и по-русски так же как минимум пишет. Индус же, щито поделать. Главное, что код хорошо пишет.
Во‐во, она.
Ты сначала бочку-то сосни, а потом кукарекай. Бочку сосать это тебе не пруверы писать.
Знатоки и ценители русского языка из 7б в треде.
Ебать у них там сборище убогих додиков, у меня годовую норму кринжа переполнило с десяти минут.
СУПЕР-ПУПЕР-КОНПУКТЕР-САЕНТИСТ СПЕЦИАЛИСТ ПО ФОРМАЛЬНЫМ МЕТОДАМ
@
СНЯЛ УЖЕ ХУЛИОН ВИДОСОВ СО СВОИМ ПИЗДЕЖОМ
@
НИКАК НЕ МОЖЕТ НАСТРОИТЬ ЕБАНЫЙ ЗВУК
Ты опять мимо /b промахнулся, друг?
Сохацкий, не гори!
И никак не может научиться правильно составлять элементарные фразы на ангельском.
Кто?..
Зачем ему английский, если он владеет языком гомотопий?
>он владеет языком гомо
-> /ga
И (ко)гомологий!
Кринжи малолетние, идите нахуй отсюда. Гореть с Сохацкого можно где-нибудь ещё.
Вопрос такой: при компиляции в хаскеле сложная типизация компилируется в итоговую программу, или выкидывается? Если код написан с использованием либ типа cubicaltt Мортберга, скомпилируются все функции в полном объёме или нет? Например, в коке при экстракции кода в окамл или хаскел, многое просто выкидывается. Тут не экстракция, но мало ли. Никто не в курсе?
Вопрос такой: при компиляции в хаскеле сложная типизация компилируется в итоговую программу, или выкидывается? Если код написан с использованием либ типа cubicaltt Мортберга, скомпилируются все функции в полном объёме или нет? Например, в коке при экстракции кода в окамл или хаскел, многое просто выкидывается. Тут не экстракция, но мало ли. Никто не в курсе?
Типы в хаскелле стираются, в рантайме их нет.
В том, что делает Максим, типы тоже стираются, никаких кубов в бинарях, конечно, не будет.
А разве тогда скомпилированный екзешник будет равен исходному коду? Функции разве одни и теже будут с типами и без?
Ну понятно, что по-хорошему надо доказывать эквивалентность исходного кода конечному. Но это задача не первостепенной важности, потому что как раз тут особых проблем не наблюдается.
> Ну понятно, что по-хорошему надо доказывать эквивалентность исходного кода конечному.
Для этого всякие сертифицированные компиляторы типа CompCert? Но там же тоже типы. Если промежуточные языки типизированы в том же коке для доказательства корректности, а в итоговом бинарнике никаких типов нет, о какой сертифицированной компиляции вообще можно говорить?
Процессору вообще похуй. О какой сертификации может идти речь?
Транслятор программ из исходного языка в конечный - это функция, к которой можно написать спецификацию и доказательство. Соответственно, можно верифицировать. Конечно, чтобы потом пользоваться этим транслятором, его надо как-то преобразовать в машинный код, а для этого надо опять стирать типы. Ну, ничего не поделаешь, в какой-то момент придётся написать простейший стиратор типов и уверовать в то, что он ничего не портит.
Всегда все сводится к тому, что во что-то надо уверовать. И в самой математике так. Это норма, мир у нас такой уж.
В верификации все достоинство в том, что нужно уверовать в какой-то конечный кусок кода, который сертифицирует все остальное. Без верификации тебе нужно уверовать в неограниченное количество кода. Причем наперед известно, что баги там наверняка есть - приходится даже не уверовать, а просто уповать на то, что баги не слишком разрушительны. Что самолет не упадет из-за них через пять минут после взлета.
> Всегда все сводится к тому, что во что-то надо уверовать. И в самой математике так. Это норма, мир у нас такой уж.
Ну нахуй, это не так работает. Я вижу, что суть в типизации промежуточных языков вплоть до машинных инструкций. И далее, если есть доказательства корректности кода в машинных кодах, то и соотв машинные коды без всяких типов будут корректным кодом. А вербовать и без математики можно, для этого пруверы не нужны.
Ну ващето, так и работает. Нельзя доказать вообще всё.
>Я вижу, что суть в типизации промежуточных языков вплоть до машинных инструкций
Ну ващето нет. Типы нужны только в пруверах как средство верификации. В остальных они только для удобства. Можно же (теоретически) сразу верифицированным транслятором переводить верифицированные в том же прувере термы в машинные коды, хотя это непрактично.
Можно и сразу программы писать в машинных кодах и их верифицировать.
Только потом надо доказать, что эти машинные коды правильно записываются в память.
Да, а ещё доказать, что они правильно исполняются процессором, а результат исполнения правильно читается и интерпретируется. Ух сколько всего доказать надо!
Попробуй сначала докажи, что ты правильно доказываешь. Может это бред все.
https://twitter.com/5HT/status/1107729999468134400
Ну хоть что-то
Ну хоть что-то
> https://tonpa.guru/stream/2019/2019-03-16%20Geometry%20in%20Modal%20HoTT.htm
> Я зробив презентацію нашої бібліотеки Groupoid Infinity — усі були у захваті.
я представляю себе
> Я зробив презентацію нашої бібліотеки Groupoid Infinity — усі були у захваті.
я представляю себе
Как там Сохацкий? Все так же сосёт в математике?
Да при чем тут математика, ноль информации в твоих каментах.
Такое ощущение что ты перед кем-то выйобуешься.
Передо мной не нужно, для меня ты никто.
Сохацкий, це ті?
Нiт
>Сохацкий, це ті?
Это такой способ бампать, или вы там все реально ебанутые?
> вы там все реально ебанутые
Сохацкий, молчи уже. Это вообще не про тебя тред, что ты тут вечно возникаешь?
Вы тута умные, телевизор смотрите поди. Поясните, почему типизация записывается через стрелочку, какой у этих стрелочек смысл? Например, у функции "+" тип Nat -> Nat -> Nat. Понятно, что функция сложения берёт два натуральных числа на вход и на выходе выдаёт тоже натуральное число (как пример, ясно что складывать можно не только натуральные числа). Это все ясно. А стрелочки нахуя, почему не запятые например?
>функция сложения берёт два натуральных числа на вход и на выходе выдаёт тоже натуральное число
Нет. Эта функция каррирована, она принимает натуральное число и возвращает функцию Nat -> Nat:
Nat -> (Nat -> Nat) - скобки можно не писать из-за ассоциативности стрелки
А функция Nat -> Nat, которую вернет первая функция, уже принимает второе число и возвращает ответ. То есть в выражении
plus 3 5 на самом деле делается (plus 3) 5
Где plus 3 вернет тебе лямбду \x -> x + 3. Дальше к этой лямбде будет применена 5 и получен ответ.
А то, что ты говоришь, записывается как (Nat, Nat) -> Nat. То есть принимаем пару чисел, возвращаем число. Записываться это будет plus (3, 5). Но так как каррированные функции умеют больше, везде пишут именно их.
> Нет. Эта функция каррирована, она принимает натуральное число и возвращает функцию Nat -> Nat:
Ок. Ну а тут в чем смысл стрелочки? В логике это импликация, в множествах - отношение подмножества. Или тут смысл не в этом? Тогда в чем?
>В логике это импликация
Тут тоже что-то вроде импликации, соответствие Карри-Говарда же.
>в множествах - отношение подмножества
Не пизди, там не стрелочка.
В теоретико-множественной математике вообще функции тоже через стрелочку пишутся. f : A -> B
> Не пизди, там не стрелочка.
Не стрелочка, но я не об этом, а о том что в множествах отношение подмножества то же самое, что импликация в логике. Т.е Nat -> Nat это импликация, а первый Nat в этой схеме подмножество второго? Хуйня какая-то, не?
>Т.е Nat -> Nat это импликация
Не импликация, но что-то вроде. Соответствие Карри-Говарда, google it
>а первый Nat в этой схеме подмножество второго?
Ну функция задаёт подмножество, да. "Область прибытия" называется
>"Область прибытия"
Нет, всё-таки, "множество значений"
А если функция Nat -> Float ?
Задаёт подмножество Float.
> Не импликация, но что-то вроде. Соответствие Карри-Говарда, google it
Ну пропозишн ас тайпс / сетс. Импликация как подмножество и есть.
Я так вижу: в выражении \x -> x + x, "x" очевидное подмножество "x+x" же. Или что?
>Ну пропозишн ас тайпс / сетс. Импликация как подмножество и есть.
Если утверждения - типы, то импликация - функция.
>в выражении \x -> x + x, "x" очевидное подмножество "x+x"
Я не понял нихуя, ты занимаешься хуйнёй, что тебе нужно вообще?
> Я не понял нихуя, ты занимаешься хуйнёй, что тебе нужно вообще?
Разобраться.
Это просто стрелочка. Не надо страдать фрейдизмом. Лучше что-нибудь содержательное спроси
>В целом вышел весьма поучительный экспириенс, но и довольно болезненный.
Я тебе больше скажу — у меня сложилось мнение, что не всегда и автор этих действий сможет их с лёгкостью повторить. Отсюда скепксис по отношению к применимостью в индустрии.
Ну если только считать за деятельность копипасты из учебников, лендинги и срачи в твиттерах...
Float -- подмножество Nat?
>Понятно, что функция сложения берёт два натуральных числа на вход и на выходе выдаёт тоже натуральное число
Нет, функция (+) берет натуральное число и возвращает функцию, которая берет еще одно натуральное число и возвращает натуральное число:
(+) :: Nat -> (Nat -> Nat)
У стрелочки правая ассоциативность, поэтому скобки писать необязательно.
ай блядь, тебе уже ответили, ну похуй, не стирать же
>Ну а тут в чем смысл стрелочки?
Ну функция A -> B берет аргумент типа A и возвращает результат типа B. autism-intensifies Ну A преобразуется в B, стрелочка как бы намекает на это. Что не так-то?
>Nat -> Nat это импликация, а первый Nat в этой схеме подмножество второго? Хуйня какая-то, не?
Ну множество как бы является подмножеством себя, что не так-то? trollface
>А если функция Nat -> Float ?
Ну так ведь Nat подмножество Float, что не так-то? trollface
>Ну пропозишн ас тайпс / сетс.
Ну, функциональный тип (A -> B) соответствует логической импликации (A => B) и теоретико-множественному множеству отображений из A в B. То есть твой тип A -> B утверждает, что из A в B существует отображение, а твоя функция этого типа (любая из них) доказывает это утверждение, приводя пример такого отображения.
Ну или вот пример, функция map :: (a -> b) -> [ a ] -> [ b ]. Берет функцию и список и применяет функцию ко всем элементам этого списка, так? Расставим скобки и прочитаем как высказывание о множествах: (a -> b) -> ([ a ] -> [ b ]). То есть: если существует отображение из a в b, то есть и отображение из [ a ] в [ b ]. Логично?
>Импликация как подмножество
Ты говоришь про то, что подмножество задается так: A ≤ B <=> \forall x : (x \in A -> x \in B), так? Ну так здесь-то у тебя один и тот же x в левой и правой частях импликации, а (Nat -> Float) - это грубо говоря \forall x \exists y : (x \in Nat -> y \in Float), то есть мы в соответствие каждому Nat ставим какой-то Float. И в отличие от примера с map у нас тут конкретные типы (начинаются с заглавной буквы), а не типовые переменные (строчные буквы). Если ты хочешь делать осмысленные утверждения о типах вообще, то тебе и писать надо такие функции, которые говорят о любых типах вообще, а не о Nat и Float. Возвращаясь к твоим подмножествам, \forall x : (x \in A -> x \in B) - у тебя же получается, берет икс одного типа и возвращает тот же самый икс, но уже другого типа. Ну вот например в какой-нибудь джаве ты так можешь сделать, взяв икс и кастанув его к родительскому классу. Ну и нетрудно догадаться, что множество объектов класса-наследника есть подмножество объектов класса-родителя, так ведь?
По-моему ты просто завидуешь тому, что человек реально добился успеха в жизни, а ты сидишь на дваче и пишешь "це сохацкий?".
Тоже хочу заниматься математикой в IT, но не унылыми пруверами, а алгебраической геометрий в криптографии: разрабатывать криптосхемы на эллиптических кривых и АГ-коды на эллиптических и эрмитовых кривых. Что надо делать, чтобы это стало реальностью? Где искать работу?
>Ну так ведь Nat подмножество Float, что не так-то? trollface
А если Float -> Nat ?
В чем сложность математики?
>Ну так ведь Nat подмножество Float, что не так-то? trollface
>trollface
>А если Float -> Nat ?
>trollface
Не, я только присоединился, но может поддержку движ.
Сохацкому не завидую. Немного завидую анону с goviaji. Вот он, как раз чего то добился.
Бля, ну и ебанутый
https://twitter.com/5HT/status/1111495344540536834
https://twitter.com/5HT/status/1111495344540536834
Надо нагуглить, как заходить в хату к эрланг богам.
Это еще аутичнее пруверов. Работа только в универах. Разработать криптосхему может любой дурак, я вон сам несколько разработал. Толку-то? Нужно понимать зачем, и как гарантировать нужные свойства. А когда начинаешь это нормально понимать, то одновременно понимаешь, что все уже разработано, и тебе уже нечего делать со всеми этими знаниями.
Нет. Функция Nat -> Float выделяет в Float некоторое подмножество, изоморфное некоторому подмножеству Nat.
Как только зайдешь в хату, ты должен произнести magic cookie и назови свой pid(). Тебе могут бросить под ноги пустое сообщение. Никогда не обрабатывай его handle_call, только handle_info, в крайнем случае handle_cast. Тебя могут спросить кто ты: supervisor, или worker. Никогда не ври, отвечай честно, всё равно все со временем узнают и могут даже exit(Pid, kill), если наврал. Обязательно узнай кто в хате lager.
Спасибо, теперь понятно.
>что все уже разработано, и тебе уже нечего делать со всеми этими знаниями.
Да и это совершенно нинужно. Любую зашифрованную информацию можно добыть терморектальным криптоанализом.
Начнем с того, что в пруверах используется конструктивная логика Гейтинга, точнее интерпретация логических констант по Брауэру-Гейтингу-Колмогорову (BHK), в которой функция - это примитивный объект (лямбды либо выражения по Мартин-Лёфу), а не декартово произведение множеств определения и значений, как в классической логике и множествах. Изоиорфизм Карри-Говарда для конструктивной логики это то же самое, что изоморфизм без названия между логическими и теоретико-множественными операциями в классической логике и множествах (импликация в классической логике то же самое что подмножество в теории множеств итд). Т.о. возвращаясь к импликации и стрелочкам, в пруверах и прочих хачкелях речь именно о функции в смысле лямбд, поэтому элемент множества A -> B это функция \x.b(x), где x:A и b(x):B. Возвращаясь к функции Nat -> Float, это метод сопоставить натуральному числу или выражению, вычисляющемуся натуральному числу соотв. вещественное число или выражение, вычисляющееся в натуральное число.
>назови свой pid
Слыш, какой пид нахуй, ты чо бля, ты кого опущенным назвал?А вообще - сохранил, лол.
Блеванул с хуеты. Математика это геометрия. Изучение геометрических конструкций средствами алгебры и топологии.
Ты опять выходишь на связь, мудило?
>Математика это геометрия.
Математика это математика. Геометрия это геометрия. Теперь съеби.
Дана Скотт ссыт тебе на ебало.
>Дана Скотт
Твой протыкатель?
>протыкатель?
Сохацкий, це тьi?
Спасибо, %конструктивный% кэп.
Здравствуйте, я хочу устроиться охранником на овощебазу, посоветуйте пожалуйста какие книжки прочитать?
HoTT
Продолжаю свои охуительные истории.
Решил попробовать по совету анона атом. Ну и думаю нужно отписаться о первых впечатлениях.
Установился он сразу с агда-режимом, что это за магия такая не знаю.
Какой гений дизайна додумался до серго текста на сером фоне, я ебал.
Немного растерялся от подчеркиваний красным в случайных местах но сообразил таки что это ебаный спелчекер. Пришлось гуглить как отключить его. Как же меня вся эта хуйня заебала.
Нет подсветки. Ну еб твою мать. Грешен, не так давно отписывался в соседнем треде что она нахуй не нужна и вот она инстант карма. А в агде она бы совсем не помешала. Говорят что нужно ставить отдельный пакет с какого то хуя. Думаю что в таком случае подсветка будет на регулярочках и следовательно точно нахуй не нужна (но возможно ошибаюсь).
Но самое охуительное оказалось что атом дрищет под себя от бэкслешей в дырках, пик релейтед. ВОТ ЭТО ПРИКОЛ. Можно конечно там и лямбду написать, но с такого поворота я знатно прихуел. Сколько таких охуительных приколов может внезапно всплыть, так что я подумал да ну его нахуй пока, уж лучше в говноимаксе как-нибудь пока.
Решил попробовать по совету анона атом. Ну и думаю нужно отписаться о первых впечатлениях.
Установился он сразу с агда-режимом, что это за магия такая не знаю.
Какой гений дизайна додумался до серго текста на сером фоне, я ебал.
Немного растерялся от подчеркиваний красным в случайных местах но сообразил таки что это ебаный спелчекер. Пришлось гуглить как отключить его. Как же меня вся эта хуйня заебала.
Нет подсветки. Ну еб твою мать. Грешен, не так давно отписывался в соседнем треде что она нахуй не нужна и вот она инстант карма. А в агде она бы совсем не помешала. Говорят что нужно ставить отдельный пакет с какого то хуя. Думаю что в таком случае подсветка будет на регулярочках и следовательно точно нахуй не нужна (но возможно ошибаюсь).
Но самое охуительное оказалось что атом дрищет под себя от бэкслешей в дырках, пик релейтед. ВОТ ЭТО ПРИКОЛ. Можно конечно там и лямбду написать, но с такого поворота я знатно прихуел. Сколько таких охуительных приколов может внезапно всплыть, так что я подумал да ну его нахуй пока, уж лучше в говноимаксе как-нибудь пока.
Может кто-нибудь объяснить мне что это вообще такое? Не понимаю что это вообще за синтаксическая категория, как там может быть равно и что это значит.
алсо
Взялся я это доказывать, но рерайты что то не рерайтят нихуя. Только чуть снова сраку не надорвал. (Хотя в принципе я не утверждаю что это невозможно, может быть если кто захочет показать мастер класс буду только благодарен) Заглянул в следующую лекцию и действительно я полез впереди батьки в пекло похоже, потому что МакБрайд доказывает это уже другими техниками. Ух бля думаю почему же это (и это типа сарказм).
еще по мелочи
^U ^U ^C ^. - как же я блядь ору с этой хуйни.
Хипстеры куда то проебали шорткаты из меню. С другой стороны в имаксе в меню проебали половину команд. Так что в этом плане имеем аксиому Эскобара.
Интересный вопрос на счет стрелочек в типах. Иногда аргументы отделяются этими стрелочками, а иногда в агде и коке их хуярят просто друг за другом. Вроде должно быть какое то достаточно простое правило когда как, но я его не улавливаю.
^U ^U ^C ^. - как же я блядь ору с этой хуйни.
Хипстеры куда то проебали шорткаты из меню. С другой стороны в имаксе в меню проебали половину команд. Так что в этом плане имеем аксиому Эскобара.
Интересный вопрос на счет стрелочек в типах. Иногда аргументы отделяются этими стрелочками, а иногда в агде и коке их хуярят просто друг за другом. Вроде должно быть какое то достаточно простое правило когда как, но я его не улавливаю.
Не понимаю такой момент - в категории MAYBE-CAT единичные стрелочки id~> = yes имеют тип T -> Maybe T. Таким образом получается единичная стрелка здесь между различными объектами. Как же так?
> Интересный вопрос на счет стрелочек в типах. Иногда аргументы отделяются этими стрелочками, а иногда в агде и коке их хуярят просто друг за другом. Вроде должно быть какое то достаточно простое правило когда как, но я его не улавливаю.
Бля, ты разницу между простой стрелкой и П-типом знаешь?
Может некоторые скажут что это тривиально, но для меня было довольно неожиданно что в данном примере параметры C D E как бы прибиндины глобально в скопе модуля и например функтор F имеет тип C => D хотя явно это нигде не указывается.
(s : S) -> T s
"Простая стрелка" или П-тип?
Простая.
Врети
П.
А несколько аргументов - это просто вложенные П типы.
Π (x₁ : A) (Π (x₂ : A) (… (Π (xₙ : A))…)) : …
Подумалось, может быть дело в том что в данном контексте (F >=> G) является ко-паттерном, так ли это?
Вкатывальщик ИТТ
Получается любой многочлен можно записать в виде функции?
Получается любой многочлен можно записать в виде функции?
> Получается любой многочлен можно записать в виде функции?
Все что угодно можно записать в виде функции. MLTT итп теории типов это же основания математики.
Как в жнумаксе закомментировать/раскомментировать блок агда кода?
inb4: никак / установить десяток плагинов и неделю ебстись с их настройкой-настроечкой.
inb4: никак / установить десяток плагинов и неделю ебстись с их настройкой-настроечкой.
В spacemacs - SPC ;
А вообще comment-region
В саблайме я просто нажимаю ctrl+/ и он автоматически мне комментирует/разкомментирует все что мне нужно. Я так понимаю нихуя такого нет?
Попробовал ввести uncomment-region - не работает. Может быть нужно загрузить агду. Загрузил. РАБОТАЕТ. Ну заебок. Несколько минут спустя - повторяю те же самые действия - нихуя не работает. Что это за магия такая?
В емаксе есть всё. Только, возможно, тебе самому надо это написать. Ну уж забиндить сочетания клавиш ты сможешь, я в тебя верю
А ссылку выше на гитхаб ты открыл и посмотрел?
Вот странно. Есть много крутых программистов типа вирусописателей Indy, Pr0mix, Izg0y и других, но на дваче подсасывают и унижают только Сохацкого. Почему все внимание к себе привлекает только разная хуйсосня?
>В емаксе есть всё. Только, возможно, тебе самому надо это написать. Ну уж забиндить сочетания клавиш ты сможешь, я в тебя верю
Понимаешь, братишка, я пытаюсь разобраться в достижениях компуктер саенса на передней грани человеческих достижений и голова и так уже кипит нахуй. Поэтому у меня нет ни сил ни малейшего желания разбираться с ебаным говноредактором в котором абсолютно все по умолчанию через жопу и нихуя не работает нормально.
Нужно всего лишь прочитать томик в несколько сотен страниц документации и проникнуться ебанутой философией в которой нихуя нет но можнозделоть.
Но делать то нехуя придется разбираться похоже.
Они разбираются с -- комментариями, а я пробовал {- -} раскомментировать. Но это не важно, не знаю что я должен был вынести из этого обсуждения по-твоему. Я понял только то что у них нихуя не работает, но этим меня уже не особо удивишь.
>я пытаюсь разобраться в достижениях компуктер саенса на передней грани человеческих достижений
Не понял, а агда тебе зачем тогда?
Жми Alt+; и не будь тупым, заколебал
>Жми Alt+;
Жму - добавляются -- в конце строки - ору с прыщефункциональности
>и не будь тупым, заколебал
не будь батхертом
Ну значит холоп, разработавший agda-mode, не позаботился об удобстве для тебя-барина. Живи теперь с этим.
Мне просто неприятно видеть как вроде бы неглупые люди уплетают куски кала и визжат от радости. Но полагаю каждому свое.
Да, вот уж какая неприятность. Компьютер саентинст позволяет себе такую дерзость, как вместо занятий компьютер саенсом писать плагины для текстовых редакторов, чтобы какому-то уёбку с двачей было поудобнее черкаться, чтобы он через неделю бросил. Как страшно жить.
Теперь это настройки текстовых редакторов тред.
Шел бы ты уже подшился, маня.
Сохацкий, це тi?
>нихуя не работает нормально
>Я НЕ ТРОГАЛА, ОНО САМО
Тыж ебнутый. У тебя там настолько дохуя кода, что тяжело вручную закомментировать?
Отче наш, Мартин-Лёф!
Да святится имя твое, да придет интерпретация логических констант по Брауэру-Гейтингу-Колмогорову;
Да будет изоморфизм Карри-Говарда на небе и на земле;
Хлеб наш конструктивный вычисли нам днесь;
И прости нам тезис Черча, как и мы прощаем исключенного третьего должникам нашим;
И не введи нас в интуиционизм, и избавь нас от невычислимого.
MLTT.
Ты всерьез считаешь, что ты "вроде бы неглупый"?
Сохацкий снова горит
https://twitter.com/5HT/status/1113196186264117252
https://twitter.com/5HT/status/1113196186264117252
Он же сам на эрланге пишет.
Правильно, семенсеменыч, сам себя не похвалишь - никто не похвалит. Только не говори, что у такого убогого петуха как ты есть ещё более убогие подсиралы.
Гениально. Апплодирую стоя хуем тебе по лбу.
Конструктивист должен знать:
- изоморфизм Карри-Говарда и тезис Чёрча;
- содержание диссертации Брауэра в переводе Гейтинга;
- пять уровней языка и четыре способа отрицания по Маннури;
- интерпретацию логических констант по Брауэру-Гейтингу-Колмогорову;
- теорию статистического обучения Вапника и модель spikgram Миколова;
- отличия машины Тьюринга от машины Поста.
Конструктивист обязан:
- отрицать закон исключённого третьего;
- отрицать любую математику, не выразимую через типизированную лямбду в MLTT или нормальные алгорифмы Маркова;
- переписать на прувере AUTOMATH де Брауна книгу "Основы математического анализа" Ландау;
- представить все формальные теории в терминах алфавитов, термов и манипуляций с ними;
- свести гомологическую алгебру к исчислению предикатов, используя нумерацию Гёделя.
>горит
Блатной свой жаргончик используй с имбицилам в курилке, на ДОУ или Ебаном!
Ты тут недавно?
Сохацкий, це ті?
Если ты не понял мысль в посте, я объяснять ее не буду. Твой бред начинает надоедать.
> - отрицать закон исключённого третьего;
Гугли теорему Дьяконеску, эту скрепу можно доказать конструктивно.
> свести гомологическую алгебру к исчислению предикатов, используя нумерацию Гёделя.
К cubicaltt ваши гамалогии уже сводят. Не очень активно, но примеры есть даже у Мортберга на гитхабе. Тебе ж говорят, мань, вся математика по своей сути конструктивна, если что-то ещё не доказали в пруверах, значит этим просто некому заниматься.
Ты узнай что такое гамалогии сначала, патом уже своди.
> Ты узнай что такое гамалогии сначала, патом уже своди.
Мне твои гамалогии в хуй не стучат. Я говорю, кому это интересно, уже делают.
>вся математика уже конструктивна
>мне твоя математика в хуй не стучит
>не очень активно, но делают
Тож проиграл с этого довена-пиздабола?
Ты еблан, реально. Какие тебе гамалогии, ты русского языка не понимаешь, хотя являешься носителем. Может быть хоть отсюда сьебешь? Гореть можно где-нибудь ещё.
Очень сочный бабах, аж можно руки греть.
Когда люди не понимают тебя, они не думают что они тупые, они думают что ТЫ тупой (с) Конфуций
>Гугли теорему Дьяконеску…
Что‐то не гуглится; можно ссылку?
мимокрокодил
Diaconescu theorem же, все гуглится. Даже видос на ютубе есть. https://www.youtube.com/watch?v=21qPOReu4FI
>Diaconescu theorem
Да, так гуглится.
Напыщенные математики послали сюда. Дублирую вопрос.
Хотелось что-нибудь почитать фундаментальное о формальных системах, как-то связать это с программированием, так как я программист. Объясните нубу, с точки зрения математики эти вещи потеряли актуальность с появлением HoTT. Например если хочется математики то нет смысла читать Введение в математику Клини, а нужно читать HoTT? Подозреваю, что этот вопрос всех заебал, но все-таки.
Хотелось что-нибудь почитать фундаментальное о формальных системах, как-то связать это с программированием, так как я программист. Объясните нубу, с точки зрения математики эти вещи потеряли актуальность с появлением HoTT. Например если хочется математики то нет смысла читать Введение в математику Клини, а нужно читать HoTT? Подозреваю, что этот вопрос всех заебал, но все-таки.
>эту скрепу можно доказать конструктивно.
Аксиому выбора уже доказал? Только в классическом виде, не конструктивную псевдоаксиому.
> Аксиому выбора уже доказал? Только в классическом виде, не конструктивную псевдоаксиому.
В MLTT это не аксиома, а доказуемая теорема. Мартин-Леф доказал. И именно в том смысле, как она понимается в ZFC, только классически, в ZFC она недоказуема, поэтому классически в неё предлагается как раз таки уверовать.
> Объясните нубу, с точки зрения математики эти вещи потеряли актуальность с появлением HoTT
Нет, не потеряли. Более того, не зная азов, ты и HoTT не поймешь.
> Хотелось что-нибудь почитать фундаментальное о формальных системах, как-то связать это с программированием
"Programming in Martin-Lof type theory", например, но с нуля такое не зайдет. Хотя бы о матлогике нужно иметь представление.
О мат логике представление есть. В вузике даже что-то типа теории формальных языков было. Но я уже нихуя не помню
Переформулирую вопрос. Как вкатиться, чтобы понимать принципы того, чем я занимаюсь вообще связь программирования с математикой, какие-то определения, что такое вычислимость вообще и т.д. Software Foundations? Ну и конечно хотелось бы и основания математики понимать, а это как я понимаю HoTT теперь, или неправильно понимаю?
> связь программирования с математикой
Изоморфизм Карри-Говарда.
> какие-то определения, что такое вычислимость вообще и т.д.
В вышеупомянутой книжке
> Software Foundations?
Вполне. Для агды ещё PLFA.
> Ну и конечно хотелось бы и основания математики понимать, а это как я понимаю HoTT теперь, или неправильно понимаю?
HoTT очень сырая. Та же аксиома унивалентности Воеводского в ней недоказуема, доказать её можно в cubicaltt, ещё более сырой. Это не те темы, с которых нужно вкатываться.
>Та же аксиома унивалентности Воеводского в ней недоказуема
Ну и? HoTT Book - всё равно - всё ещё самый крупный источник по теме. И написана книжка очень хорошо. А сразу с Cubical Type Theory никто начинать не будет.
>доказать её можно в cubicaltt, ещё более сырой.
Не только, в шапку посмотри.
>Изоморфизм Карри-Говарда
В какой категории этот "изоморфизм"? Три года уже пытаемся выяснить это с пацанами из /math, ты всё никак ответить не можешь.
Если ты не понял мысль в посте, я объяснять ее не буду. Твой бред начинает надоедать.
Бампецкий вопросам
Почему стоит только спросить хоть что то немножко посложнее "посоны хачу вкотиться!111" всех икспертов как ветром сдувает.
Почему стоит только спросить хоть что то немножко посложнее "посоны хачу вкотиться!111" всех икспертов как ветром сдувает.
Да скучные вопросы просто.
Намёк: Obj = Set
Ну и на тип морфизма посмотри
Бля, я это и без тебя вижу. Дальше то что?
Нахуй эта игра в кошки-мышки, пиши прямо что и как, не будь гнилым пидорасом, можешь это для своих студентиков оставить, которые тебя на хуй послать не могут.
Это типа доёбка до слова "изоморфизм", вместо которого должно быть "соответствие"?
Конструктух такой конструктух.
>кококо
ясно.
> В какой категории этот "изоморфизм"? Три года уже пытаемся выяснить это с пацанами из /math, ты всё никак ответить не можешь.
С воображаемыми? Ты один такой ебнутый, мань.
> Это типа доёбка до слова "изоморфизм", вместо которого должно быть "соответствие"?
Будто не одно и то же.
> Конструктух такой конструктух.
По делу возражай, пукнутый, или мимо иди.
Как доказать modus ponens?
> Как доказать modus ponens?
Элиминатор импликации, ты хотел сказать. Построением пруф-обьекта, удовлетворяющего этому правилу вывода, очевидно же. "Модус пони поненс" это что-то из Аристотеля, доказательство - онскозал.
модус поненс это правило вывода взятое за основу. Как аксиома. Это не работает так что "Вот просто это правильно и примите это". Это работает так "Если мы возьмем модус поненс и несколько аксиом, то сможем вывести такие логические заключения". Ты можешь взять любое другое правило вывода и другие аксиомы и получишь свою аксиоматическую систему. Вопрос в том будет ли она выводить те же логические выводы, что и ты. Она может будет выводить что-то типа "Если конь животное и нефть топливо, то Топливо конь"
ПИДОРЫ ПОЧЕМУ МНЕ НИКТО НЕ ОТВЕЧАЕТ?
Потому что вопросы тупые.
Ну это вообще ебанутся.
А может это вы тут тупые, на самом то деле?
Да, мы тут все тупые, отвали уже.
Очень хорошо, но также интересует мнение кого-нибудь кто не тупорылый уебан.
Я давно не писал на агде, поэтому могу ответить на вопросы только по коку.
ЧИТАЙ ЁБАНЫЙ МАНУАЛ КУСОК ГОВНА ТАМ ВСЁ НАПИСАНО
> Эта гнилая отрыжка совершенно не по делу
Я продолжу ждать.
Очень даже по делу. Ты не читаешь ёбаный мануал и просишь, чтобы кто-то другой почитал и объяснил тебе. Ты жалок.
Съеби уже мразь гнилая, твое охуительное тупорылое мнение никого не ебет.
Справедливости ради, в мануале есть не все. Нотация в агде типа {B : A -> Set} для характеристической функции B a [a : A], например. У Мартин-Лефа тоже не написано, что в таком случае B : A, только в одном месте вскользь упомянуто, что характеристическую функцию можно интерпретировать как подмножество. Конечно, можно и догадаться, что в этом случае В это подмножество А, т.к все элементы В принадлежат А. Но по хорошему, в правильной нотации не должно быть такого, что нужно что-то додумывать.
Как это `B : A -> Set` и `B : A` одновременно? Кроме того, характеристическая функция - это же объект изоморфный подмножеству, а не оно само.
О каких "множествах" вы вообще говорите, совсем ебнулись? В программульках нет никаких множеств, это только в математике.
Блин блинский, и правда, как же мы так протупили?
Ну и нахуя ты сюда пришёл тогда?
Ну чо ты, напиши на стак оверфлоу лучше. Там тебя точно нахуй не пошлют.
Подумываю вкатиться в верификатора. Поясните что это за ебала такая и какие подводные?
что за
> алгоритмы ЦОС
помню в вузике изучали z-преобразование, какая то полная ебала бесполезная. Так то и кодеки ведь тоже "ЦОС", какое-то широкое понятие.
что за
> алгоритмы ЦОС
помню в вузике изучали z-преобразование, какая то полная ебала бесполезная. Так то и кодеки ведь тоже "ЦОС", какое-то широкое понятие.
> Как это `B : A -> Set` и `B : A` одновременно?
А вот так. https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.RulesForTheStandardSetFormers
> Кроме того, характеристическая функция -
Пропозициональная же. Совсем заговорился.
> О каких "множествах" вы вообще говорите, совсем ебнулись? В программульках нет никаких множеств, это только в математике.
Тыскозал? Про MLTT не слышал, что ты тогда в этом треде потерял?
Что-то я всё равно ничего не догнал.
1. B : A -> Set
B - это семейство типов, индексированное типов A. Оно задаёт подмножество в типе А (те индексы, для которых соответствующий тип населён). Если бы в агде было элементарное отношение подтипа :>, и было бы верно B :> A, это, конечно, здорово, но вроде нет такого, потому что это не умещается в теорию (хз почему).
2. B : A
B является элементом в типе А. Вот как это вообще связано с 1?
При чём тут информация, доступная по ссылке, тоже не понял. Там из чего-то следует, что стрелочный тип может каким-то образом стать нестрелочным? Или что у одних и тех же переменных может быть два типа, один стрелочный, другой нет?
>MLTT
Теория множеств Мартина-Лефа, а не что то по буковкам не сходится никак. Подучил бы ты уже мат-часть, конструшок, сколько можно поносом под себя дристать.
Martin Lёф'а TEORIA T\/T |-| () }|{ E ( T B
Делаю лямбда куб: быстро, недорого. Индуктивные типы за дополнительную плату.
> Теория множеств Мартина-Лефа, а не что то по буковкам не сходится никак. Подучил бы ты уже мат-часть, конструшок, сколько можно поносом под себя дристать.
Тебе за шиворот поносом надристал. И андеркатом твоим из барбишопа жопу вытер. Изоморфизм Карри-Говарда, маня, пропозишены как типы / множества. Я уже объяснял, когда типы могут рассматриваться как множества, а когда не могут. Это прямо следует из определения множества в MLTT. И если тип с вычислительной точки зрения задан как множество, то в данном случае он и будет множеством. Если ты этого понять не в состоянии, проблема в тебе, а не во мне и не в MLTT.
> B является элементом в типе А. Вот как это вообще связано с 1?
И подмножеством А. Т.к все элементы В это элементы А.
"Элемент" и "подмножество" - разные вещи. Да и элементы B - это функции, а не элементы A.
Це тi?
> "Элемент" и "подмножество" - разные вещи
В данном примере - нет.
> . Да и элементы B - это функции, а не элементы A.
Элементы пропозициональной функции В это таки элементы А.
>Я уже объяснял
Лол, петух все на своей волне.
ОК, пополнил словарик петушиного:
математика - вычисления, они же - рефлексы
кризис математики - теоремы Геделя
аксиома - это не аксиома
отличие актуальной бесконечности от потенциальной
- я все это сто раз объяснял
формализация - проблема останова
множество - тип
Теория типов говно, парадокс Рассела выдуман, а пропозициональной логики достаточно чтобы описать любую формальную символьную систему. Дискасс.
Я не виноват, что ты настолько тупой, что даже просто механически пересказать мои слова не в состоянии, не говоря о том, чтобы понять. Почитать источники, на которые я ссылаюсь ты не можешь, потому что там какие-то буквы нерусские,это я понял. Я вообще не представляю, что тебе от меня нужно и с какой целью ты за мной бегаешь по всему мейлру года 3 уже как. В каком месте я тебе настолько больно сделал, чтобы вызвать такую злокачественную батруху?
Опиши хотя бы кванторы пропозициональной логикой, гейний гамалогий.
Лол, конструктух в своем манямирке правда думает что какой-то негодяй бегает за ним 3 года и не понимает что над ним орет половина мейлру.
Нет, мань, таких дебилов тут 1,5 клоуна максимум. Причём, возражений по существу от вас так и не поступало. А препирания уровня детского сада с каким-то унтерменшем (или с двумя, что то же самое) мне неинтересны.
Зато я ебал твою мамашу.
Я тупенький и плохо понимаю в логике. Что посоветуете?
Непейвода
> Опиши кванторы
А что его описывать? В пропозициональной логике квантор и является пропозициональным знаком. Такой символ нельзя сказать, его можно только показать.
Если нормально с английским, есть Open Logic Text. Если плохо, учи английский.
Писатьнебудешьникогда
Портфель собрал? Или у вас каникулы?
не хожу в вуз
Новая Agda, оказывается, релизнулась.
http://hackage.haskell.org/package/Agda-2.6.0/changelog
http://hackage.haskell.org/package/Agda-2.6.0/changelog
Вкусно, как новый орбит со вкусом кубов.
Надеюсь, в следующем lts'е уже будет. Без стека агду ставить я ебал.
Сколько времени нужно на освоение каждого из этих пособий?
Как произоморфировать хотя бы утверждение:
a ∈ A ⟶ a ∈ B
a ∈ A ⟶ a ∈ B
>Added a new sort Prop of definitionally proof-irrelevant propositions.
Такая же хуитка как в петухе? Которая хуй пойми зачем нужна и вообще "was a mistake" по мнению некоторых.
В петухе немного не очень, потому что там реальная иррелевантность только в разрешимых случаях, если не добавлять аксиому К. А в агде без аксиомы нормально теперь.
Скорее как в Lean.
>аксиому К
Какие такие аксиомы, ведь швятой Браузер и пророк его Мартин-Леф так зделали что никакие аксиомы не нужны а все на рефлексах делается? Срочно вызываю конструктивного петуха в тред.
Уйди отсюда, жирнота.
Ты что еще не уверовал? Покайся грешник пока не поздно, а то изоморфизм Кари-Говарда тебя накажет!
Пишешь флаг --without-k и нет никаких аксиом. Или сразу пишешь на коке, там по умолчанию нет.
А это и не аксиома, просто название такое
>А это и не аксиома, просто название такое
Сверился со словариком на всякий случай:
>аксиома - это не аксиома
и правда, все сходится!
А что же тогда интересно?
>зделали
Сохацкий, це тi?
Объясните мне кто-нибудь максимально популярно - кого и для чего может вообще ебсти что два рефла или вообще доказательства равны между собой или нет? Ну вот реально на практике какие возникают затыки?
Меня лично отсутствие равенства бесило когда я делал структурки с пропами. Например, есть две алгебры с одинаковыми носителями и одинаковыми законами. Но равенство их доказать не можешь, потому что пропы, хотя по смыслу равенство имеет место. И приходится везде таскать разрешимость на носителе как гипотезу, а это нахуй надо? Ну или K прописывать.
>Например, есть две алгебры с одинаковыми носителями и одинаковыми законами.
Почему бы тогда не выбрать один вариант и использовать его? смекалочка
Ты конченый или троллировать пытаешься?
Да.
Я беру и пишу тип Nat. А потом пишу тип HuiNat. Потом пытаюсь написать zero=huizero но ничего не получается ((((( Поможите люди добрые придумайте систему типов чтобы все работало как я хочу.
Хотт же. Доказываешь изоморфизм, получаешь равенство.
Разве там равенство не только между объектами одного типа?
В любом случае, это сарказм был жи, в том плане что я не представляю на хуя это вообще нужно.
You might wonder why we do not just write the following for this theorem:
∀ {x y z : ℕ} → x < y → y < z → x < z
This looks more elegant, because we do not have the “≡ tt” everywhere we are
using _<_. But this expression will not type check, because as defined in the IAL,
_<_ returns a boolean (), and a boolean cannot be used as a type.
А такую оказию передовые разработки теории типов способны разрешить? А то кукарекать про изоморфизмы горазды, а вдруг хуякс и надо все по два раза писать один раз для Set (Prop) другой раз для (bool). Еще бы нормальный полиморфизм для явных-неявных аргументов завезли. Или это НОРМА и по-другому никак? Надеюсь что не оскорбил чьи то нежные чувства этим вопросом в очередной раз.
∀ {x y z : ℕ} → x < y → y < z → x < z
This looks more elegant, because we do not have the “≡ tt” everywhere we are
using _<_. But this expression will not type check, because as defined in the IAL,
_<_ returns a boolean (), and a boolean cannot be used as a type.
А такую оказию передовые разработки теории типов способны разрешить? А то кукарекать про изоморфизмы горазды, а вдруг хуякс и надо все по два раза писать один раз для Set (Prop) другой раз для (bool). Еще бы нормальный полиморфизм для явных-неявных аргументов завезли. Или это НОРМА и по-другому никак? Надеюсь что не оскорбил чьи то нежные чувства этим вопросом в очередной раз.
Движок съел жирную B от чего то, но думаю и так понятно.
Пиздец, как же я подгорел с твоей тупости.
Стоишь на асфальте, в лыжи обутый. То ли лыжи не едут, то ли ты ебанутый. Ты нормально перепиши ,тогда будет тайпчек проходить. Очевидно же, что _<_ не совсем то, что тут нужно. Но, это конечно же, изоморфизмы виноваты и лично Мартин-Леф. Пиздец ты клоун.
Типы и функции - не одно и то же, очевидно, поэтому надо сначала написать одно, потом другое, потом доказать эквивалентность и пользоваться этой эквивалентностью где хочешь. Set (Prop) и bool сильно разные по смыслу, так что ничего удивительного
В приципе-то, можно было придумать штуковину, которая залезает в кишки разрешающей процедуре и восстанавливает из неё тип с подходящей алгеброй пруфтермов. Но это чисто механическая вещь, которая не относится к самой теории, где-то на уровне тактик и солверов.
В агде вообще есть REPL?
Теория типов говно, парадокс Рассела выдуман, а пропозициональной логики достаточно чтобы описать любую формальную символьную систему.
> Теория типов говно, парадокс Рассела выдуман, а пропозициональной логики достаточно чтобы описать любую формальную символьную систему.
Всё так. Пацаны, расходимся
Призрак Витгенштейна захватывает тред. Всем на выход.
>Ты нормально перепиши ,тогда будет тайпчек проходить.
Ты че совсем ебанутый, умственный инвалид блядь, это ж пример из книги, я должен что ли писать автору - все хуйня, срочно издавайте второе издание.
>Но, это конечно же, изоморфизмы виноваты и лично Мартин-Леф
Ну когда идет пиздеж про то что программы и логика одно и тоже, а потом внезапно оказывается что для вычислений мне нужно один тип заводить, а для утверждений об этих вычислениях совсем другой, у меня складывается стойкое ощущение что где то меня наебывают.
>Set (Prop) и bool сильно разные по смыслу
Вот Prop может быть населен а может быть не населен, а у bool как раз два конструктора - просматривается некоторый изоморфизм.
>Но это чисто механическая вещь, которая не относится к самой теории, где-то на уровне тактик и солверов.
В агде обычно ведут речь о том что вычисления и мета-вычисления живут в одной реальности. Как минимум хотелось бы этого в идеале.
И вообще я вижу тут стандартный набор из гнева, отрицания, торга. Можно было в таком же ключе сказать
> есть тип list of nat а есть тип list of bool и как ты один в другой засунешь, ты что ебанутый? Поли-чего блядь, че несет. Не ну можно написать шаблонизатор который подставляет текст, может быть.
> Ну когда идет пиздеж про то что программы и логика одно и тоже, а потом внезапно оказывается что для вычислений мне нужно один тип заводить, а для утверждений об этих вычислениях совсем другой, у меня складывается стойкое ощущение что где то меня наебывают.
Над этим школьным бредом даже не орать хочется, а посочувствовать губошлепу, который это пишет. Ощущение у него складывается. А у тебя не складывается ощущение, что если против MLTT во всем мире копротивляется ровно один залупок из северной Нигерии, то проблема может быть и не в MLTT вовсе? Или это слишком сложно для тебя, а, ниспровергатель подпивасный?
>Вот Prop может быть населен а может быть не населен, а у bool как раз два конструктора - просматривается некоторый изоморфизм.
Ну да, просматривается, хотя это, строго говоря, совсем не изоморфизм. Проблема в том, что в каждой конкретной ситуации этот самый изоморфизм надо прописывать руками.
>В агде обычно ведут речь о том что вычисления и мета-вычисления живут в одной реальности. Как минимум хотелось бы этого в идеале.
Хотелось бы, конечно. Не надо забывать, что пруф ассистанты - это work in progress, и разумно было бы сперва найти хорошие теоретические основания, подходящие для практики, а уж потом все удобства, свистелки и перделки.
>> есть тип list of nat а есть тип list of bool и как ты один в другой засунешь, ты что ебанутый? Поли-чего блядь, че несет. Не ну можно написать шаблонизатор который подставляет текст, может быть.
Ну всё правильно, либо ты сам пишешь руками вложение одного типа в другой, либо пишешь механическую процедуру, которая за тебя это делает, если это возможно. Вообще непонятно, а хули ты хотел-то?
>Ну когда идет пиздеж про то что программы и логика одно и тоже, а потом внезапно оказывается что для вычислений мне нужно один тип заводить, а для утверждений об этих вычислениях совсем другой, у меня складывается стойкое ощущение что где то меня наебывают.
И вообще-то, конечно, ты тут наёбываешь сам себя, потому что Set (Prop) - это и есть логика, а bool - это всего лишь тип результата для разрешающих процедур. Если вопросы разрешимости тебя не беспокоят, можешь выбросить этот bool нахуй и писать в типах. Если наоборот, только они и беспокоят, можешь выбросить логику. А если всё-таки надо усидеть на двух стульях, как это часто бывает, пиши и то, и другое, и доказывай эквивалентность.
"вычисления и логика - одно и то же", конечно, означает только то, что истинностные значения утверждений и результаты вычислений живут в рамках одной теории и выражаются одними и теми же сущностями (типами). Разумеется, нет речи о том, что тип вычисления и тип какого-то связанного с ним утверждения совпадают. Если кто-то где-то сказал тебе иное, то да, тебя наебали.
>Вот Prop может быть населен а может быть не населен, а у bool как раз два конструктора - просматривается некоторый изоморфизм.
Для построения такого изоморфизма нужен LEM.
>умственный инвалид
>Вообще непонятно, а хули ты хотел-то?
Ну, все сходится.
Хуйню написал.
>Хуйню написал.
Тебя носом в HoTT ткнуть или сам найдёшь?
Показывай че там у тебя.
Шлите нахуй дегрода. Ничего ты этому хуепутолу не докажешь. У этой хуеты два мнения - одно его, другое неправильное.
Может пойдешь уже подошьешь свой порванный анус, а то заебал уже им тут трясти, может ведь и нагноение начаться.
Страница 127, упражнение 3.9.
Перекат time.
Логикой владеешь? Нужно дальше объяснять?
Ты долбоёб?
Ясно, отбитый тупица пытается рыпаться, ссу на кретина не способного даже в элементарную логику Аристотеля, но чего то там кукарекающего о высоких материя.
>элементарную логику Аристотеля
Когда есть логика Витгенштейна...
Когда есть логика Витгенштейна...
Вы тут все хуйней страдаете со своими типами, вместо того чтобы язык изучать.
Ты только себе на ебало нассал, долбоёб.
Или ясно докладывай свою позицию, или уёбывай отсюда.
Coq:
https://coq.inria.fr/
Lean:
http://leanprover.github.io/
Agda:
https://github.com/agda/agda
HoTT:
https://github.com/HoTT/HoTT
https://github.com/HoTT/HoTT-Agda
https://github.com/gebner/hott3
По теме: http://groupoid.space/.
Cubical Type Theory:
https://github.com/mortberg/cubicaltt
https://github.com/mortberg/yacctt
https://github.com/RedPRL/redtt
https://github.com/redprl/sml-redprl
https://github.com/JetBrains/Arend
Ну и agda --cubical.
По теме: http://cubical.systems/