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]
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.
Document type :
Theses
Complete list of metadatas

Cited literature [83 references]  Display  Hide  Download

https://hal.inria.fr/tel-01096067
Contributor : Michele Alberti <>
Submitted on : Tuesday, December 16, 2014 - 4:51:33 PM
Last modification on : Saturday, January 27, 2018 - 1:31:00 AM
Long-term archiving on : Monday, March 23, 2015 - 2:27:47 PM

File

Identifiers

  • 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⟩

Share

Metrics

Record views

359

Files downloads

247