A Semantic Account of Metric Preservation

TL;DR

This paper develops a denotational semantics framework using metric CPOs to analyze program sensitivity, extending the understanding of metric preservation in probabilistic and differential privacy contexts.

Contribution

It introduces metric CPOs as a new semantic structure for reasoning about program sensitivity and provides a model for the deterministic fragment of Fuzz.

Findings

Metric CPOs enable reasoning about metric properties of programs.

The model demonstrates how metric preservation can be understood denotationally.

Supports analysis of program robustness in privacy and cyber-physical systems.

Abstract

Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in terms of metrics on the input and output spaces, requiring that an $r$-sensitive function map inputs that are at distance $d$ to outputs that are at distance at most $r \cdot d$. Program sensitivity is thus an analogue of Lipschitz continuity for programs. Reed and Pierce introduced Fuzz, a functional language with a linear type system that can express program sensitivity. They show soundness operationally, in the form of a metric preservation property. Inspired by their work, we study program sensitivity and metric preservation from a denotational point of view. In particular, we introduce metric CPOs, a novel semantic structure for reasoning about computation on metric spaces, by endowing CPOs with a compatible notion of distance. This structure is useful for reasoning about metric properties of programs, and specifically about program sensitivity. We demonstrate metric CPOs by giving a model for the deterministic fragment of Fuzz.