; TeX output 2003.08.11:2220 C Ghtml: html: Gz html: html:4 z
=Dt G G cmr17The7tFixedPqoint7tPropserty q8vin7tSynqtheticDomainTheory /cXQ cmr12PraulTVaylor ȋ1991"Ӎ U*t: cmbx9Abstracto&)o cmr9W:epresen9tanelementaryaxiomatisationofsyntheticdomaintheoryandshowthatit is;sucien9ttodeducethexedpAointpropAertyandsolvedomainequations.MoAdelsofthese axioms basedonpartialequiv|ralencerelationsha9ve receivedmuchattention,Lbuttherearealso v9erysimplesheafmoAdelsbasedonclassicaldomaintheory:.InanycasetheaimofthispapAer istosho9wthatanimpAortanttheoremcanbAederivedfroman+j cmti9abstract$*axiomatisation,rather thanLfromaparticularmoAdel.NAlso,Zpb9yprovidingacommonframeworkinwhichbAothPER andTclassicalmoAdelscanbeexpressed,thisw9orkbuildsabridgebet9weenTthet9wo.$html: html:@ -N ff cmbx121LAxiomsK`y
cmr10SyntheticfDomainTheoryisthestudyofthedictumthat. ':
cmti10domainsar}'esetsandfal lset-theoretic functionsb}'etweendomainsare\continuous"or\computable."xPlainlywecannotmean\sets"inthe[Cclassicalsense,\sowehavehavetoworkinan(elementary)topGos
!",
cmsy10E@;andbyasetwemeananob 8jectfofE .Sinceweintendtointerpretrecursion,k\weassumethatEKalsohasanatur}'alnumbersobje}'ct,UU
msbm10N. InHatopGos,Tdenablesubob 8jectsandpredicatesareclassie}'dQbyanobject
,TwhichmeansthatsanysubGob 8jectisuniquelyexpressibleasapullbackoff>g:1!
. a"Howeversnotallpredicateswharecomputable,i.e.veriablebyaprogramwhoseoutputtypGeincludes
msam10pi/"V
cmbx10t
b>
cmmi10y[esD q!andnon-termination:8thenon-terminationpredicateontheclassofprogramsisaveryimpGortantcounterexample.Nevertheless,the^followingclearlyaresatisedbytheclassofsemi-de}'cidablepr}'edicates !:3xhtml: html:
ɍ81. Thepullback(inverseimage)f^O! cmsy7sofasemi-decidablepredicatealongamapfڧ:X!YEis semi-decidable,byStheprogramwhichrstltersitsinputthroughf.d(W*ecannotsaythe samebofr}'ecursivelyenumerablesubsets4²withoutbmakingenumerabilitybassumptionsabGout theUUtypGesthemselves.)qThereforetheclassisclassiedbyanob 8ject,analogousto
.@html: html:
@82. PredicatesEwiththesameextensionweregardasthesame,HsoisinfactasubGob 8jectof
.Whtml: html:83. BypGerformingside-ee}'ct-freeotestsinsuccession,theclassisclosedunderniteconjunction orUUintersection,soisasub-^-semilattice.Whtml: html:84. BypGerformingtestsinp}'aral lel,ltheclassisclosedunderdisjunctionorunion,soisa sublatticeUUof
(including>and?).@html: html:
@85. Recursively-indexed testsmayalsobGeperformedinparallel,&soޘ
isclosedunderN- indexedUUjoins.A Now^)consideramap:!.dPostcompGosition^)withthistransformssemidecidablepredicatesX!2)intoothersbymeansof\additionalcomputation"whichmaymakewhateveruseitseestoftheresultoftherstpredicate,butnotofthedata.PWAllthatsuchatransformationcandois outputUUsomevqalue(?)\anyway", Q1 * C Ghtml: html: !H+Iandthenifitgetssomeinput(i.e.therstpredicatehasbGeensatised),.outputsome +I\bGetter"UUvqalue(>).5GOfcourse(?)-)(>),fbutwhatwearesayingisthatisuniquely!Cdetermine}'dbythesetwoGvqaluesUU(whichmaybGearbitraryelementsofsolongasthisimplicationholds).qSo,+IPhoaQPrinciple:^ٓR cmr75W,the ob 8jectofendofunctionsofthesemi-decidablepredicate+Iclassier,UUisisomorphictofUVh͠;!Ǹi:;߸2;q")!Ǹgr,R.GItUUturnsoutthatthiscuriousaxiomisverypGowerful.!GFinallyuthereisahigher-orderprinciple.'Anyfunctionalo:^qy msbm7N!uwhichpurpGortstotestGforUUuniversaltruthreallyonlytestsuptosome\large"numbGer.?+IScottTPrinciple:qDzF*orUU:^r! msbm5N
Q²,if(n:>)then9m:(n:n4 html:.Ghtml: html:D1DenitionA1.1A mo}'del9qofsyntheticdomaintheoryis Dapair(E ;),6@whereE