Lambda the Ultimate

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.

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), lim_{y->x from left}f(y), and lim_{y->x from right}f(y).

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

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

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

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.

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

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.

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.

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 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 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 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.

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 '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?

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 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.

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 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.

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.

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 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 if exact comparisons aren't computable then the numbers themselves aren't computable?

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.

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 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.

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 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 an ordered field.

Why not?

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.

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.

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 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 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.