Termination and type systems

[Marshall]

David Hopwood wrote:
> Marshall wrote:
> > David Hopwood wrote:
> >
> >>A type system that required an annotation on all subprograms that do not
> >>provably terminate, OTOH, would not impact expressiveness at all, and would
> >>be very useful.
> >
> > Interesting. I have always imagined doing this by allowing an
> > annotation on all subprograms that *do* provably terminate. If
> > you go the other way, you have to annotate every function that
> > uses general recursion (or iteration if you swing that way) and that
> > seems like it might be burdensome.
>
> Not at all. Almost all subprograms provably terminate (with a fairly
> easy proof), even if they use general recursion or iteration.

Well, um, hmmm. If a subprogram uses recursion, and it is not
structural recursion, then I don't know how to go about proving
it terminates. Are the proof-termination techniques I don't
know about?

If we can specify a total order on the domain or some
subcomponents of the domain, and show that recursive
calls are always invoked with arguments less than (by
the order) those of the parent call, (and the domain is
well founded) then we have a termination proof.

(If we don't use recursion at all, and we only invoke
proven-terminating functions, same thing; actually
this is a degenerate case of the above.)

For iteration? Okay, a bounded for-loop is probably easy,
but a while loop? What about a function that calculates
the next prime number larger than its argument? Do we
have to embed a proof of an infinity of primes somehow?
That seems burdensome.


> If it were not the case that almost all functions provably terminate,
> then the whole idea would be hopeless.

I agree!


> If a subprogram F calls G, then
> in order to prove that F terminates, we probably have to prove that G
> terminates. Consider a program where only half of all subprograms are
> annotated as provably terminating. In that case, we would be faced with
> very many cases where the proof cannot be discharged, because an
> annotated subprogram calls an unannotated one.

Right, and you'd have to be applying the non-terminating annotation
all over the place.



> If, on the other hand, more than, say, 95% of subprograms provably
> terminate, then it is much more likely that we (or the inference
> mechanism) can easily discharge any particular proof involving more
> than one subprogram. So provably terminating should be the default,
> and other cases should be annotated.

Well, I can still imagine that the programmer doesn't care to have
non-termination examined for every part of his code. In which case,
he would still be required to add annotations even when he doesn't
care about a particular subprograms lack of a termination proof.

The pay-for-it-only-if-you-want-it approach has some benefits.
On the other hand, if it really is as common and easy as you
propose, then annotating only when no proof is available is
perhaps feasible.

I'm still a bit sceptical, though.


> I do not know how well such a type system would work in practice; it may
> be that typical programs would involve too many non-trivial proofs. This
> is something that would have to be tried out in a research language.

Yeah.


Marshall