AG
ну классическая логика она слишком "симметричная" и у неё очень расплывчатое отрицание
Size: a a a
2020 October 23
AG
если пробовать напрямую делать для неё вычислительную интерпретацию, начинают всякие свойства плыть
AG
например может оказаться так что, программа, "классически" типизированная неконфлюэнтна - один раз запустили и получили 2, а второй раз - 3
AG
хотя в самой программе никаких случайных чисел нет, просто вот так работает редукция
DF
А откуда такие странности
DF
Логика говно значит
DF
Надо интуицией жить теперь
AG
она не то чтобы говно, просто "слишком сильная"
DF
Доказательно?
AG
соответствующие ей алгебраические структуры схлопываются в тривиальные
AG
ну да, вот ключевой вопрос насчёт того же исключенного третьего
AG
в классической логике он разрешим для всего
AG
то есть вы всегда должны мочь написать программу типа
(A : Type) -> Either A (Not A)AG
а как её написать если например A это функция
DF
Очень интересные у вас знания
DF
А где можно так же научиться по этому конкретному вопросу?
AG
книжки по логике читать :)
DF
А, это по логике получается?
AG
ну да, я ж про логику всё это время рассказывал
DF
Я то думал она скучная