3.4 Базовое обучение на основе аппликативной среды информационного моделирования в учебнике М. Броя “Информатика. Основополагающее введение.” Часть I.
3.4.1 Пример базового обучения на основе аппликативного стиля.
Проблема базового обучения, включающего предъявление взаимодополняющих семантик, нашла свое отражение и в уже упоминавшемся во введении учебнике М. Броя “Информатика. Основополагающее введение.” Совпадение наших задач диктует необходимость более пристального взгляда на позицию автора. При ее рассмотрении уместно воспользоваться следующей точкой зрения - стиль программирования во многом определяется логикой, лежащей в основе [Гоген Дж.А., Мезегер Ж. “Модели и равенство в логическом программировании”, 1991]. В этом ключе в учебнике:
1) в начале исследуются возможности эквациональной логики, используется СПТ - система подстановки термов (что естественно для вхождения в аппликативную среду информационного моделирования);
“Пример (алгоритмы Маркова). Пусть задана система подстановок R на множестве символов { Ú, Ø, true, false, (, ) } для редукции булевских термов, которые построены только из символов данного множества, к нормальной форме. Эта система состоит из следующих правил:
(1) ØØ ® e
(2) Øtrue ® false
(3) Øfalse ® true
(4) (true) ® true
(5) (false) ® false
(6) falseÚ ® e
(7) Úfalse ® e
(8) trueÚtruе ® true
Алгоритм, определенный данной системой, работает по марковской стратегии корректно для замкнутых булевских термов (т.е. замкнутые булевские термы переводятся в семантически эквивалентные однозначные нормальные формы, состоящие из true и false). Это справедливо даже для замкнутых термов с неполностью расставленными скобками. Однако в этом случае возможны такие применения, которые не являются эквивалентными преобразованиями. Для терма
Øtrue Ú true
по марковской стратегии получаются вычисления:
Øtrue Ú true ® (правило (2) )
false Ú true ® (правило (6) )
true
В общей недетерминистической стратегии дополнительно получают (в смысле постановки задачи корректное) вычисление:
Ø true Ú true ® (правило (8) )
Ø true ® (правило (2) )
false “
2) затем происходит расширение эквациональной логики до многосортной логики через алгебраическую систему (у М. Броя - “вычислительную систему”). Здесь же вводится денотационная семантика, так как уже появляются функции.
“Пример вычислительной структуры ВООL.
Вычислительная структура ВООL булевских значений
Множество S типов вычислительной структуры ВООL задано так:
S = {bооl}.
Множество F символов функций структуры BOOL задано так:
F = { true , false , Ø , Ú, Ù }.
Множество данных В^ сопоставлено типу bооl, т.е. имеет место
bооlBOOL = В^ = {L, О, ^}
Для лучшей читаемости символы двуместных функций ¦ часто записываются в инфиксной форме. Вместо ¦(x, y) мы пишем выражение x ¦ y. Употребление инфиксной записи указывается через комментарии при задании функциональной зависимости. Аналогично будем записывать и символ ¦ одноместной функции - иногда предпочтем запись ¦ x вместо ¦(x). Символы функций обозначают следующие типы функции:
trueBOOL : ®В^,
falseBOOL : ®В^,
ØBOOL : В^®В^, бесскобочный префикс
ÙBOOL : В^´В^®В^, инфикс
ÚBOOL : В^´В^®В^. инфикс
Причем для а, b Î В имеет место (это уже описания функций):
trueBOOL = L, falseBOOL = О,
ØBOOL b=nоt(b), а ÚBOOL b = оr(а,b), а ÙBOOL b = аnd(а,b). “
3) требования реального программирования (динамические структуры) вынуждают перейти к инициальным моделям и, таким образом, к логико-алгебраическим спецификациям.
“Пример (двоичные деревья).
Пусть М - произвольное множество. Множество TREE(M) конечных, слоистых двоичных деревьев над М определяется индуктивно следующим образом:
(1) пустое дерево e есть элемент TREE(M),
(2) если t1, t2 Î TREE(M), то есть t1 и t2 - конечные деревья, то тройка (t1, x, t2) для каждого xÎM есть конечное дерево. Тогда x называется корнем дерева (t1, x, t2), t1 называется левым поддеревом, t2 - правым поддеревом.
Множество двоичных деревьев над натуральными числами N представляется следующим образом:
TREE(N) = { e,
(e, 0, e), (e, 1, e), ...
((e, 0, e), 0, e), ((e, 0, e), 1, e), ...
(e, 0, (e, 0, e)), (e, 1, (e, 0, e)), ... }”
Однако, нельзя не отметить главные недостатки (по крайней мере с точки зрения рассматриваемых в дипломе позиций). Во-первых, наблюдается диспропорция материала -богатство прагматического уровня и бедность теоретического, служащего обоснованием денотационной семантики рекурсии динамических структур. Во-вторых, теоретическое значение логико-алгебраических спецификаций здесь как бы “зависает”, так как дается инициальная модель и явно фиксируются равенства, заведомо ей удовлетворяющие. При этом не обсуждаются возникающие вопросы логико-алгебраической спецификации:
a) проблема полноты,
b) проблема непротиворечивости.
Итак, учебник М. Броя является примером базового обучения на основе аппликативной среды информационного моделирования с элементами логико-алгебраической спецификации при определении типов данных..
* Синтаксис: описание формального языка с помощью БНФ. В одноименном пункте М. Брой обсуждает синтаксис, формальный язык БНФ через индуктивное определение регулярных выражений (через неподвижную точку теретико-множественного решения уравнения). Можно говорить о регулярных языках двумя способами - через грамматики (порождение) и через множество слов (языки). М. Брой выбирает второе и, говоря о БНФ-нотации, вводит понятие регулярных выражений. Посмотрим, как естественно получилось увязать понятия языка и теоретико-множественного восприятия БНФ.
“При определении формальных языков для установления контекстно-свободного синтаксиса ЯП в дальнейшем вводится так называемая БНФ-нотация (форма Бэкуса-Наура). БНФ-нотация позволяет, в частности, писать выражения, которые определяют множество последовательностей символов, т.е. формальных языков.
Эти выражения, в силу простоты их построения, называют также регулярными выражениями.
Пример (десятичная запись чисел как регулярное выражение). Множество последовательностей символов, которые представляют целые числа в десятичной записи без ведущих нулей, может быть описано следующим образом:
0ï[{-}[1ï2ï3ï4ï5ï6ï7ï8ï9]{0ï1ï2ï3ï4ï5ï6ï7ï8ï9}*]
Пусть С - множество символов, называемых терминальными символами. Регулярные выражения над множеством символов С определяют формальный язык, т.е. подмножество из С*. B дальнейшем будут заданы отдельные элементы регулярных выражений и их значение.
(0) Терминальные символы: Пусть с есть символ из множества С терминальных символов; тогда с есть регулярное выражение с языком {c}.
(1) Объединение: пусть R и Q -регулярные выражения с языками Х и Y; тогда
RïQ
обозначает регулярное выражение с языком ХÈY.
(2) Конкатенация: пусть R и Q - регулярные выражения с языками Х и Y; тогда
RQ
обозначает регулярное выражение с языком {xoy: xÎX, yÎY }.
(3) Опция, итерация, расстановка скобок, пустой язык: пусть R - регулярное выражение с языком Х; тогда обозначает:
(a) {R}- регулярное выражение с языком XÈ{e},
(b) {R}* - регулярное выражение с языком
{x1o...oxn: nÎN Ù x1,...,xnÎX},
(c) {R}+ - регулярное выражение с языком
{x1o...oxn: nÎN Ù n>0 Ù x1,...,xnÎX},
(d) [R]- регулярное выражение с языком Х,
(е) {}- регулярное выражение с языком Æ.”
Следует отметить важность такого подхода, так как включается теоретическое обобщение, которое работает во многих случаях - при определении типов данных, рекурсивных функций, формальных языков.
БНФ-нотация как средство описания синтаксиса формального языка активно используется автором во всех следующих главах для определения языка аппликативной среды программирования.
* Функции.
Что касается описания функции, следует отметить проводимую параллель с математическим описанием. При этом ставится проблема свободных идентификаторов, которая решается с помощью понятия абстракции функции. Сразу же возникают понятия связывания, l-абстракции, a-конверсии. (стр. 117, 121, 127).
Объявления обозначений элементов данных и функций рассматриваются как расширение аппликативных языков. При объявлении функции автор подчеркивает единство объявления идентификатора функции, типа и спецификации вычислений.
“...идентификаторы для функций объявляются ("принимаются соглашения") с помощью записи вида
fсt ¦=(s1 х1,..., sn хn)s: Е
и говорят об объявлении функции или соглашении о функции. В объявлении функции одновременно и вводится идентификатор для функции, функциональность которой задается, и специфицируется ход (процесс) вычисления отображения.
Пример (объявления функций)
(1) Идентификатор аbs связывается с функцией ¦(х)=ïхï с помощью следующего объявления:
fсt аbс=(int х)int:
if 0£х then х else -х fi”
При объявлении функций рассматривается функциональная семантика как не рекурсивного, так и рекурсивного объявлений. Подробней о семантике рекурсивных объявлений - ниже.