-
An invitation to game comonads
Authors:
Samson Abramsky,
Luca Reggio
Abstract:
Game comonads offer a categorical view of a number of model-comparison games central to model theory, such as pebble and Ehrenfeucht-Fraïssé games. Remarkably, the categories of coalgebras for these comonads capture preservation of several fragments of resource-bounded logics, such as (infinitary) first-order logic with n variables or bounded quantifier rank, and corresponding combinatorial parame…
▽ More
Game comonads offer a categorical view of a number of model-comparison games central to model theory, such as pebble and Ehrenfeucht-Fraïssé games. Remarkably, the categories of coalgebras for these comonads capture preservation of several fragments of resource-bounded logics, such as (infinitary) first-order logic with n variables or bounded quantifier rank, and corresponding combinatorial parameters such as tree-width and tree-depth. In this way, game comonads provide a new bridge between categorical methods developed for semantics, and the combinatorial and algorithmic methods of resource-sensitive model theory.
We give an overview of this framework and outline some of its applications, including the study of homomorphism counting results in finite model theory, and of equi-resource homomorphism preservation theorems in logic using the axiomatic setting of arboreal categories. Finally, we describe some homotopical ideas that arise naturally in the context of game comonads.
△ Less
Submitted 30 June, 2024;
originally announced July 2024.
-
Game Semantics for Higher-Order Unitary Quantum Computation
Authors:
Samson Abramsky,
Radha Jagadeesan
Abstract:
We develop a symmetric monoidal closed category of games, incorporating sums and products, to model quantum computation at higher types. This model is expressive, capable of representing all unitary operators at base types. It is compatible with base types and realizable by unitary operators.
We develop a symmetric monoidal closed category of games, incorporating sums and products, to model quantum computation at higher types. This model is expressive, capable of representing all unitary operators at base types. It is compatible with base types and realizable by unitary operators.
△ Less
Submitted 9 April, 2024;
originally announced April 2024.
-
Combining contextuality and causality: a game semantics approach
Authors:
Samson Abramsky,
Rui Soares Barbosa,
Amy Searle
Abstract:
We develop an approach to combining contextuality with causality, which is general enough to cover causal background structure, adaptive measurement-based quantum computation, and causal networks. The key idea is to view contextuality as arising from a game played between Experimenter and Nature, allowing for causal dependencies in the actions of both the Experimenter (choice of measurements) and…
▽ More
We develop an approach to combining contextuality with causality, which is general enough to cover causal background structure, adaptive measurement-based quantum computation, and causal networks. The key idea is to view contextuality as arising from a game played between Experimenter and Nature, allowing for causal dependencies in the actions of both the Experimenter (choice of measurements) and Nature (choice of outcomes).
△ Less
Submitted 26 January, 2024; v1 submitted 10 July, 2023;
originally announced July 2023.
-
Linear Arboreal Categories
Authors:
Samson Abramsky,
Yoàv Montacute,
Nihil Shah
Abstract:
Arboreal categories, introduced by Abramsky and Reggio, axiomatise categories with tree-shaped objects. These categories provide a categorical language for formalising behavioural notions such as simulation, bisimulation, and resource-indexing. In this paper, we strengthen the axioms of an arboreal category to exclude `branching' behaviour, obtaining a notion of `linear arboreal category'. We then…
▽ More
Arboreal categories, introduced by Abramsky and Reggio, axiomatise categories with tree-shaped objects. These categories provide a categorical language for formalising behavioural notions such as simulation, bisimulation, and resource-indexing. In this paper, we strengthen the axioms of an arboreal category to exclude `branching' behaviour, obtaining a notion of `linear arboreal category'. We then demonstrate that every arboreal category satisfying a linearisability condition has an associated linear arboreal subcategory related via an adjunction. This identifies the relationship between the pebble-relation comonad, of Montacute and Shah, and the pebbling comonad, of Abramsky, Dawar, and Wang, and generalises it further. As another outcome of this new framework, we obtain a linear variant of the arboreal category for modal logic. By doing so we recover different linear-time equivalences between transition systems as instances of their categorical definitions. We conclude with new preservation and characterisation theorems relating trace inclusion and trace equivalence with different linear fragments of modal logic.
△ Less
Submitted 29 March, 2024; v1 submitted 24 January, 2023;
originally announced January 2023.
-
Notes on presheaf representations of strategies and cohomological refinements of $k$-consistency and $k$-equivalence
Authors:
Samson Abramsky
Abstract:
In this note, we show how positional strategies for $k$-pebble games have a natural representation as certain presheaves. These representations correspond exactly to the sheaf-theoretic models of contextuality introduced by Abramsky-Brandenburger. We study the notion of cohomological $k$-consistency recently introduced by Adam O' Conghaile from this perspective.
In this note, we show how positional strategies for $k$-pebble games have a natural representation as certain presheaves. These representations correspond exactly to the sheaf-theoretic models of contextuality introduced by Abramsky-Brandenburger. We study the notion of cohomological $k$-consistency recently introduced by Adam O' Conghaile from this perspective.
△ Less
Submitted 24 June, 2022;
originally announced June 2022.
-
Robin Milner's Work on Concurrency: An Appreciation
Authors:
Samson Abramsky
Abstract:
We give a short appreciation of Robin Milner's seminal contributions to the theory of concurrency.
We give a short appreciation of Robin Milner's seminal contributions to the theory of concurrency.
△ Less
Submitted 18 June, 2022;
originally announced June 2022.
-
Structure and Power: an emerging landscape
Authors:
Samson Abramsky
Abstract:
In this paper, we give an overview of some recent work on applying tools from category theory in finite model theory, descriptive complexity, constraint satisfaction, and combinatorics. The motivations for this work come from Computer Science, but there may also be something of interest for model theorists and other logicians.
The basic setting involves studying the category of relational struct…
▽ More
In this paper, we give an overview of some recent work on applying tools from category theory in finite model theory, descriptive complexity, constraint satisfaction, and combinatorics. The motivations for this work come from Computer Science, but there may also be something of interest for model theorists and other logicians.
The basic setting involves studying the category of relational structures via a resource-indexed family of adjunctions with some process category - which unfolds relational structures into treelike forms, allowing natural resource parameters to be assigned to these unfoldings. One basic instance of this scheme allows us to recover, in a purely structural, syntax-free way: the Ehrenfeucht-Fraisse~game; the quantifier rank fragments of first-order logic; the equivalences on structures induced by (i) the quantifier rank fragments, (ii) the restriction of this fragment to the existential positive part, and (iii) the extension with counting quantifiers; and the combinatorial parameter of tree-depth (Nesetril and Ossona de Mendez). Another instance recovers the k-pebble game, the finite-variable fragments, the corresponding equivalences, and the combinatorial parameter of treewidth. Other instances cover modal, guarded and hybrid fragments, generalized quantifiers, and a wide range of combinatorial parameters. This whole scheme has been axiomatized in a very general setting, of arboreal categories and arboreal covers.
Beyond this basic level, a landscape is beginning to emerge, in which structural features of the resource categories, adjunctions and comonads are reflected in degrees of logical and computational tractability of the corresponding languages. Examples include semantic characterisation and preservation theorems, and Lovasz-type results on counting homomorphisms.
△ Less
Submitted 3 October, 2022; v1 submitted 15 June, 2022;
originally announced June 2022.
-
Discrete density comonads and graph parameters
Authors:
Samson Abramsky,
Tomáš Jakl,
Thomas Paine
Abstract:
Game comonads have brought forth a new approach to studying finite model theory categorically. By representing model comparison games semantically as comonads, they allow important logical and combinatorial properties to be exressed in terms of their Eilenberg-Moore coalgebras. As a result, a number of results from finite model theory, such as preservation theorems and homomorphism counting theore…
▽ More
Game comonads have brought forth a new approach to studying finite model theory categorically. By representing model comparison games semantically as comonads, they allow important logical and combinatorial properties to be exressed in terms of their Eilenberg-Moore coalgebras. As a result, a number of results from finite model theory, such as preservation theorems and homomorphism counting theorems, have been formalised and parameterised by comonads, giving rise to new results simply by varying the comonad.
In this paper we study the limits of the comonadic approach in the combinatorial and homomorphism-counting aspect of the theory, regardless of whether any model comparison games are involved. We show that any standard graph parameter has a corresponding comonad, classifying the same class. This comonad is constructed via a simple Kan extension formula, making it the initial solution to this problem and, furthermore, automatically admitting a homomorphism-counting theorem.
△ Less
Submitted 25 May, 2022; v1 submitted 13 May, 2022;
originally announced May 2022.
-
Comonadic semantics for hybrid logic and bounded fragments
Authors:
Samson Abramsky,
Dan Marsden
Abstract:
In recent work, comonads and associated structures have been used to analyse a range of important notions in finite model theory, descriptive complexity and combinatorics. We extend this analysis to Hybrid logic, a widely-studied extension of basic modal logic, which corresponds to the bounded fragment of first-order logic. In addition to characterising the various resource-indexed equivalences in…
▽ More
In recent work, comonads and associated structures have been used to analyse a range of important notions in finite model theory, descriptive complexity and combinatorics. We extend this analysis to Hybrid logic, a widely-studied extension of basic modal logic, which corresponds to the bounded fragment of first-order logic. In addition to characterising the various resource-indexed equivalences induced by Hybrid logic and the bounded fragment, and the associated combinatorial decompositions of structures, we also give model-theoretic characterisations of bounded formulas in terms of invariance under generated substructures, in both the finite and infinite cases.
△ Less
Submitted 19 October, 2021;
originally announced October 2021.
-
On the Quantum-like Contextuality of Ambiguous Phrases
Authors:
Daphne Wang,
Mehrnoosh Sadrzadeh,
Samson Abramsky,
Victor H. Cervantes
Abstract:
Language is contextual as meanings of words are dependent on their contexts. Contextuality is, concomitantly, a well-defined concept in quantum mechanics where it is considered a major resource for quantum computations. We investigate whether natural language exhibits any of the quantum mechanics' contextual features. We show that meaning combinations in ambiguous phrases can be modelled in the sh…
▽ More
Language is contextual as meanings of words are dependent on their contexts. Contextuality is, concomitantly, a well-defined concept in quantum mechanics where it is considered a major resource for quantum computations. We investigate whether natural language exhibits any of the quantum mechanics' contextual features. We show that meaning combinations in ambiguous phrases can be modelled in the sheaf-theoretic framework for quantum contextuality, where they can become possibilistically contextual. Using the framework of Contextuality-by-Default (CbD), we explore the probabilistic variants of these and show that CbD-contextuality is also possible.
△ Less
Submitted 19 July, 2021;
originally announced July 2021.
-
Arboreal Categories: An Axiomatic Theory of Resources
Authors:
Samson Abramsky,
Luca Reggio
Abstract:
Game comonads provide a categorical syntax-free approach to finite model theory, and their Eilenberg-Moore coalgebras typically encode important combinatorial parameters of structures. In this paper, we develop a framework whereby the essential properties of these categories of coalgebras are captured in a purely axiomatic fashion. To this end, we introduce arboreal categories, which have an intri…
▽ More
Game comonads provide a categorical syntax-free approach to finite model theory, and their Eilenberg-Moore coalgebras typically encode important combinatorial parameters of structures. In this paper, we develop a framework whereby the essential properties of these categories of coalgebras are captured in a purely axiomatic fashion. To this end, we introduce arboreal categories, which have an intrinsic process structure, allowing dynamic notions such as bisimulation and back-and-forth games, and resource notions such as number of rounds of a game, to be defined. These are related to extensional or "static" structures via arboreal covers, which are resource-indexed comonadic adjunctions. These ideas are developed in a general, axiomatic setting, and applied to relational structures, where the comonadic constructions for pebbling, Ehrenfeucht-Fraïssé and modal bisimulation games recently introduced by Abramsky et al. are recovered, showing that many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers.
△ Less
Submitted 9 August, 2023; v1 submitted 16 February, 2021;
originally announced February 2021.
-
Contextuality: At the Borders of Paradox
Authors:
Samson Abramsky
Abstract:
Contextuality is a key feature of quantum mechanics. We present the sheaf-theoretic approach to contextuality introduced by Abramsky and Brandenburger, and show how it covers a range of logical and physical phenomena "at the borders of paradox".
Contextuality is a key feature of quantum mechanics. We present the sheaf-theoretic approach to contextuality introduced by Abramsky and Brandenburger, and show how it covers a range of logical and physical phenomena "at the borders of paradox".
△ Less
Submitted 7 November, 2020;
originally announced November 2020.
-
The logic of contextuality
Authors:
Samson Abramsky,
Rui Soares Barbosa
Abstract:
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 traditio…
▽ More
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.
△ Less
Submitted 5 November, 2020;
originally announced November 2020.
-
Whither Semantics?
Authors:
Samson Abramsky
Abstract:
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.
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.
△ Less
Submitted 23 October, 2020;
originally announced October 2020.
-
Classical logic, classical probability, and quantum mechanics
Authors:
Samson Abramsky
Abstract:
We give an overview and conceptual discussion of some of our results on contextuality and non-locality. We focus in particular on connections with the work of Itamar Pitowsky on correlation polytopes, Bell inequalities, and Boole's "conditions of possible experience".
We give an overview and conceptual discussion of some of our results on contextuality and non-locality. We focus in particular on connections with the work of Itamar Pitowsky on correlation polytopes, Bell inequalities, and Boole's "conditions of possible experience".
△ Less
Submitted 23 October, 2020;
originally announced October 2020.
-
Relating Structure and Power: Extended Version
Authors:
Samson Abramsky,
Nihil Shah
Abstract:
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-Fraisse 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 rela…
▽ More
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-Fraisse 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-Fraisse 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.
△ Less
Submitted 24 July, 2021; v1 submitted 13 October, 2020;
originally announced October 2020.
-
Comonadic semantics for guarded fragments
Authors:
Samson Abramsky,
Dan Marsden
Abstract:
In previous work, Abramsky, Dawar and Wang (LiCS 2017) and Abramsky and Shah (CSL 2018) have shown how a range of model comparison games which play a central role in finite model theory, including Ehrenfeucht-Fraisse, pebbling, and bisimulation games, can be captured in terms of resource-indexed comonads on the category of relational structures. Moreover, the coalgebras for these comonads capture…
▽ More
In previous work, Abramsky, Dawar and Wang (LiCS 2017) and Abramsky and Shah (CSL 2018) have shown how a range of model comparison games which play a central role in finite model theory, including Ehrenfeucht-Fraisse, pebbling, and bisimulation games, can be captured in terms of resource-indexed comonads on the category of relational structures. Moreover, the coalgebras for these comonads capture important combinatorial parameters such as tree-width and tree-depth.
The present paper extends this analysis to quantifier-guarded fragments of first-order logic. We give a systematic account, covering atomic, loose and clique guards. In each case, we show that coKleisli morphisms capture winning strategies for Duplicator in the existential guarded bisimulation game, while back-and-forth bisimulation, and hence equivalence in the full guarded fragment, is captured by spans of open morphisms. We study the coalgebras for these comonads, and show that they correspond to guarded tree decompositions. We relate these constructions to a syntax-free setting, with a comonad on the category of hypergraphs.
△ Less
Submitted 13 May, 2021; v1 submitted 25 August, 2020;
originally announced August 2020.
-
A comonadic view of simulation and quantum resources
Authors:
Samson Abramsky,
Rui Soares Barbosa,
Martti Karvonen,
Shane Mansfield
Abstract:
We study simulation and quantum resources in the setting of the sheaf-theoretic approach to contextuality and non-locality. Resources are viewed behaviourally, as empirical models. In earlier work, a notion of morphism for these empirical models was proposed and studied. We generalize and simplify the earlier approach, by starting with a very simple notion of morphism, and then extending it to a m…
▽ More
We study simulation and quantum resources in the setting of the sheaf-theoretic approach to contextuality and non-locality. Resources are viewed behaviourally, as empirical models. In earlier work, a notion of morphism for these empirical models was proposed and studied. We generalize and simplify the earlier approach, by starting with a very simple notion of morphism, and then extending it to a more useful one by passing to a co-Kleisli category with respect to a comonad of measurement protocols. We show that these morphisms capture notions of simulation between empirical models obtained via `free' operations in a resource theory of contextuality, including the type of classical control used in measurement-based quantum computation schemes.
△ Less
Submitted 22 April, 2019;
originally announced April 2019.
-
Relating Structure and Power: Comonadic Semantics for Computational Resources
Authors:
Samson Abramsky,
Nihil Shah
Abstract:
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-Fraisse 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 rela…
▽ More
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-Fraisse 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-Fraisse 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.
△ Less
Submitted 27 June, 2018; v1 submitted 23 June, 2018;
originally announced June 2018.
-
A complete characterisation of All-versus-Nothing arguments for stabiliser states
Authors:
Samson Abramsky,
Rui Soares Barbosa,
Giovanni Carù,
Simon Perdrix
Abstract:
An important class of contextuality arguments in quantum foundations are the All-versus-Nothing (AvN) proofs, generalising a construction originally due to Mermin. We present a general formulation of All-versus-Nothing arguments, and a complete characterisation of all such arguments which arise from stabiliser states. We show that every AvN argument for an n-qubit stabiliser state can be reduced t…
▽ More
An important class of contextuality arguments in quantum foundations are the All-versus-Nothing (AvN) proofs, generalising a construction originally due to Mermin. We present a general formulation of All-versus-Nothing arguments, and a complete characterisation of all such arguments which arise from stabiliser states. We show that every AvN argument for an n-qubit stabiliser state can be reduced to an AvN proof for a three-qubit state which is local Clifford-equivalent to the tripartite GHZ state. This is achieved through a combinatorial characterisation of AvN arguments, the AvN triple Theorem, whose proof makes use of the theory of graph states. This result enables the development of a computational method to generate all the AvN arguments in $\mathbb{Z}_2$ on n-qubit stabiliser states. We also present new insights into the stabiliser formalism and its connections with logic.
△ Less
Submitted 23 May, 2017;
originally announced May 2017.
-
The Quantum Monad on Relational Structures
Authors:
Samson Abramsky,
Rui Soares Barbosa,
Nadish de Silva,
Octavio Zapata
Abstract:
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…
▽ More
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 show a general connection between these notions and state-independent quantum realizations of strong contextuality in the Abramsky-Brandenburger formulation of contextuality. 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.
△ Less
Submitted 20 May, 2017;
originally announced May 2017.
-
Intensionality, Definability and Computation
Authors:
Samson Abramsky
Abstract:
We look at intensionality from the perspective of computation. In particular, we review how game semantics has been used to characterize the sequential functional processes, leading to powerful and flexible methods for constructing fully abstract models of programming languages, with applications in program analysis and verification. In a broader context, we can regard game semantics as a first st…
▽ More
We look at intensionality from the perspective of computation. In particular, we review how game semantics has been used to characterize the sequential functional processes, leading to powerful and flexible methods for constructing fully abstract models of programming languages, with applications in program analysis and verification. In a broader context, we can regard game semantics as a first step towards developing a positive theory of intensional structures with a robust mathematical structure, and finding the right notions of invariance for these structures.
△ Less
Submitted 12 May, 2017;
originally announced May 2017.
-
The pebbling comonad in finite model theory
Authors:
Samson Abramsky,
Anuj Dawar,
Pengming Wang
Abstract:
Pebble games are a powerful tool in the study of finite model theory, constraint satisfaction and database theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming. We show that existential k-pebble games have a natural comonadic formulation. Winning strategies for Duplicator in the k-pebble game for str…
▽ More
Pebble games are a powerful tool in the study of finite model theory, constraint satisfaction and database theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming. We show that existential k-pebble games have a natural comonadic formulation. Winning strategies for Duplicator in the k-pebble game for structures A and B are equivalent to morphisms from A to B in the coKleisli category for this comonad. This leads on to comonadic characterisations of a number of central concepts in Finite Model Theory: - Isomorphism in the co-Kleisli category characterises elementary equivalence in the k-variable logic with counting quantifiers. - Symmetric games corresponding to equivalence in full k-variable logic are also characterized. - The treewidth of a structure A is characterised in terms of its coalgebra number: the least k for which there is a coalgebra structure on A for the k-pebbling comonad. - Co-Kleisli morphisms are used to characterize strong consistency, and to give an account of a Cai-Fürer-Immerman construction. - The k-pebbling comonad is also used to give semantics to a novel modal operator. These results lay the basis for some new and promising connections between two areas within logic in computer science which have largely been disjoint: (1) finite and algorithmic model theory, and (2) semantics and categorical structures of computation.
△ Less
Submitted 17 April, 2017;
originally announced April 2017.
-
Anytime Inference in Valuation Algebras
Authors:
Abhishek Dasgupta,
Samson Abramsky
Abstract:
Anytime inference is inference performed incrementally, with the accuracy of the inference being controlled by a tunable parameter, usually time. Such anytime inference algorithms are also usually interruptible, gradually converging to the exact inference value until terminated. While anytime inference algorithms for specific domains like probability potentials exist in the literature, our objecti…
▽ More
Anytime inference is inference performed incrementally, with the accuracy of the inference being controlled by a tunable parameter, usually time. Such anytime inference algorithms are also usually interruptible, gradually converging to the exact inference value until terminated. While anytime inference algorithms for specific domains like probability potentials exist in the literature, our objective in this article is to obtain an anytime inference algorithm which is sufficiently generic to cover a wide range of domains. For this we utilise the theory of generic inference as a basis for constructing an anytime inference algorithm, and in particular, extending work done on ordered valuation algebras. The novel contribution of this work is the construction of anytime algorithms in a generic framework, which automatically gives us instantiations in various useful domains. We also show how to apply this generic framework for anytime inference in semiring induced valuation algebras, an important subclass of valuation algebras, which includes instances like probability potentials, disjunctive normal forms and distributive lattices.
Keywords: Approximation; Anytime algorithms; Resource-bounded computation; Generic inference; Valuation algebras; Local computation; Binary join trees.
△ Less
Submitted 13 May, 2016;
originally announced May 2016.
-
Information, Processes and Games
Authors:
Samson Abramsky
Abstract:
We survey the prospects for an Information Dynamics which can serve as the basis for a fundamental theory of information, incorporating qualitative and structural as well as quantitative aspects. We motivate our discussion with some basic conceptual puzzles: how can information increase in computation, and what is it that we are actually computing in general? Then we survey a number of the theorie…
▽ More
We survey the prospects for an Information Dynamics which can serve as the basis for a fundamental theory of information, incorporating qualitative and structural as well as quantitative aspects. We motivate our discussion with some basic conceptual puzzles: how can information increase in computation, and what is it that we are actually computing in general? Then we survey a number of the theories which have been developed within Computer Science, as partial exemplifications of the kind of fundamental theory which we seek: including Domain Theory, Dynamic Logic, and Process Algebra. We look at recent work showing new ways of combining quantitative and qualitative theories of information, as embodied respectively by Domain Theory and Shannon Information Theory. Then we look at Game Semantics and Geometry of Interaction, as examples of dynamic models of logic and computation in which information flow and interaction are made central and explicit. We conclude by looking briefly at some key issues for future progress.
△ Less
Submitted 9 April, 2016;
originally announced April 2016.
-
Possibilities Determine the Combinatorial Structure of Probability Polytopes
Authors:
Samson Abramsky,
Rui Soares Barbosa,
Kohei Kishida,
Raymond Lal,
Shane Mansfield
Abstract:
We study the set of no-signalling empirical models on a measurement scenario, and show that the combinatorial structure of the no-signalling polytope is completely determined by the possibilistic information given by the support of the models. This is a special case of a general result which applies to all polytopes presented in a standard form, given by linear equations together with non-negativi…
▽ More
We study the set of no-signalling empirical models on a measurement scenario, and show that the combinatorial structure of the no-signalling polytope is completely determined by the possibilistic information given by the support of the models. This is a special case of a general result which applies to all polytopes presented in a standard form, given by linear equations together with non-negativity constraints on the variables.
△ Less
Submitted 24 March, 2016;
originally announced March 2016.
-
Dynamic Game Semantics
Authors:
Norihiro Yamada,
Samson Abramsky
Abstract:
The present paper gives a mathematical, in particular, syntax-independent, formulation of intensionality and dynamics of computation in terms of games and strategies. Specifically, we give a game semantics for a higher-order programming language that distinguishes programs with the same value yet different algorithms (or intensionality), equipped with the hiding operation on strategies that precis…
▽ More
The present paper gives a mathematical, in particular, syntax-independent, formulation of intensionality and dynamics of computation in terms of games and strategies. Specifically, we give a game semantics for a higher-order programming language that distinguishes programs with the same value yet different algorithms (or intensionality), equipped with the hiding operation on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a cartesian closed bicategory, and our game semantics forms an instance of a generalization of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be the first step towards a mathematical (both categorical and game-semantic) foundation of intensional and dynamic aspects of logic and computation; our approach should be applicable to a wide range of logics and computations.
△ Less
Submitted 21 October, 2018; v1 submitted 16 January, 2016;
originally announced January 2016.
-
Process Realizability
Authors:
Samson Abramsky
Abstract:
We develop a notion of realizability for Classical Linear Logic based on a concurrent process calculus.
We develop a notion of realizability for Classical Linear Logic based on a concurrent process calculus.
△ Less
Submitted 19 December, 2015;
originally announced December 2015.
-
DEMONIC programming: a computational language for single-particle equilibrium thermodynamics, and its formal semantics
Authors:
Samson Abramsky,
Dominic Horsman
Abstract:
Maxwell's Demon, 'a being whose faculties are so sharpened that he can follow every molecule in its course', has been the centre of much debate about its abilities to violate the second law of thermodynamics. Landauer's hypothesis, that the Demon must erase its memory and incur a thermodynamic cost, has become the standard response to Maxwell's dilemma, and its implications for the thermodynamics…
▽ More
Maxwell's Demon, 'a being whose faculties are so sharpened that he can follow every molecule in its course', has been the centre of much debate about its abilities to violate the second law of thermodynamics. Landauer's hypothesis, that the Demon must erase its memory and incur a thermodynamic cost, has become the standard response to Maxwell's dilemma, and its implications for the thermodynamics of computation reach into many areas of quantum and classical computing. It remains, however, still a hypothesis. Debate has often centred around simple toy models of a single particle in a box. Despite their simplicity, the ability of these systems to accurately represent thermodynamics (specifically to satisfy the second law) and whether or not they display Landauer Erasure, has been a matter of ongoing argument. The recent Norton-Ladyman controversy is one such example.
In this paper we introduce a programming language to describe these simple thermodynamic processes, and give a formal operational semantics and program logic as a basis for formal reasoning about thermodynamic systems. We formalise the basic single-particle operations as statements in the language, and then show that the second law must be satisfied by any composition of these basic operations. This is done by finding a computational invariant of the system. We show, furthermore, that this invariant requires an erasure cost to exist within the system, equal to kTln2 for a bit of information: Landauer Erasure becomes a theorem of the formal system. The Norton-Ladyman controversy can therefore be resolved in a rigorous fashion, and moreover the formalism we introduce gives a set of reasoning tools for further analysis of Landauer erasure, which are provably consistent with the second law of thermodynamics.
△ Less
Submitted 4 November, 2015;
originally announced November 2015.
-
Games for Dependent Types
Authors:
Samson Abramsky,
Radha Jagadeesan,
Matthijs Vákár
Abstract:
We present a model of dependent type theory (DTT) with Pi-, 1-, Sigma- and intensional Id-types, which is based on a slight variation of the category of AJM-games and history-free winning 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…
▽ More
We present a model of dependent type theory (DTT) with Pi-, 1-, Sigma- and intensional Id-types, which is based on a slight variation of the category of AJM-games and history-free winning 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 model of DTT with Pi-, 1-, Sigma- 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 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.
△ Less
Submitted 20 August, 2015;
originally announced August 2015.
-
Contextuality, Cohomology and Paradox
Authors:
Samson Abramsky,
Rui Soares Barbosa,
Kohei Kishida,
Raymond Lal,
Shane Mansfield
Abstract:
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 pape…
▽ More
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.
△ Less
Submitted 5 March, 2017; v1 submitted 10 February, 2015;
originally announced February 2015.
-
Contextual Semantics: From Quantum Mechanics to Logic, Databases, Constraints, and Complexity
Authors:
Samson Abramsky
Abstract:
We discuss quantum non-locality and contextuality, emphasising logical and structural aspects. We also show how the same mathematical structures arise in various areas of classical computation.
We discuss quantum non-locality and contextuality, emphasising logical and structural aspects. We also show how the same mathematical structures arise in various areas of classical computation.
△ Less
Submitted 28 June, 2014;
originally announced June 2014.
-
An Algebraic Characterisation of Concurrent Composition
Authors:
Samson Abramsky
Abstract:
We give an algebraic characterization of a form of synchronized parallel composition allowing for true concurrency, using ideas based on Peter Landin's "Program-Machine Symmetric Automata Theory".
We give an algebraic characterization of a form of synchronized parallel composition allowing for true concurrency, using ideas based on Peter Landin's "Program-Machine Symmetric Automata Theory".
△ Less
Submitted 8 June, 2014;
originally announced June 2014.
-
Two Puzzles About Computation
Authors:
Samson Abramsky
Abstract:
The purpose of this note is to raise two different questions, which are rarely if ever considered, and to which, it seems, we lack convincing, systematic answers. These questions can be posed as:
- Why do we compute?
- What do we compute?
The point is not so much that we have no answers to these puzzles, as that we have no established body of theory which gives satisfying, systematic answers…
▽ More
The purpose of this note is to raise two different questions, which are rarely if ever considered, and to which, it seems, we lack convincing, systematic answers. These questions can be posed as:
- Why do we compute?
- What do we compute?
The point is not so much that we have no answers to these puzzles, as that we have no established body of theory which gives satisfying, systematic answers, as part of a broader understanding. By raising these questions, we hope to stimulate some thinking in this direction.
△ Less
Submitted 19 March, 2014;
originally announced March 2014.
-
Semantic Unification A sheaf theoretic approach to natural language
Authors:
Samson Abramsky,
Mehrnoosh Sadrzadeh
Abstract:
Language is contextual and sheaf theory provides a high level mathematical framework to model contextuality. We show how sheaf theory can model the contextual nature of natural language and how gluing can be used to provide a global semantics for a discourse by putting together the local logical semantics of each sentence within the discourse. We introduce a presheaf structure corresponding to a b…
▽ More
Language is contextual and sheaf theory provides a high level mathematical framework to model contextuality. We show how sheaf theory can model the contextual nature of natural language and how gluing can be used to provide a global semantics for a discourse by putting together the local logical semantics of each sentence within the discourse. We introduce a presheaf structure corresponding to a basic form of Discourse Representation Structures. Within this setting, we formulate a notion of semantic unification --- gluing meanings of parts of a discourse into a coherent whole --- as a form of sheaf-theoretic gluing. We illustrate this idea with a number of examples where it can used to represent resolutions of anaphoric references. We also discuss multivalued gluing, described using a distributions functor, which can be used to represent situations where multiple gluings are possible, and where we may need to rank them using quantitative measures.
Dedicated to Jim Lambek on the occasion of his 90th birthday.
△ Less
Submitted 13 March, 2014;
originally announced March 2014.
-
Game Semantics for Access Control
Authors:
Samson Abramsky,
Radha jagadeesan
Abstract:
We introduce a semantic approach to the study of logics for access control and dependency analysis, based on Game Semantics. We use a variant of AJM games with explicit justification (but without pointers). Based on this, we give a simple and intuitive model of the information flow constraints underlying access control. This is used to give strikingly simple proofs of \emph{non-interference theore…
▽ More
We introduce a semantic approach to the study of logics for access control and dependency analysis, based on Game Semantics. We use a variant of AJM games with explicit justification (but without pointers). Based on this, we give a simple and intuitive model of the information flow constraints underlying access control. This is used to give strikingly simple proofs of \emph{non-interference theorems} in robust, semantic versions.
△ Less
Submitted 21 January, 2014;
originally announced January 2014.
-
Retracing some paths in Process Algebra
Authors:
Samson Abramsky
Abstract:
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.
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.
△ Less
Submitted 20 January, 2014;
originally announced January 2014.
-
What are the fundamental structures of concurrency? We still don't know!
Authors:
Samson Abramsky
Abstract:
Process algebra has been successful in many ways; but we don't yet see the lineaments of a fundamental theory. Some fleeting glimpses are sought from Petri Nets, physics and geometry.
Process algebra has been successful in many ways; but we don't yet see the lineaments of a fundamental theory. Some fleeting glimpses are sought from Petri Nets, physics and geometry.
△ Less
Submitted 20 January, 2014;
originally announced January 2014.
-
Axioms for Definability and Full Completeness
Authors:
Samson Abramsky
Abstract:
Axioms are presented which encapsulate the properties satisfied by categories of games which form the basis of results on full abstraction for PCF and other programming languages, and on full completeness for various logics and type theories.
Axioms are presented on models of PCF from which full abstraction can be proved. These axioms have been distilled from recent results on definability and f…
▽ More
Axioms are presented which encapsulate the properties satisfied by categories of games which form the basis of results on full abstraction for PCF and other programming languages, and on full completeness for various logics and type theories.
Axioms are presented on models of PCF from which full abstraction can be proved. These axioms have been distilled from recent results on definability and full abstraction of game semantics for a number of programming languages. Full completeness for pure simply-typed $λ$-calculus is also axiomatized.
△ Less
Submitted 21 January, 2014; v1 submitted 19 January, 2014;
originally announced January 2014.
-
A Game Semantics for Generic Polymorphism
Authors:
Samson Abramsky,
Radha Jagadeesan
Abstract:
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. The…
▽ More
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.
△ Less
Submitted 4 December, 2013;
originally announced December 2013.
-
Semantics of Interaction
Authors:
Samson Abramsky
Abstract:
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 vers…
▽ More
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.
△ Less
Submitted 30 November, 2013;
originally announced December 2013.
-
Full Abstraction for PCF
Authors:
Samson Abramsky,
Radha Jagadeesan,
Pasquale Malacaria
Abstract:
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 s…
▽ More
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.
△ Less
Submitted 20 January, 2014; v1 submitted 24 November, 2013;
originally announced November 2013.
-
Games and Full Completeness for Multiplicative Linear Logic
Authors:
Samson Abramsky,
Radha Jagadeesan
Abstract:
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} strate…
▽ More
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.
△ Less
Submitted 23 November, 2013;
originally announced November 2013.
-
Coalgebraic Analysis of Subgame-perfect Equilibria in Infinite Games without Discounting
Authors:
Samson Abramsky,
Viktor Winschel
Abstract:
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 economicall…
▽ More
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.
△ Less
Submitted 5 June, 2013; v1 submitted 16 October, 2012;
originally announced October 2012.
-
Relational Databases and Bell's Theorem
Authors:
Samson Abramsky
Abstract:
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 o…
▽ More
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.
△ Less
Submitted 12 July, 2013; v1 submitted 31 August, 2012;
originally announced August 2012.
-
Logical Bell Inequalities
Authors:
Samson Abramsky,
Lucien Hardy
Abstract:
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 c…
▽ More
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.
△ Less
Submitted 20 June, 2012; v1 submitted 6 March, 2012;
originally announced March 2012.
-
A Generalized Kahn Principle for Abstract Asynchronous Networks
Authors:
Samson Abramsky
Abstract:
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…
▽ More
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.
△ Less
Submitted 2 December, 2011;
originally announced December 2011.
-
Domain Theory and the Logic of Observable Properties
Authors:
Samson Abramsky
Abstract:
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 program…
▽ More
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.
△ Less
Submitted 1 December, 2011;
originally announced December 2011.
-
Sequentiality vs. Concurrency in Games and Logic
Authors:
Samson Abramsky
Abstract:
Connections between the sequentiality/concurrency distinction and the semantics of proofs are investigated, with particular reference to games and Linear Logic.
Connections between the sequentiality/concurrency distinction and the semantics of proofs are investigated, with particular reference to games and Linear Logic.
△ Less
Submitted 30 November, 2011;
originally announced November 2011.
-
A Structural Approach to Reversible Computation
Authors:
Samson Abramsky
Abstract:
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…
▽ More
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.
△ Less
Submitted 30 November, 2011;
originally announced November 2011.
