1,721,122 research outputs found
Visions of Computer Science - BCS International Academic Conference
No full textProceedings of Visions of Computer Science - BCS International Academic Conferenc
Games as mathematics of logic and computation
Full text linkMathematical logic and theoretical computer science are the mathematical studies of logic and computation, respectively, which largely correspond to each other notably by the Curry-Howard isomorphism. However, logic and computation have been captured mainly syntactically, which may be criticized as conceptually unclear and mathematically cumbersome. For this point, the field of semantics has been developed, i.e., its main aim is to explain logic and computation by mathematical and in particular syntax-independent concepts. However, logic and computation have not yet been completely captured semantically, where a main obstacle lies in the point that proofs and programs are central in these fields, and they are dynamic, intensional concepts, but mainstream mathematics has been concerned mainly with static, extensional objects such as sets and functions, lacking in dynamic, intensional structures. Motivated by this foundational problem, the present thesis is written for the aim of establishing mathematically rigorous, syntax-independent, conceptually natural semantics of some central aspects of logic and computation, particularly their dynamics and intensionality, that have not been captured very well from a conceptual or mathematical viewpoint, for which our primary goal is to obtain a deeper understanding of logic and computation. Specifically, the thesis is concerned with concepts such as proof-normalization in logic (or reduction in computation), higher-order computability, and predicates in logic (or dependent types in computation). Our approach is based on mathematical structures developed in the field of game semantics for they are mathematically rigorous, syntax-independent, conceptually natural and exible enough to model various kinds of logic and computation in a systematic manner; also, they have a good potential to capture dynamics and intensionality of logic and computation. More concretely, we generalize, for each concept mentioned above, an existing variant of games to capture the concept, where each case is confirmed by a certain soundness or sometimes completeness theorem. Since each of the generalizations is orthogonal to one another, we may combine them into a single framework that provides a unified view on these developments. As technical achievements of the thesis, many of the generalizations give the first game-semantic interpretations of the corresponding concepts, for which we have introduced a number of novel mathematical structures and proved their properties. Also, conceptually, our games give dynamic, intensional semantics that explains various concepts and phenomena in a natural, intuitive yet mathematically precise manner, e.g., normalization of reduction, Π-, Σ- and Id-types as well as universes in Martin-Lof type theory, incompatibility of Σ-types and classical reasoning, and nonconstructivity of Univalence Axiom in homotopy type theory. Last but not least, since our mathematical structures capture logic and computation more completely, well beyond conventional game semantics, one of their implications would be the semantics-first-view: Logic and computation may be understood abstractly and syntax-independently as mathematics, viz., games, rather than as syntactic entities to be analyzed by various semantics, which is our intention behind the title of the thesis. In particular, our game-semantic approach enables an analytic study of logic and computation, as opposed to more standard synthetic ones such as categorical semantics, in the sense that it reduces the two concepts to the highly primitive notions of '(dialogical) arguments' between prover and refuter mathematicians, and '(computational) processes' between a computational agent and an environment, respectively, giving a deeper understanding of the very notion of logic and computation. The former can be seen particularly as a unity of proof theory and model theory: It gives a syntax-independent formulation of proofs that is also a computational description of models (by which we mean what formal languages refer to in a loose sense), namely strategies, where provability and validity of a formula simply coincide as the existence of a winning strategy on the corresponding game. By this unity, the central questions of soundness and completeness in logic just disappear. Furthermore, consistency of the logic which our games and strategies embody is immediate. These points demonstrate certain technical advantages (in addition to the conceptual naturality mentioned above) of our game-semantic approach to logic
Contention Resolution under Selfishness
No full textIn many communications settings, such as wired and wireless local-area
networks, when multiple users attempt to access a communication channel at the
same time, a conflict results and none of the communications are
successful. Contention resolution is the study of distributed transmission and
retransmission protocols designed to maximize notions of utility such as
channel utilization in the face of blocking communications.
An additional issue to be considered in the design of such protocols
is that selfish users may have incentive to deviate from the
prescribed behavior, if another transmission strategy increases their
utility. The work of Fiat et al.~\cite{Fiat07} addresses this issue by
constructing an asymptotically optimal incentive-compatible
protocol. However, their protocol assumes the cost of any single
transmission is zero, and the protocol completely collapses under non-zero
transmission costs.
In this paper, we treat the case of non-zero transmission cost .
We present asymptotically optimal contention resolution protocols that
are robust to selfish users, in two different channel feedback
models. Our main result is in the Collision Multiplicity Feedback
model, where after each time slot, the number of attempted
transmissions is returned as feedback to the users. In this setting,
we give a protocol that has expected cost and is in
-equilibrium, where is the number of users
In search of effectful dependent types
Full text linkReal world programming languages crucially depend on the availability of computational effects to achieve programming convenience and expressive power as well as program efficiency. Logical frameworks rely on predicates, or dependent types, to express detailed logical properties about entities. According to the Curry-Howard correspondence, programming languages and logical frameworks should be very closely related. However, a language that has both good support for real programming and serious proving is still missing from the programming languages zoo. We believe this is due to a fundamental lack of understanding of how dependent types should interact with computational effects. In this thesis, we make a contribution towards such an understanding, with a focus on semantic methods. Our first line of work concerns a dependently typed version of linear logic (which can be seen as a calculus for commutative effects). We develop a dependently typed dual intuitionistic linear logic as well as a sound and complete categorical semantics using certain indexed monoidal categories satisfying a comprehension axiom. We present a range of models, based on monoidal families, commutative effects, a double gluing construction, domains and strict functions and coherence spaces. Our second line of work develops a game semantics for dependent type theory, which had so far been missing altogether. We show that, if we work with deterministic well-bracketed history-free winning strategies, the semantics satisfies a full and faithful completeness result with respect to call-by-name dependent type theory for a hierarchy of types built from certain finite inductive families. We show that by relaxing the notion of strategy, we can further model various effects rather than the pure type theory. Our final line of work explores a generalisation of Levyâs call-by-push-value (CBPV) to encompass dependent types. We show that the syntax of CBPV naturally extends to a calculus we call dCBPV- in which types are allowed to depend on values but not computations. We show it has an elegant categorical semantics and a well-behaved operational semantics and that it admits a wide range of models arising from indexed monads on models of pure dependent type theory and from models of linear dependent type theory. By contrast with the simply typed situation, however, it does not suffice to encode call-by-value and call-by-name versions of dependent type theories with unrestricted effects. To obtain those, we need a richer calculus dCBPV+ with a Kleisli extension principle for dependent functions, which turns out to be less well-behaved from a semantic point of view.</p
Logical and topological contextuality in quantum mechanics and beyond
Full text linkThe main subjects of this thesis are non-locality and contextuality, two fundamental features of quantum mechanics that constitute valuable resources for quantum computation. Our analysis is based on Abramsky & Brandenburger's sheaf theoretic framework, which captures both these phenomena in a unified treatment and in a very general setting. This high-level description transcends quantum physics and allows to precisely characterise the notion of contextuality as the apparent paradox realised by data being locally consistent but globally inconsistent. More specifically, we aim to develop a deeper understanding of so-called logical forms of contextuality, i.e. situations where the phenomenon can be witnessed using purely logical arguments,
disregarding probabilities.
The sheaf theoretic description of logical contextuality has recently inspired the development of a topological treatment of the phenomenon based on sheaf cohomology. In this thesis, we embark on a detailed analysis of the cohomology of contextuality, exposing key shortcomings in the current methods, and introducing an (almost) complete cohomological characterisation of logical forms of contextuality. More specifically, we show that, in its current formulation, sheaf cohomology does not constitute a complete invariant for contextuality, not even in its strongest forms, and that higher cohomology groups cannot be used to study the phenomenon. Then, we solve these issues by introducing a novel construction, which derives refined versions of the presheaves describing empirical models to expose their deeper extendability properties, resulting in a sheaf cohomological invariant which is applicable to the vast majority of empirical models, and conjectured to work universally.
We propose a general theory of contextual semantics using the language of valuation algebras. In particular, we give a general definition of contextual behaviour as a fundamental gap between local agreement and global disagreement of information sources. Not only does this formalism aptly capture and generalise the known instances of contextuality beyond quantum theory, but it also provides inspiration for further applications of the phenomenon, and paves the way for the transfer of results and techniques between different fields. We give a prime example of this potential by developing faster algorithms to detect contextuality based on mainstream methods of generic inference.
Finally, we turn our attention back to instances of contextuality in quantum physics, and study strong contextuality in multi-qubit states. We give a complete combinatorial characterisation of All-vs-Nothing proofs of strong contextuality in stabiliser quantum mechanics.
This allows to produce the complete list of all stabiliser states exhibiting this kind of contextuality, which consitututes an important resource in certain models of quantum computation. Then, we extend our search for strongly contextual behaviour beyond stabiliser states, and identify the minimum quantum resources needed to realise strong non-locality. Additional results include a partial classification of strongly non-local models comprised of three-qubit states and local projective measurements, and the introduction of a new infinite family of strongly non-local three-qubit states.</p
Structural techniques in descriptive complexity
Full text linkIn 2017, Abramsky, Dawar, and Wang published a paper which gave a comonadic characterisation of pebble games, tree-width, and k-variable logic, a key trio of related concepts in Finite Model Theory. In 2018, Abramsky and Shah expanded upon this to give an analogous comonadic characterisation of Ehrenfeucht Fraisse games, tree-depth, and bounded quantifier rank logic. A key feature of these papers is the connection between two previously distinct subfields of logic in computer science; Categorical Semantics, and Finite Model Theory. This thesis applies the ideas and techniques in these papers to give a categorical account of some cornerstone results of Finite Model Theory, including Rossman’s Equirank Homomorphism Preservation Theorem, Courcelle’s Theorem (on the model-checking properties of structures of bounded tree-width), and Gaifman’s Locality Theorem
The regular histories formulation of quantum theory
Full text linkA measurement-independent formulation of quantum mechanics called ‘regular histories’ (RH) is presented, able to reproduce the predictions of the standard formalism without the need to for a quantum-classical divide or the presence of an observer. It applies to closed systems and features no wave-function collapse. Weights are assigned only to histories satisfying a criterion called ‘regularity’. As the set of regular histories is not closed under the Boolean operations this requires a new con- cept of weight, called ‘likelihood’. Remarkably, this single change is enough to overcome many of the well-known obstacles to a sensible interpretation of quantum mechanics. For example, Bell’s theorem, which makes essential use of probabilities, places no constraints on the locality properties of a theory based on likelihoods. Indeed, RH is both counter- factually definite and free from action-at-a-distance. Moreover, in RH the meaningful histories are exactly those that can be witnessed at least in principle. Since it is especially difficult to make sense of the concept of probability for histories whose occurrence is intrinsically indeterminable, this makes likelihoods easier to justify than probabilities. Interaction with the environment causes the kinds of histories relevant at the macroscopic scale of human experience to be witnessable and indeed to generate Boolean algebras of witnessable histories, on which likelihoods reduce to ordinary probabilities. Further- more, a formal notion of inference defined on regular histories satisfies, when restricted to such Boolean algebras, the classical axioms of implication, explaining our perception of a largely classical world. Even in the context of general quantum histories the rules of reasoning in RH are remark- ably intuitive. Classical logic must only be amended to reflect the fundamental premise that one cannot meaningfully talk about the occurrence of unwitnessable histories. Crucially, different histories with the same ‘physical content’ can be interpreted in the same way and independently of the family in which they are expressed. RH thereby rectifies a critical flaw of its inspiration, the consistent histories (CH) approach, which requires either an as yet unknown set selection rule or a paradigm shift towards an un- conventional picture of reality whose elements are histories-with-respect-to-a-framework. It can be argued that RH compares favourably with other proposed interpretations of quantum mechanics in that it resolves the measurement problem while retaining an essentially classical worldview without parallel universes, a framework-dependent reality or action-at-a-distance
Distributed anytime generic inference in valuation algebras
Full text linkIn this thesis, we construct a general theoretical framework for anytime inference which automatically gives us instantiations of inference in various important domains, such as Bayesian networks, relational algebras, disjunctive normal forms and set potentials in Dempster-Shafer theory. Our framework is based on local computation schemes for inference, which perform inference by message-passing on junction trees. We also undertake an analysis of distributed inference. Our theoretical framework is implemented as a software library to illustrate examples of anytime inference using the theoretical framework.
Exact inference in general is a #P-hard problem. Due to the prohibitive computational complexity, approximate inference is well-studied. In many applications a coarse approximation is sufficient. Ideally we would like such an approximation process to be anytime. In an anytime algorithm, the approximation improves monotonically with time, and the process can be interrupted and resumed without restarting. This is especially useful in domains where time may be limited such as continuous learning and robotics. While there are several domain-specific anytime algorithms, little work has been done on generalisation. It is advantageous to develop a theoretical framework which can work for several domains, including statistical and logical inference. We use the theory of generic inference, a unification of prior local computation schemes, as a starting point for our framework. In generic inference, information is represented as elements of an algebra called a valuation algebra, with certain axioms for approximate and exact inference. We introduce axioms and operations on valuation algebras to support anytime inference. We illustrate anytime inference with applications to several domains.
Computational overhead can also be reduced by making the algorithm distributed. For our algorithm, we analyse the tradeoffs between computational, communication and synchronisation costs. We give bounds on the number of processors for maximum concurrency and describe a processor assignment algorithm for optimisation of communication costs.
The overall aim of the thesis is to contribute to the study of anytime inference, and to do so in a manner that enables some measure of control over the degree of approximation and easy applicability to a wide range of domains.</p
- …
