# on termination

**Eray Ozkural
**
erayo@cs.bilkent.edu.tr

*Wed, 14 May 2003 16:05:54 +0300*

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