AfterMath

PhD Thesis

On operational properties of quantitative extensions of λ-calculus

I defended my dissertation on December 5th, 2014 at Aix-Marseille Université.

The members of the committee were:

• Simona Ronchi Della Rocca (President)
• Paul B. Levy (Examiner)
• Michele Pagani (Examiner)
• Laurent Regnier (Advisor)
• Simone Martini (Advisor)

along with the following invited members:

• Emmanuel Beffara
• Lionel Vaux
• Ugo Dal Lago

Abstract:

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.

Documents: Manuscript and Slides.