Введение в теорию программирования. Функциональный подход

       

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


Пожалуй, наиболее продуктивной формализацией понятия "функция" стала математическая теория, известная сегодня под названием ламбда-исчисления. Более точно это исчисление следует называть исчислением ламбда-конверсий.

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

Кроме того, конверсии обеспечивают переход к вновь введенным обозначениям и, таким образом, позволяют представлять предметную область в более компактном или более детальном виде, или, говоря математическим языком, изменять уровень абстракции по отношению к предметной области. Эту возможность широко используют также языки объектно-ориентированного и структурно-модульного программирования в иерархии объектов, фрагментов программ и структур данных. На этом же принципе основано взаимодействие компонентов приложения в .NET. Именно в этом смысле переход к новым обозначениям является одним из важнейших элементов программирования в целом, и именно ламбда-исчисление (в отличие от многих других разделов математики) представляет собой адекватный способ формализации переобозначений.

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

Заметим, однако, что под словом "функция" в математической формализации и программной реализации имеются ввиду различные понятия.

Напомним, что определение функции в математике было сформулировано в лекции 3.

В свою очередь, функцией в языке программирования называется конструкция этого языка, описывающая правила преобразования аргумента (так называемого фактического параметра) в результат.

Напомним ход эволюции теорий, лежащих в основе современного подхода к ламбда-исчислению.

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



Содержание раздела