Abstract Lipschitz Continuity: Combining Semantic and Quantitative Approximations

Abstract

We introduce Abstract Lipschitz Continuity (ALC), an extensional (i.e., input/output) property that ensures proportionally bounded differences in the semantic approximations of the output of a function (e.g., a program semantics) when the semantic approximations of the input differ slightly. ALC explicitly discerns between two complementary notions of approximation: quantitative differences, expressed via pre-metrics, and qualitative (or semantic) differences, captured through upper closure operators. This explicit separation of approximations has two main advantages. First, it enables ALC to be related to other important extensional program properties, including partial abstract non-interference in language-based security, partial completeness in abstract interpretation, and abstract robustness in machine learning. Second, ALC enables reasoning about its validity for programs through inductive reasoning on their syntax and on the chosen semantic abstractions. To this end, we propose a sound deductive system, parameterized by the quantitative and semantic approximations of interest, for proving ALC of programs. This proof system makes explicit the assumptions required for ALC, thereby ensuring a compositional proof approach.

Date