The Coq mailing list

[t x <txrev319 AT gmail.com>]

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.

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.)

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.)

##

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?

On Fri, Jun 28, 2013 at 4:33 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 06/27/2013 11:58 PM, t x wrote:

I'm reading Chapter 2 of CPDT.

tinstrDenote feels a bit too magical to me, especially the part about:
  1) statically know the # of elements on the stack
  2) statically know the type of the elements on the stack

This seems like it solves all problems in formal verification and I'm trying to understand why tinstrDenote does NOT solve all problems.

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. :)

It seems important that all programs in chapter 2 always execute a _constant_ number of steps.

It sounds like this is your intuition behind why the properties above are decidable.  I agree with the factual statement, and I agree that it suggests a pattern for deciding program behaviors.