## Continuity Analysis of Programs

Continuity Analysis of Programs, Swarat Chaudhuri, Sumit Galwani, and Roberto Lublinerman. POPL 2010.

We present an analysis to automatically determine if a program represents a continuous function, or equivalently, if infinitesimal changes to its inputs can only cause infinitesimal changes to its outputs. The analysis can be used to verify the robustness of programs whose inputs can have small amounts of error and uncertainty -- e.g., embedded controllers processing slightly unreliable sensor data, or handheld devices using slightly stale satellite data.

Continuity is a fundamental notion in mathematics. However, it is difficult to apply continuity proofs from real analysis to functions that are coded as imperative programs, especially when they use diverse data types and features such as assignments, branches, and loops. We associate data types with metric spaces as opposed to just sets of values, and continuity of typed programs is phrased in terms of these spaces. Our analysis reduces questions about continuity to verification conditions that do not refer to infinitesimal changes and can be discharged using off-the-shelf SMT solvers. Challenges arise in proving continuity of programs with branches and loops, as a small perturbation in the value of a variable often leads to divergent control-flow that can lead to large changes in values of variables. Our proof rules identify appropriate â€œsynchronization pointsâ€ between executions and their perturbed counterparts, and establish that values of certain variables converge back to the original results in spite of temporary divergence.

We prove our analysis sound with respect to the traditional epsilon-delta definition of continuity. We demonstrate the precision of our analysis by applying it to a range of classic algorithms, including algorithms for array sorting, shortest paths in graphs, minimum spanning trees, and combinatorial optimization. A prototype implementation based on the Z3 SMT-solver is also presented.

Another fun paper from POPL this year. I've seen metric spaces used to solve domain equations before, but the idea of actually considering a metric on the outputs was a new one to me.

## Comment viewing options

Cool!

### Mutation testing

I wonder if this will combine nicely with mutation testing (to empirically check if real code is continuous, and identify changes that break continuity). Also: This suggest an intriguing approach to anomaly detection.

### I was a little surprised

I was a little surprised that they didn't discuss the connection to automatic differentiation literature..

### Result

The quoted abstract makes it sound like they have a decision procedure for continuity. I won't have time to look at the paper until next week, but anyone know if that's indeed what they're claiming?

### Semi-Decision

From the paper:

In the next few sections, we present our solution to this problem. Our rules are sound. While we do not claim completeness, we offer an empirical substitute: nearly-automatic continuity proofs for 11 classic algorithms, most of them picked from a standard undergraduate textbook.

Neel was at POPL: who else?

What were the highlights?

### Aren't all computable functions continuous?

I thought it was the case that all computable functions from â„ to â„ are continuous, since computing such a function to arbitrary precision at a point of discontinuity requires infinite precision in its input.

So I'm unclear on what this paper is trying to do. Does their analysis even operate on programs in 'exact', i.e. arbitrary-precision real arithmetic?

### Not at all!

A simple discontinuous function would be:

 f(x) =
1 if x > 0
0 otherwise

This is defined and computable for all real numbers; however, it is not 'continuous'.

A continuous function will have, for all arguments x, the same values for f(x), limy->x from leftf(y), and limy->x from rightf(y).

### Not totally computable

f(0) diverges, never able to establish that x is negative or positive.

### No.

f(0) is 0, by the above definition. 0 is not > 0, after all.

### I guess you have rather

I guess you have rather something like sin(1/x) in mind which has no limit for x->0.

### Not that complicated

I just meant that testing for strict positivity cannot be done, since you'd need to inspect every digit of x - the same point vrijz re-emphasized in a sibling post.

### RE: 'inspect every digit'

So you're saying the function is not computable because you've chosen a divergent representation (one with infinite Kolmogorov complexity) for the argument?

### Not really

Your predicate (x > 0) is not computable by inspecting a finite approximation of x, since that finite approximation might be 0.0000... and you wouldn't be able to decide whether x > 0 or not.

### Irrelevant.

The above function is undeniably defined on all real numbers, and it is computable on all computable real numbers. That an input to the function may be divergent (or might not even be a real number, such as having an error range) really isn't a problem, but even if it were: it certainly isn't my problem.

The continuity analysis defined in the OP is about stability of a function in the face of approximations and errors. Continuity, not computability, is the feature for which you're looking.

### RE: computable on all computable real numbers

This seems to be the heart of the matter. Why do you think x>0 is computable for a computable real x? What definition of computable real are you using?

I agree that the original post probably has something other than the usual definition of "computable real" in mind. I'm guessing they just assume that can they perform comparison operations between reals, so that their results say something about the continuity of the functions your floating point code is approximating, but I haven't read the paper yet. What their setup involves was exactly the question asked by vrijz.

### This seems to be the heart

This seems to be the heart of the matter. Why do you think x>0 is computable for a computable real x? What definition of computable real are you using?

I'd say a computable real number has a complete representation that takes finite space and that allows all basic real number operations in finite time. Note: said representation may be algorithmic, allowing representation of a great many irrational and even transcendental numbers be computable.

By 'complete representation' I'm demanding something stronger than a common definition of 'computable numbers' (which tend to demand only a finite arbitrary-precision approximation of the number be represented in finite space and time). All 'approximations' are, by nature, computable numbers; but approximations are generally not the number being approximated.

Since real numbers are a complete ordered field, the 'basic real operations' must include at least addition, multiplication, and ordinal comparison.

Thus, any input for which I cannot compare against 0 for order... is not a computable real number.

### Thus, any input for which I

Thus, any input for which I cannot compare against 0 and receive an upper and lower bound... is not a computable real number.

I don't know what that means. The answer when you compare to 0 is either true or false. What kind of bound do you have in mind?

What if we take X to be the number whose Nth binary digit right of the decimal is either 0, if Goldbach's conjecture holds for N, or 1 otherwise. This is a computable real by the usual definition. Does it satisfy the "allows all basic real number operations in finite time" clause of your definition? (And if so, how do you compare it to 0?)

### I've reworded the above to

I've reworded the above to avoid unnecessary points of confusion.

Your example X is undecided. That is, we do not know of any finite and complete representation for it that will allow basic real operations - including ordinal comparison against 0. There may be a computable representation for X (quite possibly, X = 0), but we don't know of one at the moment.

The outcome of the above function f applied to X would, similarly, be undecided.

### So what are these computable reals?

That is, we do not know of any finite and complete representation for it that will allow basic real operations - including ordinal comparison against 0.

I'm not going to argue against a tautology (at least not on purpose). If your definition of computable real number includes the clause "comparable to other computable real numbers", then clearly your original counterexample is computable.

But your definition of "computable real number" doesn't define a particular subset of reals like the usual definition does. It just defines a set of conditions that you want to hold true for some imagined set of computable reals. The rationals, for example, satisfy your closure requirement. Do you have a particular set in mind?

### Even the formal definition

Even the formal 'usual' definition of computable number depends upon discovering an algorithm (computable function) that meets certain conditions (such as outputting an arbitrary count of digits then terminating).

What this means is that the set of 'computable numbers' is constructive in nature: for any known computable number, you can demonstrate that said number is in the set. But if no such demonstration exists, you can only say that you haven't decided whether it's in the set of computable numbers. Computable numbers themselves have always been a semi-decision.

That said, computable numbers are closed - in the sense that adding or multiplying computable numbers can only ever result in a new computable number. This is easy enough to demonstrate by inductive proof, and it remains true for the stronger definition of 'computable number' that I'm using.

Which "particular subset of the reals" are you imagining the "usual definition" excludes? Perhaps I should ask: which definition of 'computable number' are you intending to apply?

### Impredicitivity

I agree Wikipedia's definition is the usual one and the one I intend. It defines a real number to be computable if epsilon-bounds can be computed for any positive epsilon. With this definition in mind, we can note that the set of such numbers is closed under [+,-,*,/], and provide a construction to perform these operations. For emphasis: being closed under these operations is not part of the definition of computable.

It doesn't even really make sense to tack on "and any two computable numbers shall be comparable" because it makes the computability of one real depend on what other reals are computable.

### For emphasis: being closed

For emphasis: being closed under these operations is not part of the definition of computable.

For the formal definition of computable numbers in Wikipedia, one may prove closure. (That is, given computable numbers represented by computable functions f and g, there is a computable number f+g and f*g, though these may need to use smaller epsilons on f and g individually.)

It doesn't even really make sense to tack on "and any two computable numbers shall be comparable" because it makes the computability of one real depend on what other reals are computable.

You could say something similar of NP (from P vs. NP).

In any case, you cannot truly claim that computable numbers are real numbers if they lack the properties of real numbers. Computable numbers are not an ordered field. That is, computable numbers under the usual definition are not a correct model of real numbers.

By 'computable real numbers' I mean 'a subset of computable numbers that properly model real numbers'. This is a stronger definition; in the above computable functions, it would require comparisons based on limits as the epsilon approaches zero. It may turn out - as you are suggesting, and akin to P vs. NP - that not all classes of computable functions representing computable real numbers are provably in the same set.

### I'm not sure

In any case, you cannot truly claim that computable numbers are real numbers if they lack the properties of real numbers. Computable numbers are not an ordered field. That is, computable numbers under the usual definition are not a correct model of real numbers.

What if they have the properties of real numbers, but not all of those properties are themselves computable?

### Even of integers one cannot

Even of integers one cannot argue all properties are computable (nor decidable).

The basic properties for real numbers - those that make it an ordered field (specifically: ordinal comparisons, addition, and multiplication) must each compute in finite time, and the numbers must represent within finite space.

### Properties of reals

There are lots of ordered fields - the rationals are an ordered field. The reals are a complete ordered field and it is a theorem that the reals are the only complete ordered field. Completeness (equivalent in an ordered set to the property that every bounded set has a least upper bound), lets you take limits, which is what the reals are useful for. Computable reals capture the ability to take limits, but as a consequence leave comparison undecidable.

### Not the only complete ordered field

The reals are a complete ordered field and it is a theorem that the reals are the only complete ordered field.

This is a common misconception. One can impose an order on the field of rational functions over the real numbers, in more or less the obvious fashion (the indeterminate is declared greater than any real number, and everything else follows from the axioms); the result is itself a complete ordered field. Perhaps what you meant is that the real field is universally repelling in the obvious category?

(Postscript: I should have advanced some argument for why this new field isn't really the real field in disguise. Notice that it contains a bounded subfield (namely, the real subfield, bounded above by the indeterminate (hence also bounded below, since it's closed under additive inversion), whereas the real field does not.)

### My mistake

My mistake was in my mis-recollection that completeness was equivalent to the least upper bound property for totally ordered fields, which is not true if infinitesimals are around. Thanks :)

### Exactly, so why insist that

Exactly, so why insist that if exact comparisons aren't computable then the numbers themselves aren't computable?

### If they aren't comparable

Then they aren't real numbers at all (nor even a proper subset, like rationals or integers). They're some other sort of number - sometimes called 'computable numbers'. You need a different math, different model, different axioms, different theorems for them.

So I wasn't saying they aren't computable numbers. I was saying they aren't computable real numbers.

### No implementation has every desireable property

I would challenge you to come up with an implementation plan for computable reals that supports +, -, *, /, and comparison as well as exponentiation of positive reals. Once you get that going we'll talk about adding trig functions :)

### I agree: no known

I agree: no known implementation has every desirable property. (Doesn't mean there isn't one to be found, sitting in that space of enumerated Turing machines.)

But, really, you certainly can't complain about which properties you do need. My function required ordinal comparison. To start by assuming an 'implementation' that lacks ordinal comparison was counterproductive, just as much as would be assuming an implementation that lacks addition to complain that 'a+b' is computable.

I haven't worked on modeling real numbers since University. But, were I to aim for it today, I'd return to taking notes from Observational Equality, Now! to experiment with what can be done with total functions under observational constraints.

### The original

To start by assuming an 'implementation' that lacks ordinal comparison was counterproductive

I didn't make assumptions about context from your post, though - I mostly got the context from the post of vrijz to which you replied. It took me several posts to figure out where we weren't on the same page.

Also, I think it's easy enough to show that no implementation has every desirable property: given any Turing machine, form a binary digit string with a 0 in Nth position iff the machine hasn't halted after N steps. This digit string represents a real number, and that number equals 0 iff the machine doesn't halt.

### Also, I think it's easy

Also, I think it's easy enough to show that no implementation has every desirable property...

If you're going to vote the halting problem into the realnums as 'desirable', I'd honestly much rather have a machine that gives realnums based on winning lottery numbers (or future stock prices)... that's even more 'desirable'...

### Computable numbers are not

Computable numbers are not an ordered field.

Why not?

### Observational Inequality

I'm assuming a constructive logic.

To demonstrate a field is ordered requires providing a total-ordering function meeting certain requirements. Computable numbers are known when you express the appropriate computable function - a different function for each number.

Unfortunately, different expressions may result in the same computable function. Thus, constructing a total-ordering function for known computable numbers would require determining observational equality of arbitrary expressions for computable functions.

That is strictly more challenging than the halting problem. No such total-ordering function can be constructed, not even in theory.

Therefore, computable numbers cannot be an ordered field.

### Confusion of decidability with truth?

That there is no decidable procedure for comparing two computable real numbers is not the same as saying that they are incomparable. I am perfectly willing to buy that the computable numbers do not form a ‘computably ordered field’, or whatever, but I don't see how your argument shows that they do not form an ordered field, full stop.

On the other hand, you are quite right to point out that I was sweeping under the rug an appropriate choice of equivalence relation. Maybe one gets some other field, or maybe not a field at all, without this equivalence relation.

### Constructive Logic

That there is no decidable procedure for comparing two computable real numbers is not the same as saying that they are incomparable.

It is the same as saying they're in general incomparable. And since one needs a total ordering on those comparisons, a semi-decision that can compare some numbers is insufficient. A total ordering requires general comparisons.

What means "Truth" is determined by a choice of logic, not anything else. If you reject the shackles of constructive logics, you might have some different conclusions about how decidability intersects truth.

### It is the same as saying

It is the same as saying they're in general incomparable.

I'm not arguing with the consequent (although I think it's not true), only with the reasoning. The fact that a problem is not decidable just means that there is no program to decide it, not that it is somehow outside truth; that the halting problem is undecidable doesn't change the fact that all programs do, or do not, halt.

What means "Truth" is determined by a choice of logic, not anything else.

I think that this is not true. Truth is determined by axioms; provability is determined by the choice of logic.

### Truth is determined by

Truth is determined by axioms; provability is determined by the choice of logic.

When I said "What means 'Truth'", I was speaking literally: the semantics of concluding 'True' for an expression is determined entirely by the logic. Fuzzy logics, probabilistic logics, heuristic logics, modal logics, etc. - each associate a different semantics with an assertion of Truth. Constructive logics are no different in this sense.

In constructive logics, the assertion 'P' means 'P is provable' or (even more strictly) 'P has been proven'. Truth of an expression, and provability of said expression, are nearly identical.

Axioms do not determine Truth, much less do they determine what means 'Truth'. They are simply accepted (without further proof) as 'True', with whatever semantics 'True' has in the logic.

The fact that a problem is not decidable just means that there is no program to decide it, not that it is somehow outside truth; that the halting problem is undecidable doesn't change the fact that all programs do, or do not, halt.

And I suppose you're attempting to say that: "just because there is no function to compare them does not mean computable numbers are not totally ordered". Sure, in some non-constructive sense one might say that - in theory - computable numbers are ordered. But that doesn't change the fact that one can't provide a function to compare them, and therefore they are not an ordered field by at least one definition: "A field (F,+,*) together with a total order â‰¤ on F is an ordered field if the order satisfies [elided] properties." If you can't give me a total order function, you can't give me an ordered field.

### A very old idea...

...apparently not pursued. The more I read the works of the "old masters", the more amazed I am over the number of early ideas on software that have yet to make it to the mainstream.

In EWD 648, entitled Why is software so expensive?'' An explanation to the hardware designer, Edsger Dijkstra wrote about the differences between hardware design issues and software design. A relevant portion of that paper (about 3/4 of the way through) states [emphasis mine]:

When, 25 years ago, a logic designer had cooked up a circuit, his next acts were to build and to try it, and if it did not work he would probe a few signals with his scope and adjust a capacitor. And when it worked he would subject the voltages from the power supply to 10 percent variations, adjust, etc., until he had a circuit that worked correctly over the whole range of conditions he was aiming at. He made a product of which he could "see that it worked over the whole range". Of course he did not try it for "all" points of the range, but that wasn't necessary, for very general continuity considerations made it evident that it was sufficient to test the circuit under a very limited number of conditions, together "covering" the whole range.

EWD 648 was written in late 1977 or early 1978 [my interpolation based on known dates of papers bracketing it in the EWD series], which makes his phrase, "25 years ago", even more striking to me.

I'm glad to see this idea re-emerge.