On September 10 2013 01:22 sam!zdat wrote:
that's true, but incompleteness I think is not really nearly as big a deal as people think it is. It's sort of just a silly trick, really.

It is a (relatively) big deal, insofar as its implications towards the foundations of mathematics (i.e., Hilbert's program) and computer science (linking proof and program construction) goes.

sam!zdat

United States5559 Posts

September 09 2013 17:19 GMT

#523

sure. I guess what I'm saying is that I think there are much bigger problems in computation (namely computational irreducibility and p-np etc) than godel's proof, which relies on a particular sort of self referential statemtn which I'm not sure is really all that interesting philosophically. I don't know about those problems in computer science, can you explain to a layman?

Slaughter

United States20255 Posts

September 09 2013 17:50 GMT

#524

I chuckled to myself when I passed through the political science dept this morning because I thought of this thread.

One thing is for sure: get a bunch of PhDs and PhD students into one thread and you won't be short on opinions, arguments, and egos.

sam!zdat

United States5559 Posts

September 09 2013 17:55 GMT

#525

^mission accomplished! :D

opinions, arguments, and egos are what make life worth living

Slaughter

United States20255 Posts

September 09 2013 18:00 GMT

#526

On September 10 2013 02:55 sam!zdat wrote:
^mission accomplished! :D

opinions, arguments, and egos are what make life worth living

They are fun, until people take them far too seriously. Which happens all the time >_> Though most of the drama in my department hasn't happened due to academic arguments but personal drama lul.

Kambing

United States1176 Posts

September 09 2013 18:21 GMT

#527

On September 10 2013 02:19 sam!zdat wrote:
sure. I guess what I'm saying is that I think there are much bigger problems in computation (namely computational irreducibility and p-np etc) than godel's proof, which relies on a particular sort of self referential statemtn which I'm not sure is really all that interesting philosophically. I don't know about those problems in computer science, can you explain to a layman?

Yeah. Incompleteness is surely not a topic that directly affects all of computation (or philosophy for that matter). But it certainly affects its foundational core. I think what's neat here is that what was once a paradoxical parlor trick in philosophy and logic has pragmatic consequence in computing.

The short story is that computer programs and proof share a close relationship. In programming languages, a type system classifies values and expressions used in computation. For example, the expressions 5, 10 * 10, and abs(-5) + 1 all have type int, the type of integers, in most programming languages. Another way to state of the relationship between types and expressions is that these expressions inhabit the type int.

Virtually all programming languages have a notion of a function which you can think of as a box that when, given some input, produces some output. For example, abs(-5) is an example of a call to the abs function that takes -5 as input and produces 5 as output. Functions themselves also have a type, typically written A ->B to stand for a function that takes as input values of type A and produce output values of type B. We would say that abs has type int -> int.

If you are familiar with propositional logic, then the notation A -> B should not be unfamiliar. This is how you write an implication in logic where A -> B stands for the proposition that "assuming A holds then B holds". For example A -> A is a tautology because something always implies itself.

The choice of arrow notation for function types is not a coincidence. The Curry-Howard Isomorphism outlines how we can interpret a value of a certain type (in a computer program) as a proof of that type interpreted as a logical proposition. For example, we can read the int -> int function type as stating the proposition "If you give me an int, I can produce an int". The abs function is "proof" that this proposition holds because it is a realization of that statement. Thus in general, any computer program is a "proof" of its type.

For traditional programming languages this correspondence is less interesting because the type systems (read: logics) of those languages are relatively weak. However, for languages with stronger type systems (of which Haskell is one), this correspondence becomes very important as we can prove properties about our program's behavior by creating programs that obey certain types. Because we can think of a type system of a programming language as a logic, Godel's incompleteness theorem puts an upper bound on the strength of any programming language's type system.

sam!zdat

United States5559 Posts

September 09 2013 18:46 GMT

#528

what does it mean for a type system to be stronger or weaker?

Kambing

United States1176 Posts

September 09 2013 19:03 GMT

#529

On September 10 2013 03:46 sam!zdat wrote:
what does it mean for a type system to be stronger or weaker?

Broadly this means that a stronger type system can give better, more precise types to more programs than a weaker type system. A practical example, in most programming languages (e.g., Java), the conditional expression:


if e1 then e2 else e3

Requires that expression e1 have a boolean type and expressions e2 and e3 have the same types. Thus the overall type of the conditional is whatever the (shared) types of e2 and e3 are. The conditional:


if x < 5 then 0 else "hello"

is ill-typed in these languages because 0 has type int and "hello" has type string. However, this is not an inherent fundamental limitation of type systems in general, just a limitation of this particular type system. One can imagine an alternative type system where the conditional expression above has type int ^ string, the union of the types int and string. Such a type system would be able to give a type to this expression that a weaker type system would have to reject but would be more complex as a result.

sam!zdat

United States5559 Posts

September 09 2013 19:06 GMT

#530

ah, so then if you get a sufficiently strong type system all of the sudden you enable self-referential godel statements and the thing collapses?

Kambing

United States1176 Posts

September 09 2013 19:21 GMT

#531

On September 10 2013 04:06 sam!zdat wrote:
ah, so then if you get a sufficiently strong type system all of the sudden you enable self-referential godel statements and the thing collapses?

Nah, in some sense stronger type systems constrain the potential bad behavior of programs it cannot characterize in a sound way. However, the worry that you describe is precisely the line that we have to thread when building these sorts of languages.

Where mathematical foundations and PL meet is in the realm of proof assistants such as Coq and Agda. Here, the type systems are strong enough that the types can encode honest-to-god logical statements and the programs are (constructive) proofs of those propositions. Just to give a flavor of what this looks like, here is a statement of a type/proposition and program/proof in Coq that n + 0 = n for any natural number n:


plus_n_O : forall n: nat, n = n + 0 =
  fun n : nat => nat_ind (fun n0: nat => n0 = n0 + 0) eq_refl
    (fun (n0: nat) (IHn: n0 = n0 + 0) => f_equal S IHn) n

Coq contains a full-fledged (dependently-typed) programming language. However, it restricts the use of recursion (i.e., functions that can call themselves) in a particular way that other programming languages allow. This is precisely because of what you described. If Coq allowed (general) recursion, then its underlying type system/logic would become inconsistent and you could manufacture proofs of anything out of thin air.

sam!zdat

United States5559 Posts

September 09 2013 19:26 GMT

#532

'manufacture proofs of anything out of thin air'? That sounds like what we do in the english department! (probably because natural language is very badly designed and allows us to make recursive statements and prove anything because A&~A)

anyway, thanks for explaining. I think I understand what you are saying

ZenithM

France15952 Posts

September 09 2013 19:44 GMT

#533

Protip: Coq is french. (yay!)
And nice to see some theoretical computer science in this thread, cheers :D

ZenithM

France15952 Posts

September 09 2013 19:44 GMT

#534

Edit: Oh god, sorry for that.

Kambing

United States1176 Posts

September 09 2013 20:00 GMT

#535

Every french programming languages researcher I know is ultra awesome. Go France. =D

MoltkeWarding

5195 Posts

September 09 2013 20:31 GMT

#536

On September 10 2013 02:55 sam!zdat wrote:
^mission accomplished! :D

opinions, arguments, and egos are what make life worth living

I thought so too, then I fell in love. Then I fell out of love, and now I'm back in my hamster cage surrounded by my faithful friends, Mr. Opinion and Mme. Prejudice.

oneofthem

Cayman Islands24199 Posts

September 09 2013 22:09 GMT

#537

On September 10 2013 04:26 sam!zdat wrote:
'manufacture proofs of anything out of thin air'? That sounds like what we do in the english department! (probably because natural language is very badly designed and allows us to make recursive statements and prove anything because A&~A)

anyway, thanks for explaining. I think I understand what you are saying

oh dear, this one is sentient! :D

frogrubdown

1266 Posts

September 10 2013 02:37 GMT

#538

[snip]

PS ADVISE TO ALL UNDERGRAD AND GRADUATE STUDENTS IN PHILOSOPHY, BELIEVE JESUS CHRIST SON OF GOD, NOT [a metaphysician in my department], ABOUT WHAT HAPPENS WHEN YOU DIE.

Sometimes being a PhD student is wonderful