ляться одновременно.

6 Лямбда-исчисление как формализация функциональных языков

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

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

В настоящее время лямбда-исчисление является основной формализацией, применяемой в исследованиях связанных с языками программирования. Это, связано, со следующими факторами:

•Это единственная формализация, которая может быть непосредственно использована для написания программ.

•Лямбда-исчисление дает простую и естественную модель для таких важных понятий, как рекурсия и вложенные среды.

•Большинство конструкций традиционных языков программирова

ния может быть отображено в конструкции лямбда-исчисления.

• Функциональные языки являются удобной формой синтаксической записи для конструкций различных вариантов лямбда-исчисления. Некоторые современные языки например Haskell имеют полное соответствие своей семантики с семантикой подразумеваемых конструкций лямбда-исчисления.

Лямбда-выражением будем называть конструкцию вида

где Е — некоторое выражение, возможно, использующее переменную х. Пример. λх.х2 представляетсобойфункцию, возводящуюсвойаргументвквадрат.

Использование лямбда-нотации позволяет четко разделить случаи, когда под выражением вида f(x) мы понимаем саму функцию f , а когда ее значение в точке

х.

14