DOI 10.1017S0956796803004702 Printed in the United Kingdom C

We characterize the impact of a linear β-reduction on the result of a control-flow analysis. (By ‘a linear β-reduction ’ we mean the β-reduction of a linear λ-abstraction, i.e., of a λabstraction whose parameter occurs exactly once in its body.) As

c2003CambridgeUniversityPressJFP13(5):925–933,September2003.

DOI:10.1017/S0956796803004702PrintedintheUnitedKingdom925

CPStransformationof owinformation,

PartII:administrativereductions

DANIELDAMIAN

LIONBioscienceLtd.,CompassHouse,80–82NewmarketRoad,CambridgeCB58DZ,UK

(e-mail:Daniel.Damian@http://www.77cn.com.cn)

OLIVIERDANVY

BRICS,DepartmentofComputerScience,UniversityofAarhus,NyMunkegade,Building540,

DK-8000AarhusC,Denmark

(e-mail:danvy@brics.dk)

Abstract

Wecharacterizetheimpactofalinearβ-reductionontheresultofacontrol- owanalysis.(By‘alinearβ-reduction’wemeantheβ-reductionofalinearλ-abstraction,i.e.,ofaλ-abstractionwhoseparameteroccursexactlyonceinitsbody.)Asacorollary,weconsidertheadministrativereductionsofaPlotkin-styletransformationintoContinuation-PassingStyle(CPS),andhowtheya ecttheresultofaconstraint-basedcontrol- owanalysisand,inparticular,theleastelementinthespaceofsolutions.Weshowthatadministrativereductionspreservetheleastsolution.PreservationofleastsolutionssolvesaproblemthatwasleftopeninPalsbergandWand’sarticle‘CPSTransformationofFlowInformation.’Together,PalsbergandWand’sarticleandthepresentarticleshowhowtomapinlineartimetheleastsolutionofthe owconstraintsofaprogramintotheleastsolutionofthe owconstraintsoftheCPScounterpartofthisprogram,afteradministrativereductions.Furthermore,weshowhowtoCPStransformcontrol- owinformationinonepass.

1Backgroundandintroduction

Sincetheirinception,over30yearsago(Reynolds,1993),continuationsandthetransformationintoContinuation-PassingStyle(CPS)havebeenthetopicofmuchstudy,rangingfromsemanticsandlogictoimplementationsofsequential,concurrent,anddistributedprogramminglanguagesandsystems.Fifteenyearsago,MeyerandWand(Meyer&Wand,1985;Wand,1985)noticedthattheCPStransformationpreservestypesandtheyconstructedaCPStransformationoftypes.

CPStransformationtype_______________typeoftypestypeinference

direct-styleprogramtypeinferenceCPStransformationCPSprogramofterms

Thisworkwascarriedoutwhilethe rstauthorwasatBRICS.BasicResearchinComputerScience(www.brics.dk),fundedbytheDanishNationalResearchFoundation.

We characterize the impact of a linear β-reduction on the result of a control-flow analysis. (By ‘a linear β-reduction ’ we mean the β-reduction of a linear λ-abstraction, i.e., of a λabstraction whose parameter occurs exactly once in its body.) As

926D.DamianandO.Danvy

Overthelastcoupleofyears,PalsbergandWandhaveextendedthisobservationto owtypesandthe owinformationgatheredbyacontrol- owanalysis(Palsberg&Wand,2002),designingaCPStransformationof owinformation.

ow ow__CPS__transformation________informationinformationof ow owanalysis

direct-styleprogram owanalysisCPStransformationCPSprogramofterms

Independently,andwithadi erentmotivation,wehavealsodesignedaCPStrans-formationof owinformationforcontrol owandbindingtimes(Damian,2001;Damian&Danvy,2000;Damian&Danvy,2002).ThetwoCPStransformationsof owinformationcorrespondtotwodi erenttakesontheCPStransformationofλ-terms:

CPSwithadministrativeredexesadministrativeCPSUUUUreductionslllUUUUtransformationlllUUllllCPSwithoutdirectstyleadministrativeredexesRRRRRRiiiiRRRiiiitransformationintoRRiiiiintroductionofmonadicstylecontinuationsmonadicnormalform

TheCPStransformationisPlotkin’s(1975).Itisa rst-order,compositionalrewritingsystemgeneratingnumerousadministrativeredexesthatneedtobepost-reducedinpractice(Steele,1978).Alternatively(Hatcli &Danvy,1994;Sabry&Wadler,1997),theCPStransformationcanbestagedintoatransformationintomonadicnormalformfollowedbyanintroductionofcontinuations.

ThetwoCPStransformationsof owinformationcanbedepictedasfollows:

CPSwithadministrativeredexesPalsberg&Wand,UUUUthisworklllUUUUl2002llUUllllCPSwithoutdirectstyleadministrativeredexesRRRRRRiRRRiiiiiiRiDamian&Danvy,RiiiiDamian&Danvy,2002monadic2000normalform

PalsbergandWandshowhowtoconstructinlineartimethe owinform-ationcorrespondingtoaCPSprogramobtainedthroughaPlotkin-styleCPStransformation(Palsberg&Wand,2002;Plotkin,1975).TheresultingprogramscontainalladministrativeredexesinducedbyPlotkin’stransformation.Therefore,

We characterize the impact of a linear β-reduction on the result of a control-flow analysis. (By ‘a linear β-reduction ’ we mean the β-reduction of a linear λ-abstraction, i.e., of a λabstraction whose parameter occurs exactly once in its body.) As

CPStransformationof owinformation,PartII:administrativereductions927

e

π

n∈∈∈∈ExpLamLabLit::= 2 0 1π 1x|n|e 1e2|if0ee0e1|λx.e(λ-abstractionlabels)(termlabels)(integerliterals)

Fig.1.Thelanguageoflabelledλ-terms.

thecorrespondingCPSinformationof owalsocontainsspuriousinformationwhichaccountsfortheextraneousλ-abstractionsandtheir ow.Theproblemofeliminatingthisspuriousinformationisopen.

DamianandDanvyshowhowtoconstructinlineartimethe owinformationcorrespondingtotheintroductionofcontinuations,startingfrommonadicnormalforms(Damian&Danvy,2000;Hatcli &Danvy,1994).Theyalsoshowhowtoconstructinlineartimethe owinformationcorrespondingtothetransformationintomonadicnormalforms(Damian,2001;Damian&Danvy,2002).

Inthiswork,wecompletethepictureabovebyshowinghowtoperforminlineartimeadministrativereductionsonCPS-transformedprograms(Section4).Ourresulthingesonlinearreductions(Section3).But rst,wepresentthesourcelanguageandaconstraint-basedcontrol- owanalysis(Section2).

2Preliminaries

2.1Thesourcelanguage

InputtermsaregivenbythegrammarinFigure1.

distinctlabelstakenfromacountablesetLab.E …… 此处隐藏：16944字，全部文档内容请下载后查看。喜欢就下载吧 ……