Теорія мов програмування

Теорія мови програмування (англ. Programming language theory) — розділ комп'ютерних наук, який займається проєктуванням, аналізом, визначенням характеристик і класифікацією мов програмування, їх індивідуальних особливостей. Він торкається математики, програмування і лінгвістики. Це добре відома галузь інформатики, а також активна область досліджень, результати яких опубліковані в численних журналах, присвячених PLT, а також в загальних виданнях з інформатики та інженерної справи.

Маленька грецька буква λ (лямбда) це неофіційний символ області теорії мови програмування. Використання походить від лямбда-числення, моделі обчислень, введеної Алонзо Черчем у 1930-х роках і широко використовується дослідниками мов програмування. Вона прикрашає обкладинку класичної книги «Структура та інтерпретація комп'ютерних програм», а також назва так званих «лямбда матеріалів», які написані Джеральдом Джей Зуссманом і Гай Стілом, розробників мови програмування Scheme.

Історія

У деякому сенсі, історія теорії мови програмування передує навіть розвитку самих мов програмування. Лямбда-числення, розвинене Алонзо Черчем і Стівеном Коулом Кліні в 1930-х, на думку деяких, є першою в світі мовою програмування, навіть при тому, що воно було призначене більше для обчислювальних розрахунків, ніж засіб для програмістів, яке описує алгоритми комп'ютерної системи, Багато сучасних функціональних мов програмування легко описуються з точки зору лямбда-числення.

Першою мовою програмування, яка була винайдена, була Планкалкюль (нім.- обчислення планів), який була розроблена Конрадом Цузе в 1940-х, але не була відома суспільству до 1972 (і не була здійснена до 1998). Перша широко відома і успішна мова програмування — Фортран (1954—1957), яка розроблена командою дослідників IBM на чолі з Джоном Бекусом. Успіх Фортрану привів до формування комітету вчених, які намагалися розробити «універсальну» комп'ютерну мову. Результатом їх зусиль був АЛГОЛ 58. В той же час, Джон Маккарті із MIT розробив мову програмування Лісп (засновану на лямбда-численні), яка є першою успішною мовою з науковим походженням. З успіхом цих початкових зусиль мови програмування стали активної темою дослідження в 1960-х і після. Деякі інші ключові події в історії теорії мови програмування з тих пір:

1950-ті

• Ноам Чомскі розробив ієрархію Чомскі в галузі лінгвістики. Це відкриття безпосередньо вплинуло на теорію мови програмування та інші галузі інформатики.

1960-ті

• Мова Симула була розроблена Оле-Йоном Далем і Крістеном Нюгордом. Вважають, що це перший приклад об'єктно-орієнтованої мови програмування. Симула також ввела поняття співпрограми.
• У 1964 Пітер Ландін вперше реалізував лямбда-числення Черча, що може бути використаним для моделювання мов програмування. Він представляє машину Secd, яка «інтерпретує» лямбда-вирази.
• У 1965 році Ландін вводить оператор J, який є формою продовження.
• У 1966 році Ландін у своїй статті «Наступні 700 мов програмування» презентував ISWIM, абстрактну комп'ютерну мову програмування. Це мало великий вплив в подальшій розробці мов програмування, що ведуть до Haskell.
• У 1966 році Коррадо Бем представив мову програмування Coach
• У 1967 році Крістофер Стрейчі опублікував свій важливий набір конспектів лекцій щодо основних понять мов програмування, введення R-значення термінології, L-значення, параметричний поліморфізм, а також спеціальний поліморфізм.
• У 1969 році Дж Роджер Гіндлі публікує основну тип-схему^{[що це?]} об'єкта у комбінаторній логіці, пізніше узагальнену в алгоритм виведення типів Гіндлі-Мілнера.
• У 1969 році Тоні Гоар вводить логіку Гоара, форму аксіоматичної семантики.
• У 1969 році Вільям Елвін Говард помітив, що систему доведення «високого рівня», іменовану природним виведенням, можна безпосередньо інтерпретувати в надрукований варіант моделі обчислень, відомий як лямбда-числення. Пізніше це отримало назву "відповідність Каррі — Говарда". 

1970-ті

• У 1970 році Дана Скотт вперше опублікувала свою роботу по денотаціонной семантиці.
• У 1972 році було розроблені логічне програмування і пролог. Це дало можливість комп'ютерним програмам виражатися через математичку логіку.
• У 1974 році Джон С. Рейнольдс виявляє систему F. Це було уже винайдено математичним логіком Жан-Ів Жираром ще в 1971 році.
• З 1975 року, Сассмен і Стіл розробляю мову програмування Scheme і мову Лісп, яка включає лексичну зону видимості, єдиний простір імен і елементи з моделі Actor, включаючи продовження першого класу.
• Бакус, в 1977 році лекції премії Тюрінга, розкритикував поточний стан індустріальних мов і запропонував новий клас мов програмування. В даний час відомі як функціонально-рівневі мови програмування.
• In 1977, Гордон Плоткін презентував програмування обчислювальних функцій, абстрактно набрана мова
• У 1978 році Робін Мілнер вводить алгоритм виведення типів Гіндлі-Мілнера для мови програмування ML. Теорія типу стала застосовуватися як дисципліна мов програмування, цей додаток привів до величезних досягнень в області теорії типу протягом багатьох років.

1980-ті

• У 1981, Гордон Плоткін опублікував свій документ на структурованій операційній семантиці.
• У 1988 році Жиль Кан опублікував свою статтю про нормальну семантику.
• Команда вчених  Xerox PARC під керівництвом Алана Кея розробили Smalltalk, об'єктно-орієнтована мову, яка широко відома своїм інноваційним розробницьким середовищем .
• Там з'явилися обробки обчислень: обрахунок взаємодіючих систем Робіна Мілнера, модель комунікативних послідовних процесів Тоні Гоара, а також аналогічні моделі паралелізму(наприклад, модель Actor Карла Хьюітта.
• У 1985, випуск Miranda запалює навчальний інтерес до раніше відкладених чистих функціональних мов програмування. Був створений комітет для визначення відкритого стандарту, що призвів до випуску Haskell 1.0 в 1990 році.
• Бертран Мейер створив методологію проєктування (за договором) та включив її в мову програмування Eiffel.

1990-ті

• Грегор Кізалес, Джим Де Рів'єр і Даніель Г. Бобров опублікували книгу «Мистецтво протоколу метаоб'єкта».
• Євгеніо Моджі і Філіп Вадлер ввели використання монад для структурування програм, написаних на функціональних мовах програмування.

Субдисципліни і суміжні області

Є кілька областей дослідження, які або лежать в теорії мови програмування, або які надають великий вплив на неї; багато з них мають важливе значення. Крім того, PLT використовує багатьо інших областей математики, включаючи теорію обчислюваності, теорію категорій і теорію множин.

Формальна семантика

Формальна семантика це формальний опис поведінки комп'ютерних програм і мов програмування. Три загальних підходи до опису семантики або «сенс» комп'ютерної програми — денотаційна семантика, операційна семантика і аксіоматична семантика.

Теорія типів

Теорія типів це вивчення типових системі; яка є «слухняним синтаксичним методом доказу недостатності поведінки конкретної програми шляхом класифікації фраз за видами значень, які вони обчислюють». Багато мов програмування відрізняються характеристиками їх систем типів.

Аналіз програми та трансформація

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

Порівняльний аналіз мови програмування

Порівняльного аналізу мови програмування прагне класифікувати мови програмування на різні типи залежно від їх характеристик. Загальні категорії мов програмування часто називають парадигмами програмування.

Загальне і метапрограмування

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

Предметно-орієнтовані мови

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

Тлумачення компілятора

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

Системи виконання

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

Журнали, публікації та конференції

Конференції є основним місцем для презентування досліджень в мовах програмування. Найбільш відомі конференції включають це Симпозиум про принципи мов програмування (POPL-Symposium on Principles of Programming Languages), Конференція про проєктування та впровадження мов програмування(PLDI-Conference on Programming Language Design and Implementation), міжнародна конференція функціонального програмування(ICFP-International Conference on Functional Programming), та міжнародна конференція обєктно-орієнтованого програмування, систем, мов та додатків (OOPSLA-the International Conference on Object Oriented Programming, Systems, Languages and Applications).

Відомі журнали, які публікують PLT: the ACM Transactions on Programming Languages and Systems (TOPLAS), Journal of Functional Programming (JFP), Journal of Functional and Logic Programming, and Higher-Order and Symbolic Computation.

Примітки

http://www.c2.com/cgi/wiki?ModelsOfComputation [ 9 липня 2016 у Wayback Machine.]

Посилання

• Lambda the Ultimate [ 20 квітня 2016 у Wayback Machine.], a community weblog for professional discussion and repository of documents on programming language theory.
• Great Works in Programming Languages [ 2 квітня 2016 у Wayback Machine.]. Collected by Benjamin C. Pierce (University of Pennsylvania).
• Classic Papers in Programming Languages and Logic [ 11 травня 2016 у Wayback Machine.]. Collected by Karl Crary (Carnegie Mellon University).
• Programming Language Research [ 21 квітня 2016 у Wayback Machine.]. Directory by Mark Leone.
• Programming Language Theory Texts Online [ 2 жовтня 2014 у Wayback Machine.]. At Utrecht University.
• λ-Calculus: Then & Now [ 2 липня 2021 у Wayback Machine.] by Dana S. Scott for the ACM Turing Centenary Celebration
• Grand Challenges in Programming Languages [ 6 березня 2016 у Wayback Machine.]. Panel session at POPL 2009.