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

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

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

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

Благодаря реализации механизма сопоставления с образцом, такие языки функционального программирования как ML и Haskell хорошо использовать для символьной обработки.

Естественно, языки функционального программирования не лишены и некоторых недостатков.

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

Для профессиональной разработки программного обеспечения на языках функционального программирования необходимо глубоко понимать природу функции. Исследованию закономерностей и особенностей природы функции в основном и посвящены лекции 2 - 12 данного курса.

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

Так, математической функцией f с областью определения A и областью значений B называется множество упорядоченных пар

(a,b) A Ч B,

таких, что если (a,b1) f и (a,b2) f,

то b1 = b2.

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

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

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

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

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

Рассмотрим эволюцию языков программирования, развивающихся в рамках функционального подхода.

Ранние языки функционального программирования, которые берут свое начало от классического языка LISP (LISt Processing), были предназначены, для обработки списков, т.е. символьной информации. При этом основными типами были атомарный элемент и список из атомарных элементов, а основной акцент делался на анализе содержимого списка.

Развитием ранних языков программирования стали языки функционального программирования с сильной типизацией, характерным примером здесь является классический ML, и его прямой потомок SML. В языках с сильной типизацией каждая конструкция (или выражение) должна иметь тип.

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

Следующим шагом в развитии языков функционального программирования стала поддержка полиморфных функций, т.е. функций с параметрическими аргументами (аналогами математической функции с параметрами). В частности, полиморфизм поддерживается в языках SML, Miranda и Haskell.

На современном этапе развития возникли языки функционального программирования "нового поколения" со следующими расширенными возможностями: сопоставление с образцом (Scheme, SML, Miranda, Haskell), параметрический полиморфизм (SML) и так называемые "ленивые" (по мере необходимости) вычисления (Haskell, Miranda, SML).

Семейство языков функционального программирования довольно многочисленно. Об этом свидетельствует не столько значительный список языков, сколько тот факт, что многие языки дали начало целым направлениям в программировании. Напомним, что LISP дал начало целому семейству языков: Scheme, InterLisp, COMMON Lisp и др.

Не стал исключением и изучаемый нами язык программирования SML, который был создан в форме языка ML Р. Милнером (Robin Milner) в MIT (Massachusetts Institute of Technology) и первоначально предназначен для логических выводов, в частности, доказательства теорем. Язык отличается строгой типизацией, в нем отсутствует параметрический полиморфизм.

Развитием "классического" ML стали сразу три современных языка с практически одинаковыми возможностями (параметрический полиморфизм, сопоставление с образцом, "ленивые" вычисления). Это язык SML, разработанный в Великобритании и США, CaML, созданный группой французских ученых института INRIA, SML/NJ - диалект SML из New Jersey, а также российская разработка - mosml ("московский" диалект ML).

Близость к математической формализации и изначальная функциональная ориентированность послужили причиной следующих преимуществ функционального подхода:

1. простота тестирования и верификации программного кода на основе возможности построения строгого математического доказательства корректности программ;

2. унификация представления программы и данных (данные могут быть инкапсулированы в программу как аргументы функций, означивание или вычисление значения функции может производиться по мере необходимости);

3. безопасная типизация: недопустимые операции с данными исключены;

4. динамическая типизация: возможно обнаружение ошибок типизации во время выполнения (отсутствие этого свойства в ранних языках функционального программирования может приводить к переполнению оперативной памяти компьютера);

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

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

1. безопасность программного кода, т.е. гарантия отсутствия переполнения памяти (в случае корректно написанной программы) и, соответственно, защиты от потенциальной неустойчивости работы системы посредством искусственного создания переполнения (такие языки программирования как "классический" C и C++ потенциально небезопасны);

2. статическая типизация: все ошибки несоответствия типов выявляются уже на стадии контроля соответствия типов в ходе трансляции (а не во время выполнения программы, как в LISP и Scheme);

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

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

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

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

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

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

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

1. интеграция различных языков функционального программирования (при этом максимально используются преимущества каждого из языков, в частности, Scheme предоставляет механизм сопоставления с образцом, а SML - возможность вычисления по мере необходимости);

2. интеграция различных подходов к программированию на основе межъязыковой инфраструктуры Common Language Infrastructure, или CLI (в частности, возможно использование C# для обеспечения преимуществ объектно-ориентированного подхода и SML - функционального, как в настоящем курсе);

3. общая унифицированная система типизации Common Type System, CTS (единообразное и безопасное управление типами данных в программе);

4. многоступенчатая, гибкая система обеспечения безопасности программного кода (в частности, на основе механизма сборок).

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

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

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

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

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

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

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

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

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

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

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

Перейдем к описанию ламбда-исчисления как формальной системы. Согласно математической практике, необходимо определить следующие элементы теории:

· алфавит;

· утверждения;

· аксиомы;

· правила вывода.

При этом под алфавитом понимается множество символов, допустимых в нотации той или иной формализации.

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

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

Правила вывода определяют законы преобразования одних символов (объектов), исследуемых в теории, в другие объекты.

Рассмотрим алфавит ламбда-исчисления.

Допускаются элементы четырех видов:

1. константы;

2. переменные;

3. выражения (или термы);

4. специальные символы.

При этом принимаются следующие обозначения.

Константы c1, c2, ... обозначаются малыми буквами латинского алфавита, возможно, с индексами.

Переменные x, y, ... обозначаются малыми буквами латинского алфавита, возможно, с индексами.

Выражения (или, иначе, термы) M, N, ... обозначаются заглавными буквами латинского алфавита, возможно, с индексами.

Допускается использование следующих специальных символов (взяты в кавычки и разделены запятыми): "(", ")", "."

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

Ламбда-термы строятся по индукции (порядок построения можно считать определением) следующим образом.

Базис индукции: любая переменная или константа является ламбда-термом по определению.

Шаг индукции: если M, N - произвольные ламбда-термы и x - произвольная переменная, то справедливо, что:

· во-первых, выражение (лx.M) является допустимым ламбда-термом;

· во-вторых, выражение (MN) является допустимым ламбда-термом.

Заметим, что при этом ламбда-выражение (MN) обозначает операцию аппликации (или применения функции к аргументу), а ламбда-выражение (лx.M) - операцию абстракции.

Кроме того, примем, что никакой другой набор символов не является допустимым ламбда-термом.

После определения алфавита и порядка построения допустимых ламбда-выражений посредством операций аппликации и абстракции перечислим аксиомы ламбда-исчисления.

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

Следующие аксиомы задают свойства отношения конвертируемости:

() лx.a = лz.[z/x]a;

(в) (лx.a)b = [b/x]a.

Аксиома () означает возможность подстановки терма z вместо всех вхождений переменной x в ламбда-выражение а.

Аксиома (в) означает возможность редукции (то есть упрощения вида) ламбда-выражения в левой части путем подстановки b вместо всех вхождений переменной x в ламбда-выражение а. Фактически редукция означает возможность создания (в ламбда-исчислении или на языке программирования) одной функции (ламбда-выражения) как сокращенной записи другой функции (ламбда-выражения).

Перечислим правила вывода термов, которые задают характеристики отношения конвертируемости:

(м) если a=b, то ca=cb;

(н) если a=b, то ac=bc;

(о) если a=b, то lx.a=lx.b;

(с) a=a (рефлексивность);

(у) если a=b, то b=a (симметричность);

(ф) если a=b и b=c, то a=c (транзитивность).

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

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

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

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

Во-первых, скобки для операции аппликации восстанавливаются по ассоциации влево, например:

xy = (xy), xyz = ((xy)z), ...

Во-вторых, избыточные скобки могут опускаться, например:

(xy) = xy, ((xy)z) = xyz, ...

В-третьих, скобки для операции абстракции восстанавливаются по ассоциации вправо, например:

лxy.M = (лx.(лy.M)), лxyz.M = (лx.(лy.(лz.M))), ...

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

1. x;

2. 1;

3. lx.x;

4. lx.x + 1;

5. (lx.x + 1)2 = [2/x](x + 1) = 2+1 = 3;

6. a $ b.

Согласно правилам построения алфавита, первый из ламбда-термов является переменной, а второй - константой.

Третий ламбда-терм, согласно правилам построения выражений, представляет собой ламбда-абстракцию переменного терма x к самому себе, т.е. определяет функцию тождества.

Четвертый ламбда-терм отличается от третьего тем, что добавляет к аргументу x константу 1, т.е. определяет функцию инкремента (или прибавления единицы). Заметим, что в алфавите ламбда-исчисления отсутствует функция сложения как таковая, так что возможны различные интрепретации символа "+" (будем считать его далее "встроенной" функцией сложения).

Пятый ламбда-терм обозначает подстановку согласно аксиоме () константы 2 вместо всех вхождений x в выражение x+1 (вычисление значения функции в число 3 возможно при корректной интерпретации символа "+").

Шестой ламбда-терм недопустим из-за вхождения неопределенного символа "$".

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

Несмотря на то, что мы еще не изучали синтаксис языка, соответствие между ламбда-исчислением и функциональным языком настолько естественно, что сопоставление ламбда-термов SML-выражениям происходит практически интуитивно и в дальнейших комментариях не нуждается.

Приведем фрагменты SML-программ, соответствующих допустимым ламбда-термам из предыдущего списка:

1. x (переменная, тип которой определяется в процессе трансляции на этапе контроля типизации в соответствии с выводом типов);

2. 1 (константа);

3. fn x => x (функция тождества);

4. fn x => x+1 (функция инкремента);

5. (fn x => x+1) 2 (вычисление значения функции, в результате выполнения получается целое число 3).

Продолжим иллюстрацию соответствия между программами на языке SML и ламбда-выражениями, исследовав операцию аппликации функции к аргументу.

Рассмотрим описание функции инкремента:

fun f x = 1+x;

Здесь нужно учитывать, что в общем случае функция f языка программирования SML, имеющая формальный параметр x и тело b, задается следующим описанием:

fun f x = b;

Для вычисления значения выражения необходимо произвести аппликацию функции к данному выражению; для аппликации функции f к целому числу 4 нужно записать:

f 4;

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

f 2 + 3;

означает порядок аппликации (f2)+3, а не f(2+3), т.е. находится в полном соответствии с соглашениями о скобках, принятыми в ламбда-исчислении.

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

1. лаконичность (ограниченный необходимыми элементами алфавит, два способа построения выражений - аппликация и абстракция, небольшое количество аксиом и правил вывода);

2. интуитивная ясность (обозначения являются краткими и понятными);

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

4. полнота (в ламбда-исчислении можно представить произвольную, в частности, сколь угодно сложную, функцию);

5. естественная близость к языкам функционального программирования (SML, Scheme, Haskell, Miranda, Hope, Clean) была проиллюстрирована на примерах программ на языке SML.

Лекция 6. Комбинаторная логика как формальная система

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

Рассмотрим построение формальной системы логики. Заметим, что важнейшим понятием для любой формы комбинаторной логики является понятие комбинатора.

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

Переменная x называется свободной в ламбда-выражении (терме) вида лx.A, если она не имеет вхождений в терм A; в противном случае переменная x называется связанной.

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

Теперь становится возможным дать лаконичное определение комбинатора.

Ламбда-выражение (терм), не содержащее связанных переменных, называется комбинатором.

Перейдем к описанию комбинаторной логики как формальной системы. Согласно математической практике, необходимо определить следующие элементы теории:

· алфавит;

· утверждения;

· аксиомы;

· правила вывода.

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

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

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

Правила вывода определяют правила преобразования одних символов (объектов), исследуемых в теории, в другие объекты.

Рассмотрим алфавит комбинаторной логики.

Допускаются элементы четырех видов:

1. константы;

2. переменные;

3. комбинаторные выражения (или, иначе, термы);

4. специальные символы.

При этом принимаются следующие обозначения.

Константы c1, c2, ... обозначаются малыми буквами латинского алфавита, возможно, с индексами.

Переменные x, y, ... обозначаются малыми буквами латинского алфавита, возможно, с индексами.

Выражения (или, иначе, термы) M, N, ... обозначаются заглавными буквами латинского алфавита, возможно, с индексами.

Допускается использование следующих специальных символов (взяты в кавычки и разделены запятыми): "(", ")".

Рассмотрим далее порядок конструирования допустимых для заданного алфавита комбинаторных выражений, или, иначе, термов.

Комбинаторные термы строятся по индукции (порядок построения можно считать определением) следующим образом.

Базис индукции: любая переменная или константа является комбинаторным термом по определению.

Шаг индукции: если M, N - произвольные комбинаторные термы и x - произвольная переменная, то справедливо, что выражение (MN) является допустимым комбинаторным термом.

Заметим, что при этом комбинаторное выражение (MN) обозначает операцию аппликации (или применения функции к аргументу).

Кроме того, примем, что никакой другой набор символов не является допустимым комбинаторным термом.

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

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

Следующие аксиомы задают свойства отношения конвертируемости:

(I) Ix = x;

(K) Kxy = x;

(S) Sxyz = xz(yz).

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

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

Перечислим правила вывода комбинаторных термов, которые задают характеристики отношения конвертируемости:

(м) если a=b, то ca=cb;

(н) если a=b, то ac=bc;

(с) a=a (рефлексивность);

(у) если a=b, то b=a (симметричность);

(ф) если a=b и b=c, то a=c (транзитивность).

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

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

В этой связи из соображений экономии пространства для вывода соотношений принимаются следующие умолчания, позволяющие значительно сократить запись и увеличить удобство прочтения и обработки комбинаторных термов.

Во-первых, скобки для операции аппликации восстанавливаются по ассоциации влево, например:

XY = (XY), XYZ = ((XY)Z), ...

Во-вторых, избыточные скобки могут опускаться, например:

(XY) = XY, ((XY)Z) = XYZ, ...

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

Задать синтаксис языка возможно, перечислив описание его конструкций, например, с помощью форм Бэкуса-Наура или БНФ. БНФ созданы в 60-х годах Дж. Бэкусом (John Backus) и развиты П. Науром (Peter Naur) как метаязык для формализации синтаксиса языка программирования ALGOL 60. Впоследствии БНФ получили широкое распространение и в настоящее время являются основной нотацией для формализации синтаксиса языков программирования (мы будем пользоваться БНФ для формализации синтаксиса языка программирования SML). В данной нотации символ "::=" интерпретируется словами "может иметь вид", а символ "|" - словом "или". Определяемое и определяющие понятия записываются в угловых скобках, первое - слева, а последние - справа от значка "::=".

Формализуем синтаксис выражений комбинаторной логики (или комбинаторов).

БНФ-описание комбинатора имеет вид:

<комбинатор> ::= K | S | (<комбинатор> <комбинатор>)

БНФ-описание терма комбинаторной логики, возможно, содержащего переменные, имеет вид:

<комбинаторный терм> ::= K | S | <переменная> |

(<комбинаторный терм> <комбинаторный терм>)

Проиллюстрируем представленную формальную систему комбинаторной логики необходимыми примерами комбинаторов. Рассмотрим характеристические соотношения для комбинаторов, которые впоследствии окажутся теоретически интересными и практически полезными в данном курсе (некоторые из соотношений совпадают с введенными ранее аксиомами):

(I) I a = a;

(K) К ab = a;

(S) S abc = ac(bc);

(B) B abc = a(bc);

(C) C abc = acb;

(W) W xy = xyy.

Соотношение (I), как уже отмечалось, характеризует комбинатор тождества.

Соотношение (K), как отмечалось, характеризует комбинатор первой проекции (иначе именуемый канцелятором, т.е. "отменяющим" "выполнение" всех "инструкций", кроме первой).

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

Соотношение (B) характеризует комбинатор композиции, который образует последовательность комбинаторных термов и служит для объединения более элементарных "инструкций" в более сложные, а в итоге - в "программы".

Соотношения (C) и (W) определяют соответственно пермутацию (перестановку) и дублирование аргументов.

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

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

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

Проиллюстрируем моделирование механизма редукции следующим примером.

Рассмотрим комбинаторный терм вида

SKKx.

Пользуясь аксиомами (К) и (S), а также правилами вывода, произведем редукцию терма:

SKKx = (по правилу S)

Kx(Kx) = (по правилу K)

x.

В результате получаем, что SKKx = x, откуда, с учетом аксиом и правила (I), I = SKK.

Как видно из предыдущего примера, одни комбинаторы можно выразить через другие.

Возникает вопрос: существует ли конечный набор комбинаторов, посредством которого можно выразить произвольный терм комбинаторной логики? Оказывается, что ответ на поставленный вопрос утвердителен, причем введенные аксиомы и правила вывода обеспечивают весьма лаконичный набор такого рода.

Необходимость продолжения рассуждений приводит нас к понятию базиса.

Множество (минимальной мощности) комбинаторов, через элементы которого может быть выражен произвольный комбинатор, называется (минимальным) базисом.

Оказывается, можно доказать, что:

1. базис термов для комбинаторной логики действительно существует (причем существует бесконечное множество возможных базисов);

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

3. минимальный базис состоит всего из двух "инструкций"-комбинаторов, например, {K,S}.

Приведем еще несколько примеров базисов:

{I,K,S}; {I,B,C,S}; {B,W,K}.

Разложение термов в базисе {K,S} для ранее рассмотренных комбинаторов имеет вид:

B = S(KS)K; W = SS(K(SKK)); C = S(BBS)(KK).

Разложение в базисе аналогично программированию на языке базисных инструкций.

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

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

В случае комбинаторной логики будем считать, что тип a приписан комбинатору X тогда и только тогда, когда это утверждение получено из следующих аксиом:

(FI) ||-- #(I) = (a,a),

(FK) ||-- #(K) = (a,(b,a)) = (a,b,a),

(FS) ||-- #(S) = ((a,(b,c)), ((a, b)(a,c)))

и правила вывода

(F) если ||-- #(X) = (a,b) и ||-- #(U) = a,

то ||-- #(XU) = b.

Заметим, что процедура контроля соответствия типов транслятора языка программирования реализована сходным образом, причем в ней используется механизм сопоставления с образцом. В языке программирования SML, кроме того, применятся механизм получения логического вывода о типе выражения, исходя из контекста его использования. Этот механизм, известный также как выводимость типов (type inference), адекватно моделируется в терминах комбинаторной логики.

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

fun Ix = x;

fun Kxy = x;

fun Sxyz = xz(yz);

Реализация функций достаточно прозрачна и не требует пояснений.

Функция I реализует комбинатор тождества I, функция K - комбинатор-канцелятор K, а функция S - комбинатор-коннектор S.

Лекция 7. Теория типов и комбинаторная логика

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

Рассмотрим построение системы типизации на основе комбинаторной логики.

В математике принято называть типами (или, иначе, сортами) относительно устойчивые и независимые совокупности элементов, которые можно выделить во всем рассматриваемом множестве (предметной области). Заметим, что разделение элементов предметной области на типы или сорта во многом является условным и носит субъективный характер, т.к. зависит от эксперта в этой области.

Тип, подобно множеству, может определяться двояко.

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

Другим способом определения типа T является формализация общих свойств тех элементов d из предметной области D, которые объединяются в этот тип, посредством задания индивидуализирующей предикатной функции Y, значение которой истинно, если элемент принадлежит данному типу и ложно в противном случае:

T = {d: D|Ш}.

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

Чистой системой типов называется семейство ламбда-исчислений, в которых каждый элемент характеризуется тройкой <S, A, R>, где:

S - подмножество констант, называемых сортами;

A - множество аксиом вида c:s, где с является константой, а s является сортом;

R - множество троек сортов, определяющих возможные функциональные пространства и их сорта для системы.

Далее введем обозначение, характеризующее то обстоятельство, что тот или иной объект является типизированным, или, иначе говоря, что тому или иному объекту приписан тип.

В частности, для ламбда-терма M приписывание ему типа T обозначим как

#M ||-- T

и будем в таком случае говорить, что ламбда-терм M имеет тип T.

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

Во-первых, задается множество базисных типов (обозначим их символами d1, d2, и так далее).

Во-вторых, примем соглашение, что всякий базисный тип считается типом.

В-третьих, условимся, что если a и b считаются типами, то функция из a в b также считается типом и при этом имеет тип a>b.

Заметим, что в основе теории типов лежит принцип иерархичности, который заключается в том, что производные типы содержат базисные как подмножества.

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

Для иллюстрации построения теории типов расширим комбинаторную логику операцией приписывания типа.

Напомним аксиомы комбинаторной логики, задающие свойства отношения конвертируемости:

(I) Ix = x;

(K) Kxy = x;

(S) Sxyz = xz(yz).

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

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

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

Под типом (сортом) будем понимать относительно устойчивую и независимую совокупность элементов, которую можно выделить во всем рассматриваемом множестве (предметной области).

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

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

Система типов в SML формируется по следующей схеме:

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

· int - целые числа;

· string - строки символов;

· bool - логические значения.

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

Как можно заметить, формирование системы типов в SML аналогично построению системы типов в формальных математических теориях, в частности в комбинаторной логике.

Язык функционального программирования SML представляет собой язык со статической типизацией. Это означает, что процедура контроля типизации, которая является неотъемлемой частью транслятора любого современного языка программирования, должна поставить тот или иной тип в соответствие каждому выражению в тексте программы. Таким образом, приписывание типов выражениям происходит во время компиляции (compile time), а не во время выполнения (run time) программы, т.е. статически с точки зрения выполнения программы.

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

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

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

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

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

Контроль соответствия типов в языке SML, в отличие от LISP и подобных ему языков программирования, в полном объеме осуществляется на этапе компиляции, что также способствует безопасности типизации.

Еще одной важной позитивной особенностью языка программирования SML является то обстоятельство, что в нем поддерживается так называемая полиморфная типизация, суть которой можно объяснить на основе следующего примера.

Рассмотрим функцию обработки списка, которая упорядочивает его элементы по возрастанию. В классическом языке программирования со строгой типизацией, например, в языке Pascal, неизбежно придется реализовать, по крайней мере, две функции: для случаев числовых и строковых элементов списка. В SML такой необходимости не возникает, т.к. существует возможность описания функции обработки списка с переменным типом аргументов, которая безошибочно обработает и список из чисел, и список из строк, существенно сэкономив трудозатраты.

Проиллюстрируем выводимость типов в языке программирования SML на примере.

Рассмотрим функцию

let

val Id = fn x => x

in (Id 3, Id true)

end

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

Рассмотрим другую функцию

fn Id => (Id 3, Id true)) (fn x => x)

В отличие от предыдущей, данная функция является некорректно типизированной (ill-typed), поскольку однозначно определить тип параметра x, в отличие от предыдущего примера, не представляется возможным.

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

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

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

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

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

val x=2*3;

val x = 6 : int

Как и следовало ожидать, значение переменной x оказывается целочисленным (int).

Заметим, что функция val, которая используется в примере, является стандартной функцией языка программирования SML для определения типа языкового объекта, т.е. фактически осуществляет приписывание типа (при необходимости используя механизм выводимости типов).

В качестве второго примера определим тип константы, которой присвоим значение, также сводимое к целому типу:

1+2;

3 : int

Как и следовало ожидать, значение константы 3 также оказывается целочисленным (int).

Наконец, определим тип функции сложения двух целочисленных аргументов:

fun add (x : int)(y : int) = x+y;

val add = fn : int -> int -> int

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

Продолжим ряд примеров. Проиллюстрируем означивание (вычисление значения) определенной выше функции сложения двух целочисленных аргументов:

add 1 3;

val it = 4 : int

Очевидно, что, как и следует из ранее вычисленного типа

(int -> int -> int), функция, принимая на вход пару целочисленных величин, возвращает значение целочисленного типа.

Рассмотрим далее тип функции, которая является производной от функции add и производит операцию прибавления единицы:

val f = add 1;

val f = fn : int -> int

Вновь введенная функция имеет тип "из целого числа в целое число" (int -> int) .

Наконец, означивание последней функции

f 4;

val it = 5 : int

в соответствии с ее типом дает целочисленный результат.

Рассмотрим пример полиморфизма - оперирования функциями переменного типа.

Для иллюстрации исследуем поведение встроенной функции hd (от слова "head" - голова), которая выделяет "голову" (первый элемент) списка, вне зависимости от типа его элементов.

Применим функцию к списку из целочисленных элементов:

hd [1,2,3];

val it = 1 : int

Получим, что функция имеет тип функции из списка целочисленных величин в целое число (int list -> int).

В случае списка из значений истинности та же самая функция

hd [true, false, true, false];

val it = true: bool

возвращает значение истинности, т.е. имеет следующий тип:

bool list -> bool

Наконец, для случая списка кортежей из пар целых чисел

hd [(1,2)(3,4),(5,6)];

val it = (1,2) : int*int

получим тип:

((int*int)list -> (int*int)).

В итоге можно сделать вывод о том, что функция hd имеет тип (type list) -> type, где type - произвольный тип, т.е. полиморфна.

Технологическая платформа NET обеспечивает единообразное управление типами элементов всех языков программирования, реализованных на данной платформе. Это достигается за счет интегрированной обобщенной системы типизации, так называемой Common Type System, или, сокращенно, CTS.

Основная особенность CTS заключается в том, что она представляет собой единую иерархию типов, и типы объектов программы, написанной на произвольном языке программирования, который поддерживается технологической платформой NET, в ходе трансляции автоматически преобразуются в соответствующие им типы Common Type System.

Таким образом, для любого языка программирования существует отображение (функция), преобразующая произвольный тип этого языка в тот или иной тип Common Type System. Естественно, язык программирования SML не является исключением. Приведем в подтверждение фрагмент отображения типов языка программирования SML в типы иерархии CTS, оформив это соответствие в виде таблицы 6.1.

Позднее мы обсудим подобное соответствие типов для языка программирования C#.

Рассмотрим более подробно обобщенную систему типизации, принятую в NET.

Как явствует из схемы, Common Type System представляет собой иерархию, в которой стрелки указывают в сторону уменьшения общности типа.

Типы иерархии CTS подразделяются на ссылочные типы (pointer type) и типы-значения (value type).

Особенностями ссылочных типов являются необходимость использования указателей на типизированные объекты, а также централизованное хранение и освобождение памяти ("сборка мусора").

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

В свою очередь, ссылочные типы могут принимать одну из трех форм:

1. объектные типы (object type);

2. интерфейсные типы (interface type);

3. типы указателей (pointer type).

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

Таблица 6.1. Отображение типов языка программирования SML в типы иерархии CTS

№	Тип	Класс NET
1	int	System.Int32	Целое число
2	string	System.String	Строка
3	bool	System.Boolean	Логическое значение
...	...	...	...

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

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

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

Во-вторых, технологическая платформа NET обеспечивает ряд несомненных дополнительных преимуществ перед другими известными платформами в отношении системы типов.

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