= 27d567bc2d48d9f40e9ccc20ea370b15)
Skatche comments on No coinductive datatype of integers - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (138)
I deem this obnoxious.
A proof in ROT13:
Gb rnpu cbffvoyr rapbqvat bs n pbhagnoyr frg ol svavgr ovg fgevatf gurer pbeerfcbaqf n ovanel gerr: ng gur ebbg abqr lbh tb yrsg (fnl) vs gur svefg ovg vf n mreb naq evtug vs vg'f n bar, gura ng gur arkg abqr lbh tb yrsg be evtug vs gur frpbaq ovg vf n mreb be bar, naq fb sbegu. Gur npghny vagrtref pbeerfcbaq gb grezvany abqrf, ernpurq ol n svavgr ahzore bs oenapuvatf. Znysbezrq ovg fgevatf, gbb, pbeerfcbaq gb grezvany abqrf, ng gur rneyvrfg cbvag gung jr pna gryy gurl'er znysbezrq. Ubjrire, fvapr gurer ner vasvavgryl znal vagrtref, naq bayl svavgryl znal cbffvoyr ovg fgevatf bs nal tvira yratgu, gurer zhfg or ng yrnfg bar vasvavgryl ybat cngu va gur gerr, naq vs jr srrq guvf frdhrapr bs mrebf naq barf vagb bhe pbzchgre, gur pbzchgre jvyy unat.
You seem to have left out the part of the proof where you do the actual work! ROT13'd:
Fxngpur fubjf gung gurer zhfg or neovgenevyl ybat cnguf; gur ceboyrz abj vf gb fubj gung gurer vf na vasvavgryl ybat cngu. Jr pbafgehpg guvf cngu nf sbyybjf: Fvapr gurer ner vasvavgryl znal cnguf, gurer ner rvgure vasvavgryl znal cnguf fgnegvat jvgu 0, be vasvavgryl znal cnguf fgnegvat jvgu 1. Vs gur sbezre ubyqf, fgneg jvgu 0, bgurejvfr fgneg jvgu 1. Fvapr juvpurire qvtvg jr cvpxrq, gurer ner vasvavgryl znal fgnegvat jvgu vg, jr pna ybbx ng gur arkg qvtvg naq ercrng guvf cebprff. Fvapr jr pna ercrng guvf neovgenevyl, guvf trgf hf na vasvavgryl ybat cngu. Va trareny guvf nethzrag trgf lbh jung'f xabja nf Xbavt'f Yrzzn.
Sorry, I have a bit of a skewed perspective about what's obvious. :P Once I perceived the connection to binary trees it seemed plain as day.
I find that for me, and many other people I know in the mathematics department of my university, once infinities, uncountability, and such enter the picture, the accuracy of intuition quickly starts to diminish, so it's wise to be careful and make sure the proof is complete before declaring it obvious. As a good example, note how surprising and notable Cantor's diagonal argument seemed the first time you heard it- it isn't obvious that the reals aren't countable when you don't already know that, so you might start trying to construct a counting scheme and end up with one that "obviously" works.