Samson Abramsky

FSCD Conference 2024 Conference Paper

Commutation Groups and State-Independent Contextuality

• Samson Abramsky
• Serban-Ion Cercelescu
• Carmen M. Constantin

We introduce an algebraic structure for studying state-independent contextuality arguments, a key form of quantum non-classicality exemplified by the well-known Peres-Mermin magic square, and used as a source of quantum advantage. We introduce commutation groups presented by generators and relations, and analyse them in terms of a string rewriting system. There is also a linear algebraic construction, a directed version of the Heisenberg group. We introduce contextual words as a general form of contextuality witness. We characterise when contextual words can arise in commutation groups, and explicitly construct non-contextual value assignments in other cases. We give unitary representations of commutation groups as subgroups of generalized Pauli n-groups.

MFCS Conference 2022 Conference Paper

Comonadic semantics for hybrid logic

• Samson Abramsky
• Dan Marsden

Hybrid logic is a widely-studied extension of basic modal logic, which corresponds to the bounded fragment of first-order logic. We study it from two novel perspectives: (1) We apply the recently introduced paradigm of comonadic semantics, which provides a new set of tools drawing on ideas from categorical semantics which can be applied to finite model theory, descriptive complexity and combinatorics. (2) We give a novel semantic characterization of hybrid logic in terms of invariance under disjoint extensions, a minimal form of locality. A notable feature of this result is that we give a uniform proof, valid for both the finite and infinite cases.

CSL Conference 2021 Conference Paper

The Logic of Contextuality

• Samson Abramsky
• Rui Soares Barbosa

Contextuality is a key signature of quantum non-classicality, which has been shown to play a central role in enabling quantum advantage for a wide range of information-processing and computational tasks. We study the logic of contextuality from a structural point of view, in the setting of partial Boolean algebras introduced by Kochen and Specker in their seminal work. These contrast with traditional quantum logic à la Birkhoff and von Neumann in that operations such as conjunction and disjunction are partial, only being defined in the domain where they are physically meaningful. We study how this setting relates to current work on contextuality such as the sheaf-theoretic and graph-theoretic approaches. We introduce a general free construction extending the commeasurability relation on a partial Boolean algebra, i. e. the domain of definition of the binary logical operations. This construction has a surprisingly broad range of uses. We apply it in the study of a number of issues, including: - establishing the connection between the abstract measurement scenarios studied in the contextuality literature and the setting of partial Boolean algebras; - formulating various contextuality properties in this setting, including probabilistic contextuality as well as the strong, state-independent notion of contextuality given by Kochen-Specker paradoxes, which are logically contradictory statements validated by partial Boolean algebras, specifically those arising from quantum mechanics; - investigating a Logical Exclusivity Principle, and its relation to the Probabilistic Exclusivity Principle widely studied in recent work on contextuality as a step towards closing in on the set of quantum-realisable correlations; - developing some work towards a logical presentation of the Hilbert space tensor product, using logical exclusivity to capture some of its salient quantum features.

TCS Journal 2020 Journal Article

Whither semantics?

• Samson Abramsky

We discuss how mathematical semantics has evolved, and suggest some new directions for future work. As an example, we discuss some recent work on encapsulating model comparison games as comonads, in the context of finite model theory.

I&C Journal 2018 Journal Article

Game semantics for dependent types

• Matthijs Vákár
• Radha Jagadeesan
• Samson Abramsky

We present a model of dependent type theory (DTT) with Π-, 1-, Σ- and intensional Id -types, which is based on a slight variation of the (call-by-name) category of AJM-games and history-free winning well-bracketed strategies. The model satisfies Streicher's criteria of intensionality and refutes function extensionality. The principle of uniqueness of identity proofs is satisfied. We show it contains a submodel as a full subcategory which gives a faithful interpretation of DTT with Π-, 1-, Σ- and intensional Id -types and, additionally, finite inductive type families. This smaller model is fully (and faithfully) complete with respect to the syntax at the type hierarchy built without Id -types, as well as at the more general class of types where we allow for one strictly positive occurrence of an Id -type. Definability for the full type hierarchy with Id -types remains to be investigated.

CSL Conference 2018 Conference Paper

Relating Structure and Power: Comonadic Semantics for Computational Resources

• Samson Abramsky
• Nihil Shah

Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraïssé games, pebble games, and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index k is a resource parameter which bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give syntax-free characterizations of a wide range of important logical equivalences. Moreover, the coalgebras for these indexed comonads can be used to characterize key combinatorial parameters: tree-depth for the Ehrenfeucht-Fraïssé comonad, tree-width for the pebbling comonad, and synchronization-tree depth for the modal unfolding comonad. These results pave the way for systematic connections between two major branches of the field of logic in computer science which hitherto have been almost disjoint: categorical semantics, and finite and algorithmic model theory.

MFCS Conference 2017 Conference Paper

The Quantum Monad on Relational Structures

• Samson Abramsky
• Rui Soares Barbosa
• Nadish de Silva
• Octavio Zapata

Homomorphisms between relational structures play a central role in finite model theory, constraint satisfaction, and database theory. A central theme in quantum computation is to show how quantum resources can be used to gain advantage in information processing tasks. In particular, non-local games have been used to exhibit quantum advantage in boolean constraint satisfaction, and to obtain quantum versions of graph invariants such as the chromatic number. We show how quantum strategies for homomorphism games between relational structures can be viewed as Kleisli morphisms for a quantum monad on the (classical) category of relational structures and homomorphisms. We use these results to exhibit a wide range of examples of contextuality-powered quantum advantage, and to unify several apparently diverse strands of previous work.

I&C Journal 2016 Journal Article

Hardy is (almost) everywhere: Nonlocality without inequalities for almost all entangled multipartite states

• Samson Abramsky
• Carmen M. Constantin
• Shenggang Ying

We show that all n-qubit entangled states, with the exception of tensor products of single-qubit and bipartite maximally-entangled states, admit Hardy-type proofs of non-locality without inequalities or probabilities. More precisely, we show that for all such states, there are local, one-qubit observables such that the resulting probability tables are logically contextual in the sense of Abramsky and Brandenburger, this being the general form of the Hardy-type property. Moreover, our proof is constructive: given a state, we show how to produce the witnessing local observables. In fact, we give an algorithm to do this. Although the algorithm is reasonably straightforward, its proof of correctness is non-trivial. A further striking feature is that we show that n + 2 local observables suffice to witness the logical contextuality of any n-qubit state: two each for two for the parties, and one each for the remaining n − 2 parties.

CSL Conference 2015 Conference Paper

Contextuality, Cohomology and Paradox

• Samson Abramsky
• Rui Soares Barbosa
• Kohei Kishida
• Raymond Lal
• Shane Mansfield

Contextuality is a key feature of quantum mechanics that provides an important non-classical resource for quantum information and computation. Abramsky and Brandenburger used sheaf theory to give a general treatment of contextuality in quantum theory [New Journal of Physics 13 (2011) 113036]. However, contextual phenomena are found in other fields as well, for example database theory. In this paper, we shall develop this unified view of contextuality. We provide two main contributions: firstly, we expose a remarkable connection between contexuality and logical paradoxes; secondly, we show that an important class of contextuality arguments has a topological origin. More specifically, we show that "All-vs-Nothing" proofs of contextuality are witnessed by cohomological obstructions.

TCS Journal 2014 Journal Article

Events in context

• Samson Abramsky

In this short tribute to Glynn Winskel, I recall some memories of the first time we met, and describe some recent work on contextual semantics of observational systems which can be used to model quantum non-locality and contextuality, and which has been influenced by Glynn's work on event structures and presheaf semantics for concurrency.

IJCAI Conference 2013 Conference Paper

Robust Constraint Satisfaction and Local Hidden Variables in Quantum Mechanics

• Samson Abramsky
• Georg Gottlob
• Phokion G. Kolaitis

Motivated by considerations in quantum mechanics, we introduce the class of robust constraint satisfaction problems in which the question is whether every partial assignment of a certain length can be extended to a solution, provided the partial assignment does not violate any of the constraints of the given instance. We explore the complexity of specific robust colorability and robust satisfiability problems, and show that they are NPcomplete. We then use these results to establish the computational intractability of detecting local hidden-variable models in quantum mechanics.

TCS Journal 2012 Journal Article

Preface

• Samson Abramsky
• Michael Mislove
• Catuscia Palamidessi

CSL Conference 2007 Invited Paper

Full Completeness: Interactive and Geometric Characterizations of the Space of Proofs (Abstract)

• Samson Abramsky

Abstract We pursue the program of exposing the intrinsic mathematical structure of the “space of a proofs” of a logical system [AJ94b]. We study the case of Multiplicative-Additive Linear Logic (MALL). We use tools from Domain theory to develop a semantic notion of proof net for MALL, and prove a Sequentialization Theorem. We also give an interactive criterion for strategies, formalized in the same Domain-theoretic setting, to come from proofs, and show that a “semantic proof structure” satisfies the geometric correctness criterion for proof-nets if and only if it satisfies the interactive criterion for strategies. We also use the Domain-theoretic setting to give an elegant compositional account of Cut-Elimination. This work is a continuation of previous joint work with Radha Jagadeesan [AJ94b] and Paul-André Melliès [AM99].

CSL Conference 2006 Conference Paper

The Ackermann Award 2006

• Samson Abramsky
• Erich Grädel
• Johann A. Makowsky

Abstract The second Ackermann Award is presented at this CSL’06. Eligible for the 2006 Ackermann Award were PhD dissertations in topics specified by the EACSL and LICS conferences, which were formally accepted as PhD theses at a university or equivalent institution between 1. 1. 2004 and 31. 12. 2005. The jury received 14 nominations for the Ackermann Award 2006. The candidates came from 10 different nationalities from Europe, the Middle East and India, and received their PhDs in 9 different countries in Europe, Israel and North America.

TCS Journal 2005 Journal Article

A structural approach to reversible computation

• Samson Abramsky

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.

TCS Journal 2005 Journal Article

Game Theory Meets Theoretical Computer Science

• Samson Abramsky
• Marios Mavronicolas

I&C Journal 2001 Journal Article

A Domain Equation for Bisimulation

• Samson Abramsky
• Luca Aceto
• Anna Ingólfsdóttir

CSL Conference 2001 Conference Paper

Fully Complete Minimal PER Models for the Simply Typed lambda-Calculus

• Samson Abramsky
• Marina Lenisa

Abstract We show how to build a fully complete model for the maximal theory of the simply typed λ-calculus with k ground constants, λ k. This is obtained by linear realizability over an affine combinatory algebra of partial involutions from natural numbers into natural numbers. For simplicitly, we give the details of the construction of a fully complete model for λ k extended with ground permutations. The fully complete minimal model for λ k can be obtained by carrying out the previous construction over a suitable subalgebra of partial involutions. The full completeness result is then put to use in order to prove some simple results on the maximal theory.

CSL Conference 2000 Conference Paper

A Fully Complete PER Model for ML Polymorphic Types

• Samson Abramsky
• Marina Lenisa

Abstract We present a linear realizability technique for building Partial Equivalence Relations (PER) categories over Linear Combinatory Algebras. These PER categories turn out to be linear categories and to form an adjoint model with their co-Kleisli categories. We show that a special linear combinatory algebra of partial involutions, arising from Geometry of Interaction constructions, gives rise to a fully and faithfully complete model for ML polymorphic types of system F.

MFCS Conference 2000 Conference Paper

Axiomatizing Fully Complete Models for ML Polymorphic Types

• Samson Abramsky
• Marina Lenisa

Abstract We present axioms on models of system F, which are sufficient to show full completeness for ML-polymorphic types. These axioms are given for hyperdoctrine models, which arise as adjoint models, i. e. co-Kleisli categories of linear categories. Our axiomatization consists of two crucial steps. First, we axiomatize the fact that every relevant morphism in the model generates, under decomposition, a possibly infinite typed Böhm tree. Then, we introduce an axiom which rules out infinite trees from the model. Finally, we discuss the necessity of the axioms.

I&C Journal 2000 Journal Article

Full Abstraction for PCF

• Samson Abramsky
• Radha Jagadeesan
• Pasquale Malacaria

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.

TCS Journal 1999 Journal Article

Full abstraction for Idealized Algol with passive expressions

• Samson Abramsky
• Guy McCusker

A fully abstract games model of Reynolds’ Idealized Algol is described. The model gives a semantic account of the distinction between active types, such as commands, which admit side-effecting behaviour, and passive types, such as expressions, which do not.

CSL Conference 1998 Conference Paper

Call-by-Value Games

• Samson Abramsky
• Guy McCusker

Abstract A general construction of models of call-by-value from models of call-by-name computation is described. The construction makes essential use of the properties of sum types in common denotational models of call-by-name. When applied to categories of games, it yields fully abstract models of the call-by-value functional language PCF v, which can be extended to incorporate recursive types, and of a language with local references as in Standard ML.

MFCS Conference 1997 Invited Paper

Game Semantics for Programming Languages (Abstract)

• Samson Abramsky

TCS Journal 1994 Journal Article

Preface

• Samson Abramsky

TCS Journal 1994 Journal Article

Proofs as processes

• Samson Abramsky

TCS Journal 1993 Journal Article

Computational interpretations of linear logic

• Samson Abramsky

We study Girard's linear logic from the point of view of giving a concrete computational interpretation of the logic, based on the Curry—Howard isomorphism. In the case of Intuitionistic linear logic, this leads to a refinement of the lambda calculus, giving finer control over order of evaluation and storage allocation, while maintaining the logical content of programs as proofs, and computation as cut-elimination. In the classical case, it leads to a concurrent process paradigm with an operational semantics in the style of Berry and Boudol's chemical abstract machine. This opens up a promising new approach to the parallel implementation of functional programming languages; and offers the prospect of typed concurrent programming in which correctness is guaranteed by the typing.

TCS Journal 1993 Journal Article

Preface

• Samson Abramsky
• Pierre-Louis Curien

I&C Journal 1991 Journal Article

A domain equation for bisimulation

• Samson Abramsky

Some basic topics in the theory of concurrency are studied from the point of view of denotational semantics, and particularly the “domain theory in logical form” developed by the author. A domain of synchronization trees is defined by means of a recursive domain equation involving the Plotkin powerdomain. The logical counterpart of this domain is described, and shown to be related to it by Stone duality. The relationship of this domain logic to the standard Hennessy-Milner logic for transition systems is studied; the domain logic can be seen as a rational reconstruction of Hennessy-Milner logic from the standpoint of a very general and systematic theory. Finally, a denotational semantics for SCCS based on the domain of synchronization trees is given, and proved fully abstract with respect to bisimulation.

TCS Journal 1987 Journal Article

Observation equivalence as a testing equivalence

• Samson Abramsky

A notion of testing is developed for transition systems with divergence. The forms of testing include traces, refusals, copying and global testing. Both denotational and operational formulations of testing are given. The equivalence based on this notion of testing is shown to coincide with observation equivalence.