La complexité implicite étudie des calculs et des langages dont les programmes ont une complexité bornée, en terme de temps de calcul ou de mémoire requise (polynomial, exponentiel, ... par rapport aux données).

Plusieurs approches ont été utilisées pour garantir de telles bornes, notamment la Logique linéaire et ses variantes, les systèmes de réécriture avec quasi-interprétations, les types linéaires avec ressources pour les langages fonctionnels.

Cette théorie nécessite désormais que l’on trouve des éléments unificateurs, soit par des systèmes plus généraux soit par des approches plus sémantiques.

La sémantique des jeux modélise les langages de programmation en interprétant les types par des jeux à deux joueurs, les programmes par des stratégies pour l’un des joueurs (l’autre joueur représentant l’environnement d’évaluation) et les interactions par des parties. Cette présentation explicite de l’interaction comme suite de coups devrait permettre de parler de complexité au niveau sémantique.

Objectifs :

  A. une approche sémantique unificatrice pour les divers systèmes de complexité implicite à travers la sémantique des jeux ;
  B. l’extension des résultats concernant les systèmes connus, notamment la logique linéaire ;
  C. de nouveaux systèmes plus généraux, voire un cadre unitaire recouvrant plusieurs des systèmes actuels de complexité implicite.

Résultats attendus :

  D’une part des résultats fondationnels, en particulier une sémantique des jeux polynomiale permettant de comparer les systèmes de complexité implicite existants.
  D’autre part l’amélioration de l’utilisation des systèmes de complexité implicite pour la vérification statique de complexité, notamment grâce aux systèmes de types.
  Enfin la définition de nouveaux systèmes pourrait permettre d’obtenir des méthodes de vérification plus flexibles.

Méthodologie :

A. Sémantique. On définira une sémantique des jeux équipée d’une notion de complexité pour les stratégies, puis une sémantique de stratégies polynomiales. Dans un second temps on interprétera les systèmes de complexité implicite polynomiale dans cette sémantique de jeux.

B. Types lambda-calcul et réseaux. On poursuivra l’étude des variantes de logique linéaire à complexité bornée comme systèmes de types pour le lambda-calcul : on s’intéressera à l’inférence de type, aux applications à la réduction optimale et aux extensions avec des types récursifs.

C. Complexité implicite et expressivité. Utilisant les résultats des parties A et B on cherchera à définir un système plus général englobant plusieurs des systèmes existants, par exemple les types linéaires d’Hofmann et un système de logique linéaire polynomiale. Enfin on considérera la complexité au sens du modèle BSS sur une structure arbitraire et l’adaptation à ce cadre des systèmes de complexité implicite polynomiale avec ordre supérieur.