Սեմանտիկա (համակարգչային գիտություն)

**Սեմանտիկա,** ծրագրավորման լեզուների տեսության մեջ  իմաստի խիստ մաթեմատիկական ուսումնասիրություն: Սեմանտիկան հաշվարկային իմաստ է տալիս ծրագրավորման լեզվի շարահյուսությանը համապատասխան վավեր տողերին։ Այն սերտորեն կապված է մաթեմատիկական ապացույցների սեմանտիկայի հետ և հաճախ համընկնում է դրա հետ։ 

Սեմանտիկան նկարագրում է այն գործընթացները, որոնք համակարգիչը կատարում է տվյալ լեզվով գրված ծրագիրն աշխատացնելիս։ Դա կարելի է իրականացնել՝ նկարագրելով ծրագրի մուտքային և ելքային տվյալների միջև եղած կապը, կամ բացատրելով՝ թե ինչպես ծրագիրը կկատարվի որևէ հարթակում՝ այդպիսով ստեղծելով հաշվարկի մոդել։

## Պատմություն
1967 թվականին Ռոբերտ Վ. Ֆլոյդը հրապարակել է «Ծրագրերին իմաստների վերագրում» () հոդվածը։ Նրա հիմնական նպատակն էր հաստատել խիստ չափանիշներ համակարգչային ծրագրերի վերաբերյալ ապացույցների համար, ներառյալ՝ ճշտության, համարժեքության և ավարտականության ապացույցները։ Ֆլոյդը նաև գրել է․

1969 թվականին Թոնի Հոարը, հիմնվելով Ֆլոյդի գաղափարների վրա, հրապարակել է հոդված *Հոարի տրամաբանության* վերաբերյալ, որը հիմա երբեմն համատեղ անվանում են *աքսիոմատիկ սեմանտիկա*։

1970-ական թվականներին ի հայտ են եկել *օպերացիոն սեմանտիկա* և *դենոտացիոն սեմանտիկա* տերմինները։

## Ակնարկ
Ֆորմալ սեմանտիկայի ոլորտը ընդգրկում է հետևյալը․

* սեմանտիկ մոդելների սահմանում
* տարբեր սեմանտիկ մոդելների միջև հարաբերություններ
* իմաստի տարբեր մոտեցումների միջև հարաբերություններ
* հաշվարկման և այն ապահովող մաթեմատիկական կառուցվածքների միջև կապ, որոնք գալիս են տրամաբանությունից, բազմությունների տեսությունից, մոդելների տեսությունից, կատեգորիաների տեսությունից և այլն։

Այն սերտորեն կապված է համակարգչային գիտության այլ ոլորտների հետ, ինչպիսիք են ծրագրավորման լեզվի նախագծումը, տիպերի տեսությունը, կոմպիլյատորներն ու ինտերպրետատորները, ծրագրերի վավերացումը և մոդելային ստուգումը։

## Մոտեցումներ
Ֆորմալ սեմանտիկային մոտենալու բազմաթիվ եղանակներ կան, որոնք բաժանվում են երեք հիմնական դասի․

* Դենոտացիոն սեմանտիկա - այստեղ լեզվի յուրաքանչյուր արտահայտություն մեկնաբանվում է որպես *դենոտացիա*, այսինքն՝ գաղափարական իմաստ, որը կարելի է դիտարկել աբստրակտ ձևով։ Այդ դենոտացիաները հաճախ մաթեմատիկական օբյեկտներ են, որոնք պատկանում են որոշ մաթեմատիկական տարածության, բայց պարտադիր չէ, որ միշտ այդպես լինի։ Գործնական անհրաժեշտությունից ելնելով՝ դենոտացիաները նկարագրվում են մաթեմատիկական նշանագրության որևէ ձևով, որն էլ, իր հերթին, կարելի է ֆորմալացնել որպես *դենոտացիոն մետալեզու*։ Օրինակ, ֆունկցիոնալ լեզուների դենոտացիոն սեմանտիկան հաճախ լեզուն փոխադրում է *[[Դոմեններ|դոմենների]] տեսություն*։ Դենոտացիոն սեմանտիկայի նկարագրությունները կարող են նաև ծառայել որպես կոմպոզիցիոն թարգմանություն ծրագրավորման լեզվից դեպի դենոտացիոն մետալեզու և օգտագործվել որպես կոմպիլյատորների նախագծման հիմք։

* Օպերացիոն սեմանտիկա-  այս մոտեցման դեպքում լեզվի կատարման գործընթացը նկարագրվում է անմիջապես (ոչ թե թարգմանության միջոցով)։ Օպերացիոն սեմանտիկան մոտավորապես համապատասխանում է մեկնաբանմանը, թեև «մեկնաբանիչի իրականացվող լեզուն» սովորաբար մաթեմատիկական ֆորմալիզմ է։ Օպերացիոն սեմանտիկան կարող է սահմանել *աբստրակտ մեքենա* (օրինակ՝ SECD մեքենան) և իմաստ տալ արտահայտություններին՝ նկարագրելով այն անցումները, որոնք դրանք առաջացնում են մեքենայի վիճակների վրա։ Այլ տարբերակով, ինչպես *[[Լամբդա արտահայտություն|Լամբդա արտահայտության]]* դեպքում, օպերացիոն սեմանտիկան կարող է սահմանվել լեզվի արտահայտությունների վրա կիրառվող շարահյուսական փոխակերպումների միջոցով։
* Աքսիոմատիկ սեմանտիկա - այս մոտեցման դեպքում արտահայտություններին իմաստ է տրվում՝ նկարագրելով դրանց վրա կիրառվող աքսիոմները։ Աքսիոմատիկ սեմանտիկան տարբերություն չի դնում արտահայտության իմաստի և այն նկարագրող տրամաբանական բանաձևերի միջև․ դրա իմաստը հենց այն է, ինչ հնարավոր է ապացուցել դրա վերաբերյալ որոշ տրամաբանական համակարգում։ Աքսիոմատիկ սեմանտիկայի դասական օրինակն է Հոարի տրամաբանությունը։

Դենոտացիոն, օպերացիոն կամ աքսիոմատիկ մոտեցումներից բացի, ֆորմալ սեմանտիկայի համակարգերի մեծ մասը տարբերություններ ունեն հիմնականում այն պատճառով, թե որ մաթեմատիկական ֆորմալիզմն է ընտրվում աջակցման համար։

## Տարբերակներ
Ֆորմալ սեմանտիկայի որոշ տարբերակներ ներառում են հետևյալը․

* Գործողությունների սեմանտիկա (Action semantics) - մոտեցում, որը փորձում է մոդուլավորել դենոտացիոն սեմանտիկան, բաժանել ֆորմալացման գործընթացը երկու շերտի՝ մակրո- և միկրոսեմանտիկայի, և նախորոշել երեք սեմանտիկ միավորներ՝ գործողություններ, տվյալներ և արտահանում, որպեսզի պարզացվի տվյալների նկարագրությունը։

* Ալգեբրային սեմանտիկա (Algebraic semantics, սա հանրահաշվականը չէ) - աքսիոմատիկ սեմանտիկայի տեսակ, որը հիմնված է ալգեբրային օրենքների վրա և հնարավորություն է տալիս ֆորմալ կերպով նկարագրել և վերլուծել ծրագրի սեմանտիկան։ Այն նաև աջակցում է դենոտացիոն և օպերացիոն սեմանտիկային։

* Ատրիբուտային շարահյուսություն (Attribute grammars) - սահմանում են համակարգեր, որոնք համակարգված կերպով հաշվարկում են «մետատվյալներ» (attributes) լեզվի շարահյուսության տարբեր դեպքերի համար։ Ատրիբուտային շարահյուսությունները կարելի է դիտարկել որպես դենոտացիոն սեմանտիկա, որտեղ նպատակային լեզուն պարզապես նախնական լեզուն է՝ լրացված attribute-ների գրառմամբ։ 

* Կատեգորիական (Categorical) կամ «ֆունկտորիալ» (functorial) սեմանտիկա օգտագործում է կատեգորիաների տեսությունը որպես հիմնական մաթեմատիկական ֆորմալիզմ։ Կատեգորիական սեմանտիկան սովորաբար ապացուցվում է, որ համապատասխանում է որոշ աքսիոմատիկ սեմանտիկայի, որը շարահյուսական ներկայացում է տալիս կատեգորիական կառուցվածքներին։ Նաև, դենոտացիոն սեմանտիկաները հաճախ համարվում են ընդհանուր կատեգորիական սեմանտիկայի դեպքեր։
* Զուգահեռության սեմանտիկան համընդհանուր տերմին է ցանկացած ֆորմալ սեմանտիկայի համար, որը նկարագրում է համաժամանակյա հաշվարկները: 
* Խաղերի սեմանտիկան օգտագործում է խաղերի տեսությունից ոգեշնչված փոխաբերությունները։
* Տրանսֆորմատորային սեմանտիկա, որը մշակված է Էդսգեր Վ. Դեյկստրայի կողմից և նկարագրում է ծրագրի մի հատվածի իմաստը որպես ֆունկցիա, որը փոխակերպում է հետպայմանը դրա հաստատման համար անհրաժեշտ նախապայմանի։

## Հարաբերությունների նկարագրում
Որոշ պատճառներով ցանկալի է նկարագրել տարբեր ֆորմալ սեմանտիկաների միջև գոյություն ունեցող հարաբերությունները։ Օրինակ՝

* Ապացուցել, որ լեզվի որոշակի օպերացիոն սեմանտիկան բավարարում է այդ լեզվի աքսիոմատիկ սեմանտիկայի տրամաբանական բանաձևերը։ Նման ապացույցը ցույց է տալիս, որ «հիմնավոր» է դատողություններ անել որոշակի (օպերացիոն) մեկնաբանության ռազմավարության մասին՝ օգտագործելով որոշակի (աքսիոմատիկ) ապացույցների համակարգ։
* Ապացուցել, որ բարձր մակարդակի մեքենայի վրա օպերացիոն սեմանտիկան կապված է ցածր մակարդակի մեքենայի վրա սեմանտիկայի հետ սիմուլյացիայի միջոցով, որի դեպքում ցածր մակարդակի աբստրակտ մեքենան պարունակում է ավելի շատ պարզունակ գործողություններ, քան տվյալ լեզվի բարձր մակարդակի աբստրակտ մեքենայի սահմանումը։ Նման ապացույցը ցույց է տալիս, որ ցածր մակարդակի մեքենան «հավատարմորեն իրականացնում է» բարձր մակարդակի մեքենայի գործառույթները։

Հնարավոր է նաև կապ հաստատել մի քանի սեմանտիկայի միջև աբստրակցիաների միջոցով, օգտագործելով աբստրակտ մեկնաբանման տեսությունը (abstract interpretation theory)։

## Ծանոթագրություններ

Կատեգորիա:Ինֆորմատիկա
Կատեգորիա:Ծրագրավորման լեզուներ
Կատեգորիա:Ծրագրավորում
Կատեգորիա:Տեսական ինֆորմատիկա
Կատեգորիա:Տրամաբանություն
Կատեգորիա:Քերականություն
Կատեգորիա:Ֆորմալ մեթոդներ