You may want to look at the large body of work hat has been done on termination in rewrite systems, where many classes and properties have been identified over the years. I am not an expert but: The termination hierarchy for term rewriting, Applicable Algebra in Engineering, Communication and Computing, 2001, volume 12, pages 3-19 might be a good starting point, Doaitse Swierstra On donderdag, mei 8, 2003, at 12:15 Europe/Amsterdam, Peter Gammie wrote:
On Thu, 8 May 2003, Cagdas Ozgenc wrote:
The class of recursive (total) functions is not recursively enumerable, i.e. not acceptable by a Turing machine. This result can be found in any textbook on recursive function theory (ask me off list and I'll dig up a reference).
You lost me there. I thought recursive class is a subset of recursively enumerable class. Perhaps you are referring to a special case.
No, I am saying that you cannot write a program that runs on a Turing machine that accepts all and only (some representation of) the class of total functions. You can, of course, write programs that accept subsets of this class (e.g. the primitive recursive functions) or all of this class and some more (e.g. Turing-computable functions, incidentally including some partial functions along the way).
Tony Hoare wrote a paper about this that you might find interesting:
http://portal.acm.org/ citation.cfm?id=356606&coll=portal&dl=ACM&CFID=10349987&CFTOKEN=4470621 1#FullText
More interestingly, it is possible to (uniformly) define classes of total functions that are strictly larger than the primitive recursive class - in particular, this is what type theorists spend a lot of time doing. (See, for example, Simon Thompson's book on Type Theory and Functional Programming.)
I have skimmed through the following work.
http://www.math.chalmers.se/~bove/Papers/phd_thesis_abs.html
She claims that it is not possible syntactically detect termination, if the recursion is not based on smaller components at each turn. But I think she doesn't supply a proof for that.
I believe this statement as it stands is not true; there are functions that can be proved terminating but do not uniformly reduce the size of an argument. (Does Ackermann's function serve as a counter example?) Suffice it to say that Ana's condition is sufficient but not necessary, and is used in practice as it can be automated. See the work done on termination analysis in Mercury for variations on this theme:
http://citeseer.nj.nec.com/speirs97termination.html
Now, a question of my own: is it possible to uniformly define a class of functions that have a non-trivial decidable halting predicate? The notion of "uniform" is up for argument, but i want to rule out examples like Andrew's that involve combining classes in trivial ways.
You lost me once again. What do you mean, could you please eloborate?
OK:
1. The primitive recursive functions have a trivial termination predicate, viz "true". This is also the case for the type theorists' systems I have seen.
2. The Turing partially-computable functions have an undecidable termination predicate.
What I want: a class of functions that don't all terminate, don't all not terminate, and furthermore I can tell how a given element of the class will behave without running it. It must have at least some expressiveness; this is up for grabs, but it'll have to encompass at least primitive recursion to be interesting.
Utility? Absolutely none. ;-)
cheers peter _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe