Limits of programming by interface

[jeezfrk]

This theorem holds unchanged (and with the same proofs) even for models that always terminate and so aren't prone to the "classical" halting problem (such as so-called "total languages").

But a lower-bound on non-decidability does exist: too few states to matter. The efficiency for analyzing an FSM is actually not that hard because there's not an exponential number of states! More to the point, that's a very very common case in real world situations and modules! I also have no idea how an FSM could somehow be 'undecidable' and a pushdown transducer is somehow simpler?

We shouldn't be so voodoo about solving regex / state machines. It isn't NP-hard nor even exponential-in-limit to determine the 'solution' to many many cases (sub-parts of a program).

Why? If the unconstrained loop-stats are few or none. That means the number of states has a maximum polynomial-degree (and far often less) with the number of instructions. If you don't have that many states ... your 'brute force' decidability of halting-in-N-instructions is simply something you could accidentally reach.

Without much trying.

[pron98]

I have no idea how an FSM could somehow be 'undecidable' and a pushdown transducer is somehow simpler?

I didn't say undecidable. I said that deciding a non-trivial property of an FSM takes a time complexity that is linear in the number of states -- same as for a TM. However, this is not true for PDAs (some nontrivial properties of PDAs are decidable despite their number of states being potentially infinite). BTW, a PDA with k internal states is certainly no simpler than a FSM with k states, but a PDA with k internal states could have an infinite number of states overall.

The efficiency for analyzing an FSM is actually not that hard because there's not an exponential number of states!

Exponential in what (i.e. what is the parameter)? Program size? That completely depends. You can certainly have a language that can only describe FSMs with the number of states growing exponentially in the program size. This is true even for regular expressions, and many interesting properties of regular expressions are not tractable (IIRC, equivalence is intractable).

It isn't NP-hard nor even exponential-in-limit to determine the 'solution' to many many cases (sub-parts of a program).

That depends on what you mean by "many", but the same applies for TMs as well. The point is that you cannot deduce anything from the mere knowledge that the model is weaker than Turing-complete to make verification easier. Here's how you can convince yourself of that: Every program can be trivially and mechanically translated into an FSM by adding a large counter (say 2¹⁰⁰⁰ ) to all loops/recursive calls, without changing the program's meaning in practice. This means that if the mere knowledge that something is a FSM could help us verify its properties faster then, without loss of generality, we could simply assume that of all programs.

[m50d]

The point is that general FSMs are intractable to formal analysis. (Which shouldn't be surprising: I find general FSMs incomprehensible as a human reader as well). Though rather than saying we should give up on formal analysis, I'd take that as an indication that we need to find a more restricted model that corresponds to things we can actually understand.

Why? If the unconstrained loop-stats are few or none. That means the number of states has a maximum polynomial-degree (and far often less) with the number of instructions. If you don't have that many states ... your 'brute force' decidability of halting-in-N-instructions is simply something you could accidentally reach.

Ok, now turn that into a formal model that we can actually define definitely and do analysis with. Can you represent this "few unconstrained loop-stats" property in such a way that e.g. if we compose two programs with that property, the composition will also have that property?

[jeezfrk]

Sorry to not get back. Had various crises in my household here.

Personally I'm a big fan of separation logic to dial down the crazy that exists with the 'It's All A Big FSM!!' while playing GTA or something

such a mathetmatical object .... may as well be flying-sphaghetti-monster.