; TeX output 2007.07.16:1008 o#fܚ? color push Blackhtml:color push rgb 0 0 1 color pop html:[ color pop5#f? ܚhtml: html:html: html:
color push Black color popN ff cmbx12OnfftheStabilitybyUnionofReducibility Candidates"% K`y
cmr10ColinUURibaijo cmr9INPLT&LORIA-="; cmmi6?UT,Nancy:,France فߤN cmtt9riba@loria.fr(yscolor push Black /t: cmbx9Abstract. color popM&W:eɉin9vestigatesomeaspAectsofɊproofmethodsforthetermi-snationmofm(extensionsof q)thesecond-order!5" cmmi9-calculusinpresenceofunionsandTexisten9tialtypAes.
vsW:e+pro9ve*thatGirard'sreducibilit9ycandidatesarestableb9yunionitheysare_exactlythe`non-empt9ysetsofterminatingtermswhic9haredownward-sclosedTw.r.t.aw9eakobserv|rationalpreorder.sW:eksho9wkthatthisisthecasefortheCurry-st9ylesecond-order-calculus.sAs;cacorollary:,;bw9eobtainthatreducibilitycandidates;bareexactlythesT:ait'ssaturatedsetsthatarestableb9yreduction.WethenextendthesproAof+ctoasystemwithproduct,co-productandpositiv9eiso-recursivest9ypAes.html: html:@ 1N cmbx121@ In tro` ductionSincetheirintroGductionin[html:color push rgb 0 0 117 html: color pop
],unionandexistentialtypGeswithtypGeassignment rulesarepresentinmanytypGesystems.F*romafoundationalpGerspective,theyareSinterestingTasdualofrespGectivelyintersectionandsecond-orderTtypGes.ThepapGer%[4html:color push rgb 0 0 13 html: color pop ]provides$detailedinvestigationsonsyntacticaswell$assemanticsissuesofIuniontypGes.IAsatheoreticaltool,ItheyhaveIbeenusedIin[3html:color push rgb 0 0 18 html: color pop ,2html:color push rgb 0 0 19 html: color pop I]'toprovethatakindofBohmtrees,calledLGevy-Longotrees,distinguishespure
b>
cmmi10-termsexactlyUUasdoGestheirobservqationinthelazyconcurrent-calculus. InterestingvapplicationsofunionvtypGesaretheXMLvprocessinglanguagesXDucezT[2html:color push rgb 0 0 114 html: color pop
]and
msbm10CDucezU["html:color push rgb 0 0 111 html: color pop].TheydescribGetypesofXMLzKdocumentsbymeansofUUregularexpressionswhoseinternalrepresentationreliesonuniontypGes. Existentialsn)andn*unionsarealsointerestingtoGolsforrepresentingabstractionsofprograms.Inthecontextofstrictnessanalysis,unionsareusedin["html:color push rgb 0 0 115 html: color pop
]torepresentUUdisjunctivepropGertiesofprograms. F*rGederictBlanquiuandtheauthorpropGosedin[ html:color push rgb 0 0 16 html: color pop ]aterminationcriterionforhigher-order
conditional
rewritingthatuseconstrainedtypGes.Existential
con-straintsarisenaturally*,forexamplewhenprovingthatsomeimplementationsofQuickSort)$preservesthesizeofitsargument.ThisworkreliesonproGofmethodsfortheterminationoftypGed-calculusplusrewritinginpresenceofexistentialtypGes.
color push Blackff ff 8ϟ
L͍Y-=?
UMR075030CNRS-INPL-INRIA-Nancy2-UHP:,0CampusScien9tique,BP0239,54506
V:andoAeuvre-lXes-NancyTCedex,FranceL color pop ? color push Black[ color pop *o#fܚ? color push Blackhtml:color push rgb 0 0 1 color pop html:2!- ColinTRiba[ color pop5#fܚN UsualQproGofsofstrongnormalization(2 ':
cmti10i.e.termination)fortyped-calculi ? assignwtoeachtypGeTڮasetwofstronglynormalizingterms,
stmary10JTcK(theinterpr}'etation? of9Tc,withanassignmentofits8freevqariables).Then,theyusesoundnessofthis? interpretationw.r.t.thetypGesystem:typabletermsbGelongtotheinterpretation? oftheirtypGes.ButsoundnessrequiresthattypGesarenotinterpretedbyarbitrary? sets^ofterms._Theymustsatisfysomeclosur}'econditions.Thetwomost^pGopular? onesareGirard'sreducibilitycandidatesandT*ait'ssaturatedsets.See["html:color push rgb 0 0 112 html: color pop
]fora? detaileddiscussionandhistoricalreferences.AcomparisonofGirard'sandT*ait's? closureUUconditionscanalsobGefoundin[!html:color push rgb 0 0 123 html: color pop
].
XN In