Complexity and Logic:
Lecture from the Geocal'06 Winter School

Marseille - Luminy
February 6 - 10, 2006

Context: This course is part of the Geometry of Computation 2006 Winter School (Geocal06). It will be followed on February 13->17 by a workshop on Implicit Computational Complexity.
Geocal'06 is 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.

Winter school: programme of Week 2: Logic and Computation.

Lecturers:   Patrick Baillot (Paris13),   Martin Hofmann (Munich),   Jean-Yves Marion (Nancy).

References .

Slides:   Part 1.1 and 1.2 (J.-Y. Marion), part 2 (P.Baillot), part 3 (M.Hofmann).

Presentation: This lecture will present logical approaches to ensure complexity bounds on lambda-calculus or functional programs, with a particular emphasis on polynomial time complexity. This line of research can be traced back to work by Leivant on restrictions of system F, and by Girard who showed that controling the logical rules responsible for duplication in Linear logic proofs made it possible to tame the complexity of the associated programs: he obtained in this way a logical characterization of elementary complexity (ELL system) and of polynomial time complexity (LLL system). Later Lafont proposed another variant of Linear logic also characterizing polynomial time. This course will also present the typed lambda-calculi that have been designed from these systems.
Another approach is based on restrictions of the primitive recursion scheme that lead to characterizations of polynomial time functions as well as of other complexity classes. This line was developed by Bellantoni and Cook and by Leivant and Marion. Later Marion adapted these ideas to the setting of first-order rewriting systems and showed that new criteria, based on termination orderings and quasi-interpretations provided flexible techniques to control the complexity of a large class of programs.
Finally Hofmann designed a type system for a functional language based on a fragment of Linear logic and ensuring that the typed programs are non-size-increasing and can be run in polynomial time.
This course will try to stress and discuss the issue of algorithmic expressivity: even if various systems characterize polynomial time functions, it is desirable that the languages obtained are expressive enough so as to be able to write some standard algorithms.

Outline of the course ( timetable ):

  • From Primitive recursion to complexity classes. Rewriting systems and quasi-interpretation (Jean-Yves Marion). monday 6/2: 9:30->15:30
  • Linear logic, lambda-calculus and polynomial time complexity (Patrick Baillot). monday 6/2: 16:00->17:30. tuesday 7/2: 9:30->12:30
  • Non-size increasing computation and linear types (Martin Hofmann). thursday 9/2: 11:00->12:30. friday 10/2: 9:30->12:30.

    • References:

  • Andrea Asperti, Luca Roversi. Intuitionistic Light Affine Logic. ACM Transactions on Computational Logic 3(1): 137-175 (2002)
  • Patrick Baillot, Kazushige Terui. Light Types for Polynomial Time Computation in Lambda-Calculus . Proceedings of LICS 2004: pp.266-275, 2004.
  • S. Bellantoni and S. Cook. A new recursion-theoretic characterization of the poly-time functions. Computational Complexity, vol. 2, pp. 97--110, 1992.
  • G. Bonfante, J.-Y. Marion, J.-Y. Moyen. Quasi-interpretation a way to control resources. Submitted, 2005.
  • J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types, Cambridge University Press, 1989.
  • J.-Y. Girard. Light Linear Logic, Information and Computation, 1998.
  • J.-Y. Girard. Linear Logic, its syntax and semantics, Advances in Linear Logic, eds Girard, Lafont, Regnier, London Mathematical Society Lecture Notes Series 222, Cambridge University Press 1995.
  • Martin Hofmann. Linear types and non-size-increasing polynomial time computation. Information and Computation 183(1): 57-85 (2003)
  • Martin Hofmann. The strength of non-size increasing computation. proceedings of POPL 2002: pp. 260-269, 2002.
  • Yves Lafont. Soft linear logic and polynomial time. Theoretical Computer Science 318(1-2): 163-180, 2004.
  • D. Leivant. Predicative recurrence and computational complexity I: Word recurrence and poly-time. Feasible Mathematics II, ed. P. Clote and J. Remmel, pp. 320--343, Birkhauser, 1994.
  • D.Leivant and J.-Y. Marion. Lambda Calculus Characterizations of Poly-Time. Fundamenta Informaticae, 19 (1,2), pp. 167--184, 1993.
  • D. Leivant and J.-Y. Marion. Ramified recurrence and computational complexity II: substitution and poly-space . Computer Science Logic, 8th Workshop, CSL '94, Kazimierz,Poland, pp. 486--500, LNCS 933, Springer, 1994.

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

    Student grants : Some (limited) funding is possible for students attending the school (see the preregistration form).