Complexité implicite
Enseignants:
Patrick Baillot , Paulin Jacobé de Naurois
à noter:
examen: le mercredi 5/1/2011, 13h30-16h30, salle B2. Notes de cours autorisées.
Cours
Horaire: mercredi 13h30-16h30 (à partir du 10/11), salle B2.
Références
Language: this course is given in English (even though the summary below is in French).
Résumés des cours:
cours 1 (15/09/2010):
introduction à la complexité implicite.
Préliminaires:
Rappel classes de complexité P, FP, FElem (fonctions calculables en
temps élémentaire).
Système F:
règles de typage (style déduction naturelle) du système F à la Curry. Types
de données. Itération. Exemples de termes. Préservation du typage. Thme de
normalisation forte.
Chap. 1: Logique linéaire élémentaire.
intro: motivations et intuitions de la logique linéaire.
cours 2 (22/09/2010):
Système ELL (logique linéaire
élémentaire intuitionniste) en déduction naturelle, vu comme système de
types pour le lambda-calcul. EAL: version avec affaiblissement général.
Opération d'oubli de ELL vers F. Types de données dans ELL: entiers
unaires, mots binaires. Exemples de termes typés. Préservation du
typage par réduction jusqu'à la forme normale.
Thme: si t typable dans EAL de type N-o!^k N, alors t représente une
fonction élémentaire;
toute fonction élémentaire peut-être calculée par un terme de cette
forme. (première partie du thme sera démontrée dans la suite).
Réseaux de preuves (intuitionnistes) pour ELL: traduction inductive des
dérivations de type
par des réseaux. Exemples de réseaux.
cours 3 (23/09/2010):
Règles de réduction sur les réseaux (élimination des coupures). La
beta-réduction des termes simule la réduction des
réseaux. Forme
normale de réseau et forme normale de terme. Profondeur. Propriété de
stratification. Thme: un réseau R peut être réduit en au plus
K(d+1,|R|) étapes. Démonstration de ce thme (stratégie de réduction
par profondeurs). Conséquence: borne de complexité élémentaire pour les termes de type
N-o!^k N.
cours 4 (29/09/2010):
Complétude: si f est une fonction élémentaire,
alors f est représentable dans EAL. Itération dans
ELL. Coercitions de types de données.
Chap. 2: Logique linéaire light et complexité PTIME.
Langage
de formules et règles de LLL (logique linéaire light
intuitionniste) et LAL (version affine) vus comme systèmes de types.
Traduction de LLL vers ELL, et opération d'oubli vers F. Types de
données dans LLL. Exemples de termes typés. Itération dans LLL. Réseaux
de LLL et réduction. Traduction des réseaux LLL vers réseaux ELL. Thme:
si R réseau LLL de profondeur d, il peut être réduit en un réseau sans
coupure en un nombre d'étapes en O((d+1)|R|^{2^d}).
cours 5 (6/10/2010):
démonstration de la borne de complexité sur la réduction
des réseaux de LLL: notion de potentiel d'une boîte; borne sur le
potentiel; borne sur l'augmentation de taille à chaque round de
la stratégie; conclusion. Coercitions de types de données dans LLL. Thme:
les fonctions représentables dans LAL sont exactement les fonctions de FP.
cours 6 (13/10/2010):
Démonstration de la FP-complétude pour LAL (esquisse): simulation d'une machine de Turing de temps polynomial.
Le système DLAL vu comme un sous-système de LAL (restriction du
langage des formules considérées). Préservation du typage DLAL par
beta-réduction. Borne sur la beta-réduction pour les termes typables
dans DLAL (admis). Les fonctions représentables dans DLAL sont exactement les fonctions de FP.
Chap. 3: Système de types linéaires pour le calcul
non-size-increasing.
introduction: discussion sur les programmes non typables dans LAL
(contraintes sur l'imbrication des itérations).
Système de types linéaires non-size-increasing (NSI), langage de
termes, règles de typage, réduction des termes. Représentation des
listes. Exemples de programmes typables (tri par insertion). Prop: si
un programme est typable dans NSI, alors il représente une fonction de
FP.
Prop: si t typable dans NSI, de type L(A)-oL(A), alors t
représente une fonction f telle que: longueur(f(l))<= longueur
(l).
Thme: une fonction f sur les mots binaires est représentable
dans NSI ssi: f appartient à FP et pour tout mot l, longueur(f(l))<= longueur
(l). (résultats admis).
cours 7 (10/11/2010)(3h):
Rappel des fonctions
récursives primitives et récursives partielles. Equivalence entre
fonctions récursives partielles et fonctions Turing calculables.
Caractérisation de Cobham
de FP par restriction de la récursion primitive bornée en notation sur les mots binaires.
Caractérisation de Bellantoni-Cook de FP par la récursion sûre.
Extension de la caractérisation Bellantoni-Cook au cadre du calcul sur
des structures arbitraires dans le modèle Blum-Shub-Smale.
cours 8 (17/11/2010)(3h):
Rappels sur les circuits booléens. Classe PAR des langages décidables par une famille
P-uniforme de circuits de profondeur polynomiale. Thme: PAR=PSPACE.
Classe des fonctions définies par récursion sûre avec substitution (SRS: safe recursion
with substitution) (Leivant-Marion). Thme: Les fonctions de SRS à valeurs dans {0,1} sont exactement
les fonctions de PSPACE. Démonstration de ce thme. Thme: SRS=FPSPACE (fonctions calculables en espace polynomial).
Classe des fonctions définies par récursion sûre sur les arbres (RTR:
ramified tree recursion) (Leivant). Rappel des définitions des classes
NC_k et NC. Thme: Les fonctions de RTR à valeurs dans {0,1} sont
exactement
les fonctions de NC. (non encore démontré). Rappel des machines de
Turing alternantes. Thme:
ATM(log^k time, log space)=NC^k.
cours 9 (24/11/2010)(3h):
Démonstration du Thme reliant RTR et NC.
Systèmes de réécriture du 1er
ordre. Interprétations polynomiales. Caractérisation de
FP par les interprétations polynomiales (d'après Bonfante-Cichon-Marion-Touzet).
cours 10 (1/12/2010)(3h):
Ordres récursifs sur les chemins (RPO) pour garantir la
terminaison. Ordre PPO (ordre produit). Notion de quasi-interprétation d'un
système de réécriture. Thme (Marion-Moyen): les
systèmes de réécriture admettant un ordre PPO et
une quasi-interprétation additive caractérisent les
fonctions de FP.