Применение функции реализации лямбда-исчисления - PullRequest
6 голосов
/ 01 февраля 2012

Я только что нашел следующее выражение лямбда-исчисления:

(((λ f . (λ x . (f x))) (λ a . a)) (λ b . b))

Так что это функция, которая принимает аргумент f и возвращает другую функцию, которая принимает аргумент x и возвращает результат x, примененный к f.Результатом вышеприведенного выражения будет (λ b. B).

Это напоминает мне о частичном применении и карри, однако применение функции «наизнанку» (fx) вызвало у меня интерес.

Есть ли в этом выражении более глубокий теоретический смысл?

1 Ответ

8 голосов
/ 01 февраля 2012

Это выражение на самом деле довольно круто, хотя это довольно простая операция. В конце концов, функция - это просто приложение функции, верно?

Вот где все становится интересным. В лямбда-исчислении приложение является синтаксическим правилом, которое просто говорит: «Если f является выражением, а x является выражением, то f x является выражением». Приложение не является функцией любого рода. Это прискорбно: поскольку лямбда-исчисление основано на функциях, было бы ужасно полагаться на то, что не является функцией!

Ваш пример является своего рода средством от этого. Хотя мы не можем избавиться от приложения, мы можем по крайней мере определить аналог приложения. Этим аналогом является лямбда-функция (λ f . (λ x . (f x))) (или, идиоматически, λfx.f x). Эта является функцией, поэтому мы можем рассуждать об этом и использовать ее, как и любую другую функцию. Мы можем передать его в качестве аргументов другим функциям или использовать как результат функции. Внезапно функциональное приложение стало гораздо более удобным.

Это все, что у меня есть, когда речь идет о лямбда-исчислении, но эта функция и другие, подобные ей, также весьма полезны в реальной жизни. В функциональном языке программирования F # эта функция даже имеет имя «оператор обратного канала», и мы пишем, что у него есть оператор инфикса <|. Таким образом, в качестве альтернативы написанию f (x), где x - некоторое выражение, мы можем написать f <| x. Это хорошо, так как это часто может освободить нас от написания множества раздражающих скобок. Ключевым моментом, который я пытаюсь здесь подчеркнуть, является то, что, хотя на первый взгляд ваш пример кажется академическим или, может быть, просто не очень полезным, он фактически нашел свое отражение в нескольких основных языках программирования.

...