CR 13: Implicit Computational Complexity (2015-2016)

Description

Logic is widely used to analyse the correctness of programs. But on the quantitative side, can it say anything about their efficiency?

In this course we will take an abstract view on this question, through the approach of complexity. We will first present a logic which is well-suited to study quantitative properties, as it gives an explicit status to duplication and erasing: linear logic. In a second part of the course we will show how this logic leads to the design of type systems for functional calculi, which statically ensure complexity properties, e.g.: if a program is well-typed then it runs in polynomial time.

Teachers

• Patrick Baillot (Complexity)
• Olivier Laurent (Linear Logic)

Lecture 1

• References: Théorie de la démonstration (pages 8-19)
• Homework: Subject 1: Classical Sequent Calculus (return date: September 25th)

Lecture 2

• References: Théorie de la démonstration (pages 19-25 and 85-86)
• Homework: Subject 2: Linear Sequent Calculus (return date: October 2nd)

Lecture 3

• References: Théorie de la démonstration (pages 85-90)

Lecture 4

• References:
  • An Introduction to Proof Nets (pages 1-12 and additional informations on rewriting pages 29-34)
  • Théorie de la démonstration (pages 95-99 and 103-104)
• Homework: Subject 3: Multiplicative Proof-Nets (return date: October 16th)

Lecture 5

• References:
  • An Introduction to Proof Nets (pages 12-21)
  • Théorie de la démonstration (pages 106-112 and 91)

Lecture 6

• References:
  • Decorating Proof-Nets with Lambda-Terms
• Homework: (return date: November 6th) read the notes as an article, write down detailed proofs, find possible places where important details are missing (at least from your point of view), give remarks, comments, optimizations, etc and send all that.

Lecture 7

1. Intuitionistic logic and lambda-calculus
   • Sequent calculus LJ₂ and decoration with lambda-terms.
   • Properties of cut-elimination and beta-reduction.
   • Data-types: N, W.
   • Iteration on Church integers and Church binary words.
   • Strong normalisation of typable terms.
2. Elementary linear logic
   • Language and sequent calculus rules.
   • Intuitionistic version IELL and decoration with lambda-terms.
   • Forgetful map to LJ₂.
   • Affine version IEAL.
   • Data-types: N^IELL, W^IELL.

Lecture 8

2. Elementary linear logic (continued)
   • Examples of terms typed in IEAL: addition, multiplication, word concatenation, ...
   • ELL proof-nets and their reduction.
   • Complexity bound on the reduction of ELL proof-nets, in O(2_d^|R|). Beginning of the proof.

• Homework: Subject 5: Elementary linear logic (return date: November 25th)

Lecture 9

2. Elementary linear logic (continued)
   • Complexity bound on the reduction of ELL proof-nets: end of the proof.
   • The functions representable in IEAL with types (N-o!^kN) are exactly the elementary functions.
   • Iteration in IEAL.
   • Functions representable in IELL with type (!W-o!!Bool) are polynomial time predicates.

Lecture 10

2. Elementary linear logic (continued)
   • Functions representable in IELL with type (!W-o!³Bool) are exponential time predicates.
3. Light linear logic
   • Intuitionistic version ILLL and decoration with lambda-terms. Forgetful map to IELL. Affine version ILAL.
   • Data types N^ILLL, W^ILLL. Examples of typed terms.
   • Iteration.
   • LLL proof-nets and their reduction. Complexity bound on the reduction of LLL proof-nets, in O(|R|^2d). Beginning of the proof.

• Homework: Subject 6: Light linear logic (return date: December 11th)

Lecture 11

3. Light linear logic (continued)
   • Complexity bound on the reduction of LLL proof-nets: end of the proof.
   • Data-types coercions.
   • FP completeness (proof sketch).
   • The functions representable in ILAL with types (W-o§^kW) are exactly the class FP.
   • Subsystem DLAL: polynomial bound on beta reduction.

Content

• Linear Logic
  • its proof systems: sequent calculus, proof-nets, cut-elimination
  • analysis of intuitionistic logic and lambda-calculus
  • denotational semantics
• Application to complexity
  • elementary linear logic and exponential complexity classes
  • light linear logic and polynomial time complexity
  • linear type systems: types for non-size-increasing computation, linear dependent types

References

• Proofs and Types (introduction to proof theory and λ-calculus)
• Théorie de la démonstration / Proof Theory (course notes in French)
• An Introduction to Proof Nets (preliminary course notes)
• Linear Logic (J.-Y. Girard's original paper)
• LL Wiki (wiki on Linear Logic)
• Light Linear Logic (Jean-Yves Girard)
• Intuitionistic light affine logic (Andrea Asperti and Luca Roversi)
• On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy (Patrick Baillot)
• A Syntactical Analysis of Non-Size-Increasing Polynomial Time Computation (Klaus Aehlig and Helmut Schwichtenberg)

Prerequisites

• Simply typed lambda-calculus
• Bases of natural deduction and sequent calculus

Evaluation

Main evaluation will be a final exam.

Additional evaluation (leading to bonus on the final grade) will be based on homework.