AZ
В хаскеле не работает
в формалити работает, а оно бета-редцуируется, я думал в хачкеле так же
Size: a a a
2019 December 22
AK
not (логический) :: a - > Void
AZ
AZ
not (логический) :: a - > Void
Void это начальный объект, в него не может идти стрелок
KV
Void это начальный объект, в него не может идти стрелок
Ещё как может
KV
Например, из другого начального объекта
AZ
но не из forall a.
KV
но не из forall a.
А, ну да, там что-то странное написано
KV
Можно определить
type Not a = a -> VoidA
Например, из другого начального объекта
В любой объект идет стрелка из него самого)
A
Называется id
AK
Is Curry-Howard correspondent of double negation ((a->r)->r) or ((a->⊥)->⊥)? - Stack Overflow
https://stackoverflow.com/questions/30008910/is-curry-howard-correspondent-of-double-negation-a-r-r-or-a-%E2%8A%A5-%E2%8A%A5
https://stackoverflow.com/questions/30008910/is-curry-howard-correspondent-of-double-negation-a-r-r-or-a-%E2%8A%A5-%E2%8A%A5
AK
Не сам придумал, отсюда взял
AZ
Is Curry-Howard correspondent of double negation ((a->r)->r) or ((a->⊥)->⊥)? - Stack Overflow
https://stackoverflow.com/questions/30008910/is-curry-howard-correspondent-of-double-negation-a-r-r-or-a-%E2%8A%A5-%E2%8A%A5
https://stackoverflow.com/questions/30008910/is-curry-howard-correspondent-of-double-negation-a-r-r-or-a-%E2%8A%A5-%E2%8A%A5
но ведь боттом это не воид вроде
KV
но ведь боттом это не воид вроде
В этом контексте воид
AZ
еще и контексты у вас
AZ
понятно почему теоркат никто не учит)
NR
Можно пробовать ослабить формулировки теорем и смотреть что ломается в доказательстве, подбирать контрпримеры
Обучение на контрпримерах удваиваю, весьма действенная вещь, выкорчёвывающая неправильную интуицию. Становится понятно, почему все элементы определения действительно нужны.
KV
Напридумывают слов, поди разберись, что значит!
AK
Обучение на контрпримерах удваиваю, весьма действенная вещь, выкорчёвывающая неправильную интуицию. Становится понятно, почему все элементы определения действительно нужны.
А есть какие статьи по ТК с контрпримерами на примете?