Бағдарламалау тілдерін математикалық объектілер арқылы зерттеу

Програмдық тілдерді математикалық объектілер арқылы зерттеу: денотациялық семантика, формальды мағынасын қалыптастыру, құралымдық принциптері.

5 мин оқу

100%

Дереккөз: Denotational semantics — Wikipedia

Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.

Мазмұны

Кіріспе

Бағдарламалау тілдерін математикалық объектілер арқылы зерттеу

Компьютерлік ғылымда денотациялық семантика (бастапқыда математикалық семантика немесе Скотт-Страчи семантикасы деп аталған) – бағдарламалау тілдерінің мағыналарын тілдердегі өрнектердің мағыналарын сипаттайтын математикалық объектілер (денотациялар деп аталады) құрастыру арқылы ресмилендіру тәсілі. Бағдарламалау тілдерінің формалды семантикасын қамтамасыз ететін басқа тәсілдерге аксиоматикалық семантика және операциялық семантика жатады. Жалпы айтқанда, денотациялық семантика бағдарламалардың не істейтінін көрсететін домендер деп аталатын математикалық объектілерді табумен айналысады. Мысалы, бағдарламалар (немесе бағдарламалық фразалар) ішінара функциялармен немесе орта мен жүйе арасындағы ойындармен бейнеленуі мүмкін. Денотациялық семантиканың маңызды принципі – семантика композициялық болуы керек: бағдарламалық фразаның денотациясы оның ішкі фразаларының денотацияларынан құрылуы тиіс.

Тарихи дамуы

Денотациялық семантика Кристофер Стречи мен Дана Скоттың 1970 жылдардың басында жариялаған еңбектерінде қалыптасты. Ол CSP және Haskell тілдерінде қолданылады. Бұл тілдердің семантикасы құрастырмалы болып табылады, яғни тіркестің мағынасы оның құрамына кіретін тіркестердің мағынасына тәуелді. Мысалы, f(E1, E2) аппликативтік өрнегінің мағынасы f, E1 және E2 субөрімдерінің семантикасы арқылы анықталады. Қазіргі заманғы бағдарламалау тілінде E1 және E2 бір уақытта орындалуы мүмкін, ал олардың бірінің орындалуы ортақ нысандар арқылы өзара әрекеттесу нәтижесінде олардың мағыналарын бір-біріне байланысты анықтауы мүмкін. Сондай-ақ, E1 немесе E2 қателік тудыруы мүмкін, бұл екіншісінің орындалуын тоқтатуы мүмкін. Төмендегі бөлімдерде осы заманауи бағдарламалау тілдерінің семантикасының ерекше жағдайлары сипатталған.

Рекурсивті бағдарламалардың мағынасы

Денотациялық семантика бағдарламалық тіркеске ортадан (оның бос айнымалыларының ағымдағы мәндерін сақтайтын) оның денотациясына функция ретінде тағайындалады. Мысалы, тіркес екі бос айнымалысы үшін байланыс бар ортамен берілгенде денотацияны тудырады: және . Егер ортада -ның мәні 3-ке, ал -ның мәні 5-ке тең болса, онда денотация 15-ке тең болады.

Бір мезгілделіктің денотациялық семантикасы

Көптеген зерттеушілер жоғарыда келтірілген домендік теориялық модельдер бір мезгілдегі есептеулердің жалпы жағдайы үшін жеткіліксіз екенін айтты. Осы себепті, әртүрлі жаңа модельдер ұсынылды. 1980 жылдардың басында, адамдар бір мезгілдегі тілдерге семантика беру үшін денотациялық семантика әдісін қолдана бастады. Мысалдарға Уилл Клингердің актерлік модельдегі жұмысы, Глинн Винскелдің оқиға құрылымдары мен Петри желілеріндегі жұмысы, сондай-ақ Франц, Хоар, Леман және де Ровердің (1979) CSP үшін із семантикасы жөніндегі жұмысы жатады. Бұл зерттеулердің барлығы қазір де зерттелуде (мысалы, CSP үшін әртүрлі денотациялық модельдерді қараңыз).

Мемлекеттің денотациялық семантикасы

Мемлекеттік (мысалы, жиын) және қарапайым императивтік мүмкіндіктер жоғарыда сипатталған денотациялық семантикада тікелей модельделуі мүмкін. Басты идея – команданы белгілі бір күйлер доменіндегі ішінара функция ретінде қарастыру. "" операторының мәні – күйді, -қа тағайындалған күйге түрлендіретін функция болып табылады. "" операторы функциялардың композициясы арқылы белгіленеді. Содан кейін "" сияқты циклдық конструкцияларға семантика беру үшін бекітілген нүктелік құрылымдар қолданылады. Жергілікті айнымалылары бар бағдарламаларды модельдеу қиындықтар тудырады. Бір тәсіл – енді домендермен жұмыс істемеу, керісінше типтерді әлемдердің белгілі бір санаттарынан домендер санатына дейінгі функторлар ретінде қарастыру. Бағдарламалар осы функторлар арасындағы табиғи үздіксіз функциялармен белгіленеді.

Күрделілігі шектеулі бағдарламалардың денотациялық семантикасы

Сызықтық логикаға негізделген бағдарламалау тілдерінің дамуынан кейін, сызықтық қолдануға арналған тілдерге (мысалы, дәлелдеу желілері, когерентті кеңістіктер) және полиномиалдық уақыт күрделілігіне денотациялық семантика берілді.

Сәйкестіктің денотациялық семантикасы

Кезекті бағдарламалау тілі PCF үшін толық абстракция мәселесі ұзақ жылдар бойы денотациялық семантикадағы маңызды ашық сұрақ болып келді. PCF-тің қиындығы оның өте кезекті тіл екендігінде. Мысалы, PCF-те параллельдік немесе функцияны анықтау мүмкін емес. Осы себепті, жоғарыда сипатталған домендерді қолдану тәсілі толық абстракцияны қамтамасыз етпейтін денотациялық семантиканы тудырады. Бұл ашық мәселе 1990 жылдары ойын семантикасының және логикалық қатынастарға негізделген әдістердің дамуымен көбінесе шешілді. Қосымша мәліметтер үшін PCF бетіне қараңыз.

Денотациялық семантика - көзден көзге аударма

Бір бағдарламалау тілін екіншісіне аудару көбінесе пайдалы болады. Мысалы, параллель бағдарламалау тілі процестік есептеуге аударылуы мүмкін; жоғары деңгейдегі бағдарламалау тілі байт-кодқа аударылуы мүмкін. (Шындығында, дәстүрлі денотациялық семантиканы бағдарламалау тілдерін домендер санатының ішкі тіліне интерпретациялау ретінде қарастыруға болады.) Осы контексте, денотациялық семантикадан алынған толық абстракция сияқты түсініктер, қауіпсіздік талаптарын орындауға көмектеседі.

Композициялық

Бағдарламалау тілдерінің денотациялық семантикасының маңызды аспектісі – композициялылық, яғни бағдарламаның денотациясы оның бөліктерінің денотацияларынан құралады. Мысалы, "7 + 4" өрнегін қарастырайық. Бұл жағдайда композициялылық – "7 + 4" өрнегіне "7", "4" және "+" өрнектерінің мағыналары тұрғысынан мағына беру болып табылады. Домендер теориясындағы негізгі денотациялық семантика композициялық болып табылады, себебі ол келесідей беріледі. Біз бағдарлама фрагменттерін, яғни бос айнымалылары бар бағдарламаларды қарастырудан бастаймыз. Типтеу контексі әр бос айнымалыға тип тағайындайды. Мысалы, (x + y) өрнегі (x:, y:) типтеу контексінде қарастырылуы мүмкін. Енді, келесі схеманы қолдана отырып, бағдарлама фрагменттеріне денотациялық семантика береміз. Біз тілдің типтерінің мағынасын сипаттаудан бастаймыз: әр типтің мағынасы домен болуы керек. Біз τ типін білдіретін доменді 〚τ〛 деп жазамыз. Мысалы, типтің мағынасы натурал сандар домені болуы керек: 〚〛 = ⊥. Типтердің мағынасынан біз типтеу контексінің мағынасын шығарамыз. Біз 〚x1:τ1, ..., xn:τn〛 = 〚τ1〛 × ... × 〚τn〛 деп белгілейміз. Мысалы, 〚x:, y:〛 = ⊥ × ⊥. Арнайы жағдайда, айнымалылары жоқ бос типтеу контекстінің мағынасы – бір элементі бар домен, ол 1 деп белгіленеді. Соңында, біз типтеу контексінде әр бағдарлама фрагментіне мағына беруіміз керек. P бағдарлама фрагменті σ типіне ие деп есептейік, Γ типтеу контексінде, көбінесе Γ⊢P:σ деп жазылады. Онда бұл бағдарламаның типтеу контексіндегі мағынасы үздіксіз функция болуы керек: 〚Γ⊢P:σ〛: 〚Γ〛 → 〚σ〛. Мысалы, 〚⊢7:〛: 1 → ⊥ – тұрақты "7" функциясы, ал 〚x:, y:⊢x+y:〛: ⊥ × ⊥ → ⊥ – екі санды қосатын функция. Енді, (7+4) күрделі өрнегінің мағынасы үш функцияны құрау арқылы анықталады: 〚⊢7:〛: 1 → ⊥, 〚⊢4:〛: 1 → ⊥ және 〚x:, y:⊢x+y:〛: ⊥ × ⊥ → ⊥. Шындығында, бұл композициялық денотациялық семантиканың жалпы схемасы. Бұл жерде домендер мен үздіксіз функцияларға қатысты ешқандай ерекшелік жоқ. Олардың орнына басқа категорияны қолдануға болады. Мысалы, ойын семантикасында ойын категориясы ойындарды объектілер ретінде және стратегияларды морфизмдер ретінде қарастырады: типтерді ойындар ретінде, ал бағдарламаларды стратегиялар ретінде түсіндіруге болады. Жалпы рекурсиясыз қарапайым тіл үшін жиындар мен функциялар категориясы жеткілікті. Жанама әсерлері бар тіл үшін монадтың Клейсли категориясын қолдануға болады. Күйі бар тіл үшін функтор категориясын қолдануға болады. Милнер интерфейстерді объектілер ретінде және биграфтарды морфизмдер ретінде қарастыра отырып, орналасу мен өзара әрекеттесуді модельдеуді ұсынды.

An important aspect of denotational semantics of programming languages is compositionality, by which the denotation of a program is constructed from denotations of its parts. For example, consider the expression "7 + 4". Compositionality in this case is to provide a meaning for "7 + 4" in terms of the meanings of "7", "4" and "+". A basic denotational semantics in domain theory is compositional because it is given as follows. We start by considering program fragments, i. e. programs with free variables. A typing context assigns a type to each free variable. For instance, in the expression (x + y) might be considered in a typing context (x:,y:). We now give a denotational semantics to program fragments, using the following scheme. We begin by describing the meaning of the types of our language: the meaning of each type must be a domain. We write 〚τ〛 for the domain denoting the type τ. For instance, the meaning of type should be the domain of natural numbers: 〚〛= ⊥. From the meaning of types we derive a meaning for typing contexts. We set 〚 x1:τ1, , xn:τn〛 = 〚 τ1〛× ×〚τn〛. For instance, 〚x:,y:〛= ⊥×⊥. As a special case, the meaning of the empty typing context, with no variables, is the domain with one element, denoted 1. Finally, we must give a meaning to each program fragment in typing context. Suppose that P is a program fragment of type σ, in typing context Γ, often written Γ⊢P:σ. Then the meaning of this program in typing context must be a continuous function 〚Γ⊢P:σ〛:〚Γ〛→〚σ〛. For instance, 〚⊢7:〛:1→⊥ is the constantly "7" function, while 〚x:,y:⊢x+y:〛:⊥×⊥→⊥ is the function that adds two numbers. Now, the meaning of the compound expression (7+4) is determined by composing the three functions 〚⊢7:〛:1→⊥, 〚⊢4:〛:1→⊥, and 〚x:,y:⊢x+y:〛:⊥×⊥→⊥. In fact, this is a general scheme for compositional denotational semantics. There is nothing specific about domains and continuous functions here. One can work with a different category instead. For example, in game semantics, the category of games has games as objects and strategies as morphisms: we can interpret types as games, and programs as strategies. For a simple language without general recursion, we can make do with the category of sets and functions. For a language with side effects, we can work in the Kleisli category for a monad. For a language with state, we can work in a functor category. Milner has advocated modelling location and interaction by working in a category with interfaces as objects and bigraphs as morphisms.

Компьютер ғылымдарының басқа салаларымен байланысы

Денотациялық семантикадағы кейбір зерттеулер типтерді домен теориясы мағынасындағы домендер ретінде қарастырды, оны модель теориясының бір саласы деп есептеуге болады, бұл типтер теориясы және категориялар теориясымен байланысқа алып келді. Компьютер ғылымында абстрактілі интерпретация, бағдарламаны растау және модельді тексеру салаларымен байланыстар бар.