Теорія мови програмування (англ. 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

ПосиланняРедагувати