on termination

[Doaitse Swierstra]

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