On operational properties of quantitative extensions of λ-calculus

Michele Alberti 1, 2, 3
3 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Résumé : 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.
Type de document :
Thèse
Mathematics [math]. Aix Marseille Université; Università di Bologna, 2014. English
Liste complète des métadonnées

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

https://hal.inria.fr/tel-01096067
Contributeur : Michele Alberti <>
Soumis le : mardi 16 décembre 2014 - 16:51:33
Dernière modification le : jeudi 18 janvier 2018 - 02:11:40
Document(s) archivé(s) le : lundi 23 mars 2015 - 14:27:47

Fichier

Identifiants

  • HAL Id : tel-01096067, version 1

Collections

Citation

Michele Alberti. On operational properties of quantitative extensions of λ-calculus. Mathematics [math]. Aix Marseille Université; Università di Bologna, 2014. English. 〈tel-01096067〉

Partager

Métriques

Consultations de la notice

261

Téléchargements de fichiers

172