выражение исчисления Лямбда функции реализации приложения

Question

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

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

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

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

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

Answer 1

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

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

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

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