Beefy Boxes and Bandwidth Generously Provided by pair Networks
Don't ask to ask, just ask

Re: Re: Re: Re-spect!: (OT) Where is programming headed?

by mstone (Deacon)
on Dec 17, 2001 at 03:14 UTC ( #132413=note: print w/replies, xml ) Need Help??

in reply to Re: Re: Re: (OT) Where is programming headed?
in thread (OT) Where is programming headed?

couldn't resist.. ;-)

> An axiom system is a series of postulates. An axiom system is
> consistent if it doesn't prove a contraction. That theorem states,
> quite precisely, No consistent finite first order axiom system which
> includes arithmetic can prove its own consistency.

I think we're coming at the problem from opposite directions, so you see an elephant facing left, and I see an elephant facing right.

I agree that no finite set of axioms including arithmetic can generate a system that's simulaneously correct (every statement the basis generates is guaranteed to be true) and complete (the basis is guaranteed to generate every true statement). AFAIK, that doesn't negate either the existence or utility of systems that do generate from finite bases, though.

I never stated a requirement of simultaneous completeness and correctness. I made a quick reference to evoke the concept of formal systems, and in retrospect, I guess I should have said 'Post systems'.

> When using technical terms around people who actually understand
> those terms, it is advisable to give them the usual meaning.

Okay, let's review some vocabulary:

An algorithm is a procedure that solves a problem. The solution it produces must be correct, and the procedure must halt in a finite amount of time.

If an algorithm can solve a problem in finite time, the problem is decidable. If no algorithm can solve the problem in finite time, the problem is undecidable.

A solvable problem is one that can be solved by a Turing machine. A problem that cannot be solved by a Turing machine is unsolvable. Every decidable problem is solvable. Every unsolvable problem is undecidable.

Please note that solvability carries no requirement of finite solution time, the way decidability does. We often use the terms interchangably, but there are times when it's useful to make the distinction between problems that can be solved in infinite time, and problems that can't.

If we say that the halting problem is solvable, it means every program that should halt will, and every program that shouldn't halt won't. That just restates our basic definition of halting, so it must be true. If we say that the halting problem is unsolvable, we admit the possiblity of programs that should halt but don't, and programs that shouldn't halt but do. That directly contradicts our definition of halting, so it must be false. If you reject solutions that take infinite time, you break the definition of halting.

> First of all theorem provers don't ever produce information that
> wasn't a logical consequence of the input. (At least they shouldn't.)
> While we may not have known that output, we do not get out anything
> truly independent of the input.

No arguments there..

> But we do get conclusions that we might not have come up with on our
> own.

Bingo! That's what I'm talking about. The interesting question is how much distance we can put between the specification and the product.

There's a qualitative difference between a program that can extrapolate code from a minimal basis, and a Microsoft wizard. The first explores an infinite generative system, and the second walks through a finite data structure that somebody else filled and ordered. The first can expand its code base on its own, while the second will always be handcuffed to whoever fills its lookup table. The first will produce code that's correct within the limits of its basis and generative capacity, while the second is is subject to all the size -v- implicit bug problems that plague any large body of code.

> Now you seem to be a great fan of the idea that someone somewhere
> will reduce this down to a few axioms. I rather strongly doubt this.

So do I. I just think it's a significant and interesting question.. as opposed to the brain-starved dribblings of a poser who should know better than to try and cut heads with his betters. ;-)

> This is a problem which is going to have many different solutions.
> The trick isn't in making up the missing bits of the specification,
> it is doing it in a way that comes up with answers the human thinks
> are reasonable. And there isn't a simple right answer to that.

And that's why I think we'll always need programmers, no matter how much of the specification can be generated by a program. ;-)


  • Comment on Re: Re: Re: Re-spect!: (OT) Where is programming headed?

Replies are listed 'Best First'.
Re (tilly) 4: Re-spect!: (OT) Where is programming headed?
by tilly (Archbishop) on Dec 17, 2001 at 05:15 UTC
    I find your distinction between solvability and decidability somewhat interesting. I have not heard the distinction drawn that way. It has been a few years since I last looked at a book on this subject (and I gave away most of my math books about 4 years ago, so I don't even have one to look this up in right now), but I would think I would have remembered something like that.

    So I did a quick Google search. And the funny thing is that I found lots of presentations online that disagreed with your proposed usage. I found none that agreed. For a random instance this lecture states directly that the Halting problem is not solvable.

    And even when I look at your links, they say nothing about finite versus infinite. The classification they draw goes like this. A decision problem is a problem whose answers are all yes/no. A decidable problem a decision problem that is solvable. Solvable problems differ from decision problems in that solvable problems are not just limited to yes/no answers.

    The fact that infinite answers are not accepted either for definitions of decidability or solvability is underscored by this lecture. They are very explicit about the fact that solvability and decidability both require that all of the computations involved halt. In other words you need to get an answer in due time.

    Now you wouldn't just be making up your finite/infinite distinction, would you? Do you have a verifiable source you are willing to quote showing that someone else out there agrees with the usage you are claiming?

      I think we're getting caught on the difference between defining a language, and proving that a given machine accepts a langauge by inspection. The former is axiomatic, and the latter is equivalent to the halting problem.

      More fundamentals:

      A Turing machine halts if it reaches either the accept or reject state for the given input.

      If a Turing machine reaches the accept state for a given input, we say that the machine has recognized or proved that input. If a machine rejects an input, we say that the machine has disproved that input.

      A total Turing machine halts for all possible input. Intuitively, a total Turing machine breaks breaks universe into two complementary sets: 'yes' and 'no'.

      A non-total Turing machine doesn't reach the accept or reject state for some input. It breaks the universe into three sets: 'yes', 'no', and 'damned if I know'.

      A language is the set of all strings that a Turing machine recognizes.

      A language is recursive if the machine that accepts it is total. Recursive languages are provable because the machine can prove or disprove the membership of any possible input.

      A language is recursively enumerable if the machine that accepts it is not total, i.e.: does not reach either the accept or reject state for every possible input.

      Now, it's axiomatic that no Turing machine can read an infinite amount of input in a finite amount of time. If we declare all solutions that take infinite time to be indeterminate, no language that contains infinitely-long terms can be recursive. It can only be recursively enumerable.

      Thing is, if we could reject the infinite terms, it would solve the halting problem. That doesn't work, so we can't use finite solution time as the criterion to decide whether a language is provable or not. It sounds you've accidentally conflated the idea of defining a language with the idea of proving a language by inspection. Officially incorrect, but easy to do if you're moving fast and not being totally anal about checking the math.

      Now as to the halting problem:

      If a set is recursively enumerable, it is semi-decidable. It will reach the accept state for every provable input, but will either reject or loop infinitely for unprovable input.

      By that definition, we can build a lookup table that says whether any given program halts or not. We just can't do it in finite time. That same statement appears in the lecture you cited:

      It should be noted that an unsolvable problem might be partially solvable by an algorithm that makes an exhaustive search for a solution. In such a case the solution is eventually found whenever it is defined, but the search might continue forever whenever the solution is undefined.

      though I do agree that 'partially solvable' is a superior replacement for my phrase 'solvable, but only by inspection in infinite time'. It's shorter, and fits the heirarchy better.


        You just accurately regurgitated a good number of textbook definitions. Which isn't evidence of anything beyond your having access to a textbook or an equivalent online resource.

        But none of your verbiage in any way, shape, or form addressed the direct question you were directly asked about your extremely unconventional use of the word "solvable".

        Which is evidence that you are dodging the question.

        A piece of friendly advice for the future. When you find yourself caught having made a mistake, admit it up front, and don't drag it out. People tend to forgive and forget when you do that. But when you put your foot in your mouth and proceed to attempt to get the rest of the leg in, the sight tends to stick in people's minds. Besides which, you simply aren't going to succeed anyways, and it is less work that way...

Log In?

What's my password?
Create A New User
Node Status?
node history
Node Type: note [id://132413]
[SuicideJunkie]: Windirstat is what we use here for nagging people who use up the transfer share.
[SuicideJunkie]: Helps that the top level directories are people's names ;) But the nested rectangles make it easy to spot wasted space when it is lots of small stuff or a few big things.

How do I use this? | Other CB clients
Other Users?
Others scrutinizing the Monastery: (10)
As of 2017-09-20 17:02 GMT
Find Nodes?
    Voting Booth?
    During the recent solar eclipse, I:

    Results (237 votes). Check out past polls.