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

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

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

Лекция 8. Синтаксис языков программирования

программный синтаксис комбинаторный логика

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Прежде всего, необходимо договориться об обозначениях.

Рассмотрим традиционные обозначения БНФ и поясним смысл каждого из них.

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

Определяющий символ "::=" отделяет определяемую конструкцию от составляющих ее ранее определенных базовых конструкций.

Определяемая конструкция записывается слева от "::=" в угловых скобках "<" и ">".

Альтернативы (возможные варианты) конструкций перечисляются по вертикали.

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

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

<выражение> ::= <константа> | <переменная> |

(<выражение> <выражение>) |

л <переменная> . <выражение>

Поясним смысл приведенных обозначений.

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

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

2. переменной;

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

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

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

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

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

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

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

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

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

В частности, рассмотрим структуру основных синтаксически допустимых типов выражений языка.

Приведем соответствующую формализацию в терминах БНФ.

<выражение> ::= <идентификатор> | <литерал> |

<выражение> <выражение> |

<выражение> <идентификатор> <выражение>

Как видно из БНФ-формализации, синтаксически корректным выражением в языке программирования SML считается:

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

2. литерал (литералы будут рассмотрены далее в ходе лекции) или

3. последовательность из двух выражений или

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

Продолжим обсуждение выражений.

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

if <выражение> then <выражение>

else <выражение> |

(<выражение> ... <выражение>) |

let <описание> in <выражение> end |

(<выражение>)

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

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

3. описание и выражение, соединенные зарезервированными словами let ("положим"), in ("в") и end ("конец"), которые определяют операцию подстановки описания в выражение с учетом всевозможных вхождений в него указанного фрагмента описания;

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

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

Перейдем к рассмотрению структуры синтаксически допустимых видов описаний объектов языка.

Приведем соответствующую формализацию в терминах БНФ.

<описание> ::=

val < идентификатор > = < выражение > |

fun < идентификатор > < идентификатор > =

< выражение > |

local < описание > in <описание> end

Синтаксически допустимыми описаниями языка программирования SML, как следует из представленной БНФ, являются:

1. идентификатор и выражение, соединенные зарезервированными словами val и "=", которые обозначают связывание идентификатора (переменной, константы или другого синтаксически допустимого объекта языка программирования) с тем или иным выражением;

2. три идентификатора и выражение, соединенные зарезервированными словами fun и "=", которые обозначают связывание функции (обозначенной первым идентификатором) с параметром (обозначенным вторым идентификатором) с выражением, определяющим порядок вычисления значения;

3. два описания, соединенные зарезервированными словами local, in и end, которые обозначают локальное определение первого описания в контексте второго.

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

Перейдем к рассмотрению структуры синтаксически допустимых описаний типов объектов языка.

Приведем соответствующую формализацию в терминах БНФ.

<тип> ::= int | bool |

<тип> * ... * <тип> |

<тип> -> <тип>

Как следует из представленной БНФ, синтаксически допустимыми типами языка программирования SML являются:

1. целочисленные величины, обозначаемые зарезервированным словом int;

2. логические значения, обозначаемые зарезервированным словом bool;

3. кортежи - упорядоченные n-ки элементов определенных типов;

4. функции - упорядоченные n-ки элементов определенных типов, соединенных зарезервированными символами "->".

Рассмотрим следующий пример, иллюстрирующий приписывание типов в языке SML. Константа типа кортеж вида (0,false,1,true) имеет тип (int*bool*int*bool).

Заметим, что варианты типов (1) и (2) являются элементарными, тогда как (3) и (4) представляют собой производные типы с явно указанной (или выводимой) структурой, откуда и происходит название "структурированный тип".

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

Рассмотрим подробнее синтаксические особенности основных видов литералов.

Приведем соответствующую формализацию в терминах БНФ.

<литерал> ::= <литерал целого типа> |

<литерал строкового типа> |

<литерал вещественного типа>

Как следует из представленной БНФ, синтаксически допустимыми типами литералов в языке программирования SML являются следующие:

1. целочисленные литералы, имеющие тип int и лежащие в диапазоне от -230 до +230 (последнее обстоятельство связано с особенностями машинного представления данных);

2. строковые литералы, имеющие тип string и представляющие собой алфавитно-цифровые последовательности символов в коде формата ASCII;

3. вещественные литералы, имеющие базовый тип real, обобщенную форму вида M x 10E, где M - мантисса в диапазоне от -1 до +1, а E - порядок в соответствующем диапазоне.

Заметим, что значение (т.е. семантика) литералов в полной мере определяется их лексическим (а, значит, и синтаксическим) представлением.

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

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

Приведем соответствующую формализацию в терминах БНФ:

<выражение> <выражение>

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

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

Рассмотрим функцию succ, которая задается определением

fun succ n = n+1;

и осуществляет прибавление единицы к (целочисленному) аргументу.

Для рассматриваемой функции succ синтаксически корректная аппликация может иметь вид succ 2 и вычисляться в ходе выполнения программы в значение 3.

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

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

Приведем соответствующую формализацию в терминах БНФ:

if <выражение> then <выражение> else <выражение>;

Как видно из БНФ-формализации, синтаксически корректное условное выражение состоит из трех подвыражений, соединенных зарезервированными словами if, then и else, уже упоминавшихся нами в ходе лекции.

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

Заметим также, что функции сравнения встроены в язык SML и имеют вид: "=" (равно), "<" (меньше), ">" (больше), "<=" (меньше или равно), ">=" (больше или равно), "<>" (не равно). Результатом вычисления любой из этих функций является логическое значение.

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

if n>=10 then 1 else 0;

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

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

Рассмотрим структуру синтаксически допустимых конструкций, известных под названием let-выражений.

Приведем соответствующую формализацию в терминах БНФ:

let <описание> in <выражение> end;

Как видно из БНФ-формализации, синтаксически корректное let-выражение состоит из описания и выражения, соединенных зарезервированными словами let, in и end.

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

Проиллюстрируем синтаксис let-выражений примерами из языка программирования SML.

Рассмотрим следующие let-выражения:

let val n=2 in n+1 end;

let k=9876*8765 in (k-1, k, k+1) end;

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

В ходе лекции неоднократно упоминалось понятие кортежа.

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

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

(<выражение>, ..., <выражение>)

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

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

Проиллюстрируем синтаксис конструкции кортежа примерами из языка программирования SML:

Пример 1: (1, 2*1, 2*2*1)

Пример 2: (1, true, 0, false)

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

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

Рассмотрим формализации синтаксически корректных описаний переменных и функций в терминах БНФ:

<описание> ::=

val <идентификатор> = <выражение>

<описание> ::=

fun <идентификатор> <идентификатор> =

<выражение>

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

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

Пример 1. val x=2;

Пример 2. fun fact n =

if n<2 then 1

else n * fact (n - 1);

Пример 3. fun f (x,y) = x*x + y*y;

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

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

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

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

· БНФ являются актуальной и адекватной формализацией синтаксиса языка;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Приведем определения перечисленных способов комбинирования доменов.

Под функциональным пространством из домена D1 в домен D2 будем понимать домен [D1->D2], содержащий всевозможные функции с областью определения из домена D1 и областью значений из домена D2 :

[D1 -> D2] = {f | f : D1 -> D2}.

Под декартовым (или, иначе, прямым) произведением доменов

D1, D2, ... Dn будем понимать домен всевозможных n-ок вида

[D1 Ч D2 Ч ... Ч Dn]= {(d1 Ч d2 Ч ... Ч dn) | d1 D1, d2 D2, dn Dn ...,}.

Под последовательностью D* будем понимать домен всевозможных конечных последовательностей вида d=(d1,d2,...,dn) из элементов d1,d2,...,dn,... домена D, где n>0.

Наконец, под дизъюнктной суммой будем понимать домен с определением

[D1+D2+...+Dn]={ (di, i) | diDi, 0<i<n+1 },

где принадлежность элементов di компонентам Di однозначно устанавливается специальными функциями принадлежности.

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

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

Язык SMalL содержит множество выражений E, которые формализуются посредством БНФ в следующем виде:

E ::= true | false | 0 | 1 | I | -E |

E1==E2 | E1+E2

Заметим, что выражения включают логические (true и false) и целочисленные (в ограниченном объеме: 0 и 1) константы, множество идентификаторов (I), а также операции отрицания (-E), сравнения (E1==E2) и сложения (E1+E2).

Кроме того, язык SMalL содержит множество команд С, которые формализуются посредством БНФ в следующем виде:

С ::= I=E | if (E) C1 else C2 |

while(E) C | C1;C2

Отметим, что команды включают присваивание (I=E), условие (if (E) C1 else C2), цикл с предусловием (while(E) C), а также последовательность команд (C1;C2).

Деление синтаксиса языка SMalL на выражения и команды во многом является условным и служит иллюстративным целям.

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

Приведем порядок построения формальной модели семантики языка программирования SMalL согласно ранее представленному формальному описанию синтаксиса языка в терминах БНФ.

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

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

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

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

Заметим, что при выполнении программы (в частности, написанной на языке программирования SMalL) происходит изменение состояния памяти (m, memory), которое в простейшем случае характеризует соответствие идентификаторов и значений (то есть, по сути, связывание переменной со значением), либо имеет значение unbound (характеризующее отсутствие связи идентификатора со значением, т.е. аналог свободной переменной).

В соответствии с намеченной схемой рассуждений перейдем к описанию синтаксических доменов, которые в полной мере определяют синтаксис языка SMalL:

Ide = {I | I - идентификатор};

Com = {C | C - команда};

Exp = {E | E - выражение}.

Совокупность всех возможных идентификаторов языка SMalL организуем в домен Ide, команд - в домен Com, и, наконец, выражений - в домен Exp.

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

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

Параметр	Домен	Соотношение
Состояние	State	(s) State=Memory
Память	Memory	(m) Memory = Ide -> [Value+{unbound}]
Значение	Value	(v) Value=Int+Bool

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

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

Приведем семантические предложения для выражений языка программирования SMalL:

E : Exp -> [State -> [[Value, State] +

{error}]];

E[E]s = (v,s'),

если v - значение E в s,

s'- состояние после означивания;

E[E]s = error,

если возникает ошибка несоответствия типов.

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

Приведем семантические предложения для команд языка программирования SMalL:

С : Com -> [State -> [ State + {error}]].

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

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

E[0]s = (0,s);

E[1]s = (1,s);

Как видно из приведенных соотношений, денотатами констант целочисленного типа являются значения этих констант (в форме упорядоченных пар вида "значение"-"состояние"), причем смены состояния программы не происходит. Рассмотрим семантические предложения для денотатов констант логического типа языка SMalL:

E[true]s = (true,s);

E[false]s = (false,s);

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

E[I]s = (m,I=unbound) error, -> (m,I,s).

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

Рассмотрим семантические предложения для денотатов выражений языка SMalL:

E[-E]s=(E[E]s=(v,s'))

(isBool -> (not v,s'),error,error;

E[E1=E2]s=(E[E1]s=(v1,s1)) ->

(E[E2]s1= (v2,s2)) ->

(v1 = v2,s2),error),error;

E [E1+E2]s = (E [E1] s=(v1,s1)) ->

(E [E2]s1 = (v2,s2)) ->

(IsNum v1 and IsNum v2 -> v1+v2,s2),error),

error),error.

Проанализируем полученные соотношения.

Денотатом отрицания выражения является отрицание его значения; причем состояние программы изменяется. В случае несоответствия типов или небулевости выражения генерируется сообщение об ошибке.

Денотатом присваивания является присвоенное значение в новом состоянии. В случае несоответствия типов генерируется сообщение об ошибке.

Денотатом сложения является значение суммы в новом состоянии. В случае несоответствия типов генерируется сообщение об ошибке.

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

Кратко резюмируем итоги лекции.

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

По итогам обсуждения можно сделать следующие выводы:

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

2. теория вычислений является актуальной и адекватной формализацией семантики;

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

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

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

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

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

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

1. функция;

2. множество;

3. тип.

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

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

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

В качестве практической иллюстрации определения понятия рекурсии рассмотрим ряд примеров рекурсивных функций, описанных на языке программирования 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 было упомянуто понятие рекурсивного типа для списков.

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

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

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

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

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

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

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

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

Для задания рекурсивных типов в SML используются определения типов datatype следующего вида:

<определение типа>:: =

datatype <имя типа> = <описание типа>;

где

<описание типа>:: =

<выражение> |

<имя элемента типа> of <конструктор>

причем под конструктором понимается запись вида

<конструктор> = <тип> * ... * <тип>

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

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

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

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

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

Приведем описание списка из целочисленных элементов на языке SML:

datatype intlist = nil | element of int * intlist;

Приведем описание бинарного дерева из целочисленных элементов на языке SML:

datatype inttree = empty |

node of int * inttree * inttree;

Заметим, что операция "|", применяемая для конструирования типов в SML, соответствует конструктору дизъюнктной суммы "+", а операция "*" - прямого произведения доменов "x".

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

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

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

YE = E(YE).

К сожалению, выясняется, что ни один из ранее рассмотренных нами комбинаторов

(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

требуемой возможности не обеспечивает.

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

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

Сформулируем теорему о неподвижной точке функции.

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

Yf = f(Yf).

При этом объект Y имеет конечный вид

Y = лf.(лx.f(xx))(лx.f(xx)),

или, в форме комбинаторной характеристики:

Y = WS(BWB),

где

W = CSI,

C = S(BBS)(KK),

B = S(KS)K.

Таким образом, любая функция имеет "неподвижную точку" в форме комбинатора Y, характеристику которого можно явно представить в базисе комбинаторов {K,S}.

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

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

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

Далее, определим следующий тип данных:

datatype 'a t = T of 'a t -> 'a;

Теперь определим функцию:

val Y = fn f =>

(fn (Tx) => (f (fn a => x (Tx) a)))

(T (fn (Tx) => (f (fn a => x (Tx) a))));

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

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

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

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

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

Итак, существуют следующие ограничения, которые отличают домены от множеств:

1. все рекурсивные определения являются разрешимыми;

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

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

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

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

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

Кратко перечислим основные виды рекурсии.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Абстрактной машиной (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-машина получила от аббревиатур имен своих основных четырех элементов, а именно: