[Haskell-cafe] Limits of deduction

[Stefan Holdermans]

Andrew,

Jules wrote:

> It's computationally impossible, in general. I can write something  
> silly like
>
> f (x:xs) = x : (UniversalTuringMachine(x) `seq` xs)
>
> and it reduces to the halting problem.
>
> However, it might be tractable for a large class of sensible  
> programs. Someone around here might be aware of some relevant  
> research?

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.

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.

Cheers,

   Stefan