Programmeringssprogsteori (PLT ) er en sektion af datalogi , der er viet til design, analyse, karakterisering og klassificering af programmeringssprog og studiet af deres individuelle funktioner [1] . Nært beslægtet med andre grene af datalogi, er resultaterne af teorien brugt i matematik , i software engineering og lingvistik .
På en måde går historien om programmeringssprogsteori før selv udviklingen af programmeringssprog. Især λ-regningen , udviklet af Alonzo Church og Stephen Kleene i 1930'erne, er faktisk det første programmeringssprog, selvom det mere var beregnet til teoretiske spørgsmål om beregnelighed end som et værktøj for programmører; mange moderne funktionelle programmeringssprog er varianter af λ-regningen. Teoriens videre historie er tæt sammenvævet med programmeringssprogenes historie , mens der inden for rammerne af teoretisk forskning blev skabt nye paradigmer , konstruktioner og metoder, og resultaterne af deres implementering i praktiske programmeringssprog gav feedback til udvikling af teori.
Det første programmeringssprog, der blev opfundet til brug i en eksisterende elektronisk computer, er Konrad Zuses Plankalkul , men vandt ikke berømmelse blandt samtidige (det blev først studeret i 1970'erne og implementeret i 1990'erne). Det første almindeligt kendte og succesrige programmeringssprog var Fortran (1954-1957), udviklet af et team af IBM -forskere ledet af John Backus . Fortrans succes førte til dannelsen af et udvalg af videnskabsmænd, som forsøgte at udvikle et "universelt" computersprog; resultatet af deres indsats var Algol-58 . Sideløbende udviklede John McCarthy fra MIT programmeringssproget Lisp (baseret på λ-calculus), som er det første succesfulde sprog med en akademisk udviklet teoretisk ramme. 1950'erne omfatter udviklingen af Chomsky-hierarkiet , som direkte påvirkede teorien om programmeringssprog.
I 1964 implementerede Peter Landin først en variant af λ-regningen, der kunne bruges til at modellere programmeringssprog ( SECD-maskinen og J-operatøren , i det væsentlige en form for fortsættelse ). I 1966 udviklede Landin det abstrakte programmeringssprog ISWIM .
I 1966 beviste Corrado Böhm og Giuseppe Jacopini ( italiensk Giuseppe Jackopini ) en sætning , ifølge hvilken en algoritme kan konverteres til en form, der kun bruger tre kontrolstrukturer - sekventiel, forgrening og loop, senere blev dette resultat det teoretiske grundlag for struktureret programmering . Simula -sproget blev skabt af Ole-Johan Dahl og Kristen Nygor i 1967 og udviklede, hvad der menes at være det første eksempel på et objektorienteret programmeringssprog og introducerede begrebet en koroutin . En vigtig milepæl i udviklingen af retningen var forelæsningskurset Fundamental Concepts in Programming Languages af Christopher Strachey , udgivet i 1967 , hvor begrebet polymorfi ud over at systematisere viden om teorien om programmeringssprog var dybt studeret . Et væsentligt bidrag til udviklingen af begrebet typer i programmeringssprog er forbundet med arbejdet fra 1969 af Roger Hindley , hvis resultater resulterede i en generaliseret type-inferensalgoritme .
I 1969 udviklede Tony Hoare Hoares logik , det første eksempel på aksiomatisk semantik for programmeringssprog, der giver formel verifikation af programkode. Denotationel semantik blev udviklet i 1970 af Dana Scott .
I 1972 blev det logiske programmeringsparadigme og Prolog -sproget skabt , hvor programmet består direkte af et sæt Horn-klausuler . Et andet interesseområde for programmeringssprogsteoretikere i de tidlige 1970'ere var introduktionen af abstrakte datatyper på niveau med sprogkonstruktioner, hvor Clu (1974, Barbara Liskov ) blev anset for at være det første sådanne sprog .
En vigtig milepæl på vejen til dannelsen af det funktionelle programmeringsparadigme var udviklingen uafhængigt af Girard ( fr. Jean-Yves Girard ; 1971) og Reynolds ( eng. John C. Reynolds ; 1974) af systemet F - en typet λ -calculus af anden orden, som giver mulighed for at konstruere udtryk, der afhænger af fra typer. Et væsentligt bidrag til udviklingen af funktionel programmering i midten af 1970'erne blev ydet af udviklerne af programmeringssproget Scheme , en Lisp - dialekt , der inkluderede leksikalsk omfang , et samlet navneområde og elementer fra skuespillermodellen , inklusive fortsættelser . Stigningen i den udbredte interesse for funktionel programmering er forbundet med Turing-foredraget af skaberen af Fortran Backus i 1977, hvor han kritisk analyserede tilstanden for de programmeringssprog, der var populære på det tidspunkt og kom til det funktionelle paradigme.
I 1980 identificerede William Alvin Howard , med henvisning til logikeren Haskell Currys skrifter i 1950'erne, en strukturel overensstemmelse mellem computerprogrammer og matematiske beviser, som blev kendt som Curry-Howard isomorfismen og blev det teoretiske grundlag for klassen af automatisk bevis sprog .
I første halvdel af 1980'erne blev der rettet betydelig opmærksomhed mod forskning i implementeringen af parallelisme i programmeringssprog og udviklingen af varianter af procesregning : beregningen af interagerende systemer blev skabt ( Milner , 1980), sproget for at interagere sekventielle processer ( Hoare , 1985), blev Hewitt- skuespillermodellen endelig dannet ( eng. ) Carl Hewitt
Frigivelsen af Miranda -sproget i 1985 gav næring til den akademiske interesse for dovne rene funktionelle programmeringssprog , hvilket resulterede i, at en komité blev dannet til at definere en åben standard for et sådant sprog, hvilket resulterede i Haskell version 1.0 i 1990 .
I 1986, som en del af arbejdet med at skabe Eiffel -sproget, blev kontraktprogrammeringsparadigmet skabt ( Bertrand Meyer , 1986).
Teori studerer aspekter af programmeringssprog, så vidt muligt, som et sæt, ved at bruge et eller andet bestemt sprog som eksempel, men samtidig bruge midler af et tilstrækkeligt højt niveau af generalitet til, at resultaterne kan anvendes på en eller anden klasse af Sprog. I teoretiske udviklinger skabes ofte et specialiseret, " akademisk " programmeringssprog, som af den ene eller anden grund ikke er egnet til praktisk implementering, men viser visse teoretiske resultater, som efterfølgende anvendes på de sprog, der bruges i industri. Til teoretisk forskning anvendes værktøjerne fra matematikkens og den matematiske logiks grundlag , herunder mængdeteori , modelteori , beregningsbarhedsteori , såvel som sådanne abstrakte afsnit som kategoriteori , universel algebra , grafteori , og afhænger væsentligt af resultaterne af anvendte områder, herunder kompleksitetsteori computing , kodningsteori .
Formel semantik er sådan en formel beskrivelse af programmeringssprog, der tillader en matematisk at fortolke "betydningen" af et computerprogram skrevet på det sprog. Der er tre generelle tilgange til at beskrive semantikken i et programmeringssprog: denotationel semantik , operationel semantik og aksiomatisk semantik .
Typeteori er studiet af typesystemer ; er "en lydig syntaktisk metode til at bevise fejl i et bestemt programs adfærd ved at klassificere sætninger efter niveauet af værdier, de beregner" [2] . Mange programmeringssprog adskiller sig i egenskaberne af deres typesystemer.
Programanalyse er det generelle problem med at undersøge et program og bestemme de vigtigste karakteristika (såsom fraværet af fejl i programmet).
Programkonvertering er processen med at konvertere et program fra én form (sprog) til en anden form.
Komparativ programmeringssproganalyse søger at klassificere programmeringssprog i forskellige typer, afhængigt af deres egenskaber; de generelle ideer og koncepter for programmeringssprog er kendt som programmeringsparadigmer .
Generisk programmering er et programmeringsparadigme , der består i en sådan beskrivelse af data og algoritmer , der kan anvendes på forskellige typer data uden at ændre denne beskrivelse i sig selv.
Metaprogrammering er genereringen af programmer af højere orden, der, når de udføres, producerer programmer (måske på et andet sprog eller en delmængde af originalsproget) som et resultat af deres arbejde.
Domænespecifikke sprog er sprog, der er designet til effektivt at løse problemer inden for et bestemt fagområde.
Kompilerteori er teorien om at skrive kompilatorer (eller mere generelt oversættere); programmer, der oversætter et program skrevet på ét sprog til en anden form.
Compilerhandlinger er traditionelt opdelt i:
Runtime-systemer refererer til udviklingen af programmeringssprog-runtimes og deres komponenter, herunder virtuelle maskiner , garbage collection og eksterne funktionelle grænseflader