Кіріспе
Операциялық семантика – бағдарламаның дұрыстығы, қауіпсіздігі немесе қорғалуы сияқты қажетті қасиеттері, оның терминдеріне математикалық мағына берудің орнына (денотациялық семантика), орындалуы мен процедуралары туралы логикалық тұжырымдардан дәлелдер құрастыру арқылы тексерілетін ресми бағдарламалау тілі семантикасының бір саласы. Операциялық семантика екі түрге бөлінеді: құрылымдық операциялық семантика (немесе кіші қадамдық семантика) компьютерлік жүйеде есептеудің жеке қадамдары қалай орындалатынын формалды түрде сипаттайды; ал табиғи семантика (немесе үлкен қадамдық семантика) орындаудың жалпы нәтижелерін қалай алуға болатынын көрсетеді. Бағдарламалау тілдерінің ресми семантикасын ұсынудың басқа тәсілдеріне аксиоматикалық семантика және денотациялық семантика жатады. Бағдарламалау тілінің операциялық семантикасы жарамды бағдарламаның есептеу қадамдарының тізбегі ретінде қалай түсіндірілетінін сипаттайды. Осы тізбектер бағдарламаның мәнін білдіреді. Функционалдық бағдарламалау контекстінде, аяқталатын тізбектің соңғы қадамы бағдарламаның мәнін қайтарады. (Жалпы алғанда, бір бағдарлама үшін көптеген қайтару мәндері болуы мүмкін, себебі бағдарлама белгісіз болуы мүмкін, тіпті детерминистік бағдарлама үшін де көптеген есептеу тізбектері болуы мүмкін, өйткені семантика сол мәнге жету үшін операциялардың қандай тізбегін нақты көрсетпейді.) Операциялық семантиканың алғашқы ресми қолданылуы Лисп тілінің семантикасын анықтау үшін лямбда-есептеуді пайдалану болды. SECD машинасы дәстүріндегі абстрактілі машиналар да осыған тығыз байланысты.
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms (denotational semantics). Operational semantics are classified in two categories: structural operational semantics (or small step semantics) formally describe how the individual steps of a computation take place in a computer based system; by opposition natural semantics (or big step semantics) describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics. The operational semantics for a programming language describes how a valid program is interpreted as sequences of computational steps. These sequences then are the meaning of the program. In the context of functional programming, the final step in a terminating sequence returns the value of the program. (In general there can be many return values for a single program, because the program could be nondeterministic, and even for a deterministic program there can be many computation sequences since the semantics may not specify exactly what sequence of operations arrives at that value.) Perhaps the first formal incarnation of operational semantics was the use of the lambda calculus to define the semantics of Lisp. Abstract machines in the tradition of the SECD machine are also closely related.
Қадамдар
Гордон Плоткин құрылымдық операциялық семантиканы, Матиас Феллейзен мен Роберт Хиб редукциялық семантиканы, ал Жиль Кан табиғи семантиканы ұсынды.
Кеміту семантикасы
Редукциялық семантика – операциялық семантиканың баламалы ұсынысы. Оның негізгі идеялары алғаш рет 1975 жылы Гордон Плоткин lambda-есептеуінің атымен және мәні бойынша шақырудың таза функционалдық варианттарына қолданылды және 1987 жылы Маттиас Феллейзен өзінің диссертациясында императивті мүмкіндіктері бар жоғары деңгейдегі функционалдық тілдерге жалпыланды. Әдіс 1992 жылы Маттиас Феллейзен мен Роберт Хиб бақылау және күйдің толық теңдеу теориясына дейін жетілдірілді. Редукциялық семантика әрқайсысы бір ғана мүмкін редукция қадамын көрсететін редукция ережелерінің жиынтығы ретінде беріледі. Мысалы, келесі редукция ережесі айнымалы жариялануының жанында орналасқан тапсырма операторын редукциялауға болатынын көрсетеді: Тапсырма операторын осындай позицияға жеткізу үшін ол функция қолданыстары арқылы және тапсырма операторының оң жағынан «көтеріледі» (bubble up), тиісті нүктеге жеткенше. Аралық өрнектер әртүрлі айнымалыларды жариялай алатындықтан, есептеу өрнектер үшін экструзия ережесін де талап етеді. Редукциялық семантиканың көптеген жариялымдары бағалау контекстінің ыңғайлылығымен осындай «көтерілу ережелерін» анықтайды. Мысалы, қарапайым атым бойынша шақыру тіліндегі бағалау контекстінің грамматикасы былай берілуі мүмкін: , мұнда кәдімгі өрнектерді, ал толық редукцияланған мәндерді білдіреді. Әр бағалау контексінде дәл бір «тесік» болады, онда термин тұтқындау арқылы қосылады. Контекстің пішіні осы тесікте редукция қайда жүруі мүмкін екенін көрсетеді. Бағалау контекстін пайдаланып «көтерілуді» сипаттау үшін бір аксиома жеткілікті: Бұл редукция ережесі – Felleisen және Hieb lambda-есептеуінен тапсырма операторлары үшін көтеру ережесі. Бағалау контексті бұл ережені белгілі бір терминдерге шектейді, бірақ ол кез келген терминге, тіпті lambda-лардың астында да еркін қолданылады. Плоткиннің ізімен, редукция ережелері жиынтығынан алынған есептеудің пайдалылығын көрсету үшін (1) бір қадамдық қатынас үшін Черч-Россер леммасы, ол бағалау функциясын тудырады, және (2) бағалау функциясының транзитивті рефлексивті жабылуы үшін Кьюри-Фейс стандарттау леммасы қажет, ол бағалау функциясындағы детерминистік емес іздеуді детерминистік солдан оңға/сырттан ішке қарай іздеумен алмастырады. Феллейзен осы есептеудің императивті кеңейтімдері осы теоремаларды қанағаттандыратынын көрсетті. Бұл теоремалардың салдары – теңдеу теориясы – симметриялық транзитивті рефлексивті жабылу – осы тілдер үшін дұрыс пайымдау принципі. Дегенмен, практикада редукциялық семантиканың көптеген қолданыстары есептеуді тастап, тек стандартты редукцияны (және одан алынған бағалаушыны) қолданады. Редукциялық семантика бағалау контекстінің күйді немесе ерекше басқару құрылымдарын (мысалы, бірінші сыныпты жалғастырулар) модельдеудің қарапайымдығын ескере отырып, өте пайдалы. Сонымен қатар, редукциялық семантика объектіге бағытталған тілдерді, келісім-шарт жүйелерін, ерекше жағдайларды, болашақты, қажеттілік бойынша шақыруды және көптеген басқа тілдік мүмкіндіктерді модельдеу үшін қолданылған. Редукциялық семантиканың бірнеше осындай қолданыстарын егжей-тегжейлі талқылайтын толық, қазіргі заманғы қарастыруды PLT Redex-пен Семантика инженериясында Маттиас Феллейзен, Роберт Брюс Финдлер және Мэтью Флат жасады.
To get an assignment statement into such a position it is “bubbled up” through function applications and the right hand side of assignment statements until it reaches the proper point. Since intervening expressions may declare distinct variables, the calculus also demands an extrusion rule for expressions. Most published uses of reduction semantics define such “bubble rules” with the convenience of evaluation contexts. For example, the grammar of evaluation contexts in a simple call by value language can be given as
where denotes arbitrary expressions and denotes fully reduced values. Each evaluation context includes exactly one hole into which a term is plugged in a capturing fashion. The shape of the context indicates with this hole where reduction may occur. To describe “bubbling” with the aid of evaluation contexts, a single axiom suffices:
This single reduction rule is the lift rule from Felleisen and Hieb's lambda calculus for assignment statements. The evaluation contexts restrict this rule to certain terms, but it is freely applicable in any term, including under lambdas. Following Plotkin, showing the usefulness of a calculus derived from a set of reduction rules demands (1) a Church Rosser lemma for the single step relation, which induces an evaluation function, and (2) a Curry Feys standardization lemma for the transitive reflexive closure of the single step relation, which replaces the non deterministic search in the evaluation function with a deterministic left most/outermost search. Felleisen showed that imperative extensions of this calculus satisfy these theorems. Consequences of these theorems are that the equational theory—the symmetric transitive reflexive closure—is a sound reasoning principle for these languages. However, in practice, most applications of reduction semantics dispense with the calculus and use the standard reduction only (and the evaluator that can be derived from it). Reduction semantics are particularly useful given the ease by which evaluation contexts can model state or unusual control constructs (e. g., first class continuations). In addition, reduction semantics have been used to model object oriented languages, contract systems, exceptions, futures, call by need, and many other language features. A thorough, modern treatment of reduction semantics that discusses several such applications at length is given by Matthias Felleisen, Robert Bruce Findler and Matthew Flatt in Semantics Engineering with PLT Redex.
Табиғи семантика
Үлкен қадамдық құрылымдық операциялық семантика табиғи семантика, реляциялық семантика және бағалау семантикасы деген аттармен де белгілі. Үлкен қадамдық операциялық семантиканы Жилль Кан ML-дің таза түрі Mini ML-ді ұсынғанда табиғи семантика деп атап енгізген. Үлкен қадам анықтамаларын функциялар немесе, жалпы алғанда, қатынастар анықтамалары ретінде қарастыруға болады, олар әрбір тілдік құрылымды тиісті сала (домен) шеңберінде түсіндіреді. Оның түсінікті болуы бағдарламалау тілдерінде семантиканы сипаттау үшін танымал таңдауға айналдырады, бірақ оның кейбір кемшіліктері бар, олар басқаруға көп күш жұмсалатын немесе бір уақытта орындалатын тілдер сияқты көптеген жағдайларда оны қолдануды қиын немесе мүмкін емес етеді. Үлкен қадам семантикасы тілдік құрылымдардың соңғы бағалау нәтижелерін олардың синтаксистік баламаларының (субөрімдер, субмәлімдемелер және т.б.) бағалау нәтижелерін біріктіру арқылы қалай алуға болатынын, "бөліп-басқару" әдісімен сипаттайды.
Салыстыру
Кіші және үлкен қадамдық семантика арасында бағдарламалау тілінің семантикасын анықтау үшін бірін немесе екіншісін қолайлы негіз ретінде таңдауға әсер ететін бірнеше ерекшеліктер бар. Үлкен қадамдық семантика көбінесе қарапайым болуымен (азырақ тұжырымдама ережелері қажеттігімен) артықшылыққа ие, сондай-ақ тіл үшін интерпретатордың тиімді іске асырылуымен тікелей сәйкес келеді (сондықтан Кан оларды "табиғи" деп атаған). Екеуі де, мысалы, кейбір бағдарламаны түрлендіргенде дұрыстықты сақтауды дәлелдеу сияқты жағдайларда, қарапайым дәлелдемелерге алып келуі мүмкін. Үлкен қадамдық семантиканың негізгі кемшілігі – тоқтамайтын (дивергентті) есептеулерде тұжырымдама ағашы болмайды, бұл мұндай есептеулер туралы қасиеттерді көрсетуге және дәлелдеуге мүмкіндік бермейді. Кіші қадамдық семантика бағалау процесінің егжей-тегжейін және реттілігін жақсырақ бақылауға мүмкіндік береді. Инструменттелген операциялық семантика жағдайында, бұл операциялық семантикаға тілдің орындалу кезіндегі мінез-құлқы туралы дәл теоремаларды қадағалауға және дәлелдеуге мүмкіндік береді. Осы қасиеттері кіші қадамдық семантиканы операциялық семантикаға қарсы типтік жүйенің дұрыстығын дәлелдеу кезінде ыңғайлырақ етеді.