[Haskell-cafe] Limits of deduction

[Andrew Coppin]

Stefan Holdermans wrote:
> This is rather typical in the field of program analysis. Getting the 
> analysis precise is impossible and reduces to solving the halting 
> problem. So, the next best thing is to get an approximate answer. An 
> import design guideline to such an analysis is "to err on the safe 
> side". That means you'll end up either
>
> - with an analysis that tells you that a given function *is guaranteed 
> to* inspect all elements of its argument list or else that the 
> function *may* inspect less elements; or
>
> - with an analysis that tells you that a given function *is guaranteed 
> to* not inspect all elements of its argument list or else that the 
> function *may* inspect all elements.
>
> Of course, it depends on your needs which of these modalities suits 
> you best.

Right. So what you're saying is that for most program properties, you 
can partition the set of all possible problems into the set for which X 
is true, the set for which X is false, and a final set for programs 
where we can't actually determine the truth of X. Is that about right?

I find it interesting that one quite hard looking property - "this 
program is well-typed" - can always be deduced. Perhaps that's because 
the language is specifically designed to constrain the set of possible 
programs in such a way that this is possible? Or perhaps it's just that 
the set of programs which can't be proved well-typed are simply rejected 
as if they were provel ill-typed? *shrugs*

Can somebody explain to me exactly what the halting problem says? As I 
understand it, it doesn't say "you can't tell if this program halts", it 
says "you cannot write an algorithm which can tell whether *every* 
program halts or not". (Similar to the way that Galios dude didn't say 
"you can't solve high-order polynomials", he said "you can't solve all 
possible Nth order polynomials *with one formula* [involving only a 
specific set of mathematical operators]". As in, you *can* solve 
high-order polynomials - just not with a single formula for all of them. 
Or not just with the specified operators.)

> I am not aware of any work on exactly this type of analysis, but you 
> may want to have a look at strictness analysis first; I think there's 
> quite some overlap with what you are trying to achieve.

I was actually thinking about having a chain of functions, and wondering 
whether you can remove the intermediate lists, and/or "optimise" them 
into some other data structure. But that would depend on how much of the 
list is consumed - which, as I suspected, is tricky to determine.