; TeX output 2000.09.25:1752m܍3$(܍'sDtGGcmr17The7tgreatestcommondivisor:acasestudyforprogramn0extraction7tfromclassicalprosofslύ{'XQ cmr12U.BergertH.ScrhwichtenbSergύW SeptemrbSer25,2000*i1K`y 3 cmr10Yiannis-?Mosc!hovdDakissuggestedthefollowingexampleofaclassicalexistenceproMofwitha 1quan!ti er{freezkernelwhichdoMesnotobviouslycontainanalgorithm: thegcdoftwonatural1n!umbMersw. b> 3 cmmi10az|{Ycmr81 8andaz2isalinearcom!binationofthetwo. RHerewetreatthatexampleas1aqcasestudyforprogramextractionfromclassicalproMofs. @jWeeapplyH.Friedman'sA{1translation[3y]follo!wedbyamoMdi edrealizabilityinterpretationtoextractaprogramfrom1thissproMof.Ho!wever,}toobtainareasonableprogramitisessentialtouseare nementofthe1A{translationrin!troMducedinBerger/SchwichtenbMerg[2y,1q].̭Thisre nementmakesitpMossible1thatvnotallatomsintheproMofareA{translated,butonlythosewitha\critical"relation1sym!bMol.Infourexampleonlythedivisibilityrelation/!", 3 cmsy10jwillbMecritical.1LetIa;1b;c;i;j;kX?;`;m;n;qd;r&'denotenaturaln!umbMers.sOurlanguageisdeterminedbythe1constan!ts0;11;+;,,Ffunctionsym!bMolsforthequotientandtheremainderdenotedbyqd(a;1c)1andkrM޹(a;1c),a4{aryfunctiondenotedb!yabsm(kz1az1:kz2az2)kwhoseintendedmeaningisclearfrom1thenotationandanauxiliary5{aryfunctionfㆹwhic!hwillbMede nedlater.Weewillexpressthe1in!tendedmeaningofthesefunctionsymbMolsbystatingsomepropMerties(lemmata)vz1;1:::l;1vz61offthem;thesewillbMeform!ulatedasweneedthem.10"V 3 cmbx10Theorem.18az1;1az2(0 since0 Ferom,wz4ƹandwz3:1(Dqi~㼍k )Firstwecompute`z1;1`z2 1%suchthatrz1 =\(`z1;1`z2).>Thisq!isdoneby1somefauxiliaryfunctionf-,de nedb!ybN\|f-(az1;1az2;kz1;kz2;qd) :=u cmex1033 ]qkz1.n1;<ƹiffkz2az2ʫ:=fAz1 TB!:1::!Azm !?;1Cz1;:::l;CznPg.WDetermineinductiv!elytheL{criticpalx5relation&ysym!bMolsasfollows:If(;j~ĖDz1!Pz1)!:1::!(;j~ĖDzm!PzmĹ)!R(OY~CtE)&yisapMositivex5subform!ulaϭofaformulainL,andforsomei,Pzio ?orPzi Q(W~s!)whereQisL{critical,x5thenfRisL{criticaltoMo.ݩ40 m܍3$(܍3$ zV2.x5Feoreac!hformulaFletitsA{trpanslationFVA ɹbMetheformulaobtainedfromFbyreplacing x5?b!yAandeachsubformulaR(W~s!),,whereR'isL{critical,b!y(R(W~s!)!A)!A. Findx5derivdDationsXrdzuk޹:18Dqi~㼍k (Az1ʫ! :::۱! Azm k!?)zA; fand)]dzv8:;cmmi6i[vzidڹ:18ڇ~xzi Czi]:8ڇ~xzi CzȁA:jix5follo!wingftherecipMegivenin[1y]. zV3.x5ReplaceFbind[u;1vz1;:::l;vznP]:?Fbeac!hformulabyitsA{translation.WeeobtainaderivdDation*dA[uA;1v1A ;:::l;vnA 4]:A;x5wherecouA:18Dqi~㼍k (AAg1 #!E:::Q!EAAAm Jy!A)andviA ¾:18ڇ~xzi CȁA|i Թ(inductionaxiomsarereplaced x5b!yFeurthermorereplaceinthex5derivdDationoabMo!vethefreeassumptionsbythederivdDationsconstructedinstep2.˙Weegetx5theftranslatedderivdDationdztr?[vz1;1:::l;1vznP] :=dA[dzuk;dzvqAacmr619;:::l;dzvn ɹ]:A: zV4.x5ApplyfKreisel'smoMdi edrealizabilit!yinterpretation[4y]toextracta nitelistofterms]~˶tr:= (dztr?)zetsx5suc!hfthatAz1[~r>=Dqi~㼍k ]n^:1::;^AzmĹ[~r=Dqi~㼍k ]fispro!vdDablefromvz1;1:::l;1vz6.1Comments. {x5Teermextractioncomm!uteswiththelogicalrules,1e.g.(dz1dz2)etsԹ=%detsg1 detsg2,andsubsti- x5tution,fi.e.](dztr?)zets V (dA[dzuk;1dzvq19;:::l;dzvn ɹ])zets dzets:jA ﯹ[dzets:ju;1dzets:jvq1;:::l;dzets:jvn]:x5Byːthelatterw!emay rstextracttermsfromthederivdDationsdA;1dzvq19;:::l;dzvn Yandːalsox5fromtheproMofof<{inductionseparatelye,olandthensubstitutethesetermsin!tothex5termsfextractedfromdA[uA;1v1A ;:::l;vnA 4]:A. {x5AssumeRthatw!ehave xedsomesystemoflemmata8ڇ~xz1 Cz1;1:::l;18ڇ~xzn kCzn andcomputedx5the.L-criticalrelationsym!bMolsaccordingtostep1.Thenit'sclearthatwemayuseanyx5otherstrue! 8{form!ulaDQasafurtherlemma,providedDQdoMesneithercontain?norx5an!yL{criticalrelationsymbMol.Thesimplereasonis,thatinthiscaseDA 6i D.Inthex5sequelfw!ewillcallsuchformulasDDharmless.ݩ5Bm܍3$(܍3$1Computing2theL{criticalrelationsymtbYols.1No!wwecomebacktoourexample.LetusrepMeatthemainlemmatausedintheproofs 1offtheprincipleof<{inductionandthetheorem.-vz0:10 N"(㎍D~rk) '͍<ind8VdzProg:jprog601(ez0<(0;1)!}[vz0]);f1where#dȮ<indM2_Wwcw:u}~y荐Knnat !(f~y荼nat G(!f~y荼nat)!f~y荼natg1RDqi~㼍kX?z0:;jC~ĖRf(Dqi~㼍k :m(i~W0y)(n;9~1wz}~y荐Knnat !f~y荼nat:j2+;DD~㼍1k:f\~wz1D I~㼍 k~zwz29Z)((Dqi~㼍kX?z0)n+1)Dqi~㼍kX?z0;E 4N(dztr:jprog',)zetsF=Ȯ cDqi~㼍k ;~1uzf~y荼nat G(!f~y荼nat:j1)?:(dztr:jdiv q2Z)zets ﯹ((dztr:jdiv q1)zetsD a~㼍kI);ٍ(dztr:jdiv 8:i\})zetsF=Ȯ c~uzf~y荼nat:j12 :ifK0 <F~rzi `1(Dqi~㼍k ) 5then.k?~.juz1D9:~㼍9$`ziA(Dqi~㼍k) 5else)I~)tuz12D g 1andfhence3#ڍl>(dtrAprog',)ets V=Ȯ Dqi~㼍k ;~1uf~y荼nat G(!f~y荼natg1)?:Wif^0 0f(usingthefactthatthisdoesn'tc!hangetheideal).(: {x5There isanin!terestingphenomenonwhichmayoMccurifweextractaprogramfromax5classical!proMofwhic!husestheleastelementprinciple.Considerasasimpleexamplethex5w!ellfoundednessfof<,E}#\8gdznat z!nat!9kX?(gd(k++n1) 0suchthatcdividesx5az1 Q-and)az2,whereasintheexampleabMo!ve)therema!ybedi eren!tc=gd(kX?))suchthatx5gd(k++n1) 3 cmmi10K cmsy8;cmmi62cmmi8Aacmr6|{Ycmr8XQ cmr12DtGGcmr17K`y 3 cmr10u cmex10