• Log InLog In
  • Register
Liquid`
Team Liquid Liquipedia
EDT 21:28
CEST 03:28
KST 10:28
  • Home
  • Forum
  • Calendar
  • Streams
  • Liquipedia
  • Features
  • Store
  • EPT
  • TL+
  • StarCraft 2
  • Brood War
  • Smash
  • Heroes
  • Counter-Strike
  • Overwatch
  • Liquibet
  • Fantasy StarCraft
  • TLPD
  • StarCraft 2
  • Brood War
  • Blogs
Forum Sidebar
Events/Features
News
Featured News
Maestros of the Game: Week 1/Play-in Preview5[ASL20] Ro24 Preview Pt2: Take-Off7[ASL20] Ro24 Preview Pt1: Runway132v2 & SC: Evo Complete: Weekend Double Feature4Team Liquid Map Contest #21 - Presented by Monster Energy9
Community News
Weekly Cups (Aug 18-24): herO dethrones MaxPax6Maestros of The Game—$20k event w/ live finals in Paris36Weekly Cups (Aug 11-17): MaxPax triples again!13Weekly Cups (Aug 4-10): MaxPax wins a triple6SC2's Safe House 2 - October 18 & 195
StarCraft 2
General
#1: Maru - Greatest Players of All Time Maestros of the Game: Week 1/Play-in Preview Greatest Players of All Time: 2025 Update BoxeR's Wings Episode 2 - Fan Translation A Eulogy for the Six Pool
Tourneys
Kirktown Chat Brawl #8 - 4.6K max Tonight Maestros of The Game—$20k event w/ live finals in Paris LiuLi Cup - August 2025 Tournaments $5,000 WardiTV Summer Championship 2025 $5,100+ SEL Season 2 Championship (SC: Evo)
Strategy
Custom Maps
External Content
Mutation # 488 What Goes Around Mutation # 487 Think Fast Mutation # 486 Watch the Skies Mutation # 485 Death from Below
Brood War
General
Post ASL20 Ro24 discussion. BGH Auto Balance -> http://bghmmr.eu/ Easiest luckies way to get out of Asl groups BW General Discussion No Rain in ASL20?
Tourneys
[ASL20] Ro24 Group F Cosmonarchy Pro Showmatches [IPSL] CSLAN Review and CSLPRO Reimagined! [ASL20] Ro24 Group E
Strategy
Simple Questions, Simple Answers Muta micro map competition Fighting Spirit mining rates [G] Mineral Boosting
Other Games
General Games
Path of Exile General RTS Discussion Thread Mechabellum Nintendo Switch Thread Stormgate/Frost Giant Megathread
Dota 2
Official 'what is Dota anymore' discussion
League of Legends
Heroes of the Storm
Simple Questions, Simple Answers Heroes of the Storm 2.0
Hearthstone
Heroes of StarCraft mini-set
TL Mafia
TL Mafia Community Thread Vanilla Mini Mafia
Community
General
US Politics Mega-thread Russo-Ukrainian War Thread YouTube Thread Things Aren’t Peaceful in Palestine Canadian Politics Mega-thread
Fan Clubs
INnoVation Fan Club SKT1 Classic Fan Club!
Media & Entertainment
Anime Discussion Thread Movie Discussion! [Manga] One Piece [\m/] Heavy Metal Thread
Sports
2024 - 2026 Football Thread Formula 1 Discussion TeamLiquid Health and Fitness Initiative For 2023
World Cup 2022
Tech Support
Computer Build, Upgrade & Buying Resource Thread High temperatures on bridge(s) Gtx660 graphics card replacement
TL Community
The Automated Ban List TeamLiquid Team Shirt On Sale
Blogs
hello world
radishsoup
Lemme tell you a thing o…
JoinTheRain
How Culture and Conflict Imp…
TrAiDoS
RTS Design in Hypercoven
a11
Evil Gacha Games and the…
ffswowsucks
INDEPENDIENTE LA CTM
XenOsky
Customize Sidebar...

Website Feedback

Closed Threads



Active: 996 users

What is a PhD? - Page 27

Forum Index > General Forum
Post a Reply
Prev 1 25 26 27 28 29 Next All
sam!zdat
Profile Blog Joined October 2010
United States5559 Posts
September 09 2013 16:22 GMT
#521
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.
shikata ga nai
Kambing
Profile Joined May 2010
United States1176 Posts
Last Edited: 2013-09-09 17:05:55
September 09 2013 17:05 GMT
#522
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
Profile Blog Joined October 2010
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?
shikata ga nai
Slaughter
Profile Blog Joined November 2003
United States20254 Posts
Last Edited: 2013-09-09 17:52:11
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.
Never Knows Best.
sam!zdat
Profile Blog Joined October 2010
United States5559 Posts
September 09 2013 17:55 GMT
#525
^mission accomplished! :D

opinions, arguments, and egos are what make life worth living
shikata ga nai
Slaughter
Profile Blog Joined November 2003
United States20254 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.
Never Knows Best.
Kambing
Profile Joined May 2010
United States1176 Posts
Last Edited: 2013-09-09 18:22:58
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
Profile Blog Joined October 2010
United States5559 Posts
September 09 2013 18:46 GMT
#528
what does it mean for a type system to be stronger or weaker?
shikata ga nai
Kambing
Profile Joined May 2010
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
Profile Blog Joined October 2010
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?
shikata ga nai
Kambing
Profile Joined May 2010
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
Profile Blog Joined October 2010
United States5559 Posts
Last Edited: 2013-09-09 19:52:13
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
shikata ga nai
ZenithM
Profile Joined February 2011
France15952 Posts
Last Edited: 2013-09-09 19:45:04
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
Profile Joined February 2011
France15952 Posts
Last Edited: 2013-09-09 19:44:54
September 09 2013 19:44 GMT
#534
Edit: Oh god, sorry for that.
Kambing
Profile Joined May 2010
United States1176 Posts
September 09 2013 20:00 GMT
#535
Every french programming languages researcher I know is ultra awesome. Go France. =D
MoltkeWarding
Profile Joined November 2003
5195 Posts
Last Edited: 2013-09-09 20:31:36
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
Profile Blog Joined November 2005
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
We have fed the heart on fantasies, the heart's grown brutal from the fare, more substance in our enmities than in our love
frogrubdown
Profile Blog Joined June 2011
1266 Posts
Last Edited: 2013-09-10 02:38:48
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
sam!zdat
Profile Blog Joined October 2010
United States5559 Posts
September 10 2013 02:48 GMT
#539
haha what is that from?
shikata ga nai
frogrubdown
Profile Blog Joined June 2011
1266 Posts
September 10 2013 02:50 GMT
#540
Crank email. I get them pretty regularly, but usually they don't threaten me with damnation...
Prev 1 25 26 27 28 29 Next All
Please log in or register to reply.
Live Events Refresh
Next event in 10h 33m
[ Submit Event ]
Live Streams
Refresh
StarCraft 2
SpeCial 132
RuFF_SC2 131
Nina 75
StarCraft: Brood War
sSak 1127
Shuttle 697
NaDa 25
Dota 2
monkeys_forever191
Super Smash Bros
AZ_Axe167
Other Games
tarik_tv36270
gofns16594
summit1g9213
JimRising 437
WinterStarcraft164
ViBE51
ROOTCatZ10
kaitlyn1
Organizations
Other Games
gamesdonequick1856
BasetradeTV31
StarCraft 2
Blizzard YouTube
StarCraft: Brood War
BSLTrovo
sctven
[ Show 13 non-featured ]
StarCraft 2
• davetesta92
• AfreecaTV YouTube
• intothetv
• Kozan
• IndyKCrew
• LaughNgamezSOOP
• Migwel
• sooper7s
StarCraft: Brood War
• BSLYoutube
• STPLYoutube
• ZZZeroYoutube
League of Legends
• Doublelift4425
• Scarra1111
Upcoming Events
SC Evo League
10h 33m
Maestros of the Game
14h 33m
SHIN vs Creator
Astrea vs Lambo
Bunny vs SKillous
HeRoMaRinE vs TriGGeR
BSL Team Wars
17h 33m
Team Bonyth vs Team Sziky
BSL Team Wars
17h 33m
Team Dewalt vs Team Sziky
Afreeca Starleague
1d 8h
Soulkey vs BeSt
Snow vs Light
Monday Night Weeklies
1d 14h
Replay Cast
1d 22h
Sparkling Tuna Cup
2 days
PiGosaur Monday
2 days
LiuLi Cup
3 days
[ Show More ]
Replay Cast
3 days
The PondCast
4 days
RSL Revival
4 days
Maru vs SHIN
MaNa vs MaxPax
RSL Revival
5 days
Reynor vs Astrea
Classic vs sOs
BSL Team Wars
5 days
Team Bonyth vs Team Dewalt
CranKy Ducklings
6 days
RSL Revival
6 days
GuMiho vs Cham
ByuN vs TriGGeR
Cosmonarchy
6 days
TriGGeR vs YoungYakov
YoungYakov vs HonMonO
HonMonO vs TriGGeR
[BSL 2025] Weekly
6 days
Liquipedia Results

Completed

Acropolis #4 - TS1
WardiTV Summer 2025
HCC Europe

Ongoing

Copa Latinoamericana 4
BSL 20 Team Wars
KCM Race Survival 2025 Season 3
BSL 21 Qualifiers
ASL Season 20
CSL Season 18: Qualifier 2
Maestros of the Game
SEL Season 2 Championship
Sisters' Call Cup
BLAST Open Fall Qual
Esports World Cup 2025
BLAST Bounty Fall 2025
BLAST Bounty Fall Qual
IEM Cologne 2025
FISSURE Playground #1
BLAST.tv Austin Major 2025

Upcoming

CSL 2025 AUTUMN (S18)
LASL Season 20
2025 Chongqing Offline CUP
BSL Season 21
BSL 21 Team A
Chzzk MurlocKing SC1 vs SC2 Cup #2
EC S1
BLAST Rivals Fall 2025
Skyesports Masters 2025
IEM Chengdu 2025
PGL Masters Bucharest 2025
MESA Nomadic Masters Fall
Thunderpick World Champ.
CS Asia Championships 2025
ESL Pro League S22
FISSURE Playground #2
BLAST Open Fall 2025
TLPD

1. ByuN
2. TY
3. Dark
4. Solar
5. Stats
6. Nerchio
7. sOs
8. soO
9. INnoVation
10. Elazer
1. Rain
2. Flash
3. EffOrt
4. Last
5. Bisu
6. Soulkey
7. Mini
8. Sharp
Sidebar Settings...

Advertising | Privacy Policy | Terms Of Use | Contact Us

Original banner artwork: Jim Warren
The contents of this webpage are copyright © 2025 TLnet. All Rights Reserved.