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

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

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

Պատմություն

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

Ծրագրավորման լեզվի սեմանտիկական սահմանումը, մեր մոտեցմամբ, հիմնված է շարահյուսական սահմանման վրա։ Այն պետք է ճշգրտի, թե շարահյուսական առումով ճիշտ ծրագրի որ արտահայտություններն են ներկայացնում հրամաններ և ինչ պայմաններ պետք է դրվեն յուրաքանչյուր հրամանի մեկնաբանության շուրջ^[2]։

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

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

Ակնարկ

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

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

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

Մոտեցումներ

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

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

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

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

Տարբերակներ

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

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

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

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

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

Հարաբերությունների նկարագրում

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

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

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

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

↑ Goguen, Joseph A. (1975). «Semantics of computation». Category Theory Applied to Computation and Control. Lecture Notes in Computer Science. Vol. 25. Springer Publishing|Springer. էջեր 151–163. doi:10.1007/3-540-07142-3_75. ISBN 978-3-540-07142-6.
↑ ^2,0 ^2,1 Floyd, Robert W. (1967). «Assigning Meanings to Programs» (PDF). In Schwartz, J.T. (ed.). Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics. Vol. 19. American Mathematical Society. էջեր 19–32. ISBN 0821867288.
↑ Knuth, Donald E. «Memorial Resolution: Robert W. Floyd (1936–2001)» (PDF). Stanford University Faculty Memorials. Stanford Historical Society.
↑ Schmidt, David A. (1986). Denotational Semantics: A Methodology for Language Development. William C. Brown Publishers. ISBN 9780205104505.
↑ Plotkin, Gordon D. (1981). A structural approach to operational semantics (Report). Technical Report DAIMI FN-19. Computer Science Department, Aarhus University.
↑ ^6,0 ^6,1 Goguen, Joseph A.; Thatcher, James W.; Wagner, Eric G.; Wright, Jesse B. (1977). «Initial algebra semantics and continuous algebras». Journal of the ACM. 24 (1): 68–95. doi:10.1145/321992.321997. S2CID 11060837.
↑ «What's the difference between: operational, denotational and axiomatic semantics?». Computer Science Stack Exchange (անգլերեն). Վերցված է 2025 թ․ օգոստոսի 15-ին.
↑ Mosses, Peter D. (1996). Theory and practice of action semantics (Report). BRICS Report RS9653. Aarhus University.
↑ Deransart, Pierre; Jourdan, Martin; Lorho, Bernard (1988). "Attribute Grammars: Definitions, Systems and Bibliography. Lecture Notes in Computer Science 323. Springer-Verlag. ISBN 9780387500560.
↑ Lawvere, F. William (1963). «Functorial semantics of algebraic theories». Proceedings of the National Academy of Sciences of the United States of America. 50 (5): 869–872. Bibcode:1963PNAS...50..869L. doi:10.1073/pnas.50.5.869. PMC 221940. PMID 16591125.
↑ Andrzej Tarlecki; Rod M. Burstal; Joseph Goguen|Joseph A. Goguen (1991). «Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories». Theoretical Computer Science. 91 (2): 239–264. doi:10.1016/0304-3975(91)90085-G.
↑ Batty, Mark; Memarian, Kayvan; Nienhuis, Kyndylan; Pichon-Pharabod, Jean; Sewell, Peter (2015). «The problem of programming language concurrency semantics» (PDF). Proceedings of the European Symposium on Programming Languages and Systems. Springer Publishing|Springer. էջեր 283–307. doi:10.1007/978-3-662-46669-8_12.
↑ Abramsky, Samson (2009). «Semantics of interaction: An introduction to game semantics». In Andrew M. Pitts; P. Dybjer (eds.). Semantics and Logics of Computation. Cambridge University Press. էջեր 1–32. doi:10.1017/CBO9780511526619.002. ISBN 9780521580571.
↑ Dijkstra, Edsger W. (1975). «Guarded commands, nondeterminacy and formal derivation of programs». Communications of the ACM. 18 (8): 453–457. doi:10.1145/360933.360975. S2CID 1679242.
↑ Giacobazzi, Roberto; Mastroeni, Isabella (2005 թ․ հունիսի 9). «Transforming semantics by abstract interpretation». Theoretical Computer Science. էջեր 1–50. doi:10.1016/j.tcs.2004.12.021. Վերցված է 2025 թ․ օգոստոսի 15-ին.

[1] Goguen, Joseph A. (1975). «Semantics of computation». Category Theory Applied to Computation and Control. Lecture Notes in Computer Science. Vol. 25. Springer Publishing|Springer. էջեր 151–163. doi:10.1007/3-540-07142-3_75. ISBN 978-3-540-07142-6.

[floyd-2] 2,0 ^2,1 Floyd, Robert W. (1967). «Assigning Meanings to Programs» (PDF). In Schwartz, J.T. (ed.). Mathematical Aspects of Computer Science. Proceedings of Symposium on Applied Mathematics. Vol. 19. American Mathematical Society. էջեր 19–32. ISBN 0821867288.

[3] Knuth, Donald E. «Memorial Resolution: Robert W. Floyd (1936–2001)» (PDF). Stanford University Faculty Memorials. Stanford Historical Society.

[Schmidt1986-4] Schmidt, David A. (1986). Denotational Semantics: A Methodology for Language Development. William C. Brown Publishers. ISBN 9780205104505.

[Plotkin1981-5] Plotkin, Gordon D. (1981). A structural approach to operational semantics (Report). Technical Report DAIMI FN-19. Computer Science Department, Aarhus University.

[Goguen77-6] 6,0 ^6,1 Goguen, Joseph A.; Thatcher, James W.; Wagner, Eric G.; Wright, Jesse B. (1977). «Initial algebra semantics and continuous algebras». Journal of the ACM. 24 (1): 68–95. doi:10.1145/321992.321997. S2CID 11060837.

[7] «What's the difference between: operational, denotational and axiomatic semantics?». Computer Science Stack Exchange (անգլերեն). Վերցված է 2025 թ․ օգոստոսի 15-ին.

[Mosses1996-8] Mosses, Peter D. (1996). Theory and practice of action semantics (Report). BRICS Report RS9653. Aarhus University.

[9] Deransart, Pierre; Jourdan, Martin; Lorho, Bernard (1988). "Attribute Grammars: Definitions, Systems and Bibliography. Lecture Notes in Computer Science 323. Springer-Verlag. ISBN 9780387500560.

[Lawvere1963-10] Lawvere, F. William (1963). «Functorial semantics of algebraic theories». Proceedings of the National Academy of Sciences of the United States of America. 50 (5): 869–872. Bibcode:1963PNAS...50..869L. doi:10.1073/pnas.50.5.869. PMC 221940. PMID 16591125.

[11] Andrzej Tarlecki; Rod M. Burstal; Joseph Goguen|Joseph A. Goguen (1991). «Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed categories». Theoretical Computer Science. 91 (2): 239–264. doi:10.1016/0304-3975(91)90085-G.

[12] Batty, Mark; Memarian, Kayvan; Nienhuis, Kyndylan; Pichon-Pharabod, Jean; Sewell, Peter (2015). «The problem of programming language concurrency semantics» (PDF). Proceedings of the European Symposium on Programming Languages and Systems. Springer Publishing|Springer. էջեր 283–307. doi:10.1007/978-3-662-46669-8_12.

[Abramsky2009-13] Abramsky, Samson (2009). «Semantics of interaction: An introduction to game semantics». In Andrew M. Pitts; P. Dybjer (eds.). Semantics and Logics of Computation. Cambridge University Press. էջեր 1–32. doi:10.1017/CBO9780511526619.002. ISBN 9780521580571.

[Dijkstra1975-14] Dijkstra, Edsger W. (1975). «Guarded commands, nondeterminacy and formal derivation of programs». Communications of the ACM. 18 (8): 453–457. doi:10.1145/360933.360975. S2CID 1679242.

[15] Giacobazzi, Roberto; Mastroeni, Isabella (2005 թ․ հունիսի 9). «Transforming semantics by abstract interpretation». Theoretical Computer Science. էջեր 1–50. doi:10.1016/j.tcs.2004.12.021. Վերցված է 2025 թ․ օգոստոսի 15-ին.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]