EPTWhat is a PhD? - Page 27
| Forum Index > General Forum |
|
sam!zdat
United States5559 Posts
| ||
|
Kambing
United States1176 Posts
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
| ||
|
Slaughter
United States20254 Posts
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
opinions, arguments, and egos are what make life worth living | ||
|
Slaughter
United States20254 Posts
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
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
| ||
|
Kambing
United States1176 Posts
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:
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:
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
| ||
|
Kambing
United States1176 Posts
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:
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
anyway, thanks for explaining. I think I understand what you are saying | ||
|
ZenithM
France15952 Posts
And nice to see some theoretical computer science in this thread, cheers :D | ||
|
ZenithM
France15952 Posts
| ||
|
Kambing
United States1176 Posts
| ||
|
MoltkeWarding
5195 Posts
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
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
[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  | ||
|
sam!zdat
United States5559 Posts
| ||
|
frogrubdown
1266 Posts
| ||
| ||
