ЗНАЙ ИНТУИТ, Лекция, Уводна лекция
Най-важните математически формализации, разгледани в този курс, са ламбда смятане и комбинаторна логика .
Още през 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.