                                                                                                                                                                                                                                                                
Path: r9ni78645pbh.0!nntp.google.com!news2.google.com!news1.google.com!Xl.tags.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!nntp.earthlink.com!news.earthlink.com.POSTED!not-for-mail
NNTP-Posting-Date: Fri, 20 Apr 2012 11:46:57 -0500
Date: Fri, 20 Apr 2012 09:47:00 -0700
From: Patricia Shanahan <p...@acm.org>
User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120327 Thunderbird/11.0.1
MIME-Version: 1.0
Newsgroups: comp.theory,sci.logic
Subject: Re: Proof that Decidability is Always Decidable
References: <qe6dnX1dubvSnRPSnZ2dnUVZ_qednZ2d@giganews.com> <e6f32355-1c69-423c-adfe-6b45e72c2770@r2g2000pbs.googlegroups.com> <1sOdnSWdnN5VDxPSnZ2dnUVZ_jCdnZ2d@giganews.com> <pqqdnZ4ID93SKhPSnZ2dnUVZ8gqdnZ2d@giganews.com> <z_2dnSJn6tUuoBLSnZ2dnUVZ_omdnZ2d@giganews.com> <qotpqb4tfhp.fsf@ruuvi.it.helsinki.fi> <XOydnTpEA4y3eRLSnZ2dnUVZ_u-dnZ2d@giganews.com> <qotzka72817.fsf@ruuvi.it.helsinki.fi> <TLKdnfTdHbc-7w3SnZ2dnUVZ_j6dnZ2d@giganews.com> <jmqjkv$cam$1@dont-email.me> <LMKdnfeEi5SUSg3SnZ2dnUVZ_tOdnZ2d@giganews.com> <qotsjfzkm0j.fsf@ruuvi.it.helsinki.fi> <INSdnQU9E9VppwzSnZ2dnUVZ5gudnZ2d@giganews.com> <qot7gxak2z3.fsf@ruuvi.it.helsinki.fi> <iqKdnYBcGsds6wzSnZ2dnUVZ_umdnZ2d@earthlink.com> <qotipgucsn7.fsf@ruuvi.it.helsinki.fi>
In-Reply-To: <qotipgucsn7.fsf@ruuvi.it.helsinki.fi>
Message-ID: <zaCdnVIELsucDgzSnZ2dnUVZ_oqdnZ2d@earthlink.com>
Lines: 44
NNTP-Posting-Host: 70.230.201.141
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit

On 4/20/2012 8:47 AM, Jussi Piitulainen wrote:
> Patricia Shanahan writes:
>> On 4/20/2012 5:22 AM, Jussi Piitulainen wrote:
>> ...
>>> The question remains, is the third answer interesting. And is the
>>> three-valued thing implementable.
>> ...
>>
>> Three value halting decider-substitutes that return {true, false, mu}
>> are definitely implementable with "true" meaning that the input
>> definitely describes a TM computation that halts, "false" meaning that
>> the input definitely does not describe a TM computation that halts, and
>> "mu" all other cases.
>>
>> Trivially, consider a TM that unconditionally returns "mu" for all
>> inputs. It meets the conditions I described above, though it is not very
>> useful. The usefulness of such a decider-substitute increases as the
>> density of "mu" results decreases.
>
> Yes. That's why I said the question remains whether the third value is
> interesting. The third value from an overly trivial analyzer is not.

In reality, limiting the "mu" cases for various undecidable static
analysis questions is an important research area. For example, some of
the most promising approaches to deadlock recovery involve a combination
of static analysis and run-time checks. The better the static analysis,
the less time and memory needs to be spent on run-time checking.

>
>> PO has previously rejected this approach.
>
> I suspect he's now thinking that the third value would be used _only_
> in the case where the machine and its input being analyzed are defined
> in terms of a halt analyzer in such a way that the analyzer cannot
> return a correct value (hope I got the twist right). This would make
> the three-valued analyzer very interesting but I suspect questions of
> implementability (even in principle) remain. PO has not addressed such
> questions.

And he won't. He deeply believes that any function he wants to be
computable is computable. That means he expects his use of a function in
his pseudo-code to be accepted as proof of its computability.

Patricia