Школьникам это нужно в учёбе?

>>1224474 (OP)
>Coq.
Suq.

Ну давай рассказывай, как ты хлебаешь борщ.

>>1224474 (OP)
На дваче есть те, кто шарят в таком? И их даже больше 2?

>>1224747

На нульчане точно были.

>>1224747
Да полистал книжечку Type-Driven Development with Idris и уже можешь унижать тех, кто не знает.

>>1224474 (OP)
УЕБЫВАЙТЕ В /MATH

>>1224747
А тут только динамические петухи сидеть должны?

>>1224807
Математика это пучки (гомологии для алгебры и топологии для геометрии), а не доказательства теорем.

>>1230188
Пифагоровы штаны на все стороны равны. Зачем и почему? Так надо.

Если вы поняли эту шутку, значит у вас нет друзей.

Кок на шиндовс бесполезен, к нему все ставится через ОРАМ, а на винде он так работает, что я ебал. Без линукса туда и лезть не стоит, но это единственный прувер, стоящий внимания. Идрис - очень крутая вещь, вот этот метод постепенного построения с нихуя программы любой сложности "type - define - refine", "дыры", которые сами заполняются при наличии правильного контекста, мне кажется, при должном уровне аутизма на нем можно сделать вообще все что угодно, ЯП богов. Еще и генерация C, JS, NodeJS искаропки. Алсо почти не требует познаний в теории типов, как тот же кок. При этом 100% работоспособности на любой ОС, в Атоме все охуенно работает. Очень недооцененный проект на самом деле, аналогов не имеющий как любят говорить наши пропагандоны. Но как прувер он никакой, такой системы тактик как в коке, в нем не будет никогда. Новомодные пруверы на основе вычислительной теории типов (RedPRL, cubicaltt итд) экспериментальные, там сама теория еще сыровата, но вкатываться можно уже начинать.

>>1230317
>шиндовс бесполезен
Починил, брат.

Почему не сделали какого-то Демидовича в онлайн-версии? А не писать на бумаге...

>>1230663

Нормальный энтри-левел задачник.
По сравнению с конспектом по спасению долбоёбов от бутылки в армейке (Письменный) - так вообще отличный.

>>1224474 (OP)
>HoTT
>Cubical type theory
Лень читать все эти пейперы, поясните по хардкору чего там есть интересного?

>>1230880
Пытаются рефакторить основы математики.

>>1231184
Ну теперь-то, когда за это взялись программисты, они все сделают как надо.

>>1231201
Это Брауэр-то программист?

>>1231201
Я смогу задачки решать удобней?

>>1231264
Не знаю, наверное. Восторгаются этим делом исключительно программисты, которым нравится думать, что они что-то понимают в основаниях.

>>1230663
https://www.youtube.com/watch?v=MI83NiZbsFw

>>1231298
> Восторгаются этим делом исключительно программисты,
Пиздежь, ни Мартин-Леф ни Воеводский, ни Барендрегт не программисты.
> которым нравится думать, что они что-то понимают в основаниях.
Только они и понимают. Вместо того чтобы аутизм аутировать, делают настоящую, вычислимую математику а не просто значки рисуют.

>>1231298
Ты, анон, вообще понятия не имеешь, о чем говоришь. Придумал себе там что-то... не делай так больше, пожалуйста!

>>1231806
Ладно.

>>1224474 (OP)
Решительно подписался.

>>1224807
Нам там скажут "уёбывайте в /pr/"

Вопрос к пользователям Coq. Что вы находите более удобным/естественным/практичным: подход Адама Чипалы с опорой на тактики и автоматизацию или подход, предложенный проектом math-comp?

>>1224474 (OP)
Хочется научиться писать на кубике, но как-то тяжело даётся. Лекции из мортберговской репы понятны ровно до того момента, как начинают использовать композицию с более чем одним интервалом. Чего-то не хватает для понимания сути. HoTT-book не читал дальше первой главы, стоит сначала почитать?

>>1232077
-> /math

В петухе был особый режим, кажется командой proof он запускался, похожий на ssreflect немного. Так вот его выпилили. Может кто нибудь в курсе как они пришли к этому? Можно ли найти где-нибудь обсуждение этого шага? Я только хотел его освоить и внезапно его пидорнули, как-будто его и не было никогда. А что если кто-нибудь доказал с этим режимом свое охуительное доказательство на сотни тысяч строк. Может они еще чего нибудь выкинут из языка?

>>1232101
>Best guess for this image: martin lof type theory

>>1232103
> В петухе был особый режим, кажется командой proof он запускался,
Че? Это ж обозначение начала доказательства? После этой команды нужно тактики подбирать итд, сама по себе эта команда ничего не доказывала.

>>1232071
Ты уловил шутку, спасибо.

>>1232176
>сама по себе эта команда ничего не доказывала
Никто этого и не утверждал. Вот пример
https://stackoverflow.com/questions/40723002/coqs-mathematical-proof-language-rewriting-in-if-condition

>>1224474 (OP)
Ну собственно двухминутный гуглинг немедленно приводит к следующему: https://www-verimag.imag.fr/~corbinea/mmode.en.html

>>1232390
Похоже, это давно заброшенная попытка использовать вместо Ltac декларативный язык, похожий на то, что есть в Mizar.

>>1232378
Но оно работает так же как и раньше.

>>1232442
Это где и как оно работает? У меня вот в свежем коке: Error: The reference proof was not found in the current environment.

>>1232482
> Нахуя писать хуйню?
Себя спроси. Proof с большой буковы пишеццо.

>>1232676
Вот у меня даже в голове не укладывается, как можно быть таким дебилом, как ты. Ты бы хоть сначала перешёл по ссылкам выше, посмотрел, о чём вообще речь.

>>1232693
Мань, ты писать научись сначала.

>>1232378
>>1232390

>>1232729
Ты что-то не так делаешь, а именно, пишешь proof с большой буквы, и у тебя включается обычный интерактивный режим с Ltac'ом. А речь про совсем другое, см. по ссылкам выше.

>>1232747
Мне кажется, тут речь об удалении нерелевантной документации, а не об удалении собственно этого режима.

>>1232708
Я даже больше скажу - раньше в документации была целая глава
> Chapter 11 The Mathematical Proof Language
Но теперь она тю-тю вместе с режимом.

А ведь раньше раздел был с компьютер саенсом. Но похоже что то не взлетел.

Идрис разве не умер уже? Чё вы на нём пишете?

>>1232870
ДинамическиеСтатические опердени.

>>1232834
Ну правда, спроси у них самих на гитхабе\реддите\ирц, чего гадать-то.

>>1232865
Матх жи есть.

>>1232876
>Ну правда, спроси у них самих на гитхабе\реддите\ирц, чего гадать-то.
Пидора ответ.

>>1232891
Нет!

>>1232870
Примеры из книги Type-Driven Development with Idris

>>1232989
Хорош

Парни, это все очень весело, сам обожаю угорать по таким темам. Но можно ли зарабатывать этим деньги не в науке?

>>1233310
А в науке можно, лол? Этим 3.5 человека в мире занимаются, авторы упомянутых в оппосте программ.

>>1233310
maxim.livejournal.com - этот чувак зарабатывает.

>>1232077
По кубику ты можешь ещё только саму работу по CTT посмотреть. Больше ничего нет, увы.

А конкатенативные языки программирования завезли?

>>1233366
Ты про типы в конкатенативных языках?

>>1233409
Про типы и все остальное.

>>1233352
Он зарабатыфвает не этим, а функциональным программированием, причем даже не им, а продуктом, который он написал на эрланге много лет назад.

>>1233366
А зачем?

А в metamath кто-нибудь пробовал вкатиться?

>>1233447
Про типы нагуглилось только это.
http://www.codecommit.com/blog/cat/the-joy-of-concatenative-languages-part-3

Не знаю, как в такую концепцию вписать DT.

>>1233577
Я свой аналог их базовой системы делал. У них уж очень олдово, референс реализация даже не оупенсорс. Основы описаны довольно мутно, без четкой мотивации принятых решений. Все это недостатки хобби-проекта, по нему вышла вроде всего одна статья в каком-то маленьком журнале. У автора не было стимула нормально делать, все сделано для самого себя. Похоже, мало кому в науке сейчас интересны такие вещи.

>>1233626
А нет, наврал, исходники есть. Странно, мне казалось раньше их не было. Может, перепутал с чем-то другим.

>>1230551
>Демидовича
Ебануться, 18 лет прошло с того года, как я универ закончил. У меня уж и хуй стоит от силы раз в неделю, и давление выросло, и зрение упало, а студентов до сих пор ебут Демдовичем.

>>1233814
Так ведь картофан и водочка с тех пор тоже почти не изменились.

>>1233352
https://www.youtube.com/watch?v=diAccbUNoI8

>>1233919
Прикольно он заливает как некий опердень на эрланге позволил ему забыть о тяготах бытия и выйти на пенсию. Что то уровня работаю на форексе получаю сто тыщь в секунду. Наверняка либо жена его содержит, либо - еще вероятнее - сданная в аренду квартира от бабушки. Короче, не просто так даже поговорка такая есть - пиздит как хохол.

>>1234177
Про опердень на эрланге - это древняя паста с нульчана.
Опердень там в женском роде и во множественном числе, лол.
Опердень - операционный день, это из банковского сленга.

Видео не смотрел, потом гляну.

>>1233919
1) теория типов - еще тот ФАД, можно прекрасно доказывать теоремки (на конпунктере) и верифицировать что нужно без нее. Даже не думайте спиздануть про Кари-Ховарда.
2) интересно где бы он расположил линейные типы и что там еще придумали новенького (рефайнменты? gradual typing?) на этом своем кубе.
3) проблема написать доказательство из учебника по математике не в том что не придумали еще такой распиздатой теории типов, а в том что привычную математическую нотацию хуй запихнешь в компьютер, все получается очень неудобно и вырвиглазно; разве только идейным лисперам норм, они просто любят жрать говно.
PS на каком сайте посмотреть его списочек с МакЛейнами и прочими пацанами?

>>1234230
Двачую. Вон в metamath не только без типов обходятся на нижнем уровне, но и вообще практически безо всего.

>>1234195
>древняя паста с нульчана
http://erlang-mnesia-video.ru/

>>1234230
Аутист, ты хуйню сморозил, съеби с треда.

>>1234297
Что это у нас тут за животное подорвалось?

Распетляйте за ats lang, кто-то использовал? Как оно, говорят можно даже дрова на нем делать?

>>1234230
>лисперы
>математическая нотация
Анон, как бы тебе сказать... ты долбоеб, вот.

>на этом своем кубе
>своем
Съеби с треда.

>>1234377
>>лисперы
>>математическая нотация
>Анон, как бы тебе сказать... ты долбоеб, вот.
Попробуй высрать хоть пол-мысли для начала.
>>на этом своем кубе
>>своем
>Съеби с треда.
Говна вьеби, чмо тупое.

>>1234370
AuTiSm.

>>1234230
> теория типов - еще тот ФАД, можно прекрасно доказывать теоремки (на конпунктере) и верифицировать что нужно без нее. Даже не думайте спиздануть про Кари-Ховарда.
Теория типов - это один из вариантов оснований, поэтому и используется в пруверах. Теоретически можно использовать любые другие основания, хоть ZFC, но они дырявые по сравнению с конструктивными типами.

ок

>>1234332
Ты действительно считаешь, что тот мелкобуквенный дебил сказал что-то по делу?

>>1234389
Тебе всё по делу сказали: съеби.

>>1234504
>Тебе всё по делу сказали: съеби.
Попробуй просраться еще чуть-чуть
>>1234471
Как будто рядовые доказывальщики (усирающиеся в треде) вообще хоть примерно представляют как выглядят аксиомы их петуха.

>>1234617
>аксиомы их петуха
Их нет.

>>1234625
То-то же!

>>1234639
Ну охуеть теперь.

>>1234617
> Как будто рядовые доказывальщики (усирающиеся в треде) вообще хоть примерно представляют как выглядят аксиомы их петуха.
А что там представлять? Calculus of inductive construction никто не засекречивал.

>>1234749
Где же можно ознакомиться с аксиомами этой теории? Кстати, вопрос на вскидку - сколько их?

>>1234841
Почему ты разговариваешь, как аспирант со студентом на экзамене? Если хочешь что-то донести, говори прямо, как есть. Правду-матку руби с плеча!

>>1234841
> Где же можно ознакомиться с аксиомами этой теории? Кстати, вопрос на вскидку - сколько их?
Но там не аксиомы, а правила вычисления. Аксиома в теории типов это правило без посылок, в нём только заключение. Т.е это нечто такое, что не следует из чего-то, а задается априори.

>>1234861
Лол, ну ладно, смотри тогда.
Первым делом начинающий coq'ер узнает определение натурального числа. Между тем есть такая аксиоматика Пеано. Там несколько аксиом, например постулируется функция S и то что эта функция инъективна. Я особо над всем этим не задумывался, но как то наткнулся на тот факт что "оказывается" конструкторы в функциональных языках тоже инъективны. Что немного забавно если подумать, что в обычных языках типа java такого свойства у них нет. Таким образом у нас оказывается есть аксиома, которая явно нигде не прописана, но считается общеизвестной. Или что тип можно создать только его конструкторами, или что конструкторы не могут "пересекаться". Может еще есть такие над которыми я бы даже никогда не задумался? Поэтому и хотелось бы получить их полный список.

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

>>1234915
>оказывается есть аксиома, которая явно нигде не прописана
Нет, ну если не читать ни документации, ни пейперов по сабжу, и вообще не доставать голову из жопы, то конечно кажется, что нигде ничего не написано. А для желающих есть аж первая ссылка в гугле, ну да чё я распинаюсь.

>>1234915
>в обычных языках типа java такого свойства у них нет
Это с каких пор в Java завезли индуктивные типы вместе с их конструкторами?

>>1234935
Что же там за ссылочка интересно?

>>1234956
https://hal.inria.fr/hal-01094195/document
И в добавок к этому ещё актуальная документация на сайте coq.inria.fr

>>1234957
Где там конкретно про инъективность?

>>1234971
Давай тогда доказательство что можно и аксиомы которые оно использует.

Сложные значки какие-то

>>1234974
>Как будто рядовые доказывальщики (усирающиеся в треде) вообще хоть примерно представляют как выглядят аксиомы их петуха.
>Про какие аксиомы ты говоришь, я так и не понял.
ЧТД

>>1234983
Я тебе уже говорил, что там нет аксиом, сука. Их просто нет. Синтаксис и правила вывода, больше ничего нет, вообще. Ни одной аксиомы.

>>1234980
https://www.youtube.com/watch?v=XMBXVLT50vw

>>1234980
Лучше бы попытался терм упростить, чтоб людей не пугать.

>>1234993
Ничего страшного в этом терме нет, если знаешь язык. А если не знаешь, то упрощение не поможет. И вообще, захуй читать термы, если они они автоматически генерируются и автоматически типизируются?

>>1234985
Но если аксиом нет, то значит мы ничего в итоге не доказали.

>>1235009
Да съеби ты уже, клоун.

>>1235009
Аксиомы нинужны.

>>1235010
Ой ну все петух совсем порвался.
>>1235016
Математики с тобой не согласятся.

>>1234971
Буду весьма благодарен, если кто-нибудь (из еще не подорвавшихся) объяснит мне о какой logic идет речь и каким образом она captures то что там дальше написано

Алсо хотел подсмотреть термин initial algebra в вики
>an initial algebra is an initial object in the category of F-algebras for a given endofunctor F
А ну заебись, теперь то все встало на свои места.

>>1235113
>слабо представляешь
Есть такое, тут спорить не буду.
>Откуда оно, зачем и почему не основано на аксиоматике
Я думал там просто достаточно выкинуть usual suspects из аксиом - двойное отрицание и аксиому выбора - и внезапно получается конструктивизм - на оставшихся аксиомах.
>что доказал ещё Тьюринг
Как же он это доказал без аксиом та. Но если серьезно, распиши эту мысль если можно.

>>1235113
Еще у меня закрадываются подозрения, что ты возводишь fringe или просто модные идеи в разряд абсолюта, примерно как это делает Сохацкий мимоходом с улыбочкой разъясняя щеглам что доказывать теоремы без новомодной системы типов ну никак не получится (это не правда). Брауэр вроде вообще в какую-то эзотерическую хуиту верил и его вообще никто в серьез не воспринимал в свое время.

>>1235117
> Как же он это доказал без аксиом та. Но если серьезно, распиши эту мысль если можно.
Я ж говорю, в конструктивизме главное - построимость объекта, вычислимость терма. Т.е алгоритмическая разрешимость задачи такого построения. И вот, внезапно, не все вычислимо, есть алгоритмически неразрешимые задачи, то же исключенное третье в общем виде, т.е именно в виде аксиомы. Получается, что неконструктивная математика такие дыры просто затыкает невычислимыми аксиомами. Например, проблему останова можно заткнуть исключенным третьим, ну или остановится или нет))) Но с конструктивной точки зрения это манядоказательство уровня /б. Поэтому можно говорить об уточнении понятия алгоритма, а не о его формализации, такими уточнениями являются машина Тьюринга, нормальные алгорифмы Маркова, лямбда исчисление Чёрча итд. Причём, все они равнообьемны. И вместо аксиом там правила вычисления, которые неаксиоматизируемы, или что то же самое, в теории типов не любой тип обитаем.

>>1235125
Ты говоришь много воды, но по-моему ты не знаешь элементарных основ. Тот анон совершенно прав - без аксиом тебе не к чему применять правила вывода, и ты можешь только полюбоваться на них. Вот тут, например: https://en.wikipedia.org/wiki/Calculus_of_constructions роль аксиомы играет правило вывода 1 (без предпосылок).

>>1235137
> Вот тут, например: https://en.wikipedia.org/wiki/Calculus_of_constructions роль аксиомы играет правило вывода 1 (без предпосылок).
Во-первых, чуть выше я об этом и говорил, что аксиома в теории типов это правило вывода без посылок с заключением. Во-вторых, в правиле 1 по твоей ссылке заключение под чертой начинается с буквы Г, обозначающей контекст, т.е уже имеющуюся типизацию в виде списка гипотетических суждений (абзац Judgements сразу перед правилами). В разных лямбда исчислениях допустимая типизация так же разная (добавляются возможные варианты построения допустимых термов). Почему это нельзя считать аксиоматизацией, я выше рассказал - эти правила не гарантируют априори обитаемость любого типа, построенного с их помощью или что то же самое, не дают решения проблемы останова машины Тьюринга, или опять же, что то же самое, не формализуют конструктивную логику. Правила это уточнение понятия алгоритма, а не его формализация. Поэтому их основа это вычисление (которое возможно не во всех случаях), а не аксиоматика, охватывающая все возможные варианты.

>>1235128
Скажите, откуда цитаты?

>>1235009
Клован, съебись.

>>1235115
>ничо не понятно
>энти ваши котегории
>оправдывайтесь

>>1235115
>из еще не подорвавшихся
Ты в тред пришёл и хуйню несёшь.
Ты тему не осилил, зато хуйню молотить горазд.
Съеби, животное.

>>1235137
Я тебе больше скажу, в CiC даже не одна такая "аксиома", а целое счётное множество. Только они описывают (населяют) всего лишь иерархию универсумов, а логического содержания в них нет, т. е. из них ничего кроме них же самих не следует, и доказывать содержательные утверждения можно без них.

>>1235147
>эти правила не гарантируют априори обитаемость любого типа, построенного с их помощью
Это можно как-нибудь прояснить?

>>1235157
>доказывать содержательные утверждения можно без них
Не понимаю. Как доказывать без этого правила? У тебя же доказательство никогда не закончится (если ты от утверждения идешь). Мы или разную терминологию используем (ты под доказательством подразумеваешь просто написание терма?), или ты подразумеваешь какой-то иной принцип доказательства.

>>1235168
>ты под доказательством подразумеваешь просто написание терма?
Ну да, доказательство - это терм, для которого можно вывести тип. Ты говоришь, что если убрать правила вывода без посылок, то не получится построить ни одного конечного дерева вывода, потому что в дереве вывода любое суждение должно быть обоснованно применением правила. Но это не так. В конкретных ситуациях бывает, что применение правила с нетривиальным предположением обосновывается без других правил. Пример: в контексте (T : Type, x : T) можно заключить (x : T), и в силу этого факта можно применить какое-нибудь правило вывода с соответствующей посылкой. Например, можно получить, что терм (fun (T : Type) (x : T) => x) имеет тип в пустом контексте, а это уже содержательное доказательство.

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

>>1235168
> (ты под доказательством подразумеваешь просто написание терма?)
Да, в конструктивных теориях типов доказуемо только то, что выводимо, т.е сам терм (а не какая-то оторванная от вычисления аксиоматика) является доказательством себя.
>>1235165
> Это можно как-нибудь прояснить?
Правила задают правильность типизации. В них можно выразить, т.е построить только то, что в них выводимо/построимо. Если бы можно было построить всё, то эти правила решали бы и проблему останова машины Тьюринга и любую другую алгоритмически неразрешимую задачу. А так как это невычислимая/непостроимая задача, то она неразрешима в теориях типов. В чем и разница от формализма, там главное непротиворечивая аксиоматика, а в конструктивизме вычислимость. Тут уже встаёт вопрос, что есть существование математического объекта. В формализме это непротиворечивость в системе аксиом, в конструктивизме - построимость/вычислимость терма.

>>1235185
А, типа, не любое истинное утверждение можно доказать вычислением?

>>1235219
> А, типа, не любое истинное утверждение можно доказать вычислением?
В данном случае истинное = вычислимое. С конструктивной точки зрения вне вычислимости/построимости нет никакой истины, например, аксиом, оторванных от конкретного построения.

>>1235263
Ну да, понятно.

Поясните быдлу за линейную логику

>>1235180
>такое уже пытаются делать
Попо дробнее? Может и в школах уже думают конструктивизм распостранять?

>>1235479
Клевый мемас а то надоело букавы читат
ь

>>1235470
Конструктивизм там нахуй никому не нужен, очевидно же. edukera.com есть, либа для кока, формализирующая евклидову геометрию, всякое такое.

>>1224474 (OP)
Меня всегда интересовало, а вакансии по теме треда есть? Кто это использует и где?

>>1235611
Да есть конечно. Правда, там без учёной степени не берут обычно, потому что оно всё при университетах, ну и это чисто рисёрч, не индустриальное.

>>1235611
>вакансии по теме треда есть?
http://groupoid.space/
но тебя не возьмут
и меня тоже

>>1235624
>это чисто рисёрч, не индустриальное
Почему в индустрии не используют? Слишкам сложна? Какие причины, вообще? Или там недостатки какие-то серьезные, что проще на джаве команде макак нахуярить по-быстрому?

>>1235720
Ну всего понемногу. Инструменты пока ещё далеки от совершенства, теория местами не такая гладкая, как хотелось бы, экосистема не в очень адекватном состоянии. И конечно, верифицированное ПО и алгоритмы - нишевая штука, потому что далеко не везде разумно вкладываться в формальное доказательство, когда вроде и так нормально и тесты чекаются. Я думаю, это всё временно, и однажды проблемы решатся, и верифицировать ПО будет выгоднее, чем не, но сколько ждать - непонятно.

>>1235720
Верифицированный код нужен (required) очень мало где, всякое по для самолетов да рентгены

>>1235720
> Почему в индустрии не используют? Слишкам сложна?
Сложна конечно. Одно дело быдлоджава, которой за месяц можно любого дегрода обучить, другое - язык, в котором теорию типов нужно знать даже для того, чтобы просто читать код, а уж писать что-то осмысленное, это минимум профильная аспирантура.

>>1235740
То есть, в Airbus и Boeing такие вакансии есть?

>>1235742
>теорию типов
Литературу/курсы не посоветуешь?

>>1235128
>понятие условного рефлекса
Типа стукнул математика по левой коленке - дернулась нога, стукнул по правой - он доказал теорему Ферма. Очень смешно. В любом случае это только твои домыслы.
Нашел перевод одной его статьи. Там в предисловии говорится что ее не хотели принимать в философский журнал, т.к. никто не мог понять что он там за хуергу написал. Хотя казалось бы писать абсолютно лишенную смысла ахинею это modus operandi всех философов.
Еще пред тем как отбросить принцип исключения третьего он его не правильно понял как -A -> -A. У меня вообще глаза округлились от этой хуйни. Но ничего, хуйня, с каждым бывает.
>>1235147
>контекст
Контекст есть и в секвент калкулусе. Там что тоже аксиом нет?
>эти правила не гарантируют априори обитаемость любого типа, построенного с их помощью
Я так уловил что ты предлагаешь что необходимо выполнять вычисления построенного терма чтобы в убедиться в том что они будут конечны. Я слышал в typetheorypodcast с Weirich что существуют формальные системы с теорией типов где этот так. Мне это запомнилось потому что произвело даже некоторое впечатление. Но только к петуху это совсем не относится, т.к. в нем никто в здравом уме не производит вычисления над термами доказательств.
>>1235150
Если теория типов это фад, то теория категорий - это рак ебаный с метастазами. Конечно ни один вменяемый человек не полезет разбираться в их бесполезной абстрактной хуете, поэтому они срут ей в каждой статье на википедии. 1+1? Ну это терминальный объект симплициального эндофунктора...
Хорошо что хоть категориальные основания так и не набрали оборотов, а то какой-нибудь дурачок в этом треде мне бы уже усираясь доказывал что ну никак не возможно построить основания математики без категорий.
>>1235185
>Если бы можно было построить всё, то эти правила решали бы и проблему останова машины Тьюринга и любую другую алгоритмически неразрешимую задачу.
Ты повторяешь этот тезис снова и снова как мантру. Только от этого он не становится более правдой. Или даже более убедительным. Разве что для дурачков что заглядывают в тред чтобы просраться. Мне кажется что ты путаешь что выводимо, что не выводимо и какие из всего этого следствия. Но может быть в этом и есть что то. Но...
Есть такая теорема Геделя. Она очень весомо звучит в любом споре. Теорема Геделя! и можно еще по столу хлопнуть. Вот пример использования этой теоремы типичным дурачком:
>ИИ никогда не будет создан. Потому что теорема Геделя.
Вот у меня тут как раз такие ассоциации возникают.

>>1235927
> Очень смешно. В любом случае это только твои домыслы.
Это не мои домыслы. Если бы ты был знаком с физиологией и прочитал бы хоть начало 2ой части диссертации Брауэра, ты бы понял, что речь именно о рефлексах, т.к там прямым текстом отсылки к высшей нервной деятельности человека, которая рефлекторна. И само понятие примордиальной интуиции - это абстракция временнОго отношения между элементами восприятия, о чем там опять же прямым текстом, ничего даже додумывать не надо.
> Ты повторяешь этот тезис снова и снова как мантру. Только от этого он не становится более правдой. Или даже более убедительным.
А я тебя убеждать собирался? Я обьясняю, что понятие алгоритма неформализуемо по той причине, что такая формализация как формализация любого уточнения понятия алгоритма, в т.ч машины Тьюринга должна решать проблему останова. Иначе это будет не формализация, а только уточнение. Я вообще то излагаю общеизвестное ещё со времён Чёрча. Уже тогда стало понятно, что это невозможно. А ты вот и до сих пор не вдупляешь о чем речь, но ценное школомнение имеешь, разумеется.

>>1235754
Есть где-то во Франции, но это неточно.

>>1235927
>Там что тоже аксиом нет?
Вот не знаю, почему всех в треде так интересует этот дебильный вопрос, но вы может сначала поясните, что вы называете аксиомой? Вот у людей, которые пишут на коке, считается, что аксиом там нет, если только их не добавить, ну и это вполне уместно. Хотя выше в треде уже заметили, что в калькулусе вообще-то есть правила вывода с пустыми посылками, и считать ли их аксиомами - вопрос с неоднозначным ответом. Некоторые вообще называют аксиомами любые правила вывода, что тоже не лишено смысла.

>>1235927
>Я слышал в typetheorypodcast
Пиздец, пиздец.
Вот уж действительно, школьник - это как червь-пидор.
Только хуже.

>>1235969
Я еще и аниме смотрю.
Теперь можешь попробовать собрать свой сракотан по кускам.

>>1235968
>в калькулусе вообще-то есть правила вывода с пустыми посылками, и считать ли их аксиомами - вопрос с неоднозначным ответом
Один местный рефлекторный утверждает что этого делать нельзя и он - тут я цитирую -
>почему это нельзя считать аксиоматизацией, я выше рассказал
Так что либо вникай в его делирий выше по треду, либо спрашивай у него разъяснений. Я лично уже изрядно заебался с ним общаться.

>>1236127
>аниме смотрю.
Его все смотрят.
Тот факт что ты дебил и школьник это не меняет.

>>1235936
>уточнение формализации или формальное уточнение формализации не формализуема точно но это не точно.
Сразу видно человек разбирается в вопросе как рыба в воде. Хотя если у тебя весь мыслительный процесс на рефлексах, то тут уже можно не удивляться.
>Все всем давно известно аргументов не будет ты школоло
Твоя позиция ясна. Больше с тобой дискутировать смысла не вижу.

>>1236134
Я примерно понимаю, о чём он, но у него-то как раз дебильных вопросов нет, так что я не к нему обращался.

>>1236142
То есть то, что ты школьник не отрицаешь.
Фиксирую.

>>1236142
> Сразу видно человек разбирается в вопросе как рыба в воде.
Мань, ну ты же сам прекрасно понимаешь, что пытаешься поспорить просто потому что тебе печет. Возражений по делу от тебя не поступало, одно кукареканье.
> Хотя если у тебя весь мыслительный процесс на рефлексах, то тут уже можно не удивляться.
Вся высшая нервная деятельность человека имеет рефлекторную природу, это медицинский факт. Уже даже Павлов это показал более чем убедительно, не считая более поздних исследователей. Ты простую вещь пойми - твоя батруха и незнание чего-то - это не аргумент, а недостаток. Твой недостаток.

>>1236145
Анус себе зафиксируй, клоун.

>>1236151
>эта школоболь
Ясно.

>>1236150
>>1236157
Мамку ебал.

Вы ещё пососитесь тут, придурки.

>>1236162
А ты не завидуй :3

>>1236166
А ты мне не указывай, хочу и завидую.

>>1236168
>хочу и завидую.
Бедняжка :3

>>1236170
Не надо меня жалеть. Лучше повыёбывайся, а я буду смотреть.

>>1236176
>Лучше повыёбывайся
Не хочу :3

>>1236144
>Я примерно понимаю, о чём он
Может мне расскажешь и мне тоже станет немножко понятнее о чем он?

>>1236245
У аксиом нет вычислительного смысла. Они просто дают тебе готовые неделимые термы из нихуя. Согласно представлению о математической истине как о чём-то вычислимом, теоремы, полученные из аксиом, не являются истинными, тогда как хорошие правила вывода вычислительный смысл обеспечивают. В широком философском смысле вычислимая истина представляется более достоверной. Ну так вот, в исчислении конструкций и его расширениях хорошие правила вывода, и по умолчанию тех самых плохих аксиом там нет, типа закона исключённого третьего и всего такого. Это всё, конечно, зависит от того, что мы называем или не называем аксиомами.

>>1236250
Ожидал увидеть ответ в форме
>Правило вывода нельзя считать аксиомой потому что...
Но получил
>Аксиома это не правило вывода потому что...
Ну это для меня не открытие.
>В широком философском смысле вычислимая истина представляется более достоверной.
>, с точки зрения интуиционизма/конструктивизма
Поправил тут немного, можешь не благодарить.

>>1236273
>Правило вывода нельзя считать аксиомой потому что
Я же написал, почему. Потому что правила вывода и аксиомы - это разные вещи, в определённом контексте. То, что в другом контексте они могут быть отождествимы, я тоже писал выше.
>с точки зрения интуиционизма/конструктивизма
С точки зрения интуиционизма/конструктивизма невычислимое вообще никак не истинно, а широкий философский смысл позволяет расценивать вещи как более или менее достоверные.

>>1236277
Вот интересно стало, какой вычислительный смысл у терма refl, в конструкции refl:1=1.
Еще есть такие мысли. По вашему жизненно необходимо чтобы поверить в утверждение необходимо чтобы оно было справа от двоеточия и была некая программа слева. Я спрашиваю у интуициониста знает ли он доказательсто теоремы Х. Он дает мне в ответ программу. Я запускаю эту программу и вижу на экране
> "да"
или
> 42
Какая мне польза от этой программы и как она может поднять мою уверенность в верности теоремы Х мне не совсем ясно.

>>1236279
>какой вычислительный смысл у терма refl
Такой же, как у любого конструктора индуктивного типа - тривиальный.
>По вашему
По какому по-нашему? Я не из "этих". Мне вообще похую.
>Какая мне польза от этой программы и как она может поднять мою уверенность в верности теоремы Х мне не совсем ясно.
Сама по себе программа не должна поднимать уверенность, уверенность должна поднимать другая, вспомогательная программа, которая проверяет синтаксическую корректность первой. Ну а синтаксически корректные программы соответствуют корректным доказательствам теорем.

>>1236277
Ты наверняка представляешь себя ведущим философом математической мысли современности, но твои разъяснения полностью лишены содержания, примерно как это смешно утверждение
>В них можно выразить, т.е построить только то, что в них выводимо/построимо.

>Я же написал, почему. Потому что правила вывода и аксиомы - это разные вещи, в определённом контексте. То, что в другом контексте они могут быть отождествимы, я тоже писал выше.
Конечно теперь я буду с наслождением бегать по всему треду и искать что ты там и где написал и пытаться вывести "контекст" который ты подразумевал.

>а широкий философский смысл позволяет расценивать вещи как более или менее достоверные.
Спасибо, пойду наверну десяток томиков философии от Гегеля до Геделя, чтобы насладиться твоей непоколебимой правотой еще полнее.

>>1236287
>Ты наверняка представляешь себя ведущим философом математической мысли современности
Неправда, я не от кого не скрываю, что я школьник без пруфов (не тот, что выше).
>но твои разъяснения полностью лишены содержания
Тоже неправда. Есть теоремы, выводимые в одном случае и невыводимые в другом. Разница объективная и нетривиальная.
>Конечно теперь я буду с наслождением бегать по всему треду и искать что ты там и где написал и пытаться вывести "контекст" который ты подразумевал.
Я просто пытаюсь объяснить что-то, что знаю сам, тем, кому это может быть интересно. Убеждать тебя в своей правоте я не буду.
>Спасибо, пойду наверну десяток томиков философии от Гегеля до Геделя, чтобы насладиться твоей непоколебимой правотой еще полнее.
Лучше, чем сраться на дваче на пустом месте.

>>1236281
>Сама по себе программа не должна поднимать уверенность, уверенность должна поднимать другая, вспомогательная программа, которая проверяет синтаксическую корректность первой.
И у тебя нет даже ни малейшего сомнения что есть какая то странность в этой конструкции?

>>1236291
Сомнение есть всегда, его не может не быть. Но никаких очевидных проблем здесь я не вижу.

>>1236290
>Неправда, я не от кого не скрываю, что я школьник без пруфов (не тот, что выше).
Вот так споришь с кем то на сасачах до белого каления, а это оказывается школьник в итоге. Не первый раз на эти грабли наступаю. Ну успехов тебе в учебе.

>>1236297
Вот так на сосаче тебя спрашивают, как ты понимаешь чужое высказывание, а потом оказывается, что вы спорите.

>>1236279
> Какая мне польза от этой программы и как она может поднять мою уверенность в верности теоремы Х мне не совсем ясно.
Мозгов у тебя нет потому что. Я тебе миллион раз объяснял как это связано, ты же ебалай даже изоморфизм Карри-Говарда до сих пор не осилил. Хотя это и есть ответ на твой вопрос, дегрод ты злоебучий.

>>1236322
Вот это утверждение
>В них можно выразить, т.е построить только то, что в них выводимо/построимо
выдал школьник или уже-не-школьник?
>>1236339
>Даже не думайте спиздануть про Кари-Ховарда.
>ты же ебалай даже изоморфизм Карри-Говарда до сих пор не осилил
Вот ведь тупой шакал.

>>1236346
Мамку ебал.

>>1236346
>В них можно выразить, т.е построить только то, что в них выводимо/построимо
Это утверждение выдал некто, не уточнивший свой статус школьника или не-школьника.

>>1236353
Печально. Так бы хоть стала ясна причина его бессвязных лепетаний.

>>1236346
> тред про изоморфизм Карри-Говарда
>Даже не думайте спиздануть про Кари-Ховарда.
Мань, это суть пруверов как явления. То, что у тебя на это не хватает ума, как и на многое другое, само по себе доказывает только то, что ты тупень, а вовсе не то, что ты прав (как ты думаешь).

Я, блять, не пойму, вы откуда тут все такие умные? В хорошем смысле слова. Вы какие-то академики или что? Изоморфизмы-хуизмы, я даже не знаю, что это. Вы как так прокачались-то?

>>1236370
Ну в основном через чтение книжек и прослушивание лекций в университетах или на ютубе, ещё статьи всякие (вводные для нубов и научные).

>>1236370
Ну так мейлру - борда успешных людей. Фрилансер 300к/сек на академике едет и математиком погоняет.

>>1236378
Я за собой заметил, что если это не применять постоянно на практике, то все благополучно забывается.

>>1236370
На самом деле все очень просто:
1) Читаешь пару статей в википедии, в общих чертах пытаясь ухватить их суть
2) Пишешь какую-нибудь максимально туманную и бессвязную хуйню, вставляя умные слова из пункта 1
3) Всех кто тебе возражает называешь тупым школоло и поливаешь говном

>>1236381
> Всех кто тебе возражает
Возражений от тебя пока не поступало, одни кукареканья со стороны параши.

>>1236380
Ну хуй знает. Я как-то не забываю, хотя применять вообще негде.

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

>>1236381
>>1236382
Вот шакалы, вам заняться нечем? Идите в /b/.

>>1236386
Мне обычно хватает усвоить основные принципы (упражнениями) и увидеть общую картину, чтобы вся последующая информация по теме ровно ложилась на каркас и не забывалась. Если знание отвечает интуитивным представлениям (нет, я не интуиционист, отъебитесь от меня), то оно как езда на велосипеде - захочешь не забудешь.

>>1236390
А по теме треда есть какие-нибудь курсы? Просто книжки заебывает читать.

>>1236401
Есть лекции Виталия Брагилевского (вводные), есть интерактивный курс Software Foundations, где ты больше сам пишешь код, чем читаешь, есть ещё Conor McBride, который записывал лекции по агде (курс называется Computer Science 400 чё-то там). Есть ещё русскоязычные лекции по HoTT некоего Исаева, но мне они показались какими-то стрёмными.

>>1236404
> Есть лекции Виталия Брагилевского
Про Idris? Он вообще годно излагает?

>>1236410
Я имел в виду не про Idris, а которые про лямбду и Coq больше. С Idris вообще не рекомендую иметь дело. Излагает он мега-годно, на русском языке наверное лучше ничего не найти.

>>1236411
> С Idris вообще не рекомендую иметь дело.
Почему?

>>1236422
Создатель языка углядел в нём какие-то фатальные недостатки и начал пилить новый, без них. Так что я бы лучше подождал, пока он его релизнет.

>>1236425
Это, правда, не следует понимать буквально. Просто Coq и Agda вроде как надёжнее, старше и всё такое.

>>1236369
>> тред про изоморфизм Карри-Говарда
Мне казалось что тема треда пруверы. Вот смотрю в название прямо сейчас и вижу - Пруверов тред #1. Может оптический обман зрения?
>Мань, это суть пруверов как явления.
Как же тогда пруверы без изоморфизмов, их не существует? Или это какие то ненастоящие, неправильные пруверы?
>То, что у тебя на это не хватает ума, как и на многое другое, само по себе доказывает только то, что ты тупень, а вовсе не то, что ты прав (как ты думаешь).
Мне хватает ума чтобы интересоваться почему это так, в отличии от баранов молящихся на этот изоморфизм как на святую троицу.

>>1236430
Ну таки справедливости ради ОП-пост не упоминает вообще ничего, что не относилось бы к теории типов и, соответственно, к упомянутому соответствию.

>>1236353
Ай да школьник совсем запутал дядю, а вот эта фраза
>То, что в другом контексте они могут быть отождествимы, я тоже писал выше.
Это все к одному посту относится? Я так понимаю твой пост с объяснениями в треде только один.

>>1236382
Если я прошу доказать теорему X, а в ответ вижу
> Ты тупой; А->А; Почитай хотя бы вторую часть диссертации Брауэра; уебывай аутист; С философской точки зрения; Изоморфизм Кари-Ховарда тебя накажет! Лучше съеби
Тут вообще трудно что то дельное возразить.

>>1236425
>Создатель языка углядел в нём какие-то фатальные недостатки и начал пилить новый, без них.
Это ты про Blodwen?
Так он экспериментирует просто, разве нет?

>>1236281
>>какой вычислительный смысл у терма refl
>Такой же, как у любого конструктора индуктивного типа - тривиальный.
Ну так тогда можно про любую аксиому сказать, которые вы так не любите.
- Вычислительный смысл?
- Прост)))) он тривиальный.

Вот про конструкторы было бы интересно по-подробнее. А то как-то прям очень сложно все.
А еще лучше все аксиомы/правила вывода coc и coic обозреть в одной табличке.

>>1236561
>все аксиомы/правила вывода coc и coic обозреть в одной табличке.
По первому в википедии же приведено, выше ссылка. По второму статья гуглится, там многа букв, разные вариации и в целом не оче понятно.

>>1236430
> Мне хватает ума чтобы интересоваться почему это так, в отличии от баранов молящихся на этот изоморфизм как на святую троицу.
Ну и почему это так? Как ты можешь понять, почему что-то, если ты не понимаешь даже смысла этого чего-то?
> Как же тогда пруверы без изоморфизмов, их не существует? Или это какие то ненастоящие, неправильные пруверы?
Например? Речь о пруверах на основе теорий типов.
>>1236561
> Вот про конструкторы было бы интересно по-подробнее. А то как-то прям очень сложно все.
> А еще лучше все аксиомы/правила вывода coc и coic обозреть в одной табличке.
Я тебе сто раз говорил, что не только правила вывода COC, но и вся полнота картины, откуда они, зачем и как из простой лямбды постепенно строится PTS, или лямбдаС или COC что то же самое, и даже как вся эта хурма соответствует логическим исчислениям по изоморфизму, которого тут боятся, все вот это и многое другое полностью отражено в кубе Барендрегта. Правила вывода СОС в одной табличке дадут очень мало, если нет понимания откуда они взялись, зачем они и как и какому логическому исчислению соответствуют и какую часть математики в них можно представить, т.е в т.ч и доказать, для чего и нужен прувер.

>>1236561
> - Вычислительный смысл?
> - Прост)))) он тривиальный.
Вычислительный смысл это операционная семантика. Ну или денотационная и какие там ещё есть, в зависимости от конкретной реализации конкретной теории типов.

>>1236561
Съеби из треда.

>>1236547
Да, просто экспериментирует. И Idris даже активно мейнтейнится, как я посмотрел. Теперь даже и не знаю.

>>1236484
Это совсем другая фраза. И что с ней не так, непонятно.

>>1236561
>Прост)))) он тривиальный.
У слова "тривиальны" вообще-то довольно конкретный смысл есть, его не стоит понимать как "очевидно" или вроде того. Конструкторы при вычислении просто не изменяются, в отличие от термов со сложной структурой. Почему так же нельзя сделать с аксиомой - потому что аксиомы логически содержательны, они представляют собой неделимое доказательство какого-нибудь факта, может быть довольно сложного, в отличие от индуктивных типов и их конструкторов, которые бессодержательны. Конструкторы просто задают свободную алгебру, т. е. что-то типа синтаксиса.
>А еще лучше все аксиомы/правила вывода coc и coic обозреть в одной табличке
Обозри, конечно, кто тебе мешает?

>>1236635
>Обозри, конечно, кто тебе мешает?
То что ее нигде нет, трололоша.

>>1236671
Ну сделай, если тебе так надо. Дело пяти минут.

>>1234974
Сделай ты, раз такой умный.

>>1236675
>>1236672

>>1236675
Мне нахуя? Можно же просто открыть одно в одном окошке, а второе в другом.

>>1236677
Ты вообще понимаешь о чем речь? Ты не тот терминальный дебик что proof от Proof отличить не мог? Это бы многое объяснило.

>>1236680
Нет, я не тупой, мне показалось, что это предложение сделать таблицу с правилами вывода. А дерево тоже строить не буду, сказал же, сами блять стройте, это же вам надо, а не мне.

>>1236635
>У слова "тривиальны" вообще-то довольно конкретный смысл есть
С этом вообще то никто не спорит, не надо выставлять соломенных чучел себе на потеху.
>доказательство какого-нибудь факта, может быть довольно сложного
А вот тут не соглашусь. Что значит сложного/не сложного? Ты берешь некоторый факт и либо принимаешь его как аксиому либо нет.
>Конструкторы просто задают свободную алгебру, т. е. что-то типа синтаксиса.
А вот тут поподробнее если можно.

>>1236681
> это предложение сделать таблицу с правилами вывода
Да хотелось бы их увидеть. Там еще я облажался со ссылкой в одном месте.

>>1236683
>С этом вообще то никто не спорит
Ну я тогда вообще не понял, кто с чем спорит.
>Что значит сложного/не сложного
"Сложное" следует понимать как "содержательное".
>А вот тут поподробнее если можно.
Объявляя индуктивный тип с конструкторами, ты определяешь алгебру термов. Элементы алгебры - термы, построенные из конструкторов этого типа, имеющие этот самый тип. Ну и можно вывести, что разные конструкторы не равны между собой, и любые два синтаксически различных таких вот терма не приводятся вычислениями к одинаковым термам.

>>1236685
Все правила вывода есть в википедии и в пейпере Introduction to Calculus of Inductive Constructions, и то, и другое, уже кидали выше, ну и первые ссылке в гугле же.

>>1236618
>Ну и почему это так?
Блядь ты наркоман что ли? Если бы я знал, то зачем стал спрашивать на сосаче?
>если ты не понимаешь даже смысла этого чего-то?
Ну это твои личные измышления, хуй пойми на чем основанные.
>Например?
metamath, otter, HOL, TLA, тысячи всяких мелких прикладных опередений, каждый желающий может написать под себя.
>Речь о пруверах на основе теорий типов.
Эээ... почему это?
>Я тебе сто раз говорил
Первый раз вижу упоминание о кубе в треде, к контексте что он нужен чтобы понять coc. Сохацкий это ты? Ты свои разговоры с друганами в тред не проецируй.

>>1236687
>Ну и можно вывести, что разные конструкторы не равны между собой, и любые два синтаксически различных таких вот терма не приводятся вычислениями к одинаковым термам.
Я весь тред пытаюсь добиться объяснения КАК?

>>1236690
Если я тебе щас покажу пример индуктивного типа и терм, доказывающий различие двух его конструкторов, ты начнёшь ныть, чтобы я тебе строил дерево вывода и объяснял всё непонятное?

>>1236691
Вот этот терм >>1236678. Мне нужен его вывод из правил которые якобы все в пейпере. Ты ведь его читал и понял? Тогда тебе не составит труда расписать.

>>1236692
Очень даже составит. Понять, какие именно правила надо применить, совершенно нетрудно, но вот унифицировать термы и контексты довольно муторно, да я ещё и не дружу с латехом, так что придётся руками рисовать. Ну его нахуй. И вообще, мне кажется, что ты пиздишь, и не пытаешься реально что-то выяснить, а просто хочешь навести здесь присутствующих сократической индукцией на какую-нибудь хуйню, чтобы показать, что они все неправы. Если ты честно и в явном виде сформулируешь свой вопрос/претензию, я может попытаюсь тебе серьёзно ответить.

>>1236694
Хочу понять как работает coq из первых принципов. Ничего такого в своих вопросах не вижу и задан каждый в треде раз по пять.
Но может тогда ты пояснишь мне хотя бы вот этот >>1235115 момент из того самого пейпера.

>>1235115
"logic captures" - это значит, что соответствующее утверждение выводимо как терм нужного типа. Initial algebra - это что-то похожее на свободную алгебру, там тоже просто берутся исходные операции и порождаются все возможные термы, из них составленные. Если хочешь более формально, ботай категории, ничего не поделать.

>>1236704
Так о какой логике идет речь?

>>1236709
Ну о той, которая из соответствия Карри-Говарда.

>>1236704
Т.е. это просто формулировка утверждения, которое мне интересует? Где тогда его доказательство?

>>1236711
Ой не не траль плез. Хоть в пейпере про эту парочку ни слова.

>>1236689
> Первый раз вижу упоминание о кубе в треде, к контексте что он нужен чтобы понять coc.
COC это правый верхний дальний угол куба Барендрегта в стандартной позиции. Stlc, т.е простая типизированная лямбда - нижний левый передний угол, расширяемый добавлением правил в трёх направлениях, которые в итоге, комбинируясь все вместе, дают COC.
> metamath, otter, HOL, TLA, тысячи всяких мелких прикладных опередений, каждый желающий может написать под себя.
Либо игрушечные, либо все те же типы, как например HOL.

>>1236713
> Ой не не траль плез. Хоть в пейпере про эту парочку ни слова.
Потому что у читателя предполагается понимание того, как операции с типами соответствуют логике.

>>1236712
Доказательство - это терм, проходящий проверку типов.

>>1236713
Ты понимаешь, что ты конченый?

>>1236718
Nyyet лалка вот тут я тебя подловил (хотя на самом деле не собирался этого делать). Мне нужно доказательство этого утверждения, утверждения в мета теории, это ни какой не терм.
>>1236720
Может хватит уже, ебанашка? Твое мнение услышано и нахуй послано. Хватит высирать свою имбецильность через каждый десяток постов.

>>1236723
Ладно, разговор с тобой окончен.

>>1236714
Пиздец нахуй ты это все написал? Этого вообще никто не спрашивал. Определение этого куба я и так могу глянуть в вики. И сделал это лет пять назад уже. У штудентика горит поделиться с таким трудом приобретенными знаниями с миром, что он даже не вдупляет что речь вообще о другом.
Откуда про HOL дровишки? Сам с ним не так уж близко знаком, но никаких типов там не замечал.

>>1236723
Как вариант, ты конечно можешь попробовать формализовать сам coq и предоставить таки нужный терм, но думаю попка треснет от такой задачи.

>>1236726
Ну хоть одним ебанатом в треде поменьше станет.

>>1236723
> Nyyet лалка вот тут я тебя подловил (хотя на самом деле не собирался этого делать). Мне нужно доказательство этого утверждения, утверждения в мета теории, это ни какой не терм.
Мамку свою с ашотом подлови. Метатеория COC это вычислимость. А любая возможная там типизация представима в самой теории, т.к кумулятивная иерархия типов.

>>1236737
Может хватит уже хуйню нести? Либо давай доказательство, либо лучше следуй за тем дебиком выше.

>>1236748
Тупая пидорва как раз собралась в этом треде и тупит. Вы просто заебали. Если ты блядь даже не в состоянии понять вопрос, то просто так и скажи. Это не значит что тебя кто то пытаеться ололо затралить, это просто значит что ты очень тупой.

>>1236756
Тебе выше сто раз обьяснили, почему конструктивизм и алгоритм неформализуемы, и почему формализм это принципиально другой подход. Вся формализация конструктивизма это просто еще одно равнообьемное уточнение понятия алгоритма, коих и так дохуя. Ты же вместо того, чтобы вникнуть в тему, визжишь и кукарекаешь, называя всех тупыми, хотя по факту итт один тупень, и это ты.

>>1236760
Я же тебе писал что ты вообще не понимаешь что плетешь
https://en.wikipedia.org/wiki/Algorithm#Formalization
Только к моему вопросу это вообще не относиться. Я хочу увидеть конкретные аксиомы, или если ты так боишься этого слова и не понимаешь его - то правила вывода доказывающие инъективность конструкторов. И это только один вопрос, можно было бы еще много таких вопросов задать, но нет вообще никакого смысла, если в треде одни только пидорасы способные кидаться говном и диссертациями Брауэра (что примерно одно и тоже)

>>1236765
> Я же тебе писал что ты вообще не понимаешь что плетешь
Ты читал, что там по ссылке? Тебе, дебилу сто раз сказано, что машина Тьюринга не формализует понятие алгоритма, т.к не решает проблему останова, каким надо быть дегродом, чтобы не понимать таких вещей. Соси хуй короче, ты слишком деревянный.

>>1236816
>машина Тьюринга не формализует понятие алгоритма, т.к не решает проблему останова
Можешь процитировать, где на той странице такое сказано?

мимо

>>1236831
> Можешь процитировать, где на той странице такое сказано?
Исторический обзор, где про Entscheidungsproblem.

>>1236816
Пиздец ты тупой, просто пиздец.

>>1236839
> Пиздец ты тупой, просто пиздец.
Ты тоже сходи нахуй почитай по своей ссылке про Entscheidungsproblem, очень поучительная история про ограниченность формализма в математике.

>>1236845
Я про это еще в школе читал.

>>1236845
Давай прямую цитату подтверждающую твой бред как тебя просили. Ах да ее же там нет ты просто что-то в своем делирии додумал. О чем же тогда целый раздел в который я тебя ткнул, не удосужишься рассказать?

>>1236851
> О чем же тогда целый раздел в который я тебя ткнул, не удосужишься рассказать?
О машине Тьюринга, мань. Которая не решает проблему останова.
>>1236849
> Я про это еще в школе читал.
Если бы ещё и понял...

>>1236861
У меня с этим проблем нет. Вот если бы ты понимал что тебе пишут прямо сейчас прямо в этом треде было бы гораздо проще с тобой. Ждем-с.

>>1236861
Но ведь раздел немного по другому называется. Как же так получилось?

>>1236836
Я как раз этот абзац хотел скопипастить, но решил не торопить события. Давай все-таки конкретнее: процитируй конкретный текст с той страницы, где говорится, что "машина Тьюринга не формализует понятие алгоритма, т.к не решает проблему останова", пожалуйста.

(если не хочешь\не будешь этого делать, так и скажи, no big deal)

>>1236896
>Постишь дельные мысли, стараешься
>Аутист, ты хуйню сморозил, съеби с треда.
>Шизик засравший полтреда своим нелепым делирием
>(если не хочешь\не будешь этого делать, так и скажи, no big deal)
Заебись, программач доска для цивилизованных дискуссий. Психбольницу захватили психи.

>>1236955
Борда. Борда никогда не меняется.
Шизик тебя всегда победит тупо количеством текста. Отличить адекватность от шизы аудитория не может.

>>1236955
Ты лишний пост загринтекстил. Ты >>1236836-анон? Тогда ответь, пожалуйста, на >>1236894-пост (ну или на >>1236896).

>>1236894
Я на вопрос ответил исчерпывающе, и ты это понимаешь, дальше сам. Статью Тьюринга "on computable numbers" можешь почитать, хотя бы полное ее название. Но можешь и дальше тут клоуна корчить, мне все равно, правда.

>>1236978
>Ты >>1236836-анон?
Нет же ох и лол
>Отличить адекватность от шизы аудитория не может
как метко

>>1236982
>Я на вопрос ответил исчерпывающе
У меня был не вопрос, была просьба: процитировать "машина Тьюринга не формализует понятие алгоритма, т.к не решает проблему останова" с той страницы. Хотя, вопрос тоже был: "можешь процитировать?" - подразумевает ответ да\нет. Ответь, пожалуйста, исчерпывающе на этот вопрос, если тебе не трудно.

>>1236955
>дельные мысли
>хуита на половину страницы
Ты хуйню сморозил, съеби с треда.

— Почему существует только то, что порождается алгоритмом?
— Потому.

— Ты ебанутый?
— На это неоднократно давался ответ.

— Ты можешь доказать формулу Гаусса?
— Твоя вера не нужна.

— Пошёл нахуй, ебанашка.
— Ты не воспринимаешь объективные аргументы.

— Какие?
— Хватит спрашивать одно и то же.

— Ты издеваешься. Ты не можешь писать это всерьёз.
— Я не виноват, что ты такой тупой.

>>1237608
Ты только не реви, ладно?

>>1237608
Ты хуйню сморозил, съеби с треда.

>>1238094
Конечно съебу, хуле тут еще делать? Никакого дискача тут нет и похоже не будет. Одна только интуитивная обосратка брызжет своим поносом. И еще один кокер, он вроде хотел что то разъяснить, но боится что его стралят и к тому же лениво. Все еще проигрываю с этой хуйни. Ну и пара просто дибилов подсирающих односложными высерами типа это охуенно смешно.

>>1238197
> вы все дураки и не лечитесь, одна я в белом пальто красивая
Валерия Ильинична, вы ж померли?..

>>1238236
Сколько же в тебе говнища что ты никак не просрешься окончательно, больное уебище?

Просто оставлю это здесь
https://fstar-lang.org

>>1238253
> Просто оставлю это здесь
F* весьма каличная лямбда по сравнению с коком. Тогда уж надо было Morte для хачкиля вспоминать, там хотя бы COC.

>>1238253
F-залупа не нужен потому что есть Lean.
Lean еще больше не нужен потому что есть Coq.
prove me wrong

>>1238280
Coq не нужен, потому что есть Agda.

>>1238947
Agda ненужна, потому что есть ATS.

>>1238958
>>1238947
>>1238280
>>1238263
>>1238253

Что, петушки-хипстушки, вы там чёт спизданули?

http://community.wolfram.com/groups/-/m/t/1135271

>>1238965
Унеси эти костыли.

>>1238958
ATS императивная параша же

>>1238197
Опять хуйню сморозмил, съёбывай быстрее.

>>1239933
>>1238245

>>1240752
Ну как бы, если есть полноценные зависимые типы, то уже можно формулировать и доказывать теоремы. Тактики и специальные интерфейсы - это вопрос удобства, а не доказательной силы. Правда, "прувер" ещё можно понимать в значении "автоматический генератор доказательств", тут да, очевидно, нужна дополнительная машинерия.

>>1240752
Ты дурачок, лол?

>>1240761
>>1240824
Да блять, речь о наличии какой-то автоматизации доказательства. То, что для самой возможности доказательства не нужен даже идрис, и все можно доказать на бумаге, я и так знаю. В коке есть тактики и даже язык для их написания ltac. Мне интересно, чем это можно заменить в идрисе, хотя бы как-нибудь.

>обсуждать хоть что-то серьезное на доске с дегенератами у которых в идеи-треде каждая 1.5 идея это бот в не менее дегенеративном ВКонтакте

>>1240862
в /math/ два с половиной шизофреника.

>>1240878
> в /math/ два с половиной шизофреника.
Ну так обсуждай на 8chan, Reddit, stackexchange, Сосач как интеллектуальное комьюннити давно потерян. Ты тут только деградировать будешь.

>>1240882
>Reddit
А там есть русскоязычное сообщество?

>>1240916
https://www.reddit.com/r/EnglishLearning/

>>1240882
Увы, ты прав. Почему я вообще здесь сижу?

>>1240971
>Почему я вообще здесь сижу?
Потому что в нормальном месте твои высеры потрут и тебя отхуесосят и забанят. Можешь не благодарить.

>>1240984
>отхуесосят
словно что то плохое

>>1240916
>it
>русский язык
С таким подходом только на хабропарашу

>>1240984
Мдауш... хотел бы я быть таким же умным, как ты,,,

>>1241013
Нужно сначала выиграть в генетической лотерее, а потом постоянно работать над собой - иначе пиздец.

Давно уже пора делать учебник математики с йобами и мемасами. Но интерактивный, чтобы адаптировался под ученика с помощью слесарьплова. Дополнительно прикрутить Coq и всякие там демидовичи. Теоремы сначала будем писать в виде будапешт-тредов. Кто за?

>>1242063
Кроме шуток, если без блядских мемчиков и рака, то можно попробовать.

>>1242096
Если в более серьезном манере, то так это видится тобою? Я думаю, что оно должно использовать программированное обучение.

>>1242161
Я уточнил значение слова "слесарьплов" и резко передумал. Нахуй надо.

>>1242164
Это для красоты сказано. Суть в том, что все равно будет составляться индивидуальный план. Даже слесарьплов здесь не нужен особо.

>>1242223
А зачем нужен индивидуальный план?

>>1242472
Записываешь утверждение как тип (у которго тоже есть тип, у которого есть тип... различие между типами и термами размыто) и дальше пытаешься придумать терм, имеющий в точности этот тип. Если тайпчекер подтвердил, что твой терм соответствует твоему типу, то считаешь утверждение доказанным. Сам терм можно строить из других термов, либо написать последовательность тактик, из которых этот терм сгенерируется автоматически. Можно сначала написать общую структуру терма, оставляя в нём незаполненные места, сразу проверить, не ругается ли чекер, а потом уже заполнять пропуски.