Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances (Extended Version)

TL;DR

This paper develops a framework for quantitative behavioural reasoning in higher-order effectful programs, extending applicative similarity and bisimilarity to a generalized metric setting using quantales.

Contribution

It introduces an abstract, quantale-based framework for analyzing behavioural relations in effectful lambda calculus, generalizing existing notions to a metric setting.

Findings

Defined a general framework for quantale-valued relations.

Proved applicative similarity and bisimilarity are compatible metrics.

Extended concepts of relators to quantale-valued relations.

Abstract

This paper studies the quantitative refinements of Abramsky's applicative similarity and bisimilarity in the context of a generalisation of Fuzz, a call-by-value $\lambda$-calculus with a linear type system that can express programs sensitivity, enriched with algebraic operations \emph{\`a la} Plotkin and Power. To do so a general, abstract framework for studying behavioural relations taking values over quantales is defined according to Lawvere's analysis of generalised metric spaces. Barr's notion of relator (or lax extension) is then extended to quantale-valued relations adapting and extending results from the field of monoidal topology. Abstract notions of quantale-valued effectful applicative similarity and bisimilarity are then defined and proved to be a compatible generalised metric (in the sense of Lawvere) and pseudometric, respectively, under mild conditions.