Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy
CSL 2013
September 2-5, 2013
Torino, Italy
Computer Science Logic
CSL
http://www.eacsl.org/conferences.html
https://dblp.org/db/conf/csl
Leibniz International Proceedings in Informatics
LIPIcs
https://www.dagstuhl.de/dagpub/1868-8969
https://dblp.org/db/series/lipics
1868-8969
Simona
Ronchi Della Rocca
Simona Ronchi Della Rocca
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
23
2013
978-3-939897-60-6
https://www.dagstuhl.de/dagpub/978-3-939897-60-6
Frontmatter, Table of Contents, Preface, Conference Organization
Frontmatter, Table of Contents, Preface, Conference Organization
Frontmatter
Table of Contents
Preface
Conference Organization
i-xiv
Front Matter
Simona
Ronchi Della Rocca
Simona Ronchi Della Rocca
10.4230/LIPIcs.CSL.2013.i
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
The Ackermann Award 2013
Report on the Ackermann Award 2013.
Ackermann award
1-4
Regular Paper
Anuj
Dawar
Anuj Dawar
Thomas A.
Henzinger
Thomas A. Henzinger
Damian
Niwiński
Damian Niwiński
10.4230/LIPIcs.CSL.2013.1
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Res Publica: The Universal Model of Computation (Invited Talk)
We proffer a model of computation that encompasses a broad variety of contemporary generic models, such as cellular automata---including dynamic ones, and abstract state machines---incorporating, as they do, interaction and parallelism. We ponder what it means for such an intertwined system to be effective and note that the suggested framework is ideal for representing continuous-time and asynchronous systems.
Models of computation
cellular automata
abstract state machines
causal dynamics
interaction
5-10
Invited Talk
Nachum
Dershowitz
Nachum Dershowitz
10.4230/LIPIcs.CSL.2013.5
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Three lightings of logic (Invited Talk)
Whether we deal with foundations or computation, logic relates questions and answers, typically formulas and proofs: a very entangled relation due to the abuse of presuppositions.
In order to analyse syntax, we should step out from language, which is quite impossible. However, it is enough to step out from meaning: this is why our first lighting of logic is that of answers: it is possible to deal with them as meaningless artifacts assuming two basic states, implicit and explicit. The process of explicitation (a.k.a. normalisation, execution), which aims at making explicit what is only implicit, is fundamentally hazardous.
The second light is that of questions whose choice involves a formatting ensuring the convergence of explicitation, i.e., the existence of "normal forms". This formatting can be seen as the emergence of meaning. It is indeed a necessary nuisance; either too laxist or too coercitive, there is no just format. Logic should avoid the pitfall of Prussian, axiomatic, formats by trying to understand which deontic dialogue is hidden behind logical restrictions.
The third lighting, certainty deals with the adequation between answers and questions: how do we know that an answer actually matches a question? Apodictic certainty -- beyond a reasonable doubt -- is out of reach: we can only hope for epidictic, i.e., limited, reasonable, certainty. Under the second light (questions), we see that the format is made of two opposite parts, namely rights and duties, and that logical deduction relies on a strict balance between these two opposite terms, expressed by the identity group "A is A and conversely". The issue of certainty thus becomes the interrogation: "Can we afford the rights of our duties?"
Proof theory
11-23
Invited Talk
Jean-Yves
Girard
Jean-Yves Girard
10.4230/LIPIcs.CSL.2013.11
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
From determinism, non-determinism and alternation to recursion schemes for P, NP and Pspace (Invited Talk)
Our goal is to approach the classes of computational complexity P, NP, and Pspace in a recursion-theoretic manner. Here we emphasize the connection between the structure of the recursion schemes and the underlying models of computation.
Computational complexity
Recursion schemes
P
NP
Pspace
24-27
Invited Talk
Isabel
Oitavem
Isabel Oitavem
10.4230/LIPIcs.CSL.2013.24
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Means and Limits of Decision (Invited Talk)
In this talk we survey recent work in the quest for expressive logics with good algorithmic properties, starting from the two-variable fragment of first-order logic and the guarded fragment. While tracing the boundary between decidable and undecidable fragments we describe their power, limitations, similarities and differences in order to stress out key properties responsible for their good or bad behaviour. We also highlight tools and techniques that have proven most effective for designing optimal algorithms, special attention giving to the more universal ones.
classical decision problem
decidability
computational complexity
two-variable first-order logic
guarded logic
28-29
Invited Talk
Lidia
Tendera
Lidia Tendera
10.4230/LIPIcs.CSL.2013.28
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
On closure ordinals for the modal mu-calculus
The closure ordinal of a formula of modal mu-calculus mu X phi is the least ordinal kappa, if it exists, such that the denotation of the formula and the kappa-th iteration of the monotone operator induced by phi coincide across all transition systems (finite and infinite). It is known that for every alpha < omega^2 there is a formula phi of modal logic such that mu X phi has closure ordinal alpha (Czarnecki 2010). We prove that the closure ordinals arising from the alternation-free fragment of modal mu-calculus (the syntactic class capturing Sigma_2 \cap Pi_2) are bounded by omega^2. In this logic satisfaction can be characterised in terms of the existence of tableaux, trees generated by systematically breaking down formulae into their constituents according to the semantics of the calculus. To obtain optimal upper bounds we utilise the connection between closure ordinals of formulae and embedded order-types of the corresponding tableaux.
Closure ordinals
Modal mu-calculus
Tableaux
30-44
Regular Paper
Bahareh
Afshari
Bahareh Afshari
Graham E.
Leigh
Graham E. Leigh
10.4230/LIPIcs.CSL.2013.30
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1
We present a new Curry-Howard correspondence for HA + EM_1, constructive Heyting Arithmetic with the excluded middle on \Sigma^0_1-formulas. We add to the lambda calculus an operator ||_a which represents, from the viewpoint of programming, an exception operator with a delimited scope, and from the viewpoint of logic, a restricted version of the excluded middle. We motivate the restriction of the excluded middle by its use in proof mining; we introduce new techniques to prove strong normalization for HA + EM_1 and the witness property for simply existential statements. One may consider our results as an application of the ideas of Interactive realizability, which we have adapted to the new setting and used to prove our main theorems.
Interactive realizability
classical Arithmetic
witness extraction
delimited exceptions
45-60
Regular Paper
Federico
Aschieri
Federico Aschieri
Stefano
Berardi
Stefano Berardi
Giovanni
Birolo
Giovanni Birolo
10.4230/LIPIcs.CSL.2013.45
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy
Given two structures G and H distinguishable in FO^k (first-order logic with k variables), let A^k(G,H) denote the minimum alternation depth of a FO^k formula distinguishing G from H. Let A^k(n) be the maximum value of A^k(G,H) over n-element structures. We prove the strictness of the quantifier alternation hierarchy of FO^2 in a strong quantitative form, namely A^2(n) >= n/8-2, which is tight up to a constant factor. For each k >= 2, it holds that A^k(n) > log_(k+1) n-2 even over colored trees, which is also tight up to a constant factor if k >= 3. For k >= 3 the last lower bound holds also over uncolored trees, while the alternation hierarchy of FO^2 collapses even over all uncolored graphs.
We also show examples of colored graphs G and H on n vertices that can be distinguished in FO^2 much more succinctly if the alternation number is increased just by one: while in Sigma_i it is possible to distinguish G from H with bounded quantifier depth, in Pi_i this requires quantifier depth Omega(n2). The quadratic lower bound is best possible here because, if G and H can be distinguished in FO^k with i quantifier alternations, this can be done with quantifier depth n^(2k-2).
Alternation hierarchy
finite-variable logic
61-80
Regular Paper
Christoph
Berkholz
Christoph Berkholz
Andreas
Krebs
Andreas Krebs
Oleg
Verbitsky
Oleg Verbitsky
10.4230/LIPIcs.CSL.2013.61
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Unambiguity and uniformization problems on infinite trees
A nondeterministic automaton is called unambiguous if it has at most one accepting run on every input. A regular language is called unambiguous if there exists an unambiguous automaton recognizing this language. Currently, the class of unambiguous languages of infinite trees is not well-understood. In particular, there is no known decision procedure verifying if a given regular tree language is unambiguous. In this work we study the self-dual class of bi-unambiguous languages - languages that are unambiguous and their complement is also unambiguous. It turns out that thin trees (trees with only countably many branches) emerge naturally in this context.
We propose a procedure P designed to decide if a given tree automaton recognizes a bi-unambiguous language. The procedure is sound for every input. It is also complete for languages recognisable by deterministic automata. We conjecture that P is complete for all inputs but this depends on a new conjecture stating that there is no MSO-definable choice function on thin trees. This would extend a result by Gurevich and Shelah on the undefinability of choice on the binary tree.
We provide a couple of equivalent statements to our conjecture, we also give several related results about uniformizability on thin trees. In particular, we provide a new example of a language that is not unambiguous, namely the language of all thin trees. The main tool in our studies are algebras that can be seen as an adaptation of Wilke algebras to the case of infinite trees.
nondeterministic automata
infinite trees
MSO logic
81-100
Regular Paper
Marcin
Bilkowski
Marcin Bilkowski
Michał
Skrzypczak
Michał Skrzypczak
10.4230/LIPIcs.CSL.2013.81
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
A characterization of the Taylor expansion of lambda-terms
The Taylor expansion of lambda-terms, as introduced by Ehrhard and Regnier, expresses a lambda-term as a series of multi-linear terms, called simple terms, which capture bounded computations. Normal forms of Taylor expansions give a notion of infinitary normal forms, refining the notion of Böhm trees in a quantitative setting.
We give the algebraic conditions over a set of normal simple terms which characterize the property of being the normal form of the Taylor expansion of a lambda-term. From this full completeness result, we give further conditions which semantically describe normalizable and total lambda-terms.
Lambda-Calculus
Böhm trees
Differential Lambda-Calculus
Linear Logic
101-115
Regular Paper
Pierre
Boudes
Pierre Boudes
Fanny
He
Fanny He
Michele
Pagani
Michele Pagani
10.4230/LIPIcs.CSL.2013.101
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Team building in dependence
Hintikka and Sandu's Independence-Friendly Logic was introduced as a logic for partially ordered quantification, in which the independence of (existential) quantifiers from previous (universal) quantifiers is written by explicit syntax. It was originally given a semantics by games of imperfect information; Hodges then gave a (necessarily) second-order Tarskian semantics. More recently, Väänänen (2007) has proposed that the many curious features of IF logic can be better understood in his Dependence Logic, in which the (in)dependence of variables is stated in atomic formula, rather than by changing the definition of quantifier; he gives semantics in Tarskian form, via imperfect information games, and via a routine second-order perfect information game. He then defines Team Logic, where classical negation is added to the mix, resulting in a full second-order expressive logic. He remarks that no game semantics appears possible (other than by playing at second order). In this article, we explore an alternative approach to game semantics for DL, where we avoid imperfect information, yet stay locally apparently first-order, by sweeping the second-order information into longer games (infinite games in the case of countable models). Extending the game to Team Logic is not possible in standard games, but we conjecture a move to transfinite games may achieve a 'natural' game for Team Logic.
partially ordered quantification
independence-friendly logic
game semantics
116-128
Regular Paper
Julian
Bradfield
Julian Bradfield
10.4230/LIPIcs.CSL.2013.116
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Saturation-Based Model Checking of Higher-Order Recursion Schemes
Model checking of higher-order recursion schemes (HORS) has recently been studied extensively and applied to higher-order program verification. Despite recent efforts, obtaining a scalable model checker for HORS remains a big challenge. We propose a new model checking algorithm for HORS, which combines two previous, independent approaches to higher-order model checking. Like previous type-based algorithms for HORS, it directly analyzes HORS and outputs intersection types as a certificate, but like Broadbent et al.'s saturation algorithm for collapsible pushdown systems (CPDS), it propagates information backward, in the sense that it starts with target configurations and iteratively computes their pre-images. We have implemented the new algorithm and confirmed that the prototype often outperforms TRECS and CSHORe, the state-of-the-art model checkers for HORS.
Model checking
higher-order recursion schemes
intersection types
129-148
Regular Paper
Christopher
Broadbent
Christopher Broadbent
Naoki
Kobayashi
Naoki Kobayashi
10.4230/LIPIcs.CSL.2013.129
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Descriptive complexity of approximate counting CSPs
Motivated by Fagin's characterization of NP, Saluja et al. have introduced a logic based frame- work for expressing counting problems. In this setting, a counting problem (seen as a mapping C from structures to non-negative integers) is `defined’ by a first-order sentence phi if for every instance A of the problem, the number of possible satisfying assignments of the variables of phi in A is equal to C(A). The logic RHPI_1 has been introduced by Dyer et al. in their study of the counting complexity class #BIS. The interest in the class #BIS stems from the fact that, it is quite plausible that the problems in #BIS are not #P-hard, nor they admit a fully polynomial randomized approximation scheme. In the present paper we investigate which counting constraint satisfaction problems #CSP(H) are definable in the monotone fragment of RHPI_1. We prove that #CSP(H) is definable in monotone RHPI_1 whenever H is invariant under meet and join operations of a distributive lattice. We prove that the converse also holds if H contains the equality relation. We also prove similar results for counting CSPs expressible by linear Datalog. The results in this case are very similar to those for monotone RHPI1, with the addition that H has, additionally, \top (the greatest element of the lattice) as a polymorphism.
Constraint Satisfaction Problems
Approximate Counting
Descriptive Complexity
149-164
Regular Paper
Andrei
Bulatov
Andrei Bulatov
Victor
Dalmau
Victor Dalmau
Marc
Thurley
Marc Thurley
10.4230/LIPIcs.CSL.2013.149
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives
We consider partially observable Markov decision processes (POMDPs) with omega-regular conditions specified as parity objectives. The qualitative analysis problem given a POMDP and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are known to be undecidable even for very special cases of parity objectives, we establish decidability (with optimal EXPTIME-complete complexity) of the qualitative analysis problems for POMDPs with all parity objectives under finite-memory strategies. We also establish optimal (exponential) memory bounds.
POMDPs
Omega-regular objectives
Parity objectives
Qualitative analysis
165-180
Regular Paper
Krishnendu
Chatterjee
Krishnendu Chatterjee
Martin
Chmelik
Martin Chmelik
Mathieu
Tracol
Mathieu Tracol
10.4230/LIPIcs.CSL.2013.165
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Infinite-state games with finitary conditions
We study two-player zero-sum games over infinite-state graphs equipped with omega-B and finitary conditions.
Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games.
We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with omega-B-conditions, implying the decidability of solving these games. Second we consider pushdown games with finitary parity along with stack boundedness conditions, and show that solving these games is EXPTIME-complete.
Two-player games
Infinite-state systems
Pushdown games
Bounds in omega-regularity
Synthesis
181-196
Regular Paper
Krishnendu
Chatterjee
Krishnendu Chatterjee
Nathanaël
Fijalkow
Nathanaël Fijalkow
10.4230/LIPIcs.CSL.2013.181
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic
Full Intuitionistic Linear Logic (FILL) is multiplicative intuitionistic linear logic extended with par. Its proof theory has been notoriously difficult to get right, and existing sequent calculi all involve inference rules with complex annotations to guarantee soundness and cut-elimination. We give a simple and annotation-free display calculus for FILL which satisfies Belnap’s generic cut-elimination theorem. To do so, our display calculus actually handles an extension of FILL, called Bi-Intuitionistic Linear Logic (BiILL), with an ‘exclusion’ connective defined via an adjunction with par. We refine our display calculus for BiILL into a cut-free nested sequent calculus with deep inference in which the explicit structural rules of the display calculus become admissible. A separation property guarantees that proofs of FILL formulae in the deep inference calculus contain no trace of exclusion. Each such rule is sound for the semantics of FILL, thus our deep inference calculus and display calculus are conservative over FILL. The deep inference calculus also enjoys the subformula property and terminating backward proof search, which gives the NP-completeness of BiILL and FILL.
Linear logic
display calculus
nested sequent calculus
deep inference
197-214
Regular Paper
Ranald
Clouston
Ranald Clouston
Jeremy
Dawson
Jeremy Dawson
Rajeev
Goré
Rajeev Goré
Alwen
Tiu
Alwen Tiu
10.4230/LIPIcs.CSL.2013.197
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Deciding the weak definability of Büchi definable tree languages
Weakly definable languages of infinite trees are an expressive subclass of regular tree languages definable in terms of weak monadic second-order logic, or equivalently weak alternating automata. Our main result is that given a Büchi automaton, it is decidable whether the language is weakly definable. We also show that given a parity automaton, it is decidable whether the language is recognizable by a nondeterministic co-Büchi automaton.
The decidability proofs build on recent results about cost automata over infinite trees. These automata use counters to define functions from infinite trees to the natural numbers extended with infinity. We reduce to testing whether the functions defined by certain "quasi-weak" cost automata are bounded by a finite value.
Tree automata
weak definability
decidability
cost automata
boundedness
215-230
Regular Paper
Thomas
Colcombet
Thomas Colcombet
Denis
Kuperberg
Denis Kuperberg
Christof
Löding
Christof Löding
Michael
Vanden Boom
Michael Vanden Boom
10.4230/LIPIcs.CSL.2013.215
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Innocent Game Semantics via Intersection Type Assignment Systems
The aim of this work is to correlate two different approaches to the semantics of programming languages: game semantics and intersection type assignment systems (ITAS). Namely, we present an ITAS that provides the description of the semantic interpretation of a typed lambda calculus in a game model based on innocent strategies. Compared to the traditional ITAS used to describe the semantic interpretation in domain theoretic models, the ITAS presented in this paper has two main differences: the introduction of a notion of labelling on moves, and the omission of several rules, i.e. the subtyping rules and some structural rules.
Game Semantics
Intersection Type Assignment System
Lambda Calculus
231-247
Regular Paper
Pietro
Di Gianantonio
Pietro Di Gianantonio
Marina
Lenisa
Marina Lenisa
10.4230/LIPIcs.CSL.2013.231
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Cuts for circular proofs: semantics and cut-elimination
One of the authors introduced in [Santocanale, FoSSaCS, 2002] a calculus of circular proofs for studying the computability arising from the following categorical operations: finite products, finite coproducts, initial algebras, final coalgebras. The calculus presented [Santocanale, FoSSaCS, 2002] is cut-free; even if sound and complete for provability, it lacked an important property for the semantics of proofs, namely fullness w.r.t. the class of intended categorical models (called mu-bicomplete categories in [Santocanale, ITA, 2002]).
In this paper we fix this problem by adding the cut rule to the calculus and by modifying accordingly the syntactical constraint ensuring soundness of proofs. The enhanced proof system fully represents arrows of the canonical model (a free mu-bicomplete category). We also describe a cut-elimination procedure as a a model of computation arising from the above mentioned categorical operations. The procedure constructs a cut-free proof-tree with possibly infinite branches out of a finite circular proof with cuts.
categorical proof-theory
fixpoints
initial and final (co)algebras
inductive and coinductive types
248-262
Regular Paper
Jérôme
Fortier
Jérôme Fortier
Luigi
Santocanale
Luigi Santocanale
10.4230/LIPIcs.CSL.2013.248
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Hierarchies in independence logic
We study the expressive power of fragments of inclusion and independence logic defined either by restricting the number of universal quantifiers or the arity of inclusion and independence atoms in formulas. Assuming the so-called lax semantics for these logics, we relate these fragments of inclusion and independence logic to familiar sublogics of existential second-order logic. We also show that, with respect to the stronger strict semantics, inclusion logic is equivalent to existential second-order logic.
Existential second-order logic
Independence logic
Inclusion logic
Expressiveness hierarchies
263-280
Regular Paper
Pietro
Galliani
Pietro Galliani
Miika
Hannula
Miika Hannula
Juha
Kontinen
Juha Kontinen
10.4230/LIPIcs.CSL.2013.263
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Inclusion Logic and Fixed Point Logic
We investigate the properties of Inclusion Logic, that is, First Order Logic with Team Semantics extended with inclusion dependencies. We prove that Inclusion Logic is equivalent to Greatest Fixed Point Logic, and we prove that all union-closed first-order definable properties of relations are definable in it. We also provide an Ehrenfeucht-Fraïssé game for Inclusion Logic, and give an example illustrating its use.
Dependence Logic
Team Semantics
Fixpoint Logic
Inclusion
281-295
Regular Paper
Pietro
Galliani
Pietro Galliani
Lauri
Hella
Lauri Hella
10.4230/LIPIcs.CSL.2013.281
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Theories for Subexponential-size Bounded-depth Frege Proofs
This paper is a contribution to our understanding of the relationship between uniform and nonuniform proof complexity. The latter studies the lengths of proofs in various propositional proof systems such as Frege and bounded-depth Frege systems, and the former studies the strength of the corresponding logical theories such as VNC1 and V0 in [Cook/Nguyen, 2010]. A superpolynomial lower bound on the length of proofs in a propositional proof system for a family of tautologies expressing a result like the pigeonhole principle implies that the result is not provable in the theory associated with the propositional proof system.
We define a new class of bounded arithmetic theories n^epsilon-ioV^\infinity for epsilon < 1 and show that they correspond to complexity classes AltTime(O(1),O(n^epsilon)), uniform classes of subexponential-size bounded-depth circuits DepthSize(O(1),2^O(n^epsilon)). To accomplish this we introduce the novel idea of using types to control the amount of composition in our bounded arithmetic theories. This allows our theories to capture complexity classes that have weaker closure properties and are not closed under composition. We show that the proofs of Sigma^B_0-theorems in our theories translate to subexponential-size bounded-depth Frege proofs.
We use these theories to formalize the complexity theory result that problems in uniform NC1 circuits can be computed by uniform subexponential bounded-depth circuits in [Allender/Koucky, 2010]. We prove that our theories contain a variation of the theory VNC1 for the complexity class NC1. We formalize Buss's proof in [Buss, 1993] that the (unbalanced) Boolean Formula Evaluation problem is in NC1 and use it to prove the soundness of Frege systems. As a corollary, we obtain an alternative proof of [Filmus et al, ICALP, 2011] that polynomial-size Frege proofs can be simulated by subexponential-size bounded-depth Frege proofs.
Our results can be extended to theories corresponding to other nice complexity classes inside NTimeSpace(n^O(1), n^o(1)) such as NL. This is achieved by essentially formalizing the containment
NTimeSpace(n^O(1), n^o(1)) \subseteq AltTime(O(1), O(n^epsilon))
for all epsilon > 0.
Computational Complexity Theory
Proof Complexity
Bounded Arithmetic
NC1-Frege
AC0- Frege
296-315
Regular Paper
Kaveh
Ghasemloo
Kaveh Ghasemloo
Stephen A.
Cook
Stephen A. Cook
10.4230/LIPIcs.CSL.2013.296
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
The Structure of Interaction
Interaction nets form a local and strongly confluent model of computation that is per se parallel. We introduce a Curry–Howard correspondence between well-formed interaction nets and a deep-inference deduction system based on linear logic. In particular, linear logic itself is easily expressed in the system and its computational aspects materialise though the correspondence. The system of interaction nets obtained is a typed variant of already well-known sharing graphs. Due to a strong confluence property, strong normalisation for this system follows from weak normalisation. The latter is obtained via an adaptation of Girard's reducibility method. The approach is modular, readily gives rise to generalisations (e.g. second order, known as polymorphism to the programmer) and could therefore be extended to various systems of interaction nets.
Interaction Nets
Linear Logic
Curry–Howard Correspondence
Deep Inference
Calculus of Structures
Strong Normalisation
Reducibility
316-331
Regular Paper
Stéphane
Gimenez
Stéphane Gimenez
Georg
Moser
Georg Moser
10.4230/LIPIcs.CSL.2013.316
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
The Fixed-Parameter Tractability of Model Checking Concurrent Systems
We study the fixed-parameter complexity of model checking temporal logics on concurrent systems that are modeled as the product of finite systems and where the size of the formula is the parameter. We distinguish between asynchronous product and synchronous product. Sometimes it is possible to show that there is an algorithm for this with running time (\sum_i T_i|)O(1) * f(|\phi|), where the T_i are the component systems and \phi is the formula and f is computable function, thus model checking is fixed-parameter tractable when the size of the formula is the parameter.
In this paper we concern ourselves with the question, provided fixed-parameter tractability is known, whether it holds for an elementary function f. Negative answers to this question are provided for modal logic and EF logic: Depending on the mode of synchronization we show the non-existence of such an elementary function f under different assumptions from (parameterized) complexity theory.
Model Checking
Concurrent Systems
Parameterized Complexity
332-347
Regular Paper
Stefan
Göller
Stefan Göller
10.4230/LIPIcs.CSL.2013.332
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
One-variable first-order linear temporal logics with counting
First-order temporal logics are notorious for their bad computational behaviour. It is known that even the two-variable monadic fragment is highly undecidable over various timelines. However, following the introduction of the monodic formulas (where temporal operators can be applied only to subformulas with at most one free variable), there has been a renewed interest in understanding extensions of the one-variable fragment and identifying those that are decidable. Here we analyse the one-variable fragment of temporal logic extended with counting (to two), interpreted in models with constant, decreasing, and expanding first-order domains. We show that over most classes of linear orders these logics are (sometimes highly) undecidable, even without constant and function symbols, and with the sole temporal operator 'eventually'. A more general result says that the bimodal logic of commuting linear and pseudo-equivalence relations is undecidable. The proofs are by reductions of various counter machine problems.
modal and temporal logic
counting
decision procedures
348-362
Regular Paper
Christopher
Hampson
Christopher Hampson
Agi
Kurucz
Agi Kurucz
10.4230/LIPIcs.CSL.2013.348
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
On the locality of arb-invariant first-order logic with modulo counting quantifiers
We study Gaifman and Hanf locality of an extension of first-order logic with modulo p counting quantifiers (FO+MODp, for short) with arbitrary numerical predicates. We require that the validity of formulas is independent of the particular interpretation of the numerical predicates and refer to such formulas as arb-invariant formulas. This paper gives a detailed picture of locality and non-locality properties of arb-invariant FO+MODp. For example, on the class of all finite structures, for any p >= 2, arb-invariant FO+MODp is neither Hanf nor Gaifman local with respect to a sublinear locality radius. However, in case that p is an odd prime power, it is weakly Gaifman local with a polylogarithmic locality radius. And when restricting attention to the class of string structures, for odd prime powers p, arb-invariant FO+MODp is both Hanf and Gaifman local with a polylogarithmic locality radius. Our negative results build on examples of order-invariant FO+MODp formulas presented in Niemistö's PhD thesis. Our positive results make use of the close connection between FO+MODp and Boolean circuits built from NOT-gates and AND-, OR-, and MODp-gates of arbitrary fan-in.
finite model theory
Gaifman and Hanf locality
first-order logic with modulo counting quantifiers
order-invariant and arb-invariant formulas
lower
363-379
Regular Paper
Frederik
Harwath
Frederik Harwath
Nicole
Schweikardt
Nicole Schweikardt
10.4230/LIPIcs.CSL.2013.363
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
When is Metric Temporal Logic Expressively Complete?
A seminal result of Kamp is that over the reals Linear Temporal Logic (LTL) has the same expressive power as first-order logic with binary order relation < and monadic predicates. A key question is whether there exists an analogue of Kamp's theorem for Metric Temporal Logic (MTL) - a generalization of LTL in which the Until and Since modalities are annotated with intervals that express metric constraints. Hirshfeld and Rabinovich gave a negative answer, showing that first-order logic with binary order relation < and unary function +1 is strictly more expressive than MTL with integer constants. However, a recent result of Hunter, Ouaknine and Worrell shows that when rational timing constants are added to both languages, MTL has the same expressive power as first-order logic, giving a positive answer. In this paper we generalize these results by giving a precise characterization of those sets of constants for which MTL and first-order logic have the same expressive power. We also show that full first-order expressiveness can be recovered with the addition of counting modalities, strongly supporting the assertion of Hirshfeld and Rabinovich that Q2MLO is one of the most expressive decidable fragments of FO(<,+1).
Metric Temporal Logic
Expressive power
First-order logic
380-394
Regular Paper
Paul
Hunter
Paul Hunter
10.4230/LIPIcs.CSL.2013.380
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus
In this paper we present strong normalisation proofs using a technique of non-deterministic translations into Klop's extended lambda-calculus. We first illustrate the technique by showing strong normalisation of a typed calculus that corresponds to natural deduction with general elimination rules. Then we study its explicit substitution version, the type-free calculus of which does not satisfy PSN with respect to reduction of the original calculus; nevertheless it is shown that typed terms are strongly normalising with respect to reduction of the explicit substitution calculus. In the same framework we prove strong normalisation of Sørensen and Urzyczyn's cut-elimination system in intuitionistic sequent calculus.
Strong normalisation
Klop's extended lambda-calculus
Explicit substitution
Cut-elimination
395-414
Regular Paper
Kentaro
Kikuchi
Kentaro Kikuchi
10.4230/LIPIcs.CSL.2013.395
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Kleene Algebra with Products and Iteration Theories
We develop a typed equational system that subsumes both iteration theories and typed Kleene algebra in a common framework. Our approach is based on cartesian categories endowed with commutative strong monads to handle nondeterminism.
Kleene algebra
typed Kleene algebra
iteration theories
415-431
Regular Paper
Dexter
Kozen
Dexter Kozen
Konstantinos
Mamouras
Konstantinos Mamouras
10.4230/LIPIcs.CSL.2013.415
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Internalizing Relational Parametricity in the Extensional Calculus of Constructions
We give the first relationally parametric model of the extensional calculus of constructions. Our model remains as simple as traditional PER models of types, but unlike them, it additionally permits the relating of terms that implement abstract types in different ways. Using our model, we can validate the soundness of quotient types, as well as derive strong equality axioms for Church-encoded data, such as the usual induction principles for Church naturals and booleans, and the eta law for strong dependent pair types. Furthermore, we show that such equivalences, justified by relationally parametric reasoning, may soundly be internalized (i.e., added as equality axioms to our type theory). Thus, we demonstrate that it is possible to interpret equality in a dependently-typed setting using parametricity. The key idea behind our approach is to interpret types as so-called quasi-PERs (or zigzag-complete relations), which enable us to model the symmetry and transitivity of equality while at the same time allowing abstract types with different representations to be equated.
Relational parametricity
dependent types
quasi-PERs
432-451
Regular Paper
Neelakantan R.
Krishnaswami
Neelakantan R. Krishnaswami
Derek
Dreyer
Derek Dreyer
10.4230/LIPIcs.CSL.2013.432
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Modal Logic and Distributed Message Passing Automata
In a recent article, Lauri Hella and co-authors identify a canonical connection between modal logic and deterministic distributed constant-time algorithms. The paper reports a variety of highly natural logical characterizations of classes of distributed message passing automata that run in constant time. The article leaves open the question of identifying related logical characterizations when the constant running time limitation is lifted. We obtain such a characterization for a class of finite message passing automata in terms of a recursive bisimulation invariant logic which we call modal substitution calculus (MSC). We also give a logical characterization of the related class A of infinite message passing automata by showing that classes of labelled directed graphs recognizable by automata in A are exactly the classes co-definable by a modal theory. A class C is co-definable by a modal theory if the complement of C is definable by a possibly infinite set of modal formulae. We also briefly discuss expressivity and decidability issues concerning MSC. We establish that MSC contains the Sigma^\mu_1 fragment of the modal \mu-calculus in the finite. We also observe that the single variable fragment MSC^1 of MSC is not contained in MSO, and that the SAT and FINSAT problems of MSC^1 are complete for PSPACE.
Modal logic
message passing automata
descriptive characterizations
distributed computing
452-468
Regular Paper
Antti
Kuusisto
Antti Kuusisto
10.4230/LIPIcs.CSL.2013.452
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Global semantic typing for inductive and coinductive computing
Common data-types, such as N, can be identified with term algebras. Thus each type can be construed as a global set; e.g. for N this global set is instantiated in each structure S to the denotations in S of the unary numerals. We can then consider each declarative program as an axiomatic theory, and assigns to it a semantic (Curry-style) type in each structure. This leads to the intrinsic theories of [Leivant, 2002], which provide a purely logical framework for reasoning about programs and their types. The framework is of interest because of its close fit with syntactic, semantic, and proof theoretic fundamentals of formal logic.
This paper extends the framework to data given by coinductive as well as inductive declarations. We prove a Canonicity Theorem, stating that the denotational semantics of an equational program P, understood operationally, has type \tau over the canonical model iff P, understood as a formula has type \tau in every "data-correct" structure. In addition we show that every intrinsic theory is interpretable in a conservative extension of first-order arithmetic.
Inductive and coinductive types
equational programs
intrinsic theories
global model theory
469-483
Regular Paper
Daniel
Leivant
Daniel Leivant
10.4230/LIPIcs.CSL.2013.469
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Two-Variable Logic on 2-Dimensional Structures
This paper continues the study of the two-variable fragment of first-order logic (FO^2) over two- dimensional structures, more precisely structures with two orders, their induced successor relations and arbitrarily many unary relations. Our main focus is on ordered data words which are finite sequences from the set \Sigma x D where \Sigma is a finite alphabet and D is an ordered domain. These are naturally represented as labelled finite sets with a linear order <=_l and a total preorder <=_p.
We introduce ordered data automata, an automaton model for ordered data words. An ordered data automaton is a composition of a finite state transducer and a finite state automaton over the product Boolean algebra of finite and cofinite subsets of N. We show that ordered data automata are equivalent to the closure of FO^2(+1_l,<=_p,+1_p) under existential quantification of unary relations. Using this automaton model we prove that the finite satisfiability problem for this logic is decidable on structures where the <=_p-equivalence classes are of bounded size. As a corollary, we obtain that finite satisfiability of FO^2 is decidable (and it is equivalent to the reachability problem of vector addition systems) on structures with two linear order successors and a linear order corresponding to one of the successors. Further we prove undecidability of FO^2 on several other two-dimensional structures.
FO2
Data words
Satisfiability
Decidability
Automata
484-499
Regular Paper
Amaldev
Manuel
Amaldev Manuel
Thomas
Zeume
Thomas Zeume
10.4230/LIPIcs.CSL.2013.484
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Categorical Duality Theory: With Applications to Domains, Convexity, and the Distribution Monad
Utilising and expanding concepts from categorical topology and algebra, we contrive a moderately general theory of dualities between algebraic, point-free spaces and set-theoretical, point-set spaces, which encompasses infinitary Stone dualities, such as the well-known duality between frames (aka. locales) and topological spaces, and a duality between \sigma-complete Boolean algebras and measurable spaces, as well as the classic finitary Stone, Gelfand, and Pontryagin dualities. Among different applications of our theory, we focus upon domain-convexity duality in particular: from the theory we derive a duality between Scott's continuous lattices and convexity spaces, and exploit the resulting insights to identify intrinsically the dual equivalence part of a dual adjunction for algebras of the distribution monad; the dual adjunction was uncovered by Bart Jacobs, but with no characterisation of the induced equivalence, which we do give here. In the Appendix, we place categorical duality in a wider context, and elucidate philosophical underpinnings of duality.
duality
monad
categorical topology
domain theory
convex structure
500-520
Regular Paper
Yoshihiro
Maruyama
Yoshihiro Maruyama
10.4230/LIPIcs.CSL.2013.500
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Axiomatizing Subtyped Delimited Continuations
We present direct equational axiomatizations of the call-by-value lambda calculus with the control operators shift_0 and reset_0 that generalize Danvy and Filinski's shift and reset in that they allow for abstracting control beyond the top-most delimited continuation. We address an untyped version of the calculus as well as a typed version with effect subtyping. For each of the calculi we present a set of axioms that we prove sound and complete with respect to the corresponding CPS translation.
Delimited Continuations
Continuation Passing Style
Axiomatization
521-539
Regular Paper
Marek
Materzok
Marek Materzok
10.4230/LIPIcs.CSL.2013.521
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
On dialogue games and coherent strategies
We explain how to see the set of positions of a dialogue game as a coherence space in the sense of Girard or as a bistructure in the sense of Curien, Plotkin and Winskel. The coherence structure on the set of positions results from a Kripke translation of tensorial logic into linear logic extended with a necessity modality. The translation is done in such a way that every innocent strategy defines a clique or a configuration in the resulting space of positions. This leads us to study the notion of configuration designed by Curien, Plotkin and Winskel for general bistructures in the particular case of a bistructure associated to a dialogue game. We show that every such configuration may be seen as an interactive strategy equipped with a backward as well as a forward dynamics based on the interplay between the stable order and the extensional order. In that way, the category of bistructures is shown to include a full subcategory of games and coherent strategies of an interesting nature.
Game semantics
Stable order
Extensional order
Bistructures
Tensorial logic
Innocent strategies
540-562
Regular Paper
Paul-André
Melliès
Paul-André Melliès
10.4230/LIPIcs.CSL.2013.540
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Elementary Modal Logics over Transitive Structures
We show that modal logic over universally first-order definable classes of transitive frames is decidable. More precisely, let K be an arbitrary class of transitive Kripke frames definable by a universal first-order sentence. We show that the global and finite global satisfiability problems of modal logic over K are decidable in NP, regardless of choice of K. We also show that the local satisfiability and the finite local satisfiability problems of modal logic over K are decidable in NExpTime.
Modal logic
Transitive frames
Elementary modal logics
Decidability
563-577
Regular Paper
Jakub
Michaliszyn
Jakub Michaliszyn
Jan
Otop
Jan Otop
10.4230/LIPIcs.CSL.2013.563
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
A Fully Abstract Game Semantics for Parallelism with Non-Blocking Synchronization on Shared Variables
We present a fully abstract game semantics for an Algol-like parallel language with non-blocking synchronization primitive. Elaborating on Harmer's game model for nondeterminism, we develop a game framework appropriate for modeling parallelism. The game is a sophistication of the wait-notify game proposed in a previous work, which makes the signals for thread scheduling explicit with a certain set of extra moves. The extra moves induce a Kleisli category of games, on which we develop a game semantics of the Algol-like parallel language and establish the full abstraction result with a significant use of the non-blocking synchronization operation.
shared variable parallelism
non-blocking synchronization
full abstraction
game semantics
578-596
Regular Paper
Susumu
Nishimura
Susumu Nishimura
10.4230/LIPIcs.CSL.2013.578
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Extracting Herbrand trees in classical realizability using forcing
Krivine presented in [Krivine, 2011] a methodology to combine Cohen's forcing with the theory of classical realizability and showed that the forcing condition can be seen as a reference that is not subject to backtracks. The underlying classical program transformation was then analyzed by Miquel [Miquel, 2011] in a fully typed setting in classical higher-order arithmetic (PA-omega^+).
As a case study of this methodology, we present a method to extract a Herbrand tree from a classical realizer of inconsistency, following the ideas underlying the completeness theorem and the proof of Herbrand's theorem. Unlike the traditional proof based on König's lemma (using a fixed enumeration of atomic formulas), our method is based on the introduction of a particular Cohen real. It is formalized as a proof in PA-omega^+, making explicit the construction of generic sets in this framework in the particular case where the set of forcing conditions is arithmetical. We then analyze the algorithmic content of this proof.
classical realizability
forcing
Curry-Howard correspondence
Herbrand trees
597-614
Regular Paper
Lionel
Rieg
Lionel Rieg
10.4230/LIPIcs.CSL.2013.597
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
The Complexity of Abduction for Equality Constraint Languages
Abduction is a form of nonmonotonic reasoning that looks for an explanation for an observed manifestation according to some knowledge base. One form of the abduction problem studied in the literature is the propositional abduction problem parameterized by a structure \Gamma over the two-element domain. In that case, the knowledge base is a set of constraints over \Gamma, the manifestation and explanation are propositional formulas.
In this paper, we follow a similar route. Yet, we consider abduction over infinite domain. We study the equality abduction problem parameterized by a relational first-order structure \Gamma over the natural numbers such that every relation in \Gamma is definable by a Boolean combination of equalities, a manifestation is a literal of the form (x = y) or (x != y), and an explanation is a set of such literals. Our main contribution is a complete complexity characterization of the equality abduction problem. We prove that depending on \Gamma, it is \Sigma^P_2-complete, or NP-complete, or in P.
Abduction
infinite structures
equality constraint languages
computational complexity
algebraic approach
615-633
Regular Paper
Johannes
Schmidt
Johannes Schmidt
Michał
Wrona
Michał Wrona
10.4230/LIPIcs.CSL.2013.615
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
A New Type Assignment for Strongly Normalizable Terms
We consider an operator definable in the intuitionistic theory of monadic predicates and we axiomatize some of its properties in a definitional extension of that monadic logic. The axiomatization lends itself to a natural deduction formulation to which the Curry-Howard isomorphism can be applied. The resulting Church style type system has the property that an untyped term is typable if and only if it is strongly normalizable.
lambda calculus
634-652
Regular Paper
Rick
Statman
Rick Statman
10.4230/LIPIcs.CSL.2013.634
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Semantics of Intensional Type Theory extended with Decidable Equational Theories
Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions (CC) provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality generally leads to undecidable type-checking, it seems a reasonable trade-off to extend intensional equality with a decidable first-order theory, as experimented in earlier work on CoqMTU and its implementation CoqMT.
In this work, CoqMTU is extended with strong eliminations. The meta-theoretical study, particularly the part relying on semantic arguments, is more complex. A set-theoretical model of the equational theory is the key ingredient to derive the logical consistency of the formalism. Strong normalization, the main lemma from which type-decidability follows, is proved by attaching realizability information to the values of the model.
The approach we have followed is to first consider an abstract notion of first-order equational theory, and then instantiate it with a particular instance, Presburger Arithmetic. These results have been formalized using Coq.
Calculus of Constructions
Extensional Type Theory
Intensional Type Theory
Model
Meta-theory
Consistency
Strong Normalization
Presburger Arithme
653-667
Regular Paper
Qian
Wang
Qian Wang
Bruno
Barras
Bruno Barras
10.4230/LIPIcs.CSL.2013.653
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode