worth reading (and thinking about)

 Body

почему лямбда-калкулюс нельзя смоделировать в виде функций на множествах

Лямбда-калкулюс состоит из термов, каковые бывают или переменными (x, y, z), или абстракциями (λv.M, где v - переменная, а M - терм), или аппликациями, (M N, где M и N - термы).
Например, λf.(λx.f(xx))(λx.f(xx))
В первой половине 20-го века народ ломал головы - ну а как же это выразить в теории множеств-то?
Ну вроде бы речь идет о функциях. Ну пусть каждая переменная обозначает функцию, и каждое выражение обозначает функцию (где свободные переменные - под лямбдой).
Ну и вообразим на минутку, что мы лямбда-калкулюс моделируем в теории множеств, и каждый лямбда-терм M моделируется функцией f_M. Тогда терм M M будет моделироваться значением f_M(f_M). Это мы функцию применяем к самой себе. Ну чо, на языках программирования можно же.
Но штука такая, что в теории множеств, кроме множеств, ничего нету. Так что f_M - это какое-то множество, а т.к. оно у нас функция, то это множество пар. И раз она применима к самой себе, то компонентой одной из таких пар является сама f_M.
И что теперь? Пары в теории множеств моделируются как множества, (a,b) = {{a}, {a,b}}. Так что у нас получается, что f_M ∈ (f_M, ?) ∈ f_M. Вы видим цепочку, где множество является элементом элемента самого себя. Такие множества называются Квайнами, и они запрещены в приличных теориях множеств (Цермело-Френкеля, например). Ну и все, фокус не удался. В частности, не удался и фокус смоделировать язык программирования в теории множеств с помощью просто функций.
Не, на самом деле, смоделировать потом таки удалось - когда Дана Скотт придумал топологию Скотта. Короче, все не так-то просто в нашем дискурсе.
Есть вопросы?

недопонимание

В учебнике - "

je

 

porte

 

des

 

gants

 

pour

 

sortir

." - я так, ой, а зачем?