* * *

Jun. 20th, 2017 07:57 pm
bamalip: (Default)
david-christiansen дает советы для команды lean по поводу введения макросов:
https://github.com/leanprover/lean/issues/1674

* * *

Jun. 20th, 2017 09:23 am
bamalip: (Default)
Во что может превратиться ваша квартира без отдельного помещения для майнинга:

* * *

Jun. 19th, 2017 07:04 pm
bamalip: (Default)
я всегда говорил, что это выучить невозможно, проще копипастить из таблички:

http://people.inf.elte.hu/divip/AgdaTutorial/Symbols.html

https://github.com/banacorn/agda-mode/blob/master/src/keymap.ts

* * *

Jun. 18th, 2017 07:38 pm
bamalip: (Default)
Mariza. O Amarelo da Carris. Мариза. Желтый трамвай.



"Эта редкая запись с диска "Novo Homem da Cidade", который вышел в 2004 году и был посвящен 20 летию со дня ухода из жизни великого Ари душ Сантуша и 25-летию первого исполнения его фаду "Um Homem na Cidade" Карлушем ду Карму."

* * *

Jun. 17th, 2017 06:54 pm
bamalip: (Default)
(немного бытовое)

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

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

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

но в принципе разбаловала нас смычка интернета и сферы услуг, разбаловала, не так давно вообще было бы непонятно, чем это я недоволен.
bamalip: (Default)
с утра для достижения комфортного звучания приходится ставить звук на максимум

вечером тот же уровень уже неприятен и нужно прикрутить в несколько раз

в середине дня эффект еще интереснее - несколько минут слышимость слабая и сразу ставишь на максимум, но вскоре слух обостряется и прикручиваешь обратно

* * *

Jun. 15th, 2017 08:31 pm
bamalip: (Default)
Юлий Буркин - Автобиография.
http://burkin.rusf.ru/books/avtobiogr/biogr.htm

* * *

Jun. 13th, 2017 04:56 pm
bamalip: (Default)
Воеводский в последние дни разошелся в хорошем смысле:
https://arxiv.org/find/math/1/au:+Voevodsky_V/0/1/0/all/0/1

Сможем ли мы переплюнуть современного классика?..

* * *

Jun. 11th, 2017 05:19 pm
bamalip: (Default)
Давайте о чем-то хорошем и простом поболтаем. О математике.

Отставив в сторону философские талмуды (иногда захожу на stackexchange в раздел philosophy-of-mathematics - исключительно посмеяться, какие вопросы волнуют иных людей), зададимся основным вопросом математики (смех в зале), что первично - логика или абстракция? Чем определяется математика, той или этой? Почитав у френдов эссе на эту тему, решил что хотел бы выразиться по-другому.

Абстракция есть везде в человеческой деятельности и мышлении. Но её нужно правильно приготовить! Абстракция - это не просто решение забыть часть описания ситуации. Это еще и умение вспомнить забытую часть в исходном виде, подставить ее в абстрактное утверждение, получить конкретный ответ. Абстрактное рассуждение хорошо не только и не столько тем, что оно минималистично, но и тем, что оно всеобщно. Единожды научившись умножать в столбик, интегрировать суммы или использовать силлогизмы, мы сможем умножать или интегрировать что-угодно. Да что там умножать, хотя бы считать. Если мы умеем считать, то это значит - считать и яблоки, и орехи, и оленей, и белок, и членов парламента. Если посчитать яблоки получилось, а членов парламента уже нет, то это сразу звоночек о том, что что-то не так - или с нашим умением считать, или с парламентом.

Такое качественное построение абстракции делает ее результат моделью - т.е. точным, адекватным описанием исходного сложного исследуемого объекта. Если использование абстракций вообще свойственно всем людям, в особенности - базарным бабам (см. диссертацию Гегеля), то уже строгое моделирование свойственно прежде всего наукам, но снова всем наукам, а не только математике. Где же здесь место математики?

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

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

* * *

Jun. 11th, 2017 05:07 pm
bamalip: (Default)
Відписався щойно від Леді Діани.

Читав її блог більше десяти років, іще коли він був у ЖЖ. Але зараз тотальний токсичний негативізм. "Все навкого погано". Вже й у безвізі їй щось нетак. Людина або співає під чужу дудку, або перевтомилася, і їй треба на рік в антарктиду до пінгвінів, відпочити. Але вказувати їй на це нема сенсу, людина завжди робить те, що вважає за потрібне.

* * *

Jun. 9th, 2017 11:40 am
bamalip: (Default)


UPD: nationalpost.com:
bamalip: (Default)
Известно, что модели теорий зависимых типов это LCCC (с вариациями в формулировках, основанных на расслоенных категориях). Вопрос в том, как правильно определять это "LCCC". Потому как в монографиях Курьена или Джеккобса это все долго и нудно. Во-первых хочется, чтобы работало с линейными типами (программирование квантовых нововведений и все такое; ну и обычные языки этой темой начали интересоваться), т.е. недекартово обобщение, во-вторых, чтобы бодро и современно, а не ещё одна монография на тыщу страниц с диаграммным поиском. А то Гротендик, конечно, молодец со своей "йогой шести операций", но там опять же нудно и долго, потому что через 1-категории, потому что в то время, когда это писалось, ничего адекватнее не было. Но сейчас замечательно. Получается сформулировать удивительно просто - это высшая кубическая замкнутая категория, тонкости только в том, в каком виде высшая и в каком смысле замкнутая, чтобы все остальное вылезало отсюда автоматом.

Сермяжная польза такая, что получается, можно получить отсюда трансляции между языками ТК и вариантов ТТ, представляя синтаксис ТТ как инициальную высшую категорию с подходящей структурой. Ну, это общие слова про модную тему, сейчас много кто здесь ведет раскопки. В качестве немедленных результатов - категория для классической SystemF, и как результат решение скандала с Хаскеллем. Немедленно получается какой-то относительно простой вариант равенства. Можно удобно в таком сеттинге формулировать то, чем я занимался в прошлом году (хотя кому это нужно). Мне интереснее, что можно продвигаться в плане юзабельного языка на чистых топосах, с одной стороны, и в плане языковых механизмов для "ad-hoc полиморфизма" без этого ужасного резолвинга инстансов тайп-классов.

Еще хотелось бы перенести обратно на категории известные доказательства нормализуемости/cut-elimination. Для мета-разбирательств с тотальностью/консистентностью, как обычно. Не уверен, что в этом присутствует большой смысл, но имеется такой жанр и мода на него тоже не утихает. Интересно, в частности, насколько безопасны сильные формы universe polymorphism-а для случая очень предикативных иерархий.

Profile

bamalip: (Default)
шерстяной ленин

June 2017

S M T W T F S
    123
45 678 910
1112 1314 15 16 17
18 19 2021222324
252627282930 

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jun. 24th, 2017 06:49 pm
Powered by Dreamwidth Studios