Sémantika (informatika) - Semantics (computer science)

V programování teorie jazyka , sémantika je zaměřena na důsledné matematické studii o významu pole programovacích jazyků . Činí tak tak, že vyhodnotí význam syntakticky platných řetězců definovaných konkrétním programovacím jazykem a zobrazí příslušný výpočet. V takovém případě, že by vyhodnocení bylo syntakticky neplatných řetězců, by výsledkem bylo nepočítání. Sémantika popisuje procesy, kterými se počítač řídí při provádění programu v tomto konkrétním jazyce. To lze ukázat popisem vztahu mezi vstupem a výstupem programu nebo vysvětlením toho, jak bude program na určité platformě spuštěn , a tím se vytvoří model výpočtu .

Přehled

Oblast formální sémantiky zahrnuje všechny následující:

• Definice sémantických modelů
• Vztahy mezi různými sémantickými modely
• Vztahy mezi různými přístupy k významu
• Vztah mezi výpočtu a základních matematických struktur z oblastí, jako jsou logika , teorie množin , teorii modelu , teorie kategorie , atd

Má úzké vazby na další oblasti počítačové vědy, jako je návrh programovacího jazyka , teorie typů , překladače a překladače , ověřování programu a kontrola modelů .

Přístupy

Existuje mnoho přístupů k formální sémantice; tyto patří do tří hlavních tříd:

• Denotační sémantika , přičemž každá fráze v jazyce je interpretována jako denotace , tj. Pojmový význam, o kterém lze uvažovat abstraktně. Takové denotace jsou často matematické objekty obývající matematický prostor, ale není podmínkou, aby tomu tak bylo. Jako praktická nutnost jsou denotace popsány pomocí nějaké formy matematické notace, která může být zase formalizována jako denotační metajazyk. Například denotační sémantika funkčních jazyků často překládá jazyk do teorie domén . Denotační sémantické popisy mohou také sloužit jako kompoziční překlady z programovacího jazyka do denotačního metajazyka a slouží jako základ pro navrhování překladačů .
• Operační sémantika , přičemž provedení jazyka je popsáno přímo (spíše než překladem). Operační sémantika volně odpovídá interpretaci , i když opět „implementačním jazykem“ tlumočníka je obecně matematický formalismus. Operační sémantika může definovat abstraktní stroj (například stroj SECD ) a dát frázím význam popisem přechodů, které vyvolávají na stavech stroje. Alternativně, stejně jako u čistého lambda kalkulu , lze operační sémantiku definovat pomocí syntaktických transformací na fráze samotného jazyka;
• Axiomatická sémantika , přičemž člověk dává frázím význam tím, že popisuje axiomy, které se na ně vztahují. Axiomatická sémantika nedělá rozdíl mezi významem fráze a logickými formulemi, které ji popisují; jeho význam je přesně to, co se na něm dá v nějaké logice dokázat. Kanonickým příkladem axiomatické sémantiky je Hoareova logika .

Na rozdíl od volby mezi denotačními, operačními nebo axiomatickými přístupy, většina variací ve formálních sémantických systémech vyplývá z volby podpory matematického formalismu.

Variace

Některé variace formální sémantiky zahrnují následující:

• Akční sémantika je přístup, který se snaží modularizovat denotační sémantiku, rozdělit proces formalizace na dvě vrstvy (makro a mikrosemantika) a předdefinovat tři sémantické entity (akce, data a poskytovatele) za účelem zjednodušení specifikace;
• Algebraické sémantiky je forma axiomatických sémantiky na základě algebraických zákony pro popis a uvažování o programových sémantiky ve formálním způsobem;
• Gramatiky atributů definují systémy, které systematicky počítají „ metadata “ (nazývané atributy ) pro různé případy syntaxe jazyka . Gramatiky atributů lze chápat jako denotační sémantiku, kde je cílovým jazykem jednoduše původní jazyk obohacený anotacemi atributů. Kromě formální sémantiky byly také atributové gramatiky použity pro generování kódu v překladačích a pro rozšíření pravidelných nebo bezkontextových gramatik opodmínky citlivé na kontext ;
• Kategorická (nebo „funktoriální“) sémantika používá teorii kategorií jako základní matematický formalismus. U kategorické sémantiky se obvykle prokáže, že odpovídá nějaké axiomatické sémantice, která poskytuje syntaktickou prezentaci kategoriálních struktur. Denotační sémantika je také často příkladem obecné kategorické sémantiky,
• Sémantika souběžnosti je univerzální termín pro jakoukoli formální sémantiku, která popisuje souběžné výpočty. Historicky důležité souběžné formalismy zahrnovaly herecký model a procesní kameny ;
• Herní sémantika používá metaforu inspirovanou teorií her .
• Sémantika predikátového transformátoru , kterou vyvinul Edsger W. Dijkstra , popisuje význam fragmentu programu jako funkci transformující postkondicionaci na předpoklad potřebný k jejímu vytvoření.

Popis vztahů

Z různých důvodů lze popsat vztahy mezi různými formálními sémantikami. Například:

• Dokázat, že konkrétní operační sémantika pro jazyk splňuje logické vzorce axiomatické sémantiky pro daný jazyk. Takový důkaz ukazuje, že je „rozumné“ uvažovat o konkrétní (operativní) interpretační strategii pomocí konkrétního (axiomatického) důkazního systému .
• Prokázat, že operační sémantika na stroji na vysoké úrovni souvisí se simulací se sémantikou na stroji na nízké úrovni, přičemž abstraktní stroj na nízké úrovni obsahuje primitivnější operace než definice abstraktního stroje na vyšší úrovni daného jazyka. Takový důkaz ukazuje, že nízkoúrovňový stroj „věrně implementuje“ stroj vyšší úrovně.

Je také možné propojit více sémantik prostřednictvím abstrakcí prostřednictvím teorie abstraktní interpretace .

Dějiny

Robert W. Floyd má zásluhu na založení oboru sémantiky programovacích jazyků ve Floydovi (1967) .

Viz také

• Výpočetní sémantika
• Formální sémantika (logika)
• Formální sémantika (lingvistika)
• Ontologie
• Ontologie (informační věda)
• Sémantická ekvivalence
• Sémantická technologie

Reference

Další čtení

Učebnice