Church-Turning is False?

Recently found a paper rebuking the Church-Turing thesis on the grounds of infinite computations and the Y-combinator. It's a tongue-in-cheek poke at Turing's UTM vs McCarthy's LISP, but has some interesting ideas in it. I know the researcher, he's a good guy and should join LtU if he's not lurking already. Although you may question his sanity after reating this..

Infinite Order Logic and the Church-Turing Thesis
Dimitris Vyzovitis

His conclusions include:

  • LISP is an infinite-order logic
  • Halting problem is decidable in LISP (modulo Y-combinators)
  • P = NP in LISP

You can see his research and other papers (under resume) here.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Umm, so....

I've check the date twice, it's not 1st April...

Last I looked there were several implementations of Lisp interpretors that ran on stack machines....

I suspect what this guy really needs to do is read...

Recursion Theory and Joy, although perhaps he should start off with one of the introductory papers to Joy.

Not April 1st but

I found it quite funny.

From the On Insanity part onwards the paper turns into a full blown joke. The conclusion made me laugh.

Seems to be part lisp-weenie satire, while also poking a little fun at the FSF and generally going off at complete tangents towards the end.

Should have put a bit more humour in to start...

I got as far as the first statement, said "That's patently crap", looked at the first Theorem saw a vacuous proof and stopped reading.

At least give me something to chuckle about somewhere between the Abstract and the first proof.

Day of the Beast

I've check the date twice, it's not 1st April...

No, it's 6/6/6, the Day of the Beast. Don't despair however, I saw Christians in a prayer marathon, presumably for the salvation of the Church-Turing Thesis.

Context

Since the author is at the MIT Media Lab, I assume that this should either be seen as an unsubtle dig at CSAIL, or alternatively as a demonstration that the guys at CSAIL are right about the Media Lab. Actually, both interpretations work. ;)

But seriously

Why not to treat Gödel's theorems as just a paradox?
Russel's paradox was treated by abandoning naive set theory in favor of "theory of types", then why not see Gödel's theorems as an evidence of a flaw in meta-logic that allowed proving them, and abandon this meta-logic in favor of a more productive one?

Of course this question must have been asked many times, I just cannot find any reference. Could someone suggest an LtU-like site devoted to logic/epistemology?

Godel's theorems

Russell's paradox exposed a logical contradiction in naive set theory, and therefore had to be abandoned. Also, AFAIK, the most popular replacement nowadays is ZFC set theory which doesn't use classes or any "type" other than set.

Godel's theorems did no such thing. They're perfectly logically consistent (although surprising), so there's no call to abandon anything.

Consistency


Godel's theorems did no such thing. They're perfectly logically consistent (although surprising), so there's no call to abandon anything.

It would be quite strange to have an inconsistent theorem. I wonder what the beast would look like.

Less productive?

abandon this meta-logic in favor of a more productive one?

In what way are you less productive because of Gödel's incompleteness theorems?

No Epigram in Epigram

It was conjectured earlier that writing an interpreter for Epigram in Epigram is impossible because of Gödel's incompleteness theorems (this argument holds for any PL with provably terminating programs).

If this is true, I certainly find such state of science (and philosophy?) as limiting productivity of programmers. Feeling more pragmatist than idealist I suspect this might indicate that a better approach might be possible.

I suspect the "better

I suspect the "better approach" is something along the lines of the proposed general recursion monad for Epigram. I don't think we're going to find a way to beat Gödel directly, the trick's working around the restrictions.

There's nothing

There's nothing "unproductive" about ordinary logic. It just so happens that there's no proof or refutation of every proposition. That shouldn't be a strange phenomenon to a computer programmer; we live with the halting problem every single day.

In fact, you can explain Godel's second incompleteness theorem entirely in terms of computer programs, which really demystifies it. So, let's start with an untyped lambda calculus, and ask the question, which programs halt?

A partial answer to that question lies in typed lambda calculi. If we start with the simply typed lambda calculus, then we know that every term in it will halt. But while every simply-typed term halts, not all halting terms are simply typed. For example, you can't write down recursive programs in the simply-typed lambda calculus, and we know that some (but not all) of them halt.

For example, a program like:

datatype nat = Zero | Succ of nat

fun add n Zero = n
  | add n (Succ m) = Succ (add n m)

will certainly halt. On the other hand, a program like

fun loop () = loop ()

won't halt. The difference between these two programs is that there's an inductive proof that add will halt, and no such proof in the case of loop. So, we add inductive types to our type system, so that we can type some recursive programs. Now, are we done?

No, we're not. If we have a type system that accepts some recursive programs but not others, then, by the halting theorem we know that there must be halting programs our type system rejects.

Now, let's apply the Curry-Howard isomorphism. Programs are proof objects, now, and a halting program is a witness to the truth of a proposition. So the halting theorem tells us that no matter what set of inference rules we come up with, there are witnesses to truths that our inference rules can't verify.

So Godel incompleteness is almost exactly the same thing as the gap that keeps us from deciding whether programs halt. I say "almost", because Godel strengthened this argument to make clear that any sufficiently expressive logic would also have true propositions with no proof that are within the logic.

GT_2


So Godel incompleteness is almost exactly the same thing as the gap that keeps us from deciding whether programs halt. I say "almost", because Godel strengthened this argument to make clear that any sufficiently expressive logic would also have true propositions with no proof that are within the logic.

That is not entirely correct. Predicate logic is in fact complete in the sense of Godel's completness theorem.

The Godel incompleteness theorem applies to a formal theory, not logic(which is not a theory but a language), that is at leat as expressive as some arithmetic (e.g. Peano arithmetic or Robinson arithmetic).

You are quite right about Turing halting problem that can be regarded as a weak sibling of the 1st Godel incompleteness theorem for comp. sci. folks.

GT


why not see Gödel's theorems as an evidence of a flaw in meta-logic that allowed proving them, and abandon this meta-logic in favor of a more productive one?

What Godel theorem do you have in mind ?

If you mean the incompleteness theorem ), then it's a perfectly ordinary mathematical theorem, there is nothing 'meta' about it.


Could someone suggest an LtU-like site devoted to logic/epistemology?

The best way to see what the theorem is about is to go to the source:

http://home.ddc.net/ygg/etext/godel/godel3.htm

This site also has a nice exposition:

http://www.ltn.lv/~podnieks/

Thanks

Coincidentally, Karlis Podnieks (http://www.ltn.lv/~podnieks/ is his homepage) taught me "mathemathical logic" some time ago. He gave me a copy of his book on Gödel's incompleteness theorem, I didn't realize then that I would be interested in this kind of stuff 10 years later.

One of the ideas I have (not sure if I have the skills) is to restate and reprove the incompleteness theorem in light of Curry-Howard correspondence (meta-circular interpreter or a reflective system), so first, it is more accessible to non-logicians, and second, to separate the (meta-) logic used to prove the theorem from the object logic (which will get translated to programming terms).

Just hope I am not too confused.

Podnieks


Coincidentally, Karlis Podnieks (http://www.ltn.lv/~podnieks/ is his homepage) taught me "mathemathical logic" some time ago.>

His exposition is one of the few where the author clearly knows what he's talking about. I am not aware of any other online material as useful except of course the original proof ;)


to separate the (meta-) logic used to prove the theorem from the object logic (which will get translated to programming terms).

I am not sure what you mean. Godel did not use any "metalogic" to prove his theorem unless you use the word metaphorically in which case it's applicable to any formal proof.

Conor McBride on total functions

In a message on the Haskell mailing list Conor McBride writes about total functions. He shows why you can't write an self-interpreter in a total language and discusses the advantages of such a language.

Last time I read about it, Epigram had the Type is a Type rule. This makes it inconsistent by Girard's paradox so not all computations in Epigram terminate and the diagonalisation argument doesn't work. I'm not sure whether this will allow you to use general recursion and write an interpreter.

For the user of Epigram I guess this is a technicality that you won't accidently bump into. It can also be fixed by making Type stratified as in Coq.

Looping Combinator

To come back to my own question:

I'm not sure whether [Type:Type] will allow you to use general recursion and write an interpreter.

Herman Geuvers informs me that Girard's paradox lets you construct a looping combinator. This is a family of terms
Yn : (A:*) (A->A)->A
Yn σ F =β F (Yn+1 σ F).

So, almost a fixed-point combinator and sufficient for Turing equivalence.

Termination Analysis

Found several papers by searching with "termination analysis".

Site down?

I get a 403 Forbidden error when trying to grab the paper (or view his homepage).

I am just back from

I am just back from attending the second day of the origins of computation workshop. The bulk of today's presentation were about the status and meaning of the C-T thesis and whether it can in fact be proven or is just an inutitive notion. Check out the abstracts! Among the people talking today were Martin Davies and Saul Kripke, who know a couple of things about these ideas and Wilfried Sieg, a couple of whose papers about these issues can found here.

I also recommend the Stanford encyclopedia entry. Gandy's work (online?) is apparently what one should read, but I admit I haven't read these papers yet.

Reference

I don't know if you have access to SpringerLink, but Reflections on Gödel's and Gandy's Reflections on Turing's Thesis by David Israel looks relevant.

Programming as an art

The definition of an "effective" method in the Stanford encyclopedia link could be taken as a definition of the programming art with respect to formal mathematics. It is easy to confuse mathematics and programming and one could speculate that this is at the hart of a lot of trouble.
Edit: the expression "logic programming" is a confusing and misleading use of words.