Searcharxiv⌕ Search

arXiv subjects

Samson Abramsky

Publications and source records attributed to Samson Abramsky.

At least 73 records · Page 4Linked to original sources
arXiv2014

Full Abstraction for PCF

An intensional model for the programming language PCF is described, in which the types of PCF are interpreted by games, and the terms by certain "history-free" strategies. This model is shown to capture definability in PCF. More precisely, every compact strategy in the model is definable in a certain simple extension of PCF. We then introduce an intrinsic preorder on strategies, and show that it satisfies some striking properties, such that the intrinsic preorder on function types coincides with the pointwise preorder. We then obtain an order-extensional fully abstract model of PCF by quotienting the intensional model by the intrinsic preorder. This is the first syntax-independent description of the fully abstract model for PCF. (Hyland and Ong have obtained very similar results by a somewhat different route, independently and at the same time). We then consider the effective version of our model, and prove a Universality Theorem: every element of the effective extensional model is definable in PCF. Equivalently, every recursive strategy is definable up to observational equivalence.

cs.LO↗
arXiv2014

Retracing some paths in Process Algebra

We use traced monoidal categories to give a precise general version of "geometry of interaction". We give a number of examples of both "particle-style" and "wave-style" instances of this construction. We relate these ideas to semantics of computation.

cs.LO↗
arXiv2014

An Operational Interpretation of Negative Probabilities and No-Signalling Models

Negative probabilities have long been discussed in connection with the foundations of quantum mechanics. We have recently shown that, if signed measures are allowed on the hidden variables, the class of probability models which can be captured by local hidden-variable models are exactly the no-signalling models. However, the question remains of how negative probabilities are to be interpreted. In this paper, we present an operational interpretation of negative probabilities as arising from standard probabilities on signed events. This leads, by virtue of our previous result, to a systematic scheme for simulating arbitrary no-signalling models.

quant-ph↗
arXiv2013

A Game Semantics for Generic Polymorphism

Genericity is the idea that the same program can work at many different data types. Longo, Milstead and Soloviev proposed to capture the inability of generic programs to probe the structure of their instances by the following equational principle: if two generic programs, viewed as terms of type $\forall X. \, A[X]$, are equal at any given instance $A[T]$, then they are equal at all instances. They proved that this rule is admissible in a certain extension of System F, but finding a semantically motivated model satisfying this principle remained an open problem. In the present paper, we construct a categorical model of polymorphism, based on game semantics, which contains a large collection of generic types. This model builds on two novel constructions: -- A direct interpretation of variable types as games, with a natural notion of substitution of games. This allows moves in games A[T] to be decomposed into the generic part from A, and the part pertaining to the instance T. This leads to a simple and natural notion of generic strategy. -- A "relative polymorphic product" which expresses quantification over the type variable X in the variable type A with respect to a "universe'" which is explicitly given as an additional parameter B. We then solve a recursive equation involving this relative product to obtain a universe in a suitably "absolute" sense. Full Completeness for ML types (universal closures of quantifier-free types) is proved for this model.

cs.LO↗
arXiv2013

Semantics of Interaction

This is an introduction to Game Semantics based on some lecture notes given at the CLiCS II summer school in Cambridge in 1995. We will focus on the recent (1994) work on Game semantics, which has led to some striking advances in the Full Abstraction problem for PCF and other programming languages. Our aim is to give a genuinely elementary first introduction; we therefore present a simplified version of game semantics, which nonetheless contains most of the essential concepts. The more complex game semantics used by Abramsky, Jagadeesan and Malacaria and by Hyland and Ong to construct fully abstract models for PCF can be seen as refinements of what we present. Some background in category theory, type theory and linear logic would be helpful in reading these notes.

cs.LO↗
arXiv2013

Games and Full Completeness for Multiplicative Linear Logic

We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of {\em history-free} strategy; strong connections are made between history-free strategies and the Geometry of Interaction. Our semantics incorporates a natural notion of polarity, leading to a refined treatment of the additives. We make comparisons with related work by Joyal, Blass et al.

cs.LO↗
arXiv2013

Relational Databases and Bell's Theorem

Our aim in this paper is to point out a surprising formal connection, between two topics which seem on face value to have nothing to do with each other: relational database theory, and the study of non-locality and contextuality in the foundations of quantum mechanics. We shall show that there is a remarkably direct correspondence between central results such as Bell's theorem in the foundations of quantum mechanics, and questions which arise naturally and have been well-studied in relational database theory.

cs.LO↗
arXiv2013

Operational theories and Categorical quantum mechanics

A central theme in current work in quantum information and quantum foundations is to see quantum mechanics as occupying one point in a space of possible theories, and to use this perspective to understand the special features and properties which single it out, and the possibilities for alternative theories. Two formalisms which have been used in this context are operational theories, and categorical quantum mechanics. The aim of the present paper is to establish strong connections between these two formalisms. We show how models of categorical quantum mechanics have representations as operational theories. We then show how nonlocality can be formulated at this level of generality, and study a number of examples from this point of view, including Hilbert spaces, sets and relations, and stochastic maps. The local, quantum, and no-signalling models are characterized in these terms.

quant-ph↗
arXiv2013

Coalgebraic Analysis of Subgame-perfect Equilibria in Infinite Games without Discounting

We present a novel coalgebraic formulation of infinite extensive games. We define both the game trees and the strategy profiles by possibly infinite systems of corecursive equations. Certain strategy profiles are proved to be subgame perfect equilibria using a novel proof principle of predicate coinduction. We characterize all subgame perfect equilibria for the dollar auction game. The economically interesting feature is that in order to prove these results we do not need to rely on continuity assumptions on the payoffs which amount to discounting the future. In particular, we prove a form of one-deviation principle without any such assumptions. This suggests that coalgebra supports a more adequate treatment of infinite-horizon models in game theory and economics.

cs.GT↗
arXiv2012

The Cohomology of Non-Locality and Contextuality

In a previous paper with Adam Brandenburger, we used sheaf theory to analyze the structure of non-locality and contextuality. Moreover, on the basis of this formulation, we showed that the phenomena of non-locality and contextuality can be characterized precisely in terms of obstructions to the existence of global sections. Our aim in the present work is to build on these results, and to use the powerful tools of sheaf cohomology to study the structure of non-locality and contextuality. We use the Cech cohomology on an abelian presheaf derived from the support of a probabilistic model, viewed as a compatible family of distributions, in order to define a cohomological obstruction for the family as a certain cohomology class. This class vanishes if the family has a global section. Thus the non-vanishing of the obstruction provides a sufficient (but not necessary) condition for the model to be contextual. We show that for a number of salient examples, including PR boxes, GHZ states, the Peres-Mermin magic square, and the 18-vector configuration due to Cabello et al. giving a proof of the Kochen-Specker theorem in four dimensions, the obstruction does not vanish, thus yielding cohomological witnesses for contextuality.

quant-ph↗
arXiv2012

Logical Bell Inequalities

Bell inequalities play a central role in the study of quantum non-locality and entanglement, with many applications in quantum information. Despite the huge literature on Bell inequalities, it is not easy to find a clear conceptual answer to what a Bell inequality is, or a clear guiding principle as to how they may be derived. In this paper, we introduce a notion of logical Bell inequality which can be used to systematically derive testable inequalities for a very wide variety of situations. There is a single clear conceptual principle, based on purely logical consistency conditions, which underlies our notion of logical Bell inequalities. We show that in a precise sense, all Bell inequalities can be taken to be of this form. Our approach is very general. It applies directly to any family of sets of commuting observables. Thus it covers not only the n-partite scenarios to which Bell inequalities are standardly applied, but also Kochen-Specker configurations, and many other examples. There is much current work on experimental tests for contextuality. Our approach directly yields, in a systematic fashion, testable inequalities for a very general notion of contextuality. There has been much work on obtaining proofs of Bell's theorem `without inequalities' or `without probabilities'. These proofs are seen as being in a sense more definitive and logically robust than the inequality-based proofs. On the hand, they lack the fault-tolerant aspect of inequalities. Our approach reconciles these aspects, and in fact shows how the logical robustness can be converted into systematic, general derivations of inequalities with provable violations. Moreover, the kind of strong non-locality or contextuality exhibited by the GHZ argument or by Kochen-Specker configurations can be shown to lead to maximal violations of the corresponding logical Bell inequalities.

quant-ph↗
arXiv2012

No-Cloning In Categorical Quantum Mechanics

Recently, the author and Bob Coecke have introduced a categorical formulation of Quantum Mechanics. In the present paper, we shall use it to open up a novel perspective on No-Cloning. What we shall find, quite unexpectedly, is a link to some fundamental issues in logic, computation, and the foundations of mathematics. A striking feature of our results is that they are visibly in the same genre as a well-known result by Joyal in categorical logic showing that a `Boolean cartesian closed category' trivializes, which provides a major road-block to the computational interpretation of classical logic. In fact, they strengthen Joyal's result, insofar as the assumption of a full categorical product (both diagonals and projections) in the presence of a classical duality is weakened. This shows a heretofore unsuspected connection between limitative results in proof theory and No-Go theorems in quantum mechanics.

quant-ph↗
arXiv2011

A Generalized Kahn Principle for Abstract Asynchronous Networks

Our general motivation is to answer the question: "What is a model of concurrent computation?". As a preliminary exercise, we study dataflow networks. We develop a very general notion of model for asynchronous networks. The "Kahn Principle", which states that a network built from functional nodes is the least fixpoint of a system of equations associated with the network, has become a benchmark for the formal study of dataflow networks. We formulate a generalized version of the Kahn Principle, which applies to a large class of non-deterministic systems, in the setting of abstract asynchronous networks; and prove that the Kahn Principle holds under certain natural assumptions on the model. We also show that a class of models, which represent networks that compute over arbitrary event structures, generalizing dataflow networks which compute over streams, satisfy these assumptions.

cs.LO↗
arXiv2011

A Cook's Tour of the Finitary Non-Well-Founded Sets

We give multiple descriptions of a topological universe of finitary sets, which can be seen as a natural limit completion of the hereditarily finite sets. This universe is characterized as a metric completion of the hereditarily finite sets; as a Stone space arising as the solution of a functorial fixed-point equation involving the Vietoris construction; as the Stone dual of the free modal algebra; and as the subspace of maximal elements of a domain equation involving the Plotkin (or convex) powerdomain. These results illustrate the methods developed in the author's 'Domain theory in logical form', and related literature, and have been taken up in recent work on topological coalgebras. The set-theoretic universe of finitary sets also supports an interesting form of set theory. It contains non-well founded sets and a universal set; and is closed under positive versions of the usual axioms of set theory.

cs.LO↗
arXiv2011

Domain Theory and the Logic of Observable Properties

The mathematical framework of Stone duality is used to synthesize a number of hitherto separate developments in Theoretical Computer Science: - Domain Theory, the mathematical theory of computation introduced by Scott as a foundation for denotational semantics. - The theory of concurrency and systems behaviour developed by Milner, Hennessy et al. based on operational semantics. - Logics of programs. Stone duality provides a junction between semantics (spaces of points = denotations of computational processes) and logics (lattices of properties of processes). Moreover, the underlying logic is geometric, which can be computationally interpreted as the logic of observable properties---i.e. properties which can be determined to hold of a process on the basis of a finite amount of information about its execution. These ideas lead to the following programme: 1. A metalanguage is introduced, comprising - types = universes of discourse for various computational situations. - terms = programs = syntactic intensions for models or points. 2. A standard denotational interpretation of the metalanguage is given, assigning domains to types and domain elements to terms. 3. The metalanguage is also given a {\em logical} interpretation, in which types are interpreted as propositional theories and terms are interpreted via a program logic, which axiomatizes the properties they satisfy. 4. The two interpretations are related by showing that they are Stone duals of each other. Hence, semantics and logic are guaranteed to be in harmony with each other, and in fact each determines the other up to isomorphism. This opens the way to a whole range of applications. Given a denotational description of a computational situation in our meta-language, we can turn the handle to obtain a logic for that situation.

cs.LO↗
arXiv2011

A Structural Approach to Reversible Computation

Reversibility is a key issue in the interface between computation and physics, and of growing importance as miniaturization progresses towards its physical limits. Most foundational work on reversible computing to date has focussed on simulations of low-level machine models. By contrast, we develop a more structural approach. We show how high-level functional programs can be mapped compositionally (i.e. in a syntax-directed fashion) into a simple kind of automata which are immediately seen to be reversible. The size of the automaton is linear in the size of the functional term. In mathematical terms, we are building a concrete model of functional computation. This construction stems directly from ideas arising in Geometry of Interaction and Linear Logic---but can be understood without any knowledge of these topics. In fact, it serves as an excellent introduction to them. At the same time, an interesting logical delineation between reversible and irreversible forms of computation emerges from our analysis.

cs.LO↗