Volume
LIPIcs, Volume 183
29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Publication Details
- published at: 2021-01-13
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-175-7
- DBLP: db/conf/csl/csl2021
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 183, CSL 2021, Complete Volume
Abstract
LIPIcs, Volume 183, CSL 2021, Complete Volume
Cite as
29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 1-734, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@Proceedings{baier_et_al:LIPIcs.CSL.2021,
title = {{LIPIcs, Volume 183, CSL 2021, Complete Volume}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {1--734},
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},
URN = {urn:nbn:de:0030-drops-134339},
doi = {10.4230/LIPIcs.CSL.2021},
annote = {Keywords: LIPIcs, Volume 183, CSL 2021, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{baier_et_al:LIPIcs.CSL.2021.0,
author = {Baier, Christel and Goubault-Larrecq, Jean},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {0:i--0:xx},
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.0},
URN = {urn:nbn:de:0030-drops-134348},
doi = {10.4230/LIPIcs.CSL.2021.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
μ-Calculi with Atoms (Invited Talk)
Abstract
Modal μ-calculus is a well-known formalism for describing properties of state-based transition systems. It can define properties such as "[in the current state] p holds, and there is a path where is holds again at some point in the future", where p comes from some fixed vocabulary of basic predicates.
A formula of the classical μ-calculus refers only to finitely many basic predicates, which may sometimes seem restrictive. Real systems routinely operate on data coming from potentially infinite domains, such as numbers or character strings. Basic properties of such systems may reasonably include ones like "the number n was input", for every number n. It is then not clear how to say that "there exists a transition path where the currently input number is input again some time in the future" as a formula.
Various modal formalisms have been proposed to model temporal properties of systems that refer to data coming from infinite domains. Here I focus on the modal μ-calculus with atoms, which is an extension of the classical calculus with features of nominal sets. There, basic predicates, formulas and models rely on atoms that come from some fixed infinite domain and can be tested for equality (or, in an extended variant, for some fixed order).
I present a few variants of the modal μ-calculus with atoms, and describe their properties. As an example application, I show how to formulate the security property of the cryptographic Needham-Schroeder protocol, which relies on generating atomic nonces and comparing them for equality, and which famously fails due to a man-in-the-middle attack.
Much of the material presented in this talk is drawn from [C. Eberhart and B. Klin, 2019; B. Klin and M. Łełyk, 2019; B. Klin and M. Łełyk, 2017].
Cite as
Bartek Klin. μ-Calculi with Atoms (Invited Talk). In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{klin:LIPIcs.CSL.2021.1,
author = {Klin, Bartek},
title = {{\mu-Calculi with Atoms}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {1:1--1:1},
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.1},
URN = {urn:nbn:de:0030-drops-134358},
doi = {10.4230/LIPIcs.CSL.2021.1},
annote = {Keywords: modal \mu-calculus, sets with atoms}
}
Document
Invited Talk
Mathematical Structures in Dependent Type Theory (Invited Talk)
Abstract
In this talk, we discuss the role and the implementation of mathematical structures in libraries of formalised mathematics in dependent type theory.
Cite as
Assia Mahboubi. Mathematical Structures in Dependent Type Theory (Invited Talk). In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{mahboubi:LIPIcs.CSL.2021.2,
author = {Mahboubi, Assia},
title = {{Mathematical Structures in Dependent Type Theory}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {2:1--2:3},
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.2},
URN = {urn:nbn:de:0030-drops-134361},
doi = {10.4230/LIPIcs.CSL.2021.2},
annote = {Keywords: Mathematical structures, formalized mathematics, dependent type theory}
}
Document
Invited Talk
Branching in Well-Structured Transition Systems (Invited Talk)
Abstract
The framework of well-structured transition systems has been highly successful in providing generic algorithms to show the decidability of verification problems for infinite-state systems. In some of these applications, the executions in the system at hand are actually trees, and need to be "lifted" to executions over sets of configurations in order to fit in the framework. The downside of this approach is that we might lose precision when analysing the computational complexity of the algorithms, compared to reasoning over branching executions.
Cite as
Sylvain Schmitz. Branching in Well-Structured Transition Systems (Invited Talk). In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{schmitz:LIPIcs.CSL.2021.3,
author = {Schmitz, Sylvain},
title = {{Branching in Well-Structured Transition Systems}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {3:1--3:3},
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.3},
URN = {urn:nbn:de:0030-drops-134377},
doi = {10.4230/LIPIcs.CSL.2021.3},
annote = {Keywords: fast-growing complexity, well-structured transition system}
}
Document
Invited Talk
Borel Sets in Reverse Mathematics (Invited Talk)
Abstract
We present what is known about the reverse mathematical strength of weak theorems involving Borel sets.
Cite as
Linda Westrick. Borel Sets in Reverse Mathematics (Invited Talk). In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{westrick:LIPIcs.CSL.2021.4,
author = {Westrick, Linda},
title = {{Borel Sets in Reverse Mathematics}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {4:1--4:2},
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.4},
URN = {urn:nbn:de:0030-drops-134387},
doi = {10.4230/LIPIcs.CSL.2021.4},
annote = {Keywords: Borel sets, reverse mathematics, measure, category}
}
Document
The Logic of Contextuality
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
Factorize Factorization
Abstract
We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by the Hindley-Rosen technique for confluence. Specifically, our approach is well adapted to deal with extensions of the call-by-name and call-by-value λ-calculi.
The technique is first developed abstractly. We isolate a sufficient condition (called linear swap) for lifting factorization from components to the compound system, and which is compatible with β-reduction. We then closely analyze some common factorization schemas for the λ-calculus.
Concretely, we apply our technique to diverse extensions of the λ-calculus, among which de' Liguoro and Piperno’s non-deterministic λ-calculus and - for call-by-value - Carraro and Guerrieri’s shuffling calculus. For both calculi the literature contains factorization theorems. In both cases, we give a new proof which is neat, simpler than the original, and strikingly shorter.
Cite as
Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorize Factorization. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{accattoli_et_al:LIPIcs.CSL.2021.6,
author = {Accattoli, Beniamino and Faggian, Claudia and Guerrieri, Giulio},
title = {{Factorize Factorization}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {6:1--6:25},
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.6},
URN = {urn:nbn:de:0030-drops-134407},
doi = {10.4230/LIPIcs.CSL.2021.6},
annote = {Keywords: Lambda Calculus, Rewriting, Reduction Strategies, Factorization}
}
Document
The Best a Monitor Can Do
Abstract
Existing notions of monitorability for branching-time properties are fairly restrictive. This, in turn, impacts the ability to incorporate prior knowledge about the system under scrutiny - which corresponds to a branching-time property - into the runtime analysis. We propose a definition of optimal monitors that verify the best monitorable under- or over-approximation of a specification, regardless of its monitorability status. Optimal monitors can be obtained for arbitrary branching-time properties by synthesising a sound and complete monitor for their strongest monitorable consequence. We show that the strongest monitorable consequence of specifications expressed in Hennessy-Milner logic with recursion is itself expressible in this logic, and present a procedure to find it. Our procedure enables prior knowledge to be optimally incorporated into runtime monitors.
Cite as
Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. The Best a Monitor Can Do. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{aceto_et_al:LIPIcs.CSL.2021.7,
author = {Aceto, Luca and Achilleos, Antonis and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
title = {{The Best a Monitor Can Do}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {7:1--7:23},
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.7},
URN = {urn:nbn:de:0030-drops-134416},
doi = {10.4230/LIPIcs.CSL.2021.7},
annote = {Keywords: monitorability, branching-time logics, runtime verification}
}
Document
Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?
Abstract
Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy’s merge is added to that language. These results raise the question of whether there is one auxiliary binary operator whose addition to CCS leads to a finite axiomatisation of bisimilarity. This study provides a negative answer to that question based on three reasonable assumptions.
Cite as
Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{aceto_et_al:LIPIcs.CSL.2021.8,
author = {Aceto, Luca and Castiglioni, Valentina and Fokkink, Wan and Ing\'{o}lfsd\'{o}ttir, Anna and Luttik, Bas},
title = {{Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {8:1--8:17},
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.8},
URN = {urn:nbn:de:0030-drops-134425},
doi = {10.4230/LIPIcs.CSL.2021.8},
annote = {Keywords: Equational logic, CCS, bisimulation, parallel composition, non-finitely based algebras}
}
Document
A Quasi-Polynomial Black-Box Algorithm for Fixed Point Evaluation
Abstract
We consider nested fixed-point expressions like μ z. ν y. μ x. f(x,y,z) evaluated over a finite lattice, and ask how many queries to a function f are needed to find the value. The previous upper bounds for a monotone function f of arity d over the lattice {0,1}ⁿ were of the order n^{𝒪(d)}, whereas a lower bound of Ω(n²/(lg n)) is known in case when at least one alternation between the least (μ) and the greatest (ν) fixed point occurs in the expression. Following a recent development for parity games, we show here that a quasi-polynomial number of queries is sufficient, namely n^{lg(d/lg n)+𝒪(1)}. The algorithm is an abstract version of several algorithms proposed recently by a number of authors, which involve (implicitly or explicitly) the structure of a universal tree. We then show a quasi-polynomial lower bound for the number of queries used by the algorithms in consideration.
Cite as
André Arnold, Damian Niwiński, and Paweł Parys. A Quasi-Polynomial Black-Box Algorithm for Fixed Point Evaluation. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{arnold_et_al:LIPIcs.CSL.2021.9,
author = {Arnold, Andr\'{e} and Niwi\'{n}ski, Damian and Parys, Pawe{\l}},
title = {{A Quasi-Polynomial Black-Box Algorithm for Fixed Point Evaluation}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {9:1--9:23},
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.9},
URN = {urn:nbn:de:0030-drops-134430},
doi = {10.4230/LIPIcs.CSL.2021.9},
annote = {Keywords: Mu-calculus, Parity games, Quasi-polynomial time, Black-box algorithm}
}
Document
Learning Concepts Described By Weight Aggregation Logic
Abstract
We consider weighted structures, which extend ordinary relational structures by assigning weights, i.e. elements from a particular group or ring, to tuples present in the structure. We introduce an extension of first-order logic that allows to aggregate weights of tuples, compare such aggregates, and use them to build more complex formulas. We provide locality properties of fragments of this logic including Feferman-Vaught decompositions and a Gaifman normal form for a fragment called FOW₁, as well as a localisation theorem for a larger fragment called FOWA₁. This fragment can express concepts from various machine learning scenarios. Using the locality properties, we show that concepts definable in FOWA₁ over a weighted background structure of at most polylogarithmic degree are agnostically PAC-learnable in polylogarithmic time after pseudo-linear time preprocessing.
Cite as
Steffen van Bergerem and Nicole Schweikardt. Learning Concepts Described By Weight Aggregation Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{vanbergerem_et_al:LIPIcs.CSL.2021.10,
author = {van Bergerem, Steffen and Schweikardt, Nicole},
title = {{Learning Concepts Described By Weight Aggregation Logic}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {10:1--10: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.10},
URN = {urn:nbn:de:0030-drops-134447},
doi = {10.4230/LIPIcs.CSL.2021.10},
annote = {Keywords: first-order definable concept learning, agnostic probably approximately correct learning, classification problems, locality, Feferman-Vaught decomposition, Gaifman normal form, first-order logic with counting, weight aggregation logic}
}
Document
Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle
Abstract
One of the differences between Brouwerian intuitionistic logic and classical logic is their treatment of time. In classical logic truth is atemporal, whereas in intuitionistic logic it is time-relative. Thus, in intuitionistic logic it is possible to acquire new knowledge as time progresses, whereas the classical Law of Excluded Middle (LEM) is essentially flattening the notion of time stating that it is possible to decide whether or not some knowledge will ever be acquired. This paper demonstrates that, nonetheless, the two approaches are not necessarily incompatible by introducing an intuitionistic type theory along with a Beth-like model for it that provide some middle ground. On one hand they incorporate a notion of progressing time and include evolving mathematical entities in the form of choice sequences, and on the other hand they are consistent with a variant of the classical LEM. Accordingly, this new type theory provides the basis for a more classically inclined Brouwerian intuitionistic type theory.
Cite as
Mark Bickford, Liron Cohen, Robert L. Constable, and Vincent Rahli. Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bickford_et_al:LIPIcs.CSL.2021.11,
author = {Bickford, Mark and Cohen, Liron and Constable, Robert L. and Rahli, Vincent},
title = {{Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {11:1--11:23},
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.11},
URN = {urn:nbn:de:0030-drops-134455},
doi = {10.4230/LIPIcs.CSL.2021.11},
annote = {Keywords: Intuitionism, Extensional type theory, Constructive Type Theory, Realizability, Choice sequences, Classical Logic, Law of Excluded Middle, Theorem proving, Coq}
}
Document
Discounted-Sum Automata with Multiple Discount Factors
Abstract
Discounting the influence of future events is a key paradigm in economics and it is widely used in computer-science models, such as games, Markov decision processes (MDPs), reinforcement learning, and automata. While a single game or MDP may allow for several different discount factors, discounted-sum automata (NDAs) were only studied with respect to a single discount factor. For every integer λ ∈ ℕ⧵{0,1}, as opposed to every λ ∈ ℚ⧵ℕ, the class of NDAs with discount factor λ (λ-NDAs) has good computational properties: it is closed under determinization and under the algebraic operations min, max, addition, and subtraction, and there are algorithms for its basic decision problems, such as automata equivalence and containment.
We define and analyze discounted-sum automata in which each transition can have a different integral discount factor (integral NMDAs). We show that integral NMDAs with an arbitrary choice of discount factors are not closed under determinization and under algebraic operations. We then define and analyze a restricted class of integral NMDAs, which we call tidy NMDAs, in which the choice of discount factors depends on the prefix of the word read so far. Tidy NMDAs are as expressive as deterministic integral NMDAs with an arbitrary choice of discount factors, and some of their special cases are NMDAs in which the discount factor depends on the action (alphabet letter) or on the elapsed time.
We show that for every function θ that defines the choice of discount factors, the class of θ-NMDAs enjoys all of the above good properties of integral NDAs, as well as the same complexities of the required decision problems. To this end, we also improve the previously known complexities of the decision problems of integral NDAs, and present tight bounds on the size blow-up involved in algebraic operations on them.
All our results hold equally for automata on finite words and for automata on infinite words.
Cite as
Udi Boker and Guy Hefetz. Discounted-Sum Automata with Multiple Discount Factors. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{boker_et_al:LIPIcs.CSL.2021.12,
author = {Boker, Udi and Hefetz, Guy},
title = {{Discounted-Sum Automata with Multiple Discount Factors}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {12:1--12:23},
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.12},
URN = {urn:nbn:de:0030-drops-134468},
doi = {10.4230/LIPIcs.CSL.2021.12},
annote = {Keywords: Automata, Discounted-sum, Quantitative verification, NMDA, NDA}
}
Document
Reachability in Distributed Memory Automata
Abstract
We introduce Distributed Memory Automata, a model of register automata suitable to capture some features of distributed algorithms designed for shared-memory systems. In this model, each participant owns a local register and a shared register and has the ability to change its local value, to write it in the global memory and to test atomically the number of occurrences of its value in the shared memory, up to some threshold. We show that the control-state reachability problem for Distributed Memory Automata is Pspace-complete for a fixed number of participants and is in Pspace when the number of participants is not fixed a priori.
Cite as
Benedikt Bollig, Fedor Ryabinin, and Arnaud Sangnier. Reachability in Distributed Memory Automata. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{bollig_et_al:LIPIcs.CSL.2021.13,
author = {Bollig, Benedikt and Ryabinin, Fedor and Sangnier, Arnaud},
title = {{Reachability in Distributed Memory Automata}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {13:1--13:16},
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.13},
URN = {urn:nbn:de:0030-drops-134472},
doi = {10.4230/LIPIcs.CSL.2021.13},
annote = {Keywords: Distributed algorithms, Atomic snapshot objects, Register automata, Reachability}
}
Document
Pregrammars and Intersection Types
Abstract
A representation of intersection types in terms of pregrammars is presented. Pregrammar based rewriting relations, corresponding respectively to type checking and inhabitation are defined and the latter is used to implement a Wajsberg/Ben-Yelles style alternating semi-decision algorithm for inhabitation. The usefulness of the framework is illustrated by revisiting and partially extending standard inhabitation related results for intersection types, as well as establishing new ones. It is shown how the notion of bounded multiset dimension emerges naturally and the relation between the two settings is clarified. A meaningful rank independent superset of the set of rank 2 types is identified for which EXPSPACE-completeness for inhabitation as well as for counting is proved. Finally, a standard result on negatively non-duplicated simple types is extended to intersection types.
Cite as
Sabine Broda. Pregrammars and Intersection Types. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{broda:LIPIcs.CSL.2021.14,
author = {Broda, Sabine},
title = {{Pregrammars and Intersection Types}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {14:1--14:22},
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.14},
URN = {urn:nbn:de:0030-drops-134481},
doi = {10.4230/LIPIcs.CSL.2021.14},
annote = {Keywords: Intersection Types, Pregrammars, Inhabitation}
}
Document
Learning Automata and Transducers: A Categorical Approach
Abstract
In this paper, we present a categorical approach to learning automata over words, in the sense of the L*-algorithm of Angluin. This yields a new generic L*-like algorithm which can be instantiated for learning deterministic automata, automata weighted over fields, as well as subsequential transducers. The generic nature of our algorithm is obtained by adopting an approach in which automata are simply functors from a particular category representing words to a "computation category". We establish that the sufficient properties for yielding the existence of minimal automata (that were disclosed in a previous paper), in combination with some additional hypotheses relative to termination, ensure the correctness of our generic algorithm.
Cite as
Thomas Colcombet, Daniela Petrişan, and Riccardo Stabile. Learning Automata and Transducers: A Categorical Approach. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{colcombet_et_al:LIPIcs.CSL.2021.15,
author = {Colcombet, Thomas and Petri\c{s}an, Daniela and Stabile, Riccardo},
title = {{Learning Automata and Transducers: A Categorical Approach}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {15:1--15:17},
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.15},
URN = {urn:nbn:de:0030-drops-134498},
doi = {10.4230/LIPIcs.CSL.2021.15},
annote = {Keywords: Automata, transducer, learning, category}
}
Document
Game Comonads & Generalised Quantifiers
Abstract
Game comonads, introduced by Abramsky, Dawar and Wang and developed by Abramsky and Shah, give an interesting categorical semantics to some Spoiler-Duplicator games that are common in finite model theory. In particular they expose connections between one-sided and two-sided games, and parameters such as treewidth and treedepth and corresponding notions of decomposition. In the present paper, we expand the realm of game comonads to logics with generalised quantifiers. In particular, we introduce a comonad graded by two parameter n ≤ k such that isomorphisms in the resulting Kleisli category are exactly Duplicator winning strategies in Hella’s n-bijection game with k pebbles. We define a one-sided version of this game which allows us to provide a categorical semantics for a number of logics with generalised quantifiers. We also give a novel notion of tree decomposition that emerges from the construction.
Cite as
Adam Ó Conghaile and Anuj Dawar. Game Comonads & Generalised Quantifiers. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{conghaile_et_al:LIPIcs.CSL.2021.16,
author = {Conghaile, Adam \'{O} and Dawar, Anuj},
title = {{Game Comonads \& Generalised Quantifiers}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {16:1--16:17},
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.16},
URN = {urn:nbn:de:0030-drops-134501},
doi = {10.4230/LIPIcs.CSL.2021.16},
annote = {Keywords: Logic, Finite Model Theory, Game Comonads, Generalised Quantifiers}
}
Document
Semiring Provenance for Fixed-Point Logic
Abstract
Semiring provenance is a successful approach, originating in database theory, to providing detailed information on how atomic facts combine to yield the result of a query. In particular, general provenance semirings of polynomials or formal power series provide precise descriptions of the evaluation strategies or "proof trees" for the query. By evaluating these descriptions in specific application semirings, one can extract practical information for instance about the confidence of a query or the cost of its evaluation.
This paper develops semiring provenance for very general logical languages featuring the full interaction between negation and fixed-point inductions or, equivalently, arbitrary interleavings of least and greatest fixed points. This also opens the door to provenance analysis applications for modal μ-calculus and temporal logics, as well as for finite and infinite model-checking games.
Interestingly, the common approach based on Kleene’s Fixed-Point Theorem for ω-continuous semirings is not sufficient for these general languages. We show that an adequate framework for the provenance analysis of full fixed-point logics is provided by semirings that are (1) fully continuous, and (2) absorptive. Full continuity guarantees that provenance values of least and greatest fixed-points are well-defined. Absorptive semirings provide a symmetry between least and greatest fixed-points and make sure that provenance values of greatest fixed points are informative.
We identify semirings of generalized absorptive polynomials S^{∞}[X] and prove universal properties that make them the most general appropriate semirings for our framework. These semirings have the further property of being (3) chain-positive, which is responsible for having truth-preserving interpretations that give non-zero values to all true formulae. We relate the provenance analysis of fixed-point formulae with provenance values of plays and strategies in the associated model-checking games. Specifically, we prove that the provenance value of a fixed point formula gives precise information on the evaluation strategies in these games.
Cite as
Katrin M. Dannert, Erich Grädel, Matthias Naaf, and Val Tannen. Semiring Provenance for Fixed-Point Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 17:1-17:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{dannert_et_al:LIPIcs.CSL.2021.17,
author = {Dannert, Katrin M. and Gr\"{a}del, Erich and Naaf, Matthias and Tannen, Val},
title = {{Semiring Provenance for Fixed-Point Logic}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {17:1--17:22},
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.17},
URN = {urn:nbn:de:0030-drops-134518},
doi = {10.4230/LIPIcs.CSL.2021.17},
annote = {Keywords: Finite Model Theory, Semiring Provenance, Absorptive Semirings, Fixed-Point Logics}
}
Document
Extension Preservation in the Finite and Prefix Classes of First Order Logic
Abstract
It is well known that the classic Łoś-Tarski preservation theorem fails in the finite: there are first-order definable classes of finite structures closed under extensions which are not definable (in the finite) in the existential fragment of first-order logic. We strengthen this by constructing for every n, first-order definable classes of finite structures closed under extensions which are not definable with n quantifier alternations. The classes we construct are definable in the extension of Datalog with negation and indeed in the existential fragment of transitive-closure logic. This answers negatively an open question posed by Rosen and Weinstein.
Cite as
Anuj Dawar and Abhisekh Sankaran. Extension Preservation in the Finite and Prefix Classes of First Order Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 18:1-18:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{dawar_et_al:LIPIcs.CSL.2021.18,
author = {Dawar, Anuj and Sankaran, Abhisekh},
title = {{Extension Preservation in the Finite and Prefix Classes of First Order Logic}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {18:1--18:13},
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.18},
URN = {urn:nbn:de:0030-drops-134520},
doi = {10.4230/LIPIcs.CSL.2021.18},
annote = {Keywords: finite model theory, preservation theorems, extension closed, composition, Datalog, Ehrenfeucht-Fraisse games}
}
Document
Realizability with Stateful Computations for Nonstandard Analysis
Abstract
In this paper we propose a new approach to realizability interpretations for nonstandard arithmetic. We deal with nonstandard analysis in the context of intuitionistic realizability, focusing on the Lightstone-Robinson construction of a model for nonstandard analysis through an ultrapower. In particular, we consider an extension of the λ-calculus with a memory cell, that contains an integer (the state), in order to indicate in which slice of the ultrapower ℳ^{ℕ} the computation is being done. We shall pay attention to the nonstandard principles (and their computational content) obtainable in this setting. We then discuss how this product could be quotiented to mimic the Lightstone-Robinson construction.
Cite as
Bruno Dinis and Étienne Miquey. Realizability with Stateful Computations for Nonstandard Analysis. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{dinis_et_al:LIPIcs.CSL.2021.19,
author = {Dinis, Bruno and Miquey, \'{E}tienne},
title = {{Realizability with Stateful Computations for Nonstandard Analysis}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {19:1--19:23},
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.19},
URN = {urn:nbn:de:0030-drops-134531},
doi = {10.4230/LIPIcs.CSL.2021.19},
annote = {Keywords: realizability, nonstandard analysis, states, glueing, ultrafilters, {\L}o\'{s}' theorem}
}
Document
Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment
Abstract
We define a class of Separation Logic [Ishtiaq and O'Hearn, 2001; J.C. Reynolds, 2002] formulae, whose entailment problem given formulae ϕ, ψ₁, …, ψ_n, is every model of ϕ a model of some ψ_i? is 2-EXPTIME-complete. The formulae in this class are existentially quantified separating conjunctions involving predicate atoms, interpreted by the least sets of store-heap structures that satisfy a set of inductive rules, which is also part of the input to the entailment problem. Previous work [Iosif et al., 2013; Jens Katelaan et al., 2019; Jens Pagel and Florian Zuleger, 2020] consider established sets of rules, meaning that every existentially quantified variable in a rule must eventually be bound to an allocated location, i.e. from the domain of the heap. In particular, this guarantees that each structure has treewidth bounded by the size of the largest rule in the set. In contrast, here we show that establishment, although sufficient for decidability (alongside two other natural conditions), is not necessary, by providing a condition, called equational restrictedness, which applies syntactically to (dis-)equalities. The entailment problem is more general in this case, because equationally restricted rules define richer classes of structures, of unbounded treewidth. In this paper we show that
(1) every established set of rules can be converted into an equationally restricted one and
(2) the entailment problem is 2-EXPTIME-complete in the latter case, thus matching the complexity of entailments for established sets of rules [Jens Katelaan et al., 2019; Jens Pagel and Florian Zuleger, 2020].
Cite as
Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{echenim_et_al:LIPIcs.CSL.2021.20,
author = {Echenim, Mnacho and Iosif, Radu and Peltier, Nicolas},
title = {{Decidable Entailments in Separation Logic with Inductive Definitions: Beyond Establishment}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {20:1--20: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.20},
URN = {urn:nbn:de:0030-drops-134546},
doi = {10.4230/LIPIcs.CSL.2021.20},
annote = {Keywords: Separation logic, Induction definitions, Inductive theorem proving, Entailments, Complexity}
}
Document
Church’s Thesis and Related Axioms in Coq’s Type Theory
Abstract
"Church’s thesis" (CT) as an axiom in constructive logic states that every total function of type ℕ → ℕ is computable, i.e. definable in a model of computation. CT is inconsistent both in classical mathematics and in Brouwer’s intuitionism since it contradicts weak Kőnig’s lemma and the fan theorem, respectively. Recently, CT was proved consistent for (univalent) constructive type theory.
Since neither weak Kőnig’s lemma nor the fan theorem is a consequence of just logical axioms or just choice-like axioms assumed in constructive logic, it seems likely that CT is inconsistent only with a combination of classical logic and choice axioms. We study consequences of CT and its relation to several classes of axioms in Coq’s type theory, a constructive type theory with a universe of propositions which proves neither classical logical axioms nor strong choice axioms.
We thereby provide a partial answer to the question as to which axioms may preserve computational intuitions inherent to type theory, and which certainly do not. The paper can also be read as a broad survey of axioms in type theory, with all results mechanised in the Coq proof assistant.
Cite as
Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{forster:LIPIcs.CSL.2021.21,
author = {Forster, Yannick},
title = {{Church’s Thesis and Related Axioms in Coq’s Type Theory}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {21:1--21:19},
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.21},
URN = {urn:nbn:de:0030-drops-134552},
doi = {10.4230/LIPIcs.CSL.2021.21},
annote = {Keywords: Church’s thesis, constructive type theory, constructive reverse mathematics, synthetic computability theory, Coq}
}
Document
Computing Measure as a Primitive Operation in Real Number Computation
Abstract
We study the power of BSS-machines enhanced with abilities such as computing the measure of a BSS-decidable set or computing limits of BSS-computable converging sequences. Our variations coalesce into just two equivalence classes, each of which also can be described as a lower cone in the Weihrauch degrees.
We then classify computational tasks such as computing the measure of Δ⁰₂-set of reals, integrating piece-wise continuous functions and recovering a continuous function from an L₁([0, 1])-description. All these share the Weihrauch degree lim.
Cite as
Christine Gaßner, Arno Pauly, and Florian Steinberg. Computing Measure as a Primitive Operation in Real Number Computation. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{ganer_et_al:LIPIcs.CSL.2021.22,
author = {Ga{\ss}ner, Christine and Pauly, Arno and Steinberg, Florian},
title = {{Computing Measure as a Primitive Operation in Real Number Computation}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {22:1--22:22},
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.22},
URN = {urn:nbn:de:0030-drops-134564},
doi = {10.4230/LIPIcs.CSL.2021.22},
annote = {Keywords: BSS-machine, Weihrauch reducibility, integrable function, Lebesgue measure, computable analysis}
}
Document
A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations
Abstract
Program semantics is traditionally concerned with program equivalence. However, in fields like approximate, incremental and probabilistic computation, it is often useful to describe to which extent two programs behave in a similar, although non equivalent way. This has motivated the study of program (pseudo)metrics, which have found widespread applications, e.g. in differential privacy. In this paper we show that the standard metric on real numbers can be lifted to higher-order types in a novel way, yielding a metric semantics of the simply typed lambda-calculus in which types are interpreted as quantale-valued partial metric spaces. Using such metrics we define a class of higher-order denotational models, called diameter space models, that provide a quantitative semantics of approximate program transformations. Noticeably, the distances between objects of higher-types are elements of functional, thus non-numerical, quantales. This allows us to model contextual reasoning about arbitrary functions, thus deviating from classic metric semantics.
Cite as
Guillaume Geoffroy and Paolo Pistone. A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{geoffroy_et_al:LIPIcs.CSL.2021.23,
author = {Geoffroy, Guillaume and Pistone, Paolo},
title = {{A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {23:1--23: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.23},
URN = {urn:nbn:de:0030-drops-134578},
doi = {10.4230/LIPIcs.CSL.2021.23},
annote = {Keywords: Simply typed \lambda-calculus, program metrics, approximate program transformations, partial metric spaces}
}
Document
A Deep Quantitative Type System
Abstract
We investigate intersection types and resource lambda-calculus in deep-inference proof theory. We give a unified type system that is parametric in various aspects: it encompasses resource calculi, intersection-typed lambda-calculus, and simply-typed lambda-calculus; it accommodates both idempotence and non-idempotence; it characterizes strong and weak normalization; and it does so while allowing a range of algebraic laws to determine reduction behaviour, for various quantitative effects. We give a parametric resource calculus with explicit sharing, the "collection calculus", as a Curry-Howard interpretation of the type system, that embodies these computational properties.
Cite as
Giulio Guerrieri, Willem B. Heijltjes, and Joseph W.N. Paulus. A Deep Quantitative Type System. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{guerrieri_et_al:LIPIcs.CSL.2021.24,
author = {Guerrieri, Giulio and Heijltjes, Willem B. and Paulus, Joseph W.N.},
title = {{A Deep Quantitative Type System}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {24:1--24:24},
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.24},
URN = {urn:nbn:de:0030-drops-134586},
doi = {10.4230/LIPIcs.CSL.2021.24},
annote = {Keywords: Lambda-calculus, Deep inference, Intersection types, Resource calculus}
}
Document
Categorifying Non-Idempotent Intersection Types
Abstract
Non-idempotent intersection types can be seen as a syntactic presentation of a well-known denotational semantics for the lambda-calculus, the category of sets and relations. Building on previous work, we present a categorification of this line of thought in the framework of the bang calculus, an untyped version of Levy’s call-by-push-value. We define a bicategorical model for the bang calculus, whose syntactic counterpart is a suitable category of types. In the framework of distributors, we introduce intersection type distributors, a bicategorical proof relevant refinement of relational semantics. Finally, we prove that intersection type distributors characterize normalization at depth 0.
Cite as
Giulio Guerrieri and Federico Olimpieri. Categorifying Non-Idempotent Intersection Types. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 25:1-25:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{guerrieri_et_al:LIPIcs.CSL.2021.25,
author = {Guerrieri, Giulio and Olimpieri, Federico},
title = {{Categorifying Non-Idempotent Intersection Types}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {25:1--25:24},
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.25},
URN = {urn:nbn:de:0030-drops-134592},
doi = {10.4230/LIPIcs.CSL.2021.25},
annote = {Keywords: Linear logic, bang calculus, non-idempotent intersection types, distributors, relational semantics, combinatorial species, symmetric sequences, bicategory, categorification}
}
Document
The Alternating-Time μ-Calculus with Disjunctive Explicit Strategies
Abstract
Alternating-time temporal logic (ATL) and its extensions, including the alternating-time µ-calculus (AMC), serve the specification of the strategic abilities of coalitions of agents in concurrent game structures. The key ingredient of the logic are path quantifiers specifying that some coalition of agents has a joint strategy to enforce a given goal. This basic setup has been extended to let some of the agents (revocably) commit to using certain named strategies, as in ATL with explicit strategies (ATLES). In the present work, we extend ATLES with fixpoint operators and strategy disjunction, arriving at the alternating-time µ-calculus with disjunctive explicit strategies (AMCDES), which allows for a more flexible formulation of temporal properties (e.g. fairness) and, through strategy disjunction, a form of controlled non-determinism in commitments. Our main result is an ExpTime upper bound for satisfiability checking (which is thus ExpTime-complete). We also prove upper bounds QP (quasipolynomial time) and NP∩coNP for model checking under fixed interpretations of explicit strategies, and NP under open interpretation. Our key technical tool is a treatment of the AMCDES within the generic framework of coalgebraic logic, which in particular reduces the analysis of most reasoning tasks to the treatment of a very simple one-step logic featuring only propositional operators and next-step operators without nesting; we give a new model construction principle for this one-step logic that relies on a set-valued variant of first-order resolution.
Cite as
Merlin Göttlinger, Lutz Schröder, and Dirk Pattinson. The Alternating-Time μ-Calculus with Disjunctive Explicit Strategies. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{gottlinger_et_al:LIPIcs.CSL.2021.26,
author = {G\"{o}ttlinger, Merlin and Schr\"{o}der, Lutz and Pattinson, Dirk},
title = {{The Alternating-Time \mu-Calculus with Disjunctive Explicit Strategies}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {26:1--26:22},
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.26},
URN = {urn:nbn:de:0030-drops-134605},
doi = {10.4230/LIPIcs.CSL.2021.26},
annote = {Keywords: Alternating-time logic, multi-agent systems, coalitional strength}
}
Document
On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic
Abstract
Second-order Boolean logic is a generalization of QBF, whose constant alternation fragments are known to be complete for the levels of the exponential time hierarchy. We consider two types of restriction of this logic: 1) restrictions to term constructions, 2) restrictions to the form of the Boolean matrix. Of the first sort, we consider two kinds of restrictions: firstly, disallowing nested use of proper function variables, and secondly stipulating that each function variable must appear with a fixed sequence of arguments. Of the second sort, we consider Horn, Krom, and core fragments of the Boolean matrix. We classify the complexity of logics obtained by combining these two types of restrictions. We show that, in most cases, logics with k alternating blocks of function quantifiers are complete for the kth or (k-1)th level of the exponential time hierarchy. Furthermore, we establish NL-completeness for the Krom and core fragments, when k = 1 and both restrictions of the first sort are in effect.
Cite as
Miika Hannula, Juha Kontinen, Martin Lück, and Jonni Virtema. On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 27:1-27:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{hannula_et_al:LIPIcs.CSL.2021.27,
author = {Hannula, Miika and Kontinen, Juha and L\"{u}ck, Martin and Virtema, Jonni},
title = {{On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {27:1--27:22},
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.27},
URN = {urn:nbn:de:0030-drops-134610},
doi = {10.4230/LIPIcs.CSL.2021.27},
annote = {Keywords: quantified Boolean formulae, computational complexity, second-order logic, Horn and Krom fragment}
}
Document
Domain Theory in Constructive and Predicative Univalent Foundations
Abstract
We develop domain theory in constructive univalent foundations without Voevodsky’s resizing axioms. In previous work in this direction, we constructed the Scott model of PCF and proved its computational adequacy, based on directed complete posets (dcpos). Here we further consider algebraic and continuous dcpos, and construct Scott’s D_∞ model of the untyped λ-calculus. A common approach to deal with size issues in a predicative foundation is to work with information systems or abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. Here we instead accept that dcpos may be large and work with type universes to account for this. For instance, in the Scott model of PCF, the dcpos have carriers in the second universe U₁ and suprema of directed families with indexing type in the first universe U₀. Seeing a poset as a category in the usual way, we can say that these dcpos are large, but locally small, and have small filtered colimits. In the case of algebraic dcpos, in order to deal with size issues, we proceed mimicking the definition of accessible category. With such a definition, our construction of Scott’s D_∞ again gives a large, locally small, algebraic dcpo with small directed suprema.
Cite as
Tom de Jong and Martín Hötzel Escardó. Domain Theory in Constructive and Predicative Univalent Foundations. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{dejong_et_al:LIPIcs.CSL.2021.28,
author = {de Jong, Tom and Escard\'{o}, Mart{\'\i}n H\"{o}tzel},
title = {{Domain Theory in Constructive and Predicative Univalent Foundations}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {28:1--28: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.28},
URN = {urn:nbn:de:0030-drops-134625},
doi = {10.4230/LIPIcs.CSL.2021.28},
annote = {Keywords: domain theory, constructivity, predicativity, univalent foundations}
}
Document
A Cyclic Proof System for HFL_ℕ
Abstract
A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFL_ℕ, which is a higher-order predicate logic with natural numbers and alternating fixed-points. Ours is the first cyclic proof system for a higher-order logic, to our knowledge. Due to the presence of higher-order predicates and alternating fixed-points, our cyclic proof system requires a more delicate global condition on cyclic proofs than the original system of Brotherston and Simpson. We prove the decidability of checking the global condition and soundness of this system, and also prove a restricted form of standard completeness for an infinitary variant of our cyclic proof system. A potential application of our cyclic proof system is semi-automated verification of higher-order programs, based on Kobayashi et al.’s recent work on reductions from program verification to HFL_ℕ validity checking.
Cite as
Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi. A Cyclic Proof System for HFL_ℕ. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{kori_et_al:LIPIcs.CSL.2021.29,
author = {Kori, Mayuko and Tsukada, Takeshi and Kobayashi, Naoki},
title = {{A Cyclic Proof System for HFL\underline\mathbb{N}}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {29:1--29:22},
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.29},
URN = {urn:nbn:de:0030-drops-134632},
doi = {10.4230/LIPIcs.CSL.2021.29},
annote = {Keywords: Cyclic proof, higher-order logic, fixed-point logic, sequent calculus}
}
Document
Compositional Modelling of Network Games
Abstract
The analysis of games played on graph-like structures is of increasing importance due to the prevalence of social networks, both virtual and physical, in our daily life. As well as being relevant in computer science, mathematical analysis and computer simulations of such distributed games are vital methodologies in economics, politics and epidemiology, amongst other fields. Our contribution is to give compositional semantics of a family of such games as a well-behaved mapping, a strict monoidal functor, from a category of open graphs (syntax) to a category of open games (semantics). As well as introducing the theoretical framework, we identify some applications of compositionality.
Cite as
Elena Di Lavore, Jules Hedges, and Paweł Sobociński. Compositional Modelling of Network Games. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 30:1-30:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{dilavore_et_al:LIPIcs.CSL.2021.30,
author = {Di Lavore, Elena and Hedges, Jules and Soboci\'{n}ski, Pawe{\l}},
title = {{Compositional Modelling of Network Games}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {30:1--30:24},
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.30},
URN = {urn:nbn:de:0030-drops-134645},
doi = {10.4230/LIPIcs.CSL.2021.30},
annote = {Keywords: game theory, category theory, network games, open games, open graphs, compositionality}
}
Document
Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time
Abstract
In the quest for a logic capturing Ptime the next natural classes of structures to consider are those with bounded color class size. We present a canonization procedure for graphs with dihedral color classes of bounded size in the logic of Choiceless Polynomial Time (CPT), which then captures Ptime on this class of structures. This is the first result of this form for non-abelian color classes.
The first step proposes a normal form which comprises a "rigid assemblage". This roughly means that the local automorphism groups form 2-injective 3-factor subdirect products. Structures with color classes of bounded size can be reduced canonization preservingly to normal form in CPT.
In the second step, we show that for graphs in normal form with dihedral color classes of bounded size, the canonization problem can be solved in CPT. We also show the same statement for general ternary structures in normal form if the dihedral groups are defined over odd domains.
Cite as
Moritz Lichter and Pascal Schweitzer. Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 31:1-31:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{lichter_et_al:LIPIcs.CSL.2021.31,
author = {Lichter, Moritz and Schweitzer, Pascal},
title = {{Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial Time}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {31:1--31: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.31},
URN = {urn:nbn:de:0030-drops-134650},
doi = {10.4230/LIPIcs.CSL.2021.31},
annote = {Keywords: Choiceless polynomial time, canonization, relational structures, bounded color class size, dihedral groups}
}
Document
Preservation Theorems Through the Lens of Topology
Abstract
In this paper, we introduce a family of topological spaces that captures the existence of preservation theorems. The structure of those spaces allows us to study the relativisation of preservation theorems under suitable definitions of surjective morphisms, subclasses, sums, products, topological closures, and projective limits. Throughout the paper, we also integrate already known results into this new framework and show how it captures the essence of their proofs.
Cite as
Aliaume Lopez. Preservation Theorems Through the Lens of Topology. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{lopez:LIPIcs.CSL.2021.32,
author = {Lopez, Aliaume},
title = {{Preservation Theorems Through the Lens of Topology}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {32:1--32:17},
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.32},
URN = {urn:nbn:de:0030-drops-134660},
doi = {10.4230/LIPIcs.CSL.2021.32},
annote = {Keywords: Preservation theorem, Pre-spectral space, Noetherian space, Spectral space}
}
Document
Choiceless Computation and Symmetry: Limitations of Definability
Abstract
The search for a logic capturing PTIME is a long standing open problem in finite model theory. One of the most promising candidate logics for this is Choiceless Polynomial Time with counting (CPT). Abstractly speaking, CPT is an isomorphism-invariant computation model working with hereditarily finite sets as data structures. While it is easy to check that the evaluation of CPT-sentences is possible in polynomial time, the converse has been open for more than 20 years: Can every PTIME-decidable property of finite structures be expressed in CPT? We attempt to make progress towards a negative answer and show that Choiceless Polynomial Time cannot compute a preorder with colour classes of logarithmic size in every hypercube. The reason is that such preorders have super-polynomially many automorphic images, which makes it impossible for CPT to define them. While the computation of such a preorder is not a decision problem that would immediately separate P and CPT, it is significant for the following reason: The so-called Cai-Fürer-Immerman (CFI) problem is one of the standard "benchmarks" for logics and maybe best known for separating fixed-point logic with counting (FPC) from P. Hence, it is natural to consider this also a potential candidate for the separation of CPT and P. The strongest known positive result in this regard says that CPT is able to solve CFI if a preorder with logarithmically sized colour classes is present in the input structure. Our result implies that this approach cannot be generalised to unordered inputs. In other words, CFI on unordered hypercubes is a PTIME-problem which provably cannot be tackled with the state-of-the-art choiceless algorithmic techniques.
Cite as
Benedikt Pago. Choiceless Computation and Symmetry: Limitations of Definability. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{pago:LIPIcs.CSL.2021.33,
author = {Pago, Benedikt},
title = {{Choiceless Computation and Symmetry: Limitations of Definability}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {33:1--33:21},
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.33},
URN = {urn:nbn:de:0030-drops-134673},
doi = {10.4230/LIPIcs.CSL.2021.33},
annote = {Keywords: finite model theory, descriptive complexity, choiceless computation, symmetries of combinatorial objects}
}
Document
Typable Fragments of Polynomial Automatic Amortized Resource Analysis
Abstract
Being a fully automated technique for resource analysis, automatic amortized resource analysis (AARA) can fail in returning worst-case cost bounds of programs, fundamentally due to the undecidability of resource analysis. For programmers who are unfamiliar with the technical details of AARA, it is difficult to predict whether a program can be successfully analyzed in AARA. Motivated by this problem, this article identifies classes of programs that can be analyzed in type-based polynomial AARA. Firstly, it is shown that the set of functions that are typable in univariate polynomial AARA coincides with the complexity class PTime. Secondly, the article presents a sufficient condition for typability that axiomatically requires every sub-expression of a given program to be polynomial-time. It is proved that this condition implies typability in multivariate polynomial AARA under some syntactic restrictions.
Cite as
Long Pham and Jan Hoffmann. Typable Fragments of Polynomial Automatic Amortized Resource Analysis. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 34:1-34:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{pham_et_al:LIPIcs.CSL.2021.34,
author = {Pham, Long and Hoffmann, Jan},
title = {{Typable Fragments of Polynomial Automatic Amortized Resource Analysis}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {34:1--34:19},
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.34},
URN = {urn:nbn:de:0030-drops-134681},
doi = {10.4230/LIPIcs.CSL.2021.34},
annote = {Keywords: Resource consumption, Quantitative analysis, Amortized analysis, Typability}
}
Document
The Yoneda Reduction of Polymorphic Types
Abstract
In this paper we explore a family of type isomorphisms in System F whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isomorphisms hold under theories of equivalence stronger than βη-equivalence, like those induced by parametricity and dinaturality. We show that the Yoneda type isomorphisms yield a rewriting over types, that we call Yoneda reduction, which can be used to eliminate quantifiers from a polymorphic type, replacing them with a combination of monomorphic type constructors. We establish some sufficient conditions under which quantifiers can be fully eliminated from a polymorphic type, and we show some application of these conditions to count the inhabitants of a type and to compute program equivalence in some fragments of System F.
Cite as
Paolo Pistone and Luca Tranchini. The Yoneda Reduction of Polymorphic Types. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{pistone_et_al:LIPIcs.CSL.2021.35,
author = {Pistone, Paolo and Tranchini, Luca},
title = {{The Yoneda Reduction of Polymorphic Types}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {35:1--35:22},
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.35},
URN = {urn:nbn:de:0030-drops-134696},
doi = {10.4230/LIPIcs.CSL.2021.35},
annote = {Keywords: System F, Type isomorphisms, Yoneda isomorphism, Program equivalence}
}
Document
Degrees of Ambiguity for Parity Tree Automata
Abstract
An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is finitely (respectively, countably) ambiguous if for every input it has at most finitely (respectively, countably) many accepting computations. An automaton is boundedly ambiguous if there is k ∈ ℕ, such that for every input it has at most k accepting computations. We consider Parity Tree Automata (PTA) and prove that the problem whether a PTA is not unambiguous (respectively, is not boundedly ambiguous, not finitely ambiguous) is co-NP complete, and the problem whether a PTA is not countably ambiguous is co-NP hard.
Cite as
Alexander Rabinovich and Doron Tiferet. Degrees of Ambiguity for Parity Tree Automata. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{rabinovich_et_al:LIPIcs.CSL.2021.36,
author = {Rabinovich, Alexander and Tiferet, Doron},
title = {{Degrees of Ambiguity for Parity Tree Automata}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {36:1--36:20},
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.36},
URN = {urn:nbn:de:0030-drops-134709},
doi = {10.4230/LIPIcs.CSL.2021.36},
annote = {Keywords: automata on infinite trees, degree of ambiguity, omega word automata, parity automata}
}
Document
On Flat Lossy Channel Machines
Abstract
We show that reachability, repeated reachability, nontermination and unboundedness are NP-complete for Lossy Channel Machines that are flat, i.e., with no nested cycles in the control graph. The upper complexity bound relies on a fine analysis of iterations of lossy channel actions and uses compressed word techniques for efficiently reasoning with paths of exponential lengths. The lower bounds already apply to acyclic or single-path machines.
Cite as
Philippe Schnoebelen. On Flat Lossy Channel Machines. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 37:1-37:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{schnoebelen:LIPIcs.CSL.2021.37,
author = {Schnoebelen, Philippe},
title = {{On Flat Lossy Channel Machines}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {37:1--37:22},
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.37},
URN = {urn:nbn:de:0030-drops-134712},
doi = {10.4230/LIPIcs.CSL.2021.37},
annote = {Keywords: Infinite state systems, Automated verification, Flat systems, Lossy channels}
}
Document
Realizability Without Symmetry
Abstract
In categorical realizability, it is common to construct categories of assemblies and modest sets from applicative structures. In this paper, we introduce several classes of applicative structures and apply the categorical realizability construction to them. Then we obtain closed multicategories, closed categories and skew closed categories, which are more general categorical structures than Cartesian closed categories and symmetric monoidal closed categories. Moreover, we give the necessary and sufficient conditions for obtaining closed multicategories and closed categories of assemblies.
Cite as
Haruka Tomita. Realizability Without Symmetry. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 38:1-38:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
Copy BibTex To Clipboard
@InProceedings{tomita:LIPIcs.CSL.2021.38,
author = {Tomita, Haruka},
title = {{Realizability Without Symmetry}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {38:1--38:16},
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.38},
URN = {urn:nbn:de:0030-drops-134729},
doi = {10.4230/LIPIcs.CSL.2021.38},
annote = {Keywords: Realizability, combinatory algebra, closed multicategory, closed category, skew closed category}
}