Сообщений в теме: 140

[Саблин]

Если так, то вот Вам математическая задачка.

 

Дано: живёт человек в РФ. В глубинке. Зарплата 7-15 тыс. руб. Место может легко потерять. Безработица запредельная. И таких, как он, вокруг подавляющее большинство. Хотя немало и тех, у кого экономическая ситуация много лучше, есть связи, есть "непотопляемость" и всё такое прочее. Но для простого человека ситуация с каждым годом лишь ухудшается, т.к. и цены растут (а зарплата - нет), и всё новые и новые "препоны" для его выживания законодательно вводятся...

 

Вопрос: и как ему с этим быть? Как растить и обучать детей, как радоваться жизни именно в то время, пока живёшь на этой планете - именно в этом месте и в это время?

 

Сможете чего-нить толкового предложить?

марксизм.

[AndyN]

Как, собственно, гомотопическая теория типов в роли основы естествознания? Стоит вообще забивать ею себе мОзги?

[tickosen]

Как, собственно, гомотопическая теория типов в роли основы естествознания? Стоит вообще забивать ею себе мОзги?

 

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

 

По мне -- интересно. С точки зрения связи с вычислимостью, на тот момент, когда я смотрел -- аксиома унивалентности требовала экстенциального равенства. 

 

Интересно Вам будет, если вообще считаете конструктивную, proof relevant математику интересной (доказательства -- такие же математические объекты и т.д.)

 

Если есть свободное время -- почитайте. Если сама концепция ∞-группоидов понятна -- подумайте над (X = Y) ≃ (X ≃ Y) в контексте размышлений о высоком и как жить без K-аксиомы. 

 

 

В последних частях книги -- выражение многих конструкций математики в терминах HoTT.

 

К сожалению, я в последний раз смотрел в эту сторону лет так 5-6 назад, но спасибо, что напомнили

 

Концепция интересная, особенно с учетом всего движняка вокруг программы Воеводского (включая книгу и формализованные версии теории в открытом доступе):

 

Исходники книги

 

Библиотека с доказательствами на Coq (Coq основан на Calculus of Coinductive constructions)

 

Библиотека с доказательствами на Agda (Agda основана на MLTT, точнее, её intensional варианте)

 

Во всяком случае в Agda внесено множество изменений для поддержки работы в каркасе HoTT

Сообщение отредактировал tickosen: 30 Декабрь 2018 - 14:19

[tickosen]

Как, собственно, гомотопическая теория типов в роли основы естествознания? Стоит вообще забивать ею себе мОзги?

 

Извините за вопрос, а Вы с теорией категорий знакомы? 

[AndyN]

Извините за вопрос, а Вы с теорией категорий знакомы?

Нет, увы

[tickosen]

Нет, увы

 

Для занятия мозгов, возможно, советую больше, чем HoTT для начала.

 

У Вас знания в какой области? Что-то из IT? 

[AndyN]

Для занятия мозгов, возможно, советую больше, чем HoTT для начала.
 
У Вас знания в какой области? Что-то из IT?

Да. Я разрабатываю интегральные схемы.

[tickosen]

Да. Я разрабатываю интегральные схемы.

 

Здорово. И задумываетесь о формальной верификации. 

 

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

[AndyN]

За книгу спасибо. Читается на одном дыхании. Еще и выучу Хаскелл в процессе

[Саблин]

Как, собственно, гомотопическая теория типов в роли основы естествознания? Стоит вообще забивать ею себе мОзги?

точнее определите. основу чаво.

Че в вашем случае есмь естество знание.

[AndyN]

точнее определите. основу чаво.

Че в вашем случае есмь естество знание.

 

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

[Саблин]

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

мова? 

Сообщение отредактировал Саблин: 30 Декабрь 2018 - 21:32

[AndyN]

мова? 

 

Ката!

[Саблин]

Ката!

Етитская сила!!!! НЕЕЕЕЕЕЭЭЭЭТ!!!! ТОЛЬКОНЕЭТО!!!!

[AndyN]

Етитская сила!!!! НЕЕЕЕЕЕЭЭЭЭТ!!!! ТОЛЬКОНЕЭТО!!!!

 

А как еще каратюги знание передають??

[Саблин]

А как еще каратюги знание передають??

Рукоположением.

на ощупь. 21 плюс.

[tickosen]

 Есмь универсальный язык, на котором можно формулировать любое знание. 

 

Гёдель не разрешает. 

За книгу спасибо. Читается на одном дыхании. Еще и выучу Хаскелл в процессе

 

na zdorovie

[AndyN]

Гёдель не разрешает. 

 

Гёдель, мля... Гёдель мне раз чуть мозги не поломал. Те высказывания, которые Гедель запрещает доказать или опровергнуть, не играют роль для нас, простых смертных. Нам нужно-то совсем ничего, математика там, информатика, физика...

[tickosen]

Гёдель, мля... Гёдель мне раз чуть мозги не поломал. Те высказывания, которые Гедель запрещает доказать или опровергнуть, не играют роль для нас, простых смертных. Нам нужно-то совсем ничего, математика там, информатика, физика...

 

AndyN, а как у Вас всё это устроено? Verilog / VHDL какой-нибудь или это всё прошлый век давно?

[AndyN]

AndyN, а как у Вас всё это устроено? Verilog / VHDL какой-нибудь или это всё прошлый век давно?

 

VHDL... Тест бенч - UVM... Формальная верификация - SVA...