Programmeringsspråksteori (PLT ) är en del av datavetenskap som ägnas åt design, analys, karakterisering och klassificering av programmeringsspråk och studiet av deras individuella egenskaper [1] . Nära besläktade med andra grenar av datavetenskap, resultaten av teorin används i matematik , i mjukvaruteknik och lingvistik .
På sätt och vis föregår programmeringsspråksteorins historia till och med utvecklingen av själva programmeringsspråken. I synnerhet är λ-kalkylen , utvecklad av Alonzo Church och Stephen Kleene på 1930-talet, faktiskt det första programmeringsspråket, även om det var avsett mer för teoretiska frågor om beräkningsbarhet än som ett verktyg för programmerare; många moderna funktionella programmeringsspråk är varianter av λ-kalkylen. Teorins vidare historia är nära sammanflätad med programmeringsspråkens historia , medan inom ramen för teoretisk forskning skapades nya paradigm , konstruktioner och metoder, och resultaten av deras implementering i praktiska programmeringsspråk gav feedback för utvecklingen av teori.
Det första programmeringsspråket som uppfanns för användning i en befintlig elektronisk dator är Konrad Zuses Plankalkul , men blev inte känt bland samtida (det studerades först på 1970-talet och implementerades på 1990-talet). Det första allmänt kända och framgångsrika programmeringsspråket var Fortran (1954-1957), utvecklat av ett team av IBM -forskare under ledning av John Backus . Framgången med Fortran ledde till bildandet av en kommitté av vetenskapsmän som försökte utveckla ett "universellt" datorspråk; resultatet av deras ansträngning var Algol-58 . Parallellt utvecklade John McCarthy från MIT programmeringsspråket Lisp (baserat på λ-kalkyl), vilket är det första framgångsrika språket med en akademiskt utvecklad teoretisk ram. 1950-talet inkluderar utvecklingen av Chomsky-hierarkin , som direkt påverkade teorin om programmeringsspråk.
1964 implementerade Peter Landin först en variant av λ-kalkylen som kunde användas för att modellera programmeringsspråk ( SECD-maskinen och J-operatören , i huvudsak en typ av fortsättning ). 1966 utvecklade Landin det abstrakta programmeringsspråket ISWIM .
1966 bevisade Corrado Böhm och Giuseppe Jacopini ( italienska Giuseppe Jackopini ) ett teorem , enligt vilket en algoritm kan konverteras till en form som endast använder tre kontrollstrukturer - sekventiell, förgrening och loop, senare blev detta resultat den teoretiska grunden för strukturerad programmering . Simula -språket skapades av Ole-Johan Dahl och Kristen Nygor 1967 och utvecklade vad som tros vara det första exemplet på ett objektorienterat programmeringsspråk och introducerade begreppet en koroutin . En viktig milstolpe i utvecklingen av riktningen var föreläsningskursen Fundamental Concepts in Programming Languages av Christopher Strachey , släppt 1967 , där, förutom att systematisera kunskap om teorin om programmeringsspråk, begreppet polymorfism var djupt studerad . Ett betydande bidrag till utvecklingen av begreppet typer i programmeringsspråk är förknippat med arbetet från 1969 av Roger Hindley , vars resultat resulterade i en generaliserad typinferensalgoritm .
1969 utvecklade Tony Hoare Hoares logik , det första exemplet på axiomatisk semantik för programmeringsspråk som ger formell verifiering av programkod. Denotationssemantik utvecklades 1970 av Dana Scott .
1972 skapades det logiska programmeringsparadigmet och Prolog- språket , där programmet består direkt av en uppsättning Horn-satser . Ett annat område av intresse för programmeringsspråksteoretiker i början av 1970-talet var introduktionen av abstrakta datatyper på nivån för språkkonstruktioner, där Clu (1974, Barbara Liskov ) ansågs vara det första sådana språket .
En viktig milstolpe på vägen mot bildandet av det funktionella programmeringsparadigmet var utvecklingen oberoende av Girard ( fr. Jean-Yves Girard ; 1971) och Reynolds ( eng. John C. Reynolds ; 1974) av systemet F - en typad λ -kalkyl av andra ordningen, som ger möjlighet att konstruera termer som är beroende av från typer. Ett betydande bidrag till utvecklingen av funktionell programmering i mitten av 1970-talet gjordes också av utvecklarna av programmeringsspråket Scheme , en Lisp - dialekt som inkluderade lexikalisk räckvidd , ett enhetligt namnutrymme och element från skådespelarmodellen , inklusive fortsättningar . Ökningen av det breda intresset för funktionell programmering är förknippat med Turing-föreläsningen av skaparen av Fortran Backus 1977, där han kritiskt analyserade tillståndet för de programmeringsspråk som var populära vid den tiden och kom till det funktionella paradigmet.
År 1980 identifierade William Alvin Howard , med hänvisning till logikern Haskell Currys skrifter på 1950-talet, en strukturell överensstämmelse mellan datorprogram och matematiska bevis, som blev känd som Curry-Howard-isomorfismen och blev den teoretiska grunden för klassen automatiska bevisspråk .
Under första hälften av 1980-talet ägnades stor uppmärksamhet åt forskning om implementering av parallellism i programmeringsspråk och utveckling av varianter av processkalkyl : kalkylen för interagerande system skapades ( Milner , 1980), språket för interagerande sekventiella processer ( Hoare , 1985), bildades slutligen Hewitts skådespelaremodell ( eng. ) Carl Hewitt
Utgivningen av Miranda- språket 1985 underblåste det akademiska intresset för lata rena funktionella programmeringsspråk , vilket resulterade i att en kommitté bildades för att definiera en öppen standard för ett sådant språk, vilket resulterade i Haskell version 1.0 1990 .
1986, som en del av arbetet med att skapa Eiffelspråket , skapades kontraktsprogrammeringsparadigmet ( Bertrand Meyer , 1986).
Teori studerar aspekter av programmeringsspråk, så långt det är möjligt, som en uppsättning, med ett eller annat särskilt språk som exempel, men samtidigt med hjälp av medel med en tillräckligt hög generell nivå för att resultaten kan tillämpas på någon klass av språk. I teoretisk utveckling skapas ofta ett specialiserat, " akademiskt " programmeringsspråk, som av en eller annan anledning inte är lämpligt för praktisk implementering, men som visar vissa teoretiska resultat, som sedan tillämpas på de språk som används i industri. För teoretisk forskning används verktygen från grunderna för matematik och matematisk logik , inklusive mängdlära , modellteori , beräkningsbarhetsteori , såväl som sådana abstrakta avsnitt som kategoriteori , universell algebra , grafteori , och beror i hög grad på resultaten av tillämpade områden, inklusive komplexitetsteori beräkning , kodningsteori .
Formell semantik är en sådan formell beskrivning av programmeringsspråk som gör att man kan matematiskt tolka "betydelsen" av ett datorprogram skrivet på det språket. Det finns tre allmänna tillvägagångssätt för att beskriva semantiken i ett programmeringsspråk: denotationssemantik , operativ semantik och axiomatisk semantik .
Typteori är studiet av typsystem ; är "en lydig syntaktisk metod för att bevisa brister i beteendet hos ett visst program genom att klassificera fraser efter nivån på värden de beräknar" [2] . Många programmeringsspråk skiljer sig åt i egenskaperna hos deras typsystem.
Programanalys är det allmänna problemet med att undersöka ett program och bestämma huvudegenskaperna (som frånvaron av fel i programmet).
Programkonvertering är processen att konvertera ett program från en form (språk) till en annan form.
Jämförande programmeringsspråksanalys syftar till att klassificera programmeringsspråk i olika typer, beroende på deras egenskaper; de allmänna idéerna och koncepten för programmeringsspråk är kända som programmeringsparadigm .
Generisk programmering är ett programmeringsparadigm som består av en sådan beskrivning av data och algoritmer som kan appliceras på olika typer av data utan att själva ändra denna beskrivning.
Metaprogrammering är genereringen av program av högre ordning som, när de körs, producerar program (kanske på ett annat språk eller en delmängd av originalspråket) som ett resultat av deras arbete.
Domänspecifika språk är språk som är designade för att effektivt lösa problem inom ett visst ämnesområde.
Kompilatorteori är teorin om att skriva kompilatorer (eller mer allmänt översättare); program som översätter ett program skrivet på ett språk till en annan form.
Kompilatoråtgärder är traditionellt uppdelade i:
Runtime-system hänvisar till utvecklingen av programmeringsspråkskörtider och deras komponenter, inklusive virtuella maskiner , sophämtning och externa funktionella gränssnitt