CSL 2013 --- TORINO

Abstract: Computer science considers infinity a fiction, but the usual entities of classical geometry all consist of infinitely many points. to resolve the tension, modern mathematics has developed finite versions of euclidean and non-euclidean geometries, which should be of interest to the computer scientist. [Close]

Abstract: 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 to boot. [Close]

Abstract: Three main axes, three lightings of logic: 1. What is an answer? Here, the main divide is between implicit and explicit, a program before and after execution. The two don’t match, this is the lesson of undecidability. However, an hazardous process of normalisation can be devised. This process takes place in an analytic space, a sort of type-free, logic-free computational universe. 2. What is a question? Here, the main divide is between formatted and informal. The informal, untyped, approach yields strictly no guarantee as to the convergence of normalisation. The formatted approach decides which questions can/cannot be asked; as we know from incompleteness, this necessary formatting, always too repressive, is a necessary nuisance. The formatting can be explained by means of a deontic dialogue occurring in the same analytic space. 3. What conveys certainty? The typing is supposed to guarantee explicitation, at the expense of freedom. But how do we actually know that the typing actually achieves what it is supposed to achieve? Although this fundamental doubt about reasoning cannot be dismissed, it is of interest to determine which form of limited, epidictic, certainty (in contrast to absolute, apodictic, certainty) we can achieve, and how such a limited achievement possible at all! [Close]

Abstract: P, NP and Pspace are well-known classes of computational complexity that can be described following different approaches. Here we describe them in a machine inde- pendent manner, using recursion schemes, which turn the known inclusions P ⊆ NP ⊆ Pspace obvious. This work contributes to a better understanding of the involved classes, but no separation result is foreseen. Recursion-theoretic approaches lead to classes of functions instead of predicates (or boolean functions). Therefore, instead of P and Pspace we reach the classes FPtime and FPspace. As a class of functions corresponding to NP we choose FPtime ∪ NP, and we adopt the notation FNP. Our strategy is, as always in recursion-theoretic contexts, to start with a set of initial functions — which should be basic from the complexity point of view — and to close it under composition and recursion schemes. The recursion schemes can be bounded or unbounded depending on the chosen approach. In the first case we consider the Cobham’s characterization of FPtime [2], in the second case we consider the Bellantoni- Cook characterization of FPtime [1]. In both cases we work over W, instead of N, where W is interpreted over the set of 0-1 words. We look to these three classes of complexity — FPtime, FNP and FPspace — as re- sulting from three different models of computation — deterministic, non-deterministic and alternating Turing machines — and imposing the same resource constraint (poly- nomial time). Thus the adopted recursion schemes should somehow reflect the “in- creasing” computational power of the computation model. For FNP, besides the “cal- ibration” of the recursion schemes, we have an additional problem since one is dealing with a class which is not closed under composition (because NP is not closed under negation). [Close]

Abstract: In Computer Science, the use of logical formalisms to describe, query or manipulate structured data is now firmly embedded in both theory and practice. Having data described/specified within a logical formalism we often want such a specification to undergo static analysis – an automated procedure that optimizes the specification with respect to some correctness and efficiency criteria. Static analysis of specifications described in logical formalism often boils down to verifying one of the two basic logical properties, namely satisfiability and finite satisfiability. Undecidability of the classical decision problem (=the satisfiability problem for first- order logic) results in two possible responses. The first one is to develop programs to test satisfiability of arbitrary collection of first-order formulas, accepting that, however well they generally work in practise, there will always be problem instances that defeat them. The second is to restrict attention to a fragment of first-order logic for which the satisfiability problem is decidable, exploiting the fact that in many real-life situations, the formulas we encounter fit comfortably into such fragments. In this talk we overview recent work in the quest for expressive logics with good algorithmic properties. We concentrate mainly on fragments of first-order logic defined by restricting the number of variables and usage of quantifiers to guarded quantification, and their variants or extensions motivated by real-life applications. We are equally interested in satisfiability and finite satisfiability, as in many application areas we want to model systems and computation to be essentially finite. While tracing the boundary between decidable and undecidable fragments we study their similarities and differences to understand their power and limitations and to stress out key properties responsible for (un)decidability or (in)tractability. We give examples of fragments enjoying the finite model property: any satisfiable formula is true in some finite structure, and the tree model property: any satisfiable formula is true is some tree-like structure. We present fragments for which these two key properties led to optimal decision procedures and contrast these fragments with their extensions where more sophisticated reasoning is required. We give special attention to linear and integer programming techniques that have recently proved useful to design optimal algorithms to decide uniformly both, the finite and the unrestricted satisfiability problems for certain expressive fragments. The talk involves recent and ongoing work with Emanuel Kieroński, Jakub Michaliszyn, Ian Pratt-Hartmann, Wiesław Szwast, Georg Gottlob and Andreas Pieris. The title of the talk has been inspired by Quine. [Close]