Cette thèse porte sur les propriétés opérationnelles de deux extensions quantitatives du λ-calcul pur : le λ-calcul algébrique et le λ-calcul probabiliste.Dans la première partie, nous étudions la théorie de la β-réduction dans le λ-calcul algébrique. Ce calcul permet la formation de combinaisons linéaires finies de λ-termes. Bien que le système obtenu jouisse de la propriété de Church-Rosser, la relation de réduction devient triviale en présence de coefficients négatifs, ce qui la rend impropre à définir une notion de forme normale. Nous proposons une solution qui permet la définition d'une relation d'équivalence sur les termes, partielle mais cohérente. Nous introduisons une variante de la β-réduction, restreinte aux termes canoniques, dont nous montrons qu'elle caractérise en partie la notion de forme normale précédemment établie, démontrant au passage un théorème de factorisation.Dans la seconde partie, nous étudions la bisimulation et l'équivalence contextuelle dans un λ-calcul muni d'un choix probabliste. Nous donnons une technique pour établir que la bisimilarité applicative probabiliste est une congruence. Bien que notre méthode soit adaptée de celle de Howe, certains points techniques sont assez différents, et s'appuient sur des propriétés non triviales de « désintrication » sur les ensembles de nombres réels. Nous démontrons finalement que, bien que la bisimilarité soit en général strictement plus fine que l'équivalence contextuelle, elles coïncident sur les λ-termes purs. L'égalité correspondante est celle induite par les arbres de Lévy-Longo, généralement considérés comme l'équivalence extensionnelle la plus fine pour les λ-termes en évaluation paresseuse. / In this thesis we deal with the operational behaviours of two quantitative extensions of pure λ-calculus, namely the algebraic λ-calculus and the probabilistic λ-calculus.In the first part, we study the β-reduction theory of the algebraic λ-calculus, a calculus allowing formal finite linear combinations of λ-terms to be expressed. Although the system enjoys the Church-Rosser property, reduction collapses in presence of negative coefficients. We exhibit a solution to the consequent loss of the notion of (unique) normal form, allowing the definition of a partial, but consistent, term equivalence. We then introduce a variant of β-reduction defined on canonical terms only, which we show partially characterises the previously established notion of normal form. In the process, we prove a factorisation theorem.In the second part, we study bisimulation and context equivalence in a λ-calculus endowed with a probabilistic choice. We show a technique for proving congruence of probabilistic applicative bisimilarity. While the technique follows Howe's method, some of the technicalities are quite different, relying on non-trivial "disentangling" properties for sets of real numbers. Finally we show that, while bisimilarity is in general strictly finer than context equivalence, coincidence between the two relations is achieved on pure λ-terms. The resulting equality is that induced by Lévy-Longo trees, generally accepted as the finest extensional equivalence on pure λ-terms under a lazy regime.
| Identifer | oai:union.ndltd.org:theses.fr/2014AIXM4076 |
| Date | 05 December 2014 |
| Creators | Alberti, Michele |
| Contributors | Aix-Marseille, Università degli studi (Bologne, Italie). Facoltà di Ingegneria, Régnier, Laurent |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.0025 seconds