I'd like to clarify the termination decision procedure. I believe it can take the body of a function in our language and tell if the function terminates for all inputs. This implies that we can decide on termination without evaluating the function on all inputs (whose set is countably infinite). A small clarification: the 'branch-on-zero' statement should have the form "if-nonnegative exp then exp1 else exp2". Because the domain includes 'undefined' (aka NaN), the only functions that terminate for all inputs are those that leave their arguments alone and either propagate them or return constants. For example, the following functions terminate on all inputs f1(x) = x f2(x,y) = y f3(x) = 0 f4(x) = if-nonnegative power(5,125) then x else NaN The following functions will fail to terminate on at least one input: g1(x) = x + x g2(x) = if-non-negative x then x else NaN g3(x) = if-non-negative x*x then 0 else 1 Although it seems that g3 is equivalent to f3, that is not true: g3(NaN) diverges whereas f3(NaN) returns 0. These examples clarify a decision procedure, which can be stated as follows: if a partial evaluation of f(x...z) -- that is, unfolding plus constant propagation -- reduces f() to f1, f2, or f3 types, the function f() terminates on all inputs. Otherwise, there is one value (most likely NaN), that, when passed to f(), will cause it to diverge. Our partial evaluation procedure first unfolds all function calls. That is possible because the call graph does not have direct cycles (NPFIX must be treated as a special node in the call graph). Any operation (multiplication, addition, comparison, NPFIX) on a dynamic value can lead to a non-termination (if that value is NaN). Thus the only operations that can still guarantee termination are "if exp1 then exp2 else exp3" and "NPFIX exp1 exp2 exp3" where exp1 is a constant expression. We can evaluate it. Because it contains only primitive recursive functions, we provably can do that in some finite time. Therefore, we can decide which branch to take and continue to analyze exp2 or exp3. It seems the decision procedure is total and correct.
On Friday 09 May 2003 21:33, oleg@pobox.com wrote:
I'd like to clarify the termination decision procedure. I believe it can take the body of a function in our language and tell if the function terminates for all inputs. This implies that we can decide on termination without evaluating the function on all inputs (whose set is countably infinite).
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. I got confused when I read that Ackermann's function was a recursive function that was not primitive. Could you please explain this to me? Excuse me if I'm being ignorant about this subject. Regards, -- Eray Ozkural (exa) <erayo@cs.bilkent.edu.tr> 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 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 <URL: 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. Jón -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk 31 Chalmers Road jf@cl.cam.ac.uk Cambridge CB1 3SZ +44 1223 570179 (after 14:00 only, please!)
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 <URL: 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) <erayo@cs.bilkent.edu.tr> 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
If I remember correctly, that's the chief reason Ackermann came up with the function. Have a look at <URL: 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,
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.
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) <erayo@cs.bilkent.edu.tr> 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
Hi
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.
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. (Incidentally, Cayenne's type theory is the exception rather than the rule: it's much-criticized undecidable typechecking comes down to the availability of non-terminating programs at the type level. ghc with `undecidable instances' allows you to write non-terminating Prolog programs at the type level, thus breaking for exactly the same reason. What exactly is Haskell's type level programming language, anyway?) Of course, restricting to an incomplete fragment does not necessarily mean `primitive recursion' in the narrow sense which excludes Ackermann's function, viz data Nat = O | S Nat primrec :: Nat -> (Nat -> Nat -> Nat) -> Nat -> Nat primrec base step O = base primrec base step (S n) = step n (primrec base step n) Just a bit of polymorphism is enough to overcome that problem: polyprimrec :: t -> (Nat -> t -> t) -> Nat -> t polyprimrec base step O = base polyprimrec base step (S n) = step n (polyprimrec base step n) Old fashioned dependent type theories present computation over inductive datatypes by equipping their structural induction principles with a computational behaviour---an inductive proof of all n : Nat . P n, when applied to 3, reduces to step 2 (step 1 (step 0 base)), just like polyprimrec, but with base :: P 0, and step :: all n : Nat. P n -> P (S n). Suitably equipped with `pattern matching' sugar, these induction principles provide quite a rich language of terminating functions, necessarily incomplete, but including such notoriously troublesome customers as first-order unification. Moreover, a structural induction principle is just the recursion operator which comes `free of charge' with an inductive datatype: many other total recursive idioms can be proven admissible once (by a process which resembles coding up a memoization scheme), then re-used freely in programs. 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. Hope this helps Conor
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.
My question is as
follows: "What is the largest class that we can find a termination procedure?".
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?
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
Can this topic be taken elsewhere please? The discussion never had much to do with Haskell and the relevance seems to have been falling steadily. -- Alastair Reid
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
Hello, On Wednesday 14 May 2003 12:25, C T McBride wrote:
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.
I guess if Godel were here he could tell us that any consistent formal system powerful enough to express number theory is necessarily incomplete. So maybe I was asking the contrapositive, so the answer is already known? That is, if a system is complete, it cannot express number theory. This follows from incompleteness. But I'm not sure if that is what I was asking. It seems to be different: is there a language to denote any complete system? That's the question, and L_d or L_u doesn't seem to be the answer to that (on their own) Is there a known proof that one needs at least a TM to recognize all decidable languages? Ouch, I must fix my head and I'll get back to this :) If you guys think haskell-cafe is improper for this conversation we can continue on theory-edge on yahoo groups. But I don't think it's improper, after all there is all kind of theoretical weirdness talked of in the main haskell discussion list. Why should this be any less relevant??? We were just having a similar conversation about CSLs and recursive sets on theory-edge so you might want to check it out while it's hot. Regards, -- Eray Ozkural (exa) <erayo@cs.bilkent.edu.tr> 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
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
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.
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).
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.
I always thought in a similar fashion. But literature insists that the decidability is always measured with respect to a Turing Machine. Thus, I was unable to communicate to many other people on the usenet.
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 10:23, Cagdas Ozgenc wrote:
I always thought in a similar fashion. But literature insists that the decidability is always measured with respect to a Turing Machine. Thus, I was unable to communicate to many other people on the usenet.
Hmm. But, the real question you are asking doesn't seem to be quite trivial Cagdas. Cheers, -- Eray Ozkural (exa) <erayo@cs.bilkent.edu.tr> 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 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) <erayo@cs.bilkent.edu.tr> 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
Let's see: Is there a formal system to denote all complete systems and nothing else?
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.
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?
You mean "decide" not "recognize", right?
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.
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 :).
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) <erayo@cs.bilkent.edu.tr> 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
C T McBride wrote:
a simple diagonalization argument shows that the system's own normalization function (terminating, by definition) cannot be coded within the system itself.
I would be interested in seeing this. Could you elaborate, or point us to a link where this is spelled out? Sam Moelius
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) <erayo@cs.bilkent.edu.tr> 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
participants (8)
-
Alastair Reid -
Andrew J Bromage -
C T McBride -
Cagdas Ozgenc -
Eray Ozkural -
Jon Fairbairn -
oleg＠pobox.com -
Sam Moelius