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


Вступительная лекция - часть 3


Floyd) к созданию так называемого метода индуктивных утверждений, который использовался для формализации семантики протекания информации в программе. При этом существенным преимуществом предложенного Р. Флойдом метода стала возможность интуитивно прозрачной и наглядной графической иллюстрации, основанной на блок-схемах, формализующих последовательность протекания информации.

В начале 70-х годов Д. Скотт стал использовать для формализации семантики математических теорий (в частности, ламбда-исчисления) так называемые решетки, которые обладают свойствами полноты и непрерывности. На этой основе ученым был предложен денотационный подход к семантике. Такой подход предполагает анализ синтаксически корректных конструкций языка с точки зрения возможности вычисления их значений посредством специализированных функций.

Существенным продвижением в развитии теорий, моделирующих программирование, стало появление формализаций с типами или, иначе, сортами.

В 60-х годах Р. Хиндли (Roger Hindley) исследовал типизацию в комбинаторной логике. При этом основной проблемой было моделирование языков функционального программирования со строгой типизацией, к каковым, в частности, относится изучаемый в рамках курса язык SML. Р. Хиндли разработал выводимость типов (type inference), т.е. возможность неявно определять тип выражения, исходя из типов выражений, которые его окружают. Именно эта возможность широко используется в современных языках программирования, таких как SML и Haskell.

Кроме того, Р. Хиндли изучил полиморфные системы типов, т.е. такие системы типов, в которых допустимы параметризованные функции или функции, имеющие переменный тип.

Позднее, в 70-х годах, Р. Милнер предложил практическую реализацию расширенной системы полиморфной типизации для языка функционального программирования ML, давшего начало языку программирования SML.

Наконец, на рубеже 80-х и 90-х годов, рядом исследователей — У. Куком (William R. Cook), П. Кэннингом (Peter S. Canning), У.Хиллом (Walter L. Hill) и другими – была изучена концепция полиморфизма в приложении к объектно-ориентированному программированию (в частности, к языку C++) и выявлена возможность моделирования полиморфизма на основе ламбда-исчисления.




Начало  Назад  Вперед



Книжный магазин