Abstract Lipschitz Continuity
Abstract
We introduce Abstract Lipschitz Continuity (ALC), a generalization of standard Lipschitz Continuity, that ensures proportionally bounded differences in the semantic approximations of outputs when the semantic approximations of inputs differ slightly. ALC distinguishes between two complementary notions of approximation: quantitative differences, expressed via pre-metrics, and qualitative (or semantic) differences, captured through upper closure operators. ALC allows for reasoning about bounded changes in output properties in settings where standard Lipschitz continuity is too restrictive or inapplicable, such as in program analysis and verification, where understanding semantic properties of inputs and outputs is of key importance.
In the specific context of programs, we formally relate ALC to other well-established program properties, including (Partial) Completeness and (Abstract) program Robustness. Notably, we show that ALC is a stronger requirement than Partial Completeness, a consolidated notion modeling precision loss in program analysis.
Finally, we propose a language- and domain-agnostic deductive system, parametric on the quantitative and semantic approximations of interest, for proving the ALC of programs. The goal in designing this deductive system is to track the assumptions required for ALC to ensure a compositional proof.