Workshop on Implicit Computational Complexity
as part of GEOCAL'06

Marseille - Luminy
February 13 - 17, 2006

Context: This workshop is part of Geometry of Computation 2006 (Geocal06), a special series of events in theoretical computer science organized by the GEOCAL group and taking place at the CIRM from January 30 to March 3. Geocal06 is supported by the following institutions: CIRM, CNRS, Luminy, ParisNord, FRUMAM, IML, PPS, LIPN.

Programme (with Slides of the talks) and Abstracts .

Invited speakers:

• Martin Hofmann, LMU, Munich (Germany).
• James Royer, Syracuse University (USA).
• Kazushige Terui, NII, Tokyo (Japan).

Timetable of the week (3 workshops)

Presentation: Implicit Computational Complexity (ICC) has emerged from various propositions to use logic and formal methods like types, rewriting systems... to provide languages for complexity-bounded computation, in particular for polynomial time computing.
It aims at studying the computational complexity of programs without refering to a particular machine model and explicit bounds on time or memory, but instead by relying on logical or computational principles that entail complexity properties. Several approaches have been explored for that purpose, like linear logic, restrictions on primitive recursion, rewriting systems, types and lambda-calculus... They often rely on the functional programming paradigm.
Two objectives of ICC are:
- on the one hand to find natural implicit logical characterizations of functions of various complexity classes,
- on the other hand to design systems suitable for static verification of programs complexity.
In particular the latter goal requires characterizations which are general enough to include commonly used algorithms.

This meeting will be preceded by a course on Complexity and Logic (6->10/2) organized as part of the GEOCAL'06 winter school and especially targeted at PhD students, with lectures by P.Baillot, M.Hofmann and J.-Y. Marion. Some (limited) funding is possible for students attending the school and/or the workshop.
The workshop is intended to be a forum for researchers interested in ICC to discuss recent developments and open issues. It will be open to contributions on various aspects of ICC including (but not exclusively):
- logical systems for implicit computational complexity,
- linear logic,
- semantics of complexity-bounded computation,
- rewriting and termination orderings,
- types for controlling complexity,
- extensions from functional approach to ICC to imperative or concurrent setting; applications to automated verification...
Propositions of contributions consist in a title and a short abstract (see the Geocal06 site ).
After the workshop a call-for-paper for a special issue of a journal might be considered (either for the GEOCAL'06 session, or for the workshop itself), with standard refering procedure.

Preregistration: on the Geocal06 site. Deadline: October 30, 2005.

Organizers: Patrick Baillot , LIPN, Univ. Paris 13/CNRS, (contact). Jean-Yves Marion , LORIA Nancy.

Programme

Abstracts

• Vincent Atassi , LIPN, Université Paris 13, France.
  Title: Type inference in Elementary Linear Logic with coercions and its implementation
  
  Abstract: Elementary Linear Logic (ELL), is a logic in which proofs reduce to their normal form by cut-elimination in elementary time. Conversely, this system is expressive enough to encode all elementary functions from integers to integers and thus, yields an implicit and logic characterisation of the elementary time complexity class. Using the Curry-Howard correspondence, we focus on the use of ELL as type system for lambda calculus, and more precisely, on type inference. Looking at ELL proof-nets, the bounded termination properties arise from a certain discipline in placing boxes. Specifically, since some linear logic principles are not valid in ELL, a function cannot be applied to an argument if both terms are not at the same box nesting level. However, data types (such as integers) may admit coercions, that is the possibility to add boxes and increase nesting level, and from a typing point of view, that means the !^n N -o !^(n+1)N formula has a proof. To ensure typing of some basic functions such as square elevation, the programmer should explicitly place those coercions in his terms, and that is not satisfactory, for it breaks the transparency of typing. We will present an efficient type inference algorithm for ELL, and discuss its implementation in caml. Next we will introduce its extension to the automatic coercions placement, using a subtyping relation, which as a result correctly extends the set of typable terms.

• Daniel de Carvalho , IML Université Aix-Marseille II, Marseille, France.
  Title: Non uniform semantics for Lambda Calculus, intersection types and computation time
  
  Abstract: The relational semantics for Linear Logic induces a semantics for the type free Lambda Calculus. This is built on non-idempotent intersection types and we prove that the size of the derivations is related to the execution time of lambda-terms in the Krivine machine.

• Frédéric Dabrowski, INRIA Sophia Antipolis, France.
  Title: Feasible reactivity for synchronous cooperative threads
  
  Abstract: We are concerned with programs composed of cooperative threads whose execution proceeds in synchronous rounds called instants. We develop static analysis methods to guarantee that each instant terminates in time polynomial in the size of the parameters of the program at the beginning of the computation.

• Ugo Dal Lago , Università di Bologna, Italy.
  Title: Context Semantics, Linear Logic and Implicit Complexity
  
  Abstract: We study context semantics of (multiplicative) linear logic in view of implicit complexity issues. In particular, we show how semantics can be used to give bounds on the normalization time for any linear logic proof-net.

• Jean-Yves Girard, IML CNRS Marseille, France.
  Title: Hyperfiniteness and light exponentials
  
  Abstract: Light exponentials are based upon the idea of termination a priori, independently of logical correctness. This is the case for perfect logic due to the finite dimension of the spaces involved. In presence of exponentials, one needs an infinite space, but not too infinite so too speak, infinite from outside, finite from inside. The vN algebra of a locally finite discrete group is likely to answer the problem. Everything can be handled by finite matrices, but of arbitrary sizes. Although there is only one hyperfinite algebra of this form, the finite approximants -seen as syntax- will look very depending on the group. A specific group, basically devoted to the drawing of links and boxes is therefore at work.

• Emmanuel Hainry , LORIA/INPL, Nancy.
  Title:Recursive analysis and real recursive functions
  
  Abstract: From the beaver to the tortoise, every living being likes to compute, and uses its own model of computing. The most widespread and accepted computation paradigm deals with integer numbers and works in discrete time. This behaviour is embodied by Turing machines, supported by Church-Turing thesis that states that all reasonable discrete models of computation compute exactly the same class of functions : the computable functions. However computing can be done in continuous time and over continuous domains. Some machines working in this framework have been built an dused. Several different models have been created to describe such computation. Unfortunately, there exist few comparisons between these models (and most results are of inequality). Among those models, let us cite computable analysis that relies on type-2 machines which are more or less Turing machines that work on a sequence representing a real number and output a similar sequence, the General Purpose Analog Computer (proposed by Shannon) which puts together ``real'' computation units in circuits and real-recursive functions that mimics the definition of discrete computable functions as a closure. This work's aim is to exhibit a bridge between computable analysis and real recursive functions. This way, we provide algebraic characterizations of some classes of functions from computable analysis.

• Martin Hofmann, LMU Munich, Germany.
  Title Programming Languages for LOGSPACE
  
  Abstract: Joint work with Jan Johannsen and Uli Schöpp. I will describe existing logical and linguistic formalisms capturing LOGSPACE or subclasses thereof and outline a tentative research programme aimed at isolating PTIME from a natural subset of LOGSPACE that contains popular LOGSPACE algorithms (but not Reingold's algorithm!)

• Paulin Jacobé de Naurois, LIPN, Université Paris 13, France.
  Title: A Measure of Space for Computing over the Reals
  
  Abstract: We propose a new complexity measure of space for the BSS model of computation. We define LOGSPACE_W and PSPACE_W complexity classes over the reals. We prove that LOGSPACE_W is included in NC^2_R and in P_W, i.e. is small enough for being relevant. We prove that the Real Circuit Decision Problem is P_R-complete under LOGSPACE_W reductions, i.e. that LOGSPACE_W is large enough for containing natural algorithms. We also prove that PSPACE_W is included in PAR_R.

• Reinhard Kahle, Departamento de Matemática, Universidade de Coimbra, Portugal.
  Title: Towards an implicit characterization of NC^k
  
  Abstract: We report on work in progress about an implicit characterization of NC^k. This is joint work with Guillaume Bonfante, Jean-Yves Marion, and Isabel Oitavem

• Harry Mairson, Brandeis University, USA.
  
  Title MLL normalization and transitive closure: circuits, complexity, and Euler tours
  Abstract:

• Jean-Yves Moyen, LIPN, Université Paris 13, France.
  Title: Resource Control Graphs
  
  Abstract: Several programs analysis can be seen as annotation on some kind of Control Flow Graphs, thus describing properties of termination, time or space complexity. In order to try and unify them all, I introduce the notion of Resource Control Graph, based on the tool of Resource Systems with States, a generalisation of Petri nets. This allows to represent in a comprehensive way several existing analysis.

• Karl-Heinz Niggl, Technische Universität Ilmenau, Germany.
  Title: Cerifying polynomial time and linear/polynomial space for imperative programs
  
  Abstract: .pdf

• Isabel Oitavem, Universidade Nova de Lisboa, Portugal.
  Title: Pointers and polynomial space functions
  
  Abstract: In this talk, we give an implicit characterization of the class of functions computable in polynomial space by deterministic Turing machines - Pspace. This is a characterization in the vein of the Bellantoni-Cook characterization of the polytime functions, Ptime, given in [BC]. The main difference between these two characterizations is the formulation of the recursion scheme. To reach Pspace one introduces pointers in the recursion scheme.
  [BC] S. Bellantoni and S. Cook, A new recursion-theoretic characterization of polytime functions, Computational Complexity, 2:97-100, 1992

• Brian Redmond, University of Ottawa, Canada.
  Title: Multiplexor Categories and Models of Soft Linear Logic
  
  Abstract: We begin with an introduction to soft linear logic (SLL) and the corresponding notion of multiplexor category. A multiplexor category consists of a symmetric monoidal closed category (SMCC) together with a soft exponential operator ! and monoidal natural transformations called multiplexors. We shall see that a multiplexor category provides a denotational semantics for SLL. Next we consider various ways of constructing a multiplexor category from a symmetric monoidal closed category having countable limits, which leads to a large class of models. More generally, we give a categorical construction (completion) for building a multiplexor category from a SMCC having only a bounded form of multiplexing. As an application to illustrate these ideas, we construct a realizability model for SLL based on the Hofmann-Scott model for BLL. Finally, we discuss connections with Baillot's Stratified Coherence Spaces for LLL and other future work.

• Simona Ronchi della Rocca, Università di Torino, Italy.
  Title: Soft Linear Logic, lambda-calculus and Intersection Types
  
  Abstract: A type assignment system is presented, assigning to terms of lambda-calculus formulas of Lafont's Soft Linear Logic. The aim is to allow the use of $\lambda $-calculus as programming language, where types are used to assure the termination of a program in polynomial time. In order to inherit all the good properties of the logic, a natural approach would be to transform it into a type assignment system using the Curry-Howard correspondence. Clearly the application of such a correspondence in this case cannot be standard, since the modal connective (!) of the logic does not have a corresponding syntactic constructor in lambda-calculus. The resulting system does not enjoy the subject reduction property. This lack depends on the fact that the logic is presented in a sequent calculus formulation. We solve the problem by restricting both the set of formulas that can be used as types and some rules of the logic, in particular the cut rule. The result is that the set of type assignment derivations corresponds (through the Curry-Howard correspondence) to a proper subset of the Soft Linear Logic proofs. But there is not loss in expressiveness: we prove that the set of terms that can be typed in the restricted system is the same as in the whole system. The restricted system enjoys the subject reduction property, and inherits all the good properties of the Soft Linear Logic: confluence, and polynomial time termination. Polynomial time completeness can be reached through either the use of the universal quantification or by enriching the language by a set of constants with a suitable functional behaviour.
  Moreover by allowing a (restricted form) of intersection as type constructor, the set of algorithms that can be written in the typed language increases, while preserving the complexity limit.
  A language built from Soft Linear Logic through the Curry-Howard correspondence has been recently designed by Baillot and Mogbil. Their language preserves all the good properties of the logic, but, in order to do so, it remembers in its syntax all the applications of typing rules. We think that programming in the stardard lambda-calculus is more natural and friendly.

• James Royer, Syracuse University, USA.
  Title: Adventures in Time and Space
  
  Abstract: We discuss what is essentially a call-by-value version of PCF under a complexity-theoretically motivated type system. The programming formalism, ATR, has its first-order programs characterize the poly-time computable functions, and its second-order programs characterize the type-2 basic feasible functionals of Mehlhorn and Cook and Urquhart. (The ATR-types are confined to levels 0, 1, and 2.) The type system comes in two parts, one that primarily restricts the sizes of values of expressions and a second that primarily restricts the time required to evaluate expressions. The size-restricted part is motivated by Bellantoni and Cook's and Leivant's implicit characterizations of poly-time. The time-restricting part is an affine version of Barber and Plotkin's DILL. Two semantics are constructed for ATR. The first is a pruning of the naive denotational semantics for ATR. This pruning removes certain functions that cause otherwise feasible forms of recursion to go wrong. The second semantics is a model for ATR's time complexity relative to a certain abstract machine. This model provides a setting for complexity recurrences arising from ATR recursions, the solutions of which yield second-order polynomial time bounds. The time-complexity semantics is also shown to be sound relative to the costs of interpretation on the abstract machine

• Ulrich Schöpp, LMU Munich, Germany.
  Title: Space-efficiency and the Geometry of Interaction
  
  Abstract: I will report on work in progress on using the Geometry of Interaction for the space-efficient evaluation of programs. Møller-Neergaard and Mairson have recently defined the function algebra BC^-_epsilon and have shown that it captures LOGSPACE. We propose to use the Geometry of Interaction as a tool for extending this result to more convenient programming languages and to related complexity classes. Using the Geometry of Interaction, computation can be described in terms of question/answer-passing on a static network. Since questions and answers can often be stored using little space, this description can help in devising space-efficient ways of evaluating programs. The main purpose of this talk is to describe how the Geometry of Interation can be used for compiling BC^-_epsilon-expressions into LOGSPACE-programs, and how it can guide the extension of BC^-_epsilon.

• Kazushige Terui, NII Tokyo, Japan.
  Title: Intersection types for implicit computational complexity
  
  Abstract: Intersection types have proven to be useful for reducing dynamic properties of lambda-terms (eg. normalizability) to static ones (eg. typability). By considering their linear/affine analogues, it is possible to characterize even finer dynamic properties, such as normalizability within a given resource bound. In this talk, we overview some basic results on linear/affine intersection type systems, and discuss their possible applications in implicit computational complexity.

• Lorenzo Tortora de Falco, Universita Roma Tre, Italy.
  Title: Obsessional cliques: a semantic characterization of bounded time complexity.
  
  Abstract: We introduce the notion of obsessional clique and prove that the semantics of a proof-net is an obsessional clique iff the (normal form of the) proof-net belongs to ELL.

• Paolo Tranquilli, Universita Roma Tre, Italy.
  Title: The typing problem for second order light logics
  Abstract: One of the approaches to Implicit Computational Complexity consists in using the resource limitations built in Girard's Linear Logic to design type theories which enforce complexity constraints on underlying lambda-terms and which are expressive enough to exhaust the respective complexity classes. In particular we concentrated on EALogic, which enforces and encodes elementar functions, and LAL, together with its variant DLAL by Baillot and Terui, which does the same with polytime functions. Questions arise as to decidability of two problems pertaining type assiginment within these systems: type checking (TC) consists in whether a given type can be assigned to a given term, typability (TYP) in whether a given term can be assigned a type at all. These problems have great importance in an eventual implementation of such systems as programming disciplines. TC and TYP have been proved decidable for the quantifier-free versions of these systems, but second order has a paramount role in obtaining their expressive power. TC is proved to be undecidable for all these systems by an adaptation of the same result for system F by Wells, while decidability of TYP remains up to now an unsolved problem.