[Haskell-cafe] Limits of deduction

[Roberto Zunino]

Andrew Coppin wrote:
> 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?

If "X is true/false" is replaced by "X can be determined to be 
true/false", then: yes, roughly.

I say "roughly" because "the set of programs where we can't actually 
determine the truth of X" depends on the program analysis algorithm, 
i.e. is not uniquely determined by X.

For instance, you can approximate the halting problem with:
Procedure A(n):
1) run program for n steps
2) if it halts, return "Halts, I'm sure"
3) otherwise, return "Don't know"

Each algorithm A(n) partitions programs into "halting" and "???".
Each A(n) is better than A(n-1), i.e. more halting programs are 
recognised. Also, for each halting program P, there exists some n such 
that A(n) recognises P.

So, "the set of programs where we can't actually determine termination" 
has no meaning unless you specify the actual algorithm.

However, for any algorithm A you choose, you will indeed partition 
programs into the three classes "Yes/No/???" you mentioned.
Also, a better algorithm than A surely exists (i.e. with a smaller "???" 
class), so you can keep on improving your program analysis techniques 
forever. (a.k.a. Eternal Employment Theorem ;-))

> I find it interesting that one quite hard looking property - "this 
> program is well-typed" - can always be deduced.

This is not true, in general. The "naive" polymorphic type system for 
the lambda calculus is undecidable. For some tricky cases, you might 
want to look up "polymorphic recursion".

More practically, in some cases you need type signatures in your Haskell 
programs, since inference can not provide them (in general). Here's a 
simple one (involving rank-N):

(\(x :: forall a . a->a) -> x x) (\x -> x) 3

Intuition: ... => (id id) 3 => id 3 => 3 .

Also, using only rank-1:

polyf :: Int -> a -> Int
polyf x y = if x==0 then 0
             else if x==1 then polyf (x-1) (\z->z)
             else polyf (x-2) 3

Here passing both 3 and (\z->z) as y confuses the type inference.

> Perhaps that's because 
> the language is specifically designed to constrain the set of possible 
> programs in such a way that this is possible? 

Well, I would say the "naive" polymorphic type system is restricted so 
to achieve decidability without rejecting too many good programs.
(See e.g. Hindley-Milner)

(And when designing a type system, decidability is a main concern)

Examples as those above are arguably contrived, and rarely show up in 
actual code. And when it happens, adding a type signature is not too hard.

> 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*

Yes, this is the case, as for the programs above.

Also, one might argue that (if True then 42 else "a") is well-typed, and 
this is hard to check statically.

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

Your formulation of "the halting problem is undecidable" seems rather 
precise to me.

Regards,
Zun.