Зависимые типы, гомотопии и прочие ужасы
От: HrorH  
Дата: 12.07.12 13:54
Оценка:
Недавно наткнулся на интервью с математиком Владимиром Воеводским здесь
Очень заинтересовало использование понятий из топологии в теории типов.
A также то, что все это можно использовать в Coq.
Что может показаться странным, если учесть, что не знаю ни то ни другое, ни третье.

Отсюда вопрос: кто-нибудь здесь есть, кто настолько хорошо знает математику, что может понять, о чем идет речь, и рассказать на простом русском языке?

Если что, есть еще видео здесь

Ключевые слова: унивалентные основания математики, Homotopy Type Theory, Steve Awodey и др.
Re: Зависимые типы, гомотопии и прочие ужасы
От: batu Украина  
Дата: 12.07.12 14:41
Оценка:
Здравствуйте, HrorH, Вы писали:

HH>Недавно наткнулся на интервью с математиком Владимиром Воеводским здесь

HH>Очень заинтересовало использование понятий из топологии в теории типов.
HH>A также то, что все это можно использовать в Coq.
HH>Что может показаться странным, если учесть, что не знаю ни то ни другое, ни третье.

HH>Отсюда вопрос: кто-нибудь здесь есть, кто настолько хорошо знает математику, что может понять, о чем идет речь, и рассказать на простом русском языке?


HH>Если что, есть еще видео здесь


HH>Ключевые слова: унивалентные основания математики, Homotopy Type Theory, Steve Awodey и др.


Ну, вот на видео он и рассказывает о том что это такое.. Очень интересно, но у меня тормозит жутко.. Можешь мне скачать это видео? Буду ужасно благодарен.. Ну, и естественно, расскажу здесь что я понял.. Мыло я дам.
Re[2]: Зависимые типы, гомотопии и прочие ужасы
От: HrorH  
Дата: 12.07.12 14:50
Оценка:
Здравствуйте, batu, Вы писали:

B>Ну, вот на видео он и рассказывает о том что это такое.. Очень интересно, но у меня тормозит жутко.. Можешь мне скачать это видео? Буду ужасно благодарен.. Ну, и естественно, расскажу здесь что я понял.. Мыло я дам.


Вечером попробую из дома. Хотя час видео по мылу как-то не разу отправлять не приходилось.
Пока можно без видео почитать: здесь
Re[3]: Зависимые типы, гомотопии и прочие ужасы
От: batu Украина  
Дата: 12.07.12 15:24
Оценка:
Здравствуйте, HrorH, Вы писали:

HH>Здравствуйте, batu, Вы писали:


B>>Ну, вот на видео он и рассказывает о том что это такое.. Очень интересно, но у меня тормозит жутко.. Можешь мне скачать это видео? Буду ужасно благодарен.. Ну, и естественно, расскажу здесь что я понял.. Мыло я дам.


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

HH>Пока можно без видео почитать: здесь
По английски сложно будет.. Тут же он все заново определяет..Хер его знает что.. на еще и на английском
Re[4]: Зависимые типы, гомотопии и прочие ужасы
От: HrorH  
Дата: 12.07.12 16:37
Оценка:
Здравствуйте, batu, Вы писали:

B>По английски сложно будет.. Тут же он все заново определяет..Хер его знает что.. на еще и на английском


А можно еще дурацкий вопрос: там можно же на сайте ткнуть там где написано "видеозаписи" (справа) правой кнопкой и выбрать в меню "Save as target".
Не проще ли так сделать?
Хотя если у Вас не получится попробую отправить через filedropper.com
Re[5]: Зависимые типы, гомотопии и прочие ужасы
От: batu Украина  
Дата: 12.07.12 17:27
Оценка:
Здравствуйте, HrorH, Вы писали:

HH>А можно еще дурацкий вопрос: там можно же на сайте ткнуть там где написано "видеозаписи" (справа) правой кнопкой и выбрать в меню "Save as target".

HH>Не проще ли так сделать?
HH>Хотя если у Вас не получится попробую отправить через filedropper.com
ступил. пытался правой кнопкой через даунлоад.. Уже качаю
Re: Зависимые типы, гомотопии и прочие ужасы
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 24.05.13 08:51
Оценка: 16 (1) +1
Здравствуйте, HrorH, Вы писали:

HH> рассказать на простом русском языке?


Вот попытка изложить азы:
http://thedeemon.livejournal.com/65083.html
На простом как-то не очень получается, но хоть большей частью по-русски.
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.