термин Lambda может быть:
\x.t)t и s являются лямбда-терминами, то ts является приложением.Итак, приложение с абстракцией в левой части (например, (\x.t)a) выглядит хорошо. Похоже на вызов функции. Но что означает приложение, когда левая часть является переменной или другим приложением? Что означает ab, ((\x.x)a)b или a(\x.x), если a и b являются переменными?
((\x.x)b)c — это функциональное приложение. Здесь применяется b к c.
((\x.x)b)c
= bc
a(\x.y) — это функциональное приложение, применяющее функцию a к своему единственному аргументу, который оказывается функцией, а именно к функции, возвращающей y (свободная переменная).
Одной из особенностей лямбда-исчисления является простота, с которой функции могут применяться к функциям, а функции могут принимать другие функции в качестве аргументов. Ваши два примера хорошо показывают оба случая.
EDIT Существует (как минимум) две версии лямбда-исчисления: нетипизированная и типизированная. В нетипизированном исчислении, которое вы здесь используете, все можно применить к чему угодно. В типизированном исчислении существуют базовые типы, которые не являются функциями, такие как тип предложений и тип «индивидуумов». Таким образом, вы могли бы написать ab только в том случае, если тип a был типом функции, отображающим тип b во что-то.
a и b являются переменными, то ab набирается неправильно?
- person Jofsey; 06.10.2012
