Thomas Leventis
I2M, Aix-Marseille Université
/user/thomas.leventis/
Date(s) : 08/12/2016 iCal
14 h 00 min - 16 h 00 min
Soutenance de thèse–
Le lambda-calcul est un formalisation de la notion de calcul. Dans cette thèse nous nous intéresserons à certaines variantes non déterministes, et nous nous pencherons plus particulièrement sur le cas probabiliste.
L’étude du lambda-calcul probabiliste n’est pas nouvelle, mais les travaus précédents considéraient le comportement probabiliste comme un effet de bord. Notre objectif est de présenter ce calcul d’une manière plus équationnelle, en intégrant le comportement probabiliste à la réduction.
Tout d’abord nous définissons une sémantique opérationnelle déterministe et contextuelle pour le lambda-calcul probabiliste en appel par nom. Afin de traduire la signification de la somme nous définissons une équivalence synaxique dans notre calcul, dont nous démontrons qu’il ne déforme pas la réduction: considérer une réduction modulo équivalence revient à considérer simplement le résultat du calcul modulo équivalence. Nous prouvons également un résultat de standardisation.
Dans ce cadre nous définissons une notion de théorie équationnelle pour le lambda-calcul probabiliste. Nous étendons certaines notions usuelles, et en particulier celle de bon sens. Cette dernière se formalise facilement dans un cadre déterministe mais est bien plus complexe dans le cas probabiliste.
Pour finir nous prouvons une correspondance entre l’équivalence observationnelle, l’égalité des arbres de Böhm et la théorie cohérente sensée maximale. Nous définissons une notion d’arbres de Böhm probabilistes dont nous prouvons qu’elle forme un modèle. Nous démontrons ensuite un résultat de séparabilité disant que deux termes avec des arbres de Böhm distincts ne sont pas observationnellement équivalents.
Résumé en anglais :
The lambda-calculus is a way to formalize the notion of computation. In this thesis we will be interested in some of these variants introducing non deterministim, and we will focus mostly on a probabilistic calculus.
The probabilistic lambda-calculus has been studied for some time, but the probabilistic behaviour has always been treated as a side effect. Our purpose is to give a more equational representation of this calculus, by handling the probabilities inside the reduction rather than as a side effect.
To begin with we give a deterministic and contextual operational semantics for the call-by-name probabilistic lambda-calculus. To express the probabilistic behaviour of the sum we introduce a syntactic equivalence in our calculus, and we show it has little consequence on the calculus: reducing modulo equivalence amount to reducing and then looking at the result modulo equivalence. We also prove a standardization theorem.
Then using this operational semantics we define a notion of equational theories for the probabilistic lambda-calculus. We extend some usual notions to this setting, and in particular the sensibility of a theory. This notion is quite simple in a deterministic setting but becomes more complicated when we have a probabilistic computation.
Finally we prove a generalization of the equality between the observational equivalence, the Böhm tree equality and the maximal coherent sensible lambda-theory. We give a notion of probabilistic Böhm trees, and prove that this forms a model of the probabilistic lambda-calculus. Then we prove a separability result stating that two terms with different Böhm trees are separable, i.e. are not observationally equivalent.
–
Membres du jury :–
– Antonino SALIBRA, Université de Venise Ca’Foscari (Rapporteur)
– Delia KESNER, Université Paris Diderot (Examinateur)
– Ugo DAL LAGO, Université de Bologne (Examinateur)
– Michele PAGANI, Université Paris Diderot (Examinateur)
– Lionel VAUX, Aix-Marseille Université (Directeur de thèse)
– Laurent REGNIER, Aix-Marseille Université (Co-directeur de thèse)
–
–
Lien : theses.fr
Catégories