Lambda Calculus внешнее функциональное программирование?

Question

Я студент университета, и в настоящее время мы изучаем исчисление Lambda. Тем не менее, мне все еще трудно понять, почему именно это полезно для меня. Я понимаю, что если вы выполняете множество функциональных программ, это может быть полезно, однако я считаю, что это не нужно для обучения функциональному программированию, что вы думаете?

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

Answer 1

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

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

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

Answer 2

Вы просите применения вне информатики и логики. Это легко найти, например, в алгебраической топологии удобно иметь картезианскую закрытую категорию пространств, см. Удобная категория топологических пространств на nlab. Формальный язык, соответствующий картезианским закрытым категориям, является именно $ lambda $ -calculus. Позвольте мне проиллюстрировать с очень простым примером, как это пригодится.

Во -первых, в качестве упражнения для разминки, предположим, что кто -то спрашивает вас, определяется ли функция $ f: mathbb {r} to mathbb {r} $ $ f (x) = x^2 e^x + log (1 + x^2) $ дифференцируется. На самом деле вам не нужно доказывать, что это так, вы просто заметите, что это композиция дифференцируемых функций, поэтому дифференцируем. Другими словами, вы сделали легкий вывод, основанный на форма определения.

Теперь для реального примера. Предположим, что кто -то спрашивает вас, является ли функция $ f: mathbb {r} to mathbb {r} $, определенная $$ f (x) = left ( lambda f: mathcal {c} ( mathbb {r} ). int _ {-x}^{x} f (1 + t^2) dt right) ( lambda y: mathbb {r}. max (x, sin (y + 3)) $$ непрерывно. Опять же, мы можем немедленно ответить «да», потому что функция определяется с использованием $ lambda $ -calculus и начиная с непрерывных карт $ max $, $ int $, $ sin $ и т. Д.

Различные расширения $ lambda $ -calculus позволяют делать то же самое в других областях. Например, потому что Гладкий топос является закрытой категорией декартовой, любой карты, которая определяется с использованием $ lambda $ -calculus, начиная с производных, и структура кольца реальных (и вы можете добавить экспоненциальную функцию, если хотите), автоматически плавно. (На самом деле, основной тягой гладкого топоса является существование нильпотентных бесконечных матчей, которые позволяют вам осмысленно говорить такие вещи, как «мы раскрываем диск в бессонешних треугольника».)

Answer 3

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

Конечно, возможно быть очень хорошим программистом, не зная о $ lambda $ -calculus, но вы упускаете что-то прекрасное, что также очень полезно.

Answer 4

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

Я написал небольшое коммерческое приложение с использованием функционального языка, и я могу заверить вас, что, хотя и полезно для ученых и исследователей, они менее полезны в коммерческих целях, чем их процедурные кузены. На самом деле это вопрос лошадей для курсов, и наиболее практичным является язык, который может быть процедурным или функциональным по мере необходимости. Как следствие, функциональные возможности, которые были введены (для C#) в поддержку LINQ, таких как $ lambda $-Expressions, получают довольно много использования за пределами контекста запросов базы данных.

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

Answer 5

Не зная больше об этом, я слышал, что лингвисты используют исчисление лямбды.

http://www.sfu.ca/~jeffpell/ling406/lambdaabstractionoh.pdf, https://files.nyu.edu/cb125/public/lambda/