Teoria języka programowania - Programming language theory
Teoria języka programowania ( PLT ) to dział informatyki, który zajmuje się projektowaniem, implementacją, analizą, charakteryzacją i klasyfikacją języków formalnych znanych jako języki programowania oraz ich indywidualnych cech . Należy do dyscypliny informatyki, zarówno zależnej, jak i mającej wpływ na matematykę , inżynierię oprogramowania , językoznawstwo, a nawet kognitywistykę . Stała się uznaną gałęzią informatyki i aktywnym obszarem badawczym, a jej wyniki publikowane są w licznych czasopismach poświęconych PLT, a także w publikacjach z zakresu informatyki ogólnej i inżynierskiej.
Historia
Pod pewnymi względami historia teorii języków programowania wyprzedza nawet rozwój samych języków programowania. Rachunek lambda , opracowany przez Alonzo Church i Stephen Cole Kleene w 1930 roku, jest uważany przez niektórych za pierwszy na świecie język programowania, mimo że był przeznaczony do modelu obliczeń zamiast być środkiem dla programistów do opisania algorytmów do systemu komputerowego . Wiele nowoczesnych języków programowania funkcjonalnego zostało opisanych jako „cienkie okleiny” nad rachunkiem lambda, a wiele z nich można łatwo opisać w tym zakresie.
Pierwszym wynalezionym językiem programowania był Plankalkül , który został zaprojektowany przez Konrada Zuse w latach 40. XX wieku, ale nie był znany publicznie do 1972 (i nie został zaimplementowany do 1998). Pierwszym powszechnie znanym i odnoszącym sukcesy językiem programowania wysokiego poziomu był Fortran , opracowany w latach 1954-1957 przez zespół naukowców IBM kierowany przez Johna Backusa . Sukces FORTRAN doprowadził do powstania komitetu naukowców, którzy stworzyli „uniwersalny” język komputerowy; rezultatem ich wysiłków był ALGOL 58 . Osobno John McCarthy z MIT opracował Lisp , pierwszy język wywodzący się ze środowiska akademickiego, który odniósł sukces. Wraz z sukcesem tych początkowych wysiłków języki programowania stały się aktywnym tematem badań w latach 60. i później.
Kilka innych kluczowych wydarzeń w historii teorii języka programowania od tego czasu:
1950
- Noam Chomsky opracował hierarchię Chomsky'ego w dziedzinie językoznawstwa, odkrycie, które bezpośrednio wpłynęło na teorię języka programowania i inne gałęzie informatyki.
1960 1960
- Język Simula został opracowany przez Ole-Johana Dahla i Kristen Nygaard ; jest powszechnie uważany za pierwszy przykład języka programowania obiektowego ; Simula wprowadziła także pojęcie współprogramów .
- W 1964 roku Peter Landin jako pierwszy zdał sobie sprawę, że rachunek lambda Church'a może być używany do modelowania języków programowania. Przedstawia maszynę SECD, która "interpretuje" wyrażenia lambda.
- W 1965 Landin wprowadza operator J , zasadniczo formę kontynuacji .
- W 1966 Landin wprowadza ISWIM , abstrakcyjny język programowania komputerowego w swoim artykule The Next 700 Programming Languages . Ma wpływ na projektowanie języków prowadzących do języka programowania Haskell .
- W 1966 roku Corrado Böhm wprowadził język programowania CUCH (Curry-Church).
- W 1967 roku Christopher Strachey publikuje jego wpływowy zestaw wykład zauważa podstawowych pojęć w Języki programowania , wprowadzenie terminologii wartości R , L-wartości , polimorfizmu parametrycznego oraz polimorfizmu ad hoc .
- W 1969 J. Roger Hindley publikuje The Principal Type-Scheme of a Object in Combinatory Logic , później uogólniony na algorytm wnioskowania o typie Hindleya-Milnera .
- W 1969 Tony Hoare wprowadza logikę Hoare'a , formę semantyki aksjomatycznej .
- W 1969 William Alvin Howard zauważył, że „wysoki poziom” systemu dowodowego , określany jako naturalna dedukcja , może być bezpośrednio interpretowany w swojej intuicjonistycznej wersji jako typizowany wariant modelu obliczeniowego znanego jako rachunek lambda . Stało się to znane jako korespondencja Curry-Howard .
lata 70.
- W 1970 roku Dana Scott po raz pierwszy publikuje swoją pracę na temat semantyki denotacyjnej .
- W 1972 r. opracowano programowanie logiczne i Prolog , dzięki czemu programy komputerowe można wyrazić jako logikę matematyczną.
- Zespół naukowców z Xerox PARC pod kierownictwem Alana Kay opracowuje Smalltalk , język zorientowany obiektowo, powszechnie znany z innowacyjnego środowiska programistycznego.
- W 1974 roku John C. Reynolds odkrywa systemu F . Została odkryta już w 1971 roku przez matematycznego logika Jean-Yvesa Girarda .
- Od 1975 roku Gerald Jay Sussman i Guy Steele opracowują język programowania Scheme , dialekt Lisp zawierający zakres leksykalny , ujednoliconą przestrzeń nazw i elementy modelu aktorskiego, w tym pierwszorzędne kontynuacje .
- Backus, na wykładzie Turing Award 1977 , zaatakował obecny stan języków przemysłowych i zaproponował nową klasę języków programowania, znanych obecnie jako języki programowania na poziomie funkcji .
- W 1977 roku Gordon Plotkin wprowadza programowanie funkcji obliczeniowych (Programming Computable Functions ) — abstrakcyjny, typizowany język funkcjonalny.
- W 1978 Robin Milner wprowadza algorytm wnioskowania typu Hindley-Milner dla ML . Teoria typów została zastosowana jako dyscyplina w językach programowania, ta aplikacja doprowadziła na przestrzeni lat do ogromnych postępów w teorii typów.
lata 80
- W 1981 roku Gordon Plotkin publikuje artykuł na temat ustrukturyzowanej semantyki operacyjnej .
- W 1988 roku Gilles Kahn opublikował swoją pracę na temat semantyki naturalnej .
- Pojawiła kamicy proces , takich jak Rachunek komunikowania Systems o Robin Milner , a Communicating Sequential Processes model CAR Hoare , a także podobnych modeli współbieżności takich jak modelu aktora z Carl Hewitt .
- W 1985 r. wydanie Mirandy wywołało zainteresowanie akademickie leniwie ocenianymi czysto funkcjonalnymi językami programowania. Powołano komisję w celu zdefiniowania otwartego standardu, co zaowocowało wydaniem standardu Haskell 1.0 w 1990 roku.
- Bertrand Meyer stworzył metodologię Design by contract i włączył ją do języka programowania Eiffel .
1990
- Gregor Kiczales , Jim Des Rivieres i Daniel G. Bobrow opublikowali książkę The Art of the Metaobject Protocol .
- Eugenio Moggi i Philip Wadler wprowadzili zastosowanie monad do strukturyzacji programów napisanych w funkcjonalnych językach programowania .
Istnieje kilka dziedzin nauki, które albo leżą w teorii języka programowania, albo mają na nią głęboki wpływ; wiele z nich w znacznym stopniu się pokrywa. Ponadto, PLT korzysta z wielu innych dziedzin matematyki , w tym teoria obliczalności , teorii kategorii i teorii mnogości .
Semantyka formalna
Semantyka formalna to formalna specyfikacja zachowania programów komputerowych i języków programowania. Trzy wspólne podejścia do opisu semantyki lub „sens” programu komputerowego są denotational semantyki , semantyka operacyjne i aksjomatyczne semantyka .
Teoria typów
Teoria typów to nauka o systemach typów ; które są „praktyczną metodą składniową do udowadniania braku pewnych zachowań programu poprzez klasyfikację fraz według rodzajów wartości, które obliczają”. Wiele języków programowania wyróżnia się charakterystyką ich systemów typów.
Analiza i transformacja programu
Analiza programu to ogólny problem badania programu i określenia kluczowych cech (takich jak brak klas błędów programu ). Transformacja programu to proces przekształcania programu w jednej formie (języku) w inną formę.
Analiza porównawcza języka programowania
Analiza porównawcza języków programowania ma na celu klasyfikację języków programowania na różne typy na podstawie ich cech; szerokie kategorie języków programowania są często znane jako paradygmaty programowania .
Ogólne i metaprogramowanie
Metaprogramowanie to generowanie programów wyższego rzędu, które po uruchomieniu wytwarzają w rezultacie programy (prawdopodobnie w innym języku lub w podzbiorze języka oryginalnego).
Języki specyficzne dla domeny
Języki specyficzne dla domeny to języki skonstruowane w celu efektywnego rozwiązywania problemów określonej części domeny.
Budowa kompilatora
Teoria kompilatorów to teoria pisania kompilatorów (lub bardziej ogólnie tłumaczy ); programy, które tłumaczą program napisany w jednym języku na inną formę. Działania kompilatora są tradycyjnie podzielone na analizę składni ( skanowanie i parsowanie ), analizę semantyczną (określanie, co program powinien zrobić), optymalizację (poprawianie wydajności programu zgodnie z pewną metryką; zazwyczaj szybkość wykonywania) i generowanie kodu (generowanie i wyjście równoważnego programu w jakimś języku docelowym; często zestaw instrukcji procesora).
Systemy uruchomieniowe
Systemy uruchomieniowe odnoszą się do rozwoju środowisk wykonawczych języka programowania i ich komponentów, w tym maszyn wirtualnych , garbage collection i interfejsów funkcji obcych .
Czasopisma, publikacje i konferencje
Konferencje są głównym miejscem prezentacji badań w językach programowania. Najbardziej znane konferencji obejmować Sympozjum na temat zasad programowania Języki (popl), język programowania projektowania i wdrażania (PLDI), na Międzynarodowej Konferencji na temat Programowanie funkcyjne (ICFP), Międzynarodowa Konferencja na temat programowania obiektowego, systemów, języków i programów komputerowych ( OOPSLA) i Międzynarodowa Konferencja na temat architektury, za Języki programowania i systemy operacyjne (ASPLOS) .
Znane czasopisma publikujące badania PLT obejmują ACM Transactions on Programming Languages and Systems (TOPLAS), Journal of Functional Programming (JFP), Journal of Functional and Logic Programming oraz Higher-Order and Symbolic Computation .
Zobacz też
Bibliografia
Dalsza lektura
- Abadi, Martín i Cardelli, Luca . Teoria przedmiotów . Springer-Verlag.
- Michaela JC Gordona . Teoria języka programowania i jej implementacja . Sala Prezydencka.
- Gunter, Carl i Mitchell, John C. (red.). Teoretyczne aspekty języków programowania obiektowego: typy, semantyka i projektowanie języka . MIT Naciśnij.
- Harper, Robert . Praktyczne podstawy języków programowania . Wersja robocza.
- Knutha, Donalda E. (2003). Wybrane artykuły na temat języków komputerowych . Stanford, Kalifornia: Centrum Studiów Językowych i Informacji.
- Mitchell, John C. . Podstawy języków programowania .
- Mitchell, John C. . Wprowadzenie do teorii języka programowania .
- Słuchaj, Piotrze. W. i Tennent, Robercie. D. (1997). Języki podobne do algorytmów . Postęp w informatyce teoretycznej. Birkhauser, Boston.
- Pierce, Benjamin C. (2002). Typy i języki programowania . MIT Naciśnij.
- Pierce, Benjamin C. Zaawansowane tematy w typach i językach programowania .
- Pierce, Benjamin C. i in. (2010). Podstawy oprogramowania .
Linki zewnętrzne
- Lambda the Ultimate , blog społecznościowy do profesjonalnej dyskusji i repozytorium dokumentów dotyczących teorii języka programowania.
- Wielkie dzieła w językach programowania . Zebrane przez Benjamina C. Pierce'a ( Uniwersytet Pensylwanii ).
- Klasyczne artykuły w językach programowania i logice . Zebrane przez Karla Crary'ego ( Uniwersytet Carnegie Mellon ).
- Badania języka programowania . Katalog autorstwa Marka Leone .
- Teoria Języka Programowania Teksty Online . Na Uniwersytecie w Utrechcie .
- Rachunek λ: Wtedy i teraz autorstwa Dany S. Scott na obchody stulecia ACM Turinga
- Wielkie wyzwania w językach programowania . Sesja panelowa na POPL 2009.