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.