÷ƒ’À; è TeX output 2006.02.20:2002‹ ÿÿÿÿ É ýC ‘Gïhtml:ï html:ŽŽ Ÿ ‘G ýz ïhtml:ï html:Ÿ4 ‘YöóDÓít G® G® cmr17ÄInšŒqterv‘ÿäal–7tAnalysis“Without“In˜terv‘ÿäalsŽŸ ’ ¶/cóX«Q cmr12ÅP•¬raul‘ê¨T‘ÿVa“ylorŽŽŽŽŽŸˆ‹’ §©420–ê¨F‘ÿVebruary“2006ŽŸ ’ ¿ìUó0t‰: cmbx9ÛAbstractŽŸ
¬Ñ‘ ó/o´‹Ç cmr9ÚW‘ÿ:«e–D8argue“that“Dedekind“completeness“and“the“Heine{Borel“propšAÇert¾9y“should“b˜e“seen“as“partŽ¤ ‘ of–p the“\algebraic"“structure“of“the“real“line,‘†¶along“with“the“usual“arithmetic“opAÇerations“andŽ¡‘ relations.‘WDedekind–¾Lcuts“proš¾9vide“a“uniform“and“natural“w˜a˜y“of“form˜ulating“dieren˜tiation,Ž¡‘ inš¾9tegration–)mand“limits.‘ÍÎThey“and“these“examples“also“generalise“to“in˜terv‘ÿ|rals.‘ÍÎT‘ÿ:«ogether“with“theŽ¡‘ arithmetic–Z]order,‘Âcuts“enjoš¾9y“proAÇof-theoretic“in˜troAÇduction“and“elimination“rules“similar“to“thoseŽ¡‘ for–`Ülam¾9bAÇda“abstraction“and“application.‘ÿ This“system“completely“axiomatises“computablyŽ¡‘ con•¾9tin“uous–Tfunctions“on“the“real“line.Ž¡‘&ßüW‘ÿ:«e–ÍLshoš¾9w“ho˜w“this“calculus“(of“\single"“pAÇoin˜ts)“can“bAÇe“translated“formally“in˜to“In˜terv‘ÿ|ralŽ¡‘ Analysis,‘ÅÀin¾9terpreting–±Úthe“arithmetic“opšAÇerations“a“la“Mo˜ore,‘ÅÀand“compactness“as“optimisationŽ¡‘ under–À°constrainš¾9ts.‘…Notice“that“in˜terv‘ÿ|ral“computation“is“the“conclusion“and“not“the“startingŽ¡‘ pAÇoin¾9t.Ž¡‘&ßüThis–Ïcalculus“for“the“real“line“is“part“of“a“more“general“recursiv¾9e“axiomatisation“of“generalŽ¡‘ topAÇology–Tcalled“Abstract“Stone“Dualit¾9y‘ÿ:«.ŽŸÑÄïhtml:ï html:Ÿ@ ó2ÂÖN ff cmbx12Ý1Ž‘LËInŒÌtros3ductionŽŸçóKñ`y
cmr10²Reliable–•ìcomputation“givš¸ães“the“authorit˜y“of“a“theorem“to“the“results“of“n˜umerical“computations,Ž¡bš¸ãy–ñjsetting“in˜terv‘ÿqÇal“bGounds“on“eac˜h“step“of“the“calculation.‘FThis“ma˜y“bGe“done“either“within“theŽ¡xed–”precision“of“macš¸ãhine“arithmetic,‘£²or“b˜y“allo˜wing“this“to“extend“to“as“man˜y“digits“as“ma˜y“bGeŽ¡required.‘0#In–êeither“form,‘Qthis“discipline“usually“ts“inš¸ãto“the“bigger“picture“of“con˜tin˜uous-v‘ÿqÇaluedŽ¡computation–²2bš¸ãy“adapting“tec˜hniques“from“ó3ý ':
cmti10Þnumeric‘ÿ}'al‘º»²analysis.‘ˆ_It“often“doGes“this“b˜y“giving“themŽ¡\double–™vision",‘&XÞi.e.“²computing“uppšGer“and“lo•¸ãw“er–™b˜ounds“where“standard“metho˜ds“wš¸ãould“just“tak˜eŽ¡whatevš¸ãer–UUrounded“v‘ÿqÇalue“the“mac˜hine“arithmetic“pro˜vides.Ž¡‘ The–ÎAphrase“\without“in¸ãterv‘ÿqÇals"“in“the“title“of“this“papGer“signies“that“it“is“part“of“a“programmeŽ¡whose–gªlong“term“motiv‘ÿqÇation“is“to“connect“directly“with“Þthe–ÿ}'or“etic“al‘p3²analysis.‘¨ÇIn–gªthis,‘¬?the“basicŽ¡enš¸ãtities–³èare“Þsingle,–'exact,“r–ÿ}'e“al‘¼q²n˜um˜b•Gers.‘€W‘ÿ*ªe›³èb“egin˜b•¸ãy˜in“troGducing˜a˜calculus˜for˜these,‘ŒcalledŽ¡ÞA¾“bstr‘ÿ}'act–ybStone“Duality‘1A²(ASD),–NÄtogether“with“some“examples“to“sho¸ãw“that“this“is“adequate“forŽ¡Þanalysis‘\k²and–ŠJnot“merely“Þarithmetic².‘¦W‘ÿ*ªe“then“dene“a“formal“translation“that“turns“the“ASDŽ¡calculus–UUinš¸ãto“one“in˜v˜olving“mac˜hine-represen˜table“Þintervals².Ž¡‘ The–theoretical“bGenet“of“(the“a•¸ãv‘ÿqÇailabilit“y–of‘ Ç)“this“translation“is“that“it“eliminates“the“dou-Ž¡ble–æ€vision“of“inš¸ãterv‘ÿqÇal“analysis,‘
Ëin“whic˜h“in˜terv›ÿqÇal“analogues“of“single-v˜alued“concepts“(arithmetic,Ž¡trigonometry‘ÿ*ª,–(Rdierenš¸ãtiation,“Banac˜h–þspaces“...)‘l&ha˜v˜e“to“bGe“devised“Þad‘/0ho‘ÿ}'c²,›(Rone“at“a“time,˜in“aŽ¡fashion–£7that“gets“increasingly“estranged“from“an¸ãy“theoretical“rošGots.‘6hReal“analysis“can“b˜e“dev¸ãelop˜edŽ¡within–cASD‘Sin“a“single-v‘ÿqÇalued“stš¸ãyle“that“is“v˜ery“similar“to“the“traditional“one,‘!`and“then“Þtr–ÿ}'anslate“dŽ¡²in•¸ãto‘UUin“terv›ÿqÇals.‘qÇIn“terv˜als–UUare“therefore“the“outcome“and“not“the“starting“pšGoin¸ãt“of“the“metho˜d.Ž¡‘ This–|ÂpapšGer“adv¸ão˜cates“some“v¸ãery“heretical“views“ab˜out“the“foundations“of“real“and“in¸ãterv‘ÿqÇalŽ¡analysis.‘½9Y‘ÿ*ªou–n{can“either“burn“me“at“the“stakš¸ãe“for“blasphem˜y‘ÿ*ª,‘´Äor“opGen“y˜our“mind“to“the“v˜eryŽ¡simple–¸ and“natural“argumenš¸ãts“that“I‘¸xgiv˜e“here.‘=‹It“is“true“that“these“bGenet“from“the“enligh˜tenmen˜tŽ¡that–Hwš¸ãas“pro˜vided“in“the“20th“cen˜tury“b˜y“proGof“theory‘ÿ*ª,‘JÀlam˜bGda“calculus,›JÀcategory“theory‘ÿ*ª,˜domainŽ¡theory‘ÿ*ª,‘!ûdenotational–ù
semanš¸ãtics“and“the“theory“of“con˜tin˜uous“lattices.‘\ðThese“disciplines“are“no˜wŽ¡practised–¹3in“computer“science“departmenš¸ãts,‘Ò*but“most“of“the“mathematics“that“appGears“here“w˜asŽ¡already–UUfamiliar“in“the“19th“cen¸ãtury‘ÿ*ª.ŽŽŸ ’ ãÜQ1ŽŽŒ‹ * É ýC ‘Gïhtml:ï html:ŽŽ Ÿ ý„ ‘!G²The–ü6widely“made“assertion“that“mathematics“is“founded“on“set“theory“blatan¸ãtly“disregards“theŽ¤ ‘Ghistorical–
^evidence.‘™âThis“is“particularly“so“in“the“case“of“the“aspGects“of“\innitesimal“calculus"Ž¡‘Gthat–ßunderlie“the“v‘ÿqÇast“ma‘ Ž8joritš¸ãy“of“n˜umerical“tec˜hniques.‘[ The“F‘ÿ*ªourier“represen˜tation“of“reasonablyŽ¡‘Gw•¸ãell›£bGeha“v“ed˜functions,–ï·for˜example,“w•¸ãas˜dev“elopGed˜b“y˜Diric“hlet˜and˜others˜in˜the˜Þe‘ÿ}'arly‘€ ²19thŽ¡‘Gcen•¸ãtury.‘ÇXIt›Ç0w“as˜only˜Can“tor's˜Þsubse‘ÿ}'quent‘º²disco“v“ery˜that˜some˜extremely˜unpleasan“t˜\functions"Ž¡‘Gcould–úYalso“bšGe“represen¸ãted“p˜oin•¸ãt“wise›úYb“y˜trigonometric˜series˜that˜led˜him˜to˜the˜in“v“en“tion˜of˜setŽ¡‘Gtheory‘ÿ*ª.‘oFAlong–MÓwith“this“came“fanš¸ãtastical“innities,‘OSon“whic˜h“sub‘ Ž8ject“he“felt“mo˜v˜ed“to“oer“adviceŽ¡‘Gto–Hathe“V‘ÿ*ªatican“[ï%html:Dau79ï html:Ž‘1Ì].‘mvBesides“generating“wš¸ãell“kno˜wn“parado˜xes“during“its“history‘ÿ*ª,‘Jøset“theory“isŽ¡‘Gcomputationally‘UUmeaningless.Ž¡‘!GEuclidean–>™geometry“wš¸ãas“axiomatised“using“natural“ideas“suc˜h“as“lines“and“circles,‘C%so“topGologyŽ¡‘Gshould–Ïalso“treat“sucš¸ãh“things“as“opGen“and“compact“subspaces“as“its“primitiv˜es.‘EThen,›éïof“course,˜w¸ãeŽ¡‘Gmš¸ãust–›Onot“fall“in˜to“the“trap“of“referring“to“a“Þset‘Ž'²or“Þc–ÿ}'ol‘ ‚Øle“ction‘_²²[ï&html:F‘ÿ*ªef77ï html:Ž‘1Ë]–›Oof“opGen“subspaces:‘ý»MarshallŽ¡‘GStone–?˜advised“us“\alw•¸ãa“ys–?˜topšGologize",‘Cñso“these“to˜o“form“a“Þsp–ÿ}'ac“e²,‘Cñwhose–?˜(non-Hausdor‘ Ç)“top˜ologyŽ¡‘Gis–£Fnoš¸ãw“called“after“Dana“Scott.‘6mCarrying“out“this“plan,‘Æãw˜e“obtain“an“axiomatisation“of“loGcally“com-Ž¡‘Gpact–îspaces“that,‘¿since“it“wš¸ãas“nev˜er“pGolluted“b˜y“set-theoretic“ingredien˜ts,‘¿is“inheren˜tly“computableŽ¡‘G[ï$html:Gï html:Ž‘Øä].‘X%Curiously‘ÿ*ª,›üthe–÷tdescription“of“opGen“and“closed“subspaces“using“con•¸ãtin“uous‘÷tfunctions,˜ratherŽ¡‘Gthan–·as“set-theoretic“complemenš¸ãts,‘=leads“to“a“v˜ery“strong“dualit˜y“bGet˜w˜een“them“that“pGerv‘ÿqÇades“theŽ¡‘Gtheory‘ÿ*ª.‘¶åIt–l_also“makš¸ães“the“argumen˜ts“loGok“more“similar“to“classical“ones“than“to“in˜tuitionistic“butŽ¡‘Gset-based–UUtheories“[ï$html:Jï html:Ž‘#].Ž‘GŸ‘Äïhtml:ï html:Ÿ€ Ý2Ž‘LËNatural–ffaxioms“for“the“real“lineŽŸç²W‘ÿ*ªe–€shall“concenš¸ãtrate“on“the“part“of“the“theory“that“applies“to“the“real“line.‘ñÞThe“argumen˜ts“thatŽ¡Þe‘ÿ}'quality‘»ä²of–Ùgarbitrary“real“n•¸ãum“bGers–Ùgcan“nevš¸ãer“the“pro˜v˜ed“computationally“ha˜v˜e“bGeen“w˜ell“rehearsed.Ž¡ÞIne‘ÿ}'quality‘—å²and–µhthe“Þstrict‘¨@²arithmetical“ordering“of“n•¸ãum“bGers,›Ímon–µhthe“other“hand,˜can“bGe“witnessedŽ¡bš¸ãy–UUcomputing“them“sucien˜tly“precisely‘ÿ*ª.Ž¡‘ Therefore,–UUbšGesides“the“usual“arithmetic“op˜erations“+,“ó
!",š
cmsy10¸ ²,“¸“²and“¸²,Ž¡‘
ÿÿ¸ŽŽŽ‘ Þr–ÿ}'e“al‘]Þ²n•¸ãum“bGers–UUadmit“the“observ‘ÿqÇable“relations“ó
b>
cmmi10µ<²,“µ>“²and“¸6²=“but“not“¸²,“¸“²or“=,Ž© ‘
ÿÿ¸ŽŽŽ‘ ²whereas–UUÞinte›ÿ}'gers‘'v²and“Þr˜ational‘]Þ²n•¸ãum“bGers–UUadmit“all“six“of“them.Ž¡T–ÿ*ªopšGologically“,‘w*this–pfis“b˜ecause“óˆ¶È
msbm10¾R“²is“ÞHausdor‘Žú²but“not“Þdiscr‘ÿ}'ete²,‘w*whereas“¾N“²and“¾Q“²ha•¸ãv“e–pfb˜oth“prop-Ž¡erties.ŽŸ ‘ Notice–˹that“there“is“an“asymmetry“bGet•¸ãw“een–˹things“that“are“classically“negativ¸ães“of“one“another.Ž¡Indeed,‘ïrlogical–Пnegation“(¸:²)“will“not“bšGe“allo•¸ãw“ed–Пin“our“calculus.‘ã¦It“do˜es“p˜ermit“conjunction“(¸^²)Ž¡and–õdisjunction“(¸_²)“of“propšGerties,‘since“these“ma¸ãy“b˜e“understo˜o˜d“in“terms“of“running“pro˜cessesŽ¡serially–UUor“in“parallel.‘qÇIn“this“setting,Ž¡‘
ÿÿ¸ŽŽŽ‘ ²\truth"–UUof“a“propGosition“(¸>²)“amounš¸ãts“to“Þtermination‘¸²of“a“program,“whic˜h“is“Þobservable²,Ž¦‘
ÿÿ¸ŽŽŽ‘ ²and–UU\falsitš¸ãy"“(¸?²)“to“Þdiver–ÿ}'genc“e²,–UUwhic˜h“is“not.Ž¡Negation›fù(in•¸ãterc“hanging˜¸>˜²with˜¸?²)˜is˜forbidden˜computationally‘ÿ*ª.‘"SThis˜is˜bGecause˜it˜w“ould˜solv“e˜theŽ¡Þhalting‘Ï#pr‘ÿ}'oblem²,‘¥Ðwhicš¸ãh–•¸Alan“T‘ÿ*ªuring“taugh˜t“us“w˜as“impGossible“[ï%html:T‘ÿ*ªur35ï html:Ž‘Üu].‘2ïAn“excellen˜t“in˜troGductionŽ¡to–°ìthe“kind“of“logic“con
ated“with“topGology“and“computation“that“wš¸ãe're“using“w˜as“giv˜en“in“[ï%html:Vic88ï html:Ž‘¸ç],Ž¡though–UUthis“pGoinš¸ãt“of“view“has“mo˜v˜ed“on“somewhat“since“that“b•Go“ok–UUw˜as“written.Ž¡‘ Since–‚qwš¸ãe“in˜tend“to“manipulate“logical“expressions“in“the“same“w˜a˜y“as“arithmetical“ones,‘¬Ÿw˜e“needŽ¡to–Œ^givš¸ãe“a“name“to“their“t˜yp•Ge:‘
K.‘.ÊT›ÿ*ªop“ologically˜,‘´this–Œ^is“called“the“ÞSierpiAl‘ú¢$nski‘Ûsp–ÿ}'ac“e‘L¹²and–Œ^(classically)“itŽŸØälošGoks–lik¸ãe“Ÿôæ`ó ú±u
cmex10«ŽŽŽŸü
€‘ ö¸ŽŽŸ±È‘
g…ŽŽŽ‘ËŸôæ`«ŽŽŽŽ‘Ãø²,‘ìwith“one“op˜en“p˜oinš¸ãt“¸>“²and“one“closed“one“¸?².‘YT‘ÿ*ªo“C,“C++“and“Ja˜v‘ÿqÇa“programmers,ŽŸJ«–D1is“knoš¸ãwn“as“ó4ßê