On operational properties of quantitative extensions of lambda-calculus

Date(s) : 05/12/2014
10 h 30 min - 12 h 00 min

Soutenance de thèse

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.

*Membres du jury :

– Simona Ronchi Della Rocca
– Paul Levy (rapporteur)
– Michele Pagani (rapporteur)
– Laurent Regnier (directeur de thèse)
– Simone Martini (co-directrice de thèse)
– Emmanuel Beffara
– Lionel Vaux
– Ugo Dal Lago

Lien : theses.fr


Retour en haut 

Secured By miniOrange