Abstract Lipschitz Continuity

Introduction

• Concrete-value distances can obscure which data properties matter, such as ignoring byte order while tracking a file’s pattern count.The examples motivate comparing properties such as Boolean-operator counts, selected tuples, and coarsened pattern-count intervals rather than raw inputs and outputs.Source: Introduction · pp. 2–3
• ALC bounds distances between output properties by a constant times the distance between input properties, keeping property-based and quantitative approximations explicit.Property-based approximations are modeled by upper closure operators; quantitative approximations use pre-metrics, which need not be symmetric or satisfy the triangle inequality.Source: Introduction · p. 3
• ALC is sufficient for partial completeness and partial abstract non-interference, and with a null constant it implies abstract robustness, generally more strongly.For partial completeness and non-interference, the introduction also describes implications under differing abstractions and conditions for exact counterparts.Source: Introduction · pp. 3–4
• A sound deductive system proves program ALC from basic-command proofs and side conditions for sequential composition, nondeterministic choice, and iteration.The conditions address compatibility between consecutive abstractions, bounds on how joins affect output distance, and continuity or iteration-count bounds.Source: Introduction · p. 4
• This extended version adds results for differing input abstractions and shows that 0-ALC is equivalent to robustness required for every perturbation radius.For a fixed radius, 0-ALC is generally strictly stronger than abstract robustness.Source: Introduction · p. 5

1. Background

• The background separates approximations into property-based abstractions and quantitative distances, which can be combined into a general approximation.The property-based form uses upper closure operators, while the quantitative form uses pre-metrics.Source: §1 · p. 5, §1.2 · p. 7

1.1. Program Syntax and Semantics.

• Programs use basic commands, sequential composition, nondeterministic choice, and Kleene closure, with semantics defined inductively over program syntax.The language is described as general enough for deterministic imperative languages and nondeterministic computations.Source: §1.1 · pp. 5–6

1.2. Abstractions and Distances.

• A Galois connection links concrete and abstract domains through monotone abstraction and concretization functions; the framework is used in abstract interpretation.Abstract interpretation evaluates functions over an abstract domain instead of the concrete domain when exact analysis is infeasible or undecidable.Source: §1.2 · p. 7

A GC is a GI when α ◦γ = id, namely when composing the abstraction function with the concretization gives rise to the identity function id

• The paper focuses on Galois insertions (GIs), equivalently formulated in terms of upper closure operators; separately, Int maps each non-empty integer set S to [inf S, sup S], with extrema in Z ∪ {−∞, +∞}.For example, {0, 1, 4} is approximated by [0, 4].Source: A GC is a GI when α ◦γ = id, namely… · pp. 7–8

1.2.1. Property-based Approximations via Upper Closure Operators.

• An upper closure operator models a property-based approximation, grouping concrete elements that share the same property under the operator.The sign closure, for example, records whether a set contains negative, zero, or positive integers.Source: A GC is a GI when α ◦γ = id, namely… · p. 8

1.2.2. Quantitative Approximations via Pre-Metrics.

• Pre-metrics require only that each element have distance zero from itself, allowing distances that lack symmetry or the triangle inequality.Examples include size distance for set cardinalities and directed path length for steps upward in a poset.Source: §1.2.2 · pp. 9–11

1.2.3. Combining Property-based and Quantitative Approximations.

• Combining an abstraction with a distance yields approximations that satisfy both a property abstraction and a quantitative error bound.The bound is applied using δρ, the distance between abstracted values.Source: §1.2.3 · p. 12
• The combined distance δρ measures distance between property abstractions, preserving some distance axioms but losing identity-of-indiscernibles when ρ is not the identity.It is a pseudo-metric when the original distance is a metric or pseudo-metric, and a pre-metric when the original is a quasisemi-metric.Source: §1.2.3 · pp. 12–13

2. Abstract Lipschitz Continuity

• Unlike classical Lipschitz continuity, ALC permits distinct input and output pre-metrics, which need not be symmetric or satisfy the triangle inequality.Classical Lipschitz continuity bounds output perturbations linearly by input perturbations.Source: §2 · pp. 13–14
• Pre-metrics induce topologies, but metric-dependent results such as Banach’s fixed point theorem are not generally available.In these topologies, balls need not be open and limits need not be unique.Source: §2 · p. 14
• ALC bounds output approximation distance by k times input approximation distance, combining property-based upper closure operators with quantitative pre-metrics.When k = 0, finite input approximations must map to outputs at distance 0.Source: §2 · p. 15
• For byte histograms with width-w count intervals, the count-a semantics satisfies w-ALC under edit-based input distance and the interval output abstraction.A single edit changes the count by at most 1, while reordering bytes leaves it unchanged; the factor w is necessary.Source: §2 · p. 16
• The byte-count example shows that file length alone is an unsuitable input abstraction because equal-length files can have different observed counts.The files “a”^w and “b”^w have the same length but counts w and 0, yielding positive output distance despite zero input distance under a length-only abstraction.Source: §2 · p. 16
• The program R semantics satisfies 1-ALC with interval abstraction and inclusion distance, but not with the size abstraction.The size abstraction assigns distance 0 to {5} and {−5}, although their outputs have positive size distance.Source: §2 · pp. 16–17

3. ALC as a Sufficient Condition: Partial Completeness, Partial Abstract Non-Interference and Abstract Robustness

• With the same abstractions, ALC implies partial completeness and partial abstract non-interference for every threshold, regardless of its constant; 0-ALC implies abstract robustness, but is strictly stronger for a fixed radius.Under mild distance assumptions, ALC also implies exact completeness and abstract non-interference.Source: §3 · p. 17

3.1. Partial Completeness.

• When the ALC input abstraction and output abstraction coincide, ALC makes the best correct approximation ε-partially complete for every ε; a quasisemi-metric further guarantees completeness.The result applies to monotone functions and uses the same abstraction for ALC and the best correct approximation.Source: §3.1 · p. 19
• With different input abstractions, the best correct approximation is kε-partially complete, where ε bounds the input-abstraction distance measured through the abstraction used for ALC.If the analysis abstraction is more precise than the ALC abstraction, the bound becomes zero, yielding partial completeness for any threshold.Source: §3.1 · pp. 21–22
• The distinct-abstraction result guarantees 2-partial completeness for the parity analysis of the example, although ALC cannot be established directly with respect to parity.The guarantee follows by establishing ALC with respect to signs instead.Source: §3.1 · p. 21

3.2. Partial Abstract Non-Interference.

• ALC implies 0-partial abstract non-interference for any Lipschitz constant; if the output distance is a quasisemi-metric, it also implies exact abstract non-interference.The result follows from ALC with the relevant input and output abstractions and pre-metrics.Source: §3.2 · pp. 22–23
• If f satisfies k-ALC under one input abstraction, Theorem 3.14 gives 2kε-PANI under a policy abstraction, using distinct input distances for the two guarantees.The ALC distance measures the error from replacing each input with its policy abstraction; the PANI distance identifies which inputs must be indistinguishable.Source: §3.2 · p. 23
• For the collecting semantics, the parity abstraction yields a 4-PANI bound, but the actual guarantee is 1-PANI and not 0-PANI.Inputs with the same parity can produce outputs with different signs, attaining output distance 1.Source: §3.2 · p. 24
• When the policy abstraction is more precise than the ALC input abstraction, the PANI bound is zero; inputs with the same interval yield outputs with the same sign in the example.The collecting semantics satisfies 0-PANI under the interval policy abstraction and sign output abstraction.Source: §3.2 · pp. 24–25

3.3. Abstract Robustness.

• With a quasisemi-metric output distance, 0-ALC suffices for abstract robustness at any fixed radius; for positive radii, k-ALC with k > 0 need not suffice.Abstract robustness requires the abstract output classification to remain unchanged across inputs within the perturbation radius.Source: §3.3 · pp. 25–26
• For a fixed radius, abstract robustness does not imply 0-ALC, but robustness for every radius is equivalent to 0-ALC.ALC generalizes robustness by allowing output effects that are linearly bounded by input error.Source: §3.3 · pp. 26–27

4. Proving ALC for Programs

• Basic-command proofs are supplied separately, while weakening trades broader input or output abstractions for a larger ALC constant.For skip, 1 ⊢[δρ] skip [δρ] is always derivable; input and output weakening can be applied independently.Source: §4 · p. 29
• Sequential composition requires compatible intermediate abstractions: if δη ≤ tδρ, the composed constant is k1tk2; when η = ρ, t = 1.Without a useful comparison between abstractions, the side condition can use t = ∞, yielding an uninformative bound.Source: §4 · p. 30
• Non-deterministic choice requires an ⊕-bound for the output distance, including subadditivity over joins, to combine the branches’ constants soundly.For additive abstractions with path-length distance, + is an ⊕-bound; this includes the inclusion distance on ℘(L).Source: §4 · p. 30
• Iteration combines bounds for finite iterates and their joins; bounded iteration needs a finite step bound, while unbounded iteration also requires an ω-continuous output distance.The rules use abstraction-compatibility conditions and an ⊕-bound; inclusion distance on ℘(L) and its induced path-length distance are ω-continuous.Source: §4 · pp. 31–32
• For finite k and t, + yields K∞ = v + k/(1−kt) when kt < 1 and ∞ when kt ≥ 1 and k > 0; max yields max(v, k) when kt ≤ 1 and ∞ when kt > 1.With either bound, a non-expansive body (kt ≤ 1) is what makes iteration informative.Source: §4 · p. 31
• Every derivable judgment is sound for the program semantics, though the system is incomplete and may yield a constant larger than the least ALC constant.Allowing k = ∞ ensures the system can always give a sound, potentially uninformative judgment.Source: §4 · pp. 27, 28, 32

Join

• The ReLU example’s join rule overestimates its least constant because it adds branch constants despite the branches depending on disjoint input blocks.The semantics is actually 1-ALC: each additional input block can affect at most one branch, a fact the uniform sum bound cannot exploit.Source: §4 · p. 35

Example 4.12 (Iterated Scaling)

• The derived abstract Lipschitz constant is least, with the example distance exactly 1; using + remains sound but yields the non-optimal geometric-series constant 4/3.The (bound-star) rule is not applicable because no m ∈ N satisfies ∗-Bound(S∗, m).Source: §4 · p. 36

Composition side conditions

• The suitable ⊕-bound depends on the distance: + fits distances counting elements or blocks, while max gives the least constant for iterated scaling’s Hausdorff distance.For the sign path distance, max is not an ⊕-bound; for interval Hausdorff distance, both max and + are bounds, but + gives the larger scaling-closure constant.Source: §4 · pp. 36–37

Example 4.13 (Bounded Iteration)

• For bounded iteration, N* satisfies *-Bound(N*, 1), whereas the star rule yields an uninformative infinite constant.A second application of N produces the empty set, so N* S = S ∪ N S; max is not an ⊕-bound for the sign path distance because joined sets can add blocks.Source: §4 · p. 37

Identity abstractions

• With identity abstractions, the deductive system becomes a proof system for ordinary Lipschitz continuity, but distance conditions for choice and iteration remain necessary.The abstraction side conditions become trivial, while ⊕-Bound, ω-Cont, and a finite iteration bound are still required.Source: §4 · p. 37

• ALC makes output-property distances at most k times input-property distances, with distances tailored to the abstract domain rather than necessarily being metrics.This lets property-preserving changes, such as reordering file bytes, count as no perturbation.Source: §5 · pp. 37–38
• ALC implies partial completeness and partial abstract non-interference under stated distance conditions, and 0-ALC implies abstract robustness of classifiers for any perturbation radius.For partial completeness, suitable distances must be ⪯-compatible and satisfy (iff-identity); with different input abstractions, guarantees may carry imprecision proportional to k.Source: §5 · p. 38
• The language considered uses deterministic assignments; extending the system to probabilistic choice requires a suitable rule and meaningful abstractions of distributions.The authors expect the join rule to carry over with a suitable bound, but identifying distribution abstractions remains open.Source: §5 · p. 38
• ALC is global over all inputs; formalizing a local version and determining whether it can be established on canonical generators remain open questions.Dropping universal quantification may invalidate the established correlations, and reasoning locally would require assumptions about inputs reaching each program point.Source: §5 · p. 38
• The paper leaves open whether ALC-related correspondences extend to weak closures or α-relations and to other quantitative program properties.These weaker abstraction notions can represent properties without a best abstraction function.Source: §5 · pp. 38–39
• Modeling differential privacy within ALC, including privacy accounting for input/output abstractions, is left for future work.The authors note that incorporating abstractions into a distance metric on probability spaces is not immediate.Source: §5 · p. 39
• Compositional reasoning for non-deterministic choice and iteration depends on an ⊕-bound and ω-continuity; the needed ⊕ operation varies with the distance.The paper proves these properties for inclusion and path-length distances with additive abstractions, while a general characterization remains future work.Source: §5 · p. 39
• The deductive system is sound, but not complete: it can derive a constant larger than the actual one or fail to derive any finite constant.Imprecision arises from base-command requirements, uniform ⊕-bounds for branches, and iteration rules that are informative only for non-expansive bodies or bounded iteration counts.Source: §5 · p. 39