Я пытаюсь понять, какова связь между лямбда-исчислением и лямбда-выражениями в C ++.
Прежде всего, в нетипизированном лямбда-исчислении у нас нет «базовых значений», таких как булевы, целые или whatevr, поэтому все должно быть закодировано как функция, а затем мы можем применить любой термин к любому другому термину, что не совсем так. в C ++ когда-то у него есть система типов.
Более того, я видел, что лямбда-выражения либо преобразуются в указатели на функции (когда они ничего не захватывают), либо в функторы (классы с единственной целью — обертывание функций).
Поэтому мне интересно, является ли «лямбда-выражение» просто причудливым именем для анонимных функций, и, таким образом, оно будет напоминать лямбда-исчисление (в том смысле, что термины в лямбда-выражениях можно рассматривать как неназванные функции), или это еще не все?
Заранее спасибо.
Церковь Алонзо сделала больше, чем просто изобрела лямбду исчисление — он придумал
полезная запись для функций, лямбда-нотация, которую он описывает на стр. 5-7 своей книги 1941 года по лямбда-исчислению [1]:
Чтобы взять пример из теории функций натуральных чисел,
рассмотреть выражение . Если мы скажем, «больше 1000 «, мы делаем заявление, которое зависит от Икс и на самом деле не имеет никакого смысла, если Икс определяется как некоторое конкретное натуральное число. С другой стороны, если мы скажем, «является примитивной рекурсивной функцией, «мы делаем определенное утверждение, значение которого никоим образом не зависит от определения переменной Икс (так что в этом случае Икс играет роль очевидной или связанной переменной). … Мы будем
далее различать, используя … как обозначение соответствующей функции….
В 1950-х, когда Джон Маккарти разрабатывал Lisp, он принял нотацию Черча. Его статья 1960 года, описывающая Лисп, объясняет:
Функции и формы. В математике обычно — вне математической логики — неточно употребляют слово «функция» и применяют его к таким формам, как y ^ 2 + x. Поскольку позже мы вычислим выражения для функций, нам потребуется различие между функциями и формами и нотация для выражения этого различия. Это различие и нотация для его описания, от которого мы тривиально отклоняемся, даны Церковью [цитируя Церковь [2]].
(Позже он сказал: «Чтобы использовать функции в качестве аргументов, нужна запись для функций, и кажется естественным использовать лямбда-запись Церкви. Я не понял остальную часть книги, поэтому у меня не было соблазна попробовать реализовать его более общий механизм определения функций. «[3] Тем не менее, Лисп на удивление близко подходит к реализации формы лямбда-исчисления.)
Предложения по включению анонимных функций в C ++ датируются как минимум 1988 годом [4], всего через 9 лет после изобретения C ++, и авторы, похоже, хорошо знали об использовании Lisp и приняли название. Предложение, которое превратило его в стандарт C ++ 11 [5], и работа, ведущая к нему (например, [6], [7]), просто говорят (например): «Этот термин происходит от функционального программирования и лямбда-исчисления, где лямбда-абстракция определяет безымянную функцию «. [6]
Итак, чтобы ответить на ваш вопрос: лямбда-выражения связаны не столько с полным лямбда-исчислением, которое разработал Черч, но с лямбда-нотацией, которую он изобрел для обозначения анонимных функций.
Грэм, Пол, «Корни Лиспа», 2001. http://www.paulgraham.com/rootsoflisp.html
Ван Эмден, Мартен, «Рецепт Маккарти для языка программирования», 2011. https://vanemden.wordpress.com/2011/10/31/mccarthys-recipe-for-a-programming-language/
Кардоне, Феличе и Дж. Роджер Хиндли, «История лямбда-исчисления и комбинаторной логики», 2006. https://github.com/aistrate/Articles/blob/master/Haskell/History%20of%20Lambda-calculus%20and%20Combinatory%20Logic%20(Cardone,%20Hindley).pdf
Других решений пока нет …