The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 06/28/2013 12:41 PM, t x wrote:

With apologies for questioning the obvious: are the following facts correct (this attempts to "drill down" from complexity theory down to tprogDenote)

1) By Rice's Lemma / Halting problems, we know that program properties, in general, are undecidable.

This is a pretty nebulous statement, but it probably gives a decent intuition.  You should at least clarify that you're talking about Turing complete languages, which Gallina isn't.

2) Coq functions (that return bool) are all decidable -- because to define them in Coq, we need a proof of termination (via showing that some measure decreases.)

Yes, it is decidable whether any closed term of Gallina of type [bool] evaluates to [true].

3) Coq Props can be undecidable, since we can formulate Halting problem in terms of Coq Props "exists i: state( runSteps i tm_description tm_input ) == halts"

4) With law-of-excluded-middle/pierce's law/..., each Prop in Coq is either True or False -- but still undecidable in that we don't have a decision property for them. (i.e. we know that either this TM halts, or it doesn't halt, but we don't have a Coq function for computing which.)

Right.

##

Now, in regards what you said above,

>> Here's a concise answer which I hope helps: The two properties you mention are decidable.  Most program properties are undecidable.  It also helps that the two properties above are _easy_ to decide. :)

5) >> The two properties you mention are decidable.

Is this is because progDenote, as a Coq function, has a proof of termination? Therefore, there's some finite list of states that represents its computation history. The query we care about can be computed in O(n) time, given its computational history.  Thus if we just generate the computation history, we can decide it.

6) >> It also helps that the two properties above are _easy_ to decide. :)

Is this is because the "computational history" has O(1) steps/length?

I'm not proposing any general theoretical perspective on these issues.  The two properties in question just happen to be clearly decidable.  I don't know of some alternate characterization of decidability that is more useful here; sorry.