Түйінделген логика: Ресурстарды композициялау және жүйелерді талдау
Bunched logic
Бunched логикасы – компьютер жүйелерін талдауға көмектесетін, ресурстарды біріктіруге арналған логикалық құрал. Программа тексеруде, жүйелерді модельдеуде қолданылады.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Баншты логика – Питер О’Харн мен Дэвид Пим ұсынған субструктуралық логиканың бір түрі. Баншты логика ресурстардың жиынтығын талдауға қажетті бастауыш құралдарды ұсынады, бұл компьютерлік және басқа да жүйелерді құрастырып талдауға көмектеседі. Оның категориялық теориялық және шындық функциялық семантикасы бар, оны ресурстың абстрактілі түсінігі арқылы түсінуге болады. Сондай-ақ, оның дәлелдеу теориясы бар, онда Γ ⊢ A түйіндегі Γ контекстері тізімдер немесе көптеген жиынтықтар емес, ағаш тәрізді құрылымдар (топтар) болып табылады, бұл көптеген дәлелдеу есептеулерінде кездеседі. Баншты логикамен байланысты типтік теория бар, ал оның алғашқы қолданылуы императивті бағдарламаларда псевдонимдеуді және басқа да түрлі кедергілерді басқару тәсілін ұсыну болды. Бұл логика бағдарламаны тексеруде де қолданылады, ол бөліну логикасының тілдік негізін құрайды, сондай-ақ жүйелерді модельдеуде, жүйенің компоненттері қолданатын ресурстарды бөлуге мүмкіндік береді.
Bunched logic is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about resource composition, which aid in the compositional analysis of computer and other systems. It has category theoretic and truth functional semantics, which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgement Γ ⊢ A are tree like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs. The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic, and in systems modelling, where it provides a way to decompose the resources used by components of a system.
Алгебралық семантика
Топталған логиканың алгебралық семантикасы оның категориялық семантикасының ерекше жағдайы, бірақ оны түсіндіру оңай және оған қол жеткізу ықтимал. Топталған логиканың алгебралық моделі – Хейтинг алгебрасы болып табылатын және сол Хейтинг алгебрасының торы үшін қосымша коммутативті қалдық тор құрылымын (қалдық операциялары бар) қамтитын позит, яғни, реттік коммутативті моноид және сәйкес импликациясы бар. Бульдік топталған логиканың үлгілері былай болады. Бульдік топталған логиканың алгебралық моделі – Бульдік алгебра болып табылатын және қосымша қалдық коммутативті моноид құрылымын қамтитын позит.
The algebraic semantics of bunched logic is a special case of its categorical semantics, but is simple to state and can be more approachable. An algebraic model of bunched logic is a poset that is a Heyting algebra and that carries an additional commutative residuated lattice structure (for the same lattice as the Heyting algebra): that is, an ordered commutative monoid with an associated implication satisfying The boolean version of bunched logic has models as follows. An algebraic model of boolean bunched logic is a poset that is a Boolean algebra and that carries an additional residuated commutative monoid structure.
Ғарыштық логика
Карделли, Кайрес, Гордон және басқалар процестік есептеулердің логикасын зерттеді, онда конъюнкция параллель композиция арқылы түсіндіріледі. Pym және авторлар тобының SCRP жұмысынан айырмашылығы, олар жүйелердің параллель композициясы мен жүйелер пайдаланатын ресурстардың композициясы арасында ешқандай айырма жасамайды. Олардың логикасы ресурстық семантиканың мысалдарына негізделген, олар бульдік логиканың бульдік түрінің модельдерін құрайды. Бұл логикалар бульдік топталған логиканың мысалдарына әкелгенімен, олар тәуелсіз түрде алынған сияқты көрінеді және қандай жағдайда болса да, модальдықтар мен байланыстырушылар тұрғысынан маңызды қосымша құрылымға ие. XML деректерін модельдеу үшін де ұқсас логикалар ұсынылған.
Cardelli, Caires, Gordon and others have investigated a series of logics of process calculi, where a conjunction is interpreted in terms of parallel composition. Unlike the work of Pym et al. in SCRP, they do not distinguish between parallel composition of systems and composition of resources accessed by the systems. Their logics are based on instances of the resource semantics that give rise to models of the boolean variant of bunched logic. Although these logics give rise to instances of boolean bunched logic, they appear to have been arrived at independently, and in any case have significant additional structure in the way of modalities and binders. Related logics have been proposed as well for modelling XML data.