→ Пошук по сайту       Увійти / Зареєструватися
Знання Мова програмування C#

Вступ

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

Ще в 1924 р. М. Шейнфінкель (Moses Schonfinkel) розробив просту (simple) теорію функцій, яка фактично була обчисленням об'єктів-функцій і передбачила появу ламбда-числення - математичної формалізації, що підтримує мови функціонального програмування (тобто програмування в термінах функцій ).

Потім в 1934 р. А. Черч (Alonso Church) запропонував власне літочислення ламбда-переходів (або ламбда-числення) і застосував його для дослідження теорії множин. Внесок вченого був фундаментальним, так що теорія досі називається ламбда-обчисленням і часто іменується в літературі ламбда-обчисленням Черча.

Пізніше, в 1940 р., Х. Каррі (Haskell Curry) створив теорію функцій без змінних (інакше званих комбінаторами), відому нині як комбінаторна логіка. Ця теорія є розвитком ламбда-обчислення і являє собою формальну мову, подібну мові функціонального програмування.

У 60-х роках Х. Барендрегтом (H. Barendregt) були детально описані синтаксис (тобто форма конструкцій) і семантика (тобто значення конструкцій) ламбда-числення.

Саме синтаксис і семантика є найбільш суттєвими поняттями, фактично визначальними довільний мова програмування.

У 60-х роках Дж. Бекусом (John Backus) були створені основи формалізації синтаксису мов програмування за допомогою спеціальної математичної мови. Пізніше П. Науру (Peter Naur) ця мова (а з точки зору цільової мови програмування - метамова) був допрацьована, в результаті чого виникла математична нотація, відома і сьогодні під назвою "форм Бекуса-Наура", або, скорочено, БНФ.

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

У 90-х роках синтаксис сучасної мови програмування SML був сформульований Р. Мілнер (Robin Milner). У роботах, що описують синтаксис SML, і до цього дня широко використовуються форми Бекуса-Наура.

Що стосується теоретичних основ семантики обчислень, то в кінці 60-х років Д. Скотт (Dana S. Scott) запропонував застосувати для формалізації семантики математичних теорій так звані домени (поки будемо неформально розуміти їх як особливий вид множин). При цьому на основі доменів Д. Скоттом був запропонований так званий денотаціонний підхід до семантики. Такий підхід передбачає аналіз синтаксично коректних конструкцій мови (або, інакше, денотат) з точки зору можливості обчислення їх значень за допомогою спеціалізованих функцій.

Далі, у 70-х роках, М. Гордон (Michael JC Gordon) досліджував апарат денотаціоної семантики стосовно  мов функціонального програмування і зробив висновок про адекватність і практичну ефективність використання цього підходу для вирішення поставленого завдання.

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

Одним із практичних результатів досліджень у цьому напрямку стала розробка П. Лендіном (Peter J. Landin) семантики моделі мови програмування у формі абстрактної машини (тобто моделі комп'ютера), що використовувала поняття стану.

Альтернативний підхід до формалізації семантики (який був здійснений у рамках дослідження так званої операційної семантики мов програмування) привів до створення Ч. Хоаром (Charles AR Hoare) аксіоматичного методу, що моделює відносини і причинно-наслідкові зв'язки, що виникають між операторами мови програмування.

Розвиток операційної семантики мов програмування призвело Р. Флойда (Robert W. Floyd) до створення так званого методу індуктивних тверджень, який використовувався для формалізації семантики протікання інформації у програмі. При цьому суттєвою перевагою запропонованого Р. Флойдом методу стала можливість інтуїтивно прозорої  і наочної графічної ілюстрації, заснованої на блок-схемах, що формалізують послідовність протікання інформації.

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

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

У 60-х роках Р. Хиндлі (Roger Hindley) досліджував типізацію в комбінаторної логіці. При цьому основною проблемою було моделювання мов функціонального програмування з суворою типізацією, до яких, зокрема, відноситься досліджуваний у рамках курсу мова SML. Р. Хиндлі розробив виводимість типів (type inference), тобто можливість неявно визначати тип вираження, виходячи з типів виразів, які його оточують. Саме ця можливість широко використовується в сучасних мовах програмування, таких як SML і Haskell.

Крім того, Р. Хиндлі вивчив поліморфні системи типів, тобто такі системи типів, в яких припустимі параметризовані функції, що мають змінний тип.

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

Нарешті, на рубежі 80-х і 90-х років, рядом  дослідників - У. Куком (William R. Cook), П. Кеннінгом (Peter S. Canning), У. Хіллом (Walter L. Hill) і іншими - була вивчена концепція поліморфізму в додатку до об'єктно-орієнтованого програмування (зокрема, до мови C + +) і виявлено можливість моделювання поліморфізму на основі ламбда-числення.

Зауважимо, що концепція поліморфізму є не тільки суттєвою складовою функціонального програмування, але і основоположної для об'єктно-орієнтованого підходу, де створення додатків відбувається в термінах об'єктів.

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

Принципова реалізація рекурсії засобами математичної теорії була доведена С. Кліні (SC Kleene) ще в 30-х роках. При цьому фундаментом міркувань служило ламбда-числення.

У 50-х роках з'явилася комбінаторна логіка Х. Каррі - більш наближена до практики програмування формальна система з можливістю моделювання рекурсії.

Незабаром, у 60-х роках, Джоном Маккарті (John McCarthy) у ході створення мови функціонального програмування LISP, була досліджена практична застосовність рекурсивних обчислень для символьної обробки та доведено можливість реалізації рекурсії в програмуванні.

Абстрактна машина як формальна модель обчислювальної системи є дуже важливим об'єктом дослідження в рамках цієї курсу.

Ще в 30-х роках А. Тьюрінгом (Alan Mathison Turing) і Е. Постом (Emil Leon Post) незалежно один від одного були створені еквівалентні по можливостях, але практично дуже складні в реалізації формалізації, відомі як абстрактні машини i назви по іменах своїх авторів.

Комбінаторна логіка Х. Каррі дозволяє моделювати обчислення в середовищі абстрактних машин, в значній мірі схожих з віртуальною машиною. NET.

У 60-х роках Д. Тернер (David Turner) запропонував застосовувати комбінатори в якості низькорівневого коду для трансляторів мов функціонального програмування, тобто передбачив появу абстрактних машин, що використовують як інструкції комбінатори.

Також в 60-х роках П. Лендін створив першу практично реалізовану абстрактну машину на основі розширеного ламбда-числення. Машина, що одержала назву SECD, формалізувала обчислення на мові програмування ISWIM (If you See What I Mean), який згодом став прообразом мови функціонального програмування ML. Основним поняттям для SECD-машини є поняття стану.

Вже в 70-ті роки групою вчених інституту INRIA (Франція), провідну роль в роботі якої зіграв П'єр Кюрьен (P.-L. Curien), була створена ще одна абстрактна машина, заснована на зміні станів і отримала назву категоріальної абстрактної машини (КАМ ). Теорія категорій у формі категоріальної комбінаторної логіки, яка є теоретичним фундаментом для КАМ, по суті, являє собою варіант ламбда-числення. За допомогою КАМ був реалізований ще один сучасний діалект ML, що отримав назву CaML (по імені машини).

У ході дослідження абстрактних машин виникає проблема оптимізації стратегії обчислень.

В якості основної формалізації для цього курсу використовується комбінаторна логіка Х. Каррі, яка дозволяє моделювати обчислення в середовищі абстрактних машин, в значній мірі схожих з віртуальною машиною Microsoft. NET.

Дослідження різних стратегій передачі параметрів при зверненні до функцій мов програмування (зокрема, виконання функцій по імені і за значенням) були проведені Г. Плоткін (GD Plotkin) на основі розвитку формалізації SECD-машини П. Лендіна. Отримані результати лягли в основу стратегії моделювання обчислень у ранніх версіях мови функціонального програмування ML.

У 70-х роках К. Уодсворт (Christopher P. Wadsworth) запропонував механізм редукції графів для моделювання так званих "ледачих" (тобто виконуваних виключно в міру необхідності) обчислень за допомогою фундаментальної формальної теорії-числення ламбда-переходів.

Трохи пізніше Д. Тернером був представлений аналогічний механізм для "ледачих" обчислень у більш наближеній до практики програмування формальній системі, а саме, в термінах виразів комбінаторної логіки.

Потім, у 80-х роках, групі вчених на чолі з П. Кюрьеном вдалося вдосконалити формалізацію SECD-машини П. Лендіна, і була створена категоріально абстрактна машина, оптимізація коду якої вивчається в даному курсі.

Приблизно в той же період Р. Х'юса (RJM Hughes) була розроблена формальна система суперкомбінаторів (вдосконалена комбінаторна логіка Х. Каррі), що дозволяє моделювати методи реалізації мов програмування з можливістю оптимізації обчислень.

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

У 50-х роках Х. Гассе (Helmut Hasse, 1898-1979) запропонував використовувати особливого роду діаграми для графічної інтерпретації відносин часткового порядку. Зауважимо, що пізніше діаграми, відкриті вченим, стали називатися діаграмами Гассе. І до цього дня діаграми Гассе є найбільш широко поширеною графічної формалізацією механізму успадкування.

Потім в 1976 році М. Руссопулос (N.D.Roussopulos) вперше застосував фреймову нотацію для моделювання відносин між об'єктами тих чи інших предметних областей. Крім того, вченим було введено так зване ISA-відношення часткового порядку, яке адекватно моделює поняття наслідування. Зауважимо, що позначення ISA, яке виникло від англійських слів "is_a", що означають "є одним з", добре ілюструє суть поняття спадкування на природній мові.

Пізніше, в 1979 році, Д. Скотт сформулював теорію повних і безперервних решіток, яка використовується в діаграмах потоків даних. Решітка Д. Скотта представляє собою модель частково впорядкованої множини, або, інакше, модель ієрархії класів.

Потім, в 1988-90 роках Л. Карделла (Luca Cardelli), У. Куком та іншими вченими була досліджена семантика наслідування. При цьому був побудований варіант денотаціонної семантики, яка , як виявилося, адекватно формалізувала не тільки одиничне, але і множинне спадкування.

Важлива роль у курсі відводиться моделями об'єктів, що формалізують як визначення (в математичній теорії або програмі), так і взаємодію об'єктів у середовищі обчислень.

В кінці 60-х років Д. Скоттом була запропонована теорія обчислень - модель, заснована на понятті домену (яке можна неформально визначити як особливий вид множин). Ця модель принципово застосовна для формалізації об'єктів та їх взаємодії.

У 80-х роках Д. Скоттом і М. Фурманом (Michael P. Fourman) був досліджений механізм певних дескрипцій для формалізації визначень. У ході викладу ми будемо неодноразово використовувати цю лаконічну і інтуїтивно прозору нотацію для математично строгої скороченою записи визначень об'єктів, типів і класів.

Пізніше, в 90-і роки, В. Вольфенгагеном (Vyatcheslav E. Wolfengagen) була створена так звана дворівнева схема концептуалізації, заснована на дворазовому застосуванні постулату згортання (до певної міри аналогічного операції ламбда-абстракції). Модель дозволяє повно і несуперечливо описувати об'єкти предметних областей з урахуванням їх розгляду як в динаміці, так і в статиці. При цьому дворівнева схема концептуалізації дозволяє моделювати як об'єкти предметної області, так і об'єкти мов програмування. Іншою перевагою моделі є можливість її використання стосовно як до об'єктів даних, так і до об'єктів метаданих (метадані можна неформально розуміти як дані про дані).

загрузка...
Сторінки, близькі за змістом