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).
Part 1.1 and
1.2 (J.-Y. Marion),
part 2 (P.Baillot),
part 3 (M.Hofmann).
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 ):
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).