Лямбда-исчисление не казалось абстрактным. И я не вижу смысла в этом

18

Основной вопрос:

Что делает для нас лямбда-исчисление , что мы не можем сделать с основными свойствами функций и обозначениями, обычно изучаемыми в алгебре средней школы?

Прежде всего, что означает абстрактное в контексте лямбда-исчисления? Мое понимание слова абстрактное - это то, что отделено от механизма, концептуального резюме концепции.

Однако лямбда-функции, покончив с именами функций, предотвращают определенный уровень абстракции. Например:

f(x) = x + 2
h(x, y) = x + 5 y

Но даже не определяя механизм этих функций, мы можем легко говорить об их составе. Например:

1. h(x, y) . f(x) . f(x) . h(x, y) or 
2. h . f . f . h

Мы можем включить аргументы, если мы хотим, или мы можем полностью абстрагироваться, чтобы дать обзор того, что происходит. И мы можем быстро свести их к одной функции. Давайте посмотрим на композицию 2. У меня могут быть слои учеников, на которых я могу писать, в зависимости от моего акцента:

g = h . f . f . h
g(x, y) = h(x, y) . f(x) . f(x) . h(x, y)
g(x, y) = h . f . f . h = x + 10 y + 4

Давайте выполним вышеприведенное с помощью лямбда-исчисления или, по крайней мере, определим функции. Я не уверен, что это правильно, но я верю, что первое и второе выражения увеличиваются на 2.

(λuv.u(u(uv)))(λwyx.y(wyx))x

И умножить на 5лет.

(λz.y(5z))

Вместо того, чтобы быть абстрактным, это, кажется, входит в сам механизм того, что значит добавлять, умножать и т. Д. Абстракция, на мой взгляд, означает более высокий уровень, чем более низкий уровень.

Кроме того, я изо всех сил пытаюсь понять, почему лямбда-исчисление - даже вещь. В чем преимущество

(λuv.u(u(uv)))(λwyx.y(wyx))x

над

h(x) = x + 5 y

или комбинированная запись

Hxy.x+5y

или даже запись Хаскелла

h x y = x + 5 * y

Опять же, что делает для нас лямбда-исчисление, что мы не можем делать со свойствами и обозначениями функции f (x) -тиля, с которыми многие знакомы.

JDG
источник
9
Забавно, что вы привели пример из Haskell, поскольку Haskell основан на лямбда-исчислении. Лямбда-исчисление не о какой-либо конкретной записи. Это вычислительная модель, эквивалентная машинам Тьюринга, в которой «все является функцией».
Юваль Фильмус
2
Да, мне сказали, что он основан на лямбда-исчислении. Вопрос, на который я до сих пор не нашел ответа, который имеет смысл для меня, заключается в том, почему haskell основан на лямбда-исчислении, а не на справедливом. , , основные атрибуты функций я узнал в начальной школе. Это действительно суть всего этого вопроса.
JDG
6
Разве «нет цели сразу приходит на ум» почти как определение «абстрактного»? :-)
Дэвид Ричерби
1
Я бы не сказал, что это уничижительно. Эта обработка функций пригодна для исчисления. Но я вижу, как таким образом интерпретировать ярлык «средняя школа». Я отрегулирую это.
JDG
6
Я сомневаюсь, что у вас на самом деле есть формальное определение «обозначения функции алгебры средней школы». Если у вас есть какое-либо определение для таких функций, это, вероятно, теоретическое множество, которое не имеет вычислительного значения. Часть смысла лямбда-исчисления состоит в том, чтобы понимать такие обозначения на собственных терминах и, смею сказать, абстрагироваться от конкретных приложений, таких как полиномиальные функции или исчисление.
Дерек Элкинс покинул SE

Ответы:

24

Есть много причин, почему лямбда-исчисление так важно.

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

Невозможно выразить функции высшего порядка на языке алгебры средней школы.

Возьмите в качестве примера лямбда-выражение

λе,λграмм,λИкс,е(грамм(Икс))

Это простое выражение показывает нам, что в лямбда-исчислении композиция функций сама является функцией. В алгебре средней школы это не так легко выразить.

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

Вот небольшой пример. Выражение (где я здесь предполагаю прикладное лямбда-исчисление с сложением и целочисленными константами)

(λе,λграмм,λИкс,е((грамм(Икс)))(λИкс,Икс+2)

уменьшится до

λграмм,λИкс,грамм(Икс)+2

Также обратите внимание, что в лямбда-исчислении функции являются выражениями, а не определениями вида . Это освобождает нас от необходимости называть функции и проводить различие между синтаксической категорией выражений и синтаксической категорией определений.е(Икс)знак равное

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

Функциональная композиция имеет полиморфный тип

α,β,γ,(βγ)((αβ)γ)

в системе типов Хиндли-Милнера.

Очень сильным аргументом в пользу лямбда-исчисления является точное представление о типизированном лямбда-исчислении . Системы различных типов для функциональных языков программирования, таких как Haskell и семейство ML, основаны на системах типов для лямбда-исчислений, и эти системы типов предоставляют строгие гарантии в форме математических теорем:

Если программа е хорошо типизирована и сводится к остатку e , то e также будет хорошо типизированным.ее'е'

И если хорошо напечатан, то e не будет иметь определенных ошибок.ее

Доказательства в виде программ переписка особенно примечательна. Изоморфизм Карри-Ховарда (см., Например, https://www.rocq.inria.fr/semdoc/Presentations/20150217_PierreMariePedrot.pdf ) показывает, что существует очень точное соответствие между простейшим типом лямбда-исчисления и интуиционистской логикой высказываний: каждому типу соответствует логической формуле ϕT . Доказательство ϕ T соответствует лямбда-члену с типом T ,абета-редукция этого члена соответствует выполнению исключения среза в доказательстве.φTφTT

Я призываю тех, кто считает, что алгебра средней школы является хорошей альтернативой лямбда-исчислению, разработать версию алгебры средней школы полиморфного типа высшего порядка вместе с соответствующим понятием изоморфизма Карри-Говарда. Если бы вы даже смогли разработать интерактивный помощник по доказательству, основанный на алгебре средней школы, который позволил бы нам доказать многие теоремы, которые были формализованы с использованием доказательств, основанных на лямбда-исчислении, таких как Coq и Isabelle, это было бы еще лучше. Затем я бы начал использовать алгебру средней школы, и я уверен, что многие другие со мной.

Ханс Хюттель
источник
Это отличное объяснение. Полезно слышать, что функции высшего порядка (такие как композиция) и типизация лучше представлены в лямбда-исчислении, это обнадеживает, тем более что это облегчает доказательства и доказуемый код. Я не вижу последствий для большей части того, что вы упомянули, и почему традиционные обозначения неадекватны (например, из-за отсутствия необходимости в отдельном синтаксисе определения f (x) = e), однако полезно, чтобы вы назвали некоторые из этих причин и это дает представление о том, какие области улучшаются с помощью лямбда-исчисления.
JDG
Можно, конечно , ввести локальные определения вида но они уже могут быть выражены в синтаксисе лямбда-исчисления как ( λ x . e ) e . Лямбда-исчисление позволяет нам выражать функции без необходимости называть их, так же, как можно (в алгебре средней школы!) Говорить о числе 4, не называя их какой-либо переменной. позволятьИксзнак равное'ве(λИкс,е)е'4
Ганс Хюттель
5

Когда функции впервые описываются подросткам, они по существу отождествляются с графиками (графиками) или, возможно, с формулами; именно так исторически понимались функции до появления формалистических течений в математике. В настоящее время функции, как описано в первый год исчисления, являются вещественные функции, то есть, функции от до R .рр

Функции в лямбда-исчислении гораздо более общие. Точное определение зависит от того, напечатано ли ваше лямбда-исчисление или нетипизировано. В чистом нетипизированном лямбда-исчислении все является функцией. Это гораздо более общее, чем реальные функции исчисления.

Даже процедурные языки иногда используют идеи из лямбда-исчисления. Функция сортировки в C принимает в качестве параметра a сравнения , которую она использует для сравнения элементов. Лямбда-исчисление идет намного дальше - функции не только принимают функции в качестве входных данных, но также могут выводить их.

Лямбда-исчисление представляет собой модель вычисления, эквивалентную по мощности машинам Тьюринга. Это система, полная сама по себе. Чистое лямбда-исчисление не имеет «5» или «+» в качестве примитивных терминов - они могут быть определены внутри исчисления, так же как «5» и «+» не являются примитивами теории множеств. (Практические языки программирования реализуют натуральные числа по соображениям эффективности.)

Я подозреваю, что одной из причин, по которой вы не впечатлились лямбда-исчислением, является то, что его идеи настолько проникли в программный дискурс, что он больше не выглядит инновационным.

Юваль Фильмус
источник
«Я подозреваю, что одна из причин, по которой вас не впечатлило лямбда-исчисление», заключается в том, что я задаю вопрос: что делает для нас лямбда-исчисление? Другими словами, когда мы не используем лямбда-исчисление, что происходит. Когда мы используем лямбда-исчисление, что мы получаем? Если лямбда-исчисление было первым разом, когда люди думали, что если функции сами могут создавать функции, тогда это впечатляет? Среди моих первоначальных программ на Python был текст, содержащий функции, которые я позже оценил, очень похоже на делегирование задачи принятия решений другому человеку. Кажется очевидным?
JDG
это было до того, как я многое узнал. Я просто думал, что код надоедает вводить снова и снова, и что программирование должно помочь мне автоматически генерировать функциональность, включая сами функции.
JDG
2
Python поддерживает функциональное программирование. Первые языки программирования этого не сделали. Если бы вы программировали на Фортране, вы бы не создавали программы с текстом, содержащим функции, которые вы позже оценили. Даже не замечая этого, вы использовали возможности, предоставляемые идеями из лямбда-исчисления.
Юваль Фильмус
2
Eval возник в LISP , на который сильно повлияло лямбда-исчисление. Нечто подобное невозможно в FORTRAN, C, COBOL и многих других языках программирования.
Юваль Фильмус
Да, python поддерживает функциональное программирование - но я не уверен, что его способность eval () была вдохновлена ​​λCalc - вам не нужно думать о λCalc: я хочу автоматически генерировать код, который я смогу оценить позже. Это все равно, что сказать, что λКальк должен подумать: «Я скажу Миранде, чтобы она использовала свое лучшее суждение о том, как управлять ее отделом» - другими словами, получая функцию для генерации своих собственных функций. Вам не нужен λCalc, чтобы думать о делегировании задач высокого уровня. Если вы хотите поговорить о том, как черпать вдохновение из λCalc, более уместно указать лямбда-функции, понимания и т. Д.
JDG
4

Икс2ИксИкс2

λИкс,Икс2Икс2

ее(Икс)знак равноИкс2е

Использование лямбда-выражений в языках программирования имеет аналогичное преимущество; вы можете написать, что функция делает прямо там, где это необходимо, вместо того, чтобы определять совершенно новую функцию где-то в вашей программе.

ddИксИкс2ddИксИкс2


θ:ВВ**

θ(v)(е)знак равное(v)

Многие люди считают эту запись двойной оценки запутывающей и / или тревожной, а также это рекурсивное использование точечного определения функции. Лямбда-версия абстракции

θзнак равноλv,λе,е(v)

не имеет этой проблемы


Наконец, существует теорема абстрактной бессмыслицы о том, что «просто типизированное лямбда-исчисление» по сути то же самое, что и «декартово замкнутая категория» - так что, если вы когда-нибудь захотите выполнить вычисление в декартовой замкнутой категории, возможно, это хорошая идея использовать просто набрал лямбда-исчисление, чтобы сделать это.


источник
Я возвращаюсь к этому вопросу и нахожу этот ответ великолепным. Спасибо. Ответы здесь в целом действительно интересные.
JDG
4

Скажу сразу, я не эксперт по этой теме, но я потратил немного времени на его изучение, и одна из самых интересных вещей для меня в любой теме - это история. Таким образом, понимание части истории лямбда-исчисления помогает объяснить, почему оно полезно.

Краткое резюме состоит в том, что в начале 1900-х годов после того, как теория множеств начала развиваться, и математика была переосмыслена на основе множеств, некоторые математики заметили, что хотя определение теории множеств позволяет утверждать, что определенная структура существует, они не говорят вам, как построить и рассчитать это. Таким образом, теоретико-множественные определения неконструктивны . Математики начали задаваться вопросом, есть ли способ разработать конструктивные определения, которые выходят за рамки доказательства того, что что-то есть, и вместо этого доказывают, как оно есть .

Из Википедии :

В математике конструктивное доказательство - это метод доказательства, который демонстрирует существование математического объекта путем создания или предоставления метода для создания объекта. Это противоречит неконструктивному доказательству (также известному как доказательство существования или теорема чистого существования), которое доказывает существование объекта определенного типа без предоставления примера.

*

Затем было показано, что лямбда-исчисление и машина Тьюринга могут представлять любую вычислимую функцию и, таким образом, эквивалентны.

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

Лямбда-исчисление не является «полезным» в том смысле, что вы не собираетесь писать код с его использованием, но оно формирует основу для денотационной семантики, которая используется для описания программ и их динамических эффектов. Это используется в обсуждениях правильности программы и семантического значения. Это также явно сильно повлияло на разработку функциональных языков программирования, которые черпают всю свою концепцию исполнения из лямбда-исчисления.

Надеюсь, это поможет.

Изменить, чтобы добавить: я только что указал на этот документ, показывающий связь между топологией, лямбда-исчислением и физикой. Кратко рассмотрев это, я наткнулся на это фантастическое утверждение:

Хотя машину Тьюринга можно рассматривать как идеализированную упрощенную модель компьютерного оборудования , лямбда-исчисление больше похоже на простую модель программного обеспечения . ... Поэтически, лямбда-исчисление описывает вселенную, где все является программой, а все является данными: программы - это данные .

Дело в том, что лямбда-исчисление является идеализированной моделью вычислений программного обеспечения, и поэтому не привязано к конкретной реализации в любом языке программирования. Он моделирует чистые вычисления .

Дейв
источник
Больше на истории: Краткая история λ-исчисления в Стэнфордской Энциклопедии Философии. У них больше записей, чем можно обработать за всю жизнь.
Дэвид Тонхофер
3

Лямбда-исчисление не было разработано, чтобы быть языком программирования. Действительно, он был создан в 1930-х годах, за десятилетия до того, как у нас появились программируемые компьютеры. Скорее, он был создан как формальная модель для изучения вычислений. Если вы разочарованы тем, как легко он выражает код или математические функции, это потому, что это не то, для чего он нужен.

Андрей
источник
1
«десятилетия назад у нас даже были программируемые компьютеры» - неправильно. Программируемый компьютер существовал раньше (если не универсальные), а первые универсальные компьютеры были построены в 1930-х годах.
Рафаэль
-2

Лямбда-исчисление существует, так что можно создавать анонимные (лямбда-функции) функции. Если вы не покончите с именами функций, тогда пространство имен может быть загромождено, и у вас могут закончиться доступные имена функций. Это особенно важно при работе с так называемыми «функциями более высокого порядка», которые по понятным причинам возвращают функции (или указатели на функции).

По сути, лямбда-функции эквивалентны переменным локальной области видимости. Функциональное программирование без лямбда-функций аналогично процедурному программированию без каких-либо локальных переменных, то есть ужасной идеи.

«Почему лямбда-исчисление является даже вещью», математики любят избыточность. Лямбда-исчисление редко используется в математике, потому что, как вы обнаружили, нотация не очень полезна.

«Если бы вы могли даже разработать интерактивного помощника по доказательству, основанного на алгебре средней школы, который позволил бы нам доказать многие теоремы, которые были формализованы с использованием доказательств на основе лямбда-исчисления, таких как Coq и Изабель, это было бы еще лучше. затем начните использовать алгебру средней школы, и я уверен, что многие другие со мной ". Вы слышали о метамате? Никакое лямбда-исчисление там не может доказать многие из теорем Кок / Изабель

зп
источник
Помимо некоторых мнений, что предлагает этот ответ?
Рафаэль
@ Рафаэль Дезинформация. Большая часть этого ответа даже не имеет смысла. Там нет недостатка в именах. «Лямбда-функции» не эквивалентны локальным переменным; это даже не имеет смысла. Я предполагаю, что это относится к ссылкам let, но хотя они letмогут быть закодированы анонимными функциями, вы явно не можете пойти другим путем. Функциональное программирование не требует «лямбда-функций», например, Backus ' FP или Sisal .
Дерек Элкинс покинул SE
В основном я хотел оставить комментарий к ответу Ганса, но мне не хватило кармы. поэтому я решил превратить комментарий в полноценный ответ
sn