eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
0
0
10.4230/LIPIcs.CSL.2013
article
LIPIcs, Volume 23, CSL'13, Complete Volume
Ronchi Della Rocca, Simona
LIPIcs, Volume 23, CSL'13, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013/LIPIcs.CSL.2013.pdf
Conference Proceedings, Theory of Computation, Distributed Systems, Software/ Programs Verifications, Formal Definitions and Theory Languages Constructs and Features, Knowledge Representations Formalisms and Methods
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
i
xiv
10.4230/LIPIcs.CSL.2013.i
article
Frontmatter, Table of Contents, Preface, Conference Organization
Ronchi Della Rocca, Simona
Frontmatter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.i/LIPIcs.CSL.2013.i.pdf
Frontmatter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
1
4
10.4230/LIPIcs.CSL.2013.1
article
The Ackermann Award 2013
Dawar, Anuj
Henzinger, Thomas A.
Niwiński, Damian
Report on the Ackermann Award 2013.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.1/LIPIcs.CSL.2013.1.pdf
Ackermann award
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
5
10
10.4230/LIPIcs.CSL.2013.5
article
Res Publica: The Universal Model of Computation (Invited Talk)
Dershowitz, Nachum
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.5/LIPIcs.CSL.2013.5.pdf
Models of computation
cellular automata
abstract state machines
causal dynamics
interaction
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
11
23
10.4230/LIPIcs.CSL.2013.11
article
Three lightings of logic (Invited Talk)
Girard, Jean-Yves
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?"
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.11/LIPIcs.CSL.2013.11.pdf
Proof theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
24
27
10.4230/LIPIcs.CSL.2013.24
article
From determinism, non-determinism and alternation to recursion schemes for P, NP and Pspace (Invited Talk)
Oitavem, Isabel
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.24/LIPIcs.CSL.2013.24.pdf
Computational complexity
Recursion schemes
P
NP
Pspace
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
28
29
10.4230/LIPIcs.CSL.2013.28
article
Means and Limits of Decision (Invited Talk)
Tendera, Lidia
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.28/LIPIcs.CSL.2013.28.pdf
classical decision problem
decidability
computational complexity
two-variable first-order logic
guarded logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
30
44
10.4230/LIPIcs.CSL.2013.30
article
On closure ordinals for the modal mu-calculus
Afshari, Bahareh
Leigh, Graham E.
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.30/LIPIcs.CSL.2013.30.pdf
Closure ordinals
Modal mu-calculus
Tableaux
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
45
60
10.4230/LIPIcs.CSL.2013.45
article
Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1
Aschieri, Federico
Berardi, Stefano
Birolo, Giovanni
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.45/LIPIcs.CSL.2013.45.pdf
Interactive realizability
classical Arithmetic
witness extraction
delimited exceptions
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
61
80
10.4230/LIPIcs.CSL.2013.61
article
Bounds for the quantifier depth in finite-variable logics: Alternation hierarchy
Berkholz, Christoph
Krebs, Andreas
Verbitsky, Oleg
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).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.61/LIPIcs.CSL.2013.61.pdf
Alternation hierarchy
finite-variable logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
81
100
10.4230/LIPIcs.CSL.2013.81
article
Unambiguity and uniformization problems on infinite trees
Bilkowski, Marcin
Skrzypczak, Michał
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.81/LIPIcs.CSL.2013.81.pdf
nondeterministic automata
infinite trees
MSO logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
101
115
10.4230/LIPIcs.CSL.2013.101
article
A characterization of the Taylor expansion of lambda-terms
Boudes, Pierre
He, Fanny
Pagani, Michele
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.101/LIPIcs.CSL.2013.101.pdf
Lambda-Calculus
Böhm trees
Differential Lambda-Calculus
Linear Logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
116
128
10.4230/LIPIcs.CSL.2013.116
article
Team building in dependence
Bradfield, Julian
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.116/LIPIcs.CSL.2013.116.pdf
partially ordered quantification
independence-friendly logic
game semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
129
148
10.4230/LIPIcs.CSL.2013.129
article
Saturation-Based Model Checking of Higher-Order Recursion Schemes
Broadbent, Christopher
Kobayashi, Naoki
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.129/LIPIcs.CSL.2013.129.pdf
Model checking
higher-order recursion schemes
intersection types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
149
164
10.4230/LIPIcs.CSL.2013.149
article
Descriptive complexity of approximate counting CSPs
Bulatov, Andrei
Dalmau, Victor
Thurley, Marc
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.149/LIPIcs.CSL.2013.149.pdf
Constraint Satisfaction Problems
Approximate Counting
Descriptive Complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
165
180
10.4230/LIPIcs.CSL.2013.165
article
What is Decidable about Partially Observable Markov Decision Processes with omega-Regular Objectives
Chatterjee, Krishnendu
Chmelik, Martin
Tracol, Mathieu
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.165/LIPIcs.CSL.2013.165.pdf
POMDPs
Omega-regular objectives
Parity objectives
Qualitative analysis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
181
196
10.4230/LIPIcs.CSL.2013.181
article
Infinite-state games with finitary conditions
Chatterjee, Krishnendu
Fijalkow, Nathanaël
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.181/LIPIcs.CSL.2013.181.pdf
Two-player games
Infinite-state systems
Pushdown games
Bounds in omega-regularity
Synthesis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
197
214
10.4230/LIPIcs.CSL.2013.197
article
Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic
Clouston, Ranald
Dawson, Jeremy
Goré, Rajeev
Tiu, Alwen
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.197/LIPIcs.CSL.2013.197.pdf
Linear logic
display calculus
nested sequent calculus
deep inference
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
215
230
10.4230/LIPIcs.CSL.2013.215
article
Deciding the weak definability of Büchi definable tree languages
Colcombet, Thomas
Kuperberg, Denis
Löding, Christof
Vanden Boom, Michael
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.215/LIPIcs.CSL.2013.215.pdf
Tree automata
weak definability
decidability
cost automata
boundedness
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
231
247
10.4230/LIPIcs.CSL.2013.231
article
Innocent Game Semantics via Intersection Type Assignment Systems
Di Gianantonio, Pietro
Lenisa, Marina
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.231/LIPIcs.CSL.2013.231.pdf
Game Semantics
Intersection Type Assignment System
Lambda Calculus
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
248
262
10.4230/LIPIcs.CSL.2013.248
article
Cuts for circular proofs: semantics and cut-elimination
Fortier, Jérôme
Santocanale, Luigi
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.248/LIPIcs.CSL.2013.248.pdf
categorical proof-theory
fixpoints
initial and final (co)algebras
inductive and coinductive types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
263
280
10.4230/LIPIcs.CSL.2013.263
article
Hierarchies in independence logic
Galliani, Pietro
Hannula, Miika
Kontinen, Juha
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.263/LIPIcs.CSL.2013.263.pdf
Existential second-order logic
Independence logic
Inclusion logic
Expressiveness hierarchies
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
281
295
10.4230/LIPIcs.CSL.2013.281
article
Inclusion Logic and Fixed Point Logic
Galliani, Pietro
Hella, Lauri
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.281/LIPIcs.CSL.2013.281.pdf
Dependence Logic
Team Semantics
Fixpoint Logic
Inclusion
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
296
315
10.4230/LIPIcs.CSL.2013.296
article
Theories for Subexponential-size Bounded-depth Frege Proofs
Ghasemloo, Kaveh
Cook, Stephen A.
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.296/LIPIcs.CSL.2013.296.pdf
Computational Complexity Theory
Proof Complexity
Bounded Arithmetic
NC1-Frege
AC0- Frege
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
316
331
10.4230/LIPIcs.CSL.2013.316
article
The Structure of Interaction
Gimenez, Stéphane
Moser, Georg
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.316/LIPIcs.CSL.2013.316.pdf
Interaction Nets
Linear Logic
Curry–Howard Correspondence
Deep Inference
Calculus of Structures
Strong Normalisation
Reducibility
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
332
347
10.4230/LIPIcs.CSL.2013.332
article
The Fixed-Parameter Tractability of Model Checking Concurrent Systems
Göller, Stefan
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.332/LIPIcs.CSL.2013.332.pdf
Model Checking
Concurrent Systems
Parameterized Complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
348
362
10.4230/LIPIcs.CSL.2013.348
article
One-variable first-order linear temporal logics with counting
Hampson, Christopher
Kurucz, Agi
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.348/LIPIcs.CSL.2013.348.pdf
modal and temporal logic
counting
decision procedures
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
363
379
10.4230/LIPIcs.CSL.2013.363
article
On the locality of arb-invariant first-order logic with modulo counting quantifiers
Harwath, Frederik
Schweikardt, Nicole
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.363/LIPIcs.CSL.2013.363.pdf
finite model theory
Gaifman and Hanf locality
first-order logic with modulo counting quantifiers
order-invariant and arb-invariant formulas
lower
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
380
394
10.4230/LIPIcs.CSL.2013.380
article
When is Metric Temporal Logic Expressively Complete?
Hunter, Paul
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).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.380/LIPIcs.CSL.2013.380.pdf
Metric Temporal Logic
Expressive power
First-order logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
395
414
10.4230/LIPIcs.CSL.2013.395
article
Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus
Kikuchi, Kentaro
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.395/LIPIcs.CSL.2013.395.pdf
Strong normalisation
Klop's extended lambda-calculus
Explicit substitution
Cut-elimination
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
415
431
10.4230/LIPIcs.CSL.2013.415
article
Kleene Algebra with Products and Iteration Theories
Kozen, Dexter
Mamouras, Konstantinos
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.415/LIPIcs.CSL.2013.415.pdf
Kleene algebra
typed Kleene algebra
iteration theories
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
432
451
10.4230/LIPIcs.CSL.2013.432
article
Internalizing Relational Parametricity in the Extensional Calculus of Constructions
Krishnaswami, Neelakantan R.
Dreyer, Derek
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.432/LIPIcs.CSL.2013.432.pdf
Relational parametricity
dependent types
quasi-PERs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
452
468
10.4230/LIPIcs.CSL.2013.452
article
Modal Logic and Distributed Message Passing Automata
Kuusisto, Antti
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.452/LIPIcs.CSL.2013.452.pdf
Modal logic
message passing automata
descriptive characterizations
distributed computing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
469
483
10.4230/LIPIcs.CSL.2013.469
article
Global semantic typing for inductive and coinductive computing
Leivant, Daniel
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.469/LIPIcs.CSL.2013.469.pdf
Inductive and coinductive types
equational programs
intrinsic theories
global model theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
484
499
10.4230/LIPIcs.CSL.2013.484
article
Two-Variable Logic on 2-Dimensional Structures
Manuel, Amaldev
Zeume, Thomas
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.484/LIPIcs.CSL.2013.484.pdf
FO2
Data words
Satisfiability
Decidability
Automata
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
500
520
10.4230/LIPIcs.CSL.2013.500
article
Categorical Duality Theory: With Applications to Domains, Convexity, and the Distribution Monad
Maruyama, Yoshihiro
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.500/LIPIcs.CSL.2013.500.pdf
duality
monad
categorical topology
domain theory
convex structure
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
521
539
10.4230/LIPIcs.CSL.2013.521
article
Axiomatizing Subtyped Delimited Continuations
Materzok, Marek
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.521/LIPIcs.CSL.2013.521.pdf
Delimited Continuations
Continuation Passing Style
Axiomatization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
540
562
10.4230/LIPIcs.CSL.2013.540
article
On dialogue games and coherent strategies
Melliès, Paul-André
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.540/LIPIcs.CSL.2013.540.pdf
Game semantics
Stable order
Extensional order
Bistructures
Tensorial logic
Innocent strategies
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
563
577
10.4230/LIPIcs.CSL.2013.563
article
Elementary Modal Logics over Transitive Structures
Michaliszyn, Jakub
Otop, Jan
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.563/LIPIcs.CSL.2013.563.pdf
Modal logic
Transitive frames
Elementary modal logics
Decidability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
578
596
10.4230/LIPIcs.CSL.2013.578
article
A Fully Abstract Game Semantics for Parallelism with Non-Blocking Synchronization on Shared Variables
Nishimura, Susumu
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.578/LIPIcs.CSL.2013.578.pdf
shared variable parallelism
non-blocking synchronization
full abstraction
game semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
597
614
10.4230/LIPIcs.CSL.2013.597
article
Extracting Herbrand trees in classical realizability using forcing
Rieg, Lionel
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.597/LIPIcs.CSL.2013.597.pdf
classical realizability
forcing
Curry-Howard correspondence
Herbrand trees
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
615
633
10.4230/LIPIcs.CSL.2013.615
article
The Complexity of Abduction for Equality Constraint Languages
Schmidt, Johannes
Wrona, Michał
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.615/LIPIcs.CSL.2013.615.pdf
Abduction
infinite structures
equality constraint languages
computational complexity
algebraic approach
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
634
652
10.4230/LIPIcs.CSL.2013.634
article
A New Type Assignment for Strongly Normalizable Terms
Statman, Rick
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.634/LIPIcs.CSL.2013.634.pdf
lambda calculus
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
23
653
667
10.4230/LIPIcs.CSL.2013.653
article
Semantics of Intensional Type Theory extended with Decidable Equational Theories
Wang, Qian
Barras, Bruno
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.653/LIPIcs.CSL.2013.653.pdf
Calculus of Constructions
Extensional Type Theory
Intensional Type Theory
Model
Meta-theory
Consistency
Strong Normalization
Presburger Arithme