сегодня праздник у девчат

[juan_gandhi]

Закончил свою логику. (Ну там тесты еще всю ночь побегут, но это фигня, мираж.)

Comments

[rampitec]

Зачем?

[chuka_lis]

congrats)

[juan_gandhi]

Надо.

[juan_gandhi]

Thanks!!!

[anhinga_anhinga]

Класс!

А как получается, что всю ночь? Какая-то автогенерация очень большого количества тестов? Или очень нетривиальные/длинные задачи?

[juan_gandhi]

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

[rampitec]

Суров!

[rampitec]

В идеале истину надо проверять всю жизнь. И умереть за это. Но на всю жизнь оно, правда не тянет, это же не { return true; }

[spamsink]

Re subject: в гости кто пришёл?

[anhinga_anhinga]

Вот, вот, тут недавно оказалось, из ссылки в комментариях, что мы все стали понимать интуиционизм прагматично-современным образом (есть в классической математике алгебры открытых множеств топологических пространств и прочие алгебры Гейтинга, и с ними связана прелестная не вполне стандартная логика, а так ничего особенного, часть стандартной математики), а оказывается, основатель его имел в виду гораздо более радикальную интерпретацию: "The dependence of intuitionism on time is essential: statements can become provable in the course of time and therefore might become intuitionistically valid while not having been so before."

Так что, надо долго тестировать!

https://plato.stanford.edu/entries/intuitionism/

via

https://timelets.dreamwidth.org/1042186.html

[utochka]

Глыба

[juan_gandhi]

Good point!

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

Время - частный случай такого домена.

[juan_gandhi]

Удача.

[juan_gandhi]

Второй том!

[utochka]

:-)

[thedeemon]

А видели Rydeheard, Burstall "Computational Category Theory"?
http://www.cs.man.ac.uk/~david/categories/book/book.pdf
У них там код на ML, может быть интересно сравнить подходы, наверняка все иначе сделано.



...

[juan_gandhi]

О, красиво! Черт, и как компактно!

[thedeemon]

Young-il Choo сегодня ее же вспомнил, занятно. Спасибо за митап!

[juan_gandhi]

Да, надо почитать будет; жаль, ML для меня как канджи немножко.