Scott David Daniels <scott.dani...@acm.org> writes:
> Having once been a more type-A, I labored for a couple of years trying
> to build a restricted language that provably terminated for work on an
> object-oriented database research. I finally gave it up as a bad idea,
> because, in practice, we don't care if a loop will terminate or not in
> database work; a transaction that takes a year to commit is equivalent
> to an infinite loop for all applications that I have interacted with
> (and yes, I have worked allowing four day transactions to commit).
I think the purpose of the termination proofs is to ensure that
nonterminating functions don't introduce inconsistency into the
verification logic, rather than out of concern that some function
might actually loop. Consider the function
def f(x):
return 1 + f(x)
aside from the "minor" issue of infinite recursion, this is a nice,
well-typed function that doesn't have any side effects, doesn't raise
exceptions, etc. It is referentially transparent, so one can
substitute any call to it with the value from another call to the same
arg, i.e. we can substitute x=3 and deduce the equation
f(3) = 1 + f(3)
Subtracting f(3) from each side, we get 0 = 1, an erroneous "theorem"
from which the verification system can infer all kinds of other bogus
results. By requiring proof that any function purporting to return a
value really DOES return a value (rather than looping, raising an
exception, etc.), we get rid of this problem. The actual number of
computing steps before termination isn't an issue for this purpose, as
long as it is finite.
--
http://mail.python.org/mailman/listinfo/python-list
