Greetings. This may be a little off topic, but I could not get much response from comp.theory, so here it goes: Is it possible to have a programming language that can be used to produce only the programs that terminate, but at the same time decide all recursive languages? Or does such limitation automatically reduce the class of languages that such a programming language decide to primitive-recursive? Perhaps, I couldn't explain it very clearly. I suppose another way of saying this is: Is there a strongly normalizing system that can decide the class of recursive languages? Perhaps something less strong than a Turing Machine, for example deciding all recursive languages but not recognizing any recursively enumerable languages. Thanks
G'day. On Thu, May 08, 2003 at 09:05:25AM +0300, Cagdas Ozgenc wrote:
Is it possible to have a programming language that can be used to produce only the programs that terminate, but at the same time decide all recursive languages? Or does such limitation automatically reduce the class of languages that such a programming language decide to primitive-recursive?
I don't know if this answers your question, but the class of primitive recursive programs is not the largest class of provably terminating programs there is. For example, I can very easily produce a programming language which consists of primitive recursive programs plus these five other specific programs which I happen to know always terminate because I proved it by other means. Cheers, Andrew Bromage
I don't know if this answers your question, but the class of primitive recursive programs is not the largest class of provably terminating programs there is.
For example, I can very easily produce a programming language which consists of primitive recursive programs plus these five other specific programs which I happen to know always terminate because I proved it by other means.
That's a good example. So how much can we expand this class? Is it possible to cover all recursive languages, or is there a theorem that says this is not possible?
That's a good example. So how much can we expand this class? Is it possible to cover all recursive languages, or is there a theorem that says this is not possible?
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). 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.) 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. cheers peter
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.
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.
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?
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=44706211#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
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
I have read books/articles on rewriting systems. All of them talk about how to prove termination and confluence, but none of them seem to generalize and present the big picture. I don't really care about the properties of a particular rewriting system. I am looking for milestone results. Let me see if I can acquire the reference you pointed, is it available on the Internet?
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
G'day all. On Thu, May 08, 2003 at 08:15:11PM +1000, Peter Gammie wrote:
Utility? Absolutely none. ;-)
Not true. The Mercury group did this analysis for a reason, namely, that the transformation: p :- q, r. becomes p :- r, q. preserves static semantics in a declarative logic language, however it does not preserve operational semantics unless r always terminates. I suppose this is somewhat analogous to strictness analysis or other analyses designed to preserve full laziness in Haskell. Cheers, Andrew Bromage
On Fri, 9 May 2003, Andrew J Bromage wrote:
On Thu, May 08, 2003 at 08:15:11PM +1000, Peter Gammie wrote:
Utility? Absolutely none. ;-)
Not true. The Mercury group did this analysis for a reason, namely, that the transformation: p :- q, r.
becomes
p :- r, q.
preserves static semantics in a declarative logic language, however it does not preserve operational semantics unless r always terminates.
argh! having a language that satisfies my constraints is pretty useless; in practice I'd expect you're better off going for Turing completeness + analysis (ala Mercury, incomplete) or Turing incompleteness + trivial termination predicate (ala traditional Type Theory - not to belittle the efforts that go into termination/totality proofs, or expressing programs in their languages.). cheers peter
G'day all. On Thu, May 08, 2003 at 06:07:44PM +1000, Peter Gammie wrote:
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.
The Mercury group did some work on this as a static analysis. Have a look for all papers with "termination analysis" in the title: http://www.cs.mu.oz.au/research/mercury/information/papers.html Unfortunately this work is probably no use for Haskell, as they all rely on data structures not being infinite or cyclic (which they are in any logic language which features an occurs check or statically computable equivalent). Cheers, Andrew Bromage
On Fri, 9 May 2003, Andrew J Bromage wrote:
On Thu, May 08, 2003 at 06:07:44PM +1000, Peter Gammie wrote:
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.
The Mercury group did some work on this as a static analysis. Have a look for all papers with "termination analysis" in the title:
http://www.cs.mu.oz.au/research/mercury/information/papers.html
Unfortunately this work is probably no use for Haskell, as they all rely on data structures not being infinite or cyclic (which they are in any logic language which features an occurs check or statically computable equivalent).
To flog the horse a bit further: this isn't what i'm looking for, as there are predicates that do terminate and fail to be identified as such. (Putting it another way, the termination check is incomplete - as all such checks must be for a Turing-complete language.) I recall Harald reckoning their check is adequate for 80% of the predicates in the compiler, so it is impressive even so. A friend pointed me to David Turner's page on strong functional programming: http://www.cs.ukc.ac.uk/people/staff/dat/esfp.html that seems related to what we're discussing. cheers peter
On Thursday 08 May 2003 09:05, Cagdas Ozgenc wrote:
Is it possible to have a programming language that can be used to produce only the programs that terminate, but at the same time decide all recursive languages? Or does such limitation automatically reduce the class of languages that such a programming language decide to primitive-recursive?
I'm not sure if that's theoretically possible. A recursive language requires
more than an LBA for recognition. But then the new edition of Cindrella book
says when you use a polynomial-bounded TM it's not guaranteed to halt. I
pondered the same question last year but when I couldn't find an answer
easily I gave up :)
Is your intention to design such a programming language or to make a
mindblowing proof?
Maybe it's better to start with subsets of recursive languages. DL people are
dealing with decidable subsets of FOL, that might be interesting. Ouch, the
thought of all recursive sets gave me a headache (^_-)
Cheers,
--
Eray Ozkural (exa)
participants (5)
-
Andrew J Bromage -
Cagdas Ozgenc -
Doaitse Swierstra -
Eray Ozkural -
Peter Gammie