On Jan 28, 2008 11:22 AM, Bob Mottram <[EMAIL PROTECTED]> wrote: > On 27/01/2008, Vladimir Nesov <[EMAIL PROTECTED]> wrote: > > > Consider the following subset of possible requirements: the program is > > > correct > > > if and only if it halts. > > > > It's a perfectly valid requirement, and I can write all sorts of > > software that satisfies it. I can't take a piece of software that I > > didn't write and tell you it it satisfies it, but I can write piece of > > software that satisfies it, that also does all sorts of useful stuff. > > > This would seem to imply that you've solved the halting problem. >
No it won't. Halting problem is so problematic when we are given an arbitrary program from outside. On the other hand, there are very powerful languages that are decidable and also do useful stuff. As one trivial example, I can take even external arbitrary program (say, a Turing machine that I can't check in general case), place it on a dedicated tape in UTM, and add control for termination, so that if it doesn't terminate in 10^6 tacts, it will be terminated by UTM that runs it. Resulting thing will be able to do all things that original machine could in 10^6 tacts, and will also be guaranteed to terminate. You can try checking out for example this paper (link from LtU discussion), which presents a rather powerful language for describing terminating programs: http://lambda-the-ultimate.org/node/2003 Also see http://en.wikipedia.org/wiki/Total_functional_programming It's not very helpful in itself, but using sufficiently powerful type system it should also be possible to construct programs that have required computational complexity and other properties. -- Vladimir Nesov mailto:[EMAIL PROTECTED] ----- This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe or change your options, please go to: http://v2.listbox.com/member/?member_id=8660244&id_secret=90499378-2cd47f
