Лямбда-нотация

Говоря f(x), что подразумевают:

• саму функцию f,
• результат её применения к конкретному x ?

В математической статье из контекста понятно, для формального исследования необходима точность. Лямбда-нотация предложена Алонзо Чёрчем в 1930 г.

Псевдопарадокс из математического анализа

(x²)' = 2x

Подставив в обе части x := 1, получим

В действительности мы имеем равенство двух функций, а не чисел

f: x x², g: x 2x
D f = g,

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

D ∈ [[R→R]→[R→R]]

Можно записать в виде безымянных функций:

D (x x²) = (x 2x)

λ-нотация — замена стрелки : f = λx.x²