Non-laziness in implicit computational complexity and probabilistic λ-calculus
Non-paresse dans la complexité computationnelle implicite et le λ-calcul probabiliste
par Gianluca CURZI sous la direction de Michèle ¿PAGANI¿ et de Luca ROVERSI
Thèse de doctorat en Informatique. Logique
ED 386 Sciences Mathematiques de Paris Centre


Sujets
  • Complexité de calcul (informatique)
  • Lambda-calcul
  • Logique de seuil
  • Sémantique opérationnelle
Le texte intégral n’est pas librement disponible sur le web
Vous pouvez accéder au texte intégral de la thèse en vous authentifiant à l’aide des identifiants ENT de l’Université, au sein de l’établissement en utilisant un compte ou en demandant un accès extérieur si vous pouvez justifier de votre appartenance à un établissement chargé d’une mission d’enseignement supérieur ou de recherche

Se connecter ou demander un accès au texte intégral

Les thèses de doctorat soutenues à Université de Paris sont déposées au format électronique

Consultation de la thèse sur d’autres sites :

Theses.fr

Description en anglais
Description en français
Mots clés
Lambda-calcul probabiliste, Bisimulation, Temps polynomial
Resumé
Cette thèse explore les avantages de la "non-paresse" dans la Complexité Computationnelle implicite et dans le lambda calcul probabiliste. Plus précisément, cette thèse peut être divisée en deux parties principales. Dans la première, nous étudions dans tous les sens les mécanismes d'effacement et de duplication linéaire, qui nous conduisent aux systèmes de typage LEM (Lin- early Exponential Multiplicative Type Assignment) et LAM (Linearly Additive Multiplicative Type Assignment). Le premier est capable d'exprimer des versions plus faibles des règles exponentielles de la Logique Linéaire, tandis que le second est doté de règles additifs plus faibles, appelées additifs linéaires. Ces systèmes bénéficient respectivement d'une élimination de coupure cubique et d'un résultat de normalisation linéaire. Étant donné que les additifs linéaires ne nécessitent pas d'évaluation paresseuse pour éviter l'explosion exponentielle de la normalisation (contraire- ment aux additifs standard), ils peuvent être utilisés pour obtenir une caractérisation implicite des fonctions calculables en temps polynomial probabiliste qui ne dépend pas du choix de la stratégie de réduction. Ce résultat a été réalisé dans STA, un système obtenu en dotant STA (Soft Type Assignment) d'une formulation aléatoire des additifs linéaires, qui capture aussi les classes de complexité PP et BPP. La deuxième partie de la thèse est centrée sur le lambda calcul probabiliste doté d'une sémantique opérationnelle basée sur la réduction de tête, c'est-à-dire une politique d'évaluation non paresseuse d'appel par nom. Nous prouvons que la bisimilarité probabiliste est "fully abstract" par rapport à l'équivalence observationnelle. Ce résultat témoigne le pouvoir discriminant de la non-paresse, qui permet de retrouver une correspondance parfaite entre les deux équivalences qui manquait dans le cadre paresseux. De plus, nous montrons que la similarité probabiliste est correcte mais pas complète par rapport au préordre observationnel.