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

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

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

Історія[ред.ред. код]

У деякому сенсі, історія теорії мови програмування передує навіть розвитку самих мов програмування. Лямбда-числення, розвинене Алонзо Черчем і Стівеном Коулом Кліні в 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

Посилання[ред.ред. код]