on termination

[Cagdas Ozgenc]

> > On Tuesday 13 May 2003 16:08, Cagdas Ozgenc wrote:
> > > Indeed, I am still looking for a theorem of some sort that either
equates
> > > stongly normalizing systems to primitive recursive functions (if this
is
> > > the case), or a theorem that demonstrates some sort of limitation to
> > > strongly normalizing systems when compared to a turing machine, or a
system
> > > that can decide recursive class but unable to recognize recursively
> > > enumerable class.
>
> There ain't no such thing. Recursiveness is undecidable. More concretely,
> a strongly normalizing system captures a class of terminating functions
> which is necessarily incomplete: a simple diagonalization argument shows
> that the system's own normalization function (terminating, by definition)
> cannot be coded within the system itself.

I think that is not correct. Diagonalization cannot be pursued on every
situation, because it has some prerequisites (for example the system should
be capable of using its programs as subprograms, or ability to invert the
outcome of a program). If the system captures only terminating functions,
then the termination can be simply calculated like the following:

willTerminate:: (a->b) -> Bool
willTerminate = true

As you can see I decided the termination for all functions. Maybe you mean
something else. I don't quite know what "normalization function" is. Another
counter example is a Deterministic Finite Automata. It will terminate on all
finite inputs, and it can encode its own termination function (again similar
to the above trivial function).

> > Hmm, I think this depends on what a strongly normalizing system is :)
> > Slightly going out of my sphere of knowledge (^_^)
>
> A *strongly* normalizing system is one where *all* reduction strategies
> yield a normal form. Type theories are usually designed to be strongly
> normalizing, hence they are Turing incomplete; they do contain all
> programs which are *provably* terminating in the particular logic to which
> they correspond, but that logic, being consistent, is necessarily also
> incomplete.
>
> Of course, restricting to an incomplete fragment does not necessarily
> mean `primitive recursion' in the narrow sense which excludes Ackermann's
> function, viz

That's not the point. It does exclude Ackermann because it will fail to
compile if the compiler is unable to detect the termination of Ackermann's
function. I don't know much about this (it is indeed what I was trying to
learn by starting this discussion), but it may be factual that a general
termination test can only be written for primitive recursive function class
(it is irrelevant that one can prove termination for some non primitive
recursive functions, the question is "is there a general algorithm for a
wider class?"). If this is the case then too bad for us. My question is as
follows: "What is the largest class that we can find a termination
procedure?".

> So there's no magic complete answer to guaranteed termination, but it is,
> I claim, useful to work within an incomplete but terminating language
> if it enables you te express the structural reasons why your program
> works, not just what it should do next.

It will be definetely useful, and it may not necessarily be incomplete. If I
remember correctly monoid(N,+) : monoid defined over naturals with addition
operator is sound and complete. Of course systems where one can write
homological statements will be incomplete. It may be the case that a useful
strongly normalizing system may turn out to be complete. But I don't care
about completeness. Getting back to the core discussion, I really would like
to know the limitations of terminating systems.