Классификация языков программирования

Проведем классификацию языков и подходов к программированию.

Первые языки программирования возникли относительно недавно. Различные исследователи указывают в качестве времени их создания 20-е, 30-е и даже 40-е годы XX столетия. Нашей задачей является не установление самого раннего языка, а поиск закономерностей в их развитии.

Как и следовало ожидать, первые языки программирования, как и первые ЭВМ, были довольно примитивны и ориентированы на численные расчеты. Это были и чисто теоретические научные расчеты (прежде всего, математические и физические), и прикладные задачи, в частности, в области военного дела.

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

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

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

Следующее десятилетие ознаменовалось появлением языков программирования так называемого "высокого уровня", по сравнению с ранее рассмотренными предшественниками, соответственно именуемыми низкоуровневыми языками.

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

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

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

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

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

Одним из таких примеров является язык Fortran, реализующий вычислительные алгоритмы. Другой пример – язык APL, трансформировавшийся в BPL и затем в C. Основные конструкции последнего остаются неизменными вот уже несколько десятилетий и присутствуют в языке C#, который нам предстоит изучить.

Примеры других языков программирования: ALGOL, COBOL, Pascal, Basic.

В 60-х годах возникает новый подход к программированию, который до сих пор успешно конкурирует с императивным, а именно, декларативный подход.

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

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

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

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

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

Различные диалекты языка LISP (в частности, Interlisp, Common Lisp, Scheme), возникли потому, что ядро и идеология этого языка оказались весьма эффективными при реализации символьной обработки (анализе текстов).

Другие характерные примеры декларативных языков программирования: SML, Haskell, Prolog.

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

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

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

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

Концепция и возможности подхода .NET

Попытаемся найти ответ на вопрос: что такое .NET? Несмотря на популярность термина, однозначно ответить непросто, прежде всего по той причине, что ответ представляется многоаспектным.

Итак, можно сказать, что .NET – это подход к проектированию и реализации программного обеспечения, включающий, по меньшей мере, четыре компонента:

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

Остановимся подробнее на каждом из этих аспектов.

Прежде всего, постараемся объяснить идеологию подхода Microsoft .NET.

Самой корпорацией-разработчиком сформулированы приблизительно следующие важнейшие аспекты видения (vision) идеологии .NET:

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

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

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

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

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

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

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

Универсальный интерфейс .NET Framework обеспечивает интегрированное проектирование и реализацию компонентов приложений, разработанных в соответствии с различными подходами к программированию.

Говоря о .NET как о технологической платформе, нельзя не отметить тот факт, что она обеспечивает одновременную поддержку проектирования и реализации программного обеспечения с использованием различных языков программирования. При этом поддерживаются десятки языков программирования, начиная от самых первых (в частности, COBOL и FORTRAN) и заканчивая современными (например, C# и Visual Basic). Ранние языки программирования до сих пор активно используются, в частности, для обеспечения совместимости с ранее созданными приложениями (скажем, COBOL весьма широко применялся для создания прикладных программ, поддерживающих финансовую деятельность).

Технология web-сервисов – это не просто дань моде на Internet, а реальная (и, пожалуй, наиболее приемлемая практически) возможность обеспечения масштабируемости и интероперабельности приложений.

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

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

Немаловажно отметить и то обстоятельство, что новая технология .NET не только востребована мировой общественностью, но и официально признана, что отражено в соответствующих стандартах ECMA (European Computer Manufacturers Association).

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

Классификация подходов к программированию была построена нами в ходе лекции 1.

Сосредоточимся на важнейшем для данного курса функциональном подходе к программированию.

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

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

Что касается первой реализации, то она появилась в 50-х годах XX столетия в форме языка LISP, о котором речь пойдет далее.

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

Функциональный подход породил целое семейство языков, родоначальником которых, как уже отмечалось, стал язык программирования LISP. Позднее, в 70-х годах, был разработан первоначальный вариант языка ML, который впоследствии развился, в частности, в SML, а также ряд других языков. Из них, пожалуй, самым "молодым" является созданный уже совсем недавно, в 90-х годах, язык Haskell.

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

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

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

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

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

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

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

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

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

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

(a,b)

A ? B,

таких, что если

(a,b1)

f и (a,b2)

f,

то

b1 = b2.

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

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

Более точно это исчисление следует именовать исчислением ламбда-конверсий.

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

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

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

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

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

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

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

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

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

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

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

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

Функции и типы

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

fun square(x:int) = x*x

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

Возможно также задание функции с использованием fn-выражения

val square = fn x => x * x.

Базисные типы и функции языка SML.

bool — логический тип данных. В модуле bool над ним определены такие операции, как отрицание (val not: bool -> bool), преобразование к строковому типу (val toString: bool -> string), а также преобразование из строкового типа (val fromString: string -> bool). word — тип, представляющий из себя целое число без знака, и, как правило, хранящийся в форме машинного представления слова. В соответствующем модуле определены преобразования для данного типа (например, val toInt : word -> int), а также арифметические (например, val + : word * word -> word) и логические (например, val > : word * word -> bool) операции. char — символьный тип данных. В модуле char также определены функции преобразования (val toString : char -> String.string), логические операции (val isDigit : char -> bool) и другие функции. real — число с плавающей точкой. В модуле real определены операции преобразования (val toString : real -> string), а также сравнения (val >= : real * real -> bool), преобразования форматирования и точности (val maxFinite: real). int — целочисленный тип. string — тип символьной строки.

Общее описание типов данных и функций SML.NET хранится в форме файлов с описанием интерфейса в директории \src\basis целевого каталога компилятора.

Теоретические сведения

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

Типы, объекты и методы .NET

Проиллюстрируем фрагмент отображения типов языка SML.NET в систему типов Common Type System.

Соответствие типов .NET и типов SMLТип .NETТип SML.NET

System.Boolean	bool
System.Byte	Word8.word
System.Char	char
System.Double	real
System.Single	Real32.real
System.Int32	int
System.Int64	Int64.int
System.Int16	Int16.int
System.Sbyte	Int8.int
System.String	string
System.UInt16	Word16.word
System.UInt32	word
System.UInt64	Word64.word
System.Exception	exn
System.Object	object

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

type XMLParser = string -> System.Xml.XmlDocument

Следующая программа иллюстрирует использование типов SML и Common Type System .NET:

structure builtintypes_demo = struct

fun main () = ( print ( "cosh(1.2) = " ^ Real.toString( System.Math.Cosh(1.2)) ^ "\n"); print ( "System.Int32.MinValue = " ^ Int.toString( System.Int32.MinValue) ^ "\n"); print (valOf (System.Char.GetUnicodeCategory( #"Z").#ToString())) )

end

Варианты заданий

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

Целью лабораторных работ является иллюстрация

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

32-разрядная операционная система Microsoft Windows 98, ME, 2000, XP, 2003.Интегрированная среда разработки Microsoft Visual Studio .NETКомпилятор SML.NET.
Код SML.NET может быть также откомпилирован на следующем программном обеспечении:

32-разрядная операционная система Microsoft Windows 98, ME или 2000, XP, 2003.Платформа разработки Microsoft.NET Framework SDK или Microsoft.NET Framework Redistr.Компилятор SML.NET.
Компилятор для языка программирования SML в среде Microsoft .NET доступен по адресу: http://www.cl.cam.ac.uk/Research/TSG/SMLNET
Условия и правила использования среды разработки приложений Microsoft Visual Studio .NET доступны по адресу: http://www.msdn.microsoft.com/vstudio/
Описание основных функций языка программирования SML доступно по адресу: http://www.standardml.org/

Сформулируйте формальную постановку задачи, запишите

Сформулируйте формальную постановку задачи, запишите правила вывода и реализуйте программу на SML в соответствии с вариантом исполнения.

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

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

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

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

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

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

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

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

алфавит;утверждения;аксиомы;правила вывода.

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

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

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

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

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

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

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

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

Константы c 1

, c 2

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

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

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

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

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

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

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

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

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

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

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

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

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

(I) Ix = x; (K) Kxy = x; (S) Sxyz = xz(yz).

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

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

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

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

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

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

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

Другим способом определения типа 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) означает существование комбинатора (функции) взятия первой проекции, т.е. первого элемента упорядоченной пары или первого элемента списка. Интуитивно ясно, что эта аксиома близка языкам функционального программирования, оперирующим списками, и соответствует фундаментальной операции взятия головного (первого) элемента списка.

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

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

Теоретические сведения

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

x+y = y+x

определить функцию

alpha(x,y) = x + y

и оператор С

(Cf)(x,y) = f(xy),

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

alpha = C alpha.

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

fun Ix = x; fun Kxy = x; fun Sxyz = xz(yz);

Напомним, что характеристики перечисленных комбинаторных термов в рамках формальной системы комбинаторной логики имеют вид:

Ix = x, Sxyz = xz(yz), Kxy=x.

Варианты заданий

Выразить в базисе {K,S} комбинаторы с заданными характеристиками, убедиться в справедливости произведенных преобразований:

I, где Ia = a; B, где B abc = a(bc); C, где C abc = acb; W, где W ab = abb; Y, где Y abcd = a(bc)(bd); C[2], где C[2] abcd = acdb; C[2], где C[2] abcd = adbc; Y, где Ya = a (Ya); C[3], где C[3] abcde = acdeb; C[3], где C[3] abcde = aebcd; B3, где B3 abcde = a(bcde); F, где F abcd = a(bd)(cd);

Выразить в базисе {B,C,S} комбинаторы с заданными характеристиками, убедиться в справедливости произведенных преобразований:

I, где Ia = a; K, где K ab = a; S, где S abc = ac(bc); W, где W ab = abb; Y, где Y abcd = a(bc)(bd); C[2], где C[2] abcd = acdb; B2, где B2 abcd = a(bcd); Y, где Ya = a (Ya); C[3], где C[3] abcde = acdeb; C[3], где C[3] abcde = aebcd; F, где F abcd = a(bd)(cd).

Сформулируйте формальную постановку задачи, запишите

Синтаксис языков программирования

Формализуем основные конструкции языка программирования SML посредством форм Бэкуса-Наура или БНФ (история их создания изложена во вступительной лекции).

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

Определим понятие синтаксиса более строго.

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

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

Основной задачей синтаксиса является определение формы и вида допустимых языковых конструкций. Эту задачу можно решить путем перечисления описаний всех языковых конструкций. Одним из механизмов такого описания является уже упомянутая нами нотация БНФ

Мы будем рассматривать параллельно БНФ-формализации синтаксиса ламбда-исчисления и языка программирования SML. В последнем случае мы ограничимся базовым набором конструкций языка, подчеркнув такие существенные возможности, как кортежи (tuples) и let-выражения.

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

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

По завершении лексического анализа выполняется так называемая процедура синтаксического разбора текста программы, которая представляет собой проверку корректности синтаксиса текста, написанного на языке программирования.
Эта процедура, возможно, включает выполнение проверки корректности типизации в той или иной форме.
Наконец, в случае, если все конструкции языка, присутствующие в тексте программы, являются синтаксически корректными, а также не выявлено несоответствий типов, запрещенных с точки зрения анализатора корректности типизации, производится преобразование текста программы в промежуточный код (ассемблер, код той или иной абстрактной машины) или собственно машинный код.
Рассмотрим синтаксис языка программирования SML в сравнении с синтаксисом ламбда-исчисления.
Для большей наглядности и сопоставимости формализаций синтаксиса обоих языков (языка формальной математической теории и языка программирования) будем использовать единую нотацию, а именно, БНФ.
Прежде всего, необходимо договориться об обозначениях.
Рассмотрим традиционные обозначения БНФ и поясним смысл каждого из них.
Фактически БНФ представляют собой определения одних понятий через другие. При этом понятия заключаются в угловые скобки, и используется ряд специализированных символов и соглашений, суть которых поясняется далее.
Определяющий символ "::=" отделяет определяемую конструкцию от составляющих ее ранее определенных базовых конструкций.
Определяемая конструкция записывается слева от "::=" в угловых скобках "<" и ">".
Альтернативы (возможные варианты) конструкций перечисляются по вертикали.
Цитирование (подобно тому, как мы цитировали специальные символы, заключая их в двойные кавычки) не имеет обозначения.
Проиллюстрируем формализацию синтаксиса посредством нотации БНФ, рассмотрев в качестве примера формальной системы хорошо знакомое нам по предыдущим лекциям ламбда-исчисление.
<выражение> ::= <константа> | <переменная> | ( <выражение> <выражение> ) | ? <переменная> . <выражение>
Поясним смысл приведенных обозначений.
В данном примере определяется понятие выражения, синтаксическое представление которого может быть выражено в виде одной из следующих альтернатив:

константы;переменной;двух выражений, заключенных в круглые скобки, т.е. знакомой нам операции аппликации ламбда-выражений;символа ?, за которым следует переменная, точка и выражение, т.е. знакомой нам операции абстракции.
Оказывается, что синтаксис языка программирования SML имеет ряд очевидных аналогий с синтаксисом ламбда-исчисления. Эти аналогии являются неизбежными как в силу функциональной природы рассматриваемого языка программирования, так и на том основании, что язык SML разрабатывался как средство доказательства теорем, а, значит, его синтаксис (а, забегая вперед, заметим, что и семантика) должен быть прозрачен математически.
Для иллюстрации перечисленных выше тезисов рассмотрим важнейшие синтаксические категории языка программирования SML.
Под выражением будем далее понимать обозначение конструкции языка, которой может быть присвоено значение (константы, переменной, функции и т.д.).
Описанием будем в дальнейшем называть запись, связывающую выражение языка программирования с именем, обозначающим его в программе (идентификатором).
Под термином "зарезервированное" (или, иначе, служебное)слово будем иметь в виду конструкцию языка, однозначно интерпретируемую в качестве инструкции языка программирования (например, "if", "then", "let"). Напомним, что в данной нотации цитирование производится без кавычек или других символов-ограничителей.
Комментарием назовем произвольный поясняющий текст к программе, который, согласно синтаксису языка SML, положено заключать в ограничители вида "(*" и "*)".

Семантика языков программирования

Представим построение денотационной семантики важнейших функций языка программирования SML.

Напомним, что история развития теории и практики семантического анализа языков программирования была рассмотрена во вступительной лекции.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Оказывается, существует три основных вида семантик, ориентированных на интерпретацию.

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

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

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

Напомним, что теория вычислений Д. Скотта была создана до появления большинства современных языков программирования, а именно в конце 60-х годов.

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

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

Сформулируем последовательность изложения теории вычислений Д. Скотта.

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

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

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

Теоретические сведения

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

Например, простую скобочную запись a(bc) можно представить как в виде аппликации a -> (b -> c), так и в виде двоичного дерева.

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

Создадим рекурсивный тип – бинарное дерево:

datatype tree = Atom of string | Comb of tree * tree

Примем за минимальную синтаксическую единицу один символ и будем считать, что строка представляет из себя последовательную аппликацию с ассоциацией влево (f xyz):

fun Parse [next] = Atom next | Parse (next::rest) = Comb(Atom next, Parse rest);

В результате выполнения процедуры синтаксического анализа

Parse["f", "x", "y", "z"]

получим

val it = Comb (Atom "f",Comb (Atom "x", Comb (Atom "y",Atom "z"))) : tree

В аналогичном случае с ассоциацией влево ситуация будет несколько сложнее.

Запишем основные правила для синтаксического разбора:

f преобразуется в Atom "f"f x преобразуется в Comb(Atom "f", Atom "x")f xy преобразуется в Comb(Comb(Atom "f", Atom "x"), Atom "y")

Запись этих правил на SML будет выглядеть следующим образом:

fun Parser t[] = t | Parser t (next::rest) = Parser (Comb(t, Atom next)) rest; fun Parse [next] = Atom next| Parse (next::rest) = Parser (Atom next) rest; Parse["f", "x", "y", "z"];

Варианты заданий

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

a(bc)(ac)(bc)(ab)(c(de))a(b(cd)(ef))a(b(cd)(ef)g)a(b((cd)(ef))(a(bc(de)f)gh)abb(cdd(e)fg)(ab(c(de))f(g(hi))j)

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

a(bc)ac(bc)(ac)(bc)a(b(cd)(ef))a(b(cd)(ef)g)a(b((cd)(ef))(a(bc(de)f)gh)abb(cdd(e)fg)(ab(c(de))f(g(hi))j)

Сформулируйте формальную постановку задачи, запишите

Сформулируйте формальную постановку задачи, запишите правила вывода и реализуйте программу на SML в соответствии с вариантом исполнения. В качестве целевого типа взять бинарное дерево вида:
tree = Nil | Atom of string | Comb of tree * tree;

Рекурсивные функции и множества

Построим модель рекурсивных вычислений посредством формальной логики.

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

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

функция;множество;тип.

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

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

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

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

Начнем с описания известной нам функции факториала на языке SML:

fun fact n = if (n<2) 1 else n*fact(n-1);

Как следует из описания, значением функции является 1, если значение аргумента не превышает 1, и произведение чисел натурального ряда от 2 до заданного в противном случае. Заметим, что идентификатор функции fact явно присутствует как в левой, так и в правой части описания. Отметим также, что настоящий пример, по сути, представляет собой линейный вариант записи математического определения функции факториала по индукции. Наконец, еще одной особенностью рекурсии является многократность вызова одной и той же функции с различными значениями аргумента.

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

fun length lst = if (lst==[]) 0 else 1 + length(tl(lst));

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

Наконец, рассмотрим рекурсивное определение функции sumpos, суммирующей первые n чисел натурального ряда (и повторяющей отмеченные особенности функции fact):

fun sumpos n = if (n<2) 1 else n + sumpos (n-1);

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

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

Теоретические сведения

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

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

базис индукции: 0!=1;шаг индукции: n!=n*(n-1)!.

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

structure Project2 : sig val main: string option array option -> unit end = struct

fun factorial 0 = 1 | factorial (n:int) = n * factorial (n-1); fun main (a : string option array option) = (*@TODO: add your code here *) ( print ("factorial(4) = " ^ Int.toString(factorial(4)) ^ "\n" ) end

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

fun factorial n = if (n<2) then 1 else n * factorial(n-1);

Возможно рекурсивное определение не только функций, но и типов.

Например, определение списочного типа на языке SML имеет вид:

datatype slist = nil | element of char * slist;

Сформулируйте формальную постановку задачи, запишите

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

Предшествования для целых чисел.Следования для целых чисел.Суммы первых N чисел натурального ряда.Произведения первых N чисел натурального ряда (факториала).Вычисления чисел Фибоначчи.Решения задачи о размещении 8 ферзей на шахматной доске 8х8 так, чтобы никакой из них они не "бил" другого.Решения задачи о "Ханойских башнях".Упорядочения массива.Обхода двоичного дерева слева.Обхода двоичного дерева справа."Балансировки" двоичного дереваПодсчета количества элементов двоичного дерева.Упорядочения списка.Вставки элементов в упорядоченный список.Вставки элементов в "сбалансированное" двоичное дерево.Наибольшего общего делителя по алгоритму Евклида.Суммы N элементов арифметической прогрессии.Суммы N элементов геометрической прогрессии.Решения задачи о ханойских башнях (перемещение диска со стержня А на стержень В отображать посредством вывода текста "А->В").Суммы элементов списка.Инвертирования списка.Произведения с использованием только функции сложения.Суммы с использованием только функции прибавления единицы.

Абстрактные машины и категориальная комбинаторная логика

Рассмотрим особенности моделирования абстрактных машин средствами формальной системы категориальной комбинаторной логики.

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

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

Виртуальные машины представляют собой средство создания промежуточного (следующего за текстом программы на высокоуровневом языке программирования) кода (именуемого в различных реализациях Java-кодом, MSIL-кодом и т.д.), который затем транслируется в машинный код. Заметим, что последний пример промежуточного кода, а именно, MSIL (Microsoft Intermediate Language), представляет собой ни что иное, как код виртуальной машины, реализованной корпорацией Microsoft для технологической платформы .NET.

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

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

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

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

Несмотря на объективные трудности практической реализации, ранние абстрактные машины, безусловно, были весьма значимыми для развития computer science, т.к. предвосхитили появление и обозначили ряд этапов развития реальных компьютеров и языков программирования для них.

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

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

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

Свое название SECD-машина получила от аббревиатур имен своих основных четырех элементов, а именно:

Stack - стек, т.е. последовательность атомарных ламбда-выражений (переменных и констант), а также ламбда-абстракций;

Environment - среда, т.е. хранилище значений, которые связываются с переменными в ходе вычислений; Control - управление, т.е. последовательность "инструкций", управляющих работой SECD-машины;

Dump - дамп, т.е. хранилище состояния SECD-машины (обычно пуст либо содержит прежнее состояние).

Именно перечисленная четверка элементов в полной мере характеризует состояние SECD-машины в произвольный момент вычислений.

Заметим, что именно SECD-машина стала прообразом для более поздних формализаций, на которых реализованы ML-машины, в частности категориальная абстрактная машина (КАМ).

Категориальная абстрактная машина

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

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

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

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

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

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

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

Формальная система с д.з.к. должна удовлетворять следующим условиям:

определена функция тождества, или тождественное преобразование (имеющее в комбинаторной логике аналог в форме комбинатора тождества I); определена операция композиции или построения сложной функции (имеющая в комбинаторной логике аналог в форме комбинатора тождества B); определена операция образования упорядоченной пары объектов < . , . >; определена операция взятия первого элемента из упорядоченной пары объектов; определена операция взятия второго элемента из упорядоченной пары объектов; определена операция преобразования терма из алгебраической формы в аппликативную; определена операция аппликации или применения функции к аргументу.

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

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

(ass) (xoy)z = x(yz); (fst) Fst[x,y] = x; (snd) Snd[x,y] = y; (dpair) <x,y>z = [xz,yz]; (ac) ?[?(x)y,z] = x[y,z]; (quote) (‘x)y = x.

Соотношение (ass) устанавливает связь аппликации и композиции, соотношения (fst) и (snd) – первой и второй проекций и операции образования упорядоченной пары, соотношение (dpair) – спаривания и формирования совокупности, соотношение (ac) – каррирования и апплицирования, а (quote) характеризует цитирование.

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

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

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

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

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

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

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

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

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

Проиллюстрируем кодирование ламбда-терма по де Брейну следующим примером. Пусть требуется закодировать ламбда-терм следующего вида:

?x.?y.((+x)y).

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

?(?(S(S(‘+1),0))).

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

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

Формализуем понятие среды вычислений применительно к категориальной абстрактной машине.

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

(<переменная>, <значение>).

При трансляции ламбда-терма в код де Брейна, который представляет собой пару вида (<терм де Брейна>, <среда>) в соответствии с характеристическими равенствами

0![x,y] = y; (n+1)![x,y] = n!x; S[x,y] z = xz(yz);?(x)yz = x[y,z];

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

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

Переход от кода де Брейна к терму категориальной комбинаторной логики выполняется на основе известных характеристических равенств:

(ass) (xoy)z = x(yz); (fst) Fst[x,y] = x; (snd) Snd[x,y] = y; (dpair) <x,y>z = [xz,yz]; (ac) ?[?(x)y,z] = x[y,z]; (quote) (‘x)y = x.

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

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

< , > Fst Snd ‘ ??.

Оптимизация вычислений и абстрактные машины

Проиллюстрируем особенности реализации наиболее существенных стратегий вычислений на примере КАМ.

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

Кроме того, как показывает практика, именно КАМ больше всего подходит для использования в качестве виртуальной машины при реализации современных языков функционального программирования (в частности, языка CaML), в том числе с объектными расширениями (в частности, языка Object CaML).

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

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

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

Другим существенным недостатком КАМ является отсутствие поддержки рекурсивных вычислений, которое, как мы увидим впоследствии, устраняется посредством модификации среды вычислений.

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

Выявив и оценив недостатки "классической" реализации категориальной абстрактной машины, наметим возможные направления оптимизации программ на языке инструкций КАМ.

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

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

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

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

Приступим к реализации усовершенствований категориальной абстрактной машины с целью оптимизации стратегии вычислений.

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

Заменим "встроенные" в систему команд категориальной абстрактной машины одноместные функции на двухместные.

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

+<x,y> = ?o<?o<'+,x>,y>.

C учетом характеристических равенств для категориальной абстрактной машины , выведенных в ходе предыдущих лекций, получим соотношение

?o<?(x)oy,z> = xo<y,z>,

которое находится в полном соответствии с правилами редукции, принятыми в формальной системе категориальной комбинаторной логики, на основе которой построена КАМ.

Продолжим обсуждение перехода к многоместным операциям в языке программирования категориальной абстрактной машины. Пересмотрим цикл работы (схему смены состояний) категориальной абстрактной машины, расширив пространство состояний КАМ дополнительными инструкциями, которые, по аналогии с основными командами КАМ, представим в форме таблицы 12.1.

Таблица 12.1. Дополнительные инструкции пространства состояний КАМСтарое состояние КАМНовое состояние КАМТермКодСтекТермКодСтек

true	if abc	sm	S	a c	m
false	if abc	sm	S	b c	m
(a,b)	add c	S	{a+b}	C	S
(a,b)	eq c	S	true/false	C	S

<

Как видно из приведенной таблицы, пространство состояний категориальной абстрактной машины расширено посредством введения операций сравнения if, проверки условия eq, а также сложения add. Проиллюстрируем практическую эффективность программного кода усовершенствованной категориальной абстрактной машины следующим примером. Рассмотрим программу категориальной абстрактной машины, вычисляющую сумму целых чисел 2 и 3 в "классической" версии "языка программирования" КАМ:

push cur (push push cdr swap quote 2 cons app swap push cur (cdr) swap quote 3 cons app cons app) swap quote + cons app.

"Запрограммируем" ту же задачу в усовершенствованной версии КАМ:

push quote 2 swap quote 3 cons add.

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

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

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

Пересмотрим цикл работы (схему смены состояний) категориальной абстрактной машины, расширив пространство состояний КАМ дополнительными инструкциями, которые, по аналогии с основными командами абстрактной машины, представим в форме таблицы 12.2.

Таблица 12.2. Дополнительные инструкции КАМ для реализации рекурсивных вычисленийСтарое состояние КАМНовое состояние КАМТермКодСтекТермКодСтек

T	dum c	sm	$Y	C	S
[a:b]	wind c	(t$Y)S	(t.[a:b])	C	S

Как видно из приведенной таблицы, пространство состояний категориальной абстрактной машины расширено посредством введения операций wind и dum для обработки рекурсивных объектов.

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

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

При вычислении с вызовом по значению (call-by-value) все выражения должны быть означены до вычисления операции аппликации.

При вычислении с вызовом по имени (call-by-name) до вычисления операции аппликации необходима подстановка термов вместо всех вхождений формальных параметров перед означиванием. Именно эта стратегия лежит в основе "ленивых" (lazy), "отложенных" (delayed) или "замороженных" (frozen) вычислений, которые принципиально необходимы для обработки потенциально бесконечных структур данных.

Наконец, при вычислении с вызовом по необходимости (call-by-need) ранее вычисленные значения аргументов сохраняются в памяти компьютера только в том случае, если необходимо их повторное использование.

Чтобы устранить сложности с поддержкой категориальной абстрактной машиной "ленивых" вычислений, пересмотрим цикл работы КАМ, расширив пространство состояний дополнительными инструкциями для "замораживания" (freeze) и "размораживания" (unfreeze), которые представим в форме таблицы 12.3.

Таблица 12.3. Дополнительные инструкции КАМ для реализации "ленивых" вычисленийСтарое состояние КАМНовое состояние КАМТермКодСтекТермКодСтек

s	{freeze c}.C1	S	C.s	C1	S
C.s	unfreeze.C	S	s	C	S
s	unfreeze.C	S	s	C	S

Теоретические сведения

Категориальная абстрактная машина - это математическая формализация компьютера на основе категориальной комбинаторной логики.

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

Состояние категориальной абстрактной машины в произвольный момент времени характеризуется тройкой объектов:

<T,C,S>

где T - терм, C - код, S - стек или дамп.

Основными инструкциями КАМ являются следующие:

Fst Snd < , > e L ' car cdr push swap cons app cur quote

SML-функции для первых двух из этих инструкций имеют вид:

fun Fst(x,_)=x; fun Snd(_,y)=y;

Сформулируйте формальную постановку задачи, запишите

Сформулируйте формальную постановку задачи, запишите правила вывода и реализуйте программу на SML в соответствии с вариантом исполнения.
Реализовав необходимые инструкции КАМ (Fst, Snd, "<", ">", e, L, " ' ", car, cdr, push, swap, cons, app, cur, quote), после преобразования в ламбда-выражение и КАМ-код, провести максимально возможное число шагов преобразования кода и при возможности вычислить значение терма:

4!1+2+3+4