Я просто читаю лямбда-исчисление, чтобы «узнать это». Я рассматриваю это как альтернативную форму вычислений в отличие от машины Тьюринга. Это интересный способ работы с функциями / сокращениями (грубо говоря). Некоторые вопросы продолжают мучить меня, хотя:
- Какой смысл в лямбда-исчислении? Зачем проходить все эти функции / сокращения? Какова цель?
- В результате у меня остается вопрос: что именно сделал лямбда-исчисление, чтобы продвинуть теорию CS? Что это был за вклад, который позволил бы мне иметь «ага» момент понимания необходимости его существования?
- Почему лямбда-исчисление не рассматривается в текстах по теории автоматов? Обычный маршрут - прохождение различных автоматов, грамматик, машин Тьюринга и классов сложности. Лямбда-исчисление включено только в учебную программу для курсов стиля SICP (возможно, нет?). Но я редко видел, чтобы это было частью основной учебной программы CS. Означает ли это, что это не так уж и ценно? Может и нет, а может я что-то здесь упустил?
Я знаю, что функциональные языки программирования основаны на лямбда-исчислении, но я не рассматриваю это как действительный вклад, поскольку он был создан задолго до того, как у нас появились языки программирования. Итак, на самом деле, какой смысл знать / понимать лямбда-исчисление, его приложения / вклад в теорию?
soft-question
big-picture
lambda-calculus
ho.history-overview
кандидат наук
источник
источник
Functional Programming
обсуждал Haskell и немного Lisp. Преемник этого былPrinciples of Programming Languages
, который использовал ML и ввел лямбда-исчисление. Как показывают некоторые ответы, именно в этом и заключается лямбда-исчисление: в классе о языках программирования, наборе текста и т. Д.Ответы:
калькуляция выполняет две ключевые роли.λ
Это простая математическая основа последовательного, функционального вычислительного поведения высшего порядка.
Это представление доказательств в конструктивной логике.
источник
источник
источник
К вашим вопросам можно подходить со многих сторон. Я хотел бы оставить исторические и философские аспекты на стороне и ответить на ваш главный вопрос, который я считаю следующим:
В чем смысл булевой алгебры, или реляционной алгебры, или логики первого порядка, или теории типов, или какого-либо другого математического формализма / теории? Ответ заключается в том, что у них нет присущих им целей, даже если их дизайнеры создали их для той или иной цели. Лейбниц, возводя основы булевой алгебры, имел в виду определенный философский проект ; Буль изучал это по своим собственным причинам. работа де Моргана по реляционной алгебре также была мотивирована различными его проектами; У Пирса и Фреге были свои мотивы для создания современной логики.
Дело в том, что независимо от причины, по которой Церковь могла создать лямбда-исчисление, смысл лямбда-исчисления варьируется от одного практикующего к другому.
Кому-то это удобная запись для разговоров о вычислениях; альтернатива машинам Тьюринга и так далее.
С другой стороны, это прочная математическая основа для построения более сложного языка программирования (например, McCarthy, Stanley).
Для третьего лица это строгий инструмент для предоставления семантики как естественных, так и языков программирования (например, Montague, Fitch, Kratzer).
Я думаю, что лямбда-исчисление является официальным языком, который стоит изучать ради него самого. Вы можете узнать тот факт, что в нетипизированном лямбда-исчислении у нас есть эти маленькие звери, называемые Y-комбинаторами, и как они помогают нам определять рекурсивные функции и делают доказательство неразрешимости таким элегантным и простым. Вы можете узнать удивительный факт, что существует тесное соответствие между просто типизированным лямбда-исчислением и типом интуиционистской логики . Есть много других интересных тем для изучения (например, как мы должны дать семантику лямбда-исчисления? Как мы можем превратить лямбда-исчисление в дедуктивную систему, такую как FOL?)
Посмотрите введение Хиндли и Селдина в комбинаторы и λ – исчисление . «Лямбда-исчисление» Барендрегта - это Библия, поэтому, если вы зацепили Хиндли и Селдина, есть много тем как семантического, так и синтаксического характера.
источник
Тьюринг утверждал, что математика может быть сведена к комбинации символов чтения / записи, выбранных из конечного набора, и переключения между конечным числом психических «состояний». Он подтвердил это в своих машинах Тьюринга, где символы записываются в ячейках на ленте, а автомат отслеживает состояние.
Однако машины Тьюринга не являются конструктивным доказательством этого сокращения. Он утверждал, что любая «эффективная процедура» может быть реализована на некоторой машине Тьюринга, и показал, что универсальная машина Тьюринга может реализовать все эти другие машины, но на самом деле он не дал набор символов, состояний и правил обновления, которые реализуют математику. так, как он утверждал. Другими словами, он не предложил «стандартную машину Тьюринга» со стандартным набором символов, который мы можем использовать для записи нашей математики.
Лямбда-исчисление, с другой стороны, именно это. Черч специально пытался объединить нотации, используемые для записи нашей математики. Как только было показано, что LC и TM эквивалентны, мы можем использовать LC в качестве нашей «стандартной машины Тьюринга», и каждый сможет читать наши программы (ну, в теории;)).
Теперь мы могли бы спросить, почему трактовать ЛК как примитив, а не как диалект ТМ? Ответ заключается в том, что семантика LC является денотационной : термины LC имеют «внутреннее» значение. Существуют церковные цифры, есть функции сложения, умножения, рекурсии и т. Д. Это делает ЛЦ очень хорошо согласованным с практикой (формальной) математики, поэтому многие (функциональные) алгоритмы все еще представлены непосредственно в ЛК.
С другой стороны, семантика программ ТМ является оперативной : значение определяется как поведение машины. В этом смысле мы не можем вырезать какой-то фрагмент ленты и сказать «это дополнение», потому что это зависит от контекста. Поведение машины, когда она попадает в этот участок ленты, зависит от состояния машины, длины / смещения / и т.д. аргументов, сколько ленты будет использовано для результата, повредила ли какая-либо предыдущая операция этот участок ленты и т. д. Это ужасный способ работы («Никто не хочет программировать машину Тьюринга»), поэтому многие (императивные) алгоритмы представлены в виде псевдокода.
источник
другие ответы хороши, вот еще один ракурс / причина для размышлений, которые связаны с другими, но могут быть еще более определенными, но, тем не менее, может быть труднее четко иметь в виду, поскольку старые истоки несколько утрачены в песках времени:
исторический приоритет!
Лямбда-исчисление было введено, по крайней мере, еще в 1932 году в следующей ссылке:
машина Тьюринга была введена в ~ 1936 , так Lambda Исчисление предшествует появление ТМА на несколько лет!
другими словами, основной ответ заключается в том, что лямбда-исчисление во многих отношениях является конечной унаследованной системой TCS. он все еще существует во многом так же, как и Cobol, хотя не так много нового происходит в языке! Похоже, что это самая ранняя система вычислений по Тьюрингу, которая была введена и даже предшествует фундаментальной идее Полноты Тьюринга. только более поздний ретроспективный анализ показал, что лямбда-исчисление, машины Тьюринга и проблема почтовой корреспонденции были эквивалентны и ввели концепцию эквивалентности Тьюринга и тезис Черча-Тьюринга .
Лямбда-исчисление - это просто способ изучения вычислений из логически-ориентированных программ, с точки зрения представления их как математических теорем и выводов логических формул и так далее. это также показывает глубокую связь между вычислениями и рекурсией и дальнейшую тесную связь с математической индукцией .
это несколько примечательный факт, потому что он предполагает, что во многих отношениях (по крайней мере, теоретические ) источники вычислений были в основном в логике / математике , тезис, подробно изложенный / расширенный Дэвисом в его книге « Двигатели логики / математики и происхождение компьютер . (Конечно, происхождение и фундаментальная роль булевой алгебры также усиливают эту концептуальную историческую структуру.)
следовательно, драматично, можно даже сказать, что лямбда-исчисление немного похоже на педагогическую машину времени для изучения истоков вычислений!
источник
Я только что наткнулся на этот пост, и, несмотря на то, что мой пост был довольно поздним (год!), Я подумал, что, возможно, моя "ценность пенни" может быть полезной.
Во время изучения предмета в университете у меня была похожая мысль по этому поводу; Итак, я поставил перед лектором вопрос «почему» и ответил: «Составители». Как только она упомянула об этом, сила сокращения и умение оценивать, как лучше всего манипулировать им, внезапно сделали всю цель того, почему это было и остается потенциально полезным инструментом.
Ну, это, так сказать, был мой "ага" момент.
По моему мнению, мы часто считаем языки высокого уровня, шаблоны, автоматы, сложность алгоритмов и т. Д. Полезными, потому что мы можем связать их с «поставленной задачей»; тогда как исчисление Ламдбы кажется слишком абстрактным. Тем не менее, все еще есть те, кто работает с языками на низком уровне - и я думаю, что лямбда-исчисление, исчисление объектов и другие связанные с ними формализации помогли им понять и, возможно, разработать новые теории и технологии, из которых затем может извлечь пользу обычный программист. Действительно, по этой причине он, вероятно, не является основным модулем, но (по причинам, которые я изложил) будет несколько странных - кроме академиков - которые могут найти его неотъемлемой частью выбранной ими карьеры в вычислительной технике.
источник