Comments on A Neighborhood of Infinity: How can it possibly be that we can exhaustively se...

Anonymous, correct me if I'm wrong, but in a const...

2007-12-17T05:57:00.000-08:00

Anonymous, correct me if I'm wrong, but in a constructive setting shouldn't the argument of "search" be (the code of) a recursive function together with a constructive proof of its totality? Then, I guess, we can prove the termination of "search" in a constructive way, too.

Re: pure implementation of "search"

Oh, I m...

2007-12-17T02:31:00.000-08:00

Re: pure implementation of "search"

Oh, I must tie that knot on my too quick tongue. Thank you, Dan!

Anonymous. Can you suggests some books on the flav...

2007-12-16T08:30:00.000-08:00

Anonymous. Can you suggests some books on the flavour of mathematics you're espousing? It's very interesting.

Unfortunately, the pathological "A(N)" is not a va...

2007-12-14T16:11:00.000-08:00

Unfortunately, the pathological "A(N)" is not a vacuous statement: it states that the "search" program will terminate. It is more vicious than the Goodstein's theorem because it remains pathological in all coherent classical systems (the pathology arises because the Kolmogorov complexity of the predicates is not bounded). Moreover, the axiom system in which "not(A(0))", "not(A(1))", "not(A(2))", "not(A(3))"... and "there is N such that A(N)" are true is much more than a formal curiosity: it's a model of your axiomatic. That means it could be the true essence of the real world. Nobody can choose what is the real world and how it works. This is a valid instance of the real world: you coherently prove that "search" terminates in all cases and "search p" coherently loops with infinitely many p. It's even worse: it's validity is a consequence of your axiomatic, so you necessarily use it to describe the real world. This incongruity exists in all (big enough) classical systems, in all axiom systems you might believe in: there is no way to circumvent it... except being constructive.

There is no cult in constructions. Constructions are facts. Classical statements are beliefs. You can believe in a model, but it's not logic, the "good" model is beyond logic (it's not based on a recursive axiomatic), it's just a sweat dream (and we can prove that).

Anonymous,

Reminds me of Goodstein's theore...

2007-12-13T15:13:00.000-08:00

Anonymous,

Reminds me of Goodstein's theorem.

I think we're members of different mathematical cults.

In my cult, an axiom system in which "not(A(0))", "not(A(1))", "not(A(2))", "not(A(3))"... for all integers, and we can also prove "there is N such that A(N)" is an interesting curiosity, but not an axiom system I'd use to describe the real world.

:-)

> For any input, this program is guaranteed to ...

2007-12-13T06:03:00.000-08:00

> For any input, this program is guaranteed to terminate. For any input, there is a time t after which you will get a 'yes' or a 'no'.

Your proof says that "this program is guaranteed to terminate". It is provable, but is it true in the real world? Can you compute this t? In some metasystems of classical logic there is some decidable properties A(N) on integers such that: whe can prove "not(A(0))", "not(A(1))", "not(A(2))", "not(A(3))"... for all integers, and we can also prove "there is N such that A(N)", without incoherence. Despite the apparent contradiction, it's all coherent. Intuitively, we might chech the property A(N) for all integers to reach a contradiction, but no one can check an infinity of properties, even an eternal beeing, so we cannot reach a contradiction. Such a property A(N) is similar to the property "the program (search p) ends after N steps" with a well chosen p.

This kind of example is similar to the coherent system S, defined by Gödel, which says that "there is an incoherent subsystem of S". So the "search" program is not garanteed to terminate, but we can believe in its termination without fear of contradiction, even if it's false in the real world. We don't have such paradoxes with constructive proofs because each proof generates a witness of reality: if we can prove that "there is a N such that A(N)", then we can prove "A(N)" for some N. This property does not hold in classical systems (because of the König's lemma in the case of "seach").

> There is no difference between the "sear...

2007-12-12T15:40:00.000-08:00

> There is no difference between the "search" program and any looping program with an undecidable termination.

Not so. For any input, this program is guaranteed to terminate. For any input, there is a time t after which you will get a 'yes' or a 'no'. This is different from, say, doing a brute force search for a solution to Fermat's last equation. There is no time t at which such a loop would terminate and say "no solution". It can only answer "yes, here's a solution" or loop indefinitely. These are distinct classes of program.

It seems that the complexity of your "search" prog...

2007-12-12T14:49:00.000-08:00

It seems that the complexity of your "search" program is not computable because the proof of its termination is (necessarily) not constructive. The proof tells you that the program will stop but it can't tell you when it will stop. So you believe that the program will terminate in all cases but in some cases you would never see the end of its execution (even if you were an eternal beeing): each day you could think that the program will stop tomorrow. There is no difference between the "search" program and any looping program with an undecidable termination.

However, if the predicates eated by "search" are primitive recursive for example, then the complexity of "search" can probably be bounded by an Ackermann-like function (the predicates given as examples here are primitive recursive, although there is no stream in primitive recursion :o).

Anonymous,

See here for a pure implementati...

2007-12-07T08:03:00.000-08:00

Anonymous,

See here for a pure implementation: http://conway.rutgers.edu/~ccshan/wiki/blog/posts/Exhaustive/

It's interesting to note that one can't im...

2007-12-07T06:10:00.000-08:00

It's interesting to note that one can't implement "search" as a pure recursive function of the type "(Stream -> Bool) -> Bool". The problem is that its argument is a "black box", an opaque predicate. Although we know that the search tree (as described in the post) is finite, we don't know what it is and so we can't search it in finite time.

However, you can implement "search", if you allow side effects, e.g. using "unsafePerformIO". This is left as an exercise for the reader :)

I suspect that this "inevitability of impurity" is not accidental.

Fascinating stuff. And thanks for your explanatio...

2007-10-21T01:58:00.000-07:00

Fascinating stuff. And thanks for your explanation, I can't follow that paper.

I'm having a little trouble while exploring this problem more deeply. I "know" that there must not be a total function from infinite sequences of booleans onto the integers. I have devised this proof:

If there were, then we could construct a function from booleans into booleans answering the question "such and such Turing machine halts in n steps", and then we could use the algorithm you just presented to solve the halting problem.

But that doesn't give me any intuition for any deeper reasons. Could you explain a little more why there's no way to construct a total function from infinite sequences of booleans onto the integers?

Thanks,
Luke
http://luqui.org/blog

The trees were drawn with Inkscape. To misquote Ch...

2007-10-09T06:46:00.000-07:00

The trees were drawn with Inkscape. To misquote Chruchill, Inkscape is the worst free drawing application, apart from all the rest.

Thanks for the article, it was very informative. ...

2007-10-08T23:56:00.000-07:00

Thanks for the article, it was very informative. As an unrelated question, may I ask what program you used to produce those binary trees?

dthurston,

That's an epistemic "might".
...

2007-10-06T12:13:00.001-07:00

dthurston,

That's an epistemic "might".

Ie. "might" = "I do not yet know that it is impossible that" rather than "there exists an example such that".

You wrote:
But even though dp(s) is always f...

2007-10-06T12:02:00.000-07:00
You wrote:
But even though dp(s) is always finite, it might be unbounded as s varies over the infinite set of streams.

Although you come to the right conclusion in the end, what you wrote above is not true: in fact you end up proving that for a given predicate there is a definite depth that you don't need to look beyond.