Lambda the Ultimate

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.

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.

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.

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.

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.

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?

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 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 "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.

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.

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/

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.

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.

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.

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
Y_n : (A:*) (A->A)->A
Y_n σ F =_β F (Y_n+1 σ F).

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

Wikipedia entry, and homepage . previously mentioned.

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.

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.