Catálogo de publicaciones - libros

We show that, using our more or less established framework of (work started by Cristopher Moore in [9]) together with ideas and concepts of standard computability we can prove theorems of Analysis. Then we will consider our ideas as a bridging tool between the standard on one side and on the other, making real recursive functions a possible branch of . What follows is an Extended Abstract directed to a large audience of CiE 2007, Special Session on Logic and New Paradigms of Computability. (Proofs of statements can be found in a detailed long paper at the address http://fgc.math.ist.utl.pt/papers/hierarchy.pdf.)

To each computable enumerable (c.e.) set with a particular enumeration {}, there is associated a settling function (), where () is the last stage when a number less than or equal to was enumerated into . In [7], R.W. Robinson classified the complexity of c.e. sets into two groups of complexity based on whether or not the settling function was dominant. An extension of this idea to a more refined ordering of c.e. sets was first introduced by Nabutovsky and Weinberger in [6] and Soare [9], for application to differential geometry. There they defined one c.e. set to settling time dominate another c.e. set ( > ) if for every computable function , for all but finitely many , () > (()). In [4] Csima and Soare introduced a stronger ordering, where  >  if for all computable and , for almost all , () > ((())). We give a survey of the known results about these orderings, make some observations, and outline the open questions.

The authors’ ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs run in type-2 polynomial-time and all standard type-2 basic feasible functionals are ATR-definable (ATR types are confined to levels 0, 1, and 2). A limitation of the original version of ATR is that the only directly expressible recursions are tail-recursions. Here we extend ATR so that a broad range of affine recursions are directly expressible. In particular, the revised ATR can fairly naturally express the classic insertion- and selection-sort algorithms, thus overcoming a sticking point of most prior implicit-complexity-based formalisms. The paper’s main work is in extending and simplifying the original time-complexity semantics for ATR to develop a set of tools for extracting and solving the higher-type recurrences arising from feasible affine recursions.

A formal specification of an arithmetic unit for computable normalized rational numbers is proposed. This specification, developed under the scope of the paradigm known as algebraic models of processors, exploits the connection between the signed digit representation for rational numbers in Type-2 Theory of Effectivity and online arithmetic in Computer Arithmetic. The proposal aims for specification formalization and calculation reliability together with implementation feasibility.

This paper introduces two complexity-theoretic formulations of Bennett’s logical depth: and . It is shown that for both formulations, trivial and random infinite sequences are shallow, and a holds, implying that deep sequences cannot be created easily from shallow sequences. Furthermore, the E analogue of the halting language is shown to be polynomial-time deep, by proving a more general result: every language to which a nonnegligible subset of E can be reduced in uniform exponential time is polynomial-time deep.

Abstract geometrical computation naturally arises as a continuous counterpart of cellular automata. It relies on signals (dimensionless points) traveling at constant speed in a continuous space in continuous time. When signals collide, they are replaced by new signals according to some collision rules. This simple dynamics relies on real numbers with exact precision and is already known to be able to carry out any (discrete) Turing-computation. The Blum, Shub and Small (BSS) model is famous for computing over ℝ (considered here as a ℝ unlimited register machine) by performing algebraic computations.

We prove that signal machines (set of signals and corresponding rules) and the infinite-dimension linear (multiplications are only by constants) BSS machines can simulate one another.

We develop a notion of derivative of a real-valued function on a Banach space, called the L-derivative, which is constructed by introducing a generalization of Lipschitz constant of a map. The values of the L-derivative of a function are non-empty weak* compact and convex subsets of the dual of the Banach space. This is also the case for the Clarke generalised gradient. The L-derivative, however, is shown to be upper semi continuous with respect to the weak* topology, a result which is not known to hold for the Clarke gradient on infinite dimensional Banach spaces. We also formulate the notion of primitive maps dual to the L-derivative, an extension of Fundamental Theorem of Calculus for the L-derivative and a domain for computation of real-valued functions on a Banach space with a corresponding computability theory.

When defined with general elimination/application rules, natural deduction and -calculus become closer to sequent calculus. In order to get real isomorphism, normalisation has to be defined in a “multiary” variant, in which reduction rules are necessarily non-local (reason: nomalisation, like cut-elimination, acts at the of applicative terms, but natural deduction focuses at the of such terms). Non-local rules are bad, for instance, for the mechanization of the system. A solution is to extend natural deduction even further to a based on the unification of cut and general elimination. In the unified calculus, a sequent term behaves like in the sequent calculus, whereas the reduction steps of a natural deduction term are interleaved with explicit steps for bringing heads to focus. A variant of the calculus has the symmetric role of improving sequent calculus in dealing with tail-active permutative conversions.

In the framework of parameterized complexity, exploring how one parameter affects the complexity of a different parameterized (or unparameterized problem) is of general interest. A well-developed example is the investigation of how the parameter influences the complexity of (other) graph problems. The reason why such investigations are of general interest is that real-world input distributions for computational problems often inherit structure from the natural computational processes that produce the problem instances (not necessarily in obvious, or well-understood ways). The of a connected graph is the maximum number of leaves in a spanning tree for . Exploring questions analogous to the well-studied case of treewidth, we can ask: how hard is it to solve or or for graphs of bounded max leaf number? We do two things:

(1) We describe much improved FPT algorithms for a large number of graph problems, for input of bounded max leaf number, based on the polynomial-time extremal structure theory associated to the parameter max leaf number.

(2) The way that we obtain these concrete algorithmic results is general and systematic. We describe the approach.

We introduce and discuss some basic concepts of parameterized complexity theory via model-checking problems.