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 · 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.
categories and subject descriptors f.3.2 [logics and meaning
of programs]: semantics of programming languages
keywords domain theory, program sensitivity, metric spaces, lipschitz continuity