(no subject)

Сегодня семинарчик открылся по формальным основам программирования. Как и в прошлом году, опять почти про хаскель, но более абстрактно, чтобы лучше понимать что и зачем. Узнал, что есть три вида семантики и существует ужасный парадокс

(\x.F(xx))(\x.F(xx)) = F((\x.F(xx))(\x.F(xx)))

то есть любая функция F должна иметь неподвижную точку (точку, в которой значение функции равно самой этой точке, либо такой же функции, программе, если мы над ними преобразования производим). А это несправедливо по отношению к функции отрицания, например.

Upd. Литература.
Барендрегт X. Ламбда-исчисление.
В частности, конструкции ламбда-исчисления воспитывают интуицию, позволяющую ориентироваться в семантике языков программирования. Эта книга написана для логиков, математиков, специалистов по информатике и философов.