Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Классикалық емес логикалық жүйелер үшін формалды семантика
Formal semantics for non classical logic systems
Крипке семантикасы (сондай-ақ реляциялық семантика немесе кадрлық семантика деп аталады және көбінесе мүмкін әлемдер семантикасымен шатастырылады) – Саул Крипке және Андре Джойалдың 1950-ші жылдардың соңы мен 1960-шы жылдардың басында жасаған классикалық емес логикалық жүйелерге арналған формалды семантика. Алғаш рет модальдық логика үшін құрастырылған, кейін интуиционистік логика және басқа классикалық емес жүйелерге бейімделген. Крипке семантикасының дамуы классикалық емес логикалар теориясындағы маңызды қадам болды, себебі Крипкеге дейін мұндай логикалардың модельдік теориясы дерлік болған жоқ (алгебралық семантика болған, бірақ ол "жасырын синтаксис" деп есептелген).
Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Joyal. It was first conceived for modal logics, and later adapted to intuitionistic logic and other non classical systems. The development of Kripke semantics was a breakthrough in the theory of non classical logics, because the model theory of such logics was almost non existent before Kripke (algebraic semantics existed, but were considered 'syntax in disguise').
Модальдық логиканың семантикасы
Пропозициялық модальдық логика тілі санаулы сансыз пропозициялық айнымалылар жиынтығынан, шындық функционалдық байланыстырушылар жиынтығынан (осы мақалада және ) және модальдық оператордан ("қажетті") тұрады. Модальдық оператор ("мүмкін") (классикалық түрде) "қажетті" операторының дуалы болып табылады және қажеттілік арқылы былай анықталуы мүмкін: ("мүмкін A" "қажетті емес емес A" дегенмен эквивалентті деп анықталады).
The language of propositional modal logic consists of a countably infinite set of propositional variables, a set of truth functional connectives (in this article and ), and the modal operator ("necessarily"). The modal operator ("possibly") is (classically) the dual of and may be defined in terms of necessity like so: ("possibly A" is defined as equivalent to "not necessarily not A").
Крипке Джойал семантикасы
Ботақ теориясының тәуелсіз дамуының бір бөлігі ретінде 1965 жыл шамасында Крипке семантикасының топос теориясындағы экзистенциалдық квантификацияны қарастырумен тығыз байланысты екендігі анықталды. Яғни, ботақтың қималары үшін өмір сүрудің "жергілікті" сипаты "мүмкін" логикасының бір түрі болды. Бұл даму бірнеше адамның еңбегінің нәтижесі болғанмен, осы контексте Kripke–Joyal семантикасы деген атау жиі қолданылады.
As part of the independent development of sheaf theory, it was realised around 1965 that Kripke semantics was intimately related to the treatment of existential quantification in topos theory. That is, the 'local' aspect of existence for sections of a sheaf was a kind of logic of the 'possible'. Though this development was the work of a number of people, the name Kripke–Joyal semantics is often used in this connection.
Жалпы кадр семантикасы
Крипке семантикасының басты кемшілігі – Крипке-толық емес логикалардың және толық болғанымен, бірақ тұтас емес логикалардың болуы. Бұл кемшілікті Крипке жүйелерін алгебралық семантикадан алынған идеялар арқылы, мүмкін болатын бағалаулар жиынтығын шектейтін қосымша құрылыммен жабдықтау арқылы жоюға болады. Осылайша, жалпы жүйе семантикасы пайда болады.
The main defect of Kripke semantics is the existence of Kripke incomplete logics, and logics which are complete but not compact. It can be remedied by equipping Kripke frames with extra structure which restricts the set of possible valuations, using ideas from algebraic semantics. This gives rise to the general frame semantics.
Компьютерлік ғылымның қолданбалары
Блэкберн және басқалар (2001) атап көрсетеді, қатынастық құрылым – бұл жай ғана жиын және осы жиынға қатысты қатынастар жиынтығы болғандықтан, қатынастық құрылымдарды кез келген жерде кездестіруге болады. Теориялық компьютерлік ғылымнан мысал ретінде олар бағдарламаның орындалуын модельдейтін белгіленген ауысу жүйелерін келтіреді. Осы байланысқа сүйене отырып, Блэкберн және басқалар модальдық тілдердің қатынастық құрылымдарға «ішкі, жергілікті перспективаны» ұсынуға ең қолайлы екенін айтады (XII бет).
Blackburn et al. (2001) point out that because a relational structure is simply a set together with a collection of relations on that set, it is unsurprising that relational structures are to be found just about everywhere. As an example from theoretical computer science, they give labeled transition systems, which model program execution. Blackburn et al. thus claim because of this connection that modal languages are ideally suited in providing "internal, local perspective on relational structures." (p. xii)