Школьникам это нужно в учёбе?
>Coq.
Suq.
Ну давай рассказывай, как ты хлебаешь борщ.
На дваче есть те, кто шарят в таком? И их даже больше 2?
На нульчане точно были.
Да полистал книжечку Type-Driven Development with Idris и уже можешь унижать тех, кто не знает.
УЕБЫВАЙТЕ В /MATH
А тут только динамические петухи сидеть должны?
Математика это пучки (гомологии для алгебры и топологии для геометрии), а не доказательства теорем.
>Математика это пучки (гомологии для алгебры и топологии для геометрии), а не доказательства теорем.
Ну что, математики, как подоказывали?
Пифагоровы штаны на все стороны равны. Зачем и почему? Так надо.
Если вы поняли эту шутку, значит у вас нет друзей.
Кок на шиндовс бесполезен, к нему все ставится через ОРАМ, а на винде он так работает, что я ебал. Без линукса туда и лезть не стоит, но это единственный прувер, стоящий внимания. Идрис - очень крутая вещь, вот этот метод постепенного построения с нихуя программы любой сложности "type - define - refine", "дыры", которые сами заполняются при наличии правильного контекста, мне кажется, при должном уровне аутизма на нем можно сделать вообще все что угодно, ЯП богов. Еще и генерация C, JS, NodeJS искаропки. Алсо почти не требует познаний в теории типов, как тот же кок. При этом 100% работоспособности на любой ОС, в Атоме все охуенно работает. Очень недооцененный проект на самом деле, аналогов не имеющий как любят говорить наши пропагандоны. Но как прувер он никакой, такой системы тактик как в коке, в нем не будет никогда. Новомодные пруверы на основе вычислительной теории типов (RedPRL, cubicaltt итд) экспериментальные, там сама теория еще сыровата, но вкатываться можно уже начинать.
>шиндовс бесполезен
Починил, брат.
А можно посмотреть доказательство этого в прувере?
Почему не сделали какого-то Демидовича в онлайн-версии? А не писать на бумаге...
>Демидовича
Нормальный энтри-левел задачник.
По сравнению с конспектом по спасению долбоёбов от бутылки в армейке (Письменный) - так вообще отличный.
>HoTT
>Cubical type theory
Лень читать все эти пейперы, поясните по хардкору чего там есть интересного?
Пытаются рефакторить основы математики.
> Пытаются рефакторить основы математики.
Основания. И их в этом направлении с 1907 года "рефакторят", ещё до Цермело и уж тем более Френкеля.
Ну теперь-то, когда за это взялись программисты, они все сделают как надо.
Это Брауэр-то программист?
Я смогу задачки решать удобней?
Не знаю, наверное. Восторгаются этим делом исключительно программисты, которым нравится думать, что они что-то понимают в основаниях.
> Восторгаются этим делом исключительно программисты,
Пиздежь, ни Мартин-Леф ни Воеводский, ни Барендрегт не программисты.
> которым нравится думать, что они что-то понимают в основаниях.
Только они и понимают. Вместо того чтобы аутизм аутировать, делают настоящую, вычислимую математику а не просто значки рисуют.
Ты, анон, вообще понятия не имеешь, о чем говоришь. Придумал себе там что-то... не делай так больше, пожалуйста!
Ладно.
Решительно подписался.
Нам там скажут "уёбывайте в /pr/"
Вопрос к пользователям Coq. Что вы находите более удобным/естественным/практичным: подход Адама Чипалы с опорой на тактики и автоматизацию или подход, предложенный проектом math-comp?
Хочется научиться писать на кубике, но как-то тяжело даётся. Лекции из мортберговской репы понятны ровно до того момента, как начинают использовать композицию с более чем одним интервалом. Чего-то не хватает для понимания сути. HoTT-book не читал дальше первой главы, стоит сначала почитать?
-> /math
ДОБРО ПОЖАЛОВАТЬ В МЕЖДИСЦИПЛИНАРНЫЙ ЛИМБ
В петухе был особый режим, кажется командой proof он запускался, похожий на ssreflect немного. Так вот его выпилили. Может кто нибудь в курсе как они пришли к этому? Можно ли найти где-нибудь обсуждение этого шага? Я только хотел его освоить и внезапно его пидорнули, как-будто его и не было никогда. А что если кто-нибудь доказал с этим режимом свое охуительное доказательство на сотни тысяч строк. Может они еще чего нибудь выкинут из языка?
>Best guess for this image: martin lof type theory
> В петухе был особый режим, кажется командой proof он запускался,
Че? Это ж обозначение начала доказательства? После этой команды нужно тактики подбирать итд, сама по себе эта команда ничего не доказывала.
Ты уловил шутку, спасибо.
>сама по себе эта команда ничего не доказывала
Никто этого и не утверждал. Вот пример
https://stackoverflow.com/questions/40723002/coqs-mathematical-proof-language-rewriting-in-if-condition
Ну собственно двухминутный гуглинг немедленно приводит к следующему: https://www-verimag.imag.fr/~corbinea/mmode.en.html
Похоже, это давно заброшенная попытка использовать вместо Ltac декларативный язык, похожий на то, что есть в Mizar.
Но оно работает так же как и раньше.
Это где и как оно работает? У меня вот в свежем коке: Error: The reference proof was not found in the current environment.
Нахуя писать хуйню?
> Нахуя писать хуйню?
Себя спроси. Proof с большой буковы пишеццо.
Вот у меня даже в голове не укладывается, как можно быть таким дебилом, как ты. Ты бы хоть сначала перешёл по ссылкам выше, посмотрел, о чём вообще речь.
Мань, ты писать научись сначала.
Ты что-то не так делаешь, а именно, пишешь proof с большой буквы, и у тебя включается обычный интерактивный режим с Ltac'ом. А речь про совсем другое, см. по ссылкам выше.
Ок, я обосрался. Вот тут https://github.com/coq/coq/issues/6842 пикрелейтед хуй пишет, что C-zar нужно снести. Спроси у него, почему.
Мне кажется, тут речь об удалении нерелевантной документации, а не об удалении собственно этого режима.
Я даже больше скажу - раньше в документации была целая глава
> Chapter 11 The Mathematical Proof Language
Но теперь она тю-тю вместе с режимом.
А ведь раньше раздел был с компьютер саенсом. Но похоже что то не взлетел.
Идрис разве не умер уже? Чё вы на нём пишете?
ДинамическиеСтатические опердени.
Ну правда, спроси у них самих на гитхабе\реддите\ирц, чего гадать-то.
Матх жи есть.
>Ну правда, спроси у них самих на гитхабе\реддите\ирц, чего гадать-то.
Пидора ответ.
Нет!
Примеры из книги Type-Driven Development with Idris
Хорош
Парни, это все очень весело, сам обожаю угорать по таким темам. Но можно ли зарабатывать этим деньги не в науке?
А в науке можно, лол? Этим 3.5 человека в мире занимаются, авторы упомянутых в оппосте программ.
maxim.livejournal.com - этот чувак зарабатывает.
По кубику ты можешь ещё только саму работу по CTT посмотреть. Больше ничего нет, увы.
А конкатенативные языки программирования завезли?
Ты про типы в конкатенативных языках?
Про типы и все остальное.
Он зарабатыфвает не этим, а функциональным программированием, причем даже не им, а продуктом, который он написал на эрланге много лет назад.
А зачем?
А в metamath кто-нибудь пробовал вкатиться?
Про типы нагуглилось только это.
http://www.codecommit.com/blog/cat/the-joy-of-concatenative-languages-part-3
Не знаю, как в такую концепцию вписать DT.
Я свой аналог их базовой системы делал. У них уж очень олдово, референс реализация даже не оупенсорс. Основы описаны довольно мутно, без четкой мотивации принятых решений. Все это недостатки хобби-проекта, по нему вышла вроде всего одна статья в каком-то маленьком журнале. У автора не было стимула нормально делать, все сделано для самого себя. Похоже, мало кому в науке сейчас интересны такие вещи.
А нет, наврал, исходники есть. Странно, мне казалось раньше их не было. Может, перепутал с чем-то другим.
>Демидовича
Ебануться, 18 лет прошло с того года, как я универ закончил. У меня уж и хуй стоит от силы раз в неделю, и давление выросло, и зрение упало, а студентов до сих пор ебут Демдовичем.
Так ведь картофан и водочка с тех пор тоже почти не изменились.
Прикольно он заливает как некий опердень на эрланге позволил ему забыть о тяготах бытия и выйти на пенсию. Что то уровня работаю на форексе получаю сто тыщь в секунду. Наверняка либо жена его содержит, либо - еще вероятнее - сданная в аренду квартира от бабушки. Короче, не просто так даже поговорка такая есть - пиздит как хохол.
Про опердень на эрланге - это древняя паста с нульчана.
Опердень там в женском роде и во множественном числе, лол.
Опердень - операционный день, это из банковского сленга.
Видео не смотрел, потом гляну.
1) теория типов - еще тот ФАД, можно прекрасно доказывать теоремки (на конпунктере) и верифицировать что нужно без нее. Даже не думайте спиздануть про Кари-Ховарда.
2) интересно где бы он расположил линейные типы и что там еще придумали новенького (рефайнменты? gradual typing?) на этом своем кубе.
3) проблема написать доказательство из учебника по математике не в том что не придумали еще такой распиздатой теории типов, а в том что привычную математическую нотацию хуй запихнешь в компьютер, все получается очень неудобно и вырвиглазно; разве только идейным лисперам норм, они просто любят жрать говно.
PS на каком сайте посмотреть его списочек с МакЛейнами и прочими пацанами?
Двачую. Вон в metamath не только без типов обходятся на нижнем уровне, но и вообще практически безо всего.
Аутист, ты хуйню сморозил, съеби с треда.
Что это у нас тут за животное подорвалось?
Распетляйте за ats lang, кто-то использовал? Как оно, говорят можно даже дрова на нем делать?
>лисперы
>математическая нотация
Анон, как бы тебе сказать... ты долбоеб, вот.
>на этом своем кубе
>своем
Съеби с треда.
>>лисперы
>>математическая нотация
>Анон, как бы тебе сказать... ты долбоеб, вот.
Попробуй высрать хоть пол-мысли для начала.
>>на этом своем кубе
>>своем
>Съеби с треда.
Говна вьеби, чмо тупое.
AuTiSm.
> теория типов - еще тот ФАД, можно прекрасно доказывать теоремки (на конпунктере) и верифицировать что нужно без нее. Даже не думайте спиздануть про Кари-Ховарда.
Теория типов - это один из вариантов оснований, поэтому и используется в пруверах. Теоретически можно использовать любые другие основания, хоть ZFC, но они дырявые по сравнению с конструктивными типами.
ок
Ты действительно считаешь, что тот мелкобуквенный дебил сказал что-то по делу?
Тебе всё по делу сказали: съеби.
>Тебе всё по делу сказали: съеби.
Попробуй просраться еще чуть-чуть
Как будто рядовые доказывальщики (усирающиеся в треде) вообще хоть примерно представляют как выглядят аксиомы их петуха.
>аксиомы их петуха
Их нет.
То-то же!
Ну охуеть теперь.
> Как будто рядовые доказывальщики (усирающиеся в треде) вообще хоть примерно представляют как выглядят аксиомы их петуха.
А что там представлять? Calculus of inductive construction никто не засекречивал.
Где же можно ознакомиться с аксиомами этой теории? Кстати, вопрос на вскидку - сколько их?
Почему ты разговариваешь, как аспирант со студентом на экзамене? Если хочешь что-то донести, говори прямо, как есть. Правду-матку руби с плеча!
> Где же можно ознакомиться с аксиомами этой теории? Кстати, вопрос на вскидку - сколько их?
Но там не аксиомы, а правила вычисления. Аксиома в теории типов это правило без посылок, в нём только заключение. Т.е это нечто такое, что не следует из чего-то, а задается априори.
Лол, ну ладно, смотри тогда.
Первым делом начинающий coq'ер узнает определение натурального числа. Между тем есть такая аксиоматика Пеано. Там несколько аксиом, например постулируется функция S и то что эта функция инъективна. Я особо над всем этим не задумывался, но как то наткнулся на тот факт что "оказывается" конструкторы в функциональных языках тоже инъективны. Что немного забавно если подумать, что в обычных языках типа java такого свойства у них нет. Таким образом у нас оказывается есть аксиома, которая явно нигде не прописана, но считается общеизвестной. Или что тип можно создать только его конструкторами, или что конструкторы не могут "пересекаться". Может еще есть такие над которыми я бы даже никогда не задумался? Поэтому и хотелось бы получить их полный список.
В одном выступлении Воеводского, он рассказывал что в теории типов много моментов которые передаются как фольклор от компьютер саентиста компьютер саентисту, но ему с позиции математической строгости они совсем не очевидны. Какую то такую штуку он пытался разобрать и нашел ее в какой то огромной и очень сложной книге в последней главе. Но может я чего то недопонял, т.к. я вообще с трудом представляю каких целей пытается достигнуть их проект с унивалентностью и прочим.
И вот я думаю - как бы такого красавца запихнуть можно было бы в компьютер.
>оказывается есть аксиома, которая явно нигде не прописана
Нет, ну если не читать ни документации, ни пейперов по сабжу, и вообще не доставать голову из жопы, то конечно кажется, что нигде ничего не написано. А для желающих есть аж первая ссылка в гугле, ну да чё я распинаюсь.
>в обычных языках типа java такого свойства у них нет
Это с каких пор в Java завезли индуктивные типы вместе с их конструкторами?
Что же там за ссылочка интересно?
https://hal.inria.fr/hal-01094195/document
И в добавок к этому ещё актуальная документация на сайте coq.inria.fr
Где там конкретно про инъективность?
2.2 Inductive Definitions
И это даже не аксиомы, ты можешь просто через индукцию построить термы указанных типов.
Давай тогда доказательство что можно и аксиомы которые оно использует.
Терм на картинке. Про какие аксиомы ты говоришь, я так и не понял. Там правила вывода есть и синтаксис, и они таки описаны по ссылкам, которые я уже дал. Расписывать на бумаге дерево вывода конкретно для этого терма ради тебя я не стану, потому что нахуй мне оно нужно.
Сложные значки какие-то
Да ёбаный по голове, ну на тебе без значков тогда.
>Как будто рядовые доказывальщики (усирающиеся в треде) вообще хоть примерно представляют как выглядят аксиомы их петуха.
>Про какие аксиомы ты говоришь, я так и не понял.
ЧТД
Я тебе уже говорил, что там нет аксиом, сука. Их просто нет. Синтаксис и правила вывода, больше ничего нет, вообще. Ни одной аксиомы.
Лучше бы попытался терм упростить, чтоб людей не пугать.
Ничего страшного в этом терме нет, если знаешь язык. А если не знаешь, то упрощение не поможет. И вообще, захуй читать термы, если они они автоматически генерируются и автоматически типизируются?
Но если аксиом нет, то значит мы ничего в итоге не доказали.
Да съеби ты уже, клоун.
Аксиомы нинужны.
Ой ну все петух совсем порвался.
Математики с тобой не согласятся.
> Но может я чего то недопонял, т.к. я вообще с трудом представляю каких целей пытается достигнуть их проект с унивалентностью и прочим.
> Но если аксиом нет, то значит мы ничего в итоге не доказали.
> Математики с тобой не согласятся.
Ящитаю, ты очень слабо представляешь (если вообще), что такое конструктивизм, конструктивная логика, конструктивные основания. Откуда оно, зачем и почему не основано на аксиоматике. Понятие алгоритма нельзя аксиоматизировать, т.к такая аксиоматизация должна решать проблему останова, а это невозможно, что доказал ещё Тьюринг. По этой же причине неаксиоматизируема и конструктивная логика. Поэтому, вместо аксиоматики, конструктивные теории типов оперируют понятием вычислимости, например, в случае MLTT - операционной семантикой правил построения термов.
Буду весьма благодарен, если кто-нибудь (из еще не подорвавшихся) объяснит мне о какой logic идет речь и каким образом она captures то что там дальше написано
Алсо хотел подсмотреть термин initial algebra в вики
>an initial algebra is an initial object in the category of F-algebras for a given endofunctor F
А ну заебись, теперь то все встало на свои места.
>слабо представляешь
Есть такое, тут спорить не буду.
>Откуда оно, зачем и почему не основано на аксиоматике
Я думал там просто достаточно выкинуть usual suspects из аксиом - двойное отрицание и аксиому выбора - и внезапно получается конструктивизм - на оставшихся аксиомах.
>что доказал ещё Тьюринг
Как же он это доказал без аксиом та. Но если серьезно, распиши эту мысль если можно.
Еще у меня закрадываются подозрения, что ты возводишь fringe или просто модные идеи в разряд абсолюта, примерно как это делает Сохацкий мимоходом с улыбочкой разъясняя щеглам что доказывать теоремы без новомодной системы типов ну никак не получится (это не правда). Брауэр вроде вообще в какую-то эзотерическую хуиту верил и его вообще никто в серьез не воспринимал в свое время.
> Как же он это доказал без аксиом та. Но если серьезно, распиши эту мысль если можно.
Я ж говорю, в конструктивизме главное - построимость объекта, вычислимость терма. Т.е алгоритмическая разрешимость задачи такого построения. И вот, внезапно, не все вычислимо, есть алгоритмически неразрешимые задачи, то же исключенное третье в общем виде, т.е именно в виде аксиомы. Получается, что неконструктивная математика такие дыры просто затыкает невычислимыми аксиомами. Например, проблему останова можно заткнуть исключенным третьим, ну или остановится или нет))) Но с конструктивной точки зрения это манядоказательство уровня /б. Поэтому можно говорить об уточнении понятия алгоритма, а не о его формализации, такими уточнениями являются машина Тьюринга, нормальные алгорифмы Маркова, лямбда исчисление Чёрча итд. Причём, все они равнообьемны. И вместо аксиом там правила вычисления, которые неаксиоматизируемы, или что то же самое, в теории типов не любой тип обитаем.
> Брауэр вроде вообще в какую-то эзотерическую хуиту верил и его вообще никто в серьез не воспринимал в свое время.
Нет. Он не верил в хуйню, он своими словами пытался излагать понятие условного рефлекса, это очень хорошо видно в его диссере. И далее показывал, что абстракция этого понятия даёт возможность строить математические объекты и выводить их свойства рассмотрением таких ментальных построений (2 акта интуиционизма).
Ты говоришь много воды, но по-моему ты не знаешь элементарных основ. Тот анон совершенно прав - без аксиом тебе не к чему применять правила вывода, и ты можешь только полюбоваться на них. Вот тут, например: https://en.wikipedia.org/wiki/Calculus_of_constructions роль аксиомы играет правило вывода 1 (без предпосылок).
> Вот тут, например: https://en.wikipedia.org/wiki/Calculus_of_constructions роль аксиомы играет правило вывода 1 (без предпосылок).
Во-первых, чуть выше я об этом и говорил, что аксиома в теории типов это правило вывода без посылок с заключением. Во-вторых, в правиле 1 по твоей ссылке заключение под чертой начинается с буквы Г, обозначающей контекст, т.е уже имеющуюся типизацию в виде списка гипотетических суждений (абзац Judgements сразу перед правилами). В разных лямбда исчислениях допустимая типизация так же разная (добавляются возможные варианты построения допустимых термов). Почему это нельзя считать аксиоматизацией, я выше рассказал - эти правила не гарантируют априори обитаемость любого типа, построенного с их помощью или что то же самое, не дают решения проблемы останова машины Тьюринга, или опять же, что то же самое, не формализуют конструктивную логику. Правила это уточнение понятия алгоритма, а не его формализация. Поэтому их основа это вычисление (которое возможно не во всех случаях), а не аксиоматика, охватывающая все возможные варианты.
Скажите, откуда цитаты?
Клован, съебись.
>ничо не понятно
>энти ваши котегории
>оправдывайтесь
>из еще не подорвавшихся
Ты в тред пришёл и хуйню несёшь.
Ты тему не осилил, зато хуйню молотить горазд.
Съеби, животное.
Я тебе больше скажу, в CiC даже не одна такая "аксиома", а целое счётное множество. Только они описывают (населяют) всего лишь иерархию универсумов, а логического содержания в них нет, т. е. из них ничего кроме них же самих не следует, и доказывать содержательные утверждения можно без них.
> Скажите, откуда цитаты?
Van Stigt, "Brouwer's intuitionism", вроде из приложения 1 про неопубликованные части брауэровской диссертации. Есть ещё пикрелейтед перевод, тут из кембриджских лекций Брауэра.
>эти правила не гарантируют априори обитаемость любого типа, построенного с их помощью
Это можно как-нибудь прояснить?
>доказывать содержательные утверждения можно без них
Не понимаю. Как доказывать без этого правила? У тебя же доказательство никогда не закончится (если ты от утверждения идешь). Мы или разную терминологию используем (ты под доказательством подразумеваешь просто написание терма?), или ты подразумеваешь какой-то иной принцип доказательства.
>ты под доказательством подразумеваешь просто написание терма?
Ну да, доказательство - это терм, для которого можно вывести тип. Ты говоришь, что если убрать правила вывода без посылок, то не получится построить ни одного конечного дерева вывода, потому что в дереве вывода любое суждение должно быть обоснованно применением правила. Но это не так. В конкретных ситуациях бывает, что применение правила с нетривиальным предположением обосновывается без других правил. Пример: в контексте (T : Type, x : T) можно заключить (x : T), и в силу этого факта можно применить какое-нибудь правило вывода с соответствующей посылкой. Например, можно получить, что терм (fun (T : Type) (x : T) => x) имеет тип в пустом контексте, а это уже содержательное доказательство.
Хороший вопрос, кстати. Мне лично в учебе это все очень помогло, но правда пришлось учить много лишней информации, так что завозить такое в реальные школы преждевременно. Но можно запилить прувер попроще и использовать его, такое уже пытаются делать.
> (ты под доказательством подразумеваешь просто написание терма?)
Да, в конструктивных теориях типов доказуемо только то, что выводимо, т.е сам терм (а не какая-то оторванная от вычисления аксиоматика) является доказательством себя.
> Это можно как-нибудь прояснить?
Правила задают правильность типизации. В них можно выразить, т.е построить только то, что в них выводимо/построимо. Если бы можно было построить всё, то эти правила решали бы и проблему останова машины Тьюринга и любую другую алгоритмически неразрешимую задачу. А так как это невычислимая/непостроимая задача, то она неразрешима в теориях типов. В чем и разница от формализма, там главное непротиворечивая аксиоматика, а в конструктивизме вычислимость. Тут уже встаёт вопрос, что есть существование математического объекта. В формализме это непротиворечивость в системе аксиом, в конструктивизме - построимость/вычислимость терма.
А, типа, не любое истинное утверждение можно доказать вычислением?
> А, типа, не любое истинное утверждение можно доказать вычислением?
В данном случае истинное = вычислимое. С конструктивной точки зрения вне вычислимости/построимости нет никакой истины, например, аксиом, оторванных от конкретного построения.
Ну да, понятно.
Поясните быдлу за линейную логику
>такое уже пытаются делать
Попо дробнее? Может и в школах уже думают конструктивизм распостранять?
Клевый мемас а то надоело букавы читат
ь
Конструктивизм там нахуй никому не нужен, очевидно же. edukera.com есть, либа для кока, формализирующая евклидову геометрию, всякое такое.
Меня всегда интересовало, а вакансии по теме треда есть? Кто это использует и где?
Да есть конечно. Правда, там без учёной степени не берут обычно, потому что оно всё при университетах, ну и это чисто рисёрч, не индустриальное.
>это чисто рисёрч, не индустриальное
Почему в индустрии не используют? Слишкам сложна? Какие причины, вообще? Или там недостатки какие-то серьезные, что проще на джаве команде макак нахуярить по-быстрому?
Ну всего понемногу. Инструменты пока ещё далеки от совершенства, теория местами не такая гладкая, как хотелось бы, экосистема не в очень адекватном состоянии. И конечно, верифицированное ПО и алгоритмы - нишевая штука, потому что далеко не везде разумно вкладываться в формальное доказательство, когда вроде и так нормально и тесты чекаются. Я думаю, это всё временно, и однажды проблемы решатся, и верифицировать ПО будет выгоднее, чем не, но сколько ждать - непонятно.
Верифицированный код нужен (required) очень мало где, всякое по для самолетов да рентгены
> Почему в индустрии не используют? Слишкам сложна?
Сложна конечно. Одно дело быдлоджава, которой за месяц можно любого дегрода обучить, другое - язык, в котором теорию типов нужно знать даже для того, чтобы просто читать код, а уж писать что-то осмысленное, это минимум профильная аспирантура.
То есть, в Airbus и Boeing такие вакансии есть?
>теорию типов
Литературу/курсы не посоветуешь?
>понятие условного рефлекса
Типа стукнул математика по левой коленке - дернулась нога, стукнул по правой - он доказал теорему Ферма. Очень смешно. В любом случае это только твои домыслы.
Нашел перевод одной его статьи. Там в предисловии говорится что ее не хотели принимать в философский журнал, т.к. никто не мог понять что он там за хуергу написал. Хотя казалось бы писать абсолютно лишенную смысла ахинею это modus operandi всех философов.
Еще пред тем как отбросить принцип исключения третьего он его не правильно понял как -A -> -A. У меня вообще глаза округлились от этой хуйни. Но ничего, хуйня, с каждым бывает.
>контекст
Контекст есть и в секвент калкулусе. Там что тоже аксиом нет?
>эти правила не гарантируют априори обитаемость любого типа, построенного с их помощью
Я так уловил что ты предлагаешь что необходимо выполнять вычисления построенного терма чтобы в убедиться в том что они будут конечны. Я слышал в typetheorypodcast с Weirich что существуют формальные системы с теорией типов где этот так. Мне это запомнилось потому что произвело даже некоторое впечатление. Но только к петуху это совсем не относится, т.к. в нем никто в здравом уме не производит вычисления над термами доказательств.
Если теория типов это фад, то теория категорий - это рак ебаный с метастазами. Конечно ни один вменяемый человек не полезет разбираться в их бесполезной абстрактной хуете, поэтому они срут ей в каждой статье на википедии. 1+1? Ну это терминальный объект симплициального эндофунктора...
Хорошо что хоть категориальные основания так и не набрали оборотов, а то какой-нибудь дурачок в этом треде мне бы уже усираясь доказывал что ну никак не возможно построить основания математики без категорий.
>Если бы можно было построить всё, то эти правила решали бы и проблему останова машины Тьюринга и любую другую алгоритмически неразрешимую задачу.
Ты повторяешь этот тезис снова и снова как мантру. Только от этого он не становится более правдой. Или даже более убедительным. Разве что для дурачков что заглядывают в тред чтобы просраться. Мне кажется что ты путаешь что выводимо, что не выводимо и какие из всего этого следствия. Но может быть в этом и есть что то. Но...
Есть такая теорема Геделя. Она очень весомо звучит в любом споре. Теорема Геделя! и можно еще по столу хлопнуть. Вот пример использования этой теоремы типичным дурачком:
>ИИ никогда не будет создан. Потому что теорема Геделя.
Вот у меня тут как раз такие ассоциации возникают.
> Очень смешно. В любом случае это только твои домыслы.
Это не мои домыслы. Если бы ты был знаком с физиологией и прочитал бы хоть начало 2ой части диссертации Брауэра, ты бы понял, что речь именно о рефлексах, т.к там прямым текстом отсылки к высшей нервной деятельности человека, которая рефлекторна. И само понятие примордиальной интуиции - это абстракция временнОго отношения между элементами восприятия, о чем там опять же прямым текстом, ничего даже додумывать не надо.
> Ты повторяешь этот тезис снова и снова как мантру. Только от этого он не становится более правдой. Или даже более убедительным.
А я тебя убеждать собирался? Я обьясняю, что понятие алгоритма неформализуемо по той причине, что такая формализация как формализация любого уточнения понятия алгоритма, в т.ч машины Тьюринга должна решать проблему останова. Иначе это будет не формализация, а только уточнение. Я вообще то излагаю общеизвестное ещё со времён Чёрча. Уже тогда стало понятно, что это невозможно. А ты вот и до сих пор не вдупляешь о чем речь, но ценное школомнение имеешь, разумеется.
Есть где-то во Франции, но это неточно.
>Там что тоже аксиом нет?
Вот не знаю, почему всех в треде так интересует этот дебильный вопрос, но вы может сначала поясните, что вы называете аксиомой? Вот у людей, которые пишут на коке, считается, что аксиом там нет, если только их не добавить, ну и это вполне уместно. Хотя выше в треде уже заметили, что в калькулусе вообще-то есть правила вывода с пустыми посылками, и считать ли их аксиомами - вопрос с неоднозначным ответом. Некоторые вообще называют аксиомами любые правила вывода, что тоже не лишено смысла.
>Я слышал в typetheorypodcast
Пиздец, пиздец.
Вот уж действительно, школьник - это как червь-пидор.
Только хуже.
Я еще и аниме смотрю.
Теперь можешь попробовать собрать свой сракотан по кускам.
>в калькулусе вообще-то есть правила вывода с пустыми посылками, и считать ли их аксиомами - вопрос с неоднозначным ответом
Один местный рефлекторный утверждает что этого делать нельзя и он - тут я цитирую -
>почему это нельзя считать аксиоматизацией, я выше рассказал
Так что либо вникай в его делирий выше по треду, либо спрашивай у него разъяснений. Я лично уже изрядно заебался с ним общаться.
>аниме смотрю.
Его все смотрят.
Тот факт что ты дебил и школьник это не меняет.
>уточнение формализации или формальное уточнение формализации не формализуема точно но это не точно.
Сразу видно человек разбирается в вопросе как рыба в воде. Хотя если у тебя весь мыслительный процесс на рефлексах, то тут уже можно не удивляться.
>Все всем давно известно аргументов не будет ты школоло
Твоя позиция ясна. Больше с тобой дискутировать смысла не вижу.
Я примерно понимаю, о чём он, но у него-то как раз дебильных вопросов нет, так что я не к нему обращался.
То есть то, что ты школьник не отрицаешь.
Фиксирую.
> Сразу видно человек разбирается в вопросе как рыба в воде.
Мань, ну ты же сам прекрасно понимаешь, что пытаешься поспорить просто потому что тебе печет. Возражений по делу от тебя не поступало, одно кукареканье.
> Хотя если у тебя весь мыслительный процесс на рефлексах, то тут уже можно не удивляться.
Вся высшая нервная деятельность человека имеет рефлекторную природу, это медицинский факт. Уже даже Павлов это показал более чем убедительно, не считая более поздних исследователей. Ты простую вещь пойми - твоя батруха и незнание чего-то - это не аргумент, а недостаток. Твой недостаток.
Анус себе зафиксируй, клоун.
>эта школоболь
Ясно.
Мамку ебал.
Вы ещё пососитесь тут, придурки.
А ты не завидуй :3
А ты мне не указывай, хочу и завидую.
>хочу и завидую.
Бедняжка :3
Не надо меня жалеть. Лучше повыёбывайся, а я буду смотреть.
>Лучше повыёбывайся
Не хочу :3
>Я примерно понимаю, о чём он
Может мне расскажешь и мне тоже станет немножко понятнее о чем он?
У аксиом нет вычислительного смысла. Они просто дают тебе готовые неделимые термы из нихуя. Согласно представлению о математической истине как о чём-то вычислимом, теоремы, полученные из аксиом, не являются истинными, тогда как хорошие правила вывода вычислительный смысл обеспечивают. В широком философском смысле вычислимая истина представляется более достоверной. Ну так вот, в исчислении конструкций и его расширениях хорошие правила вывода, и по умолчанию тех самых плохих аксиом там нет, типа закона исключённого третьего и всего такого. Это всё, конечно, зависит от того, что мы называем или не называем аксиомами.
Ожидал увидеть ответ в форме
>Правило вывода нельзя считать аксиомой потому что...
Но получил
>Аксиома это не правило вывода потому что...
Ну это для меня не открытие.
>В широком философском смысле вычислимая истина представляется более достоверной.
>, с точки зрения интуиционизма/конструктивизма
Поправил тут немного, можешь не благодарить.
>Правило вывода нельзя считать аксиомой потому что
Я же написал, почему. Потому что правила вывода и аксиомы - это разные вещи, в определённом контексте. То, что в другом контексте они могут быть отождествимы, я тоже писал выше.
>с точки зрения интуиционизма/конструктивизма
С точки зрения интуиционизма/конструктивизма невычислимое вообще никак не истинно, а широкий философский смысл позволяет расценивать вещи как более или менее достоверные.
Вот интересно стало, какой вычислительный смысл у терма refl, в конструкции refl:1=1.
Еще есть такие мысли. По вашему жизненно необходимо чтобы поверить в утверждение необходимо чтобы оно было справа от двоеточия и была некая программа слева. Я спрашиваю у интуициониста знает ли он доказательсто теоремы Х. Он дает мне в ответ программу. Я запускаю эту программу и вижу на экране
> "да"
или
> 42
Какая мне польза от этой программы и как она может поднять мою уверенность в верности теоремы Х мне не совсем ясно.
>какой вычислительный смысл у терма refl
Такой же, как у любого конструктора индуктивного типа - тривиальный.
>По вашему
По какому по-нашему? Я не из "этих". Мне вообще похую.
>Какая мне польза от этой программы и как она может поднять мою уверенность в верности теоремы Х мне не совсем ясно.
Сама по себе программа не должна поднимать уверенность, уверенность должна поднимать другая, вспомогательная программа, которая проверяет синтаксическую корректность первой. Ну а синтаксически корректные программы соответствуют корректным доказательствам теорем.
Ты наверняка представляешь себя ведущим философом математической мысли современности, но твои разъяснения полностью лишены содержания, примерно как это смешно утверждение
>В них можно выразить, т.е построить только то, что в них выводимо/построимо.
>Я же написал, почему. Потому что правила вывода и аксиомы - это разные вещи, в определённом контексте. То, что в другом контексте они могут быть отождествимы, я тоже писал выше.
Конечно теперь я буду с наслождением бегать по всему треду и искать что ты там и где написал и пытаться вывести "контекст" который ты подразумевал.
>а широкий философский смысл позволяет расценивать вещи как более или менее достоверные.
Спасибо, пойду наверну десяток томиков философии от Гегеля до Геделя, чтобы насладиться твоей непоколебимой правотой еще полнее.
>Ты наверняка представляешь себя ведущим философом математической мысли современности
Неправда, я не от кого не скрываю, что я школьник без пруфов (не тот, что выше).
>но твои разъяснения полностью лишены содержания
Тоже неправда. Есть теоремы, выводимые в одном случае и невыводимые в другом. Разница объективная и нетривиальная.
>Конечно теперь я буду с наслождением бегать по всему треду и искать что ты там и где написал и пытаться вывести "контекст" который ты подразумевал.
Я просто пытаюсь объяснить что-то, что знаю сам, тем, кому это может быть интересно. Убеждать тебя в своей правоте я не буду.
>Спасибо, пойду наверну десяток томиков философии от Гегеля до Геделя, чтобы насладиться твоей непоколебимой правотой еще полнее.
Лучше, чем сраться на дваче на пустом месте.
>Сама по себе программа не должна поднимать уверенность, уверенность должна поднимать другая, вспомогательная программа, которая проверяет синтаксическую корректность первой.
И у тебя нет даже ни малейшего сомнения что есть какая то странность в этой конструкции?
Сомнение есть всегда, его не может не быть. Но никаких очевидных проблем здесь я не вижу.
>Неправда, я не от кого не скрываю, что я школьник без пруфов (не тот, что выше).
Вот так споришь с кем то на сасачах до белого каления, а это оказывается школьник в итоге. Не первый раз на эти грабли наступаю. Ну успехов тебе в учебе.
Вот так на сосаче тебя спрашивают, как ты понимаешь чужое высказывание, а потом оказывается, что вы спорите.
> Какая мне польза от этой программы и как она может поднять мою уверенность в верности теоремы Х мне не совсем ясно.
Мозгов у тебя нет потому что. Я тебе миллион раз объяснял как это связано, ты же ебалай даже изоморфизм Карри-Говарда до сих пор не осилил. Хотя это и есть ответ на твой вопрос, дегрод ты злоебучий.
Вот это утверждение
>В них можно выразить, т.е построить только то, что в них выводимо/построимо
выдал школьник или уже-не-школьник?
>Даже не думайте спиздануть про Кари-Ховарда.
>ты же ебалай даже изоморфизм Карри-Говарда до сих пор не осилил
Вот ведь тупой шакал.
Мамку ебал.
>В них можно выразить, т.е построить только то, что в них выводимо/построимо
Это утверждение выдал некто, не уточнивший свой статус школьника или не-школьника.
Печально. Так бы хоть стала ясна причина его бессвязных лепетаний.
> тред про изоморфизм Карри-Говарда
>Даже не думайте спиздануть про Кари-Ховарда.
Мань, это суть пруверов как явления. То, что у тебя на это не хватает ума, как и на многое другое, само по себе доказывает только то, что ты тупень, а вовсе не то, что ты прав (как ты думаешь).
Я, блять, не пойму, вы откуда тут все такие умные? В хорошем смысле слова. Вы какие-то академики или что? Изоморфизмы-хуизмы, я даже не знаю, что это. Вы как так прокачались-то?
Ну в основном через чтение книжек и прослушивание лекций в университетах или на ютубе, ещё статьи всякие (вводные для нубов и научные).
Ну так мейлру - борда успешных людей. Фрилансер 300к/сек на академике едет и математиком погоняет.
Я за собой заметил, что если это не применять постоянно на практике, то все благополучно забывается.
На самом деле все очень просто:
1) Читаешь пару статей в википедии, в общих чертах пытаясь ухватить их суть
2) Пишешь какую-нибудь максимально туманную и бессвязную хуйню, вставляя умные слова из пункта 1
3) Всех кто тебе возражает называешь тупым школоло и поливаешь говном
> Всех кто тебе возражает
Возражений от тебя пока не поступало, одни кукареканья со стороны параши.
Ну хуй знает. Я как-то не забываю, хотя применять вообще негде.
Ну так вообще-то мозг функционирует, он старается избавиться от бесполезной информации. Конечно, базовые принципы не забываются, особенно если ты их задрочил в свое время, но вот дай тебе сейчас работу по этой теме, и ты ничего не сможешь сделать и соснешь, т.к. практики нет и не было.
Вот шакалы, вам заняться нечем? Идите в /b/.
Мне обычно хватает усвоить основные принципы (упражнениями) и увидеть общую картину, чтобы вся последующая информация по теме ровно ложилась на каркас и не забывалась. Если знание отвечает интуитивным представлениям (нет, я не интуиционист, отъебитесь от меня), то оно как езда на велосипеде - захочешь не забудешь.
А по теме треда есть какие-нибудь курсы? Просто книжки заебывает читать.
Есть лекции Виталия Брагилевского (вводные), есть интерактивный курс Software Foundations, где ты больше сам пишешь код, чем читаешь, есть ещё Conor McBride, который записывал лекции по агде (курс называется Computer Science 400 чё-то там). Есть ещё русскоязычные лекции по HoTT некоего Исаева, но мне они показались какими-то стрёмными.
> Есть лекции Виталия Брагилевского
Про Idris? Он вообще годно излагает?
Я имел в виду не про Idris, а которые про лямбду и Coq больше. С Idris вообще не рекомендую иметь дело. Излагает он мега-годно, на русском языке наверное лучше ничего не найти.
> С Idris вообще не рекомендую иметь дело.
Почему?
Создатель языка углядел в нём какие-то фатальные недостатки и начал пилить новый, без них. Так что я бы лучше подождал, пока он его релизнет.
Это, правда, не следует понимать буквально. Просто Coq и Agda вроде как надёжнее, старше и всё такое.
>> тред про изоморфизм Карри-Говарда
Мне казалось что тема треда пруверы. Вот смотрю в название прямо сейчас и вижу - Пруверов тред #1. Может оптический обман зрения?
>Мань, это суть пруверов как явления.
Как же тогда пруверы без изоморфизмов, их не существует? Или это какие то ненастоящие, неправильные пруверы?
>То, что у тебя на это не хватает ума, как и на многое другое, само по себе доказывает только то, что ты тупень, а вовсе не то, что ты прав (как ты думаешь).
Мне хватает ума чтобы интересоваться почему это так, в отличии от баранов молящихся на этот изоморфизм как на святую троицу.
Ну таки справедливости ради ОП-пост не упоминает вообще ничего, что не относилось бы к теории типов и, соответственно, к упомянутому соответствию.
Ай да школьник совсем запутал дядю, а вот эта фраза
>То, что в другом контексте они могут быть отождествимы, я тоже писал выше.
Это все к одному посту относится? Я так понимаю твой пост с объяснениями в треде только один.
Если я прошу доказать теорему X, а в ответ вижу
> Ты тупой; А->А; Почитай хотя бы вторую часть диссертации Брауэра; уебывай аутист; С философской точки зрения; Изоморфизм Кари-Ховарда тебя накажет! Лучше съеби
Тут вообще трудно что то дельное возразить.
>Создатель языка углядел в нём какие-то фатальные недостатки и начал пилить новый, без них.
Это ты про Blodwen?
Так он экспериментирует просто, разве нет?
>>какой вычислительный смысл у терма refl
>Такой же, как у любого конструктора индуктивного типа - тривиальный.
Ну так тогда можно про любую аксиому сказать, которые вы так не любите.
- Вычислительный смысл?
- Прост)))) он тривиальный.
Вот про конструкторы было бы интересно по-подробнее. А то как-то прям очень сложно все.
А еще лучше все аксиомы/правила вывода coc и coic обозреть в одной табличке.
>все аксиомы/правила вывода coc и coic обозреть в одной табличке.
По первому в википедии же приведено, выше ссылка. По второму статья гуглится, там многа букв, разные вариации и в целом не оче понятно.
> Мне хватает ума чтобы интересоваться почему это так, в отличии от баранов молящихся на этот изоморфизм как на святую троицу.
Ну и почему это так? Как ты можешь понять, почему что-то, если ты не понимаешь даже смысла этого чего-то?
> Как же тогда пруверы без изоморфизмов, их не существует? Или это какие то ненастоящие, неправильные пруверы?
Например? Речь о пруверах на основе теорий типов.
> Вот про конструкторы было бы интересно по-подробнее. А то как-то прям очень сложно все.
> А еще лучше все аксиомы/правила вывода coc и coic обозреть в одной табличке.
Я тебе сто раз говорил, что не только правила вывода COC, но и вся полнота картины, откуда они, зачем и как из простой лямбды постепенно строится PTS, или лямбдаС или COC что то же самое, и даже как вся эта хурма соответствует логическим исчислениям по изоморфизму, которого тут боятся, все вот это и многое другое полностью отражено в кубе Барендрегта. Правила вывода СОС в одной табличке дадут очень мало, если нет понимания откуда они взялись, зачем они и как и какому логическому исчислению соответствуют и какую часть математики в них можно представить, т.е в т.ч и доказать, для чего и нужен прувер.
> - Вычислительный смысл?
> - Прост)))) он тривиальный.
Вычислительный смысл это операционная семантика. Ну или денотационная и какие там ещё есть, в зависимости от конкретной реализации конкретной теории типов.
Съеби из треда.
Да, просто экспериментирует. И Idris даже активно мейнтейнится, как я посмотрел. Теперь даже и не знаю.
Это совсем другая фраза. И что с ней не так, непонятно.
>Прост)))) он тривиальный.
У слова "тривиальны" вообще-то довольно конкретный смысл есть, его не стоит понимать как "очевидно" или вроде того. Конструкторы при вычислении просто не изменяются, в отличие от термов со сложной структурой. Почему так же нельзя сделать с аксиомой - потому что аксиомы логически содержательны, они представляют собой неделимое доказательство какого-нибудь факта, может быть довольно сложного, в отличие от индуктивных типов и их конструкторов, которые бессодержательны. Конструкторы просто задают свободную алгебру, т. е. что-то типа синтаксиса.
>А еще лучше все аксиомы/правила вывода coc и coic обозреть в одной табличке
Обозри, конечно, кто тебе мешает?
>Обозри, конечно, кто тебе мешает?
То что ее нигде нет, трололоша.
Ну сделай, если тебе так надо. Дело пяти минут.
Сделай ты, раз такой умный.
Мне нахуя? Можно же просто открыть одно в одном окошке, а второе в другом.
Вот этот терм упрощенный. Как мы видим никакой магии нет. Все доказательство расположилось в паттернах. Осталось только понять какие аксиомы за ними стоят.
Ты вообще понимаешь о чем речь? Ты не тот терминальный дебик что proof от Proof отличить не мог? Это бы многое объяснило.
Нет, я не тупой, мне показалось, что это предложение сделать таблицу с правилами вывода. А дерево тоже строить не буду, сказал же, сами блять стройте, это же вам надо, а не мне.
>У слова "тривиальны" вообще-то довольно конкретный смысл есть
С этом вообще то никто не спорит, не надо выставлять соломенных чучел себе на потеху.
>доказательство какого-нибудь факта, может быть довольно сложного
А вот тут не соглашусь. Что значит сложного/не сложного? Ты берешь некоторый факт и либо принимаешь его как аксиому либо нет.
>Конструкторы просто задают свободную алгебру, т. е. что-то типа синтаксиса.
А вот тут поподробнее если можно.
> это предложение сделать таблицу с правилами вывода
Да хотелось бы их увидеть. Там еще я облажался со ссылкой в одном месте.
>С этом вообще то никто не спорит
Ну я тогда вообще не понял, кто с чем спорит.
>Что значит сложного/не сложного
"Сложное" следует понимать как "содержательное".
>А вот тут поподробнее если можно.
Объявляя индуктивный тип с конструкторами, ты определяешь алгебру термов. Элементы алгебры - термы, построенные из конструкторов этого типа, имеющие этот самый тип. Ну и можно вывести, что разные конструкторы не равны между собой, и любые два синтаксически различных таких вот терма не приводятся вычислениями к одинаковым термам.
Все правила вывода есть в википедии и в пейпере Introduction to Calculus of Inductive Constructions, и то, и другое, уже кидали выше, ну и первые ссылке в гугле же.
>Ну и почему это так?
Блядь ты наркоман что ли? Если бы я знал, то зачем стал спрашивать на сосаче?
>если ты не понимаешь даже смысла этого чего-то?
Ну это твои личные измышления, хуй пойми на чем основанные.
>Например?
metamath, otter, HOL, TLA, тысячи всяких мелких прикладных опередений, каждый желающий может написать под себя.
>Речь о пруверах на основе теорий типов.
Эээ... почему это?
>Я тебе сто раз говорил
Первый раз вижу упоминание о кубе в треде, к контексте что он нужен чтобы понять coc. Сохацкий это ты? Ты свои разговоры с друганами в тред не проецируй.
>Ну и можно вывести, что разные конструкторы не равны между собой, и любые два синтаксически различных таких вот терма не приводятся вычислениями к одинаковым термам.
Я весь тред пытаюсь добиться объяснения КАК?
Если я тебе щас покажу пример индуктивного типа и терм, доказывающий различие двух его конструкторов, ты начнёшь ныть, чтобы я тебе строил дерево вывода и объяснял всё непонятное?
Вот этот терм . Мне нужен его вывод из правил которые якобы все в пейпере. Ты ведь его читал и понял? Тогда тебе не составит труда расписать.
Очень даже составит. Понять, какие именно правила надо применить, совершенно нетрудно, но вот унифицировать термы и контексты довольно муторно, да я ещё и не дружу с латехом, так что придётся руками рисовать. Ну его нахуй. И вообще, мне кажется, что ты пиздишь, и не пытаешься реально что-то выяснить, а просто хочешь навести здесь присутствующих сократической индукцией на какую-нибудь хуйню, чтобы показать, что они все неправы. Если ты честно и в явном виде сформулируешь свой вопрос/претензию, я может попытаюсь тебе серьёзно ответить.
Хочу понять как работает coq из первых принципов. Ничего такого в своих вопросах не вижу и задан каждый в треде раз по пять.
Но может тогда ты пояснишь мне хотя бы вот этот момент из того самого пейпера.
"logic captures" - это значит, что соответствующее утверждение выводимо как терм нужного типа. Initial algebra - это что-то похожее на свободную алгебру, там тоже просто берутся исходные операции и порождаются все возможные термы, из них составленные. Если хочешь более формально, ботай категории, ничего не поделать.
Так о какой логике идет речь?
Ну о той, которая из соответствия Карри-Говарда.
Т.е. это просто формулировка утверждения, которое мне интересует? Где тогда его доказательство?
Ой не не траль плез. Хоть в пейпере про эту парочку ни слова.
> Первый раз вижу упоминание о кубе в треде, к контексте что он нужен чтобы понять coc.
COC это правый верхний дальний угол куба Барендрегта в стандартной позиции. Stlc, т.е простая типизированная лямбда - нижний левый передний угол, расширяемый добавлением правил в трёх направлениях, которые в итоге, комбинируясь все вместе, дают COC.
> metamath, otter, HOL, TLA, тысячи всяких мелких прикладных опередений, каждый желающий может написать под себя.
Либо игрушечные, либо все те же типы, как например HOL.
> Ой не не траль плез. Хоть в пейпере про эту парочку ни слова.
Потому что у читателя предполагается понимание того, как операции с типами соответствуют логике.
Доказательство - это терм, проходящий проверку типов.
Ты понимаешь, что ты конченый?
Nyyet лалка вот тут я тебя подловил (хотя на самом деле не собирался этого делать). Мне нужно доказательство этого утверждения, утверждения в мета теории, это ни какой не терм.
Может хватит уже, ебанашка? Твое мнение услышано и нахуй послано. Хватит высирать свою имбецильность через каждый десяток постов.
Ладно, разговор с тобой окончен.
Пиздец нахуй ты это все написал? Этого вообще никто не спрашивал. Определение этого куба я и так могу глянуть в вики. И сделал это лет пять назад уже. У штудентика горит поделиться с таким трудом приобретенными знаниями с миром, что он даже не вдупляет что речь вообще о другом.
Откуда про HOL дровишки? Сам с ним не так уж близко знаком, но никаких типов там не замечал.
Как вариант, ты конечно можешь попробовать формализовать сам coq и предоставить таки нужный терм, но думаю попка треснет от такой задачи.
Ну хоть одним ебанатом в треде поменьше станет.
> Nyyet лалка вот тут я тебя подловил (хотя на самом деле не собирался этого делать). Мне нужно доказательство этого утверждения, утверждения в мета теории, это ни какой не терм.
Мамку свою с ашотом подлови. Метатеория COC это вычислимость. А любая возможная там типизация представима в самой теории, т.к кумулятивная иерархия типов.
Может хватит уже хуйню нести? Либо давай доказательство, либо лучше следуй за тем дебиком выше.
> Может хватит уже хуйню нести?
Мань, иди в б тупостью троллить, в других местах таким тралям принято ссать за шиворот. Хочешь разобраться в теме - читай, смотри, все в открытом доступе. Ума не хватает? Я ничем не помогу, да и никто не поможет.
Тупая пидорва как раз собралась в этом треде и тупит. Вы просто заебали. Если ты блядь даже не в состоянии понять вопрос, то просто так и скажи. Это не значит что тебя кто то пытаеться ололо затралить, это просто значит что ты очень тупой.
Тебе выше сто раз обьяснили, почему конструктивизм и алгоритм неформализуемы, и почему формализм это принципиально другой подход. Вся формализация конструктивизма это просто еще одно равнообьемное уточнение понятия алгоритма, коих и так дохуя. Ты же вместо того, чтобы вникнуть в тему, визжишь и кукарекаешь, называя всех тупыми, хотя по факту итт один тупень, и это ты.
Я же тебе писал что ты вообще не понимаешь что плетешь
https://en.wikipedia.org/wiki/Algorithm#Formalization
Только к моему вопросу это вообще не относиться. Я хочу увидеть конкретные аксиомы, или если ты так боишься этого слова и не понимаешь его - то правила вывода доказывающие инъективность конструкторов. И это только один вопрос, можно было бы еще много таких вопросов задать, но нет вообще никакого смысла, если в треде одни только пидорасы способные кидаться говном и диссертациями Брауэра (что примерно одно и тоже)
> Я же тебе писал что ты вообще не понимаешь что плетешь
Ты читал, что там по ссылке? Тебе, дебилу сто раз сказано, что машина Тьюринга не формализует понятие алгоритма, т.к не решает проблему останова, каким надо быть дегродом, чтобы не понимать таких вещей. Соси хуй короче, ты слишком деревянный.
>машина Тьюринга не формализует понятие алгоритма, т.к не решает проблему останова
Можешь процитировать, где на той странице такое сказано?
мимо
> Можешь процитировать, где на той странице такое сказано?
Исторический обзор, где про Entscheidungsproblem.
Пиздец ты тупой, просто пиздец.
> Пиздец ты тупой, просто пиздец.
Ты тоже сходи нахуй почитай по своей ссылке про Entscheidungsproblem, очень поучительная история про ограниченность формализма в математике.
Я про это еще в школе читал.
Давай прямую цитату подтверждающую твой бред как тебя просили. Ах да ее же там нет ты просто что-то в своем делирии додумал. О чем же тогда целый раздел в который я тебя ткнул, не удосужишься рассказать?
> О чем же тогда целый раздел в который я тебя ткнул, не удосужишься рассказать?
О машине Тьюринга, мань. Которая не решает проблему останова.
> Я про это еще в школе читал.
Если бы ещё и понял...
У меня с этим проблем нет. Вот если бы ты понимал что тебе пишут прямо сейчас прямо в этом треде было бы гораздо проще с тобой. Ждем-с.
Но ведь раздел немного по другому называется. Как же так получилось?
Я как раз этот абзац хотел скопипастить, но решил не торопить события. Давай все-таки конкретнее: процитируй конкретный текст с той страницы, где говорится, что "машина Тьюринга не формализует понятие алгоритма, т.к не решает проблему останова", пожалуйста.
(если не хочешь\не будешь этого делать, так и скажи, no big deal)
>Постишь дельные мысли, стараешься
>Аутист, ты хуйню сморозил, съеби с треда.
>Шизик засравший полтреда своим нелепым делирием
>(если не хочешь\не будешь этого делать, так и скажи, no big deal)
Заебись, программач доска для цивилизованных дискуссий. Психбольницу захватили психи.
Борда. Борда никогда не меняется.
Шизик тебя всегда победит тупо количеством текста. Отличить адекватность от шизы аудитория не может.
Ты лишний пост загринтекстил. Ты -анон? Тогда ответь, пожалуйста, на -пост (ну или на ).
Я на вопрос ответил исчерпывающе, и ты это понимаешь, дальше сам. Статью Тьюринга "on computable numbers" можешь почитать, хотя бы полное ее название. Но можешь и дальше тут клоуна корчить, мне все равно, правда.
>Ты -анон?
Нет же ох и лол
>Отличить адекватность от шизы аудитория не может
как метко
>Я на вопрос ответил исчерпывающе
У меня был не вопрос, была просьба: процитировать "машина Тьюринга не формализует понятие алгоритма, т.к не решает проблему останова" с той страницы. Хотя, вопрос тоже был: "можешь процитировать?" - подразумевает ответ да\нет. Ответь, пожалуйста, исчерпывающе на этот вопрос, если тебе не трудно.
>дельные мысли
>хуита на половину страницы
Ты хуйню сморозил, съеби с треда.
— Почему существует только то, что порождается алгоритмом?
— Потому.
— Ты ебанутый?
— На это неоднократно давался ответ.
— Ты можешь доказать формулу Гаусса?
— Твоя вера не нужна.
— Пошёл нахуй, ебанашка.
— Ты не воспринимаешь объективные аргументы.
— Какие?
— Хватит спрашивать одно и то же.
— Ты издеваешься. Ты не можешь писать это всерьёз.
— Я не виноват, что ты такой тупой.
— Потому.
— Ты ебанутый?
— На это неоднократно давался ответ.
— Ты можешь доказать формулу Гаусса?
— Твоя вера не нужна.
— Пошёл нахуй, ебанашка.
— Ты не воспринимаешь объективные аргументы.
— Какие?
— Хватит спрашивать одно и то же.
— Ты издеваешься. Ты не можешь писать это всерьёз.
— Я не виноват, что ты такой тупой.
Ты только не реви, ладно?
Ты хуйню сморозил, съеби с треда.
Конечно съебу, хуле тут еще делать? Никакого дискача тут нет и похоже не будет. Одна только интуитивная обосратка брызжет своим поносом. И еще один кокер, он вроде хотел что то разъяснить, но боится что его стралят и к тому же лениво. Все еще проигрываю с этой хуйни. Ну и пара просто дибилов подсирающих односложными высерами типа это охуенно смешно.
> вы все дураки и не лечитесь, одна я в белом пальто красивая
Валерия Ильинична, вы ж померли?..
Сколько же в тебе говнища что ты никак не просрешься окончательно, больное уебище?
Просто оставлю это здесь
https://fstar-lang.org
https://fstar-lang.org
> Просто оставлю это здесь
F* весьма каличная лямбда по сравнению с коком. Тогда уж надо было Morte для хачкиля вспоминать, там хотя бы COC.
F-залупа не нужен потому что есть Lean.
Lean еще больше не нужен потому что есть Coq.
prove me wrong
Coq не нужен, потому что есть Agda.
Agda ненужна, потому что есть ATS.
Унеси эти костыли.
ATS императивная параша же
Смогут ли анонимные наркоманы помочь с таким вопросом - кто что знает за elaborator reflection в Idris? Как я понял, эта хурма даёт возможность использовать Идрис в т.ч как прувер. В документации полтора примера, есть пейпер в тему, но я его не читал.
Опять хуйню сморозмил, съёбывай быстрее.
>даёт возможность использовать Идрис в т.ч как прувер
Его и без этой фичи можно так использовать. Но с ней наверное проще, потому что можно писать тактики.
>не читал
Смотри на приложенное изображение.
> Его и без этой фичи можно так использовать.
Да?..
Ну как бы, если есть полноценные зависимые типы, то уже можно формулировать и доказывать теоремы. Тактики и специальные интерфейсы - это вопрос удобства, а не доказательной силы. Правда, "прувер" ещё можно понимать в значении "автоматический генератор доказательств", тут да, очевидно, нужна дополнительная машинерия.
Ты дурачок, лол?
Да блять, речь о наличии какой-то автоматизации доказательства. То, что для самой возможности доказательства не нужен даже идрис, и все можно доказать на бумаге, я и так знаю. В коке есть тактики и даже язык для их написания ltac. Мне интересно, чем это можно заменить в идрисе, хотя бы как-нибудь.
>обсуждать хоть что-то серьезное на доске с дегенератами у которых в идеи-треде каждая 1.5 идея это бот в не менее дегенеративном ВКонтакте
в /math/ два с половиной шизофреника.
> в /math/ два с половиной шизофреника.
Ну так обсуждай на 8chan, Reddit, stackexchange, Сосач как интеллектуальное комьюннити давно потерян. Ты тут только деградировать будешь.
А там есть русскоязычное сообщество?
Увы, ты прав. Почему я вообще здесь сижу?
>Почему я вообще здесь сижу?
Потому что в нормальном месте твои высеры потрут и тебя отхуесосят и забанят. Можешь не благодарить.
>отхуесосят
словно что то плохое
>it
>русский язык
С таким подходом только на хабропарашу
Мдауш... хотел бы я быть таким же умным, как ты,,,
Нужно сначала выиграть в генетической лотерее, а потом постоянно работать над собой - иначе пиздец.
Давно уже пора делать учебник математики с йобами и мемасами. Но интерактивный, чтобы адаптировался под ученика с помощью слесарьплова. Дополнительно прикрутить Coq и всякие там демидовичи. Теоремы сначала будем писать в виде будапешт-тредов. Кто за?
Кроме шуток, если без блядских мемчиков и рака, то можно попробовать.
Если в более серьезном манере, то так это видится тобою? Я думаю, что оно должно использовать программированное обучение.
Я уточнил значение слова "слесарьплов" и резко передумал. Нахуй надо.
Это для красоты сказано. Суть в том, что все равно будет составляться индивидуальный план. Даже слесарьплов здесь не нужен особо.
А зачем нужен индивидуальный план?
Поясните за кок. Я правильно понимаю, что суть там в том, что сначала пишешь интересующую тебя теорему / лемму в виде правильно типизированного терма, а потом пытаешься ебать отдельные части этого терма (логические связки, кванторы, подтермы) тактиками или уже существующими или самописными теоремами / леммами до тех пор, пока изначальный терм не будет полностью доказан или наоборот, окажется, что это невозможно?
Записываешь утверждение как тип (у которго тоже есть тип, у которого есть тип... различие между типами и термами размыто) и дальше пытаешься придумать терм, имеющий в точности этот тип. Если тайпчекер подтвердил, что твой терм соответствует твоему типу, то считаешь утверждение доказанным. Сам терм можно строить из других термов, либо написать последовательность тактик, из которых этот терм сгенерируется автоматически. Можно сначала написать общую структуру терма, оставляя в нём незаполненные места, сразу проверить, не ругается ли чекер, а потом уже заполнять пропуски.
А, т.е теорема записывается в виде типизации, а тактиками, леммами итд строится терм, показывающий что тип, соответствующий теореме, обитаем. Либо получаем доказательство невозможности построения такого терма(элемента типа, соотв теореме). Ес-но, как тип так и терм может быть любой сложности и содержать в свою очередь типы и термы. Как-то так?
>теорема записывается в виде типизации
В виде типа, правильнее сказать.
>тактиками, леммами итд строится терм, показывающий что тип, соответствующий теореме, обитаем
Лемма - это разновидность утверждения, как теорема. Тактики - это термы отдельного языка тактик, на котором записываются выражения, из которых Coq строит терм. Ну и да, суть в том, чтобы продемонстрировать обитаемость типа, соответствующего утверждению, тогда можно считать утверждение доказанным.
>Либо получаем доказательство невозможности построения такого терма
Утверждение о невозможности построения терма принадлежит метатеории, в самом Coq это нельзя записать и, соответственно, доказать. Но можно сделать так: взять какое-то утверждение (тип) не просто, а с отрицанием, и предоставить соответствующий терм, если это возможно. Тогда в метатеории имеем: тип отрицания населён (продемонстрировано наличием конкретного терма), ложь невыводима в нашем исчислении (это считается уже известным фактом), но если бы исходный тип был населён, тогда можно было бы заключить ложь (доказательство от противного, позволительно в метатеории).
Coq может только поругаться, что твой терм не соответствует твоему типу. Это не значит, что доказательства нет, это значит только что твоя попытка доказательства оказалась неудачной.
>как тип так и терм может быть любой сложности и содержать в свою очередь типы и термы
Я не понял, что тут имеется в виду. Термы строятся из термов, типы строятся из типов, это такая своеобразная алгебра.
> Я не понял, что тут имеется в виду. Термы строятся из термов, типы строятся из типов, это такая своеобразная алгебра.
Терм может содержать типы в том числе, разве нет?
Терм может в лучшем случае содержать типовые аннотации. Скорее наоборот, тип может содержать термы, в этом суть зависимых типов.
> Терм может в лучшем случае содержать типовые аннотации. Скорее наоборот, тип может содержать термы, в этом суть зависимых типов.
В COC же вроде как 4 типа зависимостей: термы от термов, термы от типов, типы от термов, типы от типов. И особой разницы между типом и термом нет. Т.к. тип в свою очередь тоже элемент следующего в иерархии типа. Не?
Всё верно, вершина лямбда-куба же. Я просто не понял вопрос.
А ну признавайтесь кто обосрался? Интуитивный, твое говно?
Кто-то осваивает сразу, кому-то надо разжевать дополнительно.
Я думаю, лучший способ это организовать - это запилить много небольших глав и сопроводить их графом зависимостей, как это обычно делается в серьёзной учебной литературе. Разве что-то ещё можно сделать?
Ахахаха, лол
Я вообще взялся почитать основания треды с math/sci. Сколько же там годноты оказывается. Пол-часика чтения делают мой целый день. Не понимаю по каким неведомым причинам я решил их обходить стороной в свое время, эх бы сейчас окунуться в тот самый срач.
>Я вообще взялся почитать основания треды с math/sci
Можешь архивом скинуть?
Не понимаю твоего вопроса, вот эти треды:
https://2ch.hk/math/res/22.html
https://2ch.hk/math/res/3694.html
https://2ch.hk/math/res/17772.html
https://2ch.hk/math/res/21361.html
https://2ch.hk/math/res/25624.html
https://2ch.hk/math/res/40955.html
бонус:
https://2ch.hk/sci/arch/2017-01-27/res/391083.html
Наверное еще можно накопать при желании.
%%Ты же в курсе, что ты кидаешь посты залетных шкальников, которые не участвовали непосредственно в самих дискуссиях на тему сабжа, да?5%
Лол, кто-то ещё помнит те срачи. До сих пор непонятно, с чего все так толпой накинулись мне "доказывать" "неправильность" интуиционизма. Как будто это вообще можно доказать.
Найс аутотренинг, конструшок.
Вот это я понимаю настоящая вера. Надеюсь я не оскорбил твои чувства, а то сам понимаешь не хотелось бы под статью.
Ты же даже не знаешь что такое аутотренинг.
мимо
Ну давай рассказывай чего я там не знаю, или только в лужу пердеть горазд?
Лол, ну я же говорил, что это школьник.
Ясно, конструшок продолжает прямую трансляцию из манямира, подшивая порвавшийся анал.
Мань, это не мои посты даже. Пиздец, злокачественная у вас батруха, батенька, два года не проходит. Везде меня видишь, да? Под кроватью посмотри, а то вылезу ночью и...
> мань
Можете доказать населённость этого типа?
орнул немношк
Тотали релейтед.
Поехавший, ты двум разным анонам ответил. Алсо, тебе везде конструктивисты мерещатся?
Питухи-опровергатели-интуционизма и сюда залезли? Выпиздовать их из треда!
> > мань
> Можете доказать населённость этого типа?
Да запросто. Больше половины дегенератов из вышеупомянутых тредов про конструктивизм - население типа манек. Даже сюда один шизик:маня протек.
Конструктух, это ты писал? Я просто охуеваю как в одном человеке может быть столько ебанутости. Но с другой стороны - то что могут существовать два человека с таким же фанатичным дрочем на всю эту Брауэрскую хуиту - это что то еще более невероятное.
Ты можешь обсудить его личность в /soc/.
Разумнее всего отловить конструха в его естественной среде обитания, вместе с его братьями по разуму.
P.S. Не подскажешь раздел где ебут твою мамку?
Т.е ты хочешь сказать, что коллекционировать все мои посты с 2016 года и трясти ими по всему мейлру с подгоревшей попой - это поведение здорового человека?
Съеби отсюда, а то тебя конструктивисты преследуют.
Бамбпну говнотред напоследок остатками тонкого математического юмора и деконструкцией конструха.
>деконструкцией конструха.
Ты пошутил неудачно или и вправду настолько тупой, что веришь в принадлежность поста со второго пика конструктивисту?
Я, например, уже окончательно запутался, где кто и за что топит. Вы бы хоть перестали сраться на день и запилили бы FAQ с кратким изложением позиций обоих сторон.
Зачем? Там параллельно с этим тупым траленком шла интересная содержательная дискуссия деда и конструктивиста. Если кто-то не может, так сказать, отделить зерна от плевел, то ему и никакие факи не помогут. Имеющий уши да услышит.
Почему деды против конструктивизма?
Там - это где?
>деда
Валькин Деда? Что за магическая такая способность определять возраст на анонимных бордах?
Конструктивист что, сюда утёк? Лол.
проездом из math
>>деда
Это мемас, ты не шаришь просто.
Мама я в телевизоре! И что, давно он тут питается?
40472-кун
Потому что первым делом, первым делом матанализ...
Не, сюда утек шизик, который за ним носится.
>, сюда утек шизик, который за ним носится.
Да ладно, перестань, я милого узнаю по походке.
Я про -пост говорил, ты же на него отвечал.
Так когда собственно было отмечено первое появление конструктуха - в math тредах саентача или вообще еще на том самом?
Это случайно не посты одного человека? Не хотел отвечать, но ты же просто клинический тупица. Тебе нужно в школу коррекции ходить и учиться там шнурки завязывать и - не знаю там - лопатой махать и прочие полезности. Ты блядь терминально тупой хуесос. Нахуй ты тут свое охуительно важное мнение выставляешь? Всем поебать. Нормальные люди в лучшем случае только немножко поохуевают какой же ты тупой. Даже хуже конструктуха, чесслово.
Нормально шизика разорвало.
Первое, емнип.
Скоро дойдёте до треда в fag.
Квадратная доска 6x6 заполнена костяшками домино 1x2. Докажите, что можно провести вертикальный или горизонтальный разрез этой доски, не пересекающий ни одной из костяшек домино.
Как на коке это доказать?
Сперва бы понять, как условие записать формально, хотя бы даже на множествах. Я вообще не понял, что имеется в виду.
Найс подрыв, лайк.
Кстати да, давайте уже тред имени меня в фаг. А то неорганизованно бегаете по всему мейлру подгоревшими попами трясете, народ доебываете на ровном месте. Как-то локализовать надо этот цирк, просто потеряться вы не хотите почему-то.
>Кстати да, давайте уже тред имени меня в фаг. А то неорганизованно бегаете по всему мейлру подгоревшими попами трясете, народ доебываете на ровном месте. Как-то локализовать надо этот цирк, просто потеряться вы не хотите почему-то.
Пожалуйста, СЪЕБИТЕ УЖЕ НАХУЙ обратно в свой /ga/ /math/, вы такие душные кретины, что я чуть не заплакал.
Я считаю что личность такого масштаба просто обязана завести трипкод и аватарку. Ну просто чтобы всем было ясно с кем они имеют дело.
Можно было бы принять за праведное негодование, если бы тред был полон годного обсуждения самых разных вопросов. Но только это не так. А ты взбесившаяся манька которой просто хочется чтобы на нее хоть кто-нибудь обратил внимания. Вскройся нахуй.
Как тебе у нас дома срать так это норма, а как мы стали тем же заниматься у тебя припекает, да? Ладно, ладно, погромируй себе на здоровье, ухожу.
Хуя разворотило.
Лайк!
Я в math не лезу ващето. Там все равно пусто и уныло.
Тут не особо лучше, хипстеры да си-деды.
Ну и что теперь, это повод плодить помойку?
Да.
Замечалось ли повышение успеваемости у учащихся использующих конструктивный подход вместо теоретико-множественного?
У меня было наоборот, успеваемость ниже. Но зато я начал понимать математику (до этого не понимал вообще, абсолютно ничего). Это, конечно, связано в первую очередь не с самим конструктивизмом, а с тем, как он подаётся.
Интересно.
Вот двачую.
Во-первых ты не смешивай "конструктивный подход" и формальные методы, это одно и то же только в безумных фантазиях конструктушка и друзей. (Как же вы заебали)
Я уже давно отучился, но когда открыл для себя курс software foundations и формальные методы с петухом, на меня это произвело чрезвычайное впечатления. Сложно его точно описать, но можно сравнить с тем как когда в школе нам рассказали об эпсилон формализме для бесконечно малых. Понятие бесконечно малого/формального доказательства и раньше вроде бы казалось понятным, но чем то несколько эфемерным, неуловимым - и вот наконец можно увидеть что оно представляет из себя на самом деле во всей своей красоте.
Теперь я знаю что такие вещи как "вроде бы кажется достаточно убедительным" или выблевы гуманитарного скама "у каждого своя правда" я всегда могу если захочу разогнать светом формальных методов. Слава формальным методам, слава петуху!
Да, sf очень хороший курс. Я бы его включил в программу для всех, кто пользуется формальными методами, если бы он был на базе устоявшегося дефолтного прувера со всеми обвесами для индустрии
SF дико тормозной и туповатый,
лучше уж Coq'Art + Certified Programming with Dependent Types
Тред, не умирай.
Какое же говно у тебя в голове, господи...
Пацаны, ну накидайте карту, как хотя бы понять, что это такое, и если все круто с чего начинать вкатываться.
В шапке же есть ссылки.
HoTT там же математика, как ее понять то без математического бэкграунда? Cubical Type Theory, а это что такое? В каком порядке читать? Параллельно с чем?
Как соотносятся теория категорий с этим всем? Теория зависимых типов? Я уже несколько дней тыкаюсь, в систему ничего у меня в голове не складывается, куда приложиться.
Не, про хотт не надо читать, и про кубик тоже. Надо перейти по ссылкам на конкретные ассистанты и читать про их функции.
Пруф-ассистанты своим названием говорят за себя: они позволяют строить (и проверять) математические доказательства с помощью компьютера. Многие из современных (все из перечисленных в шапке) ассистантов основаны на теории зависимых типов. Тезис, связывающий математические утверждения и доказательства с типами и термами из теории типов называется "соответствие Карри-Говарда". Теория категорий тут особо ни при чём, но она может выступать как инструмент для исследования семантики различных теорий типов или как язык для описания математических сущностей (особенно в алгебраической геометрии, из которой произрастает хотт).
Спасибо, внес какую-то ясность.
Я имею представление об идеи HoTT, мне бы хотелось и ее понять. Для этого, как я понимаю, мне все равно нужно изучить то, что ты написал.
Если тебе интересен хотт, читай хоттбук сразу. Технически, он самодостаточен, но для облегчения восприятия материала могут понадобиться дополнительные источники.
Спасибо большое, анон!
CTT — это всего лишь реализация HoTT, не теряющая вычислительный смысл.
https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/
>This is done such that these principles have computational content and in particular that we can transport structures between equivalent types and that these transports compute. This is different from when one postulates the univalence axiom in a proof assistant like Coq or Agda. If one just adds an axiom there is no way for Coq or Agda to know how it should compute and one looses the good computational properties of type theory. In particular canonicity no longer holds and one can produce terms that are stuck (e.g. booleans that are neither true nor false but don’t reduce further). In other words this is like having a programming language in which one doesn’t know how to run the programs. So cubicaltt provides an operational semantics for Homotopy Type Theory and Univalent Foundations by giving a computational justification for the univalence axiom and (some) higher inductive types.
Абу — пидор.
Кстати, там случайно не появился какой-нибудь новый материал, кроме тех лекций на гитхабе?
Отвечу себе сам: у RedPRL есть какая-никакая документация, можно почитать её.
Coq:
https://coq.inria.fr/
Lean:
https://leanprover.github.io/
Agda:
https://github.com/agda/agda
Idris:
https://www.idris-lang.org/
HoTT:
https://github.com/HoTT/HoTT
https://github.com/HoTT/HoTT-Agda
https://github.com/gebner/hott3
Cubical type theory:
https://github.com/mortberg/cubicaltt
https://github.com/mortberg/yacctt
https://github.com/RedPRL/sml-redprl
Ну и agda --cubical