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)