on termination

[Eray Ozkural]

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