 |
 |
Volume 10, Issue 3
2014
1. Classical propositional logic and decidability of variables in intuitionistic propositional logic
We improve the answer to the question: what set of excluded middles for propositional variables in a formula suffices to prove the formula in intuitionistic propositional logic whenever it is provable in classical propositional logic.
2. Decidability Results for the Boundedness Problem
We prove decidability of the boundedness problem for monadic least fixed-point recursion based on positive monadic second-order (MSO) formulae over trees. Given an MSO-formula phi(X,x) that is positive in X, it is decidable whether the fixed-point recursion based on phi is spurious over the class of all trees in the sense that there is some uniform finite bound for the number of iterations phi takes to reach its least fixed point, uniformly across all trees. We also identify the exact complexity of this problem. The proof uses automata-theoretic techniques. This key result extends, by means of model-theoretic interpretations, to show decidability of the boundedness problem for MSO and guarded second-order logic (GSO) over the classes of structures of fixed finite tree-width. Further model-theoretic transfer arguments allow us to derive major known decidability results for boundedness for fragments of first-order logic as well as new ones.
3. A Fragment of Dependence Logic Capturing Polynomial Time
In this paper we study the expressive power of Horn-formulae in dependence logic and show that they can express NP-complete problems. Therefore we define an even smaller fragment D-Horn* and show that over finite successor structures it captures the complexity class P of all sets decidable in polynomial time. Furthermore we study the question which of our results can ge generalized to the case of open formulae of D-Horn* and so-called downwards monotone polynomial time properties of teams.
4. Automata theory in nominal sets
We study languages over infinite alphabets equipped with some structure that can be tested by recognizing automata. We develop a framework for studying such alphabets and the ensuing automata theory, where the key role is played by an automorphism group of the alphabet. In the process, we generalize nominal sets due to Gabbay and Pitts.
5. Reductions to the set of random strings: The resource-bounded case
This paper is motivated by a conjecture that BPP can be characterized in terms of polynomial-time nonadaptive reductions to the set of Kolmogorov-random strings. In this paper we show that an approach laid out in [Allender et al] to settle this conjecture cannot succeed without significant alteration, but that it does bear fruit if we consider time-bounded Kolmogorov complexity instead. We show that if a set A is reducible in polynomial time to the set of time-t-bounded Kolmogorov random strings (for all large enough time bounds t), then A is in P/poly, and that if in addition such a reduction exists for any universal Turing machine one uses in the definition of Kolmogorov complexity, then A is in PSPACE.
6. Finite state verifiers with constant randomness
We give a new characterization of $\mathsf{NL}$ as the class of languages whose members have certificates that can be verified with small error in polynomial time by finite state machines that use a constant number of random bits, as opposed to its conventional description in terms of deterministic logarithmic-space verifiers. It turns out that allowing two-way interaction with the prover does not change the class of verifiable languages, and that no polynomially bounded amount of randomness is useful for constant-memory computers when used as language recognizers, or public-coin verifiers. A corollary of our main result is that the class of outcome problems corresponding to O(log n)-space bounded games of incomplete information where the universal player is allowed a constant number of moves equals NL.
7. Representations of measurable sets in computable measure theory
This article is a fundamental study in computable measure theory. We use the framework of TTE, the representation approach, where computability on an abstract set X is defined by representing its elements with concrete "names", possibly countably infinite, over some alphabet {\Sigma}. As a basic computability structure we consider a computable measure on a computable $\sigma$-algebra. We introduce and compare w.r.t. reducibility several natural representations of measurable sets. They are admissible and generally form four different equivalence classes. We then compare our representations with those introduced by Y. Wu and D. Ding in 2005 and 2006 and claim that one of our representations is the most useful one for studying computability on measurable functions.
8. Deciding Conditional Termination
We address the problem of conditional termination, which is that of defining the set of initial configurations from which a given program always terminates. First we define the dual set, of initial configurations from which a non-terminating execution exists, as the greatest fixpoint of the function that maps a set of states into its pre-image with respect to the transition relation. This definition allows to compute the weakest non-termination precondition if at least one of the following holds: (i) the transition relation is deterministic, (ii) the descending Kleene sequence overapproximating the greatest fixpoint converges in finitely many steps, or (iii) the transition relation is well founded. We show that this is the case for two classes of relations, namely octagonal and finite monoid affine relations. Moreover, since the closed forms of these relations can be defined in Presburger arithmetic, we obtain the decidability of the termination problem for such loops.
9. On Ramsey properties of classes with forbidden trees
Let F be a set of relational trees and let Forbh(F) be the class of all structures that admit no homomorphism from any tree in F; all this happens over a fixed finite relational signature $\sigma$. There is a natural way to expand Forbh(F) by unary relations to an amalgamation class. This expanded class, enhanced with a linear ordering, has the Ramsey property.
10. A Concurrent Pattern Calculus
Concurrent pattern calculus (CPC) drives interaction between processes by comparing data structures, just as sequential pattern calculus drives computation. By generalising from pattern matching to pattern unification, interaction becomes symmetrical, with information flowing in both directions. CPC provides a natural language to express trade where information exchange is pivotal to interaction. The unification allows some patterns to be more discriminating than others; hence, the behavioural theory must take this aspect into account, so that bisimulation becomes subject to compatibility of patterns. Many popular process calculi can be encoded in CPC; this allows for a gain in expressiveness, formalised through encodings.
11. Refinement and Difference for Probabilistic Automata
This paper studies a difference operator for stochastic systems whose specifications are represented by Abstract Probabilistic Automata (APAs). In the case refinement fails between two specifications, the target of this operator is to produce a specification APA that represents all witness PAs of this failure. Our contribution is an algorithm that allows to approximate the difference of two APAs with arbitrary precision. Our technique relies on new quantitative notions of distances between APAs used to assess convergence of the approximations, as well as on an in-depth inspection of the refinement relation for APAs. The procedure is effective and not more complex to implement than refinement checking.
12. Ambiguity of {\omega}-Languages of Turing Machines
An {\omega}-language is a set of infinite words over a finite alphabet X. We consider the class of recursive {\omega}-languages, i.e. the class of {\omega}-languages accepted by Turing machines with a Büchi acceptance condition, which is also the class {\Sigma}11 of (effective) analytic subsets of X{\omega} for some finite alphabet X. We investigate here the notion of ambiguity for recursive {\omega}-languages with regard to acceptance by Büchi Turing machines. We first present in detail essentials on the literature on {\omega}-languages accepted by Turing Machines. Then we give a complete and broad view on the notion of ambiguity and unambiguity of Büchi Turing machines and of the {\omega}-languages they accept. To obtain our new results, we make use of results and methods of effective descriptive set theory.
13. Computable Jordan Decomposition of Linear Continuous Functionals on $C[0;1]$
By the Riesz representation theorem using the Riemann-Stieltjes integral, linear continuous functionals on the set of continuous functions from the unit interval into the reals can either be characterized by functions of bounded variation from the unit interval into the reals, or by signed measures on the Borel-subsets. Each of these objects has an (even minimal) Jordan decomposition into non-negative or non-decreasing objects. Using the representation approach to computable analysis, a computable version of the Riesz representation theorem has been proved by Jafarikhah, Lu and Weihrauch. In this article we extend this result. We study the computable relation between three Banach spaces, the space of linear continuous functionals with operator norm, the space of (normalized) functions of bounded variation with total variation norm, and the space of bounded signed Borel measures with variation norm. We introduce natural representations for defining computability. We prove that the canonical linear bijections between these spaces and their inverses are computable. We also prove that Jordan decomposition is computable on each of these spaces.
14. When is a container a comonad?
Abbott, Altenkirch, Ghani and others have taught us that many parameterized datatypes (set functors) can be usefully analyzed via container representations in terms of a set of shapes and a set of positions in each shape. This paper builds on the observation that datatypes often carry additional structure that containers alone do not account for. We introduce directed containers to capture the common situation where every position in a data-structure determines another data-structure, informally, the sub-data-structure rooted by that position. Some natural examples are non-empty lists and node-labelled trees, and data-structures with a designated position (zippers). While containers denote set functors via a fully-faithful functor, directed containers interpret fully-faithfully into comonads. But more is true: every comonad whose underlying functor is a container is represented by a directed container. In fact, directed containers are the same as containers that are comonads. We also describe some constructions of directed containers. We have formalized our development in the dependently typed programming language Agda.
15. Random strings and tt-degrees of Turing complete C.E. sets
We investigate the truth-table degrees of (co-)c.e.\ sets, in particular, sets of random strings. It is known that the set of random strings with respect to any universal prefix-free machine is Turing complete, but that truth-table completeness depends on the choice of universal machine. We show that for such sets of random strings, any finite set of their truth-table degrees do not meet to the degree~0, even within the c.e. truth-table degrees, but when taking the meet over all such truth-table degrees, the infinite meet is indeed~0. The latter result proves a conjecture of Allender, Friedman and Gasarch. We also show that there are two Turing complete c.e. sets whose truth-table degrees form a minimal pair.
16. Categorical Proof Theory of Co-Intuitionistic Linear Logic
To provide a categorical semantics for co-intuitionistic logic one has to face the fact, noted by Tristan Crolard, that the definition of co-exponents as adjuncts of coproducts does not work in the category Set, where coproducts are disjoint unions. Following the familiar construction of models of intuitionistic linear logic with exponential"!", we build models of co-intuitionistic logic in symmetric monoidal left-closed categories with additional structure, using a variant of Crolard's term assignment to co-intuitionistic logic in the construction of a free category.
17. Analysis of Timed and Long-Run Objectives for Markov Automata
Markov automata (MAs) extend labelled transition systems with random delays and probabilistic branching. Action-labelled transitions are instantaneous and yield a distribution over states, whereas timed transitions impose a random delay governed by an exponential distribution. MAs are thus a nondeterministic variation of continuous-time Markov chains. MAs are compositional and are used to provide a semantics for engineering frameworks such as (dynamic) fault trees, (generalised) stochastic Petri nets, and the Architecture Analysis & Design Language (AADL). This paper considers the quantitative analysis of MAs. We consider three objectives: expected time, long-run average, and timed (interval) reachability. Expected time objectives focus on determining the minimal (or maximal) expected time to reach a set of states. Long-run objectives determine the fraction of time to be in a set of states when considering an infinite time horizon. Timed reachability objectives are about computing the probability to reach a set of states within a given time interval. This paper presents the foundations and details of the algorithms and their correctness proofs. We report on several case studies conducted using a prototypical tool implementation of the algorithms, driven by the MAPA modelling language for efficiently generating MAs.
18. Observationally-induced algebras in Domain Theory
In this paper we revise and simplify the notion of observationally induced algebra introduced by Simpson and Schroeder for the purpose of modelling computational effects in the particular case where the ambient category is given by classical domain theory. As examples of the general framework we consider the various powerdomains. For the particular case of the Plotkin powerdomain the general recipe leads to a somewhat unexpected result which, however, makes sense from a Computer Science perspective. We analyze this "deviation" and show how to reobtain the original Plotkin powerdomain by imposing further conditions previously considered by R.~Heckmann and J.~Goubault-Larrecq.
19. Corecursive Algebras, Corecursive Monads and Bloom Monads
An algebra is called corecursive if from every coalgebra a unique coalgebra-to-algebra homomorphism exists into it. We prove that free corecursive algebras are obtained as coproducts of the terminal coalgebra (considered as an algebra) and free algebras. The monad of free corecursive algebras is proved to be the free corecursive monad, where the concept of corecursive monad is a generalization of Elgot's iterative monads, analogous to corecursive algebras generalizing completely iterative algebras. We also characterize the Eilenberg-Moore algebras for the free corecursive monad and call them Bloom algebras.
20. Fourier spectra of measures associated with algorithmically random Brownian motion
In this paper we study the behaviour at infinity of the Fourier transform of Radon measures supported by the images of fractal sets under an algorithmically random Brownian motion. We show that, under some computability conditions on these sets, the Fourier transform of the associated measures have, relative to the Hausdorff dimensions of these sets, optimal asymptotic decay at infinity. The argument relies heavily on a direct characterisation, due to Asarin and Pokrovskii, of algorithmically random Brownian motion in terms of the prefix free Kolmogorov complexity of finite binary sequences. The study also necessitates a closer look at the potential theory over fractals from a computable point of view.
21. Inferring Algebraic Effects
We present a complete polymorphic effect inference algorithm for an ML-style language with handlers of not only exceptions, but of any other algebraic effect such as input & output, mutable references and many others. Our main aim is to offer the programmer a useful insight into the effectful behaviour of programs. Handlers help here by cutting down possible effects and the resulting lengthy output that often plagues precise effect systems. Additionally, we present a set of methods that further simplify the displayed types, some even by deliberately hiding inferred information from the programmer.
22. Polynomial Interpretations over the Natural, Rational and Real Numbers Revisited
Polynomial interpretations are a useful technique for proving termination of term rewrite systems. They come in various flavors: polynomial interpretations with real, rational and integer coefficients. As to their relationship with respect to termination proving power, Lucas managed to prove in 2006 that there are rewrite systems that can be shown polynomially terminating by polynomial interpretations with real (algebraic) coefficients, but cannot be shown polynomially terminating using polynomials with rational coefficients only. He also proved the corresponding statement regarding the use of rational coefficients versus integer coefficients. In this article we extend these results, thereby giving the full picture of the relationship between the aforementioned variants of polynomial interpretations. In particular, we show that polynomial interpretations with real or rational coefficients do not subsume polynomial interpretations with integer coefficients. Our results hold also for incremental termination proofs with polynomial interpretations.
23. Improving legibility of natural deduction proofs is not trivial
In formal proof checking environments such as Mizar it is not merely the validity of mathematical formulas that is evaluated in the process of adoption to the body of accepted formalizations, but also the readability of the proofs that witness validity. As in case of computer programs, such proof scripts may sometimes be more and sometimes be less readable. To better understand the notion of readability of formal proofs, and to assess and improve their readability, we propose in this paper a method of improving proof readability based on Behaghel's First Law of sentence structure. Our method maximizes the number of local references to the directly preceding statement in a proof linearisation. It is shown that our optimization method is NP-complete.
24. On Separation by Locally Testable and Locally Threshold Testable Languages
A separator for two languages is a third language containing the first one and disjoint from the second one. We investigate the following decision problem: given two regular input languages, decide whether there exists a locally testable (resp. a locally threshold testable) separator. In both cases, we design a decision procedure based on the occurrence of special patterns in automata accepting the input languages. We prove that the problem is computationally harder than deciding membership. The correctness proof of the algorithm yields a stronger result, namely a description of a possible separator. Finally, we discuss the same problem for context-free input languages.
25. Constructing categories and setoids of setoids in type theory
In this paper we consider the problem of building rich categories of setoids, in standard intensional Martin-Löf type theory (MLTT), and in particular how to handle the problem of equality on objects in this context. Any (proof-irrelevant) family F of setoids over a setoid A gives rise to a category C(A, F) of setoids with objects A. We may regard the family F as a setoid of setoids, and a crucial issue in this article is to construct rich or large enough such families. Depending on closure conditions of F, the category C(A, F) has corresponding categorical constructions. We exemplify this with finite limits. A very large family F may be obtained from Aczel's model construction of CZF in type theory. It is proved that the category so obtained is isomorphic to the internal category of sets in this model. Set theory can thus establish (categorical) properties of C(A, F) which may be used in type theory. We also show that Aczel's model construction may be extended to include the elements of any setoid as atoms or urelements. As a byproduct we obtain a natural extension of CZF, adding atoms. This extension, CZFU, is validated by the extended model. The main theorems of the paper have been checked in the proof assistant Coq which is based on MLTT. A possible application of this development is to integrate set-theoretic and type-theoretic reasoning in proof assistants.