История λ-исчисления уходит в начало прошлого века. Этимология названия данного раздела математической логики, который служит основой для «computer science», следующая. Сам значек «λ» используется для одной из двух основных конструкций в созданной Черчем системе — абстракции. Оказывается, что выбор обозначения абстракции не был совершенно случайным, а сделан в противопоставление другой более ранней конструкции, которую использовали Whitehead и Russell и обозначали как «xˆ». Для новой конструкции, чтобы отличать ее от прежней, Черч заменил обозначение сначала на «∧x», а затем — на «λx», очевидно, интерпретировав первый символ как заглавную букву «Λ», для упрощения набора.
Опишем кратко систему λβη, то есть классическое бестиповое экстенсиональное λ-исчисление, сделав конспект классической монографии по λ-исчислению (Х. Барендрегт, «Ламбда-исчисление. Его синтаксис и семантика», перевод с английского Г. Е. Минца под редакцией А. С. Кузичева, Москва, «Мир», 1985).Читать полностью »
