2 Постановка задачи: о связном предъявлении теории информатики и практики программирования в теме исполнения для теоретического мышления. 13 Содержание 1 Введение. 1.1. Позиция в отношении к предмету. 1.2. Составляющие обучения. 2 Постановка задачи: о связном предъявлении теории информатики и практики программирования в теме ИСПОЛНЕНИЯ для теоретического мышления. 3 Аппликативный стиль. Денотационная семантика. (класс Прагматика). 3.1 Проблемная ориентированность (программистский аспект). 3.1.1 Сравнение языков программирования стиля. 3.1.2 Неподвижная точка как подходящее обобщение проблемной ориентированности. 3.2 Редукционные реализации (математический аспект). 3.3 Модели теорий и типовые языки (системологический аспект). 3.3.1 О моделях l-алгебры или l-теории. 3.3.2 Общие аспекты, связанные с неподвижной точкой. 3.4 Базовое обучение на основе аппликативной среды информационного моделирования в учебнике М. Броя “Информатика. Основополагающее введение.” Часть I. 3.4.1 Пример базового обучения на основе аппликативного стиля. 3.4.2 Некоторые замечания. 4 Класс обучаемых Универсал: предъявление понятия Выразимость. 4.1 Программистский аспект. 4.2 Математический аспект. 4.2.1 Èíèöèàëüíàÿ àëãåáðà. 4.2.2 Óïîðÿäî÷åííî-ñîðòíûå òåîðèè. 4.3 Системологический аспект. 4.4 Элементы среды саморазвития. 5 Реализация задания практикума для аппликативного стиля. 5.1 Макеты задания. 5.2 Понятия. 6 Заключение. 7 Результаты работы. 8 Литература. 9 Приложения. А. Ранние требования к предметной области системы (до введения уровня спецификаций). 1 B. Несколько слов об энергичных и ленивых интерпретаторах. 2 C. SECD-машина. 3 D. Среда саморазвития для идеи интерпретации. 5 E. Бестиповое лямбда-исчисление. Определения. 15 F. Задание практикума. 16 1 Введение. выполнена в рамках проекта “Компьютерный комплекс обучения основам информатики” (грант 93 -01-01-047 РФФИ, научный руководитель проф. Трифонов Н. П., ответственный исполнитель н.с. Громыко В. И.) и соглашения о совместной научной работе между факультетами математики и информатики FSU-Jena (Prof. G. Wechsung), Германия и факультетом ВМК по теме “Учебные пособия и обучающие системы в области информатики” с консультационным участием Prof. M. Broy, Prof. A. Blaser и н.с. А. Г. Симакина (Институт психологии). 1.1. Позиция в отношении к предмету. Важно определиться в главном - оценить происходящие изменения в человеческом виде. Исходим из признания факта, что меняется подсознательный стиль мышления. Такие периоды сопровождаются активной деятельностью рационального в нашем мышлении. Конкретно, связываем изменения с развитием компьютерного дела, требующего от рационализма обрести ту же общность, которую давно демонстрирует гуманитарное знание. Естественно, что рационализм решает эту задачу на своем пути, выводя рациональное знание на более сложный уровень - синтезирующего научного знания . Этому определяюще способствует информатика, обеспечивающая существование общества в век систем, и являющаяся сензитивной деятельностью Человека как вида. Уже прошло много лет после того, когда “мы и в самом деле преуспели в преобразовании программирования в науку, причем замечательно простым способом - решив называть ее computer science (компьютерной наукой)” [2]. С тех пор она действительно обрела нужный статус. Но настало время, когда это ее свойство должно стать заметным и для будущего профессионала в информатике и для любого человека, уже существующего в условиях информационного общества. Поэтому та же проблема (синтезирующей науки), смещенная в область образования - синтезирующего знания с навыком созидания в программировании, явление актуальное: информационный рационализм должен стать составляющей нашего интеллекта. Каким бы банальным не показалось утверждение, повторим его еще раз - базовое обучение в информатике должно сосредоточиться на синтезирующих основах предмета в аспекте их роли для конструирования в программировании (созидания). К сожалению, образование, в силу консервативности, всегда обременено “культурной отсталостью”. К тому же усложнение средств информационного моделирования потворствует примитивной позитивистской интерпретации программирования как искусства и тем самым необязательности, ненадобности (зла) научного восприятия. Итак, во многом, изменению парадигмы в образовании - от унаследования к овладению знанием - мешает позитивистский миф об искусстве программирования. Плохо, что мифу неявно потворствуют такие авторитеты как Дональд Кнут (его трехтомник /74 г./ называется “Искусство программирования для ЭВМ”). Неявно, так как его понимание искусства в программировании правильно фиксирует внимание на созидающем аспекте в программировании, а также правильно выделяет научный характер такой деятельности. На этом основании следует лучше признать синтезирующий характер профессиональной деятельности в век систем, которая, в связи с программированием, наполнена конструирующей особенностью. Впрочем, обстоятельства сильнее нас, иногда трехтомник Кнута называют “Дело программирования”. В этой же связи обратим внимание на другой авторитет - Дэвида Гриса и его книгу “Наука программирования”, который, в конце концов, заявил /81 г./: ”Из-за нашего невежества мы потратили очень много времени на то, чтобы бить по воде, вместо того, чтобы плавать. Задним числом я могу сказать, что мне лучше всего было бы пройти хороший курс логики 10 лет назад”. Также надлежит обратиться к авторитету Эдсгера Дейкстра с его книгами “Краткое введение в искусство программирования” /71 г./ и затем “Дисциплина программирования” /76 г./. Он говорит: “... я чувствую себя сродни преподавателю композиции в консерватории. Он не учит своих подопечных тому, как следует писать конкретную симфонию, но он должен помочь им обрести собственный стиль и объяснить, что под этим подразумевается”. Но уже приходится считаться, что время требует в обучении большего - сосредоточиться на развитии творческих особенностей интеллекта. Таким образом, предыдущее обучение - “преподаватель композиции” становится только необходимой составной частью. Теперь нуждаемся в “преподавателе сочинительства”. Синтезирующей особенности созидающей деятельности человека подчинено Развивающее Обучение (РО) [3]. Оно особый упор делает на приобщение к теории предмета, развитие теоретического мышления, но посредством развития свойства теоретической самоорганизации интеллекта. Поэтому так своевременна позиция Дж. Р. Хиндли, которая хорошо ориентирует в отношении нашего предмета: ”Программисты-теоретики сталкиваются с теми же вопросами, над которыми логики (особенно принадлежащие к различным школам конструктивной математики) ломают голову уже около 80 лет. Например: что такое математическое мышление и как его формализовать? Поэтому, - если, конечно, логики не совсем сбились с пути, - их исследования могут служить, по крайней мере, полезным источником идей” [9]. Исходя из этого, для целей базового обучения, информатику следует воспринимать как математику, сосредоточенную на метаматематических вопросах предъявления знаний, связанных с пониманием его существенной зависимости, возможности от выбираемых языковых средств. Тогда фундаментальными вопросами становятся: возможности и границы аксиоматического описания (основных математических структур), а также возможности и границы эффективных методов, то есть алгоритмов. (Сравним с позицией Ю. Манина, выраженной в книгах “Доказуемое и недоказуемое”, “Вычислимое и невычислимое”). В этом ключе проблемную ориентированность языковых средств программирования следует воспринимать как определение (пользовательское) истинности для соответствующего стиля. На главную роль в обучении уже претендуют среда информационного моделирования также, как раньше, - учебные вычислительные машины или позже, языковые вычислители золотого фонда языков программирования. Таким образом, приходим к необходимости рассматривать в базовом обучении информатике современный аксиоматический метод. Он включает в себя язык, теории, определение истинности, представление моделей, разрешение или выводимость (в основном, в ракурсе конструктивных предъявлений). Возможность обучения на этой основе следует из зрелости предмета информатики, выраженной в существовании пользовательской семантики фундаментальных абстракций, а главное - в наличии ясных и разработанных ориентиров нового интеллектуального качества - {конструктивности (прагматическая деятельность), эффективности (профессиональная деятельность), выразимости (мировоззренческое восприятие)}, а также столь же ясных прагматических экстенсиональных обобщений средств информационной обработки - {исполнение, типизация, система, язык}. Возможность усвоения на младших курсах абстрактных (главных) ориентиров обучения во многом связана с конструктивным воплощением изучаемого в компьютере, что позволяет обеспечить необходимую практическую (осязаемую) деятельность обучаемого. Конкретизация РО для базового обучения информатике, которое выстраивается на прагматике предмета - программировании, проводится с учетом его современных проблем. На этом пути привлекательны конструктивностью позиции Н. Вирта и Ч. Э. Р. Хоара. Первый призывает осмысливать собственные информационные проблемы посредством моделирования подходящего языка программирования (послужной список созданных им языков впечатляет: Эйлер, Алгол-W, Паскаль, Модула, Модула-2, Оберон). Тем самым он фиксирует внимание на необходимости поднимать прагматические проблемы любой деятельности по конструированию в программировании до высот их обобщенного, абстрактного восприятия. Второй неоднократно демонстрировал конструктивную мощь взаимодополняющих семантик: реализаторской, пользовательской (проблемно-ориентированной) и авторской (выражающей “идеальную”, идейную суть предметной области). Состояние дела обучения уже предлагает нам удачные образцы синтезирующего предъявления семантик. Книга А. Филда, П. Харрисона “Функциональное программирование” (1988г., у нас 1993г.) решает проблему связного изложения семантик для функциональных языков. Конечно же, в новом не все получается с первой попытки. Например, не удалось в качестве авторской семантики предложить модели l-исчислений и комбинаторных алгебр. Но вопрос этот ставится и обсуждается на основании доверия к сообщенным математическим фактам. Приведем еще один пример новаторства - учебник (в четырех частях - »1200 страниц) “Информатика. Основополагающее введение” профессора М. Броя (M. Broy), лауреата премии Лейбница Германской академии наук за 1993г., одного из лидеров немецкой теоретической школы, преемника и ученика Ф. Л. Бауэра (F. L. Bauer). Учебник написан в 1992-1995 гг., у нас первая часть вышла в 1996 г. Он продолжает традицию концептуального взгляда на предмет, заложенную в известном учебнике Ф. Л. Бауэра и Д. Гооза (G. Goos) “Информатика” (в Германии были 3 переработанные издания книги, на русском языке был перевод со 2 издания в 1976г., с 3 издания 1984 года - в 1990г.). В первой части предлагается введение в информатику на основе аппликативной среды информационного моделирования. В остальных частях рассмотрены вопросы устройства современных базовых вычислителей, устройства языков программирования, эффективности вычислений. В целом, наша позиция исследования отличается от приведенных двумя моментами: ориентацией на привлечение к обучению разных сред информационного моделирования; еще большей концептуальностью (современный аксиоматический метод) в отношении предмета информатики, но и особой заботой о восприятии обучаемым предлагаемого (логика открытия). Так как наиболее реально выражены результаты происходящих изменений в предмете, то фиксирование сущности базового обучения информатике начнем с констатации позиции в отношении предъявления предмета: на уровне среды информационного моделирования связывание прагматики программирования с теорией предмета мы проводим на основании взаимодополняющих семантик в ракурсе современного аксиоматического метода. 1.2. Составляющие обучения. Практической целью работы является повышение эффективности базового обучения информатике за счет предоставления её теоретических образующих. Противоречие между наукоемкостью теоретических понятий и неподготовленностью обучаемого (студента-первокурсника) решается методом РО. Метод состоит в подключении творческих возможностей интеллекта обучаемого при овладении предметом и для его овладения. Общей целью обучения является развитие у обучаемого умения воспринимать, предъявлять и исследовать знания . Метод РО ориентирует на предъявление предметной области (ПО) как среды развития для логики открытия (ЛО) обучаемым предмета, то есть для его творческой деятельности по самостоятельному переоткрытию предмета, и на этом основании формированию универсального качества интеллекта - теоретической адаптивности. Общая цель конкретизируется посредством РО при её разработке в отношении базового обучения информатике. Этому служат: учет системологического подхода к развитию научной культуры от века машин к веку систем; восприятие информатики как дальнейшего развития математического механизма по своевременному приобщению нашего интеллекта к познающему научному разуму века машин и к созидающему разуму века систем; понимание предмета при базовом обучении широко, как симбиоза программирования, математики и информатики. Таким образом, конкретной целью обучения является приобщение обучаемого на предмете к интеллектуальному состоянию, которое свойственно системному аналитику. То есть комплекс должен обеспечить учащегося понятийными средствами об инструментах информационного моделирования для предъявления знания для его исследования, причем сократовским методом обучения (посредством логики открытия). Актуальность задачи диктуется возрастающим объемом профессиональных граней предмета, к тому же подверженных быстрым изменениям. РО старается привить способность ученику самостоятельно переоткрывать многое на основе последовательного усложнения его видения существенного. Здесь находятся истоки РО, которое озабочено теоретическим мышлением, формируемым посредством логики открытия (обучаемым предмета). Комплексный характер задачи приводит к комплексу обучения. В нем необходимы: * учебник , выстроенный традиционно на основе логики обоснования предмета, который послужит основой для курса лекций; но выбранные темы соответствуют цели - теоретическому кругозору; * компьютерный задачник - учебник , сформированный для логики открытия обучаемым предмета, который занят естественно обучением предмету, но старается использовать теоретическую самоорганизацию интеллекта обучаемого; * обучающая система для самостоятельной работы ученика, преследующая цель помочь ему в его творческой самоорганизации. * последней составляющей, обеспечивающей комплекс достаточностью в повышении эффективности базового обучения, является традиционная связь Учитель - Ученик ; учитель корректирует, контролирует ученика в их совместной работе по творческой деятельности ученика (субъект творчества) в его самообучении. Создание комплекса переводится в реальный план посредством моделей обучаемого, предметной области (ПО), обучения. * Модель обучаемого отражает интегральное видение состояния, перспективу предмета в его отношении к интеллектуальным качествам, в особенности, связанным с самоорганизацией. Поэтому моделирование творческой самоорганизации начинается с фиксирования наиболее общих интеллектуальных состояний на предмете - априорной модели обучаемого, а также подходящего образа конкретной деятельности в программировании. Выделенными состояниями являются три класса и две категории обучаемых, представленные на рис. 1. Часть уточнённой априорной модели обучаемого, относящейся к профессионалу, с точностью до аспектов представлена на второй части рисунка. Аналогично уточняются модели классов универсала и прагматика. Рис. 1: Модель обучаемого. Такой выбор трех классов ("прагматик", "профессионал", "универсал") следует из кантовского анализа научного познания (рассудочное, разумное), которое мы связываем с использованием, устройством и границами применения компьютера для предъявления знания для его исследования. При этом использование мы соотносим с рассудочной деятельностью, а устройство и границы связываем с разумным охватом предмета. Синтезирующий характер предъявления знания и необходимая для этого самоорганизация теоретического разума приводит к выделению категории "личность". Итак, из общей цели обучения и значения концептуального каркаса предмета следует требование - дать обучаемому возможность сбалансировано представить (приобщиться) инструменты информационного моделирования: их применение (прагматик), устройство (профессионал) и границы применения (универсал). Интегральное интеллектуальное состояние на предмете соответствует состоянию системного аналитика, охватывающего предмет от его возможности по предъявлению знания до реализации этого предъявления на компьютере. Выделение категории "начинающий" вызвано требованием метода РО о необходимости предъявлять ориентиры обучения посредством познавательной инверсии. Дело в том, что метод основан на фиксировании доминирующей роли культуры (филогенез мышления) в развитии мышления каждого человека (онтогенез). Поэтому требуется отыскивать доступное представление ориентиров в ПО и посредством их раннего предъявления обучаемому (с точки зрения их позднего появления в культуре) формировать в нем целеполагание для логики открытия. Доступность представления объясняется уточнением А. Северцова закона развития Г. Геккеля: филогенез есть последовательность проявленных онтогенезов. Для предъявления ориентиров посредством познавательной инверсии разрабатываются специальные среды саморазвития. Ядро учебного материала для каждого класса обучаемых готовится на основании пользовательской семантики. Семантической разработке подвергаются средства информационного моделирования, но рассматриваемые в их отношении к главному концептуальному ориентиру класса: для прагматика - к конструктивности, для профессионала - к эффективности, для универсала - к выразимости. Таким способом практика программирования “завязывается” с необходимой для РО теорией предмета. Естественно, что наиболее ёмкий ориентир для личности - это конструктивность. Так как “планкой” обучения является стиль среды информационного моделирования, то конструктивность разрабатывается широко. Во-первых, со стороны программирования она разрабатывается инвариантно относительно языков стиля - программистский аспект. Во-вторых, со стороны информатики привлекаются: математический аспект - спецификация, проясняющая реализацию, и системологический аспект - спецификация, проясняющая предъявление знания. Для классов профессионала и универсала применим тот же подход. Но, если сравнивать с прагматиком, то, вообще говоря, действуем уже, так как рассматриваются отдельные темы - эффективность и выразимость. Эффективность, в некотором роде, является продолжением прояснения вопросов реализации, но инвариантно относительно конкретных базовых вычислителей. Выразимость, в некотором роде, является продолжением рассмотрения вопросов предъявления знания, но инвариантно относительно “реальных” предметных областей, то есть с точностью до абстрагирования информатики. Итак, инвариантность выбранных ориентиров относительно стилей и сосредоточенность на базовом обучении позволяют и требуют действовать таким способом. * Модель ПО должна вобрать ядро с большой творческой потенцией понятий, которые хорошо увязаны с прагматикой предмета. Поэтому ядро формируется на основании сред информационного моделирования , воплощенных в прагматике предмета в стилях программирования (по исполнению, по типизации, по системам): императивном, аппликативном, функциональном, логическом, Пролог-стиле, объектно-ориентированном, бестиповом, с сильной типизацией, с АТД. ПО предъявляется в двух согласованных качествах - в виде компьютерного учебника-задачника и в виде традиционного учебника. Согласование проводится на основании принципа РО, который требует пристального внимания к прагматике предмета, отыскивая в ней элементарные составляющие, непосредственно связанные с идеями фундаментальных абстракций предмета. Элементарные составляющие для развитого предмета выбираются естественно на основании его вхождения в общую культуру предмета и системологического видения основной цели обучения. Главными ориентирами выбираются естественные темы для инструментов информационного моделирования: от программирования - исполнение, типизация, система, язык; их математические обобщения - модель, алгоритм (теория), программа (язык); их обобщения в информатике - конструктивность, эффективность, выразимость. Так как в нашем рассмотрении предъявление знания выбрано общей целью обучения, то кажется уже достаточно обоснованным, что нормой анализа выбирается стиль - класс языков, связанных проблемной ориентированностью. Наличие искусственно разработанных идей в математике позволяет создать среды саморазвития для начинающего по внедрению в его интеллектуальный актив главных ориентиров предмета на основании элементарных составляющих. Ориентиры облегчат ему целеполагание в среде развития - работе с компьютерным учебником-задачником и традиционным учебником для собственного переоткрытия предмета. Компьютерный учебник-задачник формируется на основании задания практикума, предназначенным для выполнения обучаемым. Сопутствующий заданию учебный материал соотносим с интеллектуальным состоянием, зафиксированным в модели обучения в виде класса прагматика. Для задания специально отыскиваются задачи, предоставляющие возможность предъявить разнообразие материала и не фальсифицировать предмет. Из этого следует необходимость их нетривиальности и межстилевого характера. Значит, задачи непосредственно должны быть связаны с особой ролью инструментов информационного моделирования - в нашем понимании, с предъявлением знания на компьютере. Поэтому задания, в первую очередь, обслуживают главные ориентиры обучения от программирования - исполнение, типизацию, системы, язык. Во-первых, общность обеспечивает единый взгляд на сравнение стилей; во-вторых, позволяет естественно развить ориентиры классов профессионала и универсала; Кроме того, наличествует разрыв между общностью главных ориентиров обучения и узостью элементарных составляющих с сопутствующими абстрактными представлениями в идеях, удается заполнить промежуточными формами, так называемыми наследуемыми ориентирами, обогащенными конструирующей ролью. Это позволяет учебный материал программистского аспекта прагматика наполнить теоретическим видением (понятиями). Наследуемыми ориентирами являются: структурное и доказательное (инвариант цикла) программирование, связанные с примитивностью "как делать" императивного стиля; смешанные вычисления нетипизированных аппликативных вычислителей, метод индукции, языковые расширения в направлении предъявления "что делать"; высокая верифицируемость комбинаторных вычислителей, алгебра программ, фиксирование "что делать"; для логического стиля много моментов - порождающее и вычисляющее программирование функций, управление для эффективного вывода, исчисление выше первого порядка, динамические расширения исчисления, фиксация исчислением "что делать". Важно, что наследуемые ориентиры через задание практикума существуют интегрально. Во-первых, это обеспечит активность обучаемого в творческом проявлении. Во-вторых, удержит разработчиков ПО от соблазна профессиональной ориентации учебного материала. Связность учебного материала организуется межстилевым характером задания, а также наличием связующих факторов для разных интеллектуальных состояний - классов. Эти связи показаны на рисунке 2. Error! Not a valid link. Например, задание практикума для темы Исполнение имеет следующий вид: написать программу, которая моделирует алгебраическую группу и позволяет решать уравнения вида E1*x*E2=A, где E1, E2, A - произвольные термы (выражения), x - неизвестное для заданных интерпретаций. Задание необходимо выполнить в нескольких стилях, например, в императивном, аппликативном и логическом. Дополнительные требования должны выявить иерархию в стилях с точки зрения предъявления знания. Во-первых, может быть требование об изменении типа группы добавлением новых законов. Во-вторых, может быть предложено использовать несколько интерпретаций заданной группы. Учебный материал разрабатывается при подготовке ответа и указаний для выполнения задания практикума. Ответ готовится в виде макетов-программ заданий. Среда саморазвития, учебные материалы для универсала и профессионала, выделение понятий спецификаций аспектов прагматика исследуются и предлагаются специально. Для прагматика выбор материала, во многом, определяется помощью, которую необходимо оказать обучаемому по выполнению задания, привлекая для этого теорию предмета. Именно, программистский аспект прагматика нагружается понятиями и задачами для уяснения необходимых для выполнения окрестностей ЯП. Посредством наследуемых ориентиров уровень требований к характеристике учебного материала повышается и достигает необходимых теоретических обобщений (понятий). Математический аспект прагматика обеспечивается учебным материалом, связанным с рассмотрением вопроса эффективной реализации. Системологический аспект прагматика обеспечивается учебным материалом, связанным с рассмотрением вопросов выразительных возможностей проблемной ориентированности стиля. Для профессионала сосредотачиваемся на вопросах эффективности алгоритмов для компьютерных вычислителей. Для универсала сосредотачиваемся на возможности предъявления знания, которая в информатике обеспечивается современным аксиоматическим методом, то есть адаптацией теории моделей к компьютеру. Учебник строится традиционно, но также с учетом общей и конкретной целей обучения. Для этого симбиоз математики, программирования и информатики предлагается рассматривать в виде, представленном на рисунке 3: Рис. 3: Модель Предметной Области в учебнике. В целом предметы понимаются: математика - формирующая деятельность (и, прежде всего, в отношении интеллекта) по образованию рационального единства из многообразия представлений; программирование - часть информатики, нацеленная на конструктивное предъявление знания на основе алгоритмического аспекта математики. Информатика - системологическая деятельность по конструктивному предъявлению неалгоритмического (эвристического) знания. Тогда общая структура учебника имеет иерархию тем, естественную для программирования, и иерархическую организацию внутри тем: математический уровень начального осмысления; программистское толкование рассматриваемого за счет расширений проблемной ориентированности стилей; информационный уровень, замыкающий рассматриваемое со стороны современной математики, решающей проблему предъявления знания на уровне конструктивности, эффективности, выразимости современного аксиоматического метода. Темы учебника естественны: это средства упаковки и распаковки знания посредством исполнения, данных, систем и в целом языка. Что касается изложения материала, то оно строится традиционно на логике обоснования предмета. Подчеркнем, что структура учебника выбрана в соответствии с логикой открытия, то есть учитывает прагматику предмета (выбор тем), но внутренняя иерархия каждой из них соответствует общей цели обучения. Необходимость традиционной организации учебника вызвана пониманием, что логика открытия не исключает рационального метода, а выводит его на более высокий уровень. Сосредоточенность на базовом обучении проявляется в объединяющем прагматическом начале, которым является понятие - среда информационного моделирования. Это позволяет отследить сложность выбираемых абстракций. Только реальное предъявление материала в компьютерном варианте является признанием (фильтром) его подходящей приспособленности (наличествует пользовательская семантика) для восприятия, а тем самым возможному его включению в учебник. Таким объединяющим началом служат две известные (крылатые слова) парадигмы -от программирования: Алгоритмы + Структуры данных = Программа; от информатики: Универсальная алгебра + Логика = Теория моделей É АТД. В парадигмах заметны изменения в прагматике предмета: от “как делать” к “что делать”, причем с большим вниманием к тому “как это делается”. * Модель обучения должна вобрать принципы РО - приготовить предмет для переоткрытия фундаментальных абстракций на основе сократовского способа обучения (познавательная инверсия). Основой модели являются: нацеленность на самостоятельную деятельность обучаемого - нетривиальные, но классические задачи, предъявляемые в заданиях практикума; независимость от педагогических установок - объективность подготовки материала (окрестности понятий, задач); обеспечение логики открытия - среды саморазвития начинающего; невосприятие как противоречия порочных логических кругов - их разрешение проводится посредством примеров; предъявление реальной связи теории и практики - посредством уровня спецификации практического материала по программированию, нацеленного на облегчение созидания в программировании; обеспечение разнообразных связей предмета - посредством проектирования на классы обучаемых составляющих современного аксиоматического метода. Основой среды развития обучаемого является компьютерный учебник-задачник, формируемый для логики открытия, которая не зависит от конкретной предметной области, так как строится на интеллектуальных проявлениях - индукции, аналогии, наблюдении, эксперименте, гипотезе, обобщении. Она всеобща - как всеобщи перечисленные формы, используемые творческим человеком. РО нацелено на общие задачи теоретической самоорганизации интеллекта и служит логике открытия, что позволяет утвердиться в следующих ответах на ключевые вопросы базового обучения информатике: Зачем учить? - обеспечить состояние познающего интеллекта уровня воспроизводства научного знания; Кого учить? - творческую личность системно-информационного периода науки, продвигающуюся в состояние созидающего интеллекта; Чему учить? - информационному моделированию по предъявлению знания для исследования; Как учить? - тренажируя теоретическую адаптивность интеллекта. Модель обучения реально представляется системой обучения FLINT [4]. Архитектура, функциональная схема системы, база знаний подчинены функции помощи обучаемому по переоткрытию основ предмета. Этому служат блоки системы, работающие на основе эвристик, которые должны способствовать - логике открытия, теоретическому мышлению, раннему целеполаганию на основе познавательной инверсии. Адаптивность системы к обучаемому достигается посредством его динамической модели. Зафиксируем сущность предлагаемой позиции в отношении к составляющим обучения: обучается системный аналитик средам информационного моделирования (для предъявления знания) посредством среды (само)развития для логики открытия обучаемым предмета (сократовское обучение). 2 Постановка задачи: о связном предъявлении теории информатики и практики программирования в теме ИСПОЛНЕНИЯ для теоретического мышления. Связность предъявления материала, прежде всего, решается на уровне естественного согласования практики и теории предмета. Этому служит дополняющее совместное представление о тенденциях развития предметов программирования и информатики в лоне математики [4]. Имеются в виду следующие цепочки развития: * программирования: базовый вычислитель - исполнение - типизация - банки данных - системы - банки знаний - экспертные системы; * информатики (как развития математики): конкретная математика - аксиоматическая математика - теория моделей - конструктивная математика - дискретная математика - современный аксиоматический метод - самоорганизующиеся системы. Для нас важной является граничная точка (системы), непосредственно касающаяся конструирования в программировании. Вспомним Ч. Э. Р. Хоара [5]: “... разработка программы и разработка ее спецификации должны проводиться параллельно одним и тем же лицом, и должно существовать взаимодействие между этими этапами работы. Недостаточная ясность спецификации является важнейшим признаком недостатков в программе, которую она описывает, и эти две ошибки должны устраняться одновременно, до того, как приступают к проекту”. /*к реализации */ Итак, есть средство программирования, которое воспринимается * уровень-1 - через пользовательскую семантику проблемной ориентированности, то есть через уровень знания средства в конкретных языках программирования стиля; Также оно рассматривается в более общем статусе информационного моделирования: * уровень-2 - через абстрактную семантику стиля, то есть через уровень знания его в подходящем языке спецификации, причем, по возможности, в трех ракурсах: с упором на пользовательскую позицию; с упором на суженную семантику реализаторской позиции (с точностью до компьютера); с упором на обобщенную семантику авторской позиции (с точностью до предъявления знания). Поэтому выбранная тема ИСПОЛНЕНИЕ (и другие) разрешается: при разработке программистского материала в рамках среды информационного моделирования; через языки программирования, но как представителей стилей : императивного, аппликативного, логического, объектно-ориентированного, параллельного. Кроме того, различие специфицирующих подходов разных стилей (из-за их проблемной ориентированности) также нуждаются в согласовании. Этому служит современный аксиоматический метод, который мы рассматриваем как синтезирующий подход в общей проблеме предъявления знаний. Через него удается рассмотреть с единых позиций: * во-первых, проблемно-ориентированные спецификации стилей; * во-вторых, рассматриваемые темы для разных классов обучаемых (для прагматика - конструктивное предъявление знаний, для профессионала - добавить к конструктивному предъявлению необходимую эффективность , для универсала - выразительные возможности общих средств предъявления знания); * в-третьих, выделенные идеи проблемно-ориентированных стилей для создания сред саморазвития начинающего . Соберем воедино предложенную сигнатуру метапонятий обучения в ключе проблем РО. При разработке учебного материала несколько моментов являются решающими для успеха проекта - по подключению творческих возможностей обучаемого (логики открытия) для переоткрытия предмета. Во-первых, исходя из роли информатики для обеспечения нового интеллектуального качества информационного моделирования выделяем главные ориентиры обучения : исполнение, типизация, системы, язык, модель, теория, программа, конструктивность, эффективность, выразимость, стиль. Но, что еще важнее, необходима связующая позиция рассматриваемых ориентиров. Такой мы выбираем современный аксиоматический метод . Это он превратил в успех утерянную определенность математики (вспомним М. Клайна и его книгу “Математика - утрата определенности”), повысив точность и всеобщность теорий с обязательным предъявлением языка и формализацией истинности (вспомним опять же М. Клайна с его книгой “Математика - поиск истины”). Во-вторых, следует обеспечить прагматический полигон, на котором могут быть представлены и обсуждены избранные “высокие” темы. Поэтому в основу кладется задание практикума, то есть нетривиальные, классические задачи программирования. С другой стороны, так как наше требование - предъявить задания в разных стилях программирования, то это поднимает уровень их обсуждения до необходимых РО вопросов. Напомним, что в некотором роде материал для системы обучения готовится таким образом, чтобы помочь обучаемому выполнить задание практикума. В-третьих, необходимо тесно связать теоретический материал с прагматическим материалом программирования, так как в нем максимально проявляется созидание. Этому служит взаимосвязанная проработка взаимодополняющих реализаторской, пользовательской и авторской семантик на уровне стилей. То есть специально прорабатываются стили в ключе трех собирательных ориентиров обучения - базовый вычислитель (реализующий), языковой вычислитель (проблемно-ориентированный), теоретический вычислитель (ориентированный на метатеорию, то есть фиксирующий границы вычислителя в аспекте предъявления знания). В этой связи на задачи по программированию накладывается требование - наличие их теоретической спецификации. Что касается понятий, то они также должны быть обеспечены, по возможности, разноуровневой семантикой. В-четвертых, так как для логики открытия необходимо предъявить видение (целеполагание ), то обеспечивается познавательная инверсия в отношении ключевых аспектов (идей) теоретических вычислителей для начинающего. Этому служат Среды Саморазвития по идеям и их интегральному предъявлению. Это интегральное видение для предъявления идей обеспечивается через общую позицию - современный аксиоматический метод. Конечно же, здесь явно фиксируется нижняя граница требований к обучаемому - посредством выбранных элементарных составляющих, на которых, во многом, разворачивается обучение. В-пятых, необходимо всегда иметь в виду наследуемые от главных ориентиры, которые выделены в предмете на основе его прагматического развития. Они могут послужить следующим уровнем элементарных составляющих для части обучаемых, продвинутых в прагматике предмета. Поэтому же они являются хорошим ориентиром для практических целей обучения. В-шестых, для каждого класса обучаемых свой мотив предмета: эффективность для профессионала, выразимость для универсала, конструктивность для прагматика. Эти главные грани разрабатываются в соответствии с перечисленными выше пятью требованиями. Актуальным в дальнейшем продвижении комплекса обучения является установление плодотворной связи теории информатики с практикой программирования на основании синтезирующего характера современного аксиоматического метода в отношении предъявления знания. Поэтому теоретическую часть диплома составляют две задачи: · выявить ключевые понятия аппликативного стиля по теме ИСПОЛНЕНИЕ для трех уровней спецификаций, относящихся к классу обучаемых Прагматик; · выявить ключевые понятия для Класса обучаемых Универсал по вопросу ВЫРАЗИМОСТИ для организации среды саморазвития категории начинающего. Практическая часть диплома нацелена на обеспечение обучающей системы FLINT материалом для компьютерного учебника-задачника: · реализовать задание практикума для аппликативного стиля с предъявлением спецификаций на основании теоретической части диплома (задача 1). 3 Аппликативный стиль. Денотационная семантика. (класс Прагматика). В пункте 1.1 было декларировано, что связывание прагматики программирования с теорией информатики мы проводим на основании взаимодополняющих семантик в ракурсе современного аксиоматического метода. В пункте 1.2. была представлена походящая модель ПО в компьютерном учебнике-задачнике и были зафиксированы опорные моменты, которые обеспечат нужную связь. Цель этого пункта - показать, насколько близка прагматическая сторона предмета к его теоретическим основам, насколько легче её восприятие через теорию предмета. Поэтому здесь проводится анализ стиля по определенным в пункте 2 требованиям. 3.1 Проблемная ориентированность (программистский аспект). Как отмечалось в пункте 2 выявлению связи теоретического материала с прагматическим служит подход по разработке учебного материала на основании общих принципов, выраженных в следующих понятиях: главные ориентиры обучения, идеи, наследуемые ориентиры обучения, среда информационного моделирования, современный аксиоматический метод, взаимодополняющие семантики, системный аналитик. Применим подход к аппликативному стилю, чтобы выделить ключевые понятия, которые необходимо будет предъявить в учебнике-задачнике. В первую очередь исследуем общее в проблемной ориентированности конкретных языков стиля. Вспомним, что идеей среды саморазвития аппликативного стиля является функция, а наследуемыми ориентирами - смешанные вычисления, комбинаторные вычисления, языковые расширения в направлении приближения свойств стиля к выражению в нем “что делать”. 3.1.1 Сравнение языков программирования стиля. Во всех языках функционального программирования способы описания функций базируются на тех или иных формализмах, созданных в математической логике: лямбда-исчислении (Лисп), комбинаторной логике (Миранда), нормальных алгоритмах Маркова (Рефал), рекурсивных уравнениях Эрбрана-Гёделя (KRC). В более современных языках, таких, как Миранда, используются и некоторые другие достижения математики, например, теоретико-множественная нотация. В чистых языках функционального программирования обычно имеется одна главная операция - применение функции к аргументу, или аппликация, из-за чего их часто называют аппликативными . Прозрачная математическая семантика этой операции позволила Д. Тернеру (автору Миранды) говорить о ”семантической элегантности” аппликативных языков (см. пункт 3.4). Не случайно поэтому процесс написания программ на этих языках в чем-то сродни математической деятельности. Обсуждение самих этих языков позволяет легко перейти на теорию предмета, тогда возникает связь теории и практики, необходимая для целей РО. Для рассмотрения выберем следующие языки: Норе, Миранда, Лисп и FP. Проблемная ориентированность языков определяется функционалами или функциями высшего порядка. Концепция функций высшего порядка возникает из идеи о том, что функции должны иметь тот же статус, что и любой объект данных, так чтобы они сами могли быть входными и выходными данными других функций. Так, например, в Норе, как и в большинстве функциональных языков, не существует ограничений на количество и сложность подобных функций. Однако в языке FP нет средств для определения пользователем функций высшего порядка. Вместо этого язык обеспечен небольшим набором встроенных функций высшего порядка, которые рассматриваются как программно-встроенные блоки. В языке Миранда осуществлен совершенно иной подход к функциям высшего порядка: там нет механизма для явного определения лямбда-выражения, функциональные объекты в нем генерируются частичным применением существующих функций. Язык Норе. Рассмотрим следующие функции языка Норе: IncList - увеличивает на 1 каждый элемент списка (функция определяется на родовом (полиморфном) типе данных). dec IncList : list(num)®list(num); ---IncList(nil)<=nil; ---IncList(x::l)<=(x+1)::IncList(l); имеется возможность сопоставления с образцом (::) MakeStr - отображает каждый элемент списка в список из одного элемента. dec MakeStr : list(char)®list(list(char)); ---MakeStr(nil)<=nil; ---MakeStr(c::l)<=[c]::MakeStr(l); Говорят, что “тип рекурсии” в обоих случаях одинаков. В обоих вышеприведенных примерах определенная функция применяется к каждому элементу заданного списка. В первом случае она имеет следующее определяющее уравнение: ---Inc(n)<=n+1; во втором - ---Listify(c)<=[c]; (c соответствующими определениями типа). Можно выявить общую структуру, определив функцию высшего порядка, которая используя функции типа Listify и Inc в качестве аргумента, применяет их к каждому элементу заданного списка, выступающему в роли второго аргумента. Подобная функция высшего порядка широко используется и часто называется map. Поскольку мы не знаем наперед тип применяемой функции или тип обрабатываемых элементов списка, то map должна быть объявлена полиморфной функцией (alpha - динамическое определение типа для функций, beta - для элементов списка). Итак, dec map : (alpha®beta)#list(alpha)®list(beta); функция от одной двойки аргументов (кортеж). ---map(f, nil)<=nil; ---IncList(F, x::l)<=f(x)::map(f, l); Теперь, используя map и вспомогательные функции Inc и Listify можно выразить IncList и MakeStr: IncList(L) @ map(Inc, L) MakeStr(L) @ map(Listify, L). Удобство такого подхода очевидно, однако явное определение подобных функций может быть довольно неудобным. Язык Норе дает нам возможность записывать выражения (лямбда-выражения), значением которого является функция. Например, Inc будет описана так: lambda x=>x+1. Тогда IncList(L) @ map(lambda x=>x+1, L). Язык Миранда. Общий подход, принятый в языке Миранда, очень похож на подход языка Норе. но значительно отличается от него подходом к рассмотрению функций. Миранда - это строго типизированный язык высокого уровня, поддерживающий типы данных пользователя и полиморфизм, но он значительно отличается от Норе подходом к рассмотрению функций. Главное отличие в том, что Миранда - ”карринговый” язык, то есть в нем объекты, значениями которых является функция, строятся путем частичного применения существующих функций, а не с помощью явных лямбда-выражений, как это делается в Норе. Каждая функция в языке Миранда является по существу функцией высшего порядка. Когда мы на этом языке записываем определение вида f x y z = ¼ мы можем обычным образом интерпретировать f как функцию от трех аргументов x, y, z или, как в Норе, в качестве функции от одной тройки аргументов (кортеж). Однако в языке Миранда в действительности f является функцией высшего порядка только от одного аргумента x. Результатом применения f к аргументу E1 , который мы запишем в виде fE1 , является другая функция, снова только от одного аргумента y. Применение этой функции к следующему аргументу E2 снова дает функцию от оного аргумента z. Полное применение f записывается в виде fE1 E2 E3 . Итак, мы пришли к понятию карринг . Карринг - обработка функций от n аргументов как конкатенации n функций от одного аргумента. Посмотрим, как будет выглядеть функция Inc прибавления единицы к некоторому целому. На языке Миранда она может быть записана в виде частичного применения примитивной функции + к аргументу 1: (+) 1 (скобки превращают инфиксную функцию + в префиксную). Рассмотрим функцию map. Она имеет следующее определение на языке Миранда: map f []=[] map f (x : l)=(f x) : (map f l) Тогда выражение map((+) 1) L увеличивает на единицу каждый элемент списка L. В языке Миранда все функции должны иметь имена. В языке Норе мы вводим вложенные функции, используя lambda -выражения, в Миранде это достигается с помощью определения функции внутри where -выражения. Например, функция map(f 5) L where f x y=y+x*x прибавляет 25 к каждому элементу L. Заметим, что введенная функция может быть рекурсивной благодаря тому, что имеет имя. Заметим также, что нет необходимости в том, чтобы все функции были карринговыми, поскольку Миранда предоставляет также механизм для построения кортежей и для декомпозиции этих кортежей с помощью сопоставления с образцом. Язык Лисп. Лисп является нетипизированным языком обработки списков, в котором программы и данные имеют одинаковое представление. В языке Норе мы можем непосредственно записать обозначающее функцию выражение с помощью лямбда-выражения. В Лиспе существует идентичный механизм, только функция вводится с помощью специального атома LAMBDA, а не с помощью ключевого слова (lambda ), как в Норе. Например, функция, увеличивающая на единицу заданное значение x: (LAMBDA (x) (ADD x (QUOTE 1))). Используя QUOTE и LAMBDA совместно, мы можем передавать функции (лямбда-выражения) как параметры другим функциям. Рассмотрим применение map, где в качестве функции f используется функция, увеличивающая свой аргумент на единицу. Для того, чтобы эту функцию можно было передать в качестве параметра, определяющее ее лямбда-выражение заключается в кавычки. Опишем map: (defun map (lambda (f L) (cond ((eq L nil) nil) (t (cons (f (car L)) (map f (cdr L))) ) )) Тогда увеличение каждого элемента списка (1 2 3) на единицу можно описать так: (map (QUOTE (LAMBDA (x) (ADD x (QUOTE 1)))) (QUOTE (1 2 3)) ). Хочется отметить преимущества бестиповости лямбда-исчисления (и Лиспа также, так как он основан на этой теории). Продемонстрируем это на примере, показывающем, что аргумент одной и той же функции может выступать в роли как функции, так и данного (в нашем случае целого числа). Здесь также используется карринговость l-исчисления. Рассмотрим функционал Ф2 = lf. lx. f (f x) композиции функции. Так, применение этого функционала к функции g и числу 3 дает нам Ф2 g 3 ® g(g 3). Посмотрим вычисление выражения (Ф2 Ф2 ) g 3. (Ф2 Ф2 ) g 3 ® (lx. Ф2 (Ф2 x) g 3 ® Ф2 (Ф2 g) 3. Далее вычисления могут идти двумя путями. Могут использоваться ленивые вычисления (вычисления параметров откладывается до их использования) или энергичные вычисления (сначала вычисляются все параметры, затем только - применение функции). Итак, при ленивых вычислениях: ® (Ф2 g) (Ф2 g 3) ® ( l x. g (g x)) (g (g 3)) ® (g (g (g (g 3)))) = g4 3; при энергичных: ® Ф2 (lx. g (g x)) 3 ® (lx. g2 (g2 x)) 3 = g4 3. Первоначально при описании функционала предполагалось применение его к двум аргументам: функции и объекту. Но при вычислениях в качестве x выступает также функция g . Бестиповость языка позволяет нам сделать это. Отметим, что все объекты Лиспа - это S-выражения. Более того, программа на Лиспе сама является S-выражением, то есть не существует явных ключевых слов. Это приводит к одинаковому представлению программ и данных. Язык FP. Во всех языках, рассмотренных выше, определение функции дает имена объектам, передаваемым этой функции, и описывает затем, что делать с этими переданными аргументами. Поначалу этот подход кажется самым простым для понимания: определение функций принимает вид набора уравнений. Однако одной из наиболее сильных сторон функциональных языков является то, что они поддаются формальным преобразованиям. Одной из форм преобразования - “заменить равное равным”. В языке FP каждая функция выражается именно таким образом. Отличительной особенностью FP является то, что в нем нельзя выражать функции высшего порядка, определенные пользователем. Все функции высшего порядка являются встроенными - это комбинирующие формы “применить-ко-всем”, левая вставка и правая вставка. Так, в FP существует аналог функции map, работающей со списками: a f обозначает функцию, которая применяет f к каждому элементу в заданной последовательности аргументов. (a f) : <x1 ,¼,xn >=<f : x1 ,¼, f : xn > Например, a tl применяет функция выделения хвоста последовательности к заданной последовательности последовательностей (tl - примитив языка): (a tl) : <<1 2 3>,<4 5 6>>=<tl : <1 2 3>, tl : <4 5 6>>=<<2 3><5 6>>. Функционалы правая и левая вставка определяются следующим образом: (/f) : <x> = x базовый случай (/f) : <x1 ,¼,xn > = f : <x1 , /f : <x2 ,¼,xn >> - правая и (\f) : <x> = x базовый случай (\f) : <x1 ,¼,xn > = f : <\f : <x1 ,¼,x-1 >, xn > - левая. Существуют также варианты вставок, имеющие связанные с ними базовые случаи. Они указываются индексами у символов \ и /. С помощью этих встроенных функционалов мы можем записать нерекурсивный вариант такой функции как n!. Мы увидим, как FP хорошо иллюстрирует мощность функциональной нотации, и в особенности выразительную силу функций высшего порядка. Рекурсивный вариант: def fac = eq 0®1; *·[id, fac·(-·[id, 1])] где · - композиция функций, id - тождественная функция (id : x = x), 1 - константа 1, [] - “конструкция”: [f1 ,¼,fn ] : x = <f1 : x,¼,fn : x>. Заметим, что в этом определении нет ссылок на объекты, и поэтому нет символов применения функции. Тело состоит целиком из функций и функционалов. При применении fac к конкретному числу выражения становятся более привычным: fac : 3 º eq 0 : 3 ® 1; * : <3, fac : (- : <3, 1>)> = * : <3, fac : (- : <3, 1>)>. Нерекурсивный эквивалент: def fac = /1 * · i, где /1 - функция вставки (со значением в базовом случае, равном 1), i - примитив, при применении к n этот генератор дает последовательность целых от 1 до n. Тогда fac : 3 = /1 * : <1, 2, 3> = * : <1, /1 * : <2, 3>> = = * : <1, * : <2, </1 * : 3>>> = * : <1, * : <2, * : <1, 3>>>> = = * : <1, * : <2, 3>>> = * : <1, 6> = 6. 3.1.2 Неподвижная точка как подходящее обобщение проблемной ориентированности. Термин "неподвижная точка" встречается в различных разделах математики: в теории рекурсивных функций и алгоритмов, теории множеств, логике, теории автоматов, математическом анализе. Главный теоретический инструмент, использующий данное понятие - это теорема о неподвижной точке (или "теорема Клини"). В языках программирования высокого уровня необходимо иметь возможность записывать определение рекурсивных функций. Мы можем это сделать, так как имеем возможность дать имя любой функции f , а затем ссылаться на это имя где угодно в программе (при определённых ограничениях, обусловленных языком), даже в теле функции, названной этим именем, например, f(f(x)). Однако в l-исчислении функции не имеют имён. Они представляются l-выражениями (впрочем, это единственный объект l-теории). Поэтому для представления рекурсии необходимо придумать какой-то метод, который позволит функциям вызывать себя не по имени, а каким-то другим образом. Этим способом может быть механизм копирования аппликаций: то есть вид l-выражения остаётся неизменным, а рекурсия будет осуществляться уже при выполнении, посредством копирования тела функции. Для этого и используется неподвижная точка. · Неподвижная точка в лямбда-теории. Перейдём непосредственно к решению проблемы рекурсии в l-исчислении. Для этого представим рекурсивную функцию как функцию, имеющую себя в качестве аргумента. Таким образом, она будет содержать в своём теле ссылки на себя. Рассмотрим данный метод на примере функции факториал: Обобщим выражение E(F) посредством l-абстракции l f. l x. (x=0 | 1 | * x (f (- x 1))) . Обозначим эту абстракцию через G. Возникает уравнение для оператора G: z=Gy. Чтобы смоделировать рекурсию, необходимо иметь оператор Y со следующим свойством YG = G(YG) = l x. (x=0 | 1 | * x (YG (x-1))) . Тогда оператор Y для операторного уравнения z=Gy отыскивает неподвижную точку YG = G(YG) . Тогда рекурсивная функция F с телом Е(F) записывается в l-исчислении в виде: Y ( l F. E(F)). Осталось определить оператор неподвижной точки Y . Нам необходимо записать Y в виде l-выражения, так как чистое l-исчисление не имеет встроенных функций. Вид Y встречается при доказательстве теоремы о неподвижной точке в l-исчислении: Теорема . " f $ x (f x = x). Доказательство: Возьмём w = l x. f(xx). Тогда искомым x является ww. Проверим утверждение теоремы: x = ww= (l x.f(xx)) w=f(ww)=f x. ■ Как видно из доказательства оператором Y является: Y = l h. ( l x. h(xx))( l x. h(xx)). Убедимся, что именно это выражение и есть оператор неподвижной точки Y. Применим его к произвольной функции f : Y f = ( l h. ( l x. h(xx))( l x. h(xx))) f = = (l x.f(x x)) (l x.f(x x)) = f ( (l x.f(x x)) (l x.f(x x))) = f (Yf) Однако данный способ работает только в случае использования так называемого ленивого вычислителя, который “не делает ничего, пока это не потребуется“. В терминах традиционного программирования ленивое вычисление можно соотнести с вызовом по необходимости, в котором все аргументы передаются функции в невычисленном виде и вычисляются только тогда, когда в них возникает необходимость внутри тела функции. Если же использовать аппликативный порядок вычислений или энергичный вычислитель, который соответствует вызову функции по значению (при применении функции к аргументу последний сначала вычисляется, а затем уже передается функции) то самоприменение приводит к зацикливанию: Y f ® f(Y f) ® f(f(Y f)) ® ¼ Однако можно модифицировать определение Y так, чтобы обойти эту проблему, определив альтернативный Y -комбинатор как: Y1 = l h. ( l x. h( l y. xxy))( l x. h( l y. xxy)) Y и Y1 h-эквивалентны, поскольку один можно получить из другого с помощью h-преобразования (ly. xxy =h xx[1] ) . Если теперь вместо Y использовать Y1 , самоприменение вычисляется, только когда оно применяется к аргументу, соответствующему переменной y , например, к целому аргументу функции факториал F . Пример энергичного(по значению) вычисления F= l f. l x. (x=0|1| * x(f(- x 1))). Y1 F 3 ® ( l x. F ( l y. xxy))( l x. F ( l y. xxy)) 3 ® ® F ( l z. ( l x. F ( l y. xxy))( l x. F ( l y. xxy)) z ) 3 ® ® ( * 3 (( l z. ( l x. F ( l y. xxy))( l x. F ( l y. xxy)) z ) 2)) ® ® ( * 3 (( l x. F ( l y. xxy))( l x. F ( l y. xxy)) 2)) ® /* ( * 3 (Y1 F 2)) */ ® ¼ ® ( * 3 ( * 2 ( * 1 ( l x. F ( l y. xxy))( l x. F ( l y. xxy)) 0))) ® ® ( * 3 ( * 2 ( * 1 1))) ® 6. Так как w1 w1 0 ® F ( l y. w1 w1 y) 0 ® 1 , где w1 =( l x. F ( l y. xxy)). Таким образом, с помощью комбинаторов механизм рекурсии заменяется механизмом подстановки и эквивалентных преобразований. Реализовать комбинатор Y можно двумя способами: в виде лямбда-выражения или, если все лямбда-выражения представлены в графовой форме, Y просто реализуется установкой циклического указателя (см. п. редукционные реализации). · Теорема о неподвижной точке Частично упорядоченное множество называется полной структурой , если всякое его непустое подмножество имеет как точную верхнюю, так и точную нижнюю грань. Обозначим посредством ^ наименьший элемент. Определение: Точка f называется неподвижной (фиксированной) точкой функции (функционала) j , если j (f)=f. Такая точка называется наименьшей, если " е : j (e)=e => f £ e (где £ - отношение порядка (возможно частичного) на множестве определения j ). Рассмотрим класс функций, имеющих фиксированные точки, и укажем способ нахождения наименьшей. Возьмём j: P ® P - монотонное отображение на полной структуре P . Применим j к произвольному элементу a из P . К результату снова применим j и так далее. Вследствие полноты P будет существовать точная верхняя грань последовательности. Если полученная последовательность значений будет монотонной, то её и стоит подозревать на неподвижность, т.е. supk { j (a)} = a ? Следовательно, Теорема о неподвижной точке. Если j - монотонное отображение полной структуры P в себя, то j ( а ) = а для некоторого а Î P . Доказательство: Рассмотрим множество Х = {х | j( x) ³ х , x Î P}. Минимальный элемент ^ (основание) существует в силу полноты Р и ^Î Х , таким образом множество Х не пусто. Следовательно, существует а = sup Х . При этом для любого x Î Х, так как а ³ х и j - монотонно, то j( а ) ³ j ( х ) ³ х, следовательно j ( а ) ³ а . Аналогично, т.к. j - монотонно, то j(j( а )) ³ j ( а ), что влечет j( а ) Î Х и, значит, а ³ j ( а ), так как а = sup Х. Таким образом, а ³ j ( а ) ³ a => а = j ( а ). ■ Рекурсию можно воспринимать двояко: индуктивно и через решение функционального уравнения. Эти толкования рекурсии совпадают при определенных условиях на функционал. Монотонный функционал j называется (цепочно ) непрерывным , если для монотонно возрастающей последовательности x0 =^ и xi+1 =j(xi )=ji (^) справедливо: suр{j[xi ]: iÎN}=j[suр{xi : iÎN}]. Теорема о совпадении наименьшей неподвижной точки с супремумом цепочки. Если j непрерывен, то Yj совпадает с супремумом цепочки {xi : iÎN} (x0 =^, xi+1 =j(xi )). Доказательство: Из непрерывности j следует, что супремум цепочки является неподвижной точкой для j: j[suр{xi : iÎN}]=suр{j[xi ]: iÎN}=suр{xi+1 : iÎN}=suр{xi : iÎN}. Осталось доказать, что точка b=sup{xi : iÎN} будет наименьшей неподвижной точкой (по индукции). Предположим, что a - также фиксированная точка j. Докажем, что b £ х . В базовом случае ^ £ a, так как ^ - основание (минимальный элемент). Предположим, что jk (^) £ a, тогда jk+1 (^) £ j( a ) = a, так как j - монотонно, а a - фиксированная точка по предположению. Так как a ³ jk (^) для любого k, то х является верхней границей монотонной последовательности. По определению наименьшей верхней границы и b £ a . · Применение теоремы в программировании. Надо позаботиться о простоте восприятия монотонности и непрерывности оператора j при толковании рекурсивных объектов посредством теоретико-множественного решения подходящего уравнения. Во многих случаях подходит плоский (дискретный) порядок. Введем порядок на произвольных элементах: x£y, если (x=^)Ú(x=y). Например, для N мы, тем самым, определили дискретную решетку: Она является полной. Рекурсивные функции могут трактоваться как решения функциональных уравнений. Рассмотрим для простоты f: N®N. Индуцируем порядок на функциях на основании плоского порядка на N. f £ g Û Df " x [f(x) £ g(x)]. Таким образом, f£g, если g является продолжением (расширением) функции f (то есть на области определения f эти функции совпадают, и g может быть “шире”). В каком-то смысле g уточняет функцию f. В таблице изображены примеры функций, находящихся в таком порядке. Эти функции монотонны по определению порядка. F0 F1 F2 F3 ¼ F ¥ T ^ Т T T ¼ T 0 ^ 0 0 0 ¼ 0 1 ^ ^ 1 1 ¼ 1 2 ^ ^ 4 4 ¼ 4 ¼ N ^ ^ ^ ^ ¼ N2 ^ ^ ^ ^ ^ ¼ ^ Пример (индуктивное толкование рекурсивного соглашения о функции факториала). Рассматривается рекурсивное объявление fсt fас = (nаt х)nаt : if х 0 then 1 else х*fас(х-1) fi , при этом получают следующий функционал j: В соответствии с нашим определением справедливо для хÎN^ , i=0,1,¼: fас 0 (х)=^, т.е. fас 0 =W. Тем самым для функции fас i получается не рекурсивное равенство: Это можно доказать индукцией по iÎN, i=0,1,¼: (1) i=0, тогда утверждение тривиально. (2) Пусть утверждение правильно для fас i fас i+1 (х)=t[fасi ](х)=  Пример (наименьшая неподвижная точка для функционала функции факториала). Функция fас: N^ ®N^ с fас(n)=n! есть наименьшая неподвижная точка j, т.е. наименьшее решение функционального уравнения j[f]=f с  Индуктивное толкование suр{¦i : i=0,1,¼} и толкование неподвижной точки fiх j полностью идентичны, если функционал j обладает так называемым свойством непрерывности. Проверим j на непрерывность j[sup{fi : i=0,1,...}](x) = j[sup{fi (x-1): i=0,1,...}] = sup{j[fi ]: i=0,1,...}](x) = sup{j[fi (x)]: i=0,1,...}] = sup{faci+1 (x): i=0,1,...}=x! ˆ Для сравнения с хорошими функционалами рекурсивных определений приведем пример немонотонного функционала. Пусть функционал j, действуя на функцию f: N®N, выглядит следующим образом: Пусть f£g, g¹f, x0 - наибольшая точка (обычный порядок на N) области определения f. Для x¹x0 области определения f t[f]=t[g]=^. Для x=x0 t[f](x0 ) = 1, а t[g](x0 ) = ^. Таким образом, мы получили t[f](x0 ) ³ t[g](x0 ). Значит, построенный нами функционал не является монотонным. † Рекурсивные типы могут трактоваться как решения уравнений для множеств. Пример (индуктивное толкование рекурсивного объявления типа). Пусть дано следующее объявление типа двоичных деревьев sоrt m = еmрtу(еmрtу )ïсоns(m lеft, nаt rооt, m right). Если записывать e для единственного элемента типа еmрtу, то для любого множества данных М получим: D(М)={e}È{(l,х,r): lÎМ\{^} Ù хÎN Ù rÎМ\{^}}È{^}. Это приводит к следующим множествам данных: М0 ={^}, Мi+1 ={e}È{(l,х,r): lÎМi \{^} Ù хÎN Ù rÎМi \{^}}È{^}, т.е. М1 ={^, e}, М2 ={^, e, (e,0,e), (e,1,e), ...}, М3 ={^, e, (e,0,e), ((e,0,e), 0, e), ...}. Итак, получаем множество, эквивалентное множеству двоичных деревьев.  Пример (трактовка неподвижной точки для двоичных деревьев в рекурсивном объявлении типов). Пусть имеют место определения предыдущего примера. Для множества М с М=ÈМi имеет место М={e}È{(l,х,r): lÎМ\{^} Ù хÎN Ù rÎМ\{^}}È{^}, (*) т.е. М есть решение уравнения М=D(М). М является также наименьшей неподвижной точкой оператора D.  Действительно, оператор D является монотонным и непрерывным по теоретико-множественному включению. Монотонность очевидна. Если M1 ÍM2 , то D(M1 )ÍD(M2 ). Проверим непрерывность: M0 =^, Mi+1 =D(Mi ), тогда Mi ÊMi+1 . U D(Mi )=UMi+1 =D(UMi ). Формальные языки могут трактоваться как решения уравнений для множеств. Рассмотрим язык, определяемый БНФ (см. п. 3.4). <x>::=1|2<x> Зафиксируем решетку множеств по включению. Язык можем воспринимать как решение уравнения Доказательство монотонности и непрерывности оператора t аналогично случаю для оператора D. Решением уравнения является регулярное множество 2* ×1. Подведем итог использованию неподвижной точки. В рассмотренных примерах практическая роль уравнений незначительна, так как примеры достаточно простые. Это похоже на использование техники пределов для поиска предельного значения простой непрерывной функции. Но, уже приятно то, что с единых позиций рассматриваются рекурсивные функции, типы, формальные языки. Конечно же, настоящая роль теории неподвижной точки скажется в исследовании классов задач. Например, если регулярные языки будут определяться взаимной рекурсией, то известно, что их решение (наименьшую неподвижную функцию) можно искать аналогом метода Гаусса. Доказательство этого факта легче получить, если обобщить теорию неподвижной точки на декартово произведение. Тогда, выяснив совпадение индуктивной схемы и теоретико-множественной, от преобразований надо требовать свойства равносильности, то есть исследовать на теоретико-множественном уровне. 3.2 Редукционные реализации (математический аспект). Кажется весьма выгодной в отношении обучения тесная связь, существующая между теорией неподвижной точки, проблемой свободных переменных и комбинаторной редукцией. Это позволяет в обучении естественно переходить к математическому аспекту прагматика, а от него - к классу профессионала. Поэтому в этом пункте мы собираемся рассмотреть различные методы, используемые для реализации функциональных языков. При этом будет использоваться лямбда-нотация для функциональных выражений, которая является достаточно мощной, чтобы выразить все черты функционального языка, и в то же время достаточно простой, чтобы легко описать различные методы реализации без рассмотрения специфики языков. Кроме того, лямбда-нотация происходит из области математической логики, называемой лямбда-исчислением, на котором основаны многие теоретические результаты в области функциональных языков. Основные понятия бестипового лямбда-исчисления приводятся в приложении. Все функциональные языки основаны на применении функций. В лямбда-исчислении применение функций выражается b-редукцией. Неформально роль b-редукции состоит в том, чтобы заменить каждое вхождение формального параметра функции соответствующим параметром. В основе любой реализации лежит порядок выполнения последовательных редукций и условий, при которых последовательность редукций завершается. Существует два пути выполнения b-редукций: мы можем либо оставить ссылку на формальный параметр баз изменений, но запомнить обозначаемую ею величину, либо выполнить подстановку, которая заменяет ссылку на параметр его фактическим значением. Эти два подхода ведут к реализациям, основанным соответственно на контексте и копировании . Примером первого подхода является реализация, основанная на SECD-машине (см. Приложения). Кроме того, что фактические параметры запоминаются в отдельном контексте, эта реализация рассматривает лямбда-выражения “текстуально”, то есть как строки символов. Альтернативой этому является использование двумерного графового представления выражений. Общая модель, использующая такое представление, называется редукцией графов . Эта модель основана на копировании, поскольку применение функций к аргументу ведет к копированию графа тела функции с выполнением соответствующей подстановки аргумента. 3.2.1 Несколько слов о редукции графов . Редукция графов возникла как мощная модель реализации “ленивых” функциональных языков, особенно на параллельных компьютерах. Суперкомбинаторы и вполне задержанные вычисления являются двумя из важнейших методов, пригодных для эффективной реализации редукции графов. Дадим краткое описание редукции графов. Рассмотрим функциональную программу (lx. AND x x) (NOT TRUE). Представим эту программу деревом ее грамматического разбора где знак @ стоит на месте функциональной аппликации. Отметим, что карринг отражен в поддереве для (AND x x). Это дерево содержит два так называемых редуцируемых выражения (или редекса ), которые состоят из применения (аппликации) функции к своему аргументу (аргументам): применение NOT к TRUE и применение lx-абстракции к (NOT TRUE). Чтобы применить lx-абстракцию к ее аргументу (NOT TRUE) мы заменяем верхний узел @ некоторой конкретизацией тела lx-абстракции, в которой вместо каждого вхождения x подставляется указатель на аргумент: Заметим, что дерево превратилось в граф. Теперь мы можем применить NOT к его аргументу TRUE, получив Наконец, выполнив операцию AND, получим FALSE. Каждый из выполненных шагов вычисления называется редукцией . Этот простой пример показывает, что 1) Исполнение функциональной программы заключается в вычислении некоторого выражения. 2) Функциональная программа допускает естественное представление в виде дерева (или, в более общем случае, графа ). 3) Вычисление сводится к последовательности простых шагов, называемых редукциями , которые заключается в применении функции к некоторым аргументам (отсюда термин редукция графов ). Каждая редукция является локальным преобразованием графа. 4) Лямда-абстракция применяется к своему аргументу путем создания нового наполнения (конкретизации) своего тела, в котором вместо каждого свободного вхождения формального параметра подставляется указатель на этот параметр. 5) Вычисление завершается, когда больше нет редуцируемых выражений. При этом говорят, что выражение имеет нормальную форму . 6) Порядок редуцирования редексов не влияет на ответ. Теорема Черча-Россера гарантирует, что стратегия проведения - редукций - безразлична. Теорема Черча-Россера для b -редукции: Если P|>b М и P|>b N, то существует такой терм T, что M|>b T, N|>b T. 7) Редукции можно без опасений применять одновременно, так как они не мешают друг другу. Например, первые две редукции в нашем примере можно выполнить одновременно. Простейший способ реализации редукции графов заключается в том, чтобы выполнить обход тела лямбда-абстракции и построить его новую копию, подставляя указатель на аргумент вместо каждого свободного вхождения формального параметра. Тело абстракции рассматривается как шаблон и не изменяется в результате этой операции. Однако, этот способ неэффективен по причине большого количества проверок в каждом узле шаблона. Этот способ моделирует редукцию графов и является интерпретирующим. Более эффективным способом является компиляция , сопоставляющая каждому лямбда-телу фиксированную последовательность команд, которую компилятор может построить заранее. Скомпилированный код будет выполняться гораздо быстрее, чем алгоритм обхода дерева (по тем же причинам, по которым скомпилированный код выполняется быстрее интерпретированного кода в обычных языках). Но, к сожалению, не все лямбда-абстракции поддаются такой компиляции. Возникает проблема свободных переменных. 3.2.2 Проблема свободных переменных . Рассмотрим лямбда-абстракцию lx. (ly. - x y). При применении ее к некоторому аргументу, например 3, мы наполняем ее тело, создавая тем самым новую лямбда-абстракцию (lx. - y 3). Каждое применение lx-абстракции к новым аргументам создает новые и различные ly-абстракции, тем самым лишая нас надежды скомпилировать единственный фиксированный код для каждой лямбда-абстракции. Проблема заключается в свободном вхождении x в тело ly-абстракции. Каждый раз мы вынуждены строить новое наполнение ly-абстракции. Имеются ли какие-либо решения этой проблемы? К счастью, ответом является “да”. Есть два подхода, которые можно выбрать. Один из путей решения данной проблемы - обеспечить прямой доступ к значениям свободных переменных, то есть такой механизм, который поддерживает явный контекст. Этот подход приводит нас к SECD-машине, основанной на среде , содержащей значения всех свободных переменных. Другой подход заключается в том, чтобы преобразовать явные свободные переменные при компиляции. Один из способов добиться этого заключается в трансляции l-выражений в комбинаторную логику и в определении машины редукции графов для комбинаторных графов (комбинаторы, как и l-выражения, могут быть представлены в виде графов). Второй метод состоит в трактовке всех свободных переменных как аргументов дополнительных l-абстракций; этот метод называется l-поднятием (lifting ) [9] [25]. Существуют также более сложные методы, например, использование суперкомбинаторов [9]. 3.2.3 Комбинаторная редукция Рассмотрим формализацию вычислительных предписаний, которые представляются КОМБИНАТОРАМИ. В аппликативном программировании их роль значительна и в прагматическом плане (т.к. они могут послужить реализацией аппликативного интерпретатора), и в теоретическом плане (т.к. они являются теми функциями, которые порождают функции). Важно заметить, что при вычислении комбинаторы одно­образно применяются к переменным и к комбинаторам. К тому же они позволяют избежать проблемы свободных и связанных переменных. Это те факты, которые учитывались при создании аппликативного программирования. При комбинаторной реализации (реализации на основе комбинаторов) каждое l-выражение преобразуется в эквивалентное выражение, построенное только из применений примитивных функций и комбинаторов, каждый из которых является замкнутым выражением, то есть выражением без свободных переменных. В основе такого преобразования лежит функция, которая абстрагирует свободные переменные, оставляя после этого цепочку применений комбинаторов. Комбинаторная логика. Рассмотрим теорию, которая лежит в основе этого типа реализации, - комбинаторную логику. Теоретически только два комбинатора, называемые K и S, требуются для представления любого l-выражения. Но надо сказать, что результирующая комбинация является неэффективной из-за того, что требуется очень большое число таких комбинаторов (и связанных с ним применений). Комбинатором называется l-выражение, не содержащее свободных переменных. Например, функция тождества lx. x является комбинатором и обозначается обычно буквой I. Другим примером является комбинатор фиксированной точки Y = l h. (l x. h(xx))(l x. h(xx)). Двумя следующими примерами являются вычеркиватель K, задаваемый в виде K=lx.ly.x, и распределитель S, задаваемый S=lf.lg.lx. fx (gx). Любое l-выражение может быть преобразовано в аппликативное выражение , то есть в выражение, построенное целиком на применениях функций, где, таким образом, отсутствуют l-абстракции. Чтобы добиться этого нам достаточно включить в синтаксис выражения два комбинатора S и K в качестве дополнительных констант. Комбинаторная логика (КЛ). Созидается теория, в которой фиксируется, что значит равенство термов. Равенство фиксируется посредством доказательства. Подразумеваемая структура: A = <A, *, c1 ,¼,cm > - алгебраическая структура с непустым носителем А; выделенными в нем элементами c1 , c2 ,¼, cm , m³0; двуместной операцией *. {А - множество имен} Язык: термы, построенные из переменных, K, S посредством операции *. Формулы: равенства термов. Аксиомы: t = t для атомарных термов. St1 t2 t3 = t1 t3 (t2 t3 ) Kt1 t2 = t1 для произвольных термов. Правила вывода: Доказуемость: последовательность равенств a1 , a2 ,¼, an называется доказательством an , если ai - аксиома, либо имеются j, k < i такие, что ai получается из aj и ak по правилу вывода. Фактически l-исчисление и КЛ, определенная выше, являются эквивалентными в следующем смысле. Предлагаемый набор аксиом устанавливает эквивалентность двух комбинаторных выражений MКЛ и NКЛ , обозначаемую MКЛ =КЛ NКЛ . Подобным образом и в l-исчислении эквивалентность выражений =l , задается как рефлексивное, симметричное, транзитивное замыкание правил преобразования. Тогда, если El и EКЛ представляют одно и то же выражение в этих двух логиках, то можно показать, что MКЛ =КЛ NКЛ Û Ml =l Nl (если выполняется правило экстенсиональности Mx=Nx®M=N или правило h-конверсии lx. Mx=M). В этом смысле комбинаторная логика может рассматриваться как модель l-исчисления. В нашем представлении мы будем также использовать тождественный комбинатор I (его можно выразить через K и S). Заметим, что единственным механизмом сочетания выражений является применение функций - отсюда термин “аппликативное выражение”. В этом синтаксисе каждое выражение находится в чисто аппликативной форме и поэтому может быть представлено графом, в котором единственным типом внутренних вершин являются @-вершины. В этом случае не существует l-вершин. Сначала заметим, что l-выражения можно транслировать в комбинаторную форму путем последовательного абстрагирования (выделения) переменных из подвыражения. Функция comb , осуществляющая отображение l-выражений в комбинаторную форму, подробно описана в книге “Функциональное программирование” [24, стр. 294-295]. Так, например, применяя функцию трансляции comb к выражению lx.(ly. + x y), мы получим ее комбинаторную форму S (S(KS)(S (S(KS)(S(KK)(K+)) )(S(KK) I) )) (KI). В данном случае мы приходим к “программированию без переменных”. Так как переменные отсутствуют, то нет необходимости рассматривать вопрос об их именах и контексте. Таким образом, проблема свободных переменных оказывается решенной. Основная привлекательность комбинаторного подхода заключается в его математической элегантности и простоте вычислений, вытекающей из наличия только трех правил преобразования графов (исключая те, что связаны с примитивными функциями). Итак, все, что нам нужно сделать - это определить правила преобразования графов, соответствующее применениям S, K и I, и объединить их с правилами применения примитивных функций. Но, к сожалению, даже очень простое l-выражение имеет очень сложный эквивалент в КЛ. Поэтому проведем оптимизацию путем расширения набора примитивных комбинаторов S, K и I. 3.2.4 Комбинаторная редукция с помощью графов. Введем дополнительные комбинаторы B, C (композитор, перестановщик) B f x y ® f (x y) C f x y ® f y x. Тогда в КЛ, имеющей примитивные комбинаторы K, S, I, C, B, выполняются следующие равенства: S (K t1 )(K t2 ) =КЛ K (t1 t2 ) S (K t1 ) I =КЛ t1 S (K t1 ) t2 =КЛ B t1 t2 S t1 (K t2 ) =КЛ C t1 t2 . Каждое из этих равенств дает правило для упрощения применения S. Тогда применение функции comb приводит к оптимизированной форме: comb ( l x.(+ 2 (- x 3))) = B (+ 2) (C - 3). Теперь рассмотрим представление комбинаторных функций графами. Существует 2 правила. 1) Константу мы представляем в виде дерева с одной вершиной соответствующей самой константе. 2) Применения функций вида A B в виде: Пример: + 1 3 = (+ 1) 3 Пример: B (+ 2) (C - 3) 4 Для каждого комбинатора существует правило редукции, которое можно отобразить с помощью графов. 1) Редукция тождественного комбинатора 2) Редукция вычеркивателя 3) Редукция распределителя 4) Редукция перестановщика 5) Редукция композитора Ïðèìåð êîìáèíàòîðíîé ðåäóêöèè: B (+ 2) (C - 3) 4 B-ðåäóêöèÿ: 2.Ïîñòðîåíèå ãðàôîâ äëÿ âçàèìíî-ðåêóðñèâíûõ ôóíêöèé: Ïóñòü èìååòñÿ ñèñòåìà ôóíêöèé f1 = E1 f2 = E2 ... fn = En Ïðè÷åì Å1 ...Ån ìîãóò çàâèñÿòü îò f1 ...fn , òîãäà íàäî íàðèñîâàòü ãðàô äëÿ êàæäîé ôóíêöèè è ñîåäèíèòü äóãàìè îáðàùåíèÿ ê äðóãèì ôóíêöèÿì ñ âõîäàìè â íèõ. Ïðèìåð: f = comb( l x.cons x ( g x)) = S cons g g = comb( l x.cons( * x x) ( f x)) = S ( B cons square) f Îáðàùåíèå f 2 âûäàñò ïîñëåäîâàòåëüíîñòü 2 4 2 4 2 4... Ãðàô âûãëÿäèò ñëåäóþùèì îáðàçîì: Ïîñëåäíåå, ÷òî ìû ðàññìîòðèì ýòî ïðåäñòàâëåíèå ðåêóðñèâíûõ ôóíêöèé ñ ïîìîùüþ ãðàôîâ íà ïðèìåðå ôóíêöèè factorial . Ôóíêöèÿ factorial â êîìáèíàòîðíîì ïðåäñòàâëåíèå èìååò âèä factorial = S ( C ( B cond ( = 2)) 2) ( S * ( B factorial ( C - 1))). Ãðàô âûãëÿäèò ñëåäóþùèì îáðàçîì. Определим преобразование графа для представления применения Y-комбинатора. Это нетрудно сделать. Такое определение вытекает из определения фиксированной точки, то есть для любого l-выражения X имеем YX = X (YX) = X (X (X...X (YX)...)). Таким образом, граф обеспечивает корректное представление: 3.3 Модели теорий и типовые языки (системологический аспект). В этом пункте следовало бы “во всей красе” показать тесную связь техники неподвижной точки с денотационной семантикой лямбда-исчисления по Д. Скотт. Как уже отмечалось, на плоских доменах D’ и D’’ можно определить домен всех монотонных и непрерывных функций f : [D’ ® D’’]. В трактовке функций как абстрактных объектов нет ничего нового, также через комбинаторы (Карри, Чёрча) мы уже привыкли, что выражение f(x) определяется как вычислимая функция и от f, и от x. Но Д. Скотт решил задачу интерпретации: желательно было иметь множество A, в котором вкрадывалось бы его функциональное пространство A®A; по мощностным соображениям Кантора этого, однако, невозможно достичь; в 69 г. Д. Скотт построил модели лямбда-исчислений, урезав A®A до множества непрерывных (в надлежащей топологии; или, как мы показывали, через последовательности) функций на A. Конечно же, следовало бы рассмотреть пространство D¥ , но мы не готовы к этому. Поэтому в пункте 3.3.1 предлагается подход к рассмотрению графиковых моделей лямбда-исчисления по книге Э. Энгелера “Метаматематика элементарной математики”. Пункт 3.3.2 затрагивает общее значение теоремы о неподвижной точке, которое также следует разработать через аппликативный стиль. Это позволит в обучении непосредственно перейти от системологического аспекта прагматика к классу универсала. Завораживают слова Х. Барендрегта в книге “Ламбда исчисление” (стр. 155): “Как геделевская конструкция рефлексивного предложения, так и теорема рекурсии могут быть истолкованы как теоремы о неподвижной точке для подходящих предполных нумерованных множеств в смысле Ершова”. 3.3.1 Î ìîäåëÿõ l-àëãåáðû èëè l-òåîðèè. (по Э. Энглер “Метаматематика элементарной математики”, Москва “МИР”, 1987г.) Возможности и границы эффективных методов, т.е. алгоритмов, в математике образуют столь же фундаментальный комплекс вопросов, как и возможности и границы аксиоматического описания основных математических структур. Мы снова применим метатеоретический подход. Мы попытаемся говорить об алгоритмах как об объектах в том же смысле, как раньше говорили о вещественных числах или таких геометрических объектах, как точки или прямые. Основные связи между такими объектами будут введены в качестве элементов языка. Язык позволяет использовать выразительные средства, во-первых, при аксиоматическом исследовании; во-вторых, при обосновании вычислимости как теории формального оперирования с вычислительными операциями. 1 Что такое вычислительное предписание? 1.1 Алгоритмика начинается с понятия функции, точнее, понятия вычислимой функции. Разумеется, всем знакомо сведение функции к понятию множества (по Дирихле): функция F: A®B - это подмножество F Í A x B, обладающее свойством "xÎA $!yÎB (<x,y>ÎF) В соответствии с этим реляционным определением функция расположена перед нами как единое целое во всем своем протяжении или экстенсионале . Однако вычислительное предписание не соответствует такому идеализированному теоретико-множественному пониманию; оно начинает с понятия функции, которая в применении к аргументу выдает вполне определенное значение. В школе вычислительные предписания принимают главным образом вид выражений. Например, f1 =(x+2)(x-2) или f2 =x2 -4. Таким образом, f1 ¹ f2 , хотя f1 (x) = f2 (x). То есть в случае вычислительных предписаний наш интерес направлен не на экстенсионал функции, совокупность ее значений, а скорее на ее интенсионал. Например, смысл функционального выражения в алгоритмике состоит в его сущности как предписания для исполнения одной или нескольких вычислительных операций. Наша цель - обосновать алгоритмику как теорию оперирования с вычислительными предписаниями и над ними. Сравним с теорией групп - она работает с понятием умножения элементов группы. В аксиоматической алгоритмике основной операцией является применение функции к аргументу или аппликация ¦ * a . Итак, исходный пункт - понятие функции, понимаемой как вычислительное предписание. Теперь мы делаем большой скачок в неизвестное: мы мыслим вычислительные предписания собранными в одну-единственную неструктурированную совокупность. Предусмотренное нами слияние типов родственно точке зрения, принятой в теории множеств, где между множествами также нет никаких различий в уровне. (В теории множеств удается образовать на основе одного-единственного понятия “x есть элемент совокупности y” чрезвычайно многообразно структурированную совокупность математических понятий. Вспомним пару {{x}, {x,y}}. Совсем не такая точка зрения принята в анализе, где функции из R®R отличаются от функционалов (R®R)®R и т.д.) Бестиповое понимание совокупности вычислительных предписаний делает возможным столь же экономный выбор исходных понятий при аксиоматизации, как и в аксиоматической теории множеств. Например, нам не нужно различать одноместные и многоместные вычислительные предписания (карризация; F=lx.ly.f x y, тогда F*x=ly.f x y, тогда (F*x)*y=f x y. Эта идея восходит от Фреге и была впервые систематически применена Шейнфинкелем.) Примеры вычислительных предписаний. Мы можем мыслить объект B, удовлетворяющий равенству Bfgx = f(gx) {звездочки, по соглашению, опускаются} или fxyzuv = z (x (zu (yv))) (y (x (zuv))) Теперь мы выдвинем неограниченную выполнимость этой функциональной абстракции в качестве аксиоматического требования к предметной области. Комбинаторные алгебры. Пусть A = <A, *, c1 ,¼,cm > - алгебраическая структура с непустым носителем А; выделенными в нем элементами c1 , c2 ,¼, cm , m³0; двуместной операцией *. {Итак, А - множество имен} Пусть t(x1 ,¼,xn ) - терм в А , (т.е. построен из констант, обозначающих выделенные элементы, и переменных x1 ,¼,xn с помощью скобок и знака операции *. Говорят, что элемент ¦ множества А представляет терм t в А , если "a1 ,¼,an (¦ a1 ¼an = t(a1 ,¼,an )). Алгебра А комбинаторно полна, если любой терм t представим в А. В этом случае А называется комбинаторной алгеброй. Она называется нетривиальной , если А содержит более одного элемента. Достаточно комбинаторов S и K. Пусть A = <A, *, K, S> Sxyz = xz (yz) Kxy = x. Тогда А - комбинаторная алгебра. Таким образом, комбинация, заданная термом t, всегда представляется в комбинаторной алгебре (хотя бы одним) объектом. Ввиду их происхождения мы называем такие объекты комбинаторами . Доказательство обеспечим леммой. Из доказательства следует естественность выбора комбинаторов S, K. Лемма . Для любого n и терма tn (x1 , ¼ ,xn ), построенного из S, K и x1 , ¼ ,xn , имеется терм tn-1 (x1 , ¼ ,xn-1 ), построенный из S, K и x1 , ¼ ,xn-1 , такой, что tn-1 (x1 , ¼ ,xn-1 ) * xn = tn (x1 , ¼ ,xn ). Доказательство: индукцией по построению База: Пусть tn º K | S | xi , i¹n, тогда имеем tn-1 =(Ktn ). Действительно, (Ktn )*xn =tn . Пусть tn º xn , тогда имеем tn-1 =I=SKK. Действительно, SKK*xn = Kxn (Kxn ) = xn . Составные термы: , тогда имеем tn-1 = St’ n-1 t’’ n-1 . Действительно, St’ n-1 t’’ n-1 *xn = t’ n-1 xn (t’’ n-1 xn ) = t’ n t’’ n . Теперь комбинаторная полнота получается многократным применением леммы: tn (x1 ,¼,xn ) = tn-1 (x1 ,¼,xn-1 )xn = tn-2 (x1 ,¼,xn-2 )xn-1 xn =¼= to x1 ,x2 ¼,xn . Š Применим доказательство для построения комбинаторов для выражений. 1) Bxyz = x (yz) Итак, t2 (x,y) = S(Kx)y = t1 (x)y, Осталось t1 (x) = S(Kx) = to x t’o = S = Ksx t’’o = Kx, Значит to x = S(KS)Kx. Тем самым B = S (KS) K. Действительно, Bxyz = S(KS)Kxyz = (KSx)(Kx)yz = S(Kx)yz = (Kxz)(yz) = x(yz). 2) Cxyz = (xz)y Итак, Итак, , Итак, C=S (1 S (KS) (2 S (KK) S)2 )1 (KK). Действительно, Cxyz = S()1 (KK)xyz = (()1 x)Kyz = (S(()2 x))Kyz = S(K(Sx))Kyz = (K(Sx)y)(Ky)z = Sx(Ky)z = (xz)y. 3) , т.к. K=KKx. 2 Существование комбинаторных алгебр. Карри и Чёрч построили системы математики (добавив логические законы и части математики), которые оказались противоречивыми. Вспомним Фреге. Исторически первым был теоретико-доказательный подход. (То есть дань времени - программы Гильберта. Вопрос о существовании таких алгебр заменяется вопросом о непротиворечивости формальной системы; комбинаторная алгебра превращается в комбинаторную логику . Комбинаторная логика. Созидается теория, в которой фиксируется, что значит равенство термов. Фиксируется посредством доказательства. Подразумеваемая структура: A = <A, *, c1 ,¼,cm >. Язык: термы, построенные из переменных, K, S посредством операции *. Формулы: равенства термов. Аксиомы: t = t для атомарных термов. St1 t2 t3 = t1 t3 (t2 t3 ) Kt1 t2 = t1 для произвольных термов. Правила вывода: Доказуемость: последовательность равенств a1 , a2 ,¼, an называется доказательством an , если ai - аксиома, либо имеются j, k < i такие, что ai получается из aj и ak по правилу вывода. {278 Гоген} Эквациональная логика, которая по существу является логикой подстановки “равных вместо равных”, составляет фундаментальное ядро (???) функционального программирования. Вопрос о непротиворечивости сводится к доказательству того факта, что невозможно вывести все формулы соответствующего языка. Например, формулу K = S. Действительно, если K = S, то То есть t1 = t2 (дал произвольные). Исчисление редукций. Создается теория, в которой фиксируется, что значит редуцируется терм к другому. Фиксируется посредством доказательства. Язык: термы как в комбинаторной логике. Формулы: высказывания о редуцируемости t1 ® t1 Аксиомы: t ® t для атомарных термов. St1 t2 t3 ® t1 t3 (t2 t3 ) Kt1 t2 ® t1 для произвольных термов. Правила вывода: Редуцируемость: как доказуемость в комбинаторной логике. Исчисление конверсий. Еще более общее понятие (эквивалентное одновременной конверсии). Язык: термы комбинаторной логики. Формулы: t1 ||® t2 (||® семантика этого знака - редуцируется равенством). Аксиомы: t ||® t для атомарных термов. St1 t2 t3 ||® t1 t3 (t2 t3 ) Kt1 t2 ||® t1 для произвольных термов. Правила вывода: Конвертируемость: как доказуемость в комбинаторной логике. Индукцией по длине доказательства можем доказать, что Лемма 1. t1 ® t2 Û t1 || ® t11 * , t11 || ® t12 , ¼ , t1n || ® t2 . {Справа - это не тоже, что t1 || ® t2 }. Можем получить теорему Чёрча-Россера: если m=n в комбинаторной логике, тогда $z (m®z Ù n®z), причем строится z эффективно по доказательству m=n. (При доказательстве теоремы используются похожие свойства для редукции и конверсии. Для редукции: если (a®m Ù a®n) Þ $z (m®z Ù n®z). Для конверсии аналогично.) Теорема. S=K недоказуемо в комбинаторной логике. Доказательство: от противного. Пусть S=K доказуемо. Тогда $z (S®z Ù K®z) по теореме Чёрча-Россера. Тогда существует последовательность конверсий S||®c11 , ¼, c1n ||®z, что невозможно, т.к. S||®S и только. ˆ 3 Модели из термов (эрбрановская модель). Подобные модели конкретны в той же степени, что и объекты классической математики вообще. Показав, что комбинаторная логика непротиворечива, мы получили разбиение термов комбинаторной логики на классы эквивалентности посредством доказуемости. Итак, t~t¢ Û t=t¢ - можно доказать. Эта эквивалентность, по определению комбинаторной логики (t1 =t2 Þ zt1 =zt2 и t1 z=t2 z), является даже конгруэнтностью относительно операции *. То есть если t1 =t1 ¢ и t2 =t2 ¢ Þ t1 *t2 =t1 ¢*t2 ¢. Действительно, t1 =t1 ¢ Þ t1 *t2 =t1 ¢*t2 , t2 =t2 ¢ Þ t1 ¢*t2 =t1 ¢*t2 ¢.Тогда t1 *t2 =t1 ¢*t2 ¢. Итак, определения. Модель из термов. T = термы комбинаторной логики, t~t¢ Û t=t¢ доказуемо. Пусть `t = {t¢ | t~t¢}. Заметим, что отношение эквивалентности является конгруэнцией для *, т.е. t1 ~t1 ¢, t2 ~t2 ¢ влечет t1 *t2 ~ t1 ¢*t2 ¢ Система <`A, *, `S, `K> является комбинаторной алгеброй, где `A = {`t | tÎT}: .` Она называется моделью из термов. Сравним конструкцию модели из термов с моделью поля рациональных чисел. Сделаем все последовательно. Рассмотрим натуральные числа N={1,2,¼} как абелеву полугруппу с дополнением, т.е. <N, +>; x+y=y+x; x+(y+z)=(x+y)+z; x+y¹x; x¹y Þ $z (x+z=y Ú x=y+z). Перейдем к целым числам. Если n £ m Þ вычитание не может быть натуральным числом; обозначим его временно символом n Q m: n Q m = x Û n = x+m. Если мы хотим сохранить аксиомы сложения, тогда m+k = x+(m+k), kÎN m-k = x+m-k, 1 £ k < min(m,n), т.е. (*) Например, (1Q3) = (2Q4) = (3Q5) = (4Q6) = (5Q7) = ¼ Класс эквивалентности (*) можем задать в виде (**) (n1 Qm1 ) + (n2 Qm2 ) Û n1 +m2 + n2 +m1 Рассмотрим теперь всевозможные выражения nQm, n,mÎN с законом отождествления (**). Посмотрим на сложение , т.е. складывать можем покомпонентно. Посмотрим на вычитание (nQm) Q (n¢Qm¢) Û yQz. Как обычно, выразим через сложение (nQm) = (yQz) + (n¢Qm¢) = (y+n¢) Q (z+m¢), т.е. . Это нужно, так как мы хотим представить (yQz) = (y+n¢+m¢)Q(z+n¢+m¢) = (n+n¢+k)Q(m+n¢+k) = (n+m¢)Q(m+n¢). Итак, (nQm)Q(n¢Qm¢) = (n+m¢)Q(m+n¢). Рассмотрим класс эквивалентности, выберем для них формы представления и нормальные формы. Введем символ 0. Итак, целые положительные представляются (n,0), целые отрицательные представляются (0,n), ноль представляется (0,0). Классы эквивалентности образуют группу по сложению, она изоморфна множеству отрицательных чисел Z. Установление равенства представителей целых чисел устанавливается или приводимостью к нормальной форме или по свойству (m1 ,n1