Volume
LIPIcs, Volume 252
31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Event
CSL 2023, February 13-16, 2023, Warsaw, PolandEditors
Publication Details
- published at: 2023-02-01
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-264-8
- DBLP: db/conf/csl/csl2023
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 252, CSL 2023, Complete Volume
Abstract
LIPIcs, Volume 252, CSL 2023, Complete Volume
Cite as
31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 1-718, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@Proceedings{klin_et_al:LIPIcs.CSL.2023,
title = {{LIPIcs, Volume 252, CSL 2023, Complete Volume}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {1--718},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023},
URN = {urn:nbn:de:0030-drops-174603},
doi = {10.4230/LIPIcs.CSL.2023},
annote = {Keywords: LIPIcs, Volume 252, CSL 2023, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{klin_et_al:LIPIcs.CSL.2023.0,
author = {Klin, Bartek and Pimentel, Elaine},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {0:i--0:xviii},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.0},
URN = {urn:nbn:de:0030-drops-174614},
doi = {10.4230/LIPIcs.CSL.2023.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Asymptotic Rewriting (Invited Talk)
Abstract
Rewriting is a foundation for the operational theory of programming languages. The process of rewriting describes the computation of a result (typically, a normal form), with lambda-calculus being the paradigmatic example for rewriting as an abstract form of program execution. Taking this view, the execution of a program is formalized as a specific evaluation strategy, while the general rewriting theory allows for program transformations, optimizations, parallel/distributed implementations, and provides a base on which to reason about program equivalence.
In this talk, we discuss what happens when the notion of termination is asymptotic, that is, the result of computation appears as a limit, as opposed to reaching a normal form in a finite number of steps.
- Example 1. A natural example is probabilistic computation. A probabilistic program P is a stochastic model generating a distribution over all possible outputs of P. Even if the termination probability is 1 (almost sure termination), that degree of certitude is typically not reached in a finite number of steps, but as a limit. A standard example is a term M that reduces to either a normal form or M itself, with equal probability 1/2. After n steps, M is in normal form with probability 1/2 + 1/(2²) + … + 1/(2ⁿ). Only at the limit this computation terminates with probability 1.
- Example 2. Infinitary lambda-calculi (where the limits are infinitary terms such as Böhm trees), streams, algebraic rewriting systems, effectful computation (e.g. computation with outputs), quantum lambda-calculi provide several other relevant examples.
Instances of asymptotic computation are quite diverse, and moreover the specific syntax of each system may be rather complex. In the talk, we present asymptotic rewriting in a way which is independent of the specific details of each calculus, and we provide a toolkit of proof-techniques which are of general application. To do so, we rely on Quantitative Abstract Rewriting System [Claudia Faggian, 2022; Claudia Faggian and Giulio Guerrieri, 2022], building on work by Ariola and Blom [Ariola and Blom, 2002], which enrich with quantitative information the theory of Abstract Rewriting Systems (ARS) (see e.g. [Terese, 2003] or [Baader and Nipkow, 1998]). ARS are indeed the core of finitary rewriting, capturing the common substratum of rewriting theory and term transformation, independently from the particular structure of the objects. It seems then natural to seek a similar foundation for asymptotic computation. The issue is that the arguments relying on finitary termination do not transfer, in general, to limits (a game changer being that asymptotic termination does not provide a well-founded order): we need to develope an opportune formalization and suitable proof techniques.
The goal is then to identify and develop methods which only rely on the asymptotic argument - abstracting from structure specific to a setting - and so will apply to any concrete instance. For example, in infinitary lambda calculus, the limit is usually a (possibly infinite) limit term, while in probabilistic lambda calculus, the limit is a distribution over (finite) terms. The former is concerned with the depth of the redexes, the latter with the probability of reaching a result. The abstract notions of limit and of normalization subsumes both, and so abstract results apply to either setting.
Cite as
Claudia Faggian. Asymptotic Rewriting (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{faggian:LIPIcs.CSL.2023.1,
author = {Faggian, Claudia},
title = {{Asymptotic Rewriting}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.1},
URN = {urn:nbn:de:0030-drops-174621},
doi = {10.4230/LIPIcs.CSL.2023.1},
annote = {Keywords: rewriting, probabilistic rewriting, confluence, strategies, asymptotic normalization, lambda calculus}
}
Document
Invited Talk
Inductive Inference and Epistemic Modal Logic (Invited Talk)
Abstract
This paper is concerned with a link between inductive inference and dynamic epistemic logic. The bridge was first introduced in [Gierasimczuk, 2009; Nina Gierasimczuk, 2009; Gierasimczuk, 2010]. We present a synthetic view on subsequent contributions: inductive truth-tracking properties of belief revision policies seen as belief upgrade methods; topological interpretation and characterisation of inductive inference; discussion of the adequacy of the topological semantics of modal logic for characterising inductive inference. We briefly present the topological Dynamic Logic for Learning Theory. Finally, we discuss several surprising results obtained in computational inductive inference that challenge the usual understanding of certainty, and of rational inquiry as consistent and conservative learning.
Cite as
Nina Gierasimczuk. Inductive Inference and Epistemic Modal Logic (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 2:1-2:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{gierasimczuk:LIPIcs.CSL.2023.2,
author = {Gierasimczuk, Nina},
title = {{Inductive Inference and Epistemic Modal Logic}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {2:1--2:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.2},
URN = {urn:nbn:de:0030-drops-174634},
doi = {10.4230/LIPIcs.CSL.2023.2},
annote = {Keywords: modal logic, dynamic epistemic logic, inductive inference, topological semantics, computational learning theory, finite identifiability, identifiability in the limit}
}
Document
Invited Talk
A Positive Perspective on Term Representation (Invited Talk)
Abstract
We use the focused proof system LJF as a framework for describing term structures and substitution. Since the proof theory of LJF does not pick a canonical polarization for primitive types, two different approaches to term representation arise. When primitive types are given the negative polarity, LJF proofs encode terms as tree-like structures in a familiar fashion. In this situation, cut elimination also yields the familiar notion of substitution. On the other hand, when primitive types are given the positive polarity, LJF proofs yield a structure in which explicit sharing of term structures is possible. Such a representation of terms provides an explicit method for sharing term structures. In this setting, cut elimination yields a different notion of substitution. We illustrate these two approaches to term representation by applying them to the encoding of untyped λ-terms. We also exploit concurrency theory techniques - namely traces and simulation - to compare untyped λ-terms using such different structuring disciplines.
Cite as
Dale Miller and Jui-Hsuan Wu. A Positive Perspective on Term Representation (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{miller_et_al:LIPIcs.CSL.2023.3,
author = {Miller, Dale and Wu, Jui-Hsuan},
title = {{A Positive Perspective on Term Representation}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {3:1--3:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.3},
URN = {urn:nbn:de:0030-drops-174648},
doi = {10.4230/LIPIcs.CSL.2023.3},
annote = {Keywords: term representation, sharing, focused proof systems}
}
Document
Invited Talk
Enhanced Induction in Behavioural Relations (Invited Talk)
Abstract
We outline an attempt at transporting the well-known theory of enhancements for the coinduction proof method, widely used on behavioural relations such as bisimilarity, onto the realms of inductive behaviour relations, i.e., relations defined from inductive observables, and discuss relevant literature.
Cite as
Davide Sangiorgi. Enhanced Induction in Behavioural Relations (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{sangiorgi:LIPIcs.CSL.2023.4,
author = {Sangiorgi, Davide},
title = {{Enhanced Induction in Behavioural Relations}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {4:1--4:6},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.4},
URN = {urn:nbn:de:0030-drops-174658},
doi = {10.4230/LIPIcs.CSL.2023.4},
annote = {Keywords: coinduction, induction, semantics, behavioural relations}
}
Document
A Cyclic Proof System for Full Computation Tree Logic
Abstract
Full Computation Tree Logic, commonly denoted CTL*, is the extension of Linear Temporal Logic LTL by path quantification for reasoning about branching time. In contrast to traditional Computation Tree Logic CTL, the path quantifiers are not bound to specific linear modalities, resulting in a more expressive language. We present a sound and complete hypersequent calculus for CTL*. The proof system is cyclic in the sense that proofs are finite derivation trees with back-edges. A syntactic success condition on non-axiomatic leaves guarantees soundness. Completeness is established by relating cyclic proofs to a natural ill-founded sequent calculus for the logic.
Cite as
Bahareh Afshari, Graham E. Leigh, and Guillermo Menéndez Turata. A Cyclic Proof System for Full Computation Tree Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{afshari_et_al:LIPIcs.CSL.2023.5,
author = {Afshari, Bahareh and Leigh, Graham E. and Men\'{e}ndez Turata, Guillermo},
title = {{A Cyclic Proof System for Full Computation Tree Logic}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {5:1--5:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.5},
URN = {urn:nbn:de:0030-drops-174664},
doi = {10.4230/LIPIcs.CSL.2023.5},
annote = {Keywords: Full computation tree logic, Hypersequent calculus, Cyclic proofs}
}
Document
Functorial String Diagrams for Reverse-Mode Automatic Differentiation
Abstract
We formulate a reverse-mode automatic differentiation (RAD) algorithm for (applied) simply typed lambda calculus in the style of Pearlmutter and Siskind [Barak A. Pearlmutter and Jeffrey Mark Siskind, 2008], using the graphical formalism of string diagrams. Thanks to string diagram rewriting, we are able to formally prove for the first time the soundness of such an algorithm. Our approach requires developing a calculus of string diagrams with hierarchical features in the spirit of functorial boxes, in order to model closed monoidal (and cartesian closed) structure. To give an efficient yet principled implementation of the RAD algorithm, we use foliations of our hierarchical string diagrams.
Cite as
Mario Alvarez-Picallo, Dan Ghica, David Sprunger, and Fabio Zanasi. Functorial String Diagrams for Reverse-Mode Automatic Differentiation. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{alvarezpicallo_et_al:LIPIcs.CSL.2023.6,
author = {Alvarez-Picallo, Mario and Ghica, Dan and Sprunger, David and Zanasi, Fabio},
title = {{Functorial String Diagrams for Reverse-Mode Automatic Differentiation}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {6:1--6:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.6},
URN = {urn:nbn:de:0030-drops-174674},
doi = {10.4230/LIPIcs.CSL.2023.6},
annote = {Keywords: string diagrams, automatic differentiation, hierarchical hypergraphs}
}
Document
A Lattice-Theoretical View of Strategy Iteration
Abstract
Strategy iteration is a technique frequently used for two-player games in order to determine the winner or compute payoffs, but to the best of our knowledge no general framework for strategy iteration has been considered. Inspired by previous work on simple stochastic games, we propose a general formalisation of strategy iteration for solving least fixpoint equations over a suitable class of complete lattices, based on MV-chains. We devise algorithms that can be used for non-expansive fixpoint functions represented as so-called min- respectively max-decompositions. Correspondingly, we develop two different techniques: strategy iteration from above, which has to solve the problem that iteration might reach a fixpoint that is not the least, and from below, which is algorithmically simpler, but requires a more involved correctness argument. We apply our method to solve energy games and compute behavioural metrics for probabilistic automata.
Cite as
Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. A Lattice-Theoretical View of Strategy Iteration. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{baldan_et_al:LIPIcs.CSL.2023.7,
author = {Baldan, Paolo and Eggert, Richard and K\"{o}nig, Barbara and Padoan, Tommaso},
title = {{A Lattice-Theoretical View of Strategy Iteration}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {7:1--7:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.7},
URN = {urn:nbn:de:0030-drops-174680},
doi = {10.4230/LIPIcs.CSL.2023.7},
annote = {Keywords: games, strategy iteration, fixpoints, energy games, behavioural metrics}
}
Document
Reductions in Higher-Order Rewriting and Their Equivalence
Abstract
Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. We study the problem of extending the notion of proof term to higher-order rewriting, which generalizes the first-order setting by allowing terms with binders and higher-order substitution. In previous works that devise proof terms for higher-order rewriting, such as Bruggink’s, it has been noted that the challenge lies in reconciling composition of proof terms and higher-order substitution (β-equivalence). This led Bruggink to reject "nested" composition, other than at the outermost level. In this paper, we propose a notion of higher-order proof term we dub rewrites that supports nested composition. We then define two notions of equivalence on rewrites, namely permutation equivalence and projection equivalence, and show that they coincide.
Cite as
Pablo Barenbaum and Eduardo Bonelli. Reductions in Higher-Order Rewriting and Their Equivalence. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{barenbaum_et_al:LIPIcs.CSL.2023.8,
author = {Barenbaum, Pablo and Bonelli, Eduardo},
title = {{Reductions in Higher-Order Rewriting and Their Equivalence}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {8:1--8:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.8},
URN = {urn:nbn:de:0030-drops-174694},
doi = {10.4230/LIPIcs.CSL.2023.8},
annote = {Keywords: Term Rewriting, Higher-Order Rewriting, Proof terms, Equivalence of Computations}
}
Document
Proofs and Refutations for Intuitionistic and Second-Order Logic
Abstract
The λ^{PRK}-calculus is a typed λ-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical propositional logic. In this work, we extend λ^{PRK} to encompass classical second-order logic, by incorporating parametric polymorphism and existential types. The system is shown to enjoy good computational properties, such as type preservation, confluence, and strong normalization, which is established by means of a reducibility argument. We identify a syntactic restriction on proofs that characterizes exactly the intuitionistic fragment of second-order λ^{PRK}, and we study canonicity results.
Cite as
Pablo Barenbaum and Teodoro Freund. Proofs and Refutations for Intuitionistic and Second-Order Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{barenbaum_et_al:LIPIcs.CSL.2023.9,
author = {Barenbaum, Pablo and Freund, Teodoro},
title = {{Proofs and Refutations for Intuitionistic and Second-Order Logic}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {9:1--9:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.9},
URN = {urn:nbn:de:0030-drops-174707},
doi = {10.4230/LIPIcs.CSL.2023.9},
annote = {Keywords: lambda-calculus, propositions-as-types, classical logic, proof normalization}
}
Document
The Functional Machine Calculus II: Semantics
Abstract
The Functional Machine Calculus (FMC), recently introduced by the second author, is a generalization of the lambda-calculus which may faithfully encode the effects of higher-order mutable store, I/O and probabilistic/non-deterministic input. Significantly, it remains confluent and can be simply typed in the presence of these effects.
In this paper, we explore the denotational semantics of the FMC. We have three main contributions: first, we argue that its syntax - in which both effects and lambda-calculus are realised using the same syntactic constructs - is semantically natural, corresponding closely to the structure of a Scott-style domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy’s proof for the lambda-calculus, including a small simplification of the technique. Finally, we show that the typed FMC (without considering the specifics of encoded effects), modulo an appropriate equational theory, is a complete language for Cartesian closed categories.
Cite as
Chris Barrett, Willem Heijltjes, and Guy McCusker. The Functional Machine Calculus II: Semantics. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{barrett_et_al:LIPIcs.CSL.2023.10,
author = {Barrett, Chris and Heijltjes, Willem and McCusker, Guy},
title = {{The Functional Machine Calculus II: Semantics}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {10:1--10:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.10},
URN = {urn:nbn:de:0030-drops-174716},
doi = {10.4230/LIPIcs.CSL.2023.10},
annote = {Keywords: lambda-calculus, computational effects, denotational semantics, strong normalization}
}
Document
Degree Spectra, and Relative Acceptability of Notations
Abstract
We investigate the interplay between the degree spectrum of a computable relation R on the computable structure (ω, <), i.e., natural numbers with the standard order, and the computability of the successor, relativized to that relation, in all computable copies of the structure - the property we dub successor’s recoverability. In computable structure theory, this property is used to show that of all possible Turing degrees that could belong to the spectrum of R (namely, of all Δ₂ degrees), in fact only the computably enumerable degrees are contained in the spectrum. Interestingly, successor’s recoverability (in the unrelativized form) appears also in philosophy of computing where it is used to distinguish between acceptable and deviant encodings (notations) of natural numbers. Since Shapiro’s notations are rarely seen through the lens of computable structure theory, we first lay the elementary conceptual groundwork to understand notations in terms of computable structures and show how results pertinent to the former can fundamentally inform our understanding of the latter. Secondly, we prove a new result which shows that for a large class of computable relations (satisfying a certain effectiveness condition), having all c.e. degrees as a spectrum implies that the successor is recoverable from the relation. The recoverability of successor may be otherwise seen as relativized acceptability of every notation for the structure. We end with remarks about connections of our result to relative computable categoricity and to a similar direction pursued by Matthew Harrison-Trainor in [Harrison-Trainor, 2018], and with an open question.
Cite as
Nikolay Bazhenov and Dariusz Kalociński. Degree Spectra, and Relative Acceptability of Notations. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{bazhenov_et_al:LIPIcs.CSL.2023.11,
author = {Bazhenov, Nikolay and Kaloci\'{n}ski, Dariusz},
title = {{Degree Spectra, and Relative Acceptability of Notations}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {11:1--11:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.11},
URN = {urn:nbn:de:0030-drops-174725},
doi = {10.4230/LIPIcs.CSL.2023.11},
annote = {Keywords: Computable structure theory, Degree spectra, \omega-type order, C.e. degrees, \Delta₂ degrees, Acceptable notation, Successor, Learnability}
}
Document
Hennessy-Milner Theorems via Galois Connections
Abstract
We introduce a general and compositional, yet simple, framework that allows to derive soundness and expressiveness results for modal logics characterizing behavioural equivalences or metrics (also known as Hennessy-Milner theorems). It is based on Galois connections between sets of (real-valued) predicates on the one hand and equivalence relations/metrics on the other hand and covers a part of the linear-time-branching-time spectrum, both for the qualitative case (behavioural equivalences) and the quantitative case (behavioural metrics). We derive behaviour functions from a given logic and give a condition, called compatibility, that characterizes under which conditions a logically induced equivalence/metric is induced by a fixpoint equation. In particular, this framework allows to derive a new fixpoint characterization of directed trace metrics.
Cite as
Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Hennessy-Milner Theorems via Galois Connections. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{beohar_et_al:LIPIcs.CSL.2023.12,
author = {Beohar, Harsh and Gurke, Sebastian and K\"{o}nig, Barbara and Messing, Karla},
title = {{Hennessy-Milner Theorems via Galois Connections}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {12:1--12:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.12},
URN = {urn:nbn:de:0030-drops-174735},
doi = {10.4230/LIPIcs.CSL.2023.12},
annote = {Keywords: behavioural equivalences and metrics, modal logics, Galois connections}
}
Document
A Curry-Howard Correspondence for Linear, Reversible Computation
Abstract
In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic μMALL: linear logic extended with least fixed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy μMALL validity criterion and how the language simulates the cut-elimination procedure of μMALL.
Cite as
Kostia Chardonnet, Alexis Saurin, and Benoît Valiron. A Curry-Howard Correspondence for Linear, Reversible Computation. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{chardonnet_et_al:LIPIcs.CSL.2023.13,
author = {Chardonnet, Kostia and Saurin, Alexis and Valiron, Beno\^{i}t},
title = {{A Curry-Howard Correspondence for Linear, Reversible Computation}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {13:1--13:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.13},
URN = {urn:nbn:de:0030-drops-174747},
doi = {10.4230/LIPIcs.CSL.2023.13},
annote = {Keywords: Reversible Computation, Linear Logic, Curry-Howard}
}
Document
Measure-Theoretic Semantics for Quantitative Parity Automata
Abstract
Quantitative parity automata (QPAs) generalise non-deterministic parity automata (NPAs) by adding weights from a certain semiring to transitions. QPAs run on infinite word/tree-like structures, modelled as coalgebras of a polynomial functor F. They can also arise as certain products between a quantitative model (with branching modelled via the same semiring of quantities, and linear behaviour described by the functor F) and an NPA (modelling a qualitative property of F-coalgebras). We build on recent work on semiring-valued measures to define a way to measure the set of paths through a quantitative branching model which satisfy a qualitative property (captured by an unambiguous NPA running on F-coalgebras). Our main result shows that the notion of extent of a QPA (which generalises non-emptiness of an NPA, and is defined as the solution of a nested system of equations) provides an equivalent characterisation of the measure of the accepting paths through the QPA. This result makes recently-developed methods for computing nested fixpoints available for model checking qualitative, linear-time properties against quantitative branching models.
Cite as
Corina Cîrstea and Clemens Kupke. Measure-Theoretic Semantics for Quantitative Parity Automata. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{cirstea_et_al:LIPIcs.CSL.2023.14,
author = {C\^{i}rstea, Corina and Kupke, Clemens},
title = {{Measure-Theoretic Semantics for Quantitative Parity Automata}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {14:1--14:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.14},
URN = {urn:nbn:de:0030-drops-174755},
doi = {10.4230/LIPIcs.CSL.2023.14},
annote = {Keywords: parity automaton, coalgebra, measure theory}
}
Document
Realizing Continuity Using Stateful Computations
Abstract
The principle of continuity is a seminal property that holds for a number of intuitionistic theories such as System T. Roughly speaking, it states that functions on real numbers only need approximations of these numbers to compute. Generally, continuity principles have been justified using semantical arguments, but it is known that the modulus of continuity of functions can be computed using effectful computations such as exceptions or reference cells. This paper presents a class of intuitionistic theories that features stateful computations, such as reference cells, and shows that these theories can be extended with continuity axioms. The modulus of continuity of the functionals on the Baire space is directly computed using the stateful computations enabled in the theory.
Cite as
Liron Cohen and Vincent Rahli. Realizing Continuity Using Stateful Computations. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{cohen_et_al:LIPIcs.CSL.2023.15,
author = {Cohen, Liron and Rahli, Vincent},
title = {{Realizing Continuity Using Stateful Computations}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {15:1--15:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.15},
URN = {urn:nbn:de:0030-drops-174761},
doi = {10.4230/LIPIcs.CSL.2023.15},
annote = {Keywords: Continuity, Stateful computations, Intuitionism, Extensional Type Theory, Constructive Type Theory, Realizability, Theorem proving, Agda}
}
Document
Non-Uniform Complexity via Non-Wellfounded Proofs
Abstract
Cyclic and non-wellfounded proofs are now increasingly employed to establish metalogical results in a variety of settings, in particular for type systems with forms of (co)induction. Under the Curry-Howard correspondence, a cyclic proof can be seen as a typing derivation "with loops", closer to low-level machine models, and so comprise a highly expressive computational model that nonetheless enjoys excellent metalogical properties.
In recent work, we showed how the cyclic proof setting can be further employed to model computational complexity, yielding characterisations of the polynomial time and elementary computable functions. These characterisations are "implicit", inspired by Bellantoni and Cook’s famous algebra of safe recursion, but exhibit greater expressivity thanks to the looping capacity of cyclic proofs.
In this work we investigate the capacity for non-wellfounded proofs, where finite presentability is relaxed, to model non-uniformity in complexity theory. In particular, we present a characterisation of the class FP/poly of functions computed by polynomial-size circuits. While relating non-wellfoundedness to non-uniformity is a natural idea, the precise amount of irregularity, informally speaking, required to capture FP/poly is given by proof-level conditions novel to cyclic proof theory. Along the way, we formalise some (presumably) folklore techniques for characterising non-uniform classes in relativised function algebras with appropriate oracles.
Cite as
Gianluca Curzi and Anupam Das. Non-Uniform Complexity via Non-Wellfounded Proofs. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{curzi_et_al:LIPIcs.CSL.2023.16,
author = {Curzi, Gianluca and Das, Anupam},
title = {{Non-Uniform Complexity via Non-Wellfounded Proofs}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {16:1--16:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.16},
URN = {urn:nbn:de:0030-drops-174770},
doi = {10.4230/LIPIcs.CSL.2023.16},
annote = {Keywords: Cyclic proofs, non-wellfounded proof-theory, non-uniform complexity, polynomial time, safe recursion, implicit complexity}
}
Document
Open Higher-Order Logic
Abstract
We introduce a variation on Barthe et al.’s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity, differentiability, or monotonicity, can be expressed and reasoned about in a very natural way, following the structure of the underlying program. We give open higher-order logic in distinct flavors, and in particular in its relational and local versions, the latter being tailored for situations in which properties hold only in part of the underlying function’s domain of definition.
Cite as
Ugo Dal Lago, Francesco Gavazzo, and Alexis Ghyselen. Open Higher-Order Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{dallago_et_al:LIPIcs.CSL.2023.17,
author = {Dal Lago, Ugo and Gavazzo, Francesco and Ghyselen, Alexis},
title = {{Open Higher-Order Logic}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {17:1--17:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.17},
URN = {urn:nbn:de:0030-drops-174785},
doi = {10.4230/LIPIcs.CSL.2023.17},
annote = {Keywords: Formal Verification, Relational Logic, First-Order Properties}
}
Document
Frobenius Structures in Star-Autonomous Categories
Abstract
It is known that the quantale of sup-preserving maps from a complete lattice to itself is a Frobenius quantale if and only if the lattice is completely distributive. Since completely distributive lattices are the nuclear objects in the autonomous category of complete lattices and sup-preserving maps, we study the above statement in a categorical setting. We introduce the notion of Frobenius structure in an arbitrary autonomous category, generalizing that of Frobenius quantale. We prove that the monoid of endomorphisms of a nuclear object has a Frobenius structure. If the environment category is star-autonomous and has epi-mono factorizations, a variant of this theorem allows to develop an abstract phase semantics and to generalise the previous statement. Conversely, we argue that, in a star-autonomous category where the monoidal unit is a dualizing object, if the monoid of endomorphisms of an object has a Frobenius structure and the monoidal unit embeds into this object as a retract, then the object is nuclear.
Cite as
Cédric de Lacroix and Luigi Santocanale. Frobenius Structures in Star-Autonomous Categories. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{delacroix_et_al:LIPIcs.CSL.2023.18,
author = {de Lacroix, C\'{e}dric and Santocanale, Luigi},
title = {{Frobenius Structures in Star-Autonomous Categories}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {18:1--18:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.18},
URN = {urn:nbn:de:0030-drops-174798},
doi = {10.4230/LIPIcs.CSL.2023.18},
annote = {Keywords: Quantale, Frobenius quantale, Girard quantale, associative algebra, star-autonomous category, nuclear object, adjoint}
}
Document
Translating Proofs from an Impredicative Type System to a Predicative One
Abstract
As the development of formal proofs is a time-consuming task, it is important to devise ways of sharing the already written proofs to prevent wasting time redoing them. One of the challenges in this domain is to translate proofs written in proof assistants based on impredicative logics, such as Coq, Matita and the HOL family, to proof assistants based on predicative logics like Agda, whenever impredicativity is not used in an essential way.
In this paper we present an algorithm to do such a translation between a core impredicative type system and a core predicative one allowing prenex universe polymorphism like in Agda. It consists in trying to turn a potentially impredicative term into a universe polymorphic term as general as possible. The use of universe polymorphism is justified by the fact that mapping an impredicative universe to a fixed predicative one is not sufficient in most cases.
During the algorithm, we need to solve unification problems modulo the max-successor algebra on universe levels. But, in this algebra, there are solvable problems having no most general solution. We however provide an incomplete algorithm whose solutions, when it succeeds, are most general ones.
The proposed translation is of course partial, but in practice allows one to translate many proofs that do not use impredicativity in an essential way. Indeed, it was implemented in the tool Predicativize and then used to translate semi-automatically many non-trivial developments from Matita’s arithmetic library to Agda, including Bertrand’s Postulate and Fermat’s Little Theorem, which were not available in Agda yet.
Cite as
Thiago Felicissimo, Frédéric Blanqui, and Ashish Kumar Barnawal. Translating Proofs from an Impredicative Type System to a Predicative One. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{felicissimo_et_al:LIPIcs.CSL.2023.19,
author = {Felicissimo, Thiago and Blanqui, Fr\'{e}d\'{e}ric and Barnawal, Ashish Kumar},
title = {{Translating Proofs from an Impredicative Type System to a Predicative One}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {19:1--19:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.19},
URN = {urn:nbn:de:0030-drops-174801},
doi = {10.4230/LIPIcs.CSL.2023.19},
annote = {Keywords: Type Theory, Impredicativity, Predicativity, Proof Translation, Universe Polymorphism, Unification Modulo Max, Agda, Dedukti}
}
Document
A Normalized Edit Distance on Infinite Words
Abstract
We introduce ω^ ̅-NED, an edit distance between infinite words, that is a natural extension of NED, the normalized edit distance between finite words. We show it is a metric on (equivalence classes of) infinite words. We provide a polynomial time algorithm to compute the distance between two ultimately periodic words, and a polynomial time algorithm to compute the distance between two regular ω-languages given by non-deterministic Büchi automata.
Cite as
Dana Fisman, Joshua Grogin, and Gera Weiss. A Normalized Edit Distance on Infinite Words. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{fisman_et_al:LIPIcs.CSL.2023.20,
author = {Fisman, Dana and Grogin, Joshua and Weiss, Gera},
title = {{A Normalized Edit Distance on Infinite Words}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {20:1--20:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.20},
URN = {urn:nbn:de:0030-drops-174818},
doi = {10.4230/LIPIcs.CSL.2023.20},
annote = {Keywords: Edit Distance, Infinite Words, Robustness}
}
Document
Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq
Abstract
We present a constructive analysis and machine-checked theory of one-one, many-one, and truth-table reductions based on synthetic computability theory in the Calculus of Inductive Constructions, the type theory underlying the proof assistant Coq. We give elegant, synthetic, and machine-checked proofs of Post’s landmark results that a simple predicate exists, is enumerable, undecidable, but many-one incomplete (Post’s problem for many-one reducibility), and a hypersimple predicate exists, is enumerable, undecidable, but truth-table incomplete (Post’s problem for truth-table reducibility).
In synthetic computability, one assumes axioms allowing to carry out computability theory with all definitions and proofs purely in terms of functions of the type theory with no mention of a model of computation. Proofs can focus on the essence of the argument, without having to sacrifice formality. Synthetic computability also clears the lense for constructivisation.
Our constructively careful definition of simple and hypersimple predicates allows us to not assume classical axioms, not even Markov’s principle, still yielding the expected strong results.
Cite as
Yannick Forster and Felix Jahn. Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{forster_et_al:LIPIcs.CSL.2023.21,
author = {Forster, Yannick and Jahn, Felix},
title = {{Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {21:1--21:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.21},
URN = {urn:nbn:de:0030-drops-174820},
doi = {10.4230/LIPIcs.CSL.2023.21},
annote = {Keywords: type theory, computability theory, constructive mathematics, Coq}
}
Document
Quantitative Hennessy-Milner Theorems via Notions of Density
Abstract
The classical Hennessy-Milner theorem is an important tool in the analysis of concurrent processes; it guarantees that any two non-bisimilar states in finitely branching labelled transition systems can be distinguished by a modal formula. Numerous variants of this theorem have since been established for a wide range of logics and system types, including quantitative versions where lower bounds on behavioural distance (e.g. in weighted, metric, or probabilistic transition systems) are witnessed by quantitative modal formulas. Both the qualitative and the quantitative versions have been accommodated within the framework of coalgebraic logic, with distances taking values in quantales, subject to certain restrictions, such as being so-called value quantales. While previous quantitative coalgebraic Hennessy-Milner theorems apply only to liftings of set functors to (pseudo)metric spaces, in the present work we provide a quantitative coalgebraic Hennessy-Milner theorem that applies more widely to functors native to metric spaces; notably, we thus cover, for the first time, the well-known Hennessy-Milner theorem for continuous probabilistic transition systems, where transitions are given by Borel measures on metric spaces, as an instance of such a general result. In the process, we also relax the restrictions imposed on the quantale, and additionally parametrize the technical account over notions of closure and, hence, density, providing associated variants of the Stone-Weierstraß theorem; this allows us to cover, for instance, behavioural ultrametrics.
Cite as
Jonas Forster, Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Quantitative Hennessy-Milner Theorems via Notions of Density. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{forster_et_al:LIPIcs.CSL.2023.22,
author = {Forster, Jonas and Goncharov, Sergey and Hofmann, Dirk and Nora, Pedro and Schr\"{o}der, Lutz and Wild, Paul},
title = {{Quantitative Hennessy-Milner Theorems via Notions of Density}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {22:1--22:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.22},
URN = {urn:nbn:de:0030-drops-174836},
doi = {10.4230/LIPIcs.CSL.2023.22},
annote = {Keywords: Behavioural distances, coalgebra, characteristic modal logics, density, Hennessy-Milner theorems, quantale-enriched categories, Stone-Weierstra{\ss} theorems}
}
Document
Order-Invariance in the Two-Variable Fragment of First-Order Logic
Abstract
We study the expressive power of the two-variable fragment of order-invariant first-order logic. This logic departs from first-order logic in two ways: first, formulas are only allowed to quantify over two variables. Second, formulas can use an additional binary relation, which is interpreted in the structures under scrutiny as a linear order, provided that the truth value of a sentence over a finite structure never depends on which linear order is chosen on its domain.
We prove that on classes of structures of bounded degree, any property expressible in this logic is definable in first-order logic. We then show that the situation remains the same when we add counting quantifiers to this logic.
Cite as
Julien Grange. Order-Invariance in the Two-Variable Fragment of First-Order Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{grange:LIPIcs.CSL.2023.23,
author = {Grange, Julien},
title = {{Order-Invariance in the Two-Variable Fragment of First-Order Logic}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {23:1--23:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.23},
URN = {urn:nbn:de:0030-drops-174846},
doi = {10.4230/LIPIcs.CSL.2023.23},
annote = {Keywords: Finite model theory, Two-variable logic, Order-invariance}
}
Document
Explorable Automata
Abstract
We define the class of explorable automata on finite or infinite words. This is a generalization of History-Deterministic (HD) automata, where this time non-deterministic choices can be resolved by building finitely many simultaneous runs instead of just one. We show that recognizing HD parity automata of fixed index among explorable ones is in PTime, thereby giving a strong link between the two notions. We then show that recognizing explorable automata is ExpTime-complete, in the case of finite words or Büchi automata. Additionally, we define the notion of ω-explorable automata on infinite words, where countably many runs can be used to resolve the non-deterministic choices. We show that all reachability automata are ω-explorable, but this is not the case for safety ones. We finally show ExpTime-completeness for ω-explorability of automata on infinite words for the safety and co-Büchi acceptance conditions.
Cite as
Emile Hazard and Denis Kuperberg. Explorable Automata. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{hazard_et_al:LIPIcs.CSL.2023.24,
author = {Hazard, Emile and Kuperberg, Denis},
title = {{Explorable Automata}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {24:1--24:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.24},
URN = {urn:nbn:de:0030-drops-174852},
doi = {10.4230/LIPIcs.CSL.2023.24},
annote = {Keywords: Nondeterminism, automata, complexity}
}
Document
The Expressive Power of CSP-Quantifiers
Abstract
A generalized quantifier Q_𝒦 is called a CSP-quantifier if its defining class 𝒦 consists of all structures that can be homomorphically mapped to a fixed finite template structure. For all positive integers n ≥ 2 and k, we define a pebble game that characterizes equivalence of structures with respect to the logic L^k_{∞ω}(CSP^+_n), where CSP^+_n is the union of the class Q₁ of all unary quantifiers and the class CSP_n of all CSP-quantifiers with template structures that have at most n elements. Using these games we prove that for every n ≥ 2 there exists a CSP-quantifier with template of size n+1 which is not definable in L^ω_{∞ω}(CSP^+_n). The proof of this result is based on a new variation of the well-known Cai-Fürer-Immerman construction.
Cite as
Lauri Hella. The Expressive Power of CSP-Quantifiers. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{hella:LIPIcs.CSL.2023.25,
author = {Hella, Lauri},
title = {{The Expressive Power of CSP-Quantifiers}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {25:1--25:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.25},
URN = {urn:nbn:de:0030-drops-174867},
doi = {10.4230/LIPIcs.CSL.2023.25},
annote = {Keywords: generalized quantifiers, constraint satisfaction problems, pebble games, finite variable logics, descriptive complexity theory}
}
Document
Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability
Abstract
We study the computational complexity of model checking and satisfiability problems of polyadic modal logics extended with permutations and Boolean operators on accessibility relations. First, we show that the combined complexity of the model checking problem for the resulting logic is PTime-complete. Secondly, we show that the satisfiability problem of polyadic modal logic extended with negation on accessibility relations is ExpTime-complete. Finally, we show that the satisfiability problem of polyadic modal logic with permutations and Boolean operators on accessibility relations is ExpTime-complete, under the assumption that both the number of accessibility relations that can be used and their arities are bounded by a constant. If NExpTime is not contained in ExpTime, then this assumption is necessary, since already the satisfiability problem of modal logic extended with Boolean operators on accessibility relations is NExpTime-hard.
Cite as
Reijo Jaakkola. Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{jaakkola:LIPIcs.CSL.2023.26,
author = {Jaakkola, Reijo},
title = {{Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {26:1--26:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.26},
URN = {urn:nbn:de:0030-drops-174875},
doi = {10.4230/LIPIcs.CSL.2023.26},
annote = {Keywords: Polyadic modal logics, Boolean modal logics, Model checking, Satisfiability}
}
Document
Complexity Classifications via Algebraic Logic
Abstract
Complexity and decidability of logics is an active research area involving a wide range of different logical systems. We introduce an algebraic approach to complexity classifications of computational logics. Our base system GRA, or general relation algebra, is equiexpressive with first-order logic FO. It resembles cylindric algebra but employs a finite signature with only seven different operators, thus also giving a very succinct characterization of the expressive capacities of first-order logic. We provide a comprehensive classification of the decidability and complexity of the systems obtained by limiting the allowed sets of operators of GRA. We also discuss variants and extensions of GRA, and we provide algebraic characterizations of a range of well-known decidable logics.
Cite as
Reijo Jaakkola and Antti Kuusisto. Complexity Classifications via Algebraic Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{jaakkola_et_al:LIPIcs.CSL.2023.27,
author = {Jaakkola, Reijo and Kuusisto, Antti},
title = {{Complexity Classifications via Algebraic Logic}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.27},
URN = {urn:nbn:de:0030-drops-174880},
doi = {10.4230/LIPIcs.CSL.2023.27},
annote = {Keywords: Decidability, complexity, algebraic logic, fragments of first-order logic}
}
Document
Counting and Matching
Abstract
Lists, multisets and partitions are fundamental datatypes in mathematics and computing. There are basic transformations from lists to multisets (called "accumulation") and also from lists to partitions (called "matching"). We show how these transformations arise systematically by forgetting/abstracting away certain aspects of information, namely order (transposition) and identity (substitution). Our main result is that suitable restrictions of these transformations are isomorphisms: This reveals fundamental correspondences between elementary datatypes. These restrictions involve "incremental" lists/multisets and "non-crossing" partitions/lists. While the process of forgetting information can be precisely spelled out in the language of category theory, the relevant constructions are very combinatorial in nature. The lists, partitions and multisets in these constructions are counted by Bell numbers and Catalan numbers. One side-product of our main result is a (terminating) rewriting system that turns an arbitrary partition into a non-crossing partition, without improper nestings.
Cite as
Bart Jacobs and Dario Stein. Counting and Matching. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{jacobs_et_al:LIPIcs.CSL.2023.28,
author = {Jacobs, Bart and Stein, Dario},
title = {{Counting and Matching}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {28:1--28:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.28},
URN = {urn:nbn:de:0030-drops-174892},
doi = {10.4230/LIPIcs.CSL.2023.28},
annote = {Keywords: List, Multiset, Partition, Crossing}
}
Document
Evaluation Trade-Offs for Acyclic Conjunctive Queries
Abstract
We consider the evaluation of acyclic conjunctive queries, where the evaluation time is decomposed into preprocessing time and enumeration delay. In a seminal paper at CSL'07, Bagan, Durand, and Grandjean showed that acyclic queries can be evaluated with linear preprocessing time and linear enumeration delay. If the query is free-connex, the enumeration delay becomes constant. Further prior work showed that constant enumeration delay can be achieved for arbitrary acyclic conjunctive queries at the expense of a preprocessing time that is characterised by the fractional hypertree width.
We introduce an approach that exposes a trade-off between preprocessing time and enumeration delay for acyclic conjunctive queries. The aforementioned prior works represent extremes in this trade-off space. Yet our approach also allows for the enumeration delay and the preprocessing time between these extremes, in particular the delay may lie between constant and linear time.
Our approach decomposes the given query into subqueries and achieves for each subquery a trade-off that depends on a parameter controlling the times for preprocessing and enumeration. The complexity of the query is given by the Pareto optimal points of a bi-objective optimisation program whose inputs are possible query decompositions and parameter values.
Cite as
Ahmet Kara, Milos Nikolic, Dan Olteanu, and Haozhe Zhang. Evaluation Trade-Offs for Acyclic Conjunctive Queries. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{kara_et_al:LIPIcs.CSL.2023.29,
author = {Kara, Ahmet and Nikolic, Milos and Olteanu, Dan and Zhang, Haozhe},
title = {{Evaluation Trade-Offs for Acyclic Conjunctive Queries}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {29:1--29:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.29},
URN = {urn:nbn:de:0030-drops-174907},
doi = {10.4230/LIPIcs.CSL.2023.29},
annote = {Keywords: acyclic queries, query evaluation, enumeration delay}
}
Document
Gödel’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability
Abstract
Gödel published his groundbreaking first incompleteness theorem in 1931, stating that a large class of formal logics admits independent sentences which are neither provable nor refutable. This result, in conjunction with his second incompleteness theorem, established the impossibility of concluding Hilbert’s program, which pursued a possible path towards a single formal system unifying all of mathematics. Using a technical trick to refine Gödel’s original proof, the incompleteness result was strengthened further by Rosser in 1936 regarding the conditions imposed on the formal systems.
Computability theory, which also originated in the 1930s, was quickly applied to formal logics by Turing, Kleene, and others to yield incompleteness results similar in strength to Gödel’s original theorem, but weaker than Rosser’s refinement. Only much later, Kleene found an improved but far less well-known proof based on computational notions, yielding a result as strong as Rosser’s.
In this expository paper, we work in constructive type theory to reformulate Kleene’s incompleteness results abstractly in the setting of synthetic computability theory and assuming a form of Church’s thesis, an axiom internalising the fact that all functions definable in such a setting are computable. Our novel, greatly condensed reformulation showcases the simplicity of the computational argument while staying formally entirely precise, a combination hard to achieve in typical textbook presentations. As an application, we instantiate the abstract result to first-order logic in order to derive essential incompleteness and, along the way, essential undecidability of Robinson arithmetic.
This paper is accompanied by a Coq mechanisation covering all our results and based on existing libraries of undecidability proofs and first-order logic, complementing the extensive work on mechanised incompleteness using the Gödel-Rosser approach. In contrast to the related mechanisations, our development follows Kleene’s ideas and utilises Church’s thesis for additional simplicity.
Cite as
Dominik Kirst and Benjamin Peters. Gödel’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{kirst_et_al:LIPIcs.CSL.2023.30,
author = {Kirst, Dominik and Peters, Benjamin},
title = {{G\"{o}del’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {30:1--30:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.30},
URN = {urn:nbn:de:0030-drops-174911},
doi = {10.4230/LIPIcs.CSL.2023.30},
annote = {Keywords: incompleteness, undecidability, synthetic computability theory}
}
Document
Finite Model Theory and Proof Complexity Revisited: Distinguishing Graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus
Abstract
This paper extends prior work on the connections between logics from finite model theory and propositional/algebraic proof systems. We show that if all non-isomorphic graphs in a given graph class can be distinguished in the logic Choiceless Polynomial Time with counting (CPT), then they can also be distinguished in the bounded-degree extended polynomial calculus (EPC), and the refutations have roughly the same size as the resource consumption of the CPT-sentence. This allows to transfer lower bounds for EPC to CPT and thus constitutes a new potential approach towards better understanding the limits of CPT. A super-polynomial EPC lower bound for a Ptime-instance of the graph isomorphism problem would separate CPT from Ptime and thus solve a major open question in finite model theory. Further, using our result, we provide a model theoretic proof for the separation of bounded-degree polynomial calculus and bounded-degree extended polynomial calculus.
Cite as
Benedikt Pago. Finite Model Theory and Proof Complexity Revisited: Distinguishing Graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{pago:LIPIcs.CSL.2023.31,
author = {Pago, Benedikt},
title = {{Finite Model Theory and Proof Complexity Revisited: Distinguishing Graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {31:1--31:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.31},
URN = {urn:nbn:de:0030-drops-174923},
doi = {10.4230/LIPIcs.CSL.2023.31},
annote = {Keywords: finite model theory, proof complexity, graph isomorphism}
}
Document
Adding Transitivity and Counting to the Fluted Fragment
Abstract
We study the impact of adding both counting quantifiers and a single transitive relation to the fluted fragment - a fragment of first-order logic originating in the work of W.V.O. Quine. The resulting formalism can be viewed as a multi-variable, non-guarded extension of certain systems of description logic featuring number restrictions and transitive roles, but lacking role-inverses. We establish the finite model property for our logic, and show that the satisfiability problem for its k-variable sub-fragment is in (k+1)-NExpTime. We also derive ExpSpace-hardness of the satisfiability problem for the two-variable, fluted fragment with one transitive relation (but without counting quantifiers), and prove that, when a second transitive relation is allowed, both the satisfiability and the finite satisfiability problems for the two-variable fluted fragment with counting quantifiers become undecidable.
Cite as
Ian Pratt-Hartmann and Lidia Tendera. Adding Transitivity and Counting to the Fluted Fragment. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{pratthartmann_et_al:LIPIcs.CSL.2023.32,
author = {Pratt-Hartmann, Ian and Tendera, Lidia},
title = {{Adding Transitivity and Counting to the Fluted Fragment}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {32:1--32:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.32},
URN = {urn:nbn:de:0030-drops-174933},
doi = {10.4230/LIPIcs.CSL.2023.32},
annote = {Keywords: fluted logic, transitivity, counting, satisfiability, decidability, complexity}
}
Document
Parity Games of Bounded Tree-Depth
Abstract
The exact complexity of solving parity games is a major open problem. Several authors have searched for efficient algorithms over specific classes of graphs. In particular, Obdržálek showed that for graphs of bounded tree-width or clique-width, the problem is in P, which was later improved by Ganardi, who showed that it is even in LOGCFL (with an additional assumption for clique-width case). Here we extend this line of research by showing that for graphs of bounded tree-depth the problem of solving parity games is in logspace uniform AC⁰. We achieve this by first considering a parameter that we obtain from a modification of clique-width, which we call shallow clique-width. We subsequently provide a suitable reduction.
Cite as
Konrad Staniszewski. Parity Games of Bounded Tree-Depth. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{staniszewski:LIPIcs.CSL.2023.33,
author = {Staniszewski, Konrad},
title = {{Parity Games of Bounded Tree-Depth}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {33:1--33:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.33},
URN = {urn:nbn:de:0030-drops-174942},
doi = {10.4230/LIPIcs.CSL.2023.33},
annote = {Keywords: Parity Games, Circuits, Tree-Depth, Clique-Width}
}
Document
Tower-Complete Problems in Contraction-Free Substructural Logics
Abstract
We investigate the non-elementary computational complexity of a family of substructural logics without contraction. With the aid of the technique pioneered by Lazić and Schmitz (2015), we show that the deducibility problem for full Lambek calculus with exchange and weakening (FL_{ew}) is not in Elementary (i.e., the class of decision problems that can be decided in time bounded by an elementary recursive function), but is in PR (i.e., the class of decision problems that can be decided in time bounded by a primitive recursive function). More precisely, we show that this problem is complete for Tower, which is a non-elementary complexity class forming a part of the fast-growing complexity hierarchy introduced by Schmitz (2016). The same complexity result holds even for deducibility in BCK-logic, i.e., the implicational fragment of FL_{ew}. We furthermore show the Tower-completeness of the provability problem for elementary affine logic, which was proved to be decidable by Dal Lago and Martini (2004).
Cite as
Hiromi Tanaka. Tower-Complete Problems in Contraction-Free Substructural Logics. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 34:1-34:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{tanaka:LIPIcs.CSL.2023.34,
author = {Tanaka, Hiromi},
title = {{Tower-Complete Problems in Contraction-Free Substructural Logics}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {34:1--34:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.34},
URN = {urn:nbn:de:0030-drops-174954},
doi = {10.4230/LIPIcs.CSL.2023.34},
annote = {Keywords: substructural logic, linear logic, full Lambek calculus, BCK-logic, computational complexity, provability, deducibility}
}
Document
Dynamic Complexity of Regular Languages: Big Changes, Small Work
Abstract
Whether a changing string is member of a certain regular language can be maintained in the DynFO framework of Patnaik and Immerman: after changing the symbol at one position of the string, a first-order update formula can express - using additionally stored information - whether the resulting string is in the regular language.
We extend this and further known results by considering changes of many positions at once. We also investigate to which degree the obtained update formulas imply work-efficient parallel dynamic algorithms.
Cite as
Felix Tschirbs, Nils Vortmeier, and Thomas Zeume. Dynamic Complexity of Regular Languages: Big Changes, Small Work. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{tschirbs_et_al:LIPIcs.CSL.2023.35,
author = {Tschirbs, Felix and Vortmeier, Nils and Zeume, Thomas},
title = {{Dynamic Complexity of Regular Languages: Big Changes, Small Work}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {35:1--35:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.35},
URN = {urn:nbn:de:0030-drops-174963},
doi = {10.4230/LIPIcs.CSL.2023.35},
annote = {Keywords: dynamic descriptive complexity, regular languages, batch changes, work}
}
Document
Completeness of Sum-Over-Paths for Toffoli-Hadamard and the Dyadic Fragments of Quantum Computation
Abstract
The "Sum-Over-Paths" formalism is a way to symbolically manipulate linear maps that describe quantum systems, and is a tool that is used in formal verification of such systems.
We give here a new set of rewrite rules for the formalism, and show that it is complete for "Toffoli-Hadamard", the simplest approximately universal fragment of quantum mechanics. We show that the rewriting is terminating, but not confluent (which is expected from the universality of the fragment). We do so using the connection between Sum-over-Paths and graphical language ZH-Calculus, and also show how the axiomatisation translates into the latter.
Finally, we show how to enrich the rewrite system to reach completeness for the dyadic fragments of quantum computation - obtained by adding phase gates with dyadic multiples of π to the Toffoli-Hadamard gate-set - used in particular in the Quantum Fourier Transform.
Cite as
Renaud Vilmart. Completeness of Sum-Over-Paths for Toffoli-Hadamard and the Dyadic Fragments of Quantum Computation. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{vilmart:LIPIcs.CSL.2023.36,
author = {Vilmart, Renaud},
title = {{Completeness of Sum-Over-Paths for Toffoli-Hadamard and the Dyadic Fragments of Quantum Computation}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {36:1--36:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.36},
URN = {urn:nbn:de:0030-drops-174974},
doi = {10.4230/LIPIcs.CSL.2023.36},
annote = {Keywords: Quantum Computation, Verification, Sum-Over-Paths, Rewrite Strategy, Toffoli-Hadamard, Completeness}
}
Document
String Diagrams for Non-Strict Monoidal Categories
Abstract
Whereas string diagrams for strict monoidal categories are well understood, and have found application in several fields of Computer Science, graphical formalisms for non-strict monoidal categories are far less studied. In this paper, we provide a presentation by generators and relations of string diagrams for non-strict monoidal categories, and show how this construction can handle applications in domains such as digital circuits and programming languages. We prove the correctness of our construction, which yields a novel proof of Mac Lane’s strictness theorem. This in turn leads to an elementary graphical proof of Mac Lane’s coherence theorem, and in particular allows for the inductive construction of the canonical isomorphisms in a monoidal category.
Cite as
Paul Wilson, Dan Ghica, and Fabio Zanasi. String Diagrams for Non-Strict Monoidal Categories. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{wilson_et_al:LIPIcs.CSL.2023.37,
author = {Wilson, Paul and Ghica, Dan and Zanasi, Fabio},
title = {{String Diagrams for Non-Strict Monoidal Categories}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {37:1--37:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.37},
URN = {urn:nbn:de:0030-drops-174981},
doi = {10.4230/LIPIcs.CSL.2023.37},
annote = {Keywords: String Diagrams, Strictness, Coherence}
}
Document
Supported Sets - A New Foundation for Nominal Sets and Automata
Abstract
The present work proposes and discusses the category of supported sets which provides a uniform foundation for nominal sets of various kinds, such as those for equality symmetry, for the order symmetry, and renaming sets. We show that all these differently flavoured categories of nominal sets are monadic over supported sets. Thus, supported sets provide a canonical finite way to represent nominal sets and the automata therein, e.g. register automata and coalgebras in general. Name binding in supported sets is modelled by a functor following the idea of de Bruijn indices. This functor lifts to the well-known abstraction functor in nominal sets. Together with the monadicity result, this gives rise to a transformation process from finite coalgebras in supported sets to orbit-finite coalgebras in nominal sets. One instance of this process transforms the finite representation of a register automaton in supported sets into its configuration automaton in nominal sets.
Cite as
Thorsten Wißmann. Supported Sets - A New Foundation for Nominal Sets and Automata. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 38:1-38:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
Copy BibTex To Clipboard
@InProceedings{wimann:LIPIcs.CSL.2023.38,
author = {Wi{\ss}mann, Thorsten},
title = {{Supported Sets - A New Foundation for Nominal Sets and Automata}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {38:1--38:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.38},
URN = {urn:nbn:de:0030-drops-174992},
doi = {10.4230/LIPIcs.CSL.2023.38},
annote = {Keywords: Nominal Sets, Monads, LFP-Category, Supported Sets, Coalgebra}
}