On Tuesday 13 May 2003 01:17, Jon Fairbairn wrote:

On 2003-05-12 at 21:53+0300 Eray Ozkural wrote:

...

I've seen many constructions on primitive recursive functions but what I don' t understand, not having the required expertise on recursive function theory, is whether the set of primitive recursive functions correspond to recursive sets in theory of computation.

They don't, because

...

[...] Ackermann's function was a recursive function that was not primitive.

If I remember correctly, that's the chief reason Ackermann came up with the function. Have a look at http://mathworld.wolfram.com/AckermannFunction.html > and the links on that page for computable and primitive recursive, and see if that helps. The site also has a definition of recursive.

OK. Then isn't there an answer to the original question? I couldn't find a machine model that satisfies Cagdas's operational requirements. Any thoughts? Maybe it's a very easy answer but I can't see it, and I can't say I know the proof of every theorem in Cindrella book. Cheers, -- Eray Ozkural (exa) Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

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.

Hmm, I think this depends on what a strongly normalizing system is :) Slightly going out of my sphere of knowledge (^_^) Cheers, -- Eray Ozkural (exa) Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

...

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.

G'day. On Wed, May 14, 2003 at 02:59:50PM +0300, Cagdas Ozgenc wrote:

Perhaps that's a little misleading, but I don't know how to phrase it properly. Basically what is the largest class of languages that a terminating system can decide?

Assuming for the moment that your "terminating system" is a TM... I believe that if you were to produce such a class of languages, I can produce another recursively enumerable language not in your class by some kind of diagonalisation procedure. I can then create a terminating recogniser which accepts your class, plus the new language as a special case. Cheers, Andrew Bromage

Hi I'm sorry about the level of consternation this discussion seems to be generating, so let me attempt to clarify my previous remarks. The diagonalization argument which shows that any total language misses some total programs is the usual one: Godel-code everything in sight, then make the alleged universal program eat a twisted copy of itself. It's the Epimenides/Cantor/Russell/Quine/Godel/Turing argument. And it goes like this... Suppose we have a programming language in which all expressions compute to a value excluding bottom. For sake of argument, let's code expressions and values as natural numbers (an ascii source file is just a big number; so is a finite output). In particular, every function f from Nat to Nat which lives in the language is quoted by a code (quote f) :: Nat, and we know a total function which unquotes, executing a coded f at a given argument eval :: Nat -> (Nat -> Nat) with spec eval (quote f) x = f x eval _ _ = 0 Given such a function, I can summon up its evil cousin, with spec: evil :: Nat -> Nat evil code = 1 + (eval code code) Now, if eval is total, so is evil. But if evil lies within our language, it will have a number. Without loss of generality, quote evil is a human number and that number is 666. So, we get evil 666 = 1 + (eval 666 666) = 1 + evil 666 which is plainly untrue. Hence evil is a total function which is not expressible in the language (so eval better not be expressible either). Of course, for any language of total functions, its Halting Problem is trivial, but that's beside the point. There is no largest class of recognizably terminating programs, because no such class can include its own *evaluation* function, which is by definition terminating. Given a total language L, we can always construct a strictly larger language L', also recognizable, which also includes the eval function for L. Meanwhile, back in the cafe, why should Haskellers give a monkeys? Two reasons: one pertinent now, one potential. Firstly, when we make (or Haskell derives) recursive instance declarations, we might like to know that (1) the compiler will not go into a spin when attempting to compute the object code which generates the dictionary for a given instance (2) the code so generated will not loop at run-time You might argue that (1) is not so important, because you can always ctrl-C, but (2) is more serious, because if it fails, you get the situation where the compiler approves your program, then breaks it by inserting bogus code, promising to deliver an instance which does not actually exist. To guarantee these properties, we essentially need to ensure that the instance declaration language is a terminating fragment of Prolog. The various flags available now are either way too cautious or way too liberal: what's a suitable middle way? There is no most general choice. Secondly, might it be desirable to isolate a recognizable sublanguage of Haskell which contains only total programs? Pedagogically, Turner argues that it's useful to have a `safe' language in which to learn. Rhetorically, making bottom a value is just sophistry to hide the fact that looping and match failure are pretty bad side-effects available within an allegedly pure language---preferable to core-dumps or wiping your hard drive, but still bad. Logically, if you want to show a program is correct, it helps if you can get its totality for free. Pragmatically, there are fewer caveats to optimizing bottomless programs. As we've seen, such a sublanguage (perhaps called `Ask', a part of Haskell which definitely excludes Hell) cannot contain all the angels, but it certainly admits plenty of useful ones who can always answer mundane things you might Ask. It's ironic, but not disastrous that lucifer, the evaluation function by which Ask's angels bring their light, is himself an angel, but one who must be cast into Hell. Yours religiously Conor

G'day. On Wed, May 14, 2003 at 04:05:54PM +0300, Eray Ozkural wrote:

It seems to be different: is there a language to denote any complete system?

Of course there is. A language is just a subset of the power set of some symbol alphabet. So, for example, the set of all halting TMs (encoded appropriately) forms a language.

Is there a known proof that one needs at least a TM to recognize all decidable languages?

Here's my working definition of "decidable language": A language L is decidable for some class of automata C if there is an automaton in C which recognises L and halts for all inputs. That is, my working definition of "decidable language" is dependent on the class of automata in which you're trying to implement decidability. If your class of automata is DFAs, for example, all languages are decidable, so you don't even need a TM for that. If your class of automata is TMs, not even a TM will help you. Cheers, Andrew Bromage

G'day. On Thu, May 15, 2003 at 10:23:21AM +0300, Cagdas Ozgenc wrote:

It is not a power set. A language is a subset of the word monoid generated by the alphabet by applying reccurent production of the alphabet (the star operation).

You're right, sorry.

I always thought in a similar fashion. But literature insists that the decidability is always measured with respect to a Turing Machine.

That's probably because of the Church-Turing thesis (i.e. computation equals Turing Machine). However, there are smaller and larger definitions of "computation" than what can be accomplished on a TM. Cheers, Andrew Bromage

On Thursday 15 May 2003 07:16, Andrew J Bromage wrote:

G'day.

On Wed, May 14, 2003 at 04:05:54PM +0300, Eray Ozkural wrote:

...

It seems to be different: is there a language to denote any complete system?

Of course there is. A language is just a subset of the power set of some symbol alphabet. So, for example, the set of all halting TMs (encoded appropriately) forms a language.

Well... A language L \subset of \Sigma^* as Cagdas said. Anyway, by language I meant something else. Is "Formal System" better? Let's see: Is there a formal system to denote all complete systems and nothing else? Let's try it in automata jargon: We know that one needs a machine more powerful than an LBA to recognize all recursive languages. However, even an LBA, by definition is a TM and it can loop over two symbols forever. That is not all LBAs are guaranteed to halt. Can there be an alternative machine formulation that only recognizes recursive sets and nothing else? That is it should be stronger than an LBA, yet less powerful than a TM because it excludes R.E - recursive. So, we are looking for something that doesn't have a corresponding machine. It's possible that it does not exist. But the proof could be interesting for us.

...

Is there a known proof that one needs at least a TM to recognize all decidable languages? [snip]

If your class of automata is DFAs, for example, all languages are decidable, so you don't even need a TM for that. If your class of automata is TMs, not even a TM will help you.

This is not a proof I hope :P Cheers, -- Eray Ozkural (exa) Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

On Thursday 15 May 2003 15:49, Cagdas Ozgenc wrote:

Completeness is not equal to deciding all recursive languages IMO. The bottom explanation of yours is not the same as the above question. Systems with sufficient power are incomplete. The system I am looking for doesn't have to decide its own termination, but its termination should be decideable by using an auxillary TM. Be careful with the jargon. Literature insists that "undecidable" is equal to "cannot be decided by a TM". Although an automaton may not decide its own halting , it may be decided by a TM, hence will be called decideable.

Decidable means that accept or reject states are guaranteed to halt. That is as you said the defining property of recursive sets. The complement of a recursive set is recursive.... I didn't say otherwise (that it should have to decide a "halting problem" for itself). Let's rephrase. If a language is recursively enumerable but not recursive it's not decidable. You would like to exclude all such languages from your automata and would like to recognize (accept or reject) all recursive languages. Right?

The fact that there may be looping LBAs is irrelevant because we can discard those, since the halting is decidable(again note the terminology, can be decided by a TM) for LBA. Indeed the system has to be powerful than an LBA but we still should be able to write a TM that is capabale of discarding the ones that go into infinite loop. I don't know whether it is correct to say that it should be more powerful than a LBA, because it won't have the power to loop :).

You mean the following: I can write a programming language for CSL recognizers that can, at compile time, give an error message such as: ** Undecidable program!!! Check your logic! Do you mean this? And how do you, for instance generalize this to polynomial bounded automata or higher orders? Sincerely, -- Eray Ozkural (exa) Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C

On Wednesday 14 May 2003 18:10, Sam Moelius wrote:

I would be interested in seeing this. Could you elaborate, or point us to a link where this is spelled out?

I can't see an immediate diagonalization proof either. -- Eray Ozkural (exa) Comp. Sci. Dept., Bilkent University, Ankara KDE Project: http://www.kde.org www: http://www.cs.bilkent.edu.tr/~erayo Malfunction: http://mp3.com/ariza GPG public key fingerprint: 360C 852F 88B0 A745 F31B EA0F 7C07 AE16 874D 539C