Teorie programovacích jazyků (PLT ) je část informatiky věnovaná návrhu, analýze, charakterizaci a klasifikaci programovacích jazyků a studiu jejich jednotlivých vlastností [1] . Výsledky teorie jsou úzce spjaty s ostatními obory informatiky a jsou využívány v matematice , softwarovém inženýrství a lingvistice .
V jistém smyslu historie teorie programovacích jazyků předchází dokonce i vývoj samotných programovacích jazyků. Zejména λ-kalkulus , který vyvinuli Alonzo Church a Stephen Kleene ve 30. letech 20. století, je vlastně prvním programovacím jazykem, i když byl určen spíše pro teoretické otázky vyčíslitelnosti než jako nástroj pro programátory; mnoho moderních funkcionálních programovacích jazyků je variantami λ-kalkulu. Další historie teorie je úzce provázána s historií programovacích jazyků , přičemž v rámci teoretického výzkumu vznikala nová paradigmata , konstrukce a metody a výsledky jejich implementace v praktických programovacích jazycích poskytly zpětnou vazbu pro vývoj teorie.
Prvním programovacím jazykem, který byl vynalezen pro použití v existujícím elektronickém počítači, je Plankalkul Konrada Zuse , ale mezi současníky si nezískal slávu (byl studován až v 70. letech a implementován v 90. letech). První široce známý a úspěšný programovací jazyk byl Fortran (1954-1957), vyvinutý týmem výzkumníků IBM pod vedením Johna Backuse . Úspěch Fortranu vedl k vytvoření výboru vědců, kteří se pokusili vyvinout „univerzální“ počítačový jazyk; výsledkem jejich snažení byl Algol-58 . Souběžně s tím John McCarthy z MIT vyvinul programovací jazyk Lisp (založený na λ-kalkulu), který je prvním úspěšným jazykem s akademicky vyvinutým teoretickým rámcem. Padesátá léta zahrnují vývoj Chomského hierarchie , která přímo ovlivnila teorii programovacích jazyků.
V roce 1964 Peter Landin poprvé implementoval variantu λ-kalkulu, kterou bylo možné použít k modelování programovacích jazyků ( stroj SECD a J-operátor , v podstatě typ pokračování ). V roce 1966 Landin vyvinul abstraktní programovací jazyk ISWIM .
V roce 1966 Corrado Böhm a Giuseppe Jacopini ( Ital Giuseppe Jackopini ) dokázali větu , podle níž lze algoritmus převést do formy, která využívá pouze tři řídicí struktury - sekvenční, větvení a smyčku, později se tento výsledek stal teoretickým základem strukturovaného programování . Jazyk Simula , který vytvořili Ole-Johan Dahl a Kristen Nygor v roce 1967, vyvinul to, co je považováno za první příklad objektově orientovaného programovacího jazyka , a zavedl pojem coroutine . Důležitým mezníkem ve vývoji směru byl přednáškový kurz Fundamental Concepts in Programming Languages od Christophera Stracheyho vydaný v roce 1967 , kde se kromě systematizace znalostí o teorii programovacích jazyků objevil koncept polymorfismu . hluboce studoval . Významný příspěvek k rozvoji konceptu typů v programovacích jazycích je spojen s prací Rogera Hindleyho z roku 1969 , jejíž výsledky vedly ke zobecněnému algoritmu odvození typu .
V roce 1969 Tony Hoare vyvinul Hoareovu logiku , první příklad axiomatické sémantiky pro programovací jazyky, který poskytuje formální ověření programového kódu. Denotační sémantiku vyvinula v roce 1970 Dana Scottová .
V roce 1972 bylo vytvořeno logické programovací paradigma a jazyk Prolog , ve kterém se program skládá přímo ze sady Hornových klauzulí . Další oblastí zájmu teoretiků programovacích jazyků na počátku 70. let bylo zavedení abstraktních datových typů na úrovni jazykových konstruktů, přičemž za první takový jazyk byl považován Clu (1974, Barbara Liskov ) .
Důležitým mezníkem na cestě k utváření paradigmatu funkcionálního programování byl nezávislý vývoj Girarda ( fr. Jean-Yves Girard ; 1971) a Reynoldse ( eng. John C. Reynolds ; 1974) systému F - typizovaného λ -kalkul druhého řádu, který poskytuje schopnost konstruovat termíny, které závisí na z typů. K rozvoji funkcionálního programování v polovině 70. let významně přispěli také vývojáři programovacího jazyka Scheme , dialektu Lisp , který zahrnoval lexikální rozsah , jednotný jmenný prostor a prvky z modelu aktéra , včetně pokračování . Vzestup širokého zájmu o funkcionální programování je spojen s Turingovou přednáškou tvůrce Fortran Backus v roce 1977, ve které kriticky analyzoval stav programovacích jazyků, které byly v té době populární a dospěly k funkčnímu paradigmatu.
V roce 1980 William Alvin Howard s odkazem na spisy logika Haskella Curryho z 50. let identifikoval strukturální shodu mezi počítačovými programy a matematickými důkazy, která se stala známou jako Curry-Howardův izomorfismus a stala se teoretickým základem třídy automatických důkazové jazyky .
V první polovině 80. let byla značná pozornost věnována výzkumu implementace paralelismu v programovacích jazycích a vývoji variant procesního kalkulu : vznikl kalkul interagujících systémů ( Milner , 1980), jazyk interagujících sekvenční procesy ( Hoare , 1985), byl nakonec zformován Hewittův model herce ( eng. ) Carl Hewitt
Vydání jazyka Miranda v roce 1985 podnítilo akademický zájem o líné čisté funkcionální programovací jazyky , což vedlo k vytvoření výboru, který definoval otevřený standard pro takový jazyk, což v roce 1990 vyústilo ve verzi Haskell 1.0 .
V roce 1986 bylo v rámci práce na vytvoření jazyka Eiffel vytvořeno paradigma smluvního programování ( Bertrand Meyer , 1986).
Teorie studuje aspekty programovacích jazyků, pokud je to možné, jako množinu, s použitím jednoho nebo druhého konkrétního jazyka jako příkladu, ale zároveň s využitím prostředků dostatečně vysoké úrovně obecnosti, aby výsledky mohly být aplikovány na nějakou třídu jazyky. Často se v teoretickém vývoji vytváří nějaký specializovaný, „ akademický “ programovací jazyk, který z toho či onoho důvodu není vhodný pro praktickou implementaci, ale vykazuje určité teoretické výsledky, které jsou následně aplikovány na jazyky používané v průmysl. Pro teoretický výzkum se používají nástroje základů matematiky a matematické logiky , včetně teorie množin , teorie modelů , teorie vyčíslitelnosti , ale i takové abstraktní úseky jako teorie kategorií , univerzální algebra , teorie grafů a výrazně závisí na výsledcích aplikované oblasti, včetně teorie složitosti, výpočetní technika , teorie kódování .
Formální sémantika je takový formální popis programovacích jazyků, který umožňuje matematicky interpretovat „význam“ počítačového programu napsaného v tomto jazyce. Existují tři obecné přístupy k popisu sémantiky programovacího jazyka: denotační sémantika , operační sémantika a axiomatická sémantika .
Teorie typů je studium typových systémů ; je „poslušná syntaktická metoda pro dokazování chyb v chování konkrétního programu klasifikací frází podle úrovně hodnot, které počítají“ [2] . Mnoho programovacích jazyků se liší ve vlastnostech svých typových systémů.
Analýza programu je obecný problém zkoumání programu a stanovení hlavních charakteristik (jako je absence chyb v programu).
Převod programu je proces převodu programu z jedné formy (jazyka) do jiné formy.
Srovnávací analýza programovacích jazyků se snaží klasifikovat programovací jazyky do různých typů v závislosti na jejich vlastnostech; obecné myšlenky a koncepty programovacích jazyků jsou známé jako programovací paradigmata .
Generické programování je programovací paradigma , které spočívá v takovém popisu dat a algoritmů , které lze aplikovat na různé typy dat, aniž by se tento popis samotný měnil.
Metaprogramování je generování programů vyššího řádu, které po provedení vytvářejí programy (možná v jiném jazyce nebo podmnožině původního jazyka) jako výsledek své práce.
Jazyky specifické pro doménu jsou jazyky, které jsou navrženy tak, aby efektivně řešily problémy v konkrétní oblasti.
Teorie kompilátoru je teorie psaní kompilátorů (nebo obecněji překladatelů); programy, které překládají program napsaný v jednom jazyce do jiné formy.
Akce kompilátoru se tradičně dělí na:
Běhové systémy označují vývoj běhových modulů programovacího jazyka a jejich komponent, včetně virtuálních strojů , garbage collection a externích funkčních rozhraní