Оснований тред №13 112865 В конец треда | Веб
Очередной тред, посвященный первой культуре - основаниям математики. Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него. Просьба воздержаться от срачей на эту тему, так как тут и сраться не о чем.
Предыдущий:
https://2ch.hk/math/res/109635.html (М)
2 112869
Не забываем определять N.
3 112870
>>2865 (OP)
Что за дебил шапку писал?
4 112871
>>2870
Очевидный конструктивный петух, как и все треды до этого. Предлагаю в этот раз создать альтернативный непетушиный тред оснований, а петушню бойкотировать.
5 112872
>>2865 (OP)
Это тред тусовочки из какой-нибудь конфы, или тут могут накидать литературы для общего развития?
6 112873
>>2872
для общего развития можно и школьные учебники почитать (ну, без шуток, какую-нибудь биологию для продвинутых классов), так что конкретизируй
8 112879
>>2878
Спасибо

>>2873

>так что конкретизируй


Ну вот в заголовке висит:
"Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него". Это что-то из теории моделей или что это?
9 112881
>>2879

> "Дежурное напоминание - абстракция не может быть первичнее примеров, содержащих абстрагируемое свойство, а метаязык строится только над объектным языком, и так же не может быть первичнее него". Это что-то из теории моделей или что это?


Это базовые свойства абстракции и метаязыка как явлений. Один из местных клоунов, известный как N петух, просто игнорирует эти моменты в своих жалких попытках "доказать", что аксиомы Пеано якобы не определяют множество натуральных чисел. Вычитал он это у Успенского, в целом там логика уровня того мультфильма про олимпиаду, где "баба Яга против", а вся "аргументация" строится на игнорировании сути абстракции и метаязыка.
tree.png373 Кб, 1498x1984
10 112883
А про аксиому фундирования сделаю некоторое дополнение, чтобы не казалось, что претензия искусственная. Есть теория множеств Aczel'а, в которой множества рассматриваются как графы. Точки - элементы, стрелочки - отношение "быть элементом". Пикрелейтед - иллюстрация.

Все ZFC-шные множества в такой теории оказываются деревьями (из-за фундированности). Но теория Aczel'а этими множествами не ограничивается и постулирует, что любой связный ориентированный граф является картинкой какого-нибудь множества. В том числе - граф с циклами.

Например, граф, состоящий из одной точки и висящей в ней петельки является картинкой множества x = {x}.

Такая теория множеств оказывается неожиданно интересной и вполне согласующейся со здравым смыслом. Поэтому интерес рассматривать анти-фундированные множества есть. И не стоит всегда предполагать, что x и {x,y} - разные множества априори.
image.png597 Кб, 1000x568
11 112884
>>2865 (OP)
Снова в шапку забыл закинуть картинку, характерезующую тред... Плохой перекат.
12 112886
>>2865 (OP)
Общее развитие продвигается полным ходом.
13 112887
>>2879

>Это что-то из теории моделей или что это?


это просто какое-то околоматематическое ШУЕ, как по ссылке https://groupoid.github.io/formal.one/ из >>2878, такое нужно игнорировать
14 112891
>>2887
Как тебе такое ШУЕ?

https://youtube.com/watch?v=3dhC-eTH1hA
15 112892
>>2891
Это ДРУГОЕ!!!111 Да и вообще, было бы странно ожидать чего-то содержательного от деятеля, который мало того, что не знал разницы между конструктивизмом и ультрафинитизмом, так ещё и пытался перемагивать первое вторым. Интересно, с Успенским они вместе выступали на одной сцене? Биба и Боба - два великих математика.
16 112893
>>2891
не знаю, не хочется смотреть часовое видео по ссылке от тех, кто рекомендует почитать Сохацкого
17 112896
>>2893
Но он не рекомендовал читать Сохацкого, это я рекомендовал.
18 112898
>>2896
ну и нахуя ты это сделал?
19 112899
>>2898
Как минимум, он на голову выше всяких совковых образованцев, на которых тут дрочат, и которые в математику пошли ради того, чтобы на завод не погнали. Ты просто вслушайся, что несёт деятель с видоса >>2891 про связь текста и математики, это же полный пиздец. Ну можно же было что-то в тему почитать, ладно, я не говорю про Скиннера, там букв много и они нерусские какие-то, но зачем придумывать какую-то хуйню из головы? Ну просто скажи, что не знаешь темы. Но нет, надо с умным видом кринжа наваливать, профессор же типа. А потом всякие N петухи этой шизой индоктринируются и серят здесь годами.
20 112900
>>2899
Кто индоктринировал тебя, конструктивный петух?
21 112902
>>2899

>Как минимум, он на голову выше всяких совковых образованцев


Он полуграмотный шарлатан, который разводит неопытных, что не могут самостоятельно увидеть в его писанине грубые ошибки, о чём уже неоднократно писали, но ты упрямо продолжаешь пиарить разводилу.
22 112903
>>2902

> Он полуграмотный шарлатан,


До вышеупомянутых деятелей в вопросах ШУЕ ему очень далеко, тем не менее.
23 112904
>>2903
Если есть кто-то хуже, это не повод пиарить шарлатана.
24 112906
>>2902

> неопытных, что не могут самостоятельно увидеть в его писанине грубые ошибки,


Их там и нет. Пример ты все равно не приведешь, даже один.

> о чём уже неоднократно писали


Кто-то что-то пукнул без единого пруфа.
25 112907
>>2902

Наверное нужно указать, что он эти свои тексты не публиковал, а при распространении среди своих студентов просил их дальше не рассылать. Они совершенно точно имеют элемент преувеличения с художественной целью и троллинга в целом, что довольно трудно не заметить при чтении.
26 112908
>>2906

>Кто-то что-то пукнул без единого пруфа.


Ага, здрасьте, приехали, уже забыл что ли?

>Их там и нет. Пример ты все равно не приведешь, даже один.


Открываю https://groupoid.github.io/formal.one/, кликаю по ссылке «Математичні компоненти» (https://groupoid.space/misc/library/), смотрю в его «определение» «inf_grpd» и тихо охуеваю от полного непонимания им темы (даже в HoTT-буке есть про ∞-усечённые типы).
В обмен на твой анус только потом не жалуйся могу на его любимом cubicaltt пруф написать, что этот его inf_grpd эквивалентен стягиваемости (isContr, лол!) типа. И это только самое дегенеративное, что вспомнилось сходу.

>>2907

>что он эти свои тексты не публиковал


https://www.researchgate.net/profile/Maksym-Sokhatskyi-2#publications

>а при распространении среди своих студентов просил их дальше не рассылать


Неправда. Пруфов не будет, пруфы проёбаны.

>Они совершенно точно имеют элемент преувеличения с художественной целью и троллинга в целом


Всё так.

>что довольно трудно не заметить при чтении


Ну, как показывает практика, некоторым хоть ссы в глаза, всё конструктивная роса.
27 112909
>>2908

>Открываю https://groupoid.github.io/formal.one/, кликаю по ссылке «Математичні компоненти» (https://groupoid.space/misc/library/), смотрю в его «определение» «inf_grpd» и тихо охуеваю от полного непонимания им темы (даже в HoTT-буке есть про ∞-усечённые типы).


Ну так напиши ему в issue, пусть оправдывается. В чем проблема? Здесь ты максимум напугаешь N-петуха украинскими словами, опять весь тред засерит.
28 112910
>>2909

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


Так это бессмысленно: он в issue прокричит что-нибудь про агентов КГБ, удалит его через пару минут и заблочит на гитхабе. Прецеденты уже были.
29 112911
>>2883

>теории оказываются деревьями


*конечного ранга, без бесконечных веток
30 112912
>>2906
Тебе буквально несколько тредов назад показали, что "спектральная категория языков" это бессмысленная хуйня.
31 112913
>>2912
Не было такого. Разговор был о том, что идея недопилена, и все. Остальное ты сам себе напридумывал.
32 112914
>>2913
Разговор был о конкретных ошибках в его тексте о категорії формальних мов.
33 112915
>>2914

> Разговор был о конкретных ошибках в его тексте о категорії формальних мов.


Например?
35 112917
>>2916
Там дальше все это расписано подробно, с кодом. Что сказать-то хотел?
36 112918
>>2917
Да, именно, с кодом расписано, что Сохацкий херню написал, как и тут >>2908
37 112919
>>2918
Как похожая типизация с разными названиями опровергает идею спектральной категории формальных мов?
38 112920
>>2919
Какая ещё похожая типизация с разными названими?

>идею спектральной категории формальных мов


У Сохацкого никакого вразумительного определения нет, что выяснили два треда назад.
39 112921
>>2920

> У Сохацкого никакого вразумительного определения нет,


Есть и определения, и код.

> что выяснили два треда назад.


Кто выяснил? Ты и твои воображаемые друзья? Они там сейчас с тобой, в одной комнате?
1693422267604.png60 Кб, 890x348
40 112922
41 112923
>>2922
Это откуда? Ссылку бы принёс
grafik.png102 Кб, 1036x510
43 112925
>>2921
Ну ё-моё, опять за старое?

>определения


Это вот эти определения, да? Что язык только с Π-питом в язык только с Σ-типом разумным образом не вкладывается не надо опять рассказывать, надеюсь?

>код


Это вот этот код? https://github.com/groupoid/anders/blob/main/lib/foundations/mltt/mltt.anders
Универсумы там найдёшь? А индуктивные типы? А как связано «Π-form» с остальной структурой, объяснишь? А «Σ-form», кстати, тоже как? Да и «=-form», впрочем.

>Кто выяснил? Ты и твои воображаемые друзья? Они там сейчас с тобой, в одной комнате?


Забыл уже всё? Так сейчас напомним.
44 112926
>>2925

>только с Π-типом*


быстрофикс
45 112927
>>2925

> Это вот эти определения, да? Что язык только с Π-питом в язык только с Σ-типом разумным образом не вкладывается не надо опять рассказывать, надеюсь?


То есть, ты даже нотацию не осилил? Там нет никаких "языков только с П типом", это сокращённые названия для разных типизированных лямбд, прямо на твоей же картинке это есть. "Язык только с П типом" это PTS, pure type system Барендрегта итд. Читать бы научился для начала...
46 112928
>>2927
Ты чё, Сохацкий что ли? У него такая же дегенеративная манера вести дискуссии.

>Там нет никаких "языков только с П типом",


А? На первой картинке что? Как вот эту ΠΣ понимать?
А на второй картинке что такое? Зачем же в (неком) MLTT-72 в синтаксисе и Π, и Σ?

>"Язык только с П типом" это PTS, pure type system Барендрегта итд


Да, правда что ли? Таблицу (картинка 3) его же открой (где он, помимо прочего, каким-то образом связывает Σ с неким MLTT-72).
47 112929
>>2928

> А? На первой картинке что?


PTS это, на третьей же картинке прямо написано.

> Как вот эту ΠΣ понимать?


MLTT 72, опять же, это там прямо написано. Если и этого мало, дальше есть полная типизация.

> А на второй картинке что такое? Зачем же в (неком) MLTT-72 в синтаксисе и Π, и Σ?


Затем, что в MLTT 72 есть оба этих зависимых типа. Ты даже нотацию не понял, зато спорить зачем-то лезешь.
48 112930
>>2929

>PTS это, на третьей же картинке прямо написано.


ΠΣ — это PTS? Или что ты хотел сказать?

>MLTT 72, опять же, это там прямо написано.


А, так ΠΣ — это MLTT-72? Я тебе говорю: раз Сохацкий использует O_ΠΣ там, где подразумевает использование обеих конструкций (именно подразумевает, потому что никаких синтаксических деревьев он строить почему-то не хочет), то O_Σ — это, очевидно, синтаксис лишь с Σ. И, далее, где (MLTT-72) Сохацкий подразумевает использование и Π, и Σ, он пишет и O_Π, и O_Σ. Так откуда стрелки из O_Π в O_Σ?

>Затем, что в MLTT 72 есть оба этих зависимых типа.


Да, а теперь см. выше.

>Ты даже нотацию не понял, зато спорить зачем-то лезешь.


Кто тут не понял-то, ёпт?
49 112931
>>2930
В общем, как с нотацией разберёшься, приходи. Пока говорить не о чем.
50 112932
>>2931
То есть будем неудобные вопросы просто игнорировать? А с кодом-то там что, всё нормально?
Зачем ты вообще оправдываешься за этого проходимца? Лучше бы нормально в тему вкатился, чтобы не плавать в материале как Максимка, что советовали два треда назад ещё.
51 112933
>>2932
Могу ещё добавить, что в другом разделе (внезапно), можно найти эти самые O_Π и O_Σ, и там, оказывается, в O_Π только лишь Π-тип, а в O_Σ, да, только Σ-тип.
52 112934
>>2933
Описание ко второй картинке прочитай и не неси дичь.
>>2932

> То есть будем неудобные вопросы просто игнорировать?


Неудобных вопросов пока не поступало, есть только непонимание нотации.
53 112935
>>2934

>Описание ко второй картинке прочитай и не неси дичь.


Там написано, что если к языку с O_Π добавить O_Σ, получится MLTT-72 (або O_ΠΣ). В чём проблема?

Вот тебе, короче говоря, заготовка: https://pastebin.com/u70gz6Dk
Заполняй отмеченное место построением обсуждаемой стрелки.
54 112936
>>2935
Просрал номера универсумов: https://pastebin.com/bYAtQ0dN
55 112937
>>2935

> Там написано, что если к языку с O_Π добавить O_Σ, получится MLTT-72 (або O_ΠΣ). В чём проблема?


Проблема в том, что ты требуешь стрелку из PTS не в MLTT 72, а в сигма тип, который просто добавляется к PTS для получения MLTT 72. Либо это троллинг тупостью, либо ты правда не понимаешь о чем речь вообще.

> module dvach where



> data nat


> = zero


> | succ (n : nat)


И тут N петуха порвало.
grafik.png18 Кб, 753x129
56 112938
>>2937

>Проблема в том, что ты требуешь стрелку из PTS не в MLTT 72, а в сигма тип, который просто добавляется к PTS для получения MLTT 72.


Ну правильно, а у Сохацкого что на пике, алло?
17082370226930.png68 Кб, 1036x510
57 112939
>>2938

> Ну правильно, а у Сохацкого что на пике, алло?


У тебя часть пика. У Сохацкого там то же, что я описал, а именно, что каждая последующая мова в списке содержит в себе предыдущую.
58 112940
>>2939
Речь сейчас про первую часть пика (которая каким-то образом должна порождать вторую часть).
59 112941
>>2940
На первой части сокращённая запись того, что на второй.
60 112942
>>2941
Нет, он пишет, что послідовність синтаксичних дерев (первая часть пика) генерує (!) відповідну послідовність мов програмування.
На первом пике самостоятельная послідовність (объекты + стрелки), которую и обсуждаем.
Аннотация 2024-02-18 154019.png86 Кб, 772x495
61 112943
>>2942
Давай все-таки не будем из контекста что-то дергать и обсуждать как вещь в себе? Там все определения приведены, читай.
62 112944
>>2943
Какую, блядь, вещь в себе, ты гуманитарий что ли?
Тебе Сохацкий чёрным по белому написал, что есть вот такая послідовність, а ты делаешь вид, что он такого не писал.
63 112945
>>2925
Возможно имеется в виду "последовательность" в таком же смысле в каком "хуй - пизда - джигурда" последовательность слов.
64 112946
>>2945
Да, конечно, а следом почему последовательность уже настоящая, в категории? Или там тоже?
Можно миллион оправданий придумать (зачем?), а настоящий ответ один: Максим нарисовал стрелочек, чтобы нарисовать стрелочек, чтоб пацаны зауважали; никакого глубокого смысла в этих стрелках просто нет.
Или непонятно? Мне продолжить и в https://groupoid.github.io/formal.one/ и https://github.com/groupoid/anders/ ещё перлов найти?
65 112947
Как переводится derivation на Русский? Или это от лингвистического понятия деревации и прям так и писать?

"A derivation in type theory is a finite tree in which each node is a valid rule of inference"
66 112948
>>2946
Давай. Я не понимаю чего вообще этот хохол пытается показать. Вроде выстраивает какую то мета-теорию языков в своем собственном собранном на коленке язычке. План надежный просто как швейцарские часы.
67 112950
>>2948
https://github.com/groupoid/anders/commit/91bc9537b1b19ef7f539f5afa67ede207690c24a#diff-325adff688f303388bbc224312d23307967c735971ccbc5627237b256fa81146R6
Вот ему понадобился вектор типов Vec (bool × U₀) three, но он, конечно, получил ошибку, потому там был «Vec (A : U) : ℕ → U», а «bool × U₀ : U₁». Чтобы исправить положение, он меняет «A : U» на «A : U₁», и получает очередную ошибку, потому что справа в определении Vec терм не в U₀. Даже не понимая, что а) вектор типов сам должен лежать в U₁, б) ℕ-iter принимает аргументы из другого универсума, он просто включает «option girard true», которое выключает различение универсумов (а также позволяет доказать ложь).

https://github.com/groupoid/anders/commit/07aaa7ce1ee975f4d755914c0901f28a8506d9b0
Вот он пытается изобрести комонадическую модальность, не понимая, что такие модальности «require changes to the judgements of the type theory» (то есть замки; о чём в статье, ссылку на которую он сам же оставил, и написано). Его «♯ A» просто эквивалентнен A.

https://github.com/groupoid/CCHM/blob/40a6e91e8e5240653b2cbb282406cfdab84f99f3/src/real.ctt#L115-L116
Вот ещё одна попытка определить комонадическую модальность. То есть это не случайность какая-то, он этот конкретный момент совсем не понимает.

https://github.com/groupoid/anders/commit/993919ad3abe82ac1d0756bac18785dcda151723
Вот он ломает собственный прувер.

https://github.com/groupoid/anders/commit/b842e71e24a32d30409641434523f60650203430
А вот он его героически чинит.

https://github.com/groupoid/anders/blob/66c592c6246da96c5f32581460142b057425faaf/lib/mathematics/categories/cartesian.anders#L10-L16
А вот как у него определения декартово замкнутая категория: стрелки есть, никаких условий на них нет.

https://github.com/groupoid/CCHM/blob/40a6e91e8e5240653b2cbb282406cfdab84f99f3/src/category.ctt#L124
Вот от не может отличить универсум от одноэлементного типа и дописывает его в конец структуры. Получается, конечно, крайне проблемное определение.

А вот ещё занимательная дискуссия с участием нашего героя: https://gist.github.com/effectfully/2e23858032b8d5dd6ca2d65d0bd7c133
67 112950
>>2948
https://github.com/groupoid/anders/commit/91bc9537b1b19ef7f539f5afa67ede207690c24a#diff-325adff688f303388bbc224312d23307967c735971ccbc5627237b256fa81146R6
Вот ему понадобился вектор типов Vec (bool × U₀) three, но он, конечно, получил ошибку, потому там был «Vec (A : U) : ℕ → U», а «bool × U₀ : U₁». Чтобы исправить положение, он меняет «A : U» на «A : U₁», и получает очередную ошибку, потому что справа в определении Vec терм не в U₀. Даже не понимая, что а) вектор типов сам должен лежать в U₁, б) ℕ-iter принимает аргументы из другого универсума, он просто включает «option girard true», которое выключает различение универсумов (а также позволяет доказать ложь).

https://github.com/groupoid/anders/commit/07aaa7ce1ee975f4d755914c0901f28a8506d9b0
Вот он пытается изобрести комонадическую модальность, не понимая, что такие модальности «require changes to the judgements of the type theory» (то есть замки; о чём в статье, ссылку на которую он сам же оставил, и написано). Его «♯ A» просто эквивалентнен A.

https://github.com/groupoid/CCHM/blob/40a6e91e8e5240653b2cbb282406cfdab84f99f3/src/real.ctt#L115-L116
Вот ещё одна попытка определить комонадическую модальность. То есть это не случайность какая-то, он этот конкретный момент совсем не понимает.

https://github.com/groupoid/anders/commit/993919ad3abe82ac1d0756bac18785dcda151723
Вот он ломает собственный прувер.

https://github.com/groupoid/anders/commit/b842e71e24a32d30409641434523f60650203430
А вот он его героически чинит.

https://github.com/groupoid/anders/blob/66c592c6246da96c5f32581460142b057425faaf/lib/mathematics/categories/cartesian.anders#L10-L16
А вот как у него определения декартово замкнутая категория: стрелки есть, никаких условий на них нет.

https://github.com/groupoid/CCHM/blob/40a6e91e8e5240653b2cbb282406cfdab84f99f3/src/category.ctt#L124
Вот от не может отличить универсум от одноэлементного типа и дописывает его в конец структуры. Получается, конечно, крайне проблемное определение.

А вот ещё занимательная дискуссия с участием нашего героя: https://gist.github.com/effectfully/2e23858032b8d5dd6ca2d65d0bd7c133
68 112953
>>2950
А вот ещё определение окружности через пустой тип, конечно же: https://github.com/groupoid/anders/commit/447eff7b6ebd5f51a3af4d2d00aa8861d082f3f5#diff-91d9514806ff2092e37976b0bf8c79e48410ea90f57143009e962e5cf82d69ecR387
69 112954
>>2953
Ну и вот ещё несколько раз путает U с одноэлементным типом: https://github.com/groupoid/anders/blob/66c592c6246da96c5f32581460142b057425faaf/lib/mathematics/categories/abelian.anders#L11
70 112955
>>2947
Вывод / правило вывода?
71 112956
>>2955
Колмогоров — Драгалин ещё пишут «дерево вывода».
кга.png91 Кб, 686x591
72 112959
>>2956
Чекнул их "введение в матлогику", у них "дерево вывода" это "дерево формул" с доп.условием. Но поскольку в книжице по теории типов нет введения понятия формулы, а Автор постоянно используют обороты типо we express this as\they are introduced as follow, уточняя что это всё inference по inference rule которые образуют derivation. Дерево вывода оказывается более уместней, чем дерево формул без формул.
73 112960
>>2959
Вот ещё в переводе HoTT book переводчик пишет «выведение» (приложение, пункт A.2). Не самый авторитетный источник, наверное, но всё же.
https://henrychern.wordpress.com/2017/11/03/%d0%b3%d0%be%d0%bc%d0%be%d1%82%d0%be%d0%bf%d0%b8%d1%87%d0%b5%d1%81%d0%ba%d0%b0%d1%8f-%d1%82%d0%b5%d0%be%d1%80%d0%b8%d1%8f-%d1%82%d0%b8%d0%bf%d0%be%d0%b2/
74 112961
>>2960
"Выведение" хороший вариант. Звучит естественно в контексте с древом\выводом и к тому-же укладывается в одно слово.
75 112962
Где достать последние версии конспектов Вавилова? Гуглятся какие-то огрызки да ещё с такой херотенью:

wSEMYSLI, KOTORYEMOGUTPRIJTIW GOLOWUPRI^TENII DANNOJKNIGI,QWLQ@TSQINTELLEKTUALXNOJSOBSTWENNOSTX@ AWTORAIOB_EKTOMAWTORSKOGOPRAWA.iHNELICENZIROWANNOE OBDUMYWANIEZAPRE]AETSQ.
76 112963
>>2948
Бля, зачем ты саммонил хохла, поток дерьма теперь на пару тредов не остановать :С
77 112964
>>2962

> Где достать последние версии конспектов Вавилова?


Зачем тебе эта хуета? Его ШУЕ видоса чуть выше недостаточно?
>>2960
Хм, даже не знал, что HoTT book перевели. Наверное, все кто хотел, в оригинале прочитали, остались только школьники, которые не знают,как "derived" перевести.
78 112965
>>2964
Думаешь математический инфоциган сохацкий достоин моего внимания?
79 112966
>>2965

> инфоциган


Значение знаешь?

> сохацкий достоин моего внимания?


Думаю, нет, ведь ты у него даже нотацию не осилил.
80 112967
>>2966
Моя терминология предельно точна, он именно инфоциган который пиарится на хайповой теме, даже не математик а кодерок из занюханного хуторского говновузика с кафедры прикладной математики (т.е. даже ни математик ни программист).
81 112968
>>2966
Так какие там морфизмы между O_Π и O_Σ синтаксическими деревьями например?
82 112969
>>2967
Инфоциганство это не пиар на чем-то, а продажа успешного успеха в виде курсов, наставничества, гивов итп шлака. К Сохацкому можно по-разному относиться, но он не инфоциган, это факт.
83 112970
>>2969
Так он свою псевдонаучную хуергу продаёт под видом математики. Просто аудитория специфическая, но сути это не меняет.
84 112973
>>2966
Нотацию не осилил только ты, раз не можешь там стрелку увидеть.
85 112974
>>2969
Так он же успех и наставничество и продаёт. Ты его ТОПОВОГО ПРОГОММИСТА видел? А ведь ему донатили (и, вероятно, всё ещё донатят) за такое.
86 112976
>>2970

> Так он свою псевдонаучную хуергу продаё


Где он что-то продает, поридж? Все бесплатно на гитхабе.
>>2973

> Нотацию не осилил только ты,


Кринжуй отсюда, школотрон.
87 112977
>>2976
Слышь ты, хуило гуманитарное, нахуй пошёл, а?
17076319488080.jpg165 Кб, 1000x1000
88 112978
>>2977

> Слышь ты, хуило гуманитарное, нахуй пошёл, а?

grafik.png25 Кб, 464x305
89 112979
>>2978
Хули ты боевыми картиночками кидаешься, уёбище? Где построение стрелки?
сохацкий0.jpg305 Кб, 1000x1000
90 112980
>>2979

>Хули ты боевыми картиночками кидаешься, уёбище? Где построение стрелки?

91 112981
>>2980
Обпучкался с пикчи.
92 112982
>>2980
Неплохо.
93 112983
>>2979
Ты дееспособный вообще? Весь код есть в anders, там смотри. Если нотацию осилишь, что маловероятно.
94 112984
>>2983
Я этот Anders писал, так что получше тебя знаю, где какой там код. Этой конкретной стрелки там нет.
95 112985
>>2976

>Где он что-то продает, поридж? Все бесплатно на гитхабе.


Ты совсем чтоли дебил? Себя продает, свои высеры.
96 112986
Лол, конструктивный петух снова схватился за боевые картиночки.
97 112987
>>2984

> Я этот Anders писал,


Пруфанешь?

> Этой конкретной стрелки там нет.


Из PTS в MLTT 72? Хуевый ты писатель значит.
>>2985

> Себя продает, свои высеры.


Пока что только тебя продал, вон как трясешься.
98 112990
>>2987

>Из PTS в MLTT 72? Хуевый ты писатель значит.


Даже мимокроку уже понятно, что тебе говорят про стрелку из синтаксического дерева O_Π в синтаксическое дерево O_Σ.
17005685875290.jpg133 Кб, 919x750
99 112991
>>2990
Тебе само название "спектральная категория формальных мов" о чем-нибудь говорит? Стрелки там между формальными языками. О чем там прямо написано в определениях из главы 2.3. В общем, я тебя услышал, скибидитуалетикс, теперь уебывай
100 112992
>>2991

>Тебе само название "спектральная категория формальных мов" о чем-нибудь говорит?



Очевидно она говорит что автор "мов" сказочный долбоёб наципятак которому во время не дали таблеток.
101 112996
>>2992
Ты даже нотацию не осилил. Но долбаебом называешь не себя, что было бы правдой, а кого-то другого. Типичный пердеж
grafik.png20 Кб, 835x133
102 112997
>>2987

>Пруфанешь?


Оставляй фейкопочту.

>Из PTS в MLTT 72?


Из O_Π в O_Σ, ну ёпт.

>Хуевый ты писатель значит.


Я-то тут причём вообще? Я прувер писал, а не диссер Сохацкому и/или его формализацию; о наличии той или иной формализации в репозитории я могу говорить, поскольку сам прувер, стандартная библиотека к нему, а также кое-какой код Сохацкого, включая обрывочные формализации диссера, находятся в одном репозитории.
Сохацкий вообще эту, кхм, монографию о категорії формальних мов начал писать ещё до начала любых работ над Anders.

>>2991
Вообще-то речь о послідовності синтаксичних дерев (смотрим на пик), которая генерує послідовність мов, и стрелки в обсуждаемом фрагменте между деревьями/синтаксисами.
103 113002
>>2997

>Оставляй фейкопочту.


constuct_coc^K2kANUSgmB.IailPUNCTUMcoT,Tm
104 113007
>>2997

>Оставляй фейкопочту.


Cuckhole_tow+JmpaANUShueLc8vPUNCTUMuIXfa
17069317318280.jpg68 Кб, 604x417
105 113010
106 113011
>>3002
>>3007
Проиграл.
107 113012
>>2997

> Из O_Π в O_Σ, ну ёпт.


> Вообще-то речь о послідовності синтаксичних дерев (смотрим на пик), которая генерує послідовність мов, и стрелки в обсуждаемом фрагменте между деревьями/синтаксисами.


А где там в тексте прямо написано, что между индуктивными типами именно морфизмы в категорном смысле, а не просто отношение следования?
grafik.png71 Кб, 744x360
108 113013
>>3012

>что между индуктивными типами


Между синтаксическими деревьями.

>не просто отношение следования?


То есть в одном и том же предложении одно и то же слово означает разные вещи? Детские отговорки, см. >>2946
109 113014
>>3013

> То есть в одном и том же предложении одно и то же слово означает разные вещи?


Спектральная категория формальных мов прямо заявлена, а спектральная категория индуктивных типов - нет.

> Между синтаксическими деревьями.


То есть, индуктивными типами, см. визначення 23 и 24.
110 113015
>>3014

>а спектральная категория индуктивных типов - нет.


И стрелок между ними совсем нет, да?

>То есть, индуктивными типами, см. визначення 23 и 24.


Так это не любые индуктивные типы.
111 113016
>>3015

> И стрелок между ними совсем нет, да?


Так где там написано, что стрелки между индуктивными типами это морфизмы?
112 113017
>>3016
Издеваешься что ли?
113 113018
>>3017
То есть, ты не рассматриваешь вариант, что это просто стрелочные типы функций в пределах одной мовы, содержащей эти типы?
114 113019
>>3018
То есть функции в cubicaltt? Заготовка выше.
115 113020
>>3010
Это anal beads твоей мамаши? Зачем ты сюда его притащил, довен?
17062476569270.jpg138 Кб, 592x532
116 113022
>>3020

> Это anal beads твоей мамаши? Зачем ты сюда его притащил, довен?

117 113024
>>2865 (OP)

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



Зайдём с другого конца. Предположим это так, тогда на каком основании ты используешь абстракцию которую не принял как аксиому (у тебя ебанька по твоим же слоам есть только несколько конкретных примеров, тебе кто разрешал переходить к следующему примеру и т.д)? И тем более опираться на метаязык при обосновании понятий объектного языка если он вторичен? Ты ебанько задним числом математематические понятия определяешь чтоли?
118 113025
>>3024

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


N-петух, какой еще "переход к следующему примеру"? Аксиомы Пеано это и есть пример, содержащий абстракцию потенциальной бесконечности.
119 113028
Конструктивный петух... опять срёт итт картинками с зумерами.
16937118393800.mp4386 Кб, mp4,
764x720, 0:03
120 113031
121 113035
>>3025
Мовный газнюх, ты в своих газах запутался или что? Сам же предлагал обосновать абстракцию (которая вторична) фиксированной серией примеров (которые в понимании твоего пропитанного газами мозга первичны). Вот тебе и вопрос, как ты ебло на одних примерах собрался с потенциально неограниченными структурами работать? Ты это технически не можешь сделать т.к. еще не ввёл "вторичную" абстракцию. Про Пеано в очередной раз в лужу пёрнул - аксиомы сами собой ничего не обосновывают, они работают только если принята абстракция потенциальной осуществимости.
122 113039
>>3035
Что ты трясёшься, у тебя синдром Туретта?

> аксиомы сами собой ничего не обосновывают, они работают только если принята абстракция потенциальной осуществимости.


Абстракция потенциальной осуществимости - это свойство аксиом Пеано и других подобных аксиоматик, правил построения итд. Это следует из самого определения абстракции, она не висит в воздухе, а вторична по отношению к конкретным примерам, имеющим это свойство. Тут вообще не о чем спорить итд, это элементарные вещи.
123 113041
>>3039

>Что ты трясёшься, у тебя синдром Туретта?


Трясу яичками по лбу твоей мамаши.

> Абстракция потенциальной осуществимости - это свойство аксиом Пеано и других подобных аксиоматик, правил построения итд. Это следует из самого определения абстракции, она не висит в воздухе, а вторична по отношению к конкретным примерам, имеющим это свойство. Тут вообще не о чем спорить итд, это элементарные вещи.



Ты через "вторичность" пытался отрицать что абстракция потенциальной осуществимости принимается как исходное неопределяемое понятие, теперь ты говоришь что всегда её предполагал (таблетки помогли?).
При её наличии натуральное число это базовый объект плюс абстракция, определение аксиомами Пеано использует ту же базу только более сложное, а поэтому нинужно. Ты или более простое определение принеси или признай себя петухом коим ты являешься.
124 113043
>>3041
Перечитай ещё раз оп-пост, я там все изложил, и к этому нечего добавить ни мне, ни тебе. Абстракция не может быть "исходным неопределяемым понятием", у этого термина есть общепринятое определение. Натуральное число это никакой не "базовый объект", это элемент множества. Считаю этот вопрос закрытым.
127 113049
>>3043

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


Там шизофазия написана, как и вся твоя писанина.

> Абстракция не может быть "исходным неопределяемым понятием"


Опять таблетки кончились, шиз? Абстракция всегда неопределяемое понятие, т.к. не сводится к элементарным вещами иначе бы это было бы обычное определение.

>Натуральное число это никакой не "базовый объект", это элемент множества.


Базовый объект это единица, а всё множество формируется из 1 на основе абстракции потенциальной осущетвимости. Аксиоматика Пеано лишь постфактум описывает построенный таким образом объект, сама по себе она ничего не определяет. Ну и как уже говорилось в принципе не может определять т.к. даже в своей формулировке опирается на абстракцию потенциальной осуществимости в метаязыке.

>Считаю этот вопрос закрытым.


Ты своё безпруфное мнение лечащим врачам изливай, всем остальным на него похую. Ты или доказательство давай или корректное определение без скрытых замкнутых кругов и прочих логических ошибок которые в твоём пиздедже на каждом шагу.
128 113050
>>3049
А давай-ка ты источники своей шизы приведешь. И нет, той статейкой Успенского на одностраничном сайтике типа укоз ру можешь подтереться. Конкретно:

> Абстракция всегда неопределяемое понятие,


> Базовый объект это единица, а всё множество формируется из 1 на основе абстракции потенциальной осущетвимости. Аксиоматика Пеано лишь постфактум описывает построенный таким образом объект


Где это написано? Если это хуйня из головы, так и пиши. Я приводил общепринятые определения понятия абстракции и метаязыка. Теперь ты давай пруфы, что твоя писанина это не шиза совкового скуфидона, а принятые в математике вещи.
а.png333 Кб, 781x794
129 113051
Вумные мысли о N
130 113052
>>3050

Источник не мой, а твой. Просто ты читать не умеешь, копипастишь рандомные фрагменты не понимая что за ними стоит, зачем они вводятся и что (и при каких условиях) определяют.

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

Ещё про это писали как минимум Пуанкаре и Кронекер, но ты хуйло пиздливое специально как баран упёрся в одного Успенского в попытках съехать на дебильных шуточках (типа гыгы, совок успенский чета спизданул).

>Где это написано? Если это хуйня из головы, так и пиши. Я приводил общепринятые определения понятия абстракции и метаязыка.



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

Хуйня из больной головы это мовная шизофазия твоего протыка уёбка сохацкого.

>Теперь


Ты не одного пруфа не показал, какое блять "теперь"? Хоть за одно своё слово ответь, мразь тупая. Ты же спиздянул якобы аксиомы Пеано что-то там определяют, вот и тащи доказательства, как.

>ты давай пруфы, что твоя писанина это не шиза совкового скуфидона, а принятые в математике вещи.


Пруфы тебе даны неоднократно: 1) аксиомы Пеано формулируются как конкретная формальная система, любая ФС необходимо использует абстракцию потенциальной осуществимости. 2) Для доказательства существования множества удовлетворяющего этим аксиомам ты опять вынужден ссылаться на абстракцию осуществимости когда доберешься до аксиомы индукции.
131 113053
>>3052

> Ещё про это писали как минимум Пуанкаре и Кронекер,


Цитаты.

> Везде,


Ссылки где?

> Пруфы тебе даны неоднократно:


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

> любая ФС необходимо использует абстракцию потенциальной осуществимости.


Неси цитаты, где ты это взял.

> 2) Для доказательства существования множества удовлетворяющего этим аксиомам ты опять вынужден ссылаться на абстракцию осуществимости когда доберешься до аксиомы индукции.


Это не пруфы, а "твое мнение". Абстракция потенциальной осуществимости это свойство, а не какая-то высшая истина, существующая вне примеров, содержащих её. По первой же ссылке в Википедии:

> https://ru.m.wikipedia.org/wiki/%D0%90%D0%B1%D1%81%D1%82%D1%80%D0%B0%D0%BA%D1%86%D0%B8%D1%8F



> Абстра́кция (лат. abstractio «отвлечение»[1]) — процесс отвлечения (абстрагирования) от тех или иных характеристик объекта для их избирательного анализа;



> обобщающая абстракция — даёт обобщённую картину явления, отвлечённую от частных отклонений. В результате такой абстракции выделяется общее свойство исследуемых объектов или явлений. Данный вид абстракции считается основным в математике и математической логике.


Нигде нет хуйни о том, что абстракция это какое-то "неопределяемое понятие", к которому нужно возноситься в молитве для определения чего-то, содержащего абстрагируемое свойство. Один из таких примеров - аксиомы Пеано.
132 113054

> Thus, intuitionistically, truth is identified with provability, though of course not (because of Godel's incompleteness theorem) with derivability within any particular formal system.


Так как МЛ тогда предлагает доказать что-либо если не в формальной системе? Уверовать?
17042528441170.png208 Кб, 968x733
133 113055
>>3054

> поридж начинает подозревать, что конструктивизм чем-то неуловимо отличается от формализма, но вот чем? Сможет ли пердикс понять, в чем тут дело и почему интуиционизм со времён Брауэра рассматривался как отдельное направление в основаниях, а не как часть формализма? Продолжаем зоонаблюдения

image.png4 Кб, 81x433
134 113057
>>3055

>почему интуиционизм со времён Брауэра рассматривался как отдельное направление в основаниях, а не как часть формализма


Что бы не осквернять шизой в принципе вменяемую программу формализации математики?
17059089050160.mp4195 Кб, mp4,
388x360, 0:03
135 113058
>>3057

> поридж зачем-то полез читать Мартин-Лефа, не осилил и порвался

136 113059
>>3058
Я читал Сохацкого в подлиннике.
137 113060
>>3054
Результаты, связанные с нашей способностью осуществлять конструктивные процессы, в математике часто формулируются в виде теорем существования, утверждающих существование объектов, удовлетворяющих таким-то требованиям.

В конструктивной математике под этим подразумевается, что построение таких объектов потенциально осуществимо, т, е.что мы владеем способом их построения.

Это конструктивное понимание теорем существования расходится с тем, как их понимают в классической математике. Правда, „классики" не любят объяснять свое понимание таких теорем. Однако из того, как они обходятся со словом «существует», следует, что их понимание этого слова отлично от конструктивного. Они, например, считают возможным утверждать, существование конструктивного объекта, удовлетворяющего данному требованию, уже тогда, когда им удается путем «приведения к нелепости» опровергнуть предположение о том, что ни один объект не удовлетворяет этому требованию. Способ построения искомого объекта может при этом и небыть известен. Таким образом, конструктивное понимание высказываний о существовании отлично от классического.
138 113061
>>3060
Что значит "потенциально осуществимо"? Поясните плиз.
139 113062
>>3061
Абстракция потенциальной осуществимости позволяет нам рассуждать о сколь угодно длинных конструктивных процессах и сколь угодно больших конструктивных объектах. Их осуществимость потенциальна: они были бы осуществимы практически, располагай мы достаточными пространством, временем и материалом.

Абстракция потенциальной осуществимости, как и всякая абстракция, вносит туда, куда она привлекается, элемент фантазии. Он неизбежно присутствует во всякой абстрактной науке, в том числе и в математике. Классическая математика привлекает абстракции, идущие гораздо дальше абстракций конструктивной математики. В частности, она пользуется абстракцией актуальной бесконечности, т. е. позволяет себе рассуждать о „бесконечных множествах" как о законченных неконструктивных „объектах". Различие между „классиками" и„конструктивистами" состоит в том, что они привлекают раз-разные абстракции, т. е. фантазируют по-разному.
140 113063
>>3062
А что такое конструктивный процесс, и вообще процесс?
141 113064
>>3055
Конструктух, срыгос оформи.
>>3060
Не вижу ответа на вопрос. Да и к написанному есть вопросики. Источник?
17076921965340.png187 Кб, 273x392
143 113067
>>3064

> Да и к написанному есть вопросики.


Вопросики у него есть, а. Вейп вытащи из жопы, или что ты туда засовываешь, потом хотя бы пару статей из Википедии осиль вместо тиктака. Откуда вы сюда лезете такие?
144 113068
>>3067
Еще раз - ебало свое завальцуй, петушара.
145 113069
>>3067
Мовный петух получает образование на википедии, лул.
Шо, у вас на хуторе универы и книжки не завезли?
146 113070
формализм крута
17083914678490.webp55 Кб, 900x1200
147 113072
>>3069
Ты для начала хоть Википедию бы осилил уже что-то. А то будешь как N петух, даже простейшего определения абстракции не осилил, зато лезет спорить.
>>3068

> Еще раз - ебало свое завальцуй, петушара.


А то что, чепуха? Возьми вот антистресс, не трясись, ребенок.
148 113074
>>3072
Сколько дашь за сэкс с Сохацким?
149 113075
Можем договориться :)
150 113081
>>3074
-1/12
151 113082
кто против конструктивизма, тот петух
кто за конструктивизм, тот петух
все остальные — конструктивисты
image.png256 Кб, 1291x2123
152 113083
>>3049

>Базовый объект это единица, а всё множество формируется из 1 на основе абстракции потенциальной осущетвимости. Аксиоматика Пеано лишь постфактум описывает построенный таким образом объект, сама по себе она ничего не определяет.


Аксиоматика Пеано содержится в его труде Arithmetices principia, nova methodo exposita, его перевод на английский язык приведен в книге Selected works of Giuseppe Peano translated from the Italian (https://www.pdfdrive.com/selected-works-of-giuseppe-peano-translated-from-the-italian-e186125668.html ).
Похоже, что АП как раз-таки определяет "свойство быть числом". О бесконечности речи не идет. И если бы речь о бесконечности заходила, то бесконечность была бы актуальной. То есть существуют такие объекты, как числа, а их свойства описаны конечным набором конечных схем.

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


Имеется в виду возможность рассмотрения сколь угодно длинных формул? Почему бы вместо формул не рассматривать сам конечный набор конечных схем (схем правильно построенных формул), а получаемые из них формулы - считать лишь вспомогательными средствами некоего отдельного метода исследования схем? И конечно же верно, что никто никогда не может рассмотреть слишком большой набор формул, а тем более бесконечный, иначе как найдя абстрактный подход через рассмотрение вместо них заключающего их множества. Множества точно так же описываются конечным набором конечных схем. Нарушается ли финитизм где-либо в ходе таких исследований?
153 113085
>>3083
Проблема N петуха в том, что он не осилил определения абстракции и метаязыка в принципе. Конкретно, тот факт, что эти явления вторичны по отношению к примерам, содержащим абстрагируемое свойство и обьектному языку соответственно. Он не понимает, что абстракция не может существовать сама по себе, вне примеров, содержащих её, а метаязык может быть только надстройкой над объектным языком. Все это описано буквально на каждом углу, начиная с Википедии, однако же у N петуха какое-то "свое" (на самом деле взятое у Успенского) понимание абстракции и метаязыка. Учитывая, что там ШУЕ уровня Рыбникова и "основ православной арифметики", имеем что имеем - долбаеб вместо того чтобы хотя бы ПОПЫТаться разобраться в вопросе, с 2015(!) года серит шизой, что оказывается, аксиомы Пеано якобы не определяют множество натуральных чисел. Короче говоря, спорить там бесполезно, всё что можно сделать - тыкать дауна в общепринятые (а не ШУЕшные) определения абстракции и метаязыка.
154 113087
>>3085

>не осилил определения абстракции и метаязыка


>метаязык может быть только надстройкой над объектным языком


Конструшок, как тебе удается обосраться даже в совершенно очевидных понятиях и перевернуть их с ног на голову? То универсальная машина Тьюринга у тебя это обобщение МТ вообще, то вот этот бред.
155 113088
>>3087
Я так понимаю, возражений по существу нет? Или дальше будешь игнорировать общепринятые определения абстракции и метаязыка? Абстракция это свойство примеров, собственно и содержащих абстрагируемое свойство. Будешь с этим спорить? Зачем?
156 113089
>>3088
Какое понятие более общее - МТ или УМТ?
157 113090
>>3087

> Метаязы́к — язык, предназначенный для описания другого языка, называемого объектным языком


https://ru.m.wikipedia.org/wiki/%D0%9C%D0%B5%D1%82%D0%B0%D1%8F%D0%B7%D1%8B%D0%BA
Вот так просто, N петух. Нет объектного языка - нет и метаязыка для его описания.
158 113091
>>3089

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


https://ru.m.wikipedia.org/wiki/%D0%A3%D0%BD%D0%B8%D0%B2%D0%B5%D1%80%D1%81%D0%B0%D0%BB%D1%8C%D0%BD%D0%B0%D1%8F_%D0%BC%D0%B0%D1%88%D0%B8%D0%BD%D0%B0_%D0%A2%D1%8C%D1%8E%D1%80%D0%B8%D0%BD%D0%B3%D0%B0#:~:text=%D0%A3%D0%BD%D0%B8%D0%B2%D0%B5%D1%80%D1%81%D0%B0%D0%BB%D1%8C%D0%BD%D0%BE%D0%B9%20%D0%BC%D0%B0%D1%88%D0%B8%D0%BD%D0%BE%D0%B9%20%D0%A2%D1%8C%D1%8E%CC%81%D1%80%D0%B8%D0%BD%D0%B3%D0%B0%20%D0%BD%D0%B0%D0%B7%D1%8B%D0%B2%D0%B0%D1%8E%D1%82%20%D0%BC%D0%B0%D1%88%D0%B8%D0%BD%D1%83,%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC%D0%B0%20%D0%B1%D1%8B%D0%BB%D0%B0%20%D0%B4%D0%B0%D0%BD%D0%B0%20%D0%BD%D0%B0%20%D0%B2%D1%85%D0%BE%D0%B4.
159 113092
Срочно таблеток мовному петуху, он щас весь тред википедией засрет.
160 113093
>>3091
Петух, отвечай прямо, не виляй хвостиком.
161 113094
>>3093
А ты читать разучился, N петух? Универсальная потому так и называется, что способна заменить любой конкретный пример машины Тьюринга. Что сказать-то хотел?
162 113095
Не совсем понял маневр N петуха в сторону машины Тьюринга. С аксиомами Пеано, абстракцией и метаязыком обосрался, теперь хочешь с машинами Тьюринга обосраться?
163 113096
>>3094
Но я тебя не спрашивал кто кого может заменить, а

>Какое понятие более общее


Я вообще ору. Как с таким уровнем понимания чего либо ты можешь листать своего Браузера с Мартином-Лефом и искренне считать что ты чего то там понимаешь?
У тебя может пизда между ног, и ты на самом деле не петух и курица? Просто такой уровень отсутствия логического мышления у человека за гранью моего понимания.
>>3095
Просто проходил мимо, решил погонять тупого петуха по старым темам.
17083914678490.webp55 Кб, 900x1200
164 113097
>>3096

> Просто проходил мимо, решил погонять тупого петуха по старым темам.


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

> Но я тебя не спрашивал кто кого может заменить, а


> >Какое понятие более общее


То есть, само понятие "универсальная" тебе ни о чем не говорит? Хорошо, Я тебя услышал. Универсальная машина Тьюринга - более общая потому что может заменить любой частный случай. Я на твой вопрос ответил?
165 113098
>>3097

>Универсальная машина Тьюринга - более общая потому что может заменить любой частный случай. Я на твой вопрос ответил?


Ну ответить ты ответил. Но пиздец, конечно, что теперь с этим делать непонятно...
Какое понятие более общее - "автомобиль" или "зеленый автомобиль"?
166 113099
Провёл бесконечностью конструктивному петух по губам...
funeralcoach.jpg23 Кб, 350x303
167 113100
>>3099
[облизывается]

конструктивный петух
свин.png1 Мб, 900x900
168 113104
>>3100

>прикл


Напомнило...
169 113139

>The problem of too many equalities in HoTT can be understood as a problem of underspecification of the mathematical objects. N and Z as sets are isomorphic but are not if we consider them as monoids with usual addition. So, monoid of N is really the data of N together with structure and property of a monoid, which cannot be canonically isomorphic to the Z monoid.


Что скажете?
170 113140
>>3139
Тоже что и всегда, HOTT даже N не может определить, кому нужно такое "основание"? А всё остальное и в теории множеств нормально сидит.
171 113141
>>3140

> HOTT даже N не может определить,


N петух, в HoTT N определено. По абстракции потенциальной бесконечности тебя уже сто раз еблом ткнули в определение абстракции - это свойство примеров, а не наоборот.
grafik.png141 Кб, 1207x692
172 113142
>>3140
В смысле?
173 113143
>>3142
define succ
174 113144
>>3143

> define succ


N петух, это отношение следования. Абстракция потенциальной бесконечности это свойство succ, но не наоборот.
175 113145
>>3143
Вон же правило вывода, что ещё надо-то?
176 113154
>>3145
А потом спрашиваешь у анонов откуда берется инъективность конструкторов и они начинают что-то невнятно блеять про теорию категорий прикрываясь первым попавшимся пейпером по coic. Тру стори.
177 113162
>>3154
В то, что ты Сохацкому понаписал в андерс хуйни без половины морфизмов, мы поверим. Ну, почти. Но к HoTT какие претензии? Ее поумнее тебя писали, там даже Мартин-Леф в соавторах. Чего ты там ниспровергать собрался?
178 113163
>>3162
Конструктух, ты? Ты с зелеными автомобилями разобрался?
179 113164
>>3163

> Ты с зелеными автомобилями разобрался?


Нахуй путешествуй, опущ
180 113165
>>3164
Петух, ты что тупее дошкольника? Вот это хохма.
17005685875290.jpg133 Кб, 919x750
181 113166
>>3165

> Петух, ты что тупее дошкольника?


Тупее тебя нет никого. Уебывай и свои задачки для коррекционной группы детского сада забирай. Чё вас деградантов так сюда тянет? В другом месте пердежируй, аниме
182 113167
>>3166
Ору с убогого. Петух не справился со школьной программой, это известно. Теперь взят новый уровень - вопросы для дошколят оказывается петуху тоже не по зубам. Что дальше? Попытка вырабатывать условные рефлексы? Кто умнее конструктивный петух или обезьяна?
17059611102960.png127 Кб, 627x598
183 113168
>>3167

> чморидж обосрался с универсальной машиной Тьюринга, теперь кукарекает на самоподдуве, пытаясь закукарекать свой обсер


Не стыдно тебе таким дебилом быть?
184 113169
>>3168
Потешный не может ответить на вопрос для дошкольника, но уверен что обосрался не он. Какая форма неполноценности у тебя?
185 113171
>>3169

>Какая форма неполноценности у тебя?


Конструктивизм в затяжной стадии. С каждым годом его интеллект всё падает и падает. В первых тредах, он ещё пытался что-то аргументировать и аватарил Брауэрем. Теперь он уже не пытается и просто срёт картинками с зумерами.
186 113172
>>3154
Инъективность можно получить из построения односторонней обратной или, например, возможности элиминировать в универсум повыше. Почти все, кто с DTT знаком, в курсе, но причём тут инъективность вообще?
187 113173
>>3162
Кто ты-то? Ты вообще не тому анону про андерс пишешь. Разберись уже, кто кому что писал, что такое этот самый Anders и какое он имеет отношение к текстам Сохацкого.
188 113183
>>3172
Конкретно меня интересует почему 0≠1. Потому что в аксиомах Пеано это постулируется явно, а в MLTT берется хуй знает откуда. Несколько тредов в прошлом задавал этот вопрос и получал только дрист под себя от конструктивного петуха. Потом случайно наткнулся на то что для доказательства этого факта необходим универсум.
Это все при том, что coic очень сложная система и правила ее хуй где нормально описаны. Об этом еще Воеводский говорил.
189 113186
>>3183

>Конкретно меня интересует почему 0≠1.


Конкретно «0 ≠ 1» вроде как называется дизъюнктивностью конструкторов, под инъективностью понимают стандартную инъективность (то есть succ(n) = succ(m) → n = m). Впрочем, это вопросы названий, конечно.

>Потому что в аксиомах Пеано это постулируется явно, а в MLTT берется хуй знает откуда. Несколько тредов в прошлом задавал этот вопрос и получал только дрист под себя от конструктивного петуха. Потом случайно наткнулся на то что для доказательства этого факта необходим универсум.


Да, нужен универсум. Стандартный аргумент такой: мы строим функцию f из ℕ в универсум U такую, что f(0) ≡ 𝟏 (одноэлементный тип), а f(succ(n)) ≡ 𝟎 (пользуясь частным случаем индукции). Теперь если у нас есть 0 = 1, то и 𝟏 ≡ f(0) = f(1) ≡ 𝟎. Потом нужно ещё применить индукцию для равенства, чтобы из 𝟏 = 𝟎 получить функцию 𝟏 → 𝟎. Ну а 𝟏 населён, откуда мы получаем элемент типа 𝟎. Сводя всё вместе, получаем импликацию 0 = 1 → 𝟎, что и есть отрицание равенства, по стандартному определению.
Вот тут ещё пишут, что без универсума «0 ≠ 1» в MLTT не выводится: https://proofassistants.stackexchange.com/a/2626/310
190 113187
>>3186
𝟎 — пустой тип.
забыл написать
191 113188
>>3186

>дизъюнктивностью конструкторов, под инъективностью


Не спорю, но еще хотелось бы термин объединяющий эти два свойства. Особенно забавным мне кажется то что в coic это свойство подается чуть ли не как само-собой разумеющееся, в то время как в большинстве языков программирования (не функциональных) конструктор конструирует что угодно и как угодно.
Видел это доказательство, но все равно оно какой то странный привкус оставляет. Подозрительно что прувер до всего этого додумывается автоматически.

>it is well-known that Martin-Löf type theory without univeres does not prove 0≠1.


И теперь мне стало интересно кто и как это доказал. Вроде где-то видел строятся модели для этого соответствующие.
grafik.png28 Кб, 572x221
192 113189
>>3188

>конструктор конструирует что угодно и как угодно


Просто один и тот же термин (конструктор) в ООП и теориях типов используют для разных понятий.

>Подозрительно что прувер до всего этого додумывается автоматически.


Неудивительно, тактики как раз под такие стандартные случаи и забиты. А подозревать не в чем, например, в Lean тактики генерируют термы отдельно от ядра, ядро же проверяет только то, что тактика сгенерировала. То есть пруф от кривой тактики принят не будет. Можно даже посмотреть, какой конкретно пруф тактика сгенерировала (пик).

>И теперь мне стало интересно кто и как это доказал. Вроде где-то видел строятся модели для этого соответствующие.


Вот нагуглилось что-то: https://www.cse.chalmers.se/~smith/JSLPeano.pdf
Аннотация 2024-02-25 171304.png511 Кб, 1306x532
193 113190
Тут недавно выкладывали ссылку на русский перевод HoTT book. Пикрил просто первое, что бросилось в глаза, сколько там подобной параши, неизвестно. Смысла читать этот перевод, конечно же, нет.
166316825242-mykaleidoscope-ru-p-zloi-patrik-krasivo-43.jpg44 Кб, 900x900
194 113191
>>3190
Там вместо "означает" должно быть "увтерждает" как во втором примере суждения или чо?
grafik.png58 Кб, 1152x222
195 113193
>>3191
Терм a имеет тип A / терм a населяет тип A / терм a является элементом типа A.
Опечатки в переводе, вот это пиздос, да, никогда такого не было.
196 113194
>>3193
Хм. Пока ты явно не указал, я и не заметил что там элемент является типом. Видать у меня реально низкий айкю.
197 113195
>>3190

>Тут недавно выкладывали ссылку на русский перевод HoTT book


кому-то заняться совсем нечем?
Screenshot-756.png9 Кб, 513x212
198 113197
>>3189
Спасибо, почитаю.

Вот предельно упрощенный терм на coq который доказывает тезис. Осталось только его осмыслить как следует.

Почему используешь lean? Да еще на немецком, кек.
199 113198
>>3197

>Почему используешь lean?


Синтаксис приятнее (чем в Agda/Coq) кажется, метапрограммирование отличное и плагины проверяют код на лету.

>Да еще на немецком, кек.


Системная локаль.
200 113199
>>3139

>>The problem of too many equalities in HoTT can be understood as a problem of underspecification of the mathematical objects. N and Z as sets are isomorphic but are not if we consider them as monoids with usual addition. So, monoid of N is really the data of N together with structure and property of a monoid, which cannot be canonically isomorphic to the Z monoid.


>Что скажете?


Я не знаю особенности HoTT, но мне интересно ответить и оживить доску.
Буду считать, что цитата использует HoTT как обозначение математической теории, в которой интерпретируемы теория множеств и арифметики N и Z. То есть HoTT - особая основная теория, выступающая в основании математики и обосновывающая многие другие ее теории.
Далее, о чем идет речь?

>The problem of too many equalities in HoTT


Присутствуют отношения равенства, различающиеся между собой, что ли?

>N and Z as sets are isomorphic but are not if we consider them as monoids with usual addition


Мол, по одному изоморфизму они изоморфны, а по другому - нет?

>So, monoid of N is really the data of N together with structure and property of a monoid, which cannot be canonically isomorphic to the Z monoid.


(Будем считать, что речь идет об аддитивном моноиде.) Так ведь, насколько я понимаю, это полностью соответствует обычным результатам конвенциональной математики. В Z: a = a + (1 + [-1]). Тогда для любого f, если f - биекция из Z в N: f1 != f(-1), значит один из них ненулевой, и тогда fa != fa + f1 + f(-1), то есть никакая биекция f не является гомоморфизмом.
201 113200
>>3199

>Присутствуют отношения равенства, различающиеся между собой, что ли?


Да, как разные изоморфизмы.

>Мол, по одному изоморфизму они изоморфны, а по другому - нет?


Типы (ℕ и ℤ) изоморфны, структуры (то есть n-ки, тип + операция + свойства) над ними — уже нет.
202 113201
>>3199

>Я не знаю особенности HoTT


Может тогда не стоит отвечать?

HoTT (по видимому) предлагает считать N и Z тождественными понятиями, что противоречит интуиции и устоявшейся практике.
203 113202
>>3189
Странно он пишет

> Intuitively, φ(A) =⊤ means that the interpretation of the type A is a set with one element and φ(A) =⊥ means that A is interpreted as the empty set.


а потом

> φ(Eq(A, a, b)) = φ(A)


Но населенность равенства очевидно должна зависеть от того что сравнивается. Продолжу наблюдения.
204 113203
>>3202
В этой интерпретации любой тип либо пустой, либо одноэлементный.
В одноэлементном типе все элементы равны, причём одним образом (даже в HoTT), поэтому равенство там всегда, вне зависимости от a и b, — одноэлементный тип.
А в пустом типе чтобы Eq(A, a, b) просто построить, нужно найти a/b в нём, то есть его естественно интерпретировать как пустой тип.
То есть как раз φ(Eq(A, a, b)) = φ(A).
205 113229
Шел 2024 год, но определения пучка в HoTT так и не дали.
206 113230
>>3203

>причём одним образом (даже в HoTT)


А он и может быть только одним образом. Это чисто в HoTT придумали, что якобы может быть не одним образом.
207 113231
>>3230
Да нет, понятие равенства задолго до HoTT вызывало много вопросов. Это просто ты кроме тиктака ничего не знаешь.
xeYy9FFRso8.jpg126 Кб, 640x640
208 113232
>>3231

>понятие равенства задолго до HoTT вызывало много вопросов

210 113249
>>3233

>А давайте придумаем модель, где желаемое является действительным? А давайте!


Действительно, кек.
211 113250
>>3249
А, ну то есть неправильная модель, надо запретить?
212 113251
>>3250
Да не то что неправильная, просто придуманная. Художественная литература.
213 113252
>>3251
А есть какие-то богом данные модели что ли?
214 113255
Конструктивист должен знать:
1) изоморфизм Карри-Говарда и тезис Чёрча;
2) содержание диссертации Брауэра в переводе Гейтинга;
3) пять уровней языка и четыре способа отрицания по Маннури;
4) интерпретацию логических констант по Брауэру-Гейтингу-Колмогорову;
5) теорию статистического обучения Вапника и модель spikgram Миколова;
6) отличия машины Тьюринга от машины Поста.

Конструктивист обязан:
1) отрицать закон исключённого третьего;
2) отрицать любую математику, не выразимую через типизированную лямбду в MLTT или нормальные алгорифмы Маркова;
3) переписать на прувере AUTOMATH де Брауна книгу "Основы математического анализа" Ландау;
4) представить все формальные теории в терминах алфавитов, термов и манипуляций с ними;
5) свести гомологическую алгебру к исчислению предикатов, используя нумерацию Гёделя.
215 113256
>>3249
Ну придумали же множества. Оказалось полезным.
216 113258
>>3229
Реально так. Нет даже возможности алгема или алгтопа, бесполезная вещь.
217 113260
>>3258
Про алгтоп целая восьмая глава.
218 113262
>>3229
>>3258
HoTT+аксиома выбора+универсум (вроде как) взаимно интерпретируема с ZFC+недостижимые кардиналы, так что всё, что можно сделать в "стандартной" математике, можно сделать и в HoTT. Требовать "определение пучка в HoTT" это то же самое, что требовать "определение пучка в ZFC".
И вообще, практически для всей математики (в том числе для пучков) скорее всего хватит даже подсистемы арифметики второго порядка.
219 113264
>>3262
Не то же самое. Определение пучка в ZFC есть, а в HoTT нет.
220 113265
>>3264

>а в HoTT


Предпучок на сайте, удовлетворяющий ряду свойств.
GoldenWheatSheafSmall061CastleFarm106071000x.jpg.webp106 Кб, 1000x1000
221 113268
>>3265
Предпучок не канает, нужен пучок колец.
222 113280
С пучками вы тоже обосрались, как впрочем и со всем остальным. Есть у Сохацкого в андерсе.
223 113284
224 113303
Сообщаю единственное верное мнение по поводу оснований математики.

0) Основания математики должны быть $(n,r)§-категорными, где $n,r \in \mathbb{N} \cup \{ -2,-1,\infty\}$.
1) Споры об аксиоме выбора не имеют смысла. Действительно, категория $\mathrm{Set}_{\mathrm{AC}}$ множеств и отображений между ними, где все эпиморфизмы обратимы справа, и категория $\mathrm{Set}$, где это условие не обязательно выполняется, обе являются абсолютно валидными категориями. С какой именно из них работать -- зависит от конкретной ситуации.
225 113305
>>3303
0) Основания математики должны быть $(n,r)$-категорными, где $n,r \in \mathbb{N} \cup \{ -2,-1,\infty\}$.

1) Споры об аксиоме выбора не имеют смысла. Действительно, категория $\mathrm{Set}_{\mathrm{AC}}$ множеств и отображений между ними, где все эпиморфизмы обратимы справа, и категория $\mathrm{Set}$, где это условие не обязательно выполняется, обе являются абсолютно валидными категориями. С какой именно из них работать -- зависит от конкретной ситуации.
поправил
226 113306
>>3305
Дополню. Натуральные числа определяются как инициальная алгебра эндофунктора $X \mapsto \ast \coprod X$ на произвольном топосе. Кроме того, естественно рассматривать не только натуральные числа, но и конатуральные числа (конатуральные кочисла? натуральные кочисла?) и коиндукцию.
227 113316
>>3306

> не только натуральные числа, но и конатуральные числа


Отрицательные что ли? Хуя ты демон, множество Z открыл.
228 113318
>>3316
Натуральные с бесконечностью, фактически.
229 113323
>>3316
Нет, как заметил анон >>3318 , конатуральные кочисла это терминальная коалгебра на указанном мной функторе. Я не уверен, что ты понимаешь под "отрицательными числами", но подозреваю, что это двойственная категория к категории предпорядка ассоциированной к $\mathbb{N}$ как моноиду, или возможно сам $\mathbb{N}$ как комоноид. Не знаю, как ты мог перепутать это с конатуральными кочислами.

>множество Z


Как правильно определять $\mathbb{Z}$ я, к сожалению, пока не понял, для меня это открытый вопрос. Предлагаю отталкиваться от "свободный $k$-кортежный моноидальный $n$-группоид на одном объекте".
230 113324
>>3323
Интересно, как ты собрался определить натуральные числа без абстракции поенциальной осуществимости? А если с ней, то зачем мудрить а не просто взять и определить палочками как у Маркова?
231 113325
>>3324

>как ты собрался определить натуральные числа


Вот тут >>3306 написал.

>абстракции поенциальной осуществимости


Прости, не знаю, что это такое. Звучит как что-то связанное с модальной логикой и теорией моделей. Это очень интересно, но к математике (разделу линейной алгебры) и ее основаниям отношения не имеет.

>определить палочками


Не знаю, что такое "палочки". Если ты имеешь в виду терминальный объект в топосе, то это соответствует моему >>3306 определению.
232 113326
>>3324

> Интересно, как ты собрался определить натуральные числа без абстракции поенциальной осуществимости?


N петух опять завел свою ШУЕ шарманку. Абстракция потенциальной осуществимости - это свойство аксиом Пеано, а не что-то что может "существовать" отдельно от примеров, содержащих абстрагируемое свойство.
233 113327
>>3326
Cам то понял что сказал? Ты свою ШУЕ шизу как чат бот высираешь даже не задумываясь.
234 113328
>>3327

> Cам то понял что сказал?


Понял. А вот ты походу нет.

> Ты свою ШУЕ шизу как чат бот высираешь даже не задумываясь.


Это общепринятое определение абстракции, N петух. А вот у тебя реально ШУЕ.
235 113329
>>3280
А можно с нормального Западного источника?
236 113330
>>3325

>Не знаю, что такое "палочки". Если ты имеешь в виду терминальный объект в топосе


Похоже на начало пути нового петушка. Напомнило времена раннего конструктивного петуха когда он еще мог что то кроме шитпостинга чмориджами, благоговейно цитировал писания швятых Браузера и пророка его Мартина-Лефа.
237 113331
>>3330
Я по сути просто пересказываю позицию всех великих математиков второй половины двадцатого и двадцать первого веков, от Гротендика и Квиллена до Шольце и Лури.
238 113332
>>3324
N-петух - ты ультрафинитист или що? Просто если так, то очень бы хотелось увидеть какую-нибудь валидную ультрафинитную программу оснований математики
239 113336
Какое мнение было у Гротендика по поводу теории типов и HoTT?
240 113337
>>3332

> N-петух - ты ультрафинитист или що?


Ультрадолбаеб.
241 113338
>>3329

> А можно с нормального Западного источника?


Ну да, у Сохацкого есть ссылки. Вообще под гамалогии у него запилен так называемый "стек де Рама - Черубини - Шрайбера", где-то к нему и ссылки на нормальные источники чтобы обпучкаться.
242 113339
>>3330
Брауэра цитировать местным ебланам типа тебя бессмысленно, вы в Википедию-то не можете, все ваше ШУЕ и просто весь набор слов контрится первой же ссылкой оттуда. Вот ты же обосрался с универсальной машиной Тьюринга, а мог бы не обсираться а просто прочитать определение в Википедии. Как и N петух, к слову. Успенский ещё ладно, дедушка старый, ему все равно. Рано вам ещё Брауэра и Мартин-Лефа, дети тиктака.
243 113340
>>3339

>Вот ты же обосрался с универсальной машиной Тьюринга


Кек. Ты обосрался даже с зелеными машинками.
244 113341
>>3340
Я ответил на весь класс подобных вопросов, но ты этого ожидаемо не увидел, дединсайд. То есть, обосрался и в этом.
245 113342
>>3341
Твои любимые мемасы с чмориджами это универсальный ответ на все только в твоем деградировавшем мозгу.
246 113343
>>3342
Ты как-то слишком отстраненно пишешь про чмориджей, хотя сам - ярчайший представитель вида, судя по дегенеративности твоих постов.
247 113344
>>3338
(Ко)гомологии в HoTT можно и без модальностей считать (см. https://guillaumebrunerie.github.io/pdf/LIPIcs-CSL-2022-11.pdf, https://arxiv.org/pdf/2212.04182.pdf или https://arxiv.org/pdf/1706.01540.pdf), модальности нужны ради варианта SDG (https://ncatlab.org/nlab/show/synthetic+differential+geometry).
248 113352
>>3343

>Какое понятие более общее - "автомобиль" или "зеленый автомобиль"?

249 113354
>>3352
Имхо это плохая аналогия, и вопрос "какое понятие более общее" не очень хорошо определен для мат объектов. Попробуй лучше с абстрактной группой и подгруппой группы симметрий.
мимо
250 113355
Основания, где такие проблемы с определением простого пучка нинужны. Ну реально же так.
251 113356
>>3354
Чем аналогия плоха? Предельно ясная аналогия доступная даже детсадовцам чтобы навести петуха на правильный ответ.

> не очень хорошо определен для мат объектов


не в данном случае
252 113357
>>3355
Ты либо троллишь, либо дебил, второе очень вероятно учитывая этот ответ >>3268
253 113358
>>3344
Так, а это уже реально база. Там можно сделать алгеом? Кинь пожалуйста еще такое. Завтра скачаю Agda если есть алгеом. Помню в 2017 пробовал, но там даже не было когомологий.
Это же она?

>>3357
Я просто пошутил, извини. Пытаюсь троллингом вытянуть истину. Мне реально нужен теоретико-типовой пучок.
17042528441170.png208 Кб, 968x733
254 113359
>>3358

> Завтра скачаю Agda


Ты её вместе с нужными либами установить-то сможешь, пучкист?
255 113360
>>3356

>не в данном случае


Какое "понятие" более общее, абстрактной группы или подгруппы группы симметрий? Для меня этот вопрос не имеет смысла, потому что абстрактная группа (т.е. по сути синтаксическая теория) и конкретные группы (т.е. по сути ее модели) живут в разных категориях. То же с машинами Тьюринга.
Вообще, по-моему здесь происходит путаница между отношением абстрактное-конкретное и отношением общее-частное.

>Чем аналогия плоха?


Я не уверен, в каком смысле зеленая машина (эта конкретная зелена машина? понятие зеленой машины?) моделирует любую машину (любую конкретную машину? понятие машины?).
256 113361
>>3359
Да, у меня базовый artix linux, так что всё в порядке.
Скоро будут пучки на арче.
257 113362
>>3360

>Какое "понятие" более общее, абстрактной группы или подгруппы группы симметрий?


Ну я сразу понял ты предлагаешь сравнить два несравнимых понятия и доказать таким образом что любые два понятия невозможно сравнить. Это какая то форма конструктивизма головного мозга?

>Я не уверен, в каком смысле зеленая машина


очень на то похоже...
258 113363
>>3358

>Мне реально нужен теоретико-типовой пучок


Определяется пучок в HoTT так же, как везде: как предпучок на сайте, удовлетворяющий ряду свойств. Чтобы увидеть, как это определение выглядит в агде, достаточно загуглить "sheaf agda" и посмотреть, например, сюда https://github.com/jonsterling/constructive-sheaf-semantics
>>3362

>что любые два понятия невозможно сравнить


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

>Это какая то форма конструктивизма головного мозга?


Я не конструктивист.
259 113364
>>3363

>Объекты двух разных категорий действительно нельзя сравнить


О! так ты новый категориальный петушок. Милости просим.
260 113365
>>3363
>>3364

>Объекты двух разных категорий действительно нельзя сравнить


Почему нет? Для этого же функторы.
15848162669910.mp4453 Кб, mp4,
426x240, 0:07
261 113366
Перепишем петухов: монвый петух (самый гнилой пидор here), конструктивный петух, категорный петух, петух пучкист, ...
262 113368
>>3364
Давай так -- дай мне множество понятий и определи на нем отношение порядка, которое моделировало бы отношение "x есть более общее понятие, чем y". Потом расскажи, где во всей этой структуре относительно друг друга будут находиться понятия "универсальная машина Тьюринга", "машина Тьюринга", "группа", "подгруппа группы симметрий", "машина" и "зеленая машина" и почему. Или предложи альтернативную модель. Тогда может получиться какой-то разговор.
Ну или загугли хотя бы "aristotle ontological square" и помедитируй над разницей между exemplify, instantiate и inhere.
>>3365
Возьми два множества с определенными на них предпорядками (можешь рассматривать их как категории). Как "сравнить" (каким (би)функтором?) элемент первого предпорядка с элементом второго? inb4: (ко)произведение не это делает.
263 113369
>>3368
Читай абстрации. Всё что ты говоришь свойство абстракций а не конкретных примеров.
264 113370
>>3369
На что это ответ?
265 113371
>>3368
Раньше конструшок такой же напористый был, только предлагал перечитывать все писания швятого Браузера и пророка его Мартина-Лефа. Если тебе все это нужно чтобы ответить на вопрос на который легко ответит даже ребенок пяти лет, то куда то ты не туда свернул.
266 113372
>>3371
Сомневаюсь, что типичный ребенок пяти лет хорошо понимает, что такое "более общее понятие". Еще сомневаюсь, что типичный ребенок пяти лет хорошо понимает разницу между синтаксической теорией и ее моделью. Еще сомневаюсь, что мы в строгости должны ориентироваться на детей. Еще прошу заметить, что я никого читать не предлагаю, а прошу описать отношение предпорядка, с чем у умного ребенка пяти лет проблем действительно возникнуть не должно.
1604735203875.png71 Кб, 812x656
267 113373
>>3356
>>3371
Вообще вот, смотри, это глава про "понятия" из стандартного русскоязычного учебника по логике для гуманитариев, Бочарова-Маркина. Можешь почитать, и когда у тебя будет что-то сравнимое по строгости, сможем обсудить, какие понятия с какими как относятся.
16989216386531.mp4936 Кб, mp4,
352x640, 0:14
268 113374
>>3368
>>3372
Ты тут с кем-то споришь, пытаешься что-то доказать, а там вот такое чучело сидит с вероятностью процентов 95. Максимум - N петух, который пару ссылок на Википедию не осилил.
269 113375
>>3358

>Там можно сделать алгеом?


Вопрос не совсем верно задан. Как верно выше замечали, HoTT с выбором интерпретирует ZFC (теорема 10.5.11 в HoTT book’е), так что раз в ZFC можно сделать алгеом, то и в HoTT тоже.
Ты, вероятно, спрашивал о синтетическом алгеоме (то есть чтобы с ℝ не пердолиться; иначе можно задать справедливый вопрос: для чего нужны кубические теории типов). Тогда как раз можешь почитать, что пишут Черубини и Шрайбер: https://www.math.kit.edu/iag3/~wellen/media/diss.pdf, https://arxiv.org/pdf/1806.05966.pdf, https://arxiv.org/pdf/2307.00073.pdf и вообще https://arxiv.org/find/math/1/au:+Schreiber_U/0/1/0/all/0/1 и https://felix-cherubini.de/ (тут ссылки на Agda-код есть).
Если очень надо пердолиться с ℝ, при этом пользоваться синтетическими расчётами, можешь почитать https://arxiv.org/pdf/1509.07584.pdf, но, правда, насколько я знаю, это в пруверах ещё никто не реализовывал.

>Кинь пожалуйста еще такое.


Майер — Вьеторис для когомологий: https://staff.math.su.se/evan.cavallo/works/mayer-vietoris.pdf, https://staff.math.su.se/evan.cavallo/works/oxford.pdf
Вот тут подробнее: https://ncatlab.org/nlab/files/Cavallo-CohomologyInHoTT.pdf
Вот когомологии Чеха сделать пытаются: https://www.felix-cherubini.de/chech.pdf (тут тоже SDG).
Гомологии для CW-комплексов: https://arxiv.org/pdf/1802.02191.pdf
Спектральные последовательности: https://github.com/cmu-phil/Spectral, https://ncatlab.org/nlab/show/spectral+sequences+in+homotopy+type+theory, https://florisvandoorn.com/talks/17Pitt_SSS.pdf
Теорема Гуревича: https://arxiv.org/pdf/2007.05833.pdf
Тут пятая глава про когомологии: https://arxiv.org/pdf/1606.05916.pdf
Свежая статья про когомологии на агде: https://arxiv.org/pdf/2401.16336.pdf

>Это же она?


В статьях про когомологии? Да, Agda.
270 113379
>>3375
Такое-то окормление говном модульного деда. Годами квакал, что нематематика потому что гамалогий нет, а оказалось что давно уже есть.
271 113382
>>3358
Это кал, качай Anders там всё есть, в том числе и абстракции созданные на основе примеров (но и в коем случае не наоборот!).
272 113383
>>3379
В википедии такого не написано, а значет всё это кал.
273 113384
>>3383
Тут тема несколько сложнее, чем обычно в Википедии пишут. Но против твоих кукареканий и Википедии более чем достаточно. Ты просто знай своё место (оно у параши) и смирись с этим.
274 113385
>>3384
Я знаю, мой дом здесь, я все треды перекатываю.
275 113386
>>3375
База уровня выше 9000.
Спасибо, анон. Загрузил плейлист по Агде и буду постепенно вкатываться опять.
276 113388
>>3386
Тебе. Нужен. Anders.
277 113389
>>3386
База это википедия плюс Anders.
278 113390
>>3388
>>3389
В Anders вариант CTT из агды (плюс пара расширений).
279 113394
>>3388
Что это? Я вроде видел его мельком если не ошибаюсь, но синтаксис Агды пока топ для математика. Чистый, без всяких проггерских штук.
280 113395
>>3394

>Что это?


Это тебя жирно троллят. Чуть более продвинутая чем cubicaltt (но всё ещё экспериментальная) имплементация кубической теории типов.
В сравнении, в кубической агде библиотека значительно больше и много готовой автоматизации.

>синтаксис Агды пока топ для математика


В агде нельзя использовать «=» для равенства…
281 113398
>>3374
Скибиди-петух, а тебе что интересно не позволяет ответить на вопрос? Тебе же не нужно как категориальному петуху выписать категорию всего на свете чтобы было вообще о чем говорить. Подозреваю дело в том что МЛ не завез сабтайпинг и другим отношения на типах строить не велел и теперь для петуха это не доступная концепция так что от одного вопроса у него разрывает пердак. Сейчас порватыш еще чмориджей подкинет.
17069369167140.mp41017 Кб, mp4,
460x380, 0:17
282 113399
Такой смешной тред получается, прямо как никогда.
- доломали N петуха, не осилившего пару определений из Википедии
- совершенно случайно доломали модульного деда, оказалось что гамалогии давно реализованы в агде
- попутно опетушили то ли какого-то подсиралу N петуха, то ли самого N петуха, мимикрирующего под собственного подсиралу, так же не осилившего определение машины Тьюринга из Википедии.
283 113400
>>3399
И только конструктивный петух щебечет все так же резво как и раньше. Уникальный случай в истории когда петух совсем без мозга живет уже больше десятка лет.
284 113401
>>3399

>модульного деда


Он не сидит тут уже давно.
286 113423
>>3401
Ну еще бы, мовный петух-пидарок всех вменяемых разогнал своей шизой :С
287 113424
>>3423
Рад, что ты сам себя из вменяемых выписал только что. Можешь и сам отсюда танцевать нахуй. Только одно замечание - опровержение N петушества по существу (конкретными ссылками), это не шиза, как бы неприятно тебе от этого не было.
288 113426
>>3424
Шиз, ты опять сам с собой разговариваешь, таблетки забыл принять?
289 113427
>>3424

>это не шиза


>мам, ну скажи что не шиза, ну позязязяяя


хуя отрицалово
17092227787340.webm767 Кб, webm,
1280x720, 0:02
290 113429
>>3426
>>3427
Ссылки я приносил. Ну давай, возрази что-нибудь по существу. Только ты не сможешь, а будешь дальше вякать про "шизу" просто в качестве защитной реакции на тыканье тебя еблом в факты и что-то "отвечать" просто ради "рреее я последний запостил". Такие вы смешные тут долбаебы.
291 113430
>>3429
Уважаемый (на самом деле нет), ты в своих анальных половых партнёрах уже запутался. Кто там тебя в анус сношал мне фиолетово ;)
292 113435
Похоже наш конструктивный петушок наелся таблеток и спит :)
293 113436
>>3429

> возрази что-нибудь по существу.


>>3430

> ты в своих анальных половых партнёрах уже запутался. Кто там тебя в анус сношал мне фиолетово ;)


> возражение по существу


Я примерно подобного и ожидал от малолетнего дегенерата. Ок, петушоникс, я тебя услышал.
294 113437
>>3436
По существу ты шизик, это медицинский факт, но что ты от меня хочешь, петушарий? Я не из этих, ваших, если что.
295 113440
>>3437

> По существу ты шизик, это медицинский факт,


Это кукареканье долбаеба, а не факт, тем более "медицинский".

> что ты от меня хочешь,


> сам мне безостановочно написывает одну хуйню за другой


?
296 113444
>>3440
Поциэнт, это ваш диагноз а не хуйня. Не занимайтесь самолечением, обратитесь к специалистам.
image.png255 Кб, 400x400
297 113541
Поясните, плиз, логики отдельно от математиков обучаются, вместе с философами или как? Попалось мне как-то видео Андрея Родина, может он вам знаком. Вроде он не математик, но обсуждает постоянно теорию категорий, алгебраическую геометрию, труды Воеводского. Но непонятно, как можно о современной математике говорить, если ты ей не занимаешься. Насколько это все котируется в научном сообществе. Хотя он вроде не балабол, доктор философских наук, тусуется в ВШЭ, у него на защите докторской Вавилов был и хорошо о нем отзывался. Поясните, какой тут положняк?
image.png255 Кб, 400x400
298 113542
Поясните, плиз, логики отдельно от математиков обучаются, вместе с философами или как? Попалось мне как-то видео Андрея Родина, может он вам знаком. Вроде он не математик, но обсуждает постоянно теорию категорий, алгебраическую геометрию, труды Воеводского. Но непонятно, как можно о современной математике говорить, если ты ей не занимаешься. Насколько это все котируется в научном сообществе. Хотя он вроде не балабол, доктор философских наук, тусуется в ВШЭ, у него на защите докторской Вавилов был и хорошо о нем отзывался. Поясните, какой тут положняк?
https://youtu.be/lXTuJL_VaSI?si=hSXsgV4UAF52bfR7
299 113546
>>3542

>Поясните, плиз, логики отдельно от математиков обучаются, вместе с философами или как?


Есть специальность "логика" у философов (ака 5.7.5 в номенклатуре ВАК) и есть специальность "математическая логика" у математиков (ака 1.1.5).
Соответственно, часто есть кафедра (лаборатория, институт, группа...) логики (и, обычно, чего-то еще) на математическом факультете, и кафедра (лаборатория, институт, группа...) логики на философском. Учатся математики-логики и философы-логики раздельно, если не считать возможные межфакультетские и междисциплинарные курсы/семинары.

>Но непонятно, как можно о современной математике говорить, если ты ей не занимаешься


Очевидно, он в математике, о которой он говорит, разобрался достаточно, чтобы заниматься философией математики. Разобрался он, вероятно, так же, как разбираются все остальные люди - читая книжки и разговаривая с людьми, работающими в области (вот https://philomatica.org/wp-content/uploads/2013/02/colin.pdf пример такого разговора). В принципе, самоучки, которые освоили какой-то материал в достаточной степени, чтобы понимать, что пишут другие, - это не какое-то редкое явление. Собственно производством новой математики он не занимается и, вроде как, не претендует.

>Насколько это все котируется в научном сообществе


Философия математики это существующая область, и вопросы, которые он обсуждает, в ней обсуждает не только он. Он где-то преподает и пишет статьи. В этом смысле, то, что он делает, вполне себе "котируется".
300 113554
>>3054
Нашел кстати где-то у МЛ тезис о том что действительно мы не знаем что такое доказательство, если бы мы знали что такое доказательство, но мы не знаем что это такое...
Но при этом утверждается что единственный способ доказать конъюнкцию это предъявить пару доказательств. Почему нельзя это сделать еще каким то окольным путем? Или почему не учитываются возможные проблемы, например если имеются ресурсные ограничения - та самая "чернильная дыра", у человека заканчивается бумага чтобы выписать оба доказательства вместе, в формальной системе не хватает свободных переменных.
Еще интереснее тезис о применении функций к доказательствам при построении импликации. Т.е. мы не знаем что такое доказательство но мы будем применять к нему функции. Приехали.
301 113556
>>3554

> Нашел кстати где-то у МЛ тезис о том что действительно мы не знаем что такое доказательство,


Цитату неси.
302 113557
>>3556
Губой тряси.
16921935985830.mp4354 Кб, mp4,
602x338, 0:01
303 113559
>>3557

> чепуха до сих пор трясётся


Что ж вы такие тупые-то
304 113561
>>3556
https://archive-pml.github.io/martin-lof/pdfs/Truth-of-a-Proposition-Evidence-of-a-Judgment-1987.pdf

>Now, there can be no proof, no conclusive proof, that a proof really proves its conclusion, because, if such a miraculous means were available to us, we would of course always use it and be guaranteed against mistakes.


>So, clearly, there can be no proof in the proper sense of the word that a proof really proves its conclusion: the most there can be is a discussion as to whether a proof is correct or not, and such discussion arises precisely when we make mistakes, or when we have insufficient grounds or evidence for what we are doing.


>As should be clear from what I have just said, this notion of validity or conclusiveness or correctness of a proof is a very fundamental notion. Indeed, it is the most fundamental one of all, the one of all the notions that I have digcussed which has no other notion before it


в конце какая то хуйня-малофья идет про хлеб и ненастоящий сладкий хлеб и про то что можно считать доказательством то что кажется достаточно убедительным лично тебе (или не считать, тут я не понял мнение лично МЛ на этот счет)
305 113562
>>3559
Петух, ты разобрался какое понятие более общее "зеленые автомобили" или "автомобили" или для тебе это все еще неподъемная задача, кек?
306 113563
>>3562
Хуй там, это ебанько даже определение абстракции не осилило, теперь вот бегает как опущенный со своей википедией. Такая вот абсиракция, лол.
307 113564
>>3563
N петух, общепринятое определение абстракции я цитировал. Но ты его не осилил, зато уверовал в рандомной ШУЕ.
308 113565
>>3564
Ты копипастил нерелевантуню хуйню которую даже нормально прочитать и понять не смог. Ты даже отрицал что абстракция это понитие, т.е. у тебя мозги отшиблены на прочь от слова совсем, тебе с школьной программы нужно начинать а потом уже в основания лезть. О чём с тобой после этого говорить? Эта болезнь головного мозга (асемасия) описана у Манина в "доказумом и не доказуемом", он там приводил примеры как больные с частиным поражением мозга могли копипастить относительно сложные фразы (как например делаешь ты, хотя ни Мартин Лёфа ни Маркова ты не читал) при этом путались в элементарных понятиях. Если будет второе издание книги, тебя нужно в пример поставить, с цитатами, как канонического ебанька.
16937118393800.mp4386 Кб, mp4,
764x720, 0:03
309 113567
>>3565
Энпе Тух, ты просто клоун. Все твои кукареканья - это всего лишь защитная реакция. А все твои маняаргументы контрятся первой же ссылкой из Википедии. Ты пытаешься приплести какую-то нерелевантную хуйню, какую-то "сасимасию Манина" (чего?), какие-то выдуманные "диагнозы", которые с готовностью приписываешь несогласным с твоим ШУЕ итд. Все это просто чтобы не признавать своего обсера в простейшем вопросе - определении абстракции. А это определение есть на каждом углу начиная с Википедии. Ты это прекрасно понимаешь. И тебе от этого никуда не деться, терпи Энпе Тух, терпи.
310 113568
>>3567
Ничего, стадия отрицания у тебя скоро закончится и придёт сирение, мовный петух. Как говорили в одном фильме "...и тебя вылечат".

Твоя уровень это детские книжки с соовтествующими "определениями" для детей, что бы не травмировать психику раньше времени. Только непонятно, если ты дебил, зачем во взрослые треды лезешь со своим свиным рылом, ась? Отвечай, мовная петушара.
311 113569
>>3567

> Ты пытаешься приплести какую-то нерелевантную хуйню, какую-то "сасимасию Манина" (чего?)



Ты бы лучше вместо ШУЕ уёбка сохацкого что нибудь путное почитал, того же Манина например.
Ведь один в один твой случай, как будто с тебя писали:

«Мл. лейтенант Засецкий, 23 лет, получил 2 марта 1943 года пулевое проникающее ранение черепа левой теменно-затылочной области. Ранение... осложнилось воспалительным процессом, вызвавшим слипчивый процесс в оболочках мозга и выраженные изменения в окружающих тканях мозгового вещества».

Нарушения психики Засецкого поначалу ужасны. Над всем доминирует асемасия — разрывы связей между знаком и его значением.
Первая встреча Засецкого с врачом: «Попробуйте прочитать эту страничку! «—»... Нет, что это? ... не знаю ... я не понимаю, что это ... Нет ... какое это? ... — «Ну, попробуйте посчитать что-нибудь простое, например сложите семь и шесть! ...»— «Семь ... шесть .. .как же это ... семь... нет, я не могу ... нет,-я совсем не знаю ...».
Утрачено понимание простейших предикатов:
«Что бывает перед зимой?» — «Перед зимой... или после зимы .. . лето ... или что-нибудь ... нет. Это у меня не выходит ...» — «А перед весной?» — «Перед весной ... сейчас весна ... а вот до ... или после ... я уже теряюсь ... нет ... у меня не выходит . . .»
Нарушается интерпретация смыслоорганизующих кодов синтаксиса:
«В школу, где училась Дуня, с фабрики пришла работница, чтобы сделать доклад». Что это? Кто же сделал доклад? Дуня? Работница? А где училась Дуня? И кто пришел с фабрики? И куда?»
Это трудный пример (текст А. Р. Лурия), но вот что пишет сам Засецкий: «А еще: «слон больше мухи» и «муха больше слона» ... Я понимал только, что «муха» маленькая, а «слон» большой, но разобраться в этих словах и ответить на вопрос, муха меньше слона или больше, я почему-то не мог. Главная же беда была в том, что я не мог понять, к чему относится слово «меньше» (или «больше») — к мухе или слону . . .».
Обращает на себя внимание сложность метаязыкового текста, описывающего языковые нарушения. Точность анализа нарушений кажется несовместимой с грубостью нарушений, которые анализируются. Это можно было бы объяснить тем, что анализ ретроспективен, но вот описание в настоящем времени, еще более глубокое: «... Я снова припоминаю про понятия «муха меньше слона» или «муха больше слона». Берусь думать над ними, как они должны правильно пониматься и как неправильно. От перестановки слов в этих понятиях изменяется смысл понятия. Мне же они кажутся на первый взгляд одинаковыми, словно ничего не изменяется от перестановки этих слов. А подольше подумаешь, заме-
чаешь, что or перестановки слов изменяется смысл указанных четырех слов (слон, муха, меньше, больше). Но мой мозг, моя память после ранения и до сих пор не в силах сразу охватить, к кому отнести слово меньше (или больше) — к слону или к мухе? Перестановок даже в этих четырех словах очень много».
Это сохранение сложных психических способностей при утрате «простых» видно и на образцах творческого воображения Засец-кого, близких к литературно-психологическим этюдам: «Вот-я врач. Я осматриваю больного, сердечно обеспокоен его состоянием, болею за него всей душой, ну как же, ведь это же человек, такой же, как и все, но только он сильно болен, ему надо помочь. Ведь я тоже могу болеть, и мне тоже кто-то должен помочь, а теперь вот надо помочь этому больному. Иначе нельзя. А вот я другой врач. Ох, и надоели мне эти больные со своими жалобами. Я не знаю, зачем я связался с этой медициной. Мне не хочется ничего делать, не хочется никому помогать. Правда, я. помогаю больше тем, кто и мне оказывает какую-нибудь помощь. И не беда, если умрет какой-нибудь больной, не в первый раз они умирали и умирают».
Все это показывает полную неосновательность мнения Дж. Россера [6]: «Когда доказательство открыто и записано на языке символической логики, его может проверить любой слабоумный (moron)».
311 113569
>>3567

> Ты пытаешься приплести какую-то нерелевантную хуйню, какую-то "сасимасию Манина" (чего?)



Ты бы лучше вместо ШУЕ уёбка сохацкого что нибудь путное почитал, того же Манина например.
Ведь один в один твой случай, как будто с тебя писали:

«Мл. лейтенант Засецкий, 23 лет, получил 2 марта 1943 года пулевое проникающее ранение черепа левой теменно-затылочной области. Ранение... осложнилось воспалительным процессом, вызвавшим слипчивый процесс в оболочках мозга и выраженные изменения в окружающих тканях мозгового вещества».

Нарушения психики Засецкого поначалу ужасны. Над всем доминирует асемасия — разрывы связей между знаком и его значением.
Первая встреча Засецкого с врачом: «Попробуйте прочитать эту страничку! «—»... Нет, что это? ... не знаю ... я не понимаю, что это ... Нет ... какое это? ... — «Ну, попробуйте посчитать что-нибудь простое, например сложите семь и шесть! ...»— «Семь ... шесть .. .как же это ... семь... нет, я не могу ... нет,-я совсем не знаю ...».
Утрачено понимание простейших предикатов:
«Что бывает перед зимой?» — «Перед зимой... или после зимы .. . лето ... или что-нибудь ... нет. Это у меня не выходит ...» — «А перед весной?» — «Перед весной ... сейчас весна ... а вот до ... или после ... я уже теряюсь ... нет ... у меня не выходит . . .»
Нарушается интерпретация смыслоорганизующих кодов синтаксиса:
«В школу, где училась Дуня, с фабрики пришла работница, чтобы сделать доклад». Что это? Кто же сделал доклад? Дуня? Работница? А где училась Дуня? И кто пришел с фабрики? И куда?»
Это трудный пример (текст А. Р. Лурия), но вот что пишет сам Засецкий: «А еще: «слон больше мухи» и «муха больше слона» ... Я понимал только, что «муха» маленькая, а «слон» большой, но разобраться в этих словах и ответить на вопрос, муха меньше слона или больше, я почему-то не мог. Главная же беда была в том, что я не мог понять, к чему относится слово «меньше» (или «больше») — к мухе или слону . . .».
Обращает на себя внимание сложность метаязыкового текста, описывающего языковые нарушения. Точность анализа нарушений кажется несовместимой с грубостью нарушений, которые анализируются. Это можно было бы объяснить тем, что анализ ретроспективен, но вот описание в настоящем времени, еще более глубокое: «... Я снова припоминаю про понятия «муха меньше слона» или «муха больше слона». Берусь думать над ними, как они должны правильно пониматься и как неправильно. От перестановки слов в этих понятиях изменяется смысл понятия. Мне же они кажутся на первый взгляд одинаковыми, словно ничего не изменяется от перестановки этих слов. А подольше подумаешь, заме-
чаешь, что or перестановки слов изменяется смысл указанных четырех слов (слон, муха, меньше, больше). Но мой мозг, моя память после ранения и до сих пор не в силах сразу охватить, к кому отнести слово меньше (или больше) — к слону или к мухе? Перестановок даже в этих четырех словах очень много».
Это сохранение сложных психических способностей при утрате «простых» видно и на образцах творческого воображения Засец-кого, близких к литературно-психологическим этюдам: «Вот-я врач. Я осматриваю больного, сердечно обеспокоен его состоянием, болею за него всей душой, ну как же, ведь это же человек, такой же, как и все, но только он сильно болен, ему надо помочь. Ведь я тоже могу болеть, и мне тоже кто-то должен помочь, а теперь вот надо помочь этому больному. Иначе нельзя. А вот я другой врач. Ох, и надоели мне эти больные со своими жалобами. Я не знаю, зачем я связался с этой медициной. Мне не хочется ничего делать, не хочется никому помогать. Правда, я. помогаю больше тем, кто и мне оказывает какую-нибудь помощь. И не беда, если умрет какой-нибудь больной, не в первый раз они умирали и умирают».
Все это показывает полную неосновательность мнения Дж. Россера [6]: «Когда доказательство открыто и записано на языке символической логики, его может проверить любой слабоумный (moron)».
312 113570
>>3568
Энпе Тух, приведи свое петушиное определение абстракции, противоречащее общепринятому. Со ссылками, разумеется.
313 113571
>>3570
Тебе и из википедии сойдёт, ты только его читать нучись без своей ШУЕ примеси.
А главное, это ты поясни почему оно не является понятием и кто тебе разрешал испльзовать в математике понятия без определения и одновременно не считать их исходными неопределямыми.
314 113572
>>3571

> Тебе и из википедии сойдёт,


А тебе почему не сойдёт?
315 113573
>>3572
Меня оно устраивает если без твоих ШУЕ-интерпретаций, на остальную часть поста отвечай.
316 113574
>>3573

> Меня оно устраивает


То есть, вопросов у тебя больше нет?
317 113576
>>3574
Больной асемасией, вы зря бросили лечение.
videoPreview.jpeg50 Кб, 720x405
318 113580
>>3576

> асемасией


Асисяй? Так какие претензии к определению абстракции в Википедии? Это приказ Израиля, чи шо?
>>3568

> детские книжки с соовтествующими "определениями" для детей, что бы не травмировать психику раньше времени


А у тебя какое-то тайноведение, закрытые оккультные писания не для всех, где абстракция определяется как-то иначе чем в общепринятом её понимании?
319 113610
>>3546
Местные основатели тоже терминов из книжек и разговоров нахватались и тоже получается философией математики занимаются тут.
320 113712
>>3580
То что ты привёл из википедии никакого отношения к нашему дискурсу не имеет, более того нисколько не противоречит тому что я писал. Просто ты как и подобает болезному умом простейший текст осилить не можешь, только бегаешь как опущенный с копипастами.

Это у тебя тупого ГСМ-ебанька абстракция магически сама себя определяет, в математике напротив, есть либо исходные понятия (аксиомы или доказательства/редукция к более простым понятиям). Касательно N ты ни первый способ ни второй не продемонстрировал, а значит можно в очередной раз сделать вывод что ты пиздливое хуйло.
321 113713
>>3712
10 дней обтекал? Лови тогда ещё струю мочи в ебало.

> абстракция магически сама себя определяет,


Абстракция это свойство примеров, собственно, содержащих её. В случае N, абстракция потенциальной осуществимости является свойством аксиом Пеано.
322 113714
>>3712

> Касательно N ты ни первый способ ни второй не продемонстрировал


N определяется аксиомами Пеано, абстракция потенциальной осуществимости это свойство аксиом Пеано. Следовательно, N определено. Свободен, клоун.
323 113725
(Почти) $2$-категорные основания теоретико-множественной математики подъехали: https://arxiv.org/abs/2403.03647v1
324 113732
>>3725
О, в треде есть реально полезный контент, чаю
325 113733
>>3732

>полезный контент


>стрелкодрист

17097325350750.jpg75 Кб, 446x334
326 113738
>>3732

> О, в треде есть реально полезный контент, чаю


"А что, так можно было?!" Прикинь, можно. Достаточно писать что-то по теме треда, а не только выгуливать тут шизу, пытаясь "ниспровергать" общепризнанные давно доказанные вещи писаниями ноунейм ШУЕшников.
327 113739
>>3733
а что не дрист, пучки? там же тоже стрелки
328 113741
>>3725
ШУЕ какое-то.
329 113743
>>3739
Только для стрелкосвиньи которая везде ищет стрелкогрязь.
330 113745
>>3741
Чем?
331 113749
>>3743
неплохо, пучки без функторов и естественных преобразований, уважение
332 113752
>>3749
Да ты не шаришь. Пучок - это первичное неопределяемое понятие...
333 113753
>>3745
Чем Сохацкий.
334 113754
>>3749
Стандартно. Вот если бы через преобразование Фурье, вот это была бы настоящая чмондель-техника.
335 113756
>>3754
Луракй пук Бернедектта
336 113757
>>3752
>>3753
>>3754
>>3756
обпучкался
337 113833
Есть в пруверах что-нибудь про криптографию и пучки, определяющие эллиптическую кривую?
338 113838
>>3833
Есть эллиптические кривые без пучков.
339 113839
>>3838
А с сохацким есть?
340 113841
>>3838
Как же так? Ведь эллиптическая кривая и есть пучок. Но так уж и быть, можно ссылку?
341 113842
>>3841
Ты загуглить не осилил, буквально. Кто тебе сказал, что ты криптографию в агде осилишь?
342 113843
>>3842
Я больше доверяю местным анонимусам, чем Гуглу.
343 113846
>>3843
Правильно делаешь, я например создал пучки в anders на сбруйной мове.
344 113847
Пучкаю с последних постов в штаны.
345 113848
>>3846
Я хочу создать криптографический пучок, чтобы только я знал, как ему дать формальное определение в теории типов Мартина-Лефа.
346 113849
>>3841
Пучки есть, эллиптические кривые есть, объединяй и будет тебе счастье.
347 113862
>>3849
Но пучок - понятие первичное.
348 113864
А интересно, какая у пучка логическая/теоретико-типовая интерпретация?
349 113865
>>3864
Пук Бернедектта на свiдомых мовах.
350 113889
хрю?
351 113892
>>3889
Бернадектт одобряет.
352 113902
>>3864
А если серьезно, без шуток?
353 113906
>>3902

> А если серьезно, без шуток?


Читать научиться для начала. Стек де Рама - Черубини - Шрайбера тут неоднократно упоминали.
354 113908
>>3906
Стек Намдака Томпы на banders имхо получше будет.
355 113912
>>3906
так это для алгтопа
Гойда.png35 Кб, 1026x164
357 113914
Бурбаки.jpg2,4 Мб, 3120x4208
358 114069
В переводе первой книги Бурбаков обнаружил фамилию УСПЕНСКИЙ.
359 114073
>>4069

>теория множеств


Может лучше сжечь книгу? Есть же теория категорий, ну или теория типов на крайний случай.
360 114074
>>4073

>теория категорий


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

>теория типов


Удобно как если на беговую дорожку прийти в латексном костюме. Может можно будет о чем то говорить когда компуктер-саентисты разберутся с десятками взаимоисключающих способов определить равенства, структуры, высказывания.
Теория множеств - оптимальная золотая середина на данный момент.
361 114079
>>4074

>Не дает интуиции, просто язык для описания некоторых свойств.


А теория множеств какую интуицию даёт?

>Удобно как если на беговую дорожку прийти в латексном костюме.


Ты аксиоматическую теорию множеств видел? Как там удобно функции строить, например, знаешь?А когда с десятками взаимоисключающих способов определить категорию Set разберутся?
Для математика, который не занимается вознёй в основаниях, в целом, не очень важно, в какой системе работать, а те, кто возятся, в любом случае окажутся по уши в сотне технических проблем.
362 114081
>>4074

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


Они-то давно разобрались, это ты разберись.

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


Заодно разберись, что такое теория категорий. Судя по вышенаписанному, у тебя вообще нет понимания, что это и зачем.
363 114083
>>4079
Функция определяется тем как действует на элементы. Определи мне возведение в квадрат в терминах теории категорий, а я над тобой поржу. Что такое топос определяется через аналогии с SET; вот если бы было наоборот тогда бы к мокрым мечтам категорщиков не было никаких вопросов.
Пока что потуги перевести основания на альтернативный формализм категорий или типов напоминают мне лисперов которым синтаксис ненужон.
>>4081
Иди терм отредуцируй, клоунесса конструктивная.
364 114084
>>4083

>Функция определяется тем как действует на элементы.


Ты же в курсе, что функция из A в B в теории множеств стандартно определяется как подмножество A × B с рядом условий, да?

>Определи мне возведение в квадрат в терминах теории категорий, а я над тобой поржу.


Возведение в квадрат чего? Натурального числа? Вещественного числа? Множества? Группы?

>Что такое топос определяется через аналогии с SET


Причём тут топос? Какие аналогии? Ты же в курсе, что для категории Set нужны классы или там, например, универсум Гротендика, да?
365 114086
>>4084
А ты в курсе как функция определяется в ТК? Никак
Допустим я хочу понять что из себя представялет возведение в квадрат и я смотрю:
1 - 1
2 - 4
3 - 9
...
поэлементно
Твои действия в аналогичной ситуации в рамках категориального подхода?
17116379301190.png996 Кб, 1000x900
366 114088
>>4086

> А ты в курсе как функция определяется в ТК? Никак


Первичное неопределяемое понятие!
367 114089
>>4086

>А ты в курсе как функция определяется в ТК?


Ты про какое-нибудь ETCS, да? А как тогда множество определяется в теории множеств? А отношение принадлежности там же? А как тип определяется в теории типов? А как определяется число в арифметике Пеано? А отношение «лежать между» в https://en.wikipedia.org/wiki/Tarski%27s_axioms?

>Допустим я хочу понять что из себя представялет возведение в квадрат и я смотрю:


Начнём с того, что функцией возведения в квадрат будет множество упорядоченных пар вида {(0, 0), (1, 1), (2, 4), (3, 9), …}.
В теории множеств известно, как определить функцию умножения натуральных чисел (пусть будет Π), поэтому возведение в квадрат естественно определить через неё как {(x, Π(x, x)) | x ∈ ℕ}, которое на самом деле сокращение к {(x, y) ∈ ℕ × ℕ | y = Π(x, x)}, которое на самом деле сокращение к {w ∈ ℕ × ℕ | ∃ x ∈ ℕ: ∃ y ∈ ℕ ∧ (x, y) = w ∧ ((x, x), y) ∈ Π}, если не пользоваться ε-оператором и сокращением для полного образа. Ой, сколько машинерии-то вдруг понадобилось для квадрата, а это мы даже не обсуждали, как произведение определить, в том числе и произведение множеств.

>Твои действия в аналогичной ситуации в рамках категориального подхода?


В ETCS, внезапно, тоже можно определить произведение Π, которое будет стрелкой из ℕ × ℕ в ℕ, а также диагональ Δ из ℕ в ℕ × ℕ, которая n ↦ (n, n). Возведение в квадрат, неожиданно, окажется композицией Π ∘ Δ. Более того, что тоже крайне неожиданно, такой же композицией его можно определить в теории множеств (надо лишь не забыть определить композицию функций, которая там напрямую не дана, да).
После точно так же можно посмотреть значение этой функции на конкретном числе, которое стрелка из терминального объекта в ℕ: есть стрелка 0 из терминального объекта в ℕ и стрелка succ из ℕ в ℕ, а Π ∘ Δ ∘ succ ∘ succ ∘ … ∘ succ ∘ 0, например, значением и будет.

>поэлементно


В детский сад.
368 114090
>>4089

>>поэлементно


>В детский сад.


Ясн. Ни для чего не пригодный формализм. Разве что только чтобы "переоткрывать" то что уже давно доказано через множества

> тоже крайне неожиданно


Да нет, крайне ожидаемо - категорщики пытаются одевать штаны через голову - смешно смотреть.
369 114091
>>4090
Ты, долбоёбина, функцию Аккермана тоже поэлементно исследовать будешь? А функции из ℝ в ℝ, особенно разрывные?

>Ни для чего не пригодный формализм.


У тебя, блядь, формализмами являются и теории множеств, и ETCS, дегенерат ебучий.
370 114092
>>4091

>У тебя, блядь, формализмами являются и теории множеств, и ETCS, дегенерат ебучий.


Это противоречит чему именно? Только тому что ты не тупая ебанашка, не пиши мне больше.
371 114093
>>4092
Сука, уёбок, у тебя в двух формализмах квадрат примерно одинаково определяется, но ты продолжаешь верещать, что один формализм априори лучше, а другой вообще не нужен, не разбираясь, блядь, ни в каком из них. Иди просто нахуй отсюда.
372 114094
>>4093
Не истери

>Иди просто нахуй отсюда


Хуй соси, губой тряси.
373 114095
>>4094
Поплачь ещё.
374 114096
>>4095

>Поплачь ещё.


Сказала манька, вытирая мокрые щечки.
375 114097
>>4074

>Не дает интуиции,


Вся моя интуиция строится как раз на ней и теории типов, а не на теории множеств.
376 114098
>>4084

>универсум Гротендика


Почти самая база, которая есть во всей математике.
377 114099
>>4097
Скажи что такое >группа, например?
379 114101
>>4084

>Ты же в курсе, что для категории Set нужны классы или там, например, универсум Гротендика, да?


NBG равнонепротиворечива с ZFC, а люди всё ещё ссут кровавой мочой от классов..
380 114102
>>4079
Гоша?
381 114103
Почему по поводу аксиомы выбора возникают такие споры? Что это вообще с точки зрения Гротендика и теории категорий? Знаю, что Гротендик был недоволен состоянием топологии и её привязки к анализу.
382 114104
>>4103

>Почему по поводу аксиомы выбора возникают такие споры?


Всегда удивляло тоже, ведь самое проблемное место теории множеств - это схема выделения..

>Что это вообще с точки зрения Гротендика и теории категорий?


Что у тебя эпи в Set расщепимы, т.е. почти тоже самое, что любой модуль над F_1 проективен..

>Знаю, что Гротендик был недоволен состоянием топологии и её привязки к анализу.


У меня скорее ощущение, что общей топологии быть не должно..
Просто так совпало, что мы изобрели настолько слабый концепт, что он работает в случаях, где мы используем совершенно разные методы
383 114106
>>4100
Давай своими словами, если конечно мозги есть. Группа это - ...
384 114107
>>4106
алгебра Хопфа над F1
385 114108
>>4107
Попробуй потоньше.
386 114109
>>4108
над F2
387 114110
>>4106
Зачем своими? Там лучше написано. Интуицию словами передавать это особый навык.
388 114111
>>4110
Ясно, так бы сразу и писал что своих мозгов нет.
389 114113
>>4111
Ты хочешь своровать категорные интуиции?
390 114114
Категория - первичное понятие во всей математике.
21499660-wheat-bunch.jpg124 Кб, 660x440
391 114115
bunch-of-ripe-wheat-ears-close-up-isolated-on-white-background-sheaf-of-wheat-ears99432-6291.jpg40 Кб, 626x626
392 114116
505635391.jpg36 Кб, 375x250
393 114117
394 114118
Вопрос: что изображено на каждой фотографии?
>>4115
>>4116
>>4117
395 114119
>>4118
пучки
396 114120
>>4119
На первой схема, на второй пучок групп, на третьей пучок категорий.
397 114121
>>4118
>>4120
Колхозная суть пучкизма?
398 114122
>>4088
А в чём, кстати, проблема с "первичными", "неопределяемыми" понятиями?

Мимо другой анон
399 114123
>>4121
Не колхозная, а природная. Пучки отражают естественную красоту мира и связь локального с глобальным.
400 114124
Как можно воевать против пучков и считать себя "математиком"?
401 114125
>>4124
А знаешь, кто ещё воевал против любителей пучков?
402 114126
>>4125
Подозреваю, что какой-то не математик?
403 114127
>>4115
>>4116
>>4117
Чет пучкнул.
404 114129
>>4127
ПУЧК ПУЧК ПУЧК ПУЧК ПУЧК
405 114130
>>4103
Потому что из неё следует что движением можно клонировать шарики.
406 114131
>>4084

>Ты же в курсе, что функция из A в B в теории множеств стандартно определяется как подмножество A × B с рядом условий, да?


Ну это так себе определение, по сути эквивалентно самой упорядоченной паре т.к. если ты определил пару ты уже фиксировал соответствие. Тут как множество это совокупность, а совокупность это множество. Один хер с разных сторон.
407 114132
>>4083
Подпесалсо. Проблема в том что все альтернативы теории множеств контринтуитивны и при этом не дают ничего нового в в том плане что все равно по сути повторяют конструкции в теории множеств только на более сложном языке.
408 114133
>>4131
Книгу по аксиоматической теории множеств какую-нибудь открой и не позорься.
409 114134
>>4132
Зато большие кардиналы интуитивны, да.
410 114136
>>4133
Опущ не умеющий читать, пшёл нах.
411 114137
>>4136
Съеби, дегенерат.
412 114138
>>4134
А почему не?
413 114139
>>4137

>пук сына шлюхи

17121476380070[1].mp44,3 Мб, mp4,
848x464, 0:23
414 114140
Мовный петух показал «Скибиди-туалет».
415 114141
>>4140
Это схема или алгебраическое многообразие?
416 114143
>>4141
Спектральная мова.
417 114145
>>4143
Спектральный пук.
Снимок экрана 2024-04-10 в 11.16.01.png196 Кб, 1354x1514
418 114233
>>4069
Да, это тот самый Успенский.

>>4073
Бурбаки с того света продолжают писать книги. В 2016 начала выходить Алгебраическая топология, там есть зайчатки теорката "по Бурбаки".

>>4083
На самом деле связи топосов с SET довольно спорны. По моему скромному мнению, гораздо более правильным является установление связей топосов с геометрией эйлеровых кругов на плоскости.
419 114245
Я уважаю только топосы, теоркат и немного теорию типов.
Лайк.jpg356 Кб, 1043x912
420 114248
гротендик десу.jpg94 Кб, 1200x675
421 114254
У вас бывало такое, что вы пытались интерпретировать просмотренное аниме или прочитанную визуальную новеллу с помощью категорий? У меня не получается понять, какие должны быть морфизмы и объекты в категории по выбранному аниме 𝔸.
Сначала хотел сделать персонажей объектами, а их отношения морфизмами, но потом понял, что какая-то тривиальная категория получается. Мне кажется, нужно брать отдельную категорию для каждого аспекта произведения, например - категория Сюжет(𝔸), Темы(𝔸) и т.д. Что думаете, братья категористы?
422 114258
>>4254
думаю, что пора покупать макбук
423 114290
>>4258
Я серьезно.
424 114291
>>4290
я тоже
425 114341
>>4254
Можно сделать морфизмы "тропами" а ля tvtropes, а любой объект это простр "болванка", полностью определённая морфизмами из и в, т.е. всеми применимыми "тропами".
426 114352
>>4341
namdak trompa spoq
гротендик 57.jpeg111 Кб, 700x611
427 114355
>>4341
В принципе идея неплохая, гораздо лучше моей, но вижу проблему. Думаю тоже будет тривиальная категория или некий скелет высшей категории. Некоторые персонажи в аниме/визуальных новеллах обладают глубиной, которая выше тропов заложенных в них, т.е. тут есть некая высшая структура которая описуема только условными 2-морфизмами в этой категории.

Она не захватывает всей структуры.

Или может нужно использовать интуицию теории пучков и алгема? Локально персонаж определен полностью тропами, но глобально может быть что-то нетривиальное.
428 114491
Вот есть логика, теория множеств, теория категорий и теория типов, как писали выше. В каком порядке это изучать, чтобы сохранить рассудок?
429 114496
>>4491
Ну у меня получилось немного нестандартно.

>программирование - теория типов - гомотопическая теория типов - теоркат - алгтоп - алгем и ПУЧКИ


Самое нормальное:

>база логики - теоркат и теория типов одновременно - алгем, алгтоп, высший теоркат и т.д.


Главное не останавливаться только на одном теоркате или теории типов, там точно с ума можно сойти. И множества вообще не трогай, можно навсегда стать инвалидом в математическом плане. И разбавляй нормальную первокультурную математику теоркатом и теорией типов, чтобы понимать глубинные смыслы.
430 114504
>>4355
Начинай с терии множеств как и все толковые математики, и не слушай шизиков вроде этого >>4496 а то как они едиенственное чего добьёшься - будешь срать на сосаче как они.
431 114638
Перекатываю вопрос из другого треда:
>>114625 →
432 114641
>>4638
Лучше сначала объясни, какие «противоречия, найдённые Гёделем» и как именно решила «типология Рассела»?
433 114642
>>4638
Нет, нельзя. И дело не в Гёделе. Формализация всей математики упирается в проблему разрешимости Гильберта, которая неразрешима, что доказал Тьюринг.
434 114643
>>4642
Неразрешимость означает, что в общем случае нельзя алгоритмически доказательства искать; возможность загнать всё в одну большую систему и доказать её непротиворечивость она не исключает (исключает теорема Гёделя в известных случаях).
435 114645
>>4638
Всё, сам нашёл. ZFC/NBG.
436 114708
>>4643
Это конструктивный петух, он у нас особенный. Так что лучше приготовься к потоку шитпостов если хочешь ему чего то доказать.
437 114713
>>4642
Сохацкий доказал обратное. Учи мовы, чмо.
438 114715
>>4713
А Сохацкому удалось на мове доказать существование N?
439 114716
>>4715
Докажи лучше существование Z.
440 114717
>>4716
Думаю уёбок сохацкий за последние пару лет на своей жопе почувствовал её существование, лол.
441 114718
>>4716
Проиграл.
442 114719
>>4716
>>4717
Обпучкался с этого.
443 114733
>>4717
мде вот только Z оказалась не бесконечная
444 114734
>>4733
ультрафинитисты насрали
445 115666
Почему теория типов вызывает такие негативные эмоции у разного круга лиц?
Раньше любил троллить с помощью неё на других бордах финитистов, математиков, алгемщиков пучкистов, и много кого.
446 115667
>>5666
Какой тип у 1?
Алсо достаточно глянуть на конструктивного петуха чтобы отпало желание заниматься теорией типов и вообще основаниями.
447 115669
>>5667
"X имеет тип Y" это же не предикат в теории типов, а утверждение мета уровня. В твоём случае вопрос не имеет смысла, потому что не существует абстрактного объекта в вакууме без типа. Дай определение 1, и сразу поймешь какой у него тип.
За счёт этого и хорошо получается троллить притворяясь ярым сторонником теории типов. Приверженцы других теорий оснований и математики сильно горят от неё, хотя по сути о ней знают очень мало.
448 115670
Почему ещё нет оснований, где именно пучок является первичным и неопределимым понятием? Почему первая культура так остаёт в основаниях? После Гротендика всё скатилось.
449 115671
>>5669

>утверждение мета уровня


Бла-бла-бла, бред. Не более "мета" чем существование пустого множества в теории множеств. От того что дурачки повторяют заученные швятые писание они не становятся правдой.

>не существует абстрактного объекта в вакууме без типа


Ты сказал?
На самом деле подвох был в том что 1 это натуральное число. А так же это целое число. И нечетное число. Это очевидно любому здравомыслящему человеку как и то что теория типов ущербна.
Когда будешь тролить в следующий раз расскажи еще про пятьдесят оттенков равенства в теории типов. Тогда ты точно будешь у мамки главным тралом.
N.jpg239 Кб, 1920x1080
450 115672
>>5671
Существование пустого множества выразимо в самой теории типов. x : A это не предикат, как предикат существования или принадлежности множеству. В теории типов любая точка принадлежит какому-то пространству, без этого невозможно даже говорить об этой точке.
Но это сказал не я, а Мартин Лёв. Если хочешь доказать его неправоту, покажи хоть один объект без типа в теории типов. 1 не имеет смысла в контексте оснований без более глубокого объяснения того, о чём мы говорим. 1 натуральное число, если мы говорим о типе натуральных чисел определенных индуктивно, также это и целое число, если мы говорим о Дедекиновых сечениях.
Понимаешь, запись концепта не равна концепту, который она описывает. 1 может быть даже терминальным объектом в категории.

Про разные равенства кстати математики хорошо понимают интуитивно, но вот именно то, о чём мы сейчас говорим вызывает у них диссонанс. Норм почва для троллинга и финитистов, и теоретико-множественников. Прочитал HoTT и можно троллить почти весь математический контингент, да даже программистов.
451 115673
>>5672

>Существование пустого множества выразимо в самой теории типов


множеств*
452 115674
>>5672

>Но это сказал не я, а Мартин Лёв.


Почему мне должно быть не похуй?

>покажи хоть один объект без типа в теории типов


>В Писании написано что Бог есть - шах и мат аметисты


Всех затралил лалок, переиграл и уничтожил.
453 115675
>>5674
1-0
Ещё одна победу в мою копилку.
454 115676
>>5675
Вообще смешно как МЛ придумал концепцию "джаджментов" - это как аксиомы, но только аксиому другую можно выкинуть нахуй (как это провернул пришвятой Браузер например) а вот "джаджмент" это нечто "совершенно фундаментальное и само-собой разумеющееся" и если будешь в этом сомневаться то незримый дух конструктивизма тебя покарает. При этой разумеющности МЛ несколько раз менял фундаментальные "джаджменты" своей теории типов, обсираясь в процессе с парадоксами. Но дурачки хавают. just sayin.
(И это еще петух похоже еще где то гуляет на каникулах, а то уже весь тред в его перьях бы был)
455 115677
Еще одна очень интересная штука это тайп-классы. Очень смешно это как будто такая теория типов которую теортипизаторы придумали как бы "для себя". У каждого объекта должен быть только один тип и задается он при определении? Вы че ебанутые? Нет, "для себя" мы сделаем все ровно наоборот, мы же не ебнутые.
456 115678
>>5676

>При этой разумеющности МЛ несколько раз менял фундаментальные "джаджменты" своей теории типов


Я слушал только одну его лекцию и не читал книги, он говорит эти джаджменты отражают объективную реальность или они работают только в пределах его теории типов? Если второе, то думаю они могут меняться.
>>5677
Тайп классы это ведь что-то из проггерства? Там вообще непонятно что происходит, у них там и вымышленная категория типов хаскеля есть.
457 115679
Кстати что там происходит с исследованиями в области HoTT? Открыли что-нибудь новое?
458 115680
>>5672

>Про разные равенства кстати математики хорошо понимают интуитивно


Ты наверно и аксиому унивалетности выпишешь с закрытыми глазами? Только не перепутай equivalence, equality и isomorphism.
459 115681
>>5680
Я да, недавно даже думал про неё в обычной жизни. Нормальные математики (то есть алгебраисты, пучкисты и прочие первокультурщики) интуитивно понимают различие изоморфизма и равенства. Им только нужно объяснить judgemental equality.
HoTT Brouwer-Wildberger.png14 Кб, 720x78
460 115682
>>5679
Добавили новую аксиому Брауэра-Вайлдбергера о неконструктивности множества целых чисел и уникальности единицы.
461 115688
>>5667

>Какой тип у 1?


Универсум какой-нибудь, если ты про типичное DTT и тип-синглетон.
462 115689
>>5688
А, дальше прочитал; увидел, что это был унылый говнотроллинг.
463 115690
>>5689
В чем состоит "говнотроллинг"? Если слова делают тебе бобо это еще не значит что кто-то пытается тебя затролить.
>>5681
А за observational equality сможешь пояснить своими словами?
464 115691
>>5690

>В чем состоит "говнотроллинг"?


В унылых доёбах до технических деталей каких-то теорий.
Точно так же можно визжать про то, почему в теории множеств зачастую 1 ∈ 3 и иногда (0, 0) = 2. Здравомыслящим людям там как, нормально вообще?
Можно повизжать про малые и большие множества, а заодно про классы, про необходимость городить универсум (Гротендика) ради теории категорий. А без теоремы о дедукции много доказать сможешь в Hilbert-style системе? Как, удобно?
465 115692
>>5690

>observational equality


Не знаю что это, я читал только HoTT. Интересный концепт? Пригоден для троллинга?
466 115693
>>5692
По сути HoTT без всяких многомерных штук (то есть с UIP).
467 115694
>>5693
Тогда же вообще получается скучная проггерская тема.
468 115695
>>5691

>В унылых доёбах до технических деталей каких-то теорий.


Я говорю что то что тейк про то что у чего угодно должон быть один само-собой разумеющийся тип хуйня и это не очевидно только промытым адептам теории типов. Каким хуем это техническая деталь ТТ когда это ее самая основа, ты совсем чтоли ебанько тупое?
>>5692
Пытаюсь разобраться, иногда возвращаюсь в него потыкать. Можно тралить унылых типизаторов тем что у них овер50 различных сортов равенств с которыми они сами разобраться не могут. Можно этот пассаж с ncatlab скидывать как пруф:
https://ncatlab.org/nlab/show/extensional+type+theory
Note: For a while, the nLab incorrectly used “extensional type theory” to refer to what we now call set-level type theory. If you encounter uses of this sort, please correct them.
469 115696
>>5694

>скучная проггерская тема


Как же у меня печет с ебанашки. HoTT это и есть скучная проггерская тема. А "математики" используют ZFC и вообще про основания не парятся.
470 115697
>>5695

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


А я говорю тебе, что ты хуесос и пидорас, благодаря единственности типа проще добиться завершимости алгоритма проверки типов, а в теориях, где у терма может быть много типов (ничего себе, а так не один такой умник, да?), за этим надо отдельно следить (Coq).
471 115698
>>5697

>проще добиться


Пффф проблемы типоманек, страдайте - добивайтесь, проще должно быть нормальным людям.

>завершимости алгоритма проверки типов


А кто тебе сказал что он должон завершатся? (ты ведь о разрешимости тайпчекинга) Опять транслируешь догматы швятых отцов или можешь привести какие то аргументы?

>у терма может быть много типов


>Coq


Разве там есть такое? Не припомню.
472 115699
>>5697
Кстати, обрати внимани я использовал оборот "я говорю" т.к. ссылался на раннее написанное в треде. Но ты этого не понял, но решил повторить этот оборот за мной, т.к. ты и есть тупой хуесос и пидорас у которого разорвало сраку.
grafik.png37 Кб, 749x247
473 115700
>>5698

>Пффф проблемы типоманек, страдайте - добивайтесь, проще должно быть нормальным людям.


Добейтесь тогда, чтобы в теории множеств не было хуйни вроде «1 ∈ 2». (Ты долбоёб?)

>А кто тебе сказал что он должон завершатся? (ты ведь о разрешимости тайпчекинга) Опять транслируешь догматы швятых отцов или можешь привести какие то аргументы?


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

>Разве там есть такое? Не припомню.


Доброе утро.
>>5699
Какой же ты дегенерат ебанутый.
474 115701
>>5700

>Добейтесь тогда, чтобы в теории множеств не было хуйни вроде «1 ∈ 2».


Нахуя?

>(Ты долбоёб?)


Пичот?

>Очевидно, при реализации завершающегося алгоритма можно опираться на пруф завершимости.


Напиши по-человечески что там тебе очевидно.

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


Т.е. ты представляешь себе такую гипотетическую ситуацию что - ты скармливаешь чекеру свою теорему. Он начинает чего то там бздеть-пердеть. И тут у тебя есть только два варианта - либо чекер говно, либо ты написал хуйню. Так? И вообще никаких способов выбрать одно или другое у тебя нет. Но вот если чекер исправно тебе выдает да/нет, то

> Значит уровень доверия к такому чекеру выше.


(при том что на практике чекер может точно так же сколько угодно бздеть-пердеть потому что "за конечное время" еще не значит что ты его сможешь дождаться за свою жизнь)
У тебя кашка в голове.

>Доброе утро.


Ну это мы уже реально дошли

>до технических деталей каких-то теорий


>Though Set and Type are different in Coq, this is mostly due to historical reasons



>Какой же ты дегенерат ебанутый.


Твоей мамке норм, вчера орала как последняя сучка.
grafik.png43 Кб, 755x258
475 115702
>>5701

>Нахуя?


А ради твоих хотелок кто чего добиваться должен, петушок?

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


Тупой хуесос не может понять, что ситуация «скормили терм чекеру, он зациклился, но мы не знаем, проблема в реализации или терме» предпочтительнее ситуации «скормили терм чекеру, он зациклился, но мы не знаем, проблемы в реализации, теории или терме».

>при том что на практике чекер может точно так же сколько угодно бздеть-пердеть потому что "за конечное время" еще не значит что ты его сможешь дождаться за свою жизнь


Правда что ли? Вот это да! Никогда такого не было!

>Ну это мы уже реально дошли


>>Though Set and Type are different in Coq, this is mostly due to historical reasons


Причём тут отличия Set и Type, хуесосина тупая? Ты видишь, что там красным подчёркнуто, потому что слева и справа от равенства стоят термы разных типов?
476 115704
>>5702

>А ради твоих хотелок кто чего добиваться должен, петушок?


Такая смешная тупая обиженка. А ты - А ты - А ты. Аргументов нет т.к. всякая мыслительная деятельность заменена на цитирование швятых отцов.
Должен потому что типизаторы хотят чтобы их построениями пользовались мейнстримные математики, а те в свою очередь в своей работе не различают 1:N и 1:Z и им типы только мешают. Все то надо дауненку разжевывать.
(И чтоб дауненок не квакал еще - нет 1 ∈ 2 математики не доказывают и ровно поэтому им это не мешает ничем, стрелочка не поворачивается)

>ситуация


Ты скормил терм тайпчекеру, он бздит уже второй день. Твои действия?

>Правда что ли? Вот это да! Никогда такого не было!


У долбоебушки ничего сложнее a+b=b+a не доказывавшего безусловно. Out of memory это тоже народные придания.
Напомню мы говорим про

>Значит уровень доверия к такому чекеру выше.


Т.е. ты продолжаешь настаивать что ты больше веруешь в тайпчекер потому что можно доказать что он обязательно рано или поздно остановится на любом входе. Потому что?... Даже если бы он представлял из себя миллион строк говнокода. Ну долбоебушка.

>Причём тут отличия Set и Type, хуесосина тупая? Ты видишь, что там красным подчёркнуто


Конечно я же слетал на машине времени чтобы глянут в картинку которую ты запостишь в будущем. Значит ты все таки говоришь про Universe polymorphism, который кстати тоже меняли в coq разок-другой. Чем он вообще релевантен дискуссии? Ты просто решил притащить какого то невнятного говна чтобы все думали какой ты умный. Ты случайно не конструктивный клоун? Нужно срочно проверить.
Ответь пожалуйста на простой вопрос: какое понятие более общее - Машина Тьюринга или Универсальная Машина Тьюринга.
477 115706
>>5704

>Должен потому что типизаторы хотят чтобы их построениями пользовались мейнстримные математики


Мейнстримные математики ими пользуются, несмотря на твоё кудахтанье.

>У долбоебушки ничего сложнее a+b=b+a не доказывавшего безусловно. Out of memory это тоже народные придания.


В отличие от тебя, диванного тупого хуесоса, я OOM в разных чекерах видел не раз.

>Т.е. ты продолжаешь настаивать что ты больше веруешь


Понимаешь, петушок, веруешь тут только ты, у тебя есть мантры (типов у терма должно быть много), ересь (тип должен быть один), святые отцы (настоящие™ мейнстримные математики) и отступники (проклятые программисты). В реальном же мире бывает и так (MLTT), и сяк (теории типов с subtyping), и даже в Coq’е иногда доказывают False, а в Lean так вообще фундаментальные проблемы с разрешимостью, но мейнстримные математики, о ужас, им всё равно пользуются.
И да, это не означает, что разрешимость нинужна.

>Значит ты все таки говоришь про Universe polymorphism


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

>Чем он вообще релевантен дискуссии?


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

>Ответь пожалуйста на простой вопрос: какое понятие более общее - Машина Тьюринга или Универсальная Машина Тьюринга.


Машина Тьюринга.
478 115707

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



Получается, так и не было дано определение порядка, на котором здесь даётся определение первичности. Понятное дело, что для метаязыка как прессуппозиция подразумевается язык-объект подобно тому как пресуппозицией для вопроса "перестали ли вы пить коньяк по утрам?" является утверждение "вы пили коньяк" или для "является ли король Франции лысым?" утверждение "Франция не является республикой". Но я здесь не ставлю задачей себе логический анализ языка, а ставлю задачей выставить автора тупым долбоёбом и хохлом. Поэтому я добавлю, что для целых чисел отношение "больше" абсолютно изморфно отношению "меньше", и лишь если мы добавим аксиому, что "0<1", то мы сможешь сказать, что единица меньше минус-едницы, а не наоборот. Чисто экстенционально, без учёта смысла слов "больше" и "меньше", эти отношения одинаковые. Поэтому понять, какой смысл автор-хохол вкладывает в свои слова представляется затруднительным, а сам он его сформулировать не в состоянии в силу врождённой тупости и регидности мышления.
479 115708
>>5707
Опа, дежурный петух опять вылез. Санитарам объявляется выговор.
480 115709
>>5706
Я бы вообще этот вопрос ставил таким образом, что это не бог-из-машины, а вот как лично я могу написать программу, например, на питоне чтобы считать свои формулы, например, на латексе. Что я должен знать? Какими принципами руководствоваться? И банально какие аксиомы как правила преобразования строк мне нужны?
То есть это банальное требование воспроизводимости эксперимента, а не i+1 i-1
481 115710
>>5709
Ты для начало понятие строки попробуй определить строго, многие вопросы отпадут.
482 115711
>>5710
Понятия не имею, что ты подразумеваешь под строкой. Вот у меня текстовый редактор видит \n - значит дальше новая строка. У каждого свой взгляд.
483 115712
>>5710
А вот давай погорим, что такое вообще ЗНАК. Вот в отношении SRC - MSG - DST. Вот в этих рамках. И посмотрим, что ты ск4ажешь.
484 115713
>>5706

>Мейнстримные математики ими пользуются


А про 1 ∈ 2 нечего не спизданешь еще? Ну пользуются конечно поплевываясь, куда деваться.
Только совершенно ебанутый будет утверждать что нет никаких трудностей при переносе неформальной математики в формальную когда надо дохуя всего переиначить чтобы просто запихнуть в прувер то что тебе надо. Будешь отрицать?

>OOM в разных чекерах видел не раз.


А к чему тогда были твои восклицания. Анивей, как к такому повороту отнеслись в твоей церкви Швятой Разрешимости?

>В реальном же мире бывает и так (MLTT), и сяк


Но сначала один анон спизданул что 1 это только если 1:N а по другому никак и быть не может в сам целый Мартин Леф так сказал. А потом ты закукарекал про разрешимость и... без нее тоже наверное никак?
Но если бывает и так и сяк, то у меня больше вопросов нет.

расшифруй только еще

>Очевидно, при реализации завершающегося алгоритма можно опираться на пруф завершимости.



>Coq’е у терма два разных типа бывает


Как это поможет мне определять существенно разные типы для одного терма - 1:N, 1:Z. Давай по-новой, чего ты там хотел доказать принеся какую то обскурную

>The status of Universe Polymorphism is experimental.


фичу из coq. То что чем больше фичей в теории типов тем она сложнее? Ну охуеть ты мне глаза открыл.

Ну хотя бы не конструктивный петух, так что диалог в принципе возможен.
485 115714
>>5712
Знак это клеймо на жопе мовно-конструктивной петушары.
486 115715
>>5713

>куда деваться.


Заставляют, надо понимать, жрать теорию типов?

>Только совершенно ебанутый будет утверждать что нет никаких трудностей при переносе неформальной математики в формальную


А я такое утверждал что ли?

>когда надо дохуя всего переиначить чтобы просто запихнуть в прувер то что тебе надо


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

>Будешь отрицать?


Я же не ебанутый.

>Но сначала один анон спизданул что 1 это только если 1:N а по другому никак и быть не может в сам целый Мартин Леф так сказал.


Это проблемы одного анона.

>А потом ты закукарекал про разрешимость и... без нее тоже наверное никак?


Как никак, если я тебе сам же привёл в пример Lean, у которого с ней проблемы. Разрешимость тайпчекинга — одно из хороших свойств, как непрерывность — хорошее свойство функции. Зачем вообще нужна непрерывность, без непрерывности нельзя что ли? Иногда можно, иногда нужно, точно так же как и с разрешимостью тайпчекинга (да и разрешимостью предикатов вообще). Или зачем группе коммутативность?

>расшифруй только еще


Я же уже писал. Точно так же Lean, ядро которого хорошо отделено от фронтенда (в виде парсера, elaborator’а и прочего), вызывает больше доверия, чем ядро Coq, которое перемешано с языком (языками) тактик.
Как выше верно писали, такое ещё позволяет проще «воспроизвести эксперимент». У Lean, например, есть экспортный формат, то есть ты можешь написать свой независимый чекер термов в этом формате и проверить, действительно ли пруфы из Mathlib (https://github.com/leanprover-community/mathlib4) пруфы, а не наёбка, не занимаясь восстановлением алгоритма вывода типов и сотен тактик, как это было бы в Coq’е.
Что, собственно, уже не раз делали, одна из последних попыток, например: https://github.com/digama0/lean4lean

>Как это поможет мне определять существенно разные типы для одного терма - 1:N, 1:Z. Давай по-новой, чего ты там хотел доказать принеся какую то обскурную


А разные юниверсы — это несущественно разные типы что ли, ёбаный в рот? Где проходит граница существенности?
Впрочем, то, чего именно ты хочешь, называется subtyping; хотя эти проблемы реально неплохо решаются продвинутым парсером вместе с тайпклассами (и нет, обычно их частью синтаксиса теории не делают, предвосхищая вскукареки про две разные теории на бумаге и в реализации).

>>The status of Universe Polymorphism is experimental.


Сука, блядь, какой polymorphism? Ну ты мне объясни, блядь, причём тут polymorphism? Нахуя ты его приплетаешь?
Фича, о которой я говорю, которая ломает единственность типа, называется universe cumulativity.
486 115715
>>5713

>куда деваться.


Заставляют, надо понимать, жрать теорию типов?

>Только совершенно ебанутый будет утверждать что нет никаких трудностей при переносе неформальной математики в формальную


А я такое утверждал что ли?

>когда надо дохуя всего переиначить чтобы просто запихнуть в прувер то что тебе надо


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

>Будешь отрицать?


Я же не ебанутый.

>Но сначала один анон спизданул что 1 это только если 1:N а по другому никак и быть не может в сам целый Мартин Леф так сказал.


Это проблемы одного анона.

>А потом ты закукарекал про разрешимость и... без нее тоже наверное никак?


Как никак, если я тебе сам же привёл в пример Lean, у которого с ней проблемы. Разрешимость тайпчекинга — одно из хороших свойств, как непрерывность — хорошее свойство функции. Зачем вообще нужна непрерывность, без непрерывности нельзя что ли? Иногда можно, иногда нужно, точно так же как и с разрешимостью тайпчекинга (да и разрешимостью предикатов вообще). Или зачем группе коммутативность?

>расшифруй только еще


Я же уже писал. Точно так же Lean, ядро которого хорошо отделено от фронтенда (в виде парсера, elaborator’а и прочего), вызывает больше доверия, чем ядро Coq, которое перемешано с языком (языками) тактик.
Как выше верно писали, такое ещё позволяет проще «воспроизвести эксперимент». У Lean, например, есть экспортный формат, то есть ты можешь написать свой независимый чекер термов в этом формате и проверить, действительно ли пруфы из Mathlib (https://github.com/leanprover-community/mathlib4) пруфы, а не наёбка, не занимаясь восстановлением алгоритма вывода типов и сотен тактик, как это было бы в Coq’е.
Что, собственно, уже не раз делали, одна из последних попыток, например: https://github.com/digama0/lean4lean

>Как это поможет мне определять существенно разные типы для одного терма - 1:N, 1:Z. Давай по-новой, чего ты там хотел доказать принеся какую то обскурную


А разные юниверсы — это несущественно разные типы что ли, ёбаный в рот? Где проходит граница существенности?
Впрочем, то, чего именно ты хочешь, называется subtyping; хотя эти проблемы реально неплохо решаются продвинутым парсером вместе с тайпклассами (и нет, обычно их частью синтаксиса теории не делают, предвосхищая вскукареки про две разные теории на бумаге и в реализации).

>>The status of Universe Polymorphism is experimental.


Сука, блядь, какой polymorphism? Ну ты мне объясни, блядь, причём тут polymorphism? Нахуя ты его приплетаешь?
Фича, о которой я говорю, которая ломает единственность типа, называется universe cumulativity.
487 115716
>>5715

>Заставляют, надо понимать, жрать теорию типов?


Да, можно и так сказать. Когда математику надоедает марать бумагу он лезет посмотреть какие там пруверы самые модные и молодежные. И видит там - coq, agda, lean... Приходится жрать что дают.
Видел тезис что если бы в безтиповые пруферы вливали бы столько же средств то и они бы были тоже вполне конкурентны.

>Разрешимость тайпчекинга — одно из хороших свойств, как непрерывность — хорошее свойство функции.


Пример у тебя абсолютно ебанутый. Даже не знаю что еще сказать.

>Точно так же Lean, ядро которого хорошо отделено от фронтенда


Да какое блядь это имеет отношение к разрешимости. Ты совсем дурачек и не понимаешь что никакого или просто пишешь хуйню лишь бы написать побольше хуйни?
Тебе часто в детстве говорили что ты какой то тупенький?

>А разные юниверсы — это несущественно разные типы что ли, ёбаный в рот?


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

>Сука, блядь, какой polymorphism?


Кек знал что у тебя опять подорвет. Я мог бы написать как одно отменяет другое, ну да похуй. Я еще раз повторяю - нахуя ты его притащил, чудик? Чего хотел этим доказать?
488 115717
>>5716

>Видел тезис что если бы в безтиповые пруферы вливали бы столько же средств то и они бы были тоже вполне конкурентны.


Тут спорить не буду, вполне возможно, да.

>Пример у тебя абсолютно ебанутый. Даже не знаю что еще сказать.


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

>Да какое блядь это имеет отношение к разрешимости. Ты совсем дурачек и не понимаешь что никакого или просто пишешь хуйню лишь бы написать побольше хуйни?


Сука, ну такая же мотивация, блядь, что ядро маленьким делать, что разрешимости добиваться. Ты реально не понимаешь?

>Тебе часто в детстве говорили что ты какой то тупенький?


У тебя комплексы какие-то?

>Я мог бы написать как одно отменяет другое, ну да похуй.


Что кого? Без (universe) полиморфизма не бывает кумулятивности? Без кумулятивности не бывает полиморфизма? Так ты же дегенерат.

>Но ведь ты прекрасно понял о чем я, зачем тогда опять включаешь дурачка?


Так это не ты верещал, что всем директивно спустили необходимость иметь каждому терму ровно один тип?

>Чего хотел этим доказать?


>>в Coq’е у терма может быть много типов


>>привожу пример


>аррряяя ПОЛИМОРФИЗМ аррряяяя


Я пишу тебе, блядь, бывает у терма много типов, даже в, казалось бы, Coq’е (но не только там), хоть и не в той форме, какой тебе надо, но у тебя почему-то от этого истошный визг.
489 115718
>>5717

>>Пример у тебя абсолютно ебанутый. Даже не знаю что еще сказать.


>Ну и в чём разница? У теорий типов точно так же есть синтаксис, как у, например, групп, и точно так же есть модели.


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

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


Теперь при более детальном рассмотрении я вижу что в нем столько нонсеквитуров что даже лениво их все разбирать.

>Сука, ну такая же мотивация, блядь, что ядро маленьким делать, что разрешимости добиваться. Ты реально не понимаешь?


Тяжело понять бред от безмозглого дебила. Маленькое ядро может реализовывать неразрешимую систему типов. Это вообще ортогональные консерны, можешь ты это уже понять ебаклак?

>>Я мог бы написать как одно отменяет другое, ну да похуй.


>Что кого? Без (universe) полиморфизма не бывает кумулятивности? Без кумулятивности не бывает полиморфизма? Так ты же дегенерат.


Сам себе напридумывал. Сам же себе и подибил. Главное по плечу себя не забудь похлопать какой ты у мамки молодец.

>хоть и не в той форме, какой тебе надо


>но у тебя почему-то от этого истошный визг.


Ору с даунича. Может потому что

>не в той форме, какой тебе надо


Не? Может попробуешь в какой надо форме принести чтобы не было никаких визгов? Но я понял твой модус-операнди это спиздануть какую то слайтли-релейтед хуету и пытаться делать умный вид.
490 115719
>>5718
Какой же ты непрошибаемо тупой хуесос.

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


Я уже написал, что необязательно, ты это прочитал, но уже, видимо, забыл.

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


А, так это ты, хуесосина полуграмотная? Иди нахуй отсюда, уёбок тупой.

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


А где я писал обратное, дебилушка? Покажешь?

>Это вообще ортогональные консерны, можешь ты это уже понять ебаклак?


Опять ты жопой прочитал, но сделал далеко идущие выводы.

>Сам себе напридумывал.


Так ты напишешь, кто кого отменяет? Зачем-то начал верещать про полиморфизм, а теперь загадочно умалчиваешь, зачем, делая вид дохуя специалиста.

>Может попробуешь в какой надо форме принести чтобы не было никаких визгов?


Верещал нагло придуманную хуйню про

>У каждого объекта должен быть только один тип и задается он при определении? Вы че ебанутые?


А теперь оправдывается, что он, видите ли, на самом деле, про subtyping говорил. Просто говна поешь.
491 115721
>>5719

>А, так это ты


Кто? У тебя делирий?

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


>А где я писал обратное, дебилушка? Покажешь?


Нахуй ты вообще притащил свое маленькое ядро, клоунесса ебаная.

>Зачем-то начал верещать про полиморфизм, а теперь загадочно умалчиваешь, зачем, делая вид дохуя специалиста.


Очевидно чтобы сральню тебе разворотить. Как видишь план удался.

>>У каждого объекта должен быть только один тип и задается он при определении? Вы че ебанутые?


>А теперь оправдывается, что он, видите ли, на самом деле, про subtyping говорил.


> на самом деле, про subtyping говорил.


Чего блядь? Энивей, я же тебе говорю показывай теорию типов в которой рутинно объявляют один объект с разными типами вроде

>1 это натуральное число. А так же это целое число. И нечетное число.


А свой исторический флюк с coq'овским Set-Prop-Type-MProp(?)-сабтайпами для них и чего они там еще нахуевертели засунь себе в разорванную сральню откуда ты их вынул.
492 115722
>>5721
Можешь не продолжать, я уже узнал тебя по твоим неуместным латинизмами, долбоёб.

>Энивей, я же тебе говорю показывай теорию типов в которой рутинно объявляют один объект с разными типами вроде


Хули тебе показывать, если ты всё равно нихуя не понимаешь.

>А свой исторический флюк с coq'овским Set-Prop-Type-MProp(?)-сабтайпами для них и чего они там еще нахуевертели засунь себе в разорванную сральню откуда ты их вынул.


Что вот это предложение ярко и демонстрирует. Исторический флюк у него, блядь, во дегенерат.
493 115723
>>5722

>Можешь не продолжать, я уже узнал тебя по твоим неуместным латинизмами, долбоёб.


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

>Хули тебе показывать, если ты всё равно нихуя не понимаешь.


На самом интересном месте слился, жаль.

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


Контр-аргументы? Будешь утверждать что в coq не нахуевертели говна? Ты похоже еще на десяток ийсикю пунктов отупел от бессильной злобы.
494 115724
>>5723
Продолжай мриять, что не насрал хуйни, а филигранно затроллил.

>Будешь утверждать что в coq не нахуевертели говна?


Хули ты на ходу придумываешь тезисы, пидорас-хуесос-говноед? Вот где про это речь шла?
495 115725
>>5724
Чет маня совсем слилась. Думал манька будет получше. Но очень плохая манька попалась, некачественная к сожалению.
496 115726
>>5725
Чё там MProp?
497 115727
>>5726
Хорошо, не болеет.
498 115971
Линейный морфизм пучков.
499 115972
>>5727
Чего не скажешь о Сохацком подцепившем сифилис в ТЦК.
500 116184
Обновить тред
« /math/В начало тредаВеб-версияНастройки
/a//b//mu//s//vg/Все доски

Скачать тред только с превьюс превью и прикрепленными файлами

Второй вариант может долго скачиваться. Файлы будут только в живых или недавно утонувших тредах.Подробнее