Raphaëlle Crubillé (Univ. Paris 7 & Univ. Bologna), Metrics Reasoning about lambda-terms



Terms of Church's lambda-calculus can be considered equivalent along many different definitions, but context equivalence is certainly the most direct and universally accepted one. However, this definition has the drawback of being based on an universal quantification over all contexts. In order to give handier characterisations, coinductive methodologies have been developped since 1990 by Abramsky (among others) for deterministic computations, and later by Lassen for non-deterministic ones, with new and exciting results appearing recently also for probabilistic languages: applicative bisimilarity, a coinductively defined notion of equivalence for functional programs, has been shown to be sound, and sometime even fully abstract, for probabilistic lambda-calculi. In the probabilistic case, however, equivalence can be seen as too discriminating: terms which have totally unrelated behaviours are treated the same as terms which behave very similarly. We study the problem of evaluating the distance between lambda-terms. A natural generalisation of context equivalence, is shown to be characterised in a restricted affine setting by a notion of trace distance, and to be bounded from above by a coinductively defined distance based on the Kantorovich metric on distributions. A different, again fully-abstract, tuple-based notion of trace distance is shown to be able to handle nontrivial examples, and to allow a generalisation to the non-affine case.