Уводна лекция

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

Още през 1924 г. М. Scheinfinkel (Moses Schonfinkel) разработва проста (проста) теория на функциите, която всъщност е смятане на функционални обекти и очаква появата на ламбда смятане - математическа формализация, която поддържа функционални езици за програмиране (т.е. по отношение на функциите).

След това, през 1934 г. А. Чърч (Църквата на Алонсо) предлага действителното смятане на ламбда преобразувания (или ламбда смятане) и го прилага за изучаването на теорията на множествата. Приносът на учения е бил основен, така че теорията все още се нарича ламбда смятане и често в литературата се нарича ламбда смятане на Църквата.

По-късно, през 1940 г., Х. Къри (Haskell Curry) създава теорията на функциите без променливи (иначе наричани комбинатори), която сега е известна като комбинаторна логика. Тази теория е разработка на ламбда смятането и е формален език, подобен на езика за функционално програмиране.

През 60-те години H. Barendregt описва подробно синтаксиса (т.е. формата на конструкциите) и семантиката (т.е. значението на конструкциите) на ламбда смятането.

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

През 60-те години Джон Бакус създава основите за формализиране на синтаксиса на програмните езици чрез специален математически език. По-късно P. Naur (Peter Naur) този език (и от гледна точка на целевия език за програмиране - метаезикът) е финализиран, в резултат на което възниква математическа нотация, известна днес като "Backus-Naur формы", или накратко BNF .

Тази нотация е специално разработена, за да формализира синтаксиса на езика за програмиране (по това време той беше много популярен, предимно в математическата среда, език за програмиране ALGOL 60 с ясен, но доста дълъг синтаксис). BNF все още е теоретично адекватен и практически приложим инструмент за формализиране на синтаксиса на програмните езици.

През 90-те години синтаксисът на съвременния език за програмиране SML е формулиран от R. Milner (Robin Milner). Формите на Backus-Naur все още се използват широко в произведения, описващи синтаксиса на SML.

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

Освен това през 70-те години М. Гордън (Michael J. C. Гордън) изследва апарата на денотационната семантика във връзка с функционалните езици за програмиране и прави заключение относно адекватността и практическата ефективност на използването на този подход за решаване на проблема.

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

Един от практическите резултати от изследванията в тази насока е развитието от Питър Дж. Ландин на семантиката на езиков модел за програмиране под формата на абстрактна машина (т.е. компютърен модел), която използва концепцията за състояние.

Алтернативен подход за формализиране на семантиката (който беше осъществен в рамките на изследването на т. Нар. Оперативна семантика на програмните езици) доведе до създаването от Чарлз А.Р. Хоаре на аксиоматичен метод, който моделира връзки и причинно-следствени връзки които възникват между оператори на език за програмиране.

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

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

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

През 60-те години Роджър Хиндли изследва машинопис в комбинаторната логика. В същото време основният проблем беше моделирането на функционални езици за програмиране със силно писане, към които, по-специално, принадлежи изучаваният в курса SML език. Р. Хиндли разработи типов извод, т.е. способността имплицитно да определя типа на израза въз основа на видовете изрази, които го заобикалят. Именно тази функция е широко използвана в съвременните програмни езици като SML и Haskell.

Освен това Р. Хиндли изучава системи от полиморфен тип, т.е. тип системи, в които са разрешени параметризирани функции или функции от променлив тип.

По-късно, през 70-те години, Р. Милнер предлага практическо внедряване на разширената полиморфна система за типизиране на функционалния език за програмиране ML, което дава началото на езика за програмиране SML .

И накрая, в края на 80-те и 90-те години редица изследователи - Уилям Р. Кук, П. Канинг, У. Хил (Уолтър Л. Хил) и други - изучават концепцията за полиморфизъм, прилагана към обектно-ориентираното програмиране ( по-специално към езика C ++) и беше разкрита възможността за моделиране на полиморфизъм въз основа на ламбда смятането.

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

Ключовият елемент в изпълнението на функционални езици за програмиране е рекурсивно изчисление, т.е. изчисления, базирани на прилагане на функция към себе си като аргумент.

Фундаменталната осъществимост на рекурсията посредством математическа теория е доказана от S.C. Kleene още през 30-те години. В този случай основата на разсъжденията беше ламбда смятането .

През 50-те години се появява комбинаторната логика на Х. Къри - формална система, по-близка до практиката на програмиране с възможност за симулиране на рекурсия.

Скоро, през 60-те, Джон Маккарти, по време на създаването на функционалния език за програмиране LISP, изследва практическата приложимост на рекурсивни изчисления за символна обработка и доказва възможността за прилагане на рекурсия в програмирането.

Абстрактната машина като формален модел на изчислителна система е много важен обект на изследване в рамките на този курс.

Комбинаторната логика на H. Curry позволява да се симулират изчисления в средата на абстрактни машини, подобно на виртуална машина. НЕТ .

През 60-те години Дейвид Търнър предлага да се използват комбинатори като код на ниско ниво за преводачи на функционални езици за програмиране, т.е. очакваха появата на абстрактни машини, използващи комбинатори като инструкции.

Също през 60-те години П. Лендин създава първата практически осъществима абстрактна машина, базирана на разширеното ламбда смятане. Машината, наречена SECD, формализира изчисления в езика за програмиране ISWIM (Ако виждате какво имам предвид), който по-късно се превръща в прототип на функционалния език за програмиране ML. Основната концепция за SECD машината е концепцията за държавата.

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

Като основна формализация за този курс се използва комбинаторната логика на H. Curry, която позволява да се симулират изчисления в средата на абстрактни машини, до голяма степен подобна на виртуалната машина на Microsoft. НЕТ .

Изследвания на различни стратегии за предаване на параметри при позоваване на функции на програмни езици (по-специално извикване на функции по име и по стойност) бяха извършени от Г. Плоткин въз основа на развитието на SECD машинната формализация на П. Лендин. Получените резултати са в основата на стратегията за моделиране на изчисления в ранните версии на езика за функционално програмиране ML.

През 70-те години Кристофър П. Уодсуърт предложи механизъм за намаляване на графика за моделиране на така наречените "мързеливи" (т.е. изпълнявани само при необходимост) изчисления, използвайки основната формална теория-смятане на ламбда преобразувания.

Малко по-късно Д. Търнър представи подобен механизъм за „мързеливи“ изчисления във формална система, по-близка до практиката на програмиране, а именно по отношение на изрази на комбинаторната логика.

Около същия период R.J.M. Hughes разработва официална система от суперкомбинатори (усъвършенствана комбинаторна логика на H. Curry), която позволява моделиране на методи за внедряване на програмни езици с възможност за оптимизиране на изчисленията.

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

През 50-те години Х. Хасе (Хелмут Хасе, 1898-1979) предлага да се използва специален вид диаграма за графична интерпретация на връзката на частичния ред. Обърнете внимание, че по-късно диаграмите, открити от учения, започнаха да се наричат ​​диаграми на Хасе. И до днес диаграмите на Хасе са най-широко използваната графична формализация на механизма за наследяване.

След това, през 1976 г., Н. Д. Русопулос за първи път прилага рамкова нотация за моделиране на връзки между обекти в определени домейни. В допълнение, ученият въведе така наречената ISA - частна връзка на реда, която адекватно моделира концепцията за наследяване. Имайте предвид, че обозначението ISA, което произхожда от английските думи „is a“, което означава „е един от“, добре илюстрира същността на концепцията за наследяване на естествен език.

По-късно, през 1979 г., Д. Скот формулира теорията на пълните и непрекъснатите решетки, която се използва в диаграмите на потока от данни. Решетката на Д. Скот е частично подреден набор от модели или, с други думи, модел на йерархия на класа.

След това, през 1988-90 г. Л. Кардели (Лука Кардели), У. Кук и други учени изследват семантиката на наследяването. В същото време е изграден вариант на денотативна семантика, който, както се оказа, адекватно формализира не само единично, но и множествено наследяване .

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

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

През 80-те години Д. Скот и М. Фурман (Майкъл П. Фурман) изследват механизма на определени описания за формализиране на определенията. В хода на тази презентация ние многократно ще използваме тази лаконична и интуитивно прозрачна нотация за математически строга съкратена нотация на дефиниции на обект, тип и клас.

По-късно, през 90-те години, В. Волфенгаген (Vyatcheslav E. Wolfengagen) създава така наречената схема за концептуализация на две нива, базирана на двойното приложение на сгъваемия постулат (до известна степен, подобна на операцията на ламбда абстракция). Моделът ви позволява да опишете изцяло и последователно обектите от предметните области, като вземете предвид тяхното разглеждане както в динамика, така и в статика. В същото време схемата за концептуализация на две нива дава възможност да се моделират както обекти от предметната област, така и обекти на програмни езици. Друго предимство на модела е възможността да се използва по отношение както на обекти от данни, така и на обекти на метаданни (метаданните могат да се разбират неформално като данни за данни).

За по-подробно самостоятелно запознаване с темата на лекцията се препоръчва следният списък с източници: [23, 38, [51], [61], [63]].