21 Search Results for "Abramsky, Samson"

Document
DOI: 10.4230/LIPIcs.FSCD.2024.5
The Flower Calculus

Authors: Pablo Donato

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
We introduce the flower calculus, a deep inference proof system for intuitionistic first-order logic inspired by Peirce’s existential graphs. It works as a rewriting system over inductive objects called "flowers", that enjoy both a graphical interpretation as topological diagrams, and a textual presentation as nested sequents akin to coherent formulas. Importantly, the calculus dispenses completely with the traditional notion of symbolic connective, operating solely on nested flowers containing atomic predicates. We prove both the soundness of the full calculus and the completeness of an analytic fragment with respect to Kripke semantics. This provides to our knowledge the first analyticity result for a proof system based on existential graphs, adapting semantic cut-elimination techniques to a deep inference setting. Furthermore, the kernel of rules targetted by completeness is fully invertible, a desirable property for both automated and interactive proof search.
Cite as

Pablo Donato. The Flower Calculus. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 5:1-5:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{donato:LIPIcs.FSCD.2024.5,
  author =	{Donato, Pablo},
  title =	{{The Flower Calculus}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{5:1--5:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.5},
  URN =		{urn:nbn:de:0030-drops-203343},
  doi =		{10.4230/LIPIcs.FSCD.2024.5},
  annote =	{Keywords: deep inference, graphical calculi, existential graphs, intuitionistic logic, Kripke semantics, cut-elimination}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.15
Adjoint Natural Deduction

Authors: Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.
Cite as

Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka. Adjoint Natural Deduction. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 15:1-15:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{jang_et_al:LIPIcs.FSCD.2024.15,
  author =	{Jang, Junyoung and Roshal, Sophia and Pfenning, Frank and Pientka, Brigitte},
  title =	{{Adjoint Natural Deduction}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{15:1--15:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.15},
  URN =		{urn:nbn:de:0030-drops-203441},
  doi =		{10.4230/LIPIcs.FSCD.2024.15},
  annote =	{Keywords: Substructural Logic, Type Systems, Functional Programming}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.24
IMELL Cut Elimination with Linear Overhead

Authors: Beniamino Accattoli and Claudio Sacerdoti Coen

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed with rewriting rules at-a-distance for cut elimination. He also introduced a new cut elimination strategy, dubbed the good strategy, and showed that its number of steps is a time cost model with polynomial overhead for ESC/IMELL, and the first such one. Here, we refine Accattoli’s result by introducing an abstract machine for ESC and proving that it implements the good strategy and computes cut-free terms/proofs within a linear overhead.
Cite as

Beniamino Accattoli and Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.24,
  author =	{Accattoli, Beniamino and Sacerdoti Coen, Claudio},
  title =	{{IMELL Cut Elimination with Linear Overhead}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{24:1--24:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.24},
  URN =		{urn:nbn:de:0030-drops-203539},
  doi =		{10.4230/LIPIcs.FSCD.2024.24},
  annote =	{Keywords: Lambda calculus, linear logic, abstract machines}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.28
Commutation Groups and State-Independent Contextuality

Authors: Samson Abramsky, Şerban-Ion Cercelescu, and Carmen-Maria Constantin

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
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.
Cite as

Samson Abramsky, Şerban-Ion Cercelescu, and Carmen-Maria Constantin. Commutation Groups and State-Independent Contextuality. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{abramsky_et_al:LIPIcs.FSCD.2024.28,
  author =	{Abramsky, Samson and Cercelescu, \c{S}erban-Ion and Constantin, Carmen-Maria},
  title =	{{Commutation Groups and State-Independent Contextuality}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.28},
  URN =		{urn:nbn:de:0030-drops-203572},
  doi =		{10.4230/LIPIcs.FSCD.2024.28},
  annote =	{Keywords: Contextuality, state-independence, quantum mechanics, Pauli group, group presentations, unitary representations}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2024.84
The k-Opt Algorithm for the Traveling Salesman Problem Has Exponential Running Time for k ≥ 5

Authors: Sophia Heimann, Hung P. Hoang, and Stefan Hougardy

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
The k-Opt algorithm is a local search algorithm for the Traveling Salesman Problem. Starting with an initial tour, it iteratively replaces at most k edges in the tour with the same number of edges to obtain a better tour. Krentel (FOCS 1989) showed that the Traveling Salesman Problem with the k-Opt neighborhood is complete for the class PLS (polynomial time local search) and that the k-Opt algorithm can have exponential running time for any pivot rule. However, his proof requires k ≫ 1000 and has a substantial gap. We show the two properties above for a much smaller value of k, addressing an open question by Monien, Dumrauf, and Tscheuschner (ICALP 2010). In particular, we prove the PLS-completeness for k ≥ 17 and the exponential running time for k ≥ 5.
Cite as

Sophia Heimann, Hung P. Hoang, and Stefan Hougardy. The k-Opt Algorithm for the Traveling Salesman Problem Has Exponential Running Time for k ≥ 5. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 84:1-84:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{heimann_et_al:LIPIcs.ICALP.2024.84,
  author =	{Heimann, Sophia and Hoang, Hung P. and Hougardy, Stefan},
  title =	{{The k-Opt Algorithm for the Traveling Salesman Problem Has Exponential Running Time for k ≥ 5}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{84:1--84:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.84},
  URN =		{urn:nbn:de:0030-drops-202270},
  doi =		{10.4230/LIPIcs.ICALP.2024.84},
  annote =	{Keywords: Traveling Salesman Problem, k-Opt algorithm, PLS-completeness}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.130
Function Spaces for Orbit-Finite Sets

Authors: Mikołaj Bojańczyk, Lê Thành Dũng (Tito) Nguyễn, and Rafał Stefański

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
Orbit-finite sets are a generalisation of finite sets, and as such support many operations allowed for finite sets, such as pairing, quotienting, or taking subsets. However, they do not support function spaces, i.e. if X and Y are orbit-finite sets, then the space of finitely supported functions from X to Y is not orbit-finite. We propose a solution to this problem inspired by linear logic.
Cite as

Mikołaj Bojańczyk, Lê Thành Dũng (Tito) Nguyễn, and Rafał Stefański. Function Spaces for Orbit-Finite Sets. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 130:1-130:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.ICALP.2024.130,
  author =	{Boja\'{n}czyk, Miko{\l}aj and Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito) and Stefa\'{n}ski, Rafa{\l}},
  title =	{{Function Spaces for Orbit-Finite Sets}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{130:1--130:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.130},
  URN =		{urn:nbn:de:0030-drops-202730},
  doi =		{10.4230/LIPIcs.ICALP.2024.130},
  annote =	{Keywords: Orbit-finite sets, automata, linear types, game semantics}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.131
The Structure of Trees in the Pushdown Hierarchy

Authors: Arnaud Carayol and Lucien Charamond

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
In this article, we investigate the structure of the trees in the pushdown hierarchy, a hierarchy of infinite graphs having a decidable MSO-theory. We show that a binary complete tree in the pushdown hierarchy must contain at least two different subtrees which are isomorphic. We extend this property to any tree with no leaves and with chains of unary vertices of bounded length. We provided two applications of this result. A first application in formal language theory, gives a simple argument to show that some languages are not deterministic higher-order indexed languages. A second application in number theory shows that the real numbers defined by deterministic higher-order pushdown automata are either rational or transcendental.
Cite as

Arnaud Carayol and Lucien Charamond. The Structure of Trees in the Pushdown Hierarchy. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 131:1-131:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{carayol_et_al:LIPIcs.ICALP.2024.131,
  author =	{Carayol, Arnaud and Charamond, Lucien},
  title =	{{The Structure of Trees in the Pushdown Hierarchy}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{131:1--131:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.131},
  URN =		{urn:nbn:de:0030-drops-202749},
  doi =		{10.4230/LIPIcs.ICALP.2024.131},
  annote =	{Keywords: Pushdown hierarchy, Monadic second-order logic, Automatic numbers}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.136
Improved Algorithm for Reachability in d-VASS

Authors: Yuxi Fu, Qizhe Yang, and Yangluo Zheng

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
An 𝖥_{d} upper bound for the reachability problem in vector addition systems with states (VASS) in fixed dimension is given, where 𝖥_d is the d-th level of the Grzegorczyk hierarchy of complexity classes. The new algorithm combines the idea of the linear path scheme characterization of the reachability in the 2-dimension VASSes with the general decomposition algorithm by Mayr, Kosaraju and Lambert. The result improves the 𝖥_{d + 4} upper bound due to Leroux and Schmitz (LICS 2019).
Cite as

Yuxi Fu, Qizhe Yang, and Yangluo Zheng. Improved Algorithm for Reachability in d-VASS. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 136:1-136:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{fu_et_al:LIPIcs.ICALP.2024.136,
  author =	{Fu, Yuxi and Yang, Qizhe and Zheng, Yangluo},
  title =	{{Improved Algorithm for Reachability in d-VASS}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{136:1--136:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.136},
  URN =		{urn:nbn:de:0030-drops-202799},
  doi =		{10.4230/LIPIcs.ICALP.2024.136},
  annote =	{Keywords: Petri net, vector addition system, reachability}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.7
Comonadic semantics for hybrid logic

Authors: Samson Abramsky and Dan Marsden

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
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.
Cite as

Samson Abramsky and Dan Marsden. Comonadic semantics for hybrid logic. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{abramsky_et_al:LIPIcs.MFCS.2022.7,
  author =	{Abramsky, Samson and Marsden, Dan},
  title =	{{Comonadic semantics for hybrid logic}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{7:1--7:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.7},
  URN =		{urn:nbn:de:0030-drops-168055},
  doi =		{10.4230/LIPIcs.MFCS.2022.7},
  annote =	{Keywords: comonads, model comparison games, semantic characterizations, hybrid logic, bounded fragment}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.75
Cohomology in Constraint Satisfaction and Structure Isomorphism

Authors: Adam Ó Conghaile

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
Constraint satisfaction (CSP) and structure isomorphism (SI) are among the most well-studied computational problems in Computer Science. While neither problem is thought to be in PTIME, much work is done on PTIME approximations to both problems. Two such historically important approximations are the k-consistency algorithm for CSP and the k-Weisfeiler-Leman algorithm for SI, both of which are based on propagating local partial solutions. The limitations of these algorithms are well-known – k-consistency can solve precisely those CSPs of bounded width and k-Weisfeiler-Leman can only distinguish structures which differ on properties definable in C^k. In this paper, we introduce a novel sheaf-theoretic approach to CSP and SI and their approximations. We show that both problems can be viewed as deciding the existence of global sections of presheaves, ℋ_k(A,B) and ℐ_k(A,B) and that the success of the k-consistency and k-Weisfeiler-Leman algorithms correspond to the existence of certain efficiently computable subpresheaves of these. Furthermore, building on work of Abramsky and others in quantum foundations, we show how to use Čech cohomology in ℋ_k(A,B) and ℐ_k(A,B) to detect obstructions to the existence of the desired global sections and derive new efficient cohomological algorithms extending k-consistency and k-Weisfeiler-Leman. We show that cohomological k-consistency can solve systems of equations over all finite rings and that cohomological Weisfeiler-Leman can distinguish positive and negative instances of the Cai-Fürer-Immerman property over several important classes of structures.
Cite as

Adam Ó Conghaile. Cohomology in Constraint Satisfaction and Structure Isomorphism. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 75:1-75:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{oconghaile:LIPIcs.MFCS.2022.75,
  author =	{\'{O} Conghaile, Adam},
  title =	{{Cohomology in Constraint Satisfaction and Structure Isomorphism}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{75:1--75:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.75},
  URN =		{urn:nbn:de:0030-drops-168738},
  doi =		{10.4230/LIPIcs.MFCS.2022.75},
  annote =	{Keywords: constraint satisfaction problems, finite model theory, descriptive complexity, rank logic, Weisfeiler-Leman algorithm, cohomology}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.115
Arboreal Categories and Resources

Authors: Samson Abramsky and Luca Reggio

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
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 very general, axiomatic setting, and applied to relational structures, where the comonadic constructions for pebbling, Ehrenfeucht-Fraïssé and modal bisimulation games recently introduced in [Abramsky et al., 2017; S. Abramsky and N. Shah, 2018; Abramsky and Shah, 2021] are recovered, showing that many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers.
Cite as

Samson Abramsky and Luca Reggio. Arboreal Categories and Resources. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 115:1-115:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{abramsky_et_al:LIPIcs.ICALP.2021.115,
  author =	{Abramsky, Samson and Reggio, Luca},
  title =	{{Arboreal Categories and Resources}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{115:1--115:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.115},
  URN =		{urn:nbn:de:0030-drops-141845},
  doi =		{10.4230/LIPIcs.ICALP.2021.115},
  annote =	{Keywords: factorisation system, embedding, comonad, coalgebra, open maps, bisimulation, game, resources, relational structures, finite model theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.5
The Logic of Contextuality

Authors: Samson Abramsky and Rui Soares Barbosa

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

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 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.
Cite as

Samson Abramsky and Rui Soares Barbosa. The Logic of Contextuality. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{abramsky_et_al:LIPIcs.CSL.2021.5,
  author =	{Abramsky, Samson and Barbosa, Rui Soares},
  title =	{{The Logic of Contextuality}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{5:1--5:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.5},
  URN =		{urn:nbn:de:0030-drops-134394},
  doi =		{10.4230/LIPIcs.CSL.2021.5},
  annote =	{Keywords: partial Boolean algebras, contextuality, exclusivity principles, Kochen-Specker paradoxes, tensor product}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.2
Relating Structure and Power: Comonadic Semantics for Computational Resources

Authors: Samson Abramsky and Nihil Shah

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

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-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.
Cite as

Samson Abramsky and Nihil Shah. Relating Structure and Power: Comonadic Semantics for Computational Resources. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{abramsky_et_al:LIPIcs.CSL.2018.2,
  author =	{Abramsky, Samson and Shah, Nihil},
  title =	{{Relating Structure and Power: Comonadic Semantics for Computational Resources}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{2:1--2:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.2},
  URN =		{urn:nbn:de:0030-drops-96698},
  doi =		{10.4230/LIPIcs.CSL.2018.2},
  annote =	{Keywords: Finite model theory, combinatorial games, Ehrenfeucht-Fra\"{i}ss\'{e} games, pebble games, bisimulation, comonads, coKleisli category, coalgebras of a comonad}
}
Document
DOI: 10.4230/LIPIcs.TQC.2017.9
Minimum Quantum Resources for Strong Non-Locality

Authors: Samson Abramsky, Rui Soares Barbosa, Giovanni Carù, Nadish de Silva, Kohei Kishida, and Shane Mansfield

Published in: LIPIcs, Volume 73, 12th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2017)

Abstract
We analyse the minimum quantum resources needed to realise strong non-locality, as exemplified e.g. by the classical GHZ construction. It was already known that no two-qubit system, with any finite number of local measurements, can realise strong non-locality. For three-qubit systems, we show that strong non-locality can only be realised in the GHZ SLOCC class, and with equatorial measurements. However, we show that in this class there is an infinite family of states which are pairwise non LU-equivalent that realise strong non-locality with finitely many measurements. These states have decreasing entanglement between one qubit and the other two, necessitating an increasing number of local measurements on the latter.
Cite as

Samson Abramsky, Rui Soares Barbosa, Giovanni Carù, Nadish de Silva, Kohei Kishida, and Shane Mansfield. Minimum Quantum Resources for Strong Non-Locality. In 12th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 73, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{abramsky_et_al:LIPIcs.TQC.2017.9,
  author =	{Abramsky, Samson and Barbosa, Rui Soares and Car\`{u}, Giovanni and de Silva, Nadish and Kishida, Kohei and Mansfield, Shane},
  title =	{{Minimum Quantum Resources for Strong Non-Locality}},
  booktitle =	{12th Conference on the Theory of Quantum Computation, Communication and Cryptography (TQC 2017)},
  pages =	{9:1--9:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-034-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{73},
  editor =	{Wilde, Mark M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TQC.2017.9},
  URN =		{urn:nbn:de:0030-drops-85822},
  doi =		{10.4230/LIPIcs.TQC.2017.9},
  annote =	{Keywords: strong non-locality, maximal non-locality, quantum resources, three-qubit states}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.35
The Quantum Monad on Relational Structures

Authors: Samson Abramsky, Rui Soares Barbosa, Nadish de Silva, and Octavio Zapata

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

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 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.
Cite as

Samson Abramsky, Rui Soares Barbosa, Nadish de Silva, and Octavio Zapata. The Quantum Monad on Relational Structures. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{abramsky_et_al:LIPIcs.MFCS.2017.35,
  author =	{Abramsky, Samson and Barbosa, Rui Soares and de Silva, Nadish and Zapata, Octavio},
  title =	{{The Quantum Monad on Relational Structures}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.35},
  URN =		{urn:nbn:de:0030-drops-81290},
  doi =		{10.4230/LIPIcs.MFCS.2017.35},
  annote =	{Keywords: non-local games, quantum computation, monads}
}
  • Refine by Author
  • 13 Abramsky, Samson
  • 3 Barbosa, Rui Soares
  • 2 Kishida, Kohei
  • 2 Mansfield, Shane
  • 2 Winschel, Viktor
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Finite Model Theory
  • 2 Theory of computation → Categorical semantics
  • 2 Theory of computation → Proof theory
  • 1 Mathematics of computing
  • 1 Theory of computation
  • Show More...

  • Refine by Keyword
  • 3 Category theory
  • 2 bisimulation
  • 2 cohomology
  • 2 comonads
  • 2 contextuality
  • Show More...

  • Refine by Type
  • 21 document

  • Refine by Publication Year
  • 8 2024
  • 2 2013
  • 2 2015
  • 2 2018
  • 2 2021
  • Show More...

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact