Francesco Gavazzo: An abstract account to behavioural equivalences and metrics for higher-order effectful language, part 2
[This is the second part of a two-part series of seminars.]
University of Bologna & Inria
Abstract: Behavioural equivalences for higher-order languages have been extensively studied in the last decades, often leading to rich and satisfactory theories. However, in presence of effectful computations behavioural equivalences can be too discriminating, as highlighted by probabilistic languages. An elegant way to avoid such problem is to move from behavioural equivalences to behavioural metrics.
Extending our previous work on effectful applicative bisimilarity, in this seminar we outline an abstract theory of behavioural 'distances' for higher-order effectful languages. In order to have a unified treatment of both behavioural equivalences and metrics, we follow Lawvere's work on generalized metric spaces and let distances take value in a quantale, which play the role of a set of abstract quantities. As we will see, a satisfactory treatment of behavioural distances cannot be done in ordinary functional languages, due to the lack of control on their 'copying-capabilities'. To avoid such problem we introduce a generalisation of Fuzz, a functional language with a linear type system that can express program sensitivity. Finally, we develop the relational and categorical apparatus based on Barr's theory of lax extensions, which will allow us to give abstract definitions of interesting behavioural metrics, viz. contextual and applicative bisimilarity metrics.
