Ця стаття містить правописні, лексичні, граматичні, стилістичні або інші мовні помилки, які треба виправити. |
Теорія мови програмування (англ. Programming language theory) — розділ комп'ютерних наук, який займається проєктуванням, аналізом, визначенням характеристик і класифікацією мов програмування, їх індивідуальних особливостей. Він торкається математики, програмування і лінгвістики. Це добре відома галузь інформатики, а також активна область досліджень, результати яких опубліковані в численних журналах, присвячених PLT, а також в загальних виданнях з інформатики та інженерної справи.
Історія
У деякому сенсі, історія теорії мови програмування передує навіть розвитку самих мов програмування. Лямбда-числення, розвинене Алонзо Черчем і Стівеном Коулом Кліні в 1930-х, на думку деяких, є першою в світі мовою програмування, навіть при тому, що воно було призначене більше для обчислювальних розрахунків, ніж засіб для програмістів, яке описує алгоритми комп'ютерної системи, Багато сучасних функціональних мов програмування легко описуються з точки зору лямбда-числення.
Першою мовою програмування, яка була винайдена, була Планкалкюль (нім.- обчислення планів), який була розроблена Конрадом Цузе в 1940-х, але не була відома суспільству до 1972 (і не була здійснена до 1998). Перша широко відома і успішна мова програмування — Фортран (1954—1957), яка розроблена командою дослідників IBM на чолі з Джоном Бекусом. Успіх Фортрану привів до формування комітету вчених, які намагалися розробити «універсальну» комп'ютерну мову. Результатом їх зусиль був АЛГОЛ 58. В той же час, Джон Маккарті із MIT розробив мову програмування Лісп (засновану на лямбда-численні), яка є першою успішною мовою з науковим походженням. З успіхом цих початкових зусиль мови програмування стали активної темою дослідження в 1960-х і після. Деякі інші ключові події в історії теорії мови програмування з тих пір:
1950-ті
- Ноам Чомскі розробив ієрархію Чомскі в галузі лінгвістики. Це відкриття безпосередньо вплинуло на теорію мови програмування та інші галузі інформатики.
1960-ті
- Мова Симула була розроблена Оле-Йоном Далем і Крістеном Нюгордом. Вважають, що це перший приклад об'єктно-орієнтованої мови програмування. Симула також ввела поняття співпрограми.
- У 1964 вперше реалізував лямбда-числення Черча, що може бути використаним для моделювання мов програмування. Він представляє машину Secd, яка «інтерпретує» лямбда-вирази.
- У 1965 році Ландін вводить оператор J, який є формою продовження.
- У 1966 році Ландін у своїй статті «Наступні 700 мов програмування» презентував , абстрактну комп'ютерну мову програмування. Це мало великий вплив в подальшій розробці мов програмування, що ведуть до Haskell.
- У 1966 році Коррадо Бем представив мову програмування
- У 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.
Ця стаття потребує додаткових для поліпшення її . (березень 2017) |
Це незавершена стаття про мови програмування. Ви можете проєкту, виправивши або дописавши її. |
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Cya stattya mistit pravopisni leksichni gramatichni stilistichni abo inshi movni pomilki yaki treba vipraviti Vi mozhete dopomogti vdoskonaliti cyu stattyu pogodivshi yiyi iz chinnimi movnimi standartami Teoriya movi programuvannya angl Programming language theory rozdil komp yuternih nauk yakij zajmayetsya proyektuvannyam analizom viznachennyam harakteristik i klasifikaciyeyu mov programuvannya yih individualnih osoblivostej Vin torkayetsya matematiki programuvannya i lingvistiki Ce dobre vidoma galuz informatiki a takozh aktivna oblast doslidzhen rezultati yakih opublikovani v chislennih zhurnalah prisvyachenih PLT a takozh v zagalnih vidannyah z informatiki ta inzhenernoyi spravi Malenka grecka bukva l lyambda ce neoficijnij simvol oblasti teoriyi movi programuvannya Vikoristannya pohodit vid lyambda chislennya modeli obchislen vvedenoyi Alonzo Cherchem u 1930 h rokah i shiroko vikoristovuyetsya doslidnikami mov programuvannya Vona prikrashaye obkladinku klasichnoyi knigi Struktura ta interpretaciya komp yuternih program a takozh nazva tak zvanih lyambda materialiv yaki napisani Dzheraldom Dzhej Zussmanom i Gaj Stilom rozrobnikiv movi programuvannya Scheme IstoriyaU deyakomu sensi istoriya teoriyi movi programuvannya pereduye navit rozvitku samih mov programuvannya Lyambda chislennya rozvinene Alonzo Cherchem i Stivenom Koulom Klini v 1930 h na dumku deyakih ye pershoyu v sviti movoyu programuvannya navit pri tomu sho vono bulo priznachene bilshe dlya obchislyuvalnih rozrahunkiv nizh zasib dlya programistiv yake opisuye algoritmi komp yuternoyi sistemi Bagato suchasnih funkcionalnih mov programuvannya legko opisuyutsya z tochki zoru lyambda chislennya Pershoyu movoyu programuvannya yaka bula vinajdena bula Plankalkyul nim obchislennya planiv yakij bula rozroblena Konradom Cuze v 1940 h ale ne bula vidoma suspilstvu do 1972 i ne bula zdijsnena do 1998 Persha shiroko vidoma i uspishna mova programuvannya Fortran 1954 1957 yaka rozroblena komandoyu doslidnikiv IBM na choli z Dzhonom Bekusom Uspih Fortranu priviv do formuvannya komitetu vchenih yaki namagalisya rozrobiti universalnu komp yuternu movu Rezultatom yih zusil buv ALGOL 58 V toj zhe chas Dzhon Makkarti iz MIT rozrobiv movu programuvannya Lisp zasnovanu na lyambda chislenni yaka ye pershoyu uspishnoyu movoyu z naukovim pohodzhennyam Z uspihom cih pochatkovih zusil movi programuvannya stali aktivnoyi temoyu doslidzhennya v 1960 h i pislya Deyaki inshi klyuchovi podiyi v istoriyi teoriyi movi programuvannya z tih pir 1950 ti Noam Chomski rozrobiv iyerarhiyu Chomski v galuzi lingvistiki Ce vidkrittya bezposeredno vplinulo na teoriyu movi programuvannya ta inshi galuzi informatiki 1960 ti Mova Simula bula rozroblena Ole Jonom Dalem i Kristenom Nyugordom Vvazhayut sho ce pershij priklad ob yektno oriyentovanoyi movi programuvannya Simula takozh vvela ponyattya spivprogrami U 1964 vpershe realizuvav lyambda chislennya Chercha sho mozhe buti vikoristanim dlya modelyuvannya mov programuvannya Vin predstavlyaye mashinu Secd yaka interpretuye lyambda virazi U 1965 roci Landin vvodit operator J yakij ye formoyu prodovzhennya U 1966 roci Landin u svoyij statti Nastupni 700 mov programuvannya prezentuvav abstraktnu komp yuternu movu programuvannya Ce malo velikij vpliv v podalshij rozrobci mov programuvannya sho vedut do Haskell U 1966 roci Korrado Bem predstaviv movu programuvannya U 1967 roci Kristofer Strejchi opublikuvav svij vazhlivij nabir konspektiv lekcij shodo osnovnih ponyat mov programuvannya vvedennya R znachennya terminologiyi L znachennya parametrichnij polimorfizm a takozh specialnij polimorfizm U 1969 roci Dzh Rodzher Gindli publikuye osnovnu tip shemu sho ce ob yekta u kombinatornij logici piznishe uzagalnenu v algoritm vivedennya tipiv Gindli Milnera U 1969 roci Toni Goar vvodit logiku Goara formu aksiomatichnoyi semantiki U 1969 roci Vilyam Elvin Govard pomitiv sho sistemu dovedennya visokogo rivnya imenovanu prirodnim vivedennyam mozhna bezposeredno interpretuvati v nadrukovanij variant modeli obchislen vidomij yak lyambda chislennya Piznishe ce otrimalo nazvu vidpovidnist Karri Govarda 1970 ti U 1970 roci Dana Skott vpershe opublikuvala svoyu robotu po denotacionnoj semantici U 1972 roci bulo rozrobleni logichne programuvannya i prolog Ce dalo mozhlivist komp yuternim programam virazhatisya cherez matematichku logiku U 1974 roci Dzhon S Rejnolds viyavlyaye sistemu F Ce bulo uzhe vinajdeno matematichnim logikom Zhan Iv Zhirarom she v 1971 roci Z 1975 roku Sassmen i Stil rozroblyayu movu programuvannya Scheme i movu Lisp yaka vklyuchaye leksichnu zonu vidimosti yedinij prostir imen i elementi z modeli Actor vklyuchayuchi prodovzhennya pershogo klasu Bakus v 1977 roci lekciyi premiyi Tyuringa rozkritikuvav potochnij stan industrialnih mov i zaproponuvav novij klas mov programuvannya V danij chas vidomi yak funkcionalno rivnevi movi programuvannya In 1977 Gordon Plotkin prezentuvav programuvannya obchislyuvalnih funkcij abstraktno nabrana mova U 1978 roci Robin Milner vvodit algoritm vivedennya tipiv Gindli Milnera dlya movi programuvannya ML Teoriya tipu stala zastosovuvatisya yak disciplina mov programuvannya cej dodatok priviv do velicheznih dosyagnen v oblasti teoriyi tipu protyagom bagatoh rokiv 1980 ti U 1981 Gordon Plotkin opublikuvav svij dokument na strukturovanij operacijnij semantici U 1988 roci Zhil Kan opublikuvav svoyu stattyu pro normalnu semantiku Komanda vchenih Xerox PARC pid kerivnictvom Alana Keya rozrobili Smalltalk ob yektno oriyentovana movu yaka shiroko vidoma svoyim innovacijnim rozrobnickim seredovishem Tam z yavilisya obrobki obchislen obrahunok vzayemodiyuchih sistem Robina Milnera model komunikativnih poslidovnih procesiv Toni Goara a takozh analogichni modeli paralelizmu napriklad model Actor Karla Hyuitta U 1985 vipusk Miranda zapalyuye navchalnij interes do ranishe vidkladenih chistih funkcionalnih mov programuvannya Buv stvorenij komitet dlya viznachennya vidkritogo standartu sho prizviv do vipusku Haskell 1 0 v 1990 roci Bertran Mejer stvoriv metodologiyu proyektuvannya za dogovorom ta vklyuchiv yiyi v movu programuvannya Eiffel 1990 ti Gregor Kizales Dzhim De Riv yer i Daniel G Bobrov opublikuvali knigu Yevgenio Modzhi i Filip Vadler vveli vikoristannya monad dlya strukturuvannya program napisanih na funkcionalnih movah programuvannya Subdisciplini i sumizhni oblastiYe kilka oblastej doslidzhennya yaki abo lezhat v teoriyi movi programuvannya abo yaki nadayut velikij vpliv na neyi bagato z nih mayut vazhlive znachennya Krim togo PLT vikoristovuye bagato inshih oblastej matematiki vklyuchayuchi teoriyu obchislyuvanosti teoriyu kategorij i teoriyu mnozhin Formalna semantika Formalna semantika ce formalnij opis povedinki komp yuternih program i mov programuvannya Tri zagalnih pidhodi do opisu semantiki abo sens komp yuternoyi programi denotacijna semantika operacijna semantika i aksiomatichna semantika Teoriya tipiv Teoriya tipiv ce vivchennya tipovih sistemi yaka ye sluhnyanim sintaksichnim metodom dokazu nedostatnosti povedinki konkretnoyi programi shlyahom klasifikaciyi fraz za vidami znachen yaki voni obchislyuyut Bagato mov programuvannya vidriznyayutsya harakteristikami yih sistem tipiv Analiz programi ta transformaciya Analiz programi ce zagalna problema vivchennya programi i viznachennya klyuchovih harakteristik napriklad vidsutnist pomilok u programi Peretvorennya programi ce proces peretvorennya programi z odniyeyi formi movi v inshu formu Porivnyalnij analiz movi programuvannya Porivnyalnogo analizu movi programuvannya pragne klasifikuvati movi programuvannya na rizni tipi zalezhno vid yih harakteristik Zagalni kategoriyi mov programuvannya chasto nazivayut paradigmami programuvannya Zagalne i metaprogramuvannya Metaprogramuvannya generaciya program vishogo poryadku yaki koli vikonuyutsya porodzhuyut programi mozhlivo na inshij movi abo v pidmnozhini pochatkovogo movi yak rezultat svoyeyi roboti Predmetno oriyentovani movi Predmetno oriyentovani movi movi pobudovani dlya efektivnogo virishennya zavdan v konkretnij predmetnij oblasti Tlumachennya kompilyatora Teoriya kompilyatora ce teoriya napisannya kompilyatoriv abo v bilsh zagalnomu plani translyatoriv Ce programi yaki perevodyat programu napisanu odniyeyu movoyu v inshu formu Diyi kompilyatora tradicijno rozbiti na sintaksichnij analiz skanuvannya i sintaksichnij analiz semantichnij analiz viznachennya togo sho programa povinna robiti optimizaciyu pidvishennya produktivnosti programi sho zaznacheno v deyakij metrici yak pravilo shvidkist vikonannya i generaciyi kodu generaciya i visnovok ekvivalentnoyi programi v tij chi inshij movi perekladu chasto nabir instrukcij procesora Sistemi vikonannya Sistemi vikonannya nalezhat do rozrobki seredovish vikonannya movi programuvannya ta yih komponentiv vklyuchayuchi virtualni mashini zbirku smittya i zovnishni funkcionalni interfejsi Zhurnali publikaciyi ta konferenciyiKonferenciyi ye osnovnim miscem dlya prezentuvannya doslidzhen v movah programuvannya Najbilsh vidomi konferenciyi vklyuchayut ce Simpozium pro principi mov programuvannya POPL Symposium on Principles of Programming Languages Konferenciya pro proyektuvannya ta vprovadzhennya mov programuvannya PLDI Conference on Programming Language Design and Implementation mizhnarodna konferenciya funkcionalnogo programuvannya ICFP International Conference on Functional Programming ta mizhnarodna konferenciya obyektno oriyentovanogo programuvannya sistem mov ta dodatkiv OOPSLA the International Conference on Object Oriented Programming Systems Languages and Applications Vidomi zhurnali yaki publikuyut 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 Primitkihttp www c2 com cgi wiki ModelsOfComputation 9 lipnya 2016 u Wayback Machine PosilannyaLambda the Ultimate 20 kvitnya 2016 u Wayback Machine a community weblog for professional discussion and repository of documents on programming language theory Great Works in Programming Languages 2 kvitnya 2016 u Wayback Machine Collected by Benjamin C Pierce University of Pennsylvania Classic Papers in Programming Languages and Logic 11 travnya 2016 u Wayback Machine Collected by Karl Crary Carnegie Mellon University Programming Language Research 21 kvitnya 2016 u Wayback Machine Directory by Mark Leone Programming Language Theory Texts Online 2 zhovtnya 2014 u Wayback Machine At Utrecht University l Calculus Then amp Now 2 lipnya 2021 u Wayback Machine by Dana S Scott for the ACM Turing Centenary Celebration Grand Challenges in Programming Languages 6 bereznya 2016 u Wayback Machine Panel session at POPL 2009 Cya stattya potrebuye dodatkovih posilan na dzherela dlya polipshennya yiyi perevirnosti Bud laska dopomozhit udoskonaliti cyu stattyu dodavshi posilannya na nadijni avtoritetni dzherela Zvernitsya na storinku obgovorennya za poyasnennyami ta dopomozhit vipraviti nedoliki Material bez dzherel mozhe buti piddano sumnivu ta vilucheno berezen 2017 Ce nezavershena stattya pro movi programuvannya Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi