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

[juan_gandhi]

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

Comments

[anhinga_anhinga]

Класс!

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

[juan_gandhi]

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

[rampitec]

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

[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

[juan_gandhi]

Good point!

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

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