Именованные выражения

Возможность опеделять безымянные функции является преимуществом лямбда-исчисления. Было показано, что рекурсивные функции можно определить, не вводя каких имен. Тем не менее, возможность давать имена выражениям полезна, поскольку позволяет избегать переписывания именованных выражений. Простая форма именования может быть введена как форма «синтаксического сахара» над чистым лямбда-исчисление:

Можно связать несколько выражений с переменными в последовательном или параллельном стиле. В первом случае let-конструкции вкладываюся друг в друга. Во втором используется запись:

let { x₁ = S₁, x₂ = S₂,..., х_п = S_n }in T

Это выражение можно рассматривать как «синтаксический сахар» для:

(λ (x ₁,..., x _n) T)(S ₁... S _n)

Вместо префиксной формы с let можно ввести постфиксный вариант:

Т where х = S

С помощью let-нотации можно определять функции, введя соглашение, что

let f х ₁ х ₂ ... х _n = S in T

означает

let f = λx ₁ x ₂ ... x_n.S in T

Для определения рекурсивных функций можно ввести соглашение по использованию комбинатора неподвижной точки, т.е. let f = F f in S означает

let f = Y F in S.

Рассмотренная система «синтаксического сахара» позволяет поддерживать понимаемый человеком синтаксис для чистого лямбда-исчисления, и с ее помощью можно писать программы на языке, близком к настоящему языку программирования, такому как Haskell.

Программа представляет собой единственное выражение. Однако, имея в распоряжении механизм let для связывания подвыражений с именами, более естественно рассматривать программу как набор определений вспомогательных функций, за которыми следует само выражение. В Haskell введено соглашение опускать конструкцию let в определениях верхнего уровня.

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

В действительности выражение-программа вычисляется с помощью «развертывания» всех конструкций до уровня чистого лямбда-исчисления и последующего применения β -конверсий. Хотя в самой программе нет информации по ее выполнению, при ее составлении подразумевается некоторая стратегия исполнения.

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