Catálogo de publicaciones - libros

This paper describes a type-1 framework for computable analysis designed to facilitate efficient implementations and discusses properties that have not been well studied before for type-1 approaches: the introduction of complexity measures for type-1 representations of real functions, and ways to define intensional functions, i.e. functions that may return different real numbers for the same real argument given in different representations. This approach has been used in a recently developed package for exact real number computations, which achieves performance comparable to the performance of machine precision floating point.

We study computability on sequence spaces, as they are used in functional analysis. It is known that non-separable normed spaces cannot be admissibly represented on Turing machines. We prove that under the Axiom of Choice non-separable normed spaces cannot even be admissibly represented with respect to any compatible topology (a compatible topology is one which makes all bounded linear functionals continuous). Surprisingly, it turns out that when one replaces the Axiom of Choice by the Axiom of Dependent Choice and the Baire Property, then some non-separable normed spaces can be represented admissibly on Turing machines with respect to the weak topology (which is just the weakest compatible topology). Thus the ability to adequately handle sequence spaces on Turing machines sensitively relies on the underlying axiomatic setting.

We give a Natural Deduction formulation of an adaptation of Gödel’s functional ( Dialectica ) interpretation to the extraction of (more) efficient programs from (classical) proofs. We adapt Jørgensen’s formulation of pure Dialectica translation by eliminating his “Contraction Lemma” and allowing free variables in the extracted terms (which is more suitable in a Natural Deduction setting). We also adapt Berger’s uniform existential and universal quantifiers to the Dialectica-extraction context. The use of such quantifiers without computational meaning permits the identification and isolation of contraction formulas which would otherwise be redundantly included in the pure-Dialectica extracted terms. In the end we sketch the possible combination of our refinement of Gödel’s Dialectica interpretation with its adaptation to the extraction of bounds due to Kohlenbach into a light monotone functional interpretation.

We show that Csanky’s fast parallel algorithm for computing the characteristic polynomial of a matrix can be formalized in the logical theory LAP , and can be proved correct in LAP from the principle of linear independence. LAP is a natural theory for reasoning about linear algebra introduced in [8]. Further, we show that several principles of matrix algebra, such as linear independence or the Cayley-Hamilton Theorem, can be shown equivalent in the logical theory QLA . Applying the separation between complexity classes $\textbf{AC}^0[2]\subsetneq\textbf{DET}(\text{GF}(2))$ , we show that these principles are in fact not provable in QLA . In a nutshell, we show that linear independence is “all there is” to elementary linear algebra (from a proof complexity point of view), and furthermore, linear independence cannot be proved trivially (again, from a proof complexity point of view).

The proof system G $_{\rm 0}^{\rm *}$ of the quantified propositional calculus corresponds to NC ^1, and G $_{\rm 1}^{\rm *}$ corresponds to P , but no formula-based proof system that corresponds log space reasoning has ever been developed. This paper does this by developing GL ^*. We begin by defining a class Σ CNF (2) of quantified formulas that can be evaluated in log space. Then GL ^* is defined as G $_{\rm 1}^{\rm *}$ with cuts restricted to Σ CNF (2) formulas and no cut formula that is not quantifier free contains a non-parameter free variable. To show that GL ^* is strong enough to capture log space reasoning, we translate theorems of Σ $_{\rm 0}^{B}$ -rec into a family of tautologies that have polynomial size GL ^* proofs. Σ $_{\rm 0}^{B}$ -rec is a theory of bounded arithmetic that is known to correspond to log space. To do the translation, we find an appropriate axiomatization of Σ $_{\rm 0}^{B}$ -rec, and put Σ $_{\rm 0}^{B}$ -rec proofs into a new normal form. To show that GL ^* is not too strong, we prove the soundness of GL ^* in such a way that it can be formalized in Σ $_{\rm 0}^{B}$ -rec. This is done by giving a log space algorithm that witnesses GL ^* proofs.

We present a sound and sufficient criterion for identifying polynomial-time recursive functions over higher-order data structures generalizing the seminal results by Bellantoni and Cook [1] and Leivant [2] to complex structural data-types. The criterion, presented as a deductive system, always terminates with a response that is either yes or don’t know . The criterion is complete in the sense that every polynomial-time recursive function over binary strings has at least one implementation that is identified by our criterion; whether this is also true for arbitrary higher-order data structures remains an open problem. Logic programming serves as the underlying model of computation and our results apply to the Horn fragment as well to the fragment of hereditary Harrop formulas.

We show that confluence of shallow and right-linear term rewriting systems is decidable. This class of rewriting system is expressive enough to include nontrivial nonground rules such as commutativity, identity, and idempotence. Our proof uses the fact that this class of rewrite systems is known to be regularity-preserving, which implies that its reachability and joinability problems are decidable. The new decidability result is obtained by building upon our prior work for the class of ground term rewriting systems and shallow linear term rewriting systems. The proof relies on the concept of extracting more general rewrite derivations from a given rewrite derivation.

At the annual conference of the EACSL, CSL’04, it was suggested to the newly elected president of EACSL that steps be taken to make the Annual Conference of EACSL even more attractive for young researchers in Logic and Computer Science. In response to this suggestion, the EACSL Board decided in November 2004 to launch the Ackermann Award, the EACSL Outstanding Dissertation Award for Logic in Computer Science.

The treasurer and board member of the European Association for Computer Science Logic (EACSL), Prof. Dr. Clemens Lautemann passed away on 29 April 2005 at the age of only 53 years after a short, serious illness. He is survived by his wife Rose and his two children Anne (21) and Christopher (16). Clemens Lautemann joined the board of the EACSL as treasurer in 1997. We, the EACSL community, and all who knew him, will miss him and remember him warmly. After studying Mathematics, Political Sciences, Philosophy and Computer Sciences at the Universities of Marburg, Bielefeld and Berlin, Clemens Lautemann earned a doctorate in Natural Sciences in June 1983. He dedicated himself to scientific research in Berlin, Osnabrück, Bremen, Edinburgh and Mainz. Theoretical Computer Science was his field of interest, especially Logic and Computational Complexity, and he obtained important results in the fields of Graph Theory, Structural Complexity and Finite Model Theory. His scientific work gained worldwide recognition. Clemens Lautemann joined the Institute for Computer Science at the Johannes Gutenberg University as Professor for Theoretical Computer Science in 1989. He was an inspiring teacher who motivated his students in his special field of expertise and he was actively engaged in encouraging young people. He supported the Bundeswettbewerb Informatik by accompanying pupils interested in the Natural Sciences. Several of his students and PhD candidates were awarded scientific prizes. Clemens Lautemann was deeply concerned with the further development of the Institute for Computer Science. He cared very much for the Institute’s future and played a major part in establishing the new Bachelor of Computer Science program. He was also interested in interdisciplinary cooperation and was one of the founders of the research group Bioinformatik at his university. Clemens Lautemann distinguished himself in many ways, as a warm and forthcoming person, as an original scientist, and as a committed teacher and supervisor with a vision beyond the shortlived fashions of the day. We all liked him very much and will miss his friendly, open-hearted personality. We are very sad that he will not be with us any longer. Clemens Lautemann’s family, friends, students, and colleagues will keep pleasant memories of him with them for a long time.