اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدGame Comonads & Generalised Quantifiers
196
0
0.0
(
0
)
نشر من قبل
Adam \\'O Conghaile
تاريخ النشر
2020
مجال البحث
الهندسة المعلوماتية
والبحث باللغة
English
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Game comonads, introduced by Abramsky, Dawar and Wang and developed by Abramsky and Shah, give an interesting categorical semantics to some Spoiler-Duplicator games that are common in finite model theory. In particular they expose connections between one-sided and two-sided games, and parameters such as treewidth and treedepth and corresponding notions of decomposition. In the present paper, we expand the realm of game comonads to logics with generalised quantifiers. In particular, we introduce a comonad graded by two parameter $n leq k$ such that isomorphisms in the resulting Kleisli category are exactly Duplicator winning strategies in Hellas $n$-bijection game with $k$ pebbles. We define a one-sided version of this game which allows us to provide a categorical semantics for a number of logics with generalised quantifiers. We also give a novel notion of tree decomposition that emerges from the construction.
قيم البحث
اقرأ أيضاً
Lovasz (1967) showed that two finite relational structures A and B are isomorphic if, and only if, the number of homomorphisms from C to A is the same as the number of homomorphisms from C to B for any finite structure C. Soon after, Pultr (1973) pro
ved a categorical generalisation of this fact. We propose a new categorical formulation, which applies to any locally finite category with pushouts and a proper factorisation system. As special cases of this general theorem, we obtain two variants of Lovasz theorem: the result by Dvov{r}ak (2010) that characterises equivalence of graphs in the k-dimensional Weisfeiler-Leman equivalence by homomorphism counts from graphs of tree-width at most k, and the result of Grohe (2020) characterising equivalence with respect to first-order logic with counting and quantifier depth k in terms of homomorphism counts from graphs of tree-depth at most k. The connection of our categorical formulation with these results is obtained by means of the game comonads of Abramsky et al. We also present a novel application to homomorphism counts in modal logic.
Automated program verification is a difficult problem. It is undecidable even for transition systems over Linear Integer Arithmetic (LIA). Extending the transition system with theory of Arrays, further complicates the problem by requiring inference a
nd reasoning with universally quantified formulas. In this paper, we present a new algorithm, Quic3, that extends IC3 to infer universally quantified invariants over the combined theory of LIA and Arrays. Unlike other approaches that use either IC3 or an SMT solver as a black box, Quic3 carefully manages quantified generalization (to construct quantified invariants) and quantifier instantiation (to detect convergence in the presence of quantifiers). While Quic3 is not guaranteed to converge, it is guaranteed to make progress by exploring longer and longer executions. We have implemented Quic3 within the Constrained Horn Clause solver engine of Z3 and experimented with it by applying Quic3 to verifying a variety of public benchmarks of array manipulating C programs.
We study the logic obtained by endowing the language of first-order arithmetic with second-order measure quantifiers. This new kind of quantification allows us to express that the argument formula is true in a certain portion of all possible interpre
tations of the quantified variable. We show that first-order arithmetic with measure quantifiers is capable of formalizing simple results from probability theory and, most importantly, of representing every recursive random function. Moreover, we introduce a realizability interpretation of this logic in which programs have access to an oracle from the Cantor space.
This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new and `wen are distinct from the s
elf-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new distributes over positive operators while `wen distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as formulae in MAV1. The technical challenge is to establish a cut elimination result, from which essential properties including the transitivity of implication follow. Since the system is defined using the calculus of structures, a generalisation of the sequent calculus, novel techniques are employed. The proof relies on an intricately designed multiset-based measure of the size of a proof, which is used to guide a normalisation technique called splitting. The presence of equivariance, which swaps successive quantifiers, induces complex inter-dependencies between nominal quantifiers, additive conjunction and multiplicative operators in the proof of splitting. Every rule is justified by an example demonstrating why the rule is necessary for soundly embedding processes and ensuring that cut elimination holds.
Game semantics is a rich and successful class of denotational models for programming languages. Most game models feature a rather intuitive setup, yet surprisingly difficult proofs of such basic results as associativity of composition of strategies.
We set out to unify these models into a basic abstract framework for game semantics, game settings. Our main contribution is the generic construction, for any game setting, of a category of games and strategies. Furthermore, we extend the framework to deal with innocence, and prove that innocent strategies form a subcategory. We finally show that our constructions cover many concrete cases, mainly among the early models and the very recent sheaf-based ones.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
