Well-founded-Iterations-of-ITTMs成立的迭代ittms课件

RelationstoWolfram’swork:Goodprojectforanordinalanalysis:justbeyondthestrongestcurrentlyanalyzedsystemRelationstoWolfram’swork:Goodprojectforanordinalanalysis:justbeyondthestrongestcurrentlyanalyzedsystemIterationandhyper-iteration/feedbackEx: a)Fixedpointsofinductivedefinitions:iterateddefinitions(Pohlers),inductivedefinitionswithfeedback–theμ-calculus(Möllerfeld)Iterationandhyper-iteration/feedbackExamples: a)Fixedpointsofinductivedefinitions:iterateddefinitions(Pohlers),inductivedefinitionswithfeedback–theμ-calculus(Möllerfeld) b)Turingjump:IterationalonganyordinalgeneratedalongthewayyieldsthehyperarithmeticsetsIterationandhyper-iteration/feedbackExamples: a)Fixedpointsofinductivedefinitions: theμ-calculus b)Turingjump:hyperarithmeticsets c)InfinitetimeTuringmachines:???InfinitetimeTuringmachine (Hamkins&Lewis):aregularTuringmachinewithlimitstages.Atalimitstage:machineisinadedicatedstateheadisonthe0thcellcontentofacellislimsupofthepreviouscontents (i.e.0ifeventually0,1ifeventually1,1ifcofinallyalternating)definitionsRωiswritableif itscharacteristicfunctionisontheoutputtapeattheendofahaltingcomputation.Anordinalαiswritableif somerealcodingα(viasomestandardrepresentation)iswritable.λ:=sup{α|αiswritable}proposition

RωiswritableiffRLλ.definitionsRωiseventuallywritableif itscharacteristicfunctionisontheoutputtape,nevertochange,ofacomputation.Anordinalαiseventuallywritableif somerealcodingα(viasomestandardrepresentation)iseventuallywritable.ζ:=sup{α|αiseventuallywritable}prop

RωiseventuallywritableiffRLζ.definitionsRωisaccidentallywritableif itscharacteristicfunctionisontheoutputtapeatanytimeduringacomputation.Anordinalαisaccidentallywritableif somerealcodingα(viasomestandardrepresentation)isaccidentallywritable.Σ:=sup{α|αisaccidentallywritable}prop

RωisaccidentallywritableiffRLΣSummary:

λ=supwritables ζ=supeventuallywritables Σ=supaccidentallywritablesClearly,λ≤ζ≤Σ.Summary:

λ=supwritables ζ=supeventuallywritables Σ=supaccidentallywritablesClearly,λ≤ζ≤Σ.theorem(Welch)ζistheleastordinalαsuchthatLαhasaΣ2-elementaryextension. (ζistheleastΣ2-extendibleordinal.) TheordinalofthatextensionisΣ. LλistheleastΣ1-elementarysubstructureofLζ.Timetoiterate–def0▼={(e,x)|φe(x)↓(i.e.converges)}Timetoiterate–def0▼={(e,x)|φe(x)↓(i.e.converges)}propThedefinitionsofλ,ζ,andΣrelativize(toλ▼,ζ▼,andΣ▼)tocomputationsfrom0▼. Furthermore,ζ▼istheleastΣ2-extendiblelimitofΣ2-extendibles,theordinalofitsΣ2extensionisΣ▼,andλ▼istheordinalofits leastΣ1-elementarysubstructure.ITTMswitharbitraryiteration:Acomputationmayaskaconvergencequestionaboutanothercomputation.Thiscanbeconsideredcallingasub-compu-tation.Thatsub-computationmightdothesame.Thiscancontinue,generatingatreeofsub-computations.Eventually,perhaps,acomputationisrunwhichcallsnosub-computation.Thiseitherconvergesordiverges.Thatanswerisreturnedtoitscallingcomputation,whichthencontinues.Goodexample

Goodexample

BadexampleOnecannaturallydefinethecourseofacomputationifandonlyifthetreeofsub-computationsiswell-founded.Howisthistobedealtwith?Oneoption:Whenthemaincomputationmakesasub-call,thecallmustbemadewithanordinal.Whenasub-callmakesasub-callitself,thatmustbedonewithasmallerordinal.Definitionsofλ,ζ,andΣrelativize(toλit▼,ζit▼,andΣit▼).defs

βis0-(or1-)extendibleifit’sΣ2-extendible.

βis(α+1)-extendibleifit’saΣ2-extendiblelimitofα-extendibles. βisκ-extendibleifit’saΣ2-extendiblelimitofα-extendiblesforeachα<κ.prop

ζit▼istheleastκwhichisκ-extendible,Σit▼isitsΣ2extension,andλit▼itsleastΣ1substructure.Anotheroption:Allowallpossiblesub-computationcalls,evenifthetreeofsub-computationsisill-founded,andconsideronlythoseforwhichthetreeofsub-computationsjustsohappenstobewell-founded.Sosomelegalcomputationshaveanundefinedresult.Still,amongthosewithadefinedresult,somecomputationsarehalting,andsomedivergentcomputationshaveastableoutput.BIGFACTIfarealiseventuallywritableinthisfashion,thenit’swritable.proofGivene,runthecomputationofφe.Keepasking“ifIcontinuerunningthiscomputationuntilcell0changes,isthatcomputationconvergentordivergent?”Eventuallyyouwillget“divergent”asyouranswer.Thengoontocell1,thencell2,etc.Aftergoingthroughallthenaturalnumbers,youknowtherealonyouroutputtapeistheeventuallywritablerealyouwant.Sohalt.BIGFACTIfarealiseventuallywritableinthisfashion,thenit’swritable.SECONDBIGFACTIfarealisaccidentallywritableinthisfashion,thenit’swritable.QUESTIONWhyisn’tthisacontradiction?Whycan’tyoudiagonalize?QUESTIONWhyisn’tthisacontradiction?Whycan’tyoudiagonalize?ANSWER

Thereisnouniversalmachine.QUESTIONWhyisn’tthisacontradiction?Whycan’tyoudiagonalize?ANSWER

Thereisnouniversalmachine.Assoonasamachinewithcodeforauniversalmachinemakesanill-foundedsub-computationcall,itfreezes.defRisfreezinglywritableifRappearsanytimeduringsuchacomputation,evenifthatcomputationlaterfreezes.claimInordertounderstandthewritablerealsinthiscontext,oneneedstounderstandthefreezinglywritablereals.Onealsoneedstounderstandthetreeofsub-computationsforfreezingcomputations.notationLetΛbethesupoftheordinalssowritable(i.e.withwell-foundedoraclecalls).sub-comp.treeoffreezingcomputation:a)somenodehasmorethanΛ-manychildren,orb)everylevelhassizelessthanΛ,butthosesizesarecofinalinΛ,orc)thetotalnumberofnodesisboundedbeneathΛ.propositionOptionsa)andb)areincompatible:therecannotbeonetreeofsub-computationswith>Λ-muchsplittingbeneathanodeandanotherwiththesplittingsbeneathallthenodescofinalinΛ.Yetanotheroption:parallelcomputation: Anoraclecallmaybethequestion“doesoneofthesecomputationsconverge?”Thecomputationaskedabouthasanindexe,parameterx,andfreevariablen.Ifone(naturalnumber)valuefornyieldsaconvergentcomputation,theansweris“yes”,evenifothervaluesyieldfreezingcomputations.Yetanotheroption:parallelcomputation: Anoraclecallmaybethequestion“doesoneofthesecomputationsconverge?”Answer“yes”meanssomenaturalnumberyieldsaconvergentcomputation,evenifothernumbersyieldfreezing.Answer“no”meansallparametervaluesyieldnon-freezingcomputationsandalla