Введение в теорию программирования. Объектно-ориентированный подход
Вступительная лекция
Важнейшими математическими формализациями, рассматриваемыми в данном курсе, являются ламбда-исчисление и комбинаторная логика.
Еще в 1924 г. М. Шейнфинкель (Moses Schonfinkel) разработал простую (simple) теорию функций, которая фактически являлась исчислением объектов-функций и предвосхитила появление ламбда-исчисления – математической формализации, поддерживающей языки функционального программирования (т.е. программирования в терминах функций).
Затем в 1934 г. А. Черч (Alonso Church) предложил собственно исчисление ламбда-конверсий (или ламбда-исчисление) и применил его для исследования теории множеств. Вклад ученого был фундаментальным, так что теория до сих пор называется ламбда-исчислением и часто именуется в литературе ламбда-исчислением Черча.
Позднее, в 1940 г., Х. Карри (Haskell Curry) создал теорию функций без переменных (иначе называемых комбинаторами), известную в настоящее время как комбинаторная логика. Эта теория является развитием ламбда-исчисления и представляет собой формальный язык, подобный языку функционального программирования.
В 60-х годах Х. Барендрегтом (H. Barendregt) были детально описаны синтаксис (т.е. форма конструкций) и семантика (т.е. значение конструкций) ламбда-исчисления.
Именно синтаксис и семантика являются наиболее существенными понятиями, фактически определяющими произвольный язык программирования.
В 60-х годах Дж. Бэкусом (John Backus) были созданы основы формализации синтаксиса языков программирования посредством специального математического языка. Позднее П. Науром (Peter Naur) этот язык (а с точки зрения целевого языка программирования — метаязык) был доработан, в результате чего возникла математическая нотация, известная и сегодня под названием "форм Бэкуса-Наура", или, сокращенно, БНФ.
Данная нотация была специально разработана с целью формализации синтаксиса языка программирования (в то время это был весьма популярный, прежде всего в математической среде, язык программирования ALGOL 60 с ясным, но довольно пространным синтаксисом).
БНФ и сегодня являются теоретически адекватным и практически применимым средством формализации синтаксиса языков программирования.
В 90-х годах синтаксис современного языка программирования SML был сформулирован Р. Милнером (Robin Milner). В работах, описывающих синтаксис SML, и по сей день широко используются формы Бэкуса-Наура.
Что касается теоретических основ семантики вычислений, то в конце 60-х годов Д. Скотт (Dana S. Scott) предложил применить для формализации семантики математических теорий так называемые домены (пока будем неформально понимать их как особый вид множеств). При этом на основе доменов Д. Скоттом был предложен так называемый денотационный подход к семантике. Такой подход предполагает анализ синтаксически корректных конструкций языка (или, иначе, денотатов) с точки зрения возможности вычисления их значений посредством специализированных функций.
Далее, в 70-х годах, М. Гордон (Michael J.C. Gordon) исследовал аппарат денотационной семантики применительно к языкам функционального программирования и сделал вывод об адекватности и практической эффективности использования этого подхода для решения поставленной задачи.
Параллельным направлением изучения семантики был подход, исследовавший изменения, которые происходили в процессе работы программы на основе отслеживания смены состояний программы.
Одним из практических результатов исследований в этом направлении стала разработка П. Лендином (Peter J. Landin) семантики модели языка программирования в форме абстрактной машины (т.е. модели компьютера), использовавшей понятие состояния.
Альтернативный подход к формализации семантики (который был осуществлен в рамках исследования так называемой операционной семантики языков программирования) привел к созданию Ч. Хоаром (Charles A.R. Hoare) аксиоматического метода, моделирующего отношения и причинно-следственные связи, возникающие между операторами языка программирования.
Развитие операционной семантики языков программирования привело Р. Флойда (Robert W.
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++) и выявлена возможность моделирования полиморфизма на основе ламбда-исчисления.
Заметим, что концепция полиморфизма является не только существенной составляющей функционального программирования, но и основополагающей для объектно-ориентированного подхода, где создание приложений происходит в терминах объектов.
Ключевым элементом реализации языков функционального программирования являются рекурсивные вычисления, т.е. вычисления, основанные на применении функции к самой себе как к аргументу.
Принципиальная реализуемость рекурсии средствами математической теории была доказана С. Клини (S.C. Kleene) еще в 30-х годах. При этом фундаментом рассуждений служило ламбда-исчисление.
В 50-х годах появилась комбинаторная логика Х. Карри – более приближенная к практике программирования формальная система с возможностью моделирования рекурсии.
Вскоре, в 60-х годах, Джоном Маккарти (John McCarthy) в ходе создания языка функционального программирования LISP, была исследована практическая применимость рекурсивных вычислений для символьной обработки и доказана возможность реализации рекурсии в программировании.
Абстрактная машина как формальная модель вычислительной системы является весьма важным объектом исследования в рамках настоящего курса.
Еще в 30-х годах А. Тьюрингом (Alan Mathison Turing) и Э. Постом (Emil Leon Post) независимо друг от друга были созданы эквивалентные по возможностям, но практически весьма сложные в реализации формализации, известные как абстрактные машины и получившие названия по именам своих авторов.
Комбинаторная логика Х. Карри позволяет моделировать вычисления в среде абстрактных машин, в значительной мере схожих с виртуальной машиной .NET.
В 60-х годах Д. Тернер (David Turner) предложил применять комбинаторы в качестве низкоуровневого кода для трансляторов языков функционального программирования, т.е. предвосхитил появление абстрактных машин, использующих в качестве инструкций комбинаторы.
Также в 60-х годах П. Лендин создал первую практически реализуемую абстрактную машину на основе расширенного ламбда-исчисления. Машина, получившая название SECD, формализовала вычисления на языке программирования ISWIM (If you See What I Mean), который впоследствии стал прообразом языка функционального программирования ML.
Основным понятием для SECD-машины является понятие состояния.
Уже в 70- е годы группой ученых института INRIA (Франция), ведущую роль в работе которой сыграл Пьер Кюрьен (P.-L. Curien), была создана еще одна абстрактная машина, основанная на смене состояний и получившая название категориальной абстрактной машины (КАМ). Теория категорий в форме категориальной комбинаторной логики, которая является теоретическим фундаментом для КАМ, по сути, представляет собой вариант ламбда-исчисления. С помощью КАМ был реализован еще один современный диалект ML, получивший название CaML (по имени машины).
В ходе исследования абстрактных машин возникает проблема оптимизации стратегии вычислений.
В качестве основной формализации для настоящего курса используется комбинаторная логика Х. Карри, которая позволяет моделировать вычисления в среде абстрактных машин, в значительной мере схожих с виртуальной машиной Microsoft .NET.
Исследования различных стратегий передачи параметров при обращении к функциям языков программирования (в частности, вызова функций по имени и по значению) были проведены Г. Плоткиным (G.D. Plotkin) на основе развития формализации SECD-машины П. Лендина. Полученные результаты легли в основу стратегии моделирования вычислений в ранних версиях языка функционального программирования ML.
В 70-х годах К. Уодсворт (Christopher P. Wadsworth) предложил механизм редукции графов для моделирования так называемых "ленивых" (т.е. выполняемых исключительно по мере необходимости) вычислений с помощью фундаментальной формальной теории-исчисления ламбда-конверсий.
Несколько позже Д. Тернером был представлен аналогичный механизм для "ленивых" вычислений в более приближенной к практике программирования формальной системе, а именно, в терминах выражений комбинаторной логики.
Затем, в 80-х годах, группе ученых во главе с П. Кюрьеном удалось усовершенствовать формализацию SECD-машины П. Лендина, и была создана категориальная абстрактная машина, оптимизация кода которой изучается в данном курсе.
Примерно в тот же период Р. Хьюсом (R.J.M. Hughes) была разработана формальная система суперкомбинаторов (усовершенствованная комбинаторная логика Х. Карри), позволяющая моделировать методы реализации языков программирования с возможностью оптимизации вычислений.
Настоящий курс предполагает сравнительное изучение функционального и объектно-ориентированного (основанного на объектах) подходов к программированию. Основными концепциями, характеризующими объектно-ориентированное программирование, являются наследование (сохранение производными объектами свойств базовых объектов) и инкапсуляция (изоляция определений объектов от методов управления ими), а также уже упомянутое понятие полиморфизма.
В 50-х годах Х. Хассе (Helmut Hasse, 1898-1979) предложил использовать особого рода диаграммы для графической интерпретации отношения частичного порядка. Заметим, что позднее диаграммы, открытые ученым, стали называться диаграммами Хассе. И по сей день диаграммы Хассе являются наиболее широко распространенной графической формализацией механизма наследования.
Затем в 1976 году Н.Руссопулос (N.D.Roussopulos) впервые применил фреймовую нотацию для моделирования отношений между объектами тех или иных предметных областей. Кроме того, ученым было введено так называемое ISA-отношение частичного порядка, которое адекватно моделирует понятие наследования. Заметим, что обозначение ISA, которое возникло от английских слов " is a ", означающих " является одним из ", хорошо иллюстрирует суть понятия наследования на естественном языке.
Позднее, в 1979 году, Д.Скотт сформулировал теорию полных и непрерывных решеток, которая используется в диаграммах потоков данных. Решетка Д.Скотта представляет собой модель частично упорядоченного множества, или, иначе, модель иерархии классов.
Затем, в 1988-90 годах Л. Карделли (Luca Cardelli), У. Куком и другими учеными была исследована семантика наследования. При этом был построен вариант денотационной семантики, который, как оказалось, адекватно формализовал не только единичное, но и множественное наследование.
Важная роль в курсе отводится моделям объектов, формализующим как определения (в математической теории или программе), так и взаимодействие объектов в среде вычислений.
В конце 60-х годов Д. Скоттом была предложена теория вычислений — модель, основанная на понятии домена (которое можно неформально определить как особый вид множеств). Эта модель принципиально применима для формализации объектов и их взаимодействия.
В 80-х годах Д. Скоттом и М. Фурманом (Michael P. Fourman) был исследован механизм определенных дескрипций для формализации определений. В ходе изложения мы будем неоднократно использовать эту лаконичную и интуитивно прозрачную нотацию для математически строгой сокращенной записи определений объектов, типов и классов.
Позднее, в 90-е годы, В. Вольфенгагеном (Vyatcheslav E. Wolfengagen) была создана так называемая двухуровневая схема концептуализации, основанная на двукратном применении постулата свертывания (до известной степени аналогичного операции ламбда-абстракции). Модель позволяет полно и непротиворечиво описывать объекты предметных областей с учетом их рассмотрения как в динамике, так и в статике. При этом двухуровневая схема концептуализации позволяет моделировать как объекты предметной области, так и объекты языков программирования. Другим преимуществом модели является возможность ее использования применительно как к объектам данных, так и к объектам метаданных (метаданные можно неформально понимать как данные о данных).
Для более подробного самостоятельного ознакомления с тематикой лекции рекомендуется следующий список источников: [23, 38, [51], [61], [63]].
