Behavioral Equivalences for Higher-Order Languages with Probabilities

Valeria Vignudelli 1, 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Résumé : Les langages d'ordre supérieur, dont l'exemple paradigmatique est le λ-calcul, sont des langages avec des opérateurs capables de manipuler et d'échanger des programmes. Cette thèse étudie les équivalences comportementales pour des programmes ayant des caractéristiques probabilistes et d'ordre supérieur. L'équivalence comportementale est formalisée comme un contexte et deux axes de recherche sont poursuivis dans la thèse. La première partie de la thèse se concentre sur l'équivalence contextuelle comme moyen d'étudier l'expressivité des différentes langages. Les pouvoirs discriminants offerts par les langages concurrents d'ordre supérieur (comme le π-calcul d'ordre supérieur) sont comparés à ceux offerts par les langages séquentiels d'ordre supérieur (comme le λ-calcul) et par les langages concurrents de premier ordre (comme le CCS). La comparaison est réalisée en examinant les équivalences contextuelles induites par les langages sur deux classes de processus de premier ordre: les processus non déterministes, et les processus probabilistes. En conséquence, on obtient le spectre des pouvoirs discriminants de plusieurs variétés de langages de premier ordre et d'ordre supérieur, dans un cadre non déterministe et dans un cadre probabiliste. La deuxième partie de la thèse est consacrée aux techniques de preuve pour l'équivalence contextuelle dans les λ-calculs probabilistes. Les techniques de preuve basées sur la bisimulation sont étudiées, avec un accent particulier sur la dérivation de bisimulations qui sont complètement abstraites pour l'équivalence contextuelle (c'est-à-dire qui coïncident avec elle). Comme premier résultat, l'abstraction complète de la bisimilarité applicative et de la similarité est prouvée pour un λ-calcul probabiliste en appel par valeur avec un opérateur de disjonction parallèle. Les bisimulations applicatives sont cependant connues pour ne pas être applicables à des langages plus riches. Par conséquent, des notions plus robustes de bisimulation pour les calculs probabilistes sont considérées, sous la forme de bisimulations environnementales. Les bisimulations environnementales sont définies pour des λ-calculs probabilistes en appel par nom et en appel par valeur, et pour un λ-calcul probabiliste (en appel par valeur) avec références. Dans chaque cas, des résultats d'abstraction complets sont prouvés.
Type de document :
Thèse
Logic in Computer Science [cs.LO]. University of Bologna, 2017. English
Liste complète des métadonnées

Littérature citée [122 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01644462
Contributeur : Vignudelli Valeria <>
Soumis le : mercredi 22 novembre 2017 - 12:13:38
Dernière modification le : mercredi 10 octobre 2018 - 10:09:59

Fichier

Vignudelli_Valeria_tesi.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : tel-01644462, version 1

Collections

Citation

Valeria Vignudelli. Behavioral Equivalences for Higher-Order Languages with Probabilities. Logic in Computer Science [cs.LO]. University of Bologna, 2017. English. 〈tel-01644462〉

Partager

Métriques

Consultations de la notice

385

Téléchargements de fichiers

82