Немножко про всякие равенства

[deni_ok]

 
В современной теории типов выделяют два основных класса равенств: Definitional equality и Propositional equality. 

Comments

[nivanych]

А как же observational?...

[deni_ok]

Пускай Epigram 2 выкатывают, тогда и напишу :)

[nponeccop]

К перу ещё надо бы Бенгта нашего Норстрома присовокупить:

http://www.cse.chalmers.se/research/group/logic/book/

Там как раз идея интенсиональности-экстенсиональности в деталях разобрана.

[deni_ok]

Да, я сейчас посмотрел - полезная книжка. Мне их терминология не нравилась, они называют set то, что стоило бы называть type.

[nponeccop]

А я наоборот считаю, что Пер зачем-то назвал типами то, что всегда было множествами.

Педагогически это уменьшит путаницу в типах 1-5 (см. http://nponeccop.livejournal.com/297483.html), привьет мысль о том, что типы - это абстрактные метки произвольной природы.