relationrewrite

RewriteSystemswithAbstractionand/3-rule:Types,ApproximantsandNormalizationSteffenvanBakel1FrancoBarbanera2MaribelFern&ndez31DepartmentofComputing,ImperialCollege,180QueensGate,LondonSW72BZ,svb@doc.
ic.
ac.
uk2DipartimentodiInformatica,UniversithdegliStudidiTorino,CorsoSvizzera185,10149Torino,Italia,barba~di.
unito.
it3DMI-LIENS(CNRSURA1327),EcoleNormaleSup~rieure,45,rued'Ulm,75005Paris,France,maribel~ens.
frAbstract.
Inthispaperwedefineandstudyintersectiontypeassign-mentsystemsforfirst-orderrewritingextendedwithapplication,A-ab-straction,and/~-reduction(TRS+/~).
Oneofthemainresultspresentedisthat,usingasuitablenotionofapproximationofterms,anytypeabletermofaTRS+/~thatsatisfiesageneralschemeforrecursivedefinitionshasanapproximantofthesametype.
Fromthisresultwededuce,fordifferentclassesoftypeableterms,ahead-normalizationandanormal-izationtheorem.
IntroductionLambdaCalculus(LC)andTermRewritingSystems(TRS)aretwocomputa-tionalparadigmsthathavebeenthoroughlyinvestigatedbecauseoftheiradapt-nesstomodelingfundamentalaspectsofcomputing.
Inthepast,thesefieldswereoftenstudiedseparately.
Thisenabledabetterunderstandingofparticularfeaturesoftheactualpracticeofcomputing,byisolatingandabstractingthosefromthewidercontextinwhichtheyareusuallyfound.
Recently,agreaterinteresthasdevelopedforthestudyofacombinationofthesetwoformalisms.
Thiscombinationisinterestingnotonlyfromthepointofviewofprogramminglanguages,butalsofromamoretheoreticalside.
Indeed,suchacombinationallowstoinvestigatetheinteractionsofthedifferentaspectsofcomputing,andenableseithertodevelopnewcomputationalmethodsandparadigms,ortobetterunderstandandimprovetheactualcomputingpractice.
Variouscombinationsofthesetwoformalismshavebeenstudiedextensivelyinrecentyears,bothintypedanduntypedcontexts.
Intheabsenceoftypes,thetwosystemsdonotinteractinaverysmoothmanner.
Forinstance,in[21]Klopshowedthatconfluence,ahighlydesirablepropertyinpractice,islostifasurjectivepairingoperationisaddedtotheuntypedLC.
In[16],Doughertyprovidedsomerestrictionsonterms,thusensuringthatpropertiesthatLCandTRSbothpossesscanbepreservedwhenthesesystemsarecombined.
Instead,inthepresenceoftypesthecombinationprovedtobemuchsafer.
Typedisciplinesprovideanenvironmentinwhichrewriterulesandj3-reductioncanbecombinedwithoutlossoftheirusefulproperties(forexample,strong388normalizationandconfluencearepreservedunderthecombinationoftypedLCandfirst-orderTRS).
Thisissupportedbyanumberofresultsforabroadrangeoftypesystemsandcalculi[12,13,14,20,23,9],butstilllacksevidenceinordertobecompletelyacceptedinitsfullgenerality.
Morespecifically,allthesystemsstudiedinthepapersmentionedabovehaveexplicittypedisciplines(alsocalleddlaChurch),i.
e.
typedisciplineswheretermscometogetherwithtypesand,hence,eachtermhasexactlyonetype.
Whentypesareconsideredtobefunctionalpropertiesofterms,thiswayofusingtypesforcestoproveapropertyofatermatthesametimethattermisconstructed.
Typedisciplines~laChurch,however,arenottheonlyonesusedwithinthesettingofprogramminglanguages.
Insomelanguagesitispossibletowritetype-freeprogramsandconstructtheirfunctionalcharacterizationsatalaterstage,i.
e.
toassigntypestothem.
Thissortoftypediscipline(alsocalledhlaCurry)isfruitfullyexploitedinseveralfunctionalprogramminglanguages,likeML[18]andMiranda4[26].
So,beforestatinginfullgeneralitythattypedisciplinesprovideagoodenvironmentforasmoothinteractionofcomputingmodeledbyLCandTRS,alsodisciplinesoftypeassignmenthavetoconsidered.
TypeassignmentdisciplineswerewidelyinvestigatedincontextsofLC,butverylittlewasdoneinthisdirectionforTRS.
Thesystempresentedin[8],forexample,combinesatypeassignmentsystemforLCwithTRSthataretyped~laChurch.
Thismeansthat[8]didnotpresentreallyatypeassignmentenvironmentforLCandTRS,butratherawaytoembedexplicitlytypedTRSinatypeassignmentdisciplineforLC.
Recently,however,newideasandresultshavecomeinaidtothesearchforatypeassignmentenvironmentforbothLCandTRS.
Forexample,in[3]anotionoftypeassignmentforTRShasbeendeveloped.
Inparticular,thatpaperconsideredsystemsinwhichitispossibletomakehypothesesaboutthefunctionalcharacterizationofthefunctionsymbolsinthesignatureoftheTRS.
Thesoundnessofthesehypothesesshouldthenbecheckedagainstthestructureoftherewriterules,and,usingthesehypotheses,typescanbederivedforterms.
Thistypeassignmentsystemenjoysinterestingnormalizationproperties[5,6].
HavingnowagoodnotionoftypeassignmentathandforTRSaswell,inthepresentpaperwearegoingtodefineatypeassignmentenvironmentforthecombinationofTRSandLC.
Toourknowledge,thisisthefirstpresentationofatypeassignmentsystemwherebothformalismsaretreatedinthesameway.
Wehopethatthedesignofsuchsystemwillprovideevidencefortheclaimstatedabove,i.
e.
thattypedisciplinesareagoodsettingforsoundinteractionofcomputationalparadigms.
Infact,wealreadyhavepositiveresultsconcerningthenormalizationpropertiesofthecombinedsystem.
Moreprecisely,inthispaperwepresentanintersectiontypeassignmentsys-temwithwandsorts(i.
e.
constanttypes)forTRSextendedwithapplication,A-abstractionandf~-reduction.
Thissystemisanextensionofthetypeassign-mentsystemsforTRSpresentedin[3].
Itexploitsthepowerandgeneralityofintersectiontypeswithw(see,e.
g.
,[11,2,4]),managingtotypebroadand4MirandaisatrademarkofResearchSoftwareLTD.
389meaningfulsetsoftermsandrewriterules.
WewillshowthatthenormalizationpropertiesofLCandTRSarepreservedinoursystem.
Itiswell-knownthatintersectiontypesystemsforLCareusefulnotonlyinthestudyofnormalizationproperties,butalsointhestudyofthesemanticsoftheLC(see,e.
g.
,[11,2]).
ThenotionofintersectiontypeassignmentforTRSdevelopedin[3,5,6]enablesthestudyoftherelationbetweensemanticsofreductionandtypeassignmentintheframeworkofTRS.
In[7]thenotionofapproximantandtherelatedapproximationmodeldefinedbyThatte[25]areusedtoshowthateverytypethatcanbeassignedtoaterm,canalsobeassignedtooneofitsapproximants(providedtheTRSsatisfiescertainconditions).
Inthissense,thetypeassignedtothetermgivesfinitaryinformationaboutthereductionprocess.
ThispaperpresentsthatresultforthecombinationofLCandTRS,butbecauseofthepresenceofabstraction,theappliedtechniquedifferssignificantly.
Ontheotherhand,theuseofintersectiontypesmodelsinaveryelegantwaythedistributionoftheactualargumentofafunctionduringthecomputation.
Thatmorethanonetypecanbeassignedtoatermcorresponds,inthissetting,tothefactthatanoperandisusedmorethanonceduringreduction,evenatalaterpointthanjustduringthecontractionoftheredexathand.
InthepresentpaperwedefineapproximantsforthecombinationofTRSandLC.
ThisnotionofapproximantisacombinationofsimilardefinitionsgivenbyThatte[25]andWadsworth[27]forTRSandLC,respectively.
WeshowthatalsointhecombinationofTRSandLCeverytypeabletermhasanapproximantofthesametype.
ThisApproximationTheoremwillbeprovedforsystemsthatuserecursioninarestrictedway:wewillconsiderrewriterulesthatsatisfyavariantofthegeneralschemesdefinedin[6,7].
Wewillthenusethisresulttoproveahead-normalizationandanormalizationtheoremfordifferentclassesoftypeableterms.
Worthnotingisthat,applyingthetechniqueusedin[8,5]itisalsopossibletoprovethatifthetypeconstantwisnotinthetypesystem,thentypeabletermsarestronglynormalizable;wewillnotdiscussthatresultforthecalculuspresentedhere,becauseofthegreatsimilaritieswiththosetwopapers.
Thispaperisorganizedasfollows:InSection1wedefineTRSwithapplica-tion,),-abstractionand/~-reduction(TRS+~),andinSection2thetypeassign-mentsystemforTRS+fl.
InSection3wedefineapproximantsandprovetheapproximationtheorem,andinSection4weprovethenormalizationtheorems.
Section5containstheconclusions.
1TermRewritingSystemswithf~-reductionruleInthissectionwepresentacombinationofuntypedLambdaCalculuswithuntypedAlgebraicRewriting,obtainedbyextendingfirst-orderTRSwithno-tionsofapplicationandabstraction,andafl-reductionrule.
WecanlookatsuchcalculialsoasextensionsoftheCurryfiedTermRewritingSystems(~rRS)con-sideredin[3,5,6],byadding)`-abstractionandafLreductionrule.
WeassumethereadertobefamiliarwithLC[10]andreferto[22,15]forrewritesystems.
390Definition1.
AnalphabetorsignatureEconsistsof:1.
AcountableinfinitesetA'ofvariablesxl,x2,x3.
.
.
.
(orx,y,z,x',y'2.
Anon-emptyset~"offunctionsymbolsF,G,.
.
.
,eachequippedwithan'arity'.
3.
Aspecialbinaryoperator,calledapplication(Ap).
Definition2.
1.
ThesetT(gr,,2()oftermsisdefinedinductively:(a)XCT(~,X).
(b)IfFe~U{Ap}isann-arysymbol(n>0),andtl,.
.
.
,tneT(~,,X),thenF(tl,.
.
.
,tn)ET(~,,X).
(c)Ift6T(~,X),andx6X,thenAx.
t6T(~,2~).
Wewillconsidertermsmoduloc~-conversion.
Acontextisatermwithahole,anditisdenotedasusualbyC[].
2.
(a)AneutraltermisatermnotoftheformAx.
t.
(b)Alambdatermisatermnotcontainingfunctionsymbols.
Thesetoffreevariablesofatermtisdefinedasusual,anddenotedbyFV(t).
Todenoteaterm-substitution,weusecapitalcharacterslike'R',insteadofGreekcharacterslike'a',whichwillbeusedtodenotetypes.
Sometimesweusethenotation{Xl~tl,.
.
.
,Xn~-~tn}.
WewritetRfortheresultofapplyingtheterm-substitutionRtot.
Inthenextdefinition,wepresentanotionofrewritingonT(~,,X)thatisdefinedthroughrewriterulestogetherwithafl-reductionrule.
Definition3Reduction.
1.
Arewriteruleisapair(l,r)ofterms.
Often,arewriterulewillgetaname,e.
g.
r,andwewritel-~rr.
Threeconditionsareimposed:lisnotavariableoranabstractionAx.
t,FV(r)C_FV(l),andApdoesnotoccurinI.
ThepatternsofarewriteruleF(tl,.
9tn)--*rrarethetermsti,1_0)wealsowriteto--**tn,andto--*+tnifto--**tninonestepormore.
Definition4.
ATermRewritingSystemwith~-reduetionrule(TRS+B)isde-finedbyapair(Z,R)ofanalphabet5:andasetRofrewriterules.
Notethatincontrastwith~stherewriterulesconsideredinthispapercancontainA-abstractions.
Wetaketheviewthatinarewriteruleacertainsymbolisdefined.
391Definition5.
InarewriteruleF(tl,.
.
.
,tn)-~rr,Fiscalledthedefinedsymbolofr,andrissaidtodefineF.
Fisadefinedsymbol,ifthereisarewriterulethatdefinesF,andQE~"iscalledaconstructorifQisnotadefinedsymbol.
(NoticethatApisneveradefinedsymbol.
)Example6.
Thefollowingisasetofrewriterulesthatdefinesthefunctionsappendandmaponlistsandestablishestheassociativityofappend.
Thefunctionsymbolsnilandconsareconstructors.
append(nil,l)append(cons(x,l),l')append(append(l,l'),l')map()~x.
t,nil)map(~x.
t,cons(y,l))--~cons(x,append(l,l'))--~append(l,(append(l',l'))-~nilcons(Ap(~x.
t,y),map()~x.
t,l))SincevariablesinTRS+/3canbesubstitutedbyA-expressions,weobtaintheusualfunctionalprogrammingparadigm,extendedwithdefinitionsofoperatorsanddatastructures.
DefinitionT.
Let(,U,R)beaTRS+/3.
1.
Atermisinnormalformifitcontainsnoredex.
2.
Atermtisinheadnormal]ormifforallt'suchthatt--**t':(a)ttisnotitselfaredex,and(b)ift'=Ap(v,u),thenvisinheadnormalform,(c)ift'=)~x.
u,thenuisinheadnormalform.
Notethattitselfcannotbearedex.
3.
Atermis(head)normalizableifitcanbereducedtoatermin(head)normalform;atermisstronglynormalizableifalltherewritesequencesstartingwithtarefinite.
4.
(,U,R)isstronglynormalizing(normalizing,head-normalizing)ifeverytermis.
5.
(,U,R)isconfluentifforalltsuchthatt4"uandt-~*v,thereexistsssuchthatu--**sandv--**s.
Example8.
TaketheTRS+/3F(G,x)--*A(H)S(C)--*GH--*HthenthetermF(B(C),)~y.
Ap(G,y))isnotaredex.
Itisnotahead-normalformeither,sinceitreducestoF(G,Ay.
Ap(G,y))whichisaredex.
ThistermreducestoA(H)thatisahead-normalform(itrewritesonlytoitself,soitwillneverbecomearedex).
Anotherterminhead-normalformis,forinstance,Ay.
Ap(y,B(C)).
OurdefinitionofheadnormalformisanextensiontorewritesystemswithApofthenotionofrootstableformdefinedin[1].
NotethattheheadofatermoftheformAp(v,u)isinv,sincewethinkofApasaninvisiblesymbol.
3922TypeassignmentinTRS+f~Typeassignmentsystemsareformalsystemsdefinedbyspecifyingasetofterms,asetoftypes,andasetoftypeassignmentrules.
InthissectionwedefineatypeassignmentsystemforTRS+/~,thatcanbeseenasanextensionoftheintersectiontypeassignmentsystempresentedin[3].
TheLC-fragmentofourtypeassignmentsystemcorrespondsdirectlytothesystempresentedin[4].
Weassumethereadertobefamiliarwithintersectiontypeassignmentsys-tems;wereferto[11,2,3]fordetails.
2.
1TypesAsin[6],wewillusestrictintersectiontypesovertype-variablesandsorts(con-stanttypes).
Weassumethatwisthesameasanintersectionoverzeroelements:ifn=0,thenain.
.
.
nan--w;soinanintersectionaln.
.
.
nqn,noicanbew.
Moreover,intersectiontypes(soalsow)occurinstricttypesonlyintheleft-handsideofanarrowtype.
Definition9Types.
1.
Ts,thesetofstricttypes,andTs,thesetofstrictintersectiontypes,aredefinedbymutualinduction:(a)alltype-variables~0,~l,.
.
.
ETs,andallsortsSo,sl,.
.
.
ETs,(b)ifTETsandaE7~,thena--,r9Ts.
(c)Ifal,.
.
.
,an9Ts(n_~0),thenaln.
.
.
nan9Ts.
2.
OnTs,therelation1)[gin.
9.
na.
0)[a1.
3.
IfB1.
.
.
.
,Bnarebases,thenll{B1,.
.
.
,Bn}isthebasisdefinedasfollows:x:aln.
.
"hameII{B1,.
.
.
,Bn}ifandonlyif{x:al,.
.
.
,x:am}isthe(non-empty)setofallstatementsaboutxthatoccurinB1U.
.
.
UBn.
3934.
WeextendO)X:Tt:alN"9"nan(a)Ifx:aistheonlystatementaboutxonwhicht:~-depends.
394(b)IfFE~'u{Ap},andthereexistsachainCsuchthatal-an--.
a=c(E(f)).
2.
WewriteBF~t:aifandonlyift:aisderivablefromthebasisBusingtheaboverules.
Noticethat,byrule(hi),B~-~t:wforalltermstandbasesB.
Wewillcallthosetermstypeablethatcanbeassignedatypedifferentfromw.
Toensurethesubjectreductionproperty,asin[3],typeassignmentonrewriteruleswillbedefinedusingthenotionofprincipalpairforatypeableterm.
Definition13.
Apair(P,~r)iscalledaprincipalpairfortwithrespectto~,ifPt-~t:TrandforeveryB,asuchthatBF~t:athereisachainCsuchthatC((P,r))=(S,a).
Wedefinenowtypeassignmentonrewriterules.
Thetype,abilityofrulesensuresconsistencewithrespecttotheenvironmentusedinthetypeassignmentforterms.
Definition14.
1.
Wesaythatl-*r~RwithdefinedsymbolFistypeablewithrespectto~,ifthereareP,and7rE:/~suchthat:(a)(P,~r)isaprincipalpairforlwithrespecttoC,andPF-rr:Tr.
(b)InPFrl:TrandPFrr:%alloccurrencesofFaretypedwithC(F).
2.
Wesaythat(~,R)istypeablewithrespectto~,ifallrERare.
Fromnowon,wewillonlyconsiderTRS+~thataretypeablewithrespecttoagivenenvironmentC.
Usingacombinationofthetechniquesusedin[3,4],itispossibletoshowthatthethreeoperations(substitution,expansion,andlifting)aresoundontypedterms.
.
Thatis,wehave:Theoreml5.
IfBFet:athen,foreveryCsuchthatC((B,a))=(B',a'),B'F~t:a'.
9Thenitispossibletoprovethattypeassignmentisclosedunderreduction.
Theorem16SubjectReduction.
IfBFxt:a,andt--*t',thenB~-~t':a.
Proof.
Thecaseofa~3-reductionfollowsfromthefactthatitispossibletoprovethat,foreveryt,u,Bt-~(Ax.
t)u:a~BF-~t{x~u}:a.
Thecaseofarewritingcanbeprovedusingthesametechniqueasin[3].
93ApproximationresultsInthissectionwedefineapproximantsofthetermsofourcalculus,andprovetheapproximationtheorem(anytypeabletermhasanapproximantwiththesametype).
OurdefinitionofapproximantsisinspiredbytheonegivenbyWadsworth[27]fortheLC,andthenotionofapproximantsforTermRewritingSystemsgivenbyThatte[25],whichinturnisbasedonthedefinitionof/2-normalformsofHuetandL6vy[19].
Asinthosepapers,inthesequelwewillonlyconsiderconfluentsystems.
Westartbyaddingaspecialsymbol_L(bottom)tothelanguage.
395DefinitionlT.
ThesetT(~,~_L)ofpartialtermsisdefinedinthesamewayasthesetT(jr,,2(),byaddingtoDefinition1thecase4.
Aspecialsymbol_L.
andtoDefinition2-1thecase1.
(d)_LET(~,,Pd,_l_).
Noticethat_Lr5rand_LrX.
TodefinetypeassignmentonT(~',X,_L),thetypeassignmentrules(Def-inition12)neednotbechanged,itsufficesthattermsareallowedtobeinT(~,rt',_l_).
Since_L~'U{Ap},_Lcanonlybetypedwithworappearinsub-termsthataretypedwithw(i.
e.
forwhichthederivationrule(hi)isusedwithn=0).
Wedefinethefollowingrelationonpartialterms.
Definition18.
1.
tEuisinductivelydefinedby:(a)ForeveryuET(~,,rt',_L),iEu.
(b)Foreveryt9T(~,X,tEt.
(c)tEu~Ax.
tEAx.
u.
(d)V1rnutC-~j[~],wheredenotessuperterm)andmuldenotesmultisetextension,andmoreover,ineveryrewriterule2.
(a)patternscannotbetypedwithw(i.
e.
novariabletypedwithwoccurstwiceinF~(C[~],y),andnosubtermofC[~]canbetypedwithw),and(b)thetypederivationsforC'~j[~](1~_j0)rVlaBaUiftt>U,andthereexistal9A(t)anda29A(u)suchthatal~_t,a2Uu,Bt-~ava,B}-ca2:a,andalc>a2.
Intuitively,t--*~auifuisareductoftforwhichthereisanapproximantwiththesameformandthesametype.
TherelationC>~isastrictsubtermorderingthatpreservesthepreviousproperty.
Definition30.
Lett>standforthewell-foundedencompassmentordering,i.
e.
uE>vifu~vmodulorenamingofvariables,anduip=vRforsomepositionp9uandsubstitutionR.
Let>~denotethestandardorderingonnaturalnumbers,andlex,muldenoterespectivelythelexicographic(fromlefttoright)andmultisetextensionofanordering.
Let(~,R)beaTRS+f~.
Wedefinetheordering>~ontriples-anaturalnumber,aterm,andamultisetoftermsthataretypeableinabasisB~withatypes{Pi}-astheobject(>IN,c>aB,p,Ut>B,p,),n~l)lex.
Property31.
LettbesuchthatB~-~t:a,andRbecomputableinB(i.
e.
foreveryx:piinB,Comp(B',xR,Pi)holds).
ThenComp(B',tR,a)holds.
Proof.
WewillinterpretatermuRbythetriple(i,u,{R}),whereiisthemax-imalsuper-indexofthefunctionsymbols(seeDefinition25)belongingtou,and{R}isthemultisetoftypeableterms{xR[x9FV(u)}.
Thesetriplesarecomparedintheordering>>.
SinceRiscomputableinB,~%iswell-foundedontheimageofRThes~Oi"unionof~>~,p~and--*~,p~isalsowell-founded.
Hence,>>isawell-foundedordering.
Theproofofthepropertygoesbynoetherianinductionon>>andcaseanalysis.
9Withthisresultweareabletoprovethemaintheoremofthissection.
Theorem32ApproximationTheorem.
If(~,R)istypeableinCandsafe,thenforeverytermtsuchthatB}-~t:a,thereisana9,4(t)suchthatBF-xa:a.
Proof.
ThetheoremfollowsfromProperties31andC1,takingRsuchthatxR~X.
94NormalizationresultsInthissectionwewillusetheApproximationTheoremtoprovetheoremsofhead-normalizationandnormalization.
Wewillalsostateastrong-normalizationtheoremforarestrictedsystem.
Theorem33.
Let(,U,R)betypeablein~andsafe.
IfBt-~t:a,anda~w,thenthasahead-normalform.
Proof.
IfB~-ct:a,thenbyTheorem32,thereisanaE.
A(t)suchthatBt-~a:a.
Sincea~w,a~and,sinceaE.
A(t),thereisavsuchthatt--**vandaE400iDA(v).
Then,byLemma24-2,visinhead-normalform,so,inparticular,thasahead-normalform.
9IntheintersectiontypeassignmentsystemforLC,termsthataretypeablewithatypeafromabasisBsuchthatwdoesnotoccurinBanda,arenor-malizable[11].
IntheframeworkofG/rRSthispropertyholdsfornon-Curryfiedterms(i.
e.
termswithoutApandCurryfiedfunctions),providedtherewriterulessatisfycertainconditions:thefunctiondefinitionshavetobesufficientlycomplete(see[6]formoredetails).
InthecaseofTRS+f~,CurryfiedversionsofthefunctionsymbolsofthesignatureareobtainedthroughtheuseofA-abstraction(wedonotneedrulestodefinethemsincewehave/~-reduction).
TheonlytermsthatwehavetoexcludearethosecontainingsubtermsoftheformAp(F(tl,.
.
.
,tn),u),whereFE~"witharitynandtl,.
.
.
,tn,uarearbi-traryterms.
ThisisbecauseatermofthisformcanhaveatypewithoutwevenifFisusedwithatypecontainingw.
Toexcludetheseterms,wewillassumethattheenvironment~issuchthatF(tl,.
.
.
,tn)cannothaveanarrowtypeifFhasarityn.
ThedefinitionofcompleteTRS+/~issimilartothedefinitionofcomplete~rRS[6,7].
Definition34.
Let~beanenvironmentsuchthatforanyFE~"ofarityn,F(tl,.
.
.
,t,~)cannothaveanarrowtype.
ATRS+f~iscompleteintheenviron-mentCifwheneveratypeabletermt,ofwhichthetypedoesnotcontainw,isreducibleatapositionpsuchthattipcanbeassignedatypecontainingw,thereexistsqrewritesystems,whichmodelalgebraicoperationsondatastructures,withthepowerofLC.
ThetypeassignmentsystemthatwedefinedisatrueextensionoftheintersectionsystemforLC,sothepureLC-fragmentofthelanguagehasthewell-knownnormalizationproperties:1.
thesetoftermstypeablewithoutwisthesetofstronglynormalizableterms,2.
thesetoftermstypeablewithtypeafromabasisB,suchthatwdoesnotoccurinBanda,isthesetofnormalizableterms,and3.
thesetoftermstypeablewithtypea~=wisthesetoftermshavingaheadnormalform.
Ifwedonotallowabstractionsinright-handsidesofrewriterules,andcon-siderthealgebraicfragmentofourlanguage,weobtaina~rrRS,forwhichthefollowingpropertieshold[7]:1.
termstypeablewithoutoJarestronglynormalizable,2.
non-CurryfiedtermstypeablewithtypeafromabasisB,suchthatwdoesnotoccurinBandaarenormalizable,and3.
termstypeablewithtypea~=whaveaheadnormalform.
Noticethattheconversesofthepreviouspropertiesdonothold,becausetheenvironmentisgiven(andfixed).
In[7],thesepropertieswereproveddirectlyfromthestrongnormalizationpropertyof"derivationreduction,"arewriterelationonderivationsthatisstronglynormalizingevenintypesystemswithw.
TheApproximationTheo-remisalsoaconsequenceofthisproperty.
Sinceitisatthismomentnotclearifthattechniqueextendstosystemswithabstraction,inthispaperwehavegivenadirectproofoftheApproximationTheoremfromwhichwecaneasilydeducethehead-normalizationandnormalizationproperties(attheexpenseofamorecomplicatedstrongnormalizationproof).
Wehaveshownthatthenormalizationpropertiesthatareenjoyedbybothlanguageswhenconsideredseparately,areinheritedbythecombinedlanguage.
ThissupportsourinitialclaimthattypeassignmentsystemsprovideasoundenvironmentforthecombinationoftheprogrammingparadigmsbasedonTRS402andLC.
Butinordertoprovidemoreevidenceforthisclaim,otherimportantproperties(suchasconfluence,preservationofnormalizingstrategies)havetobestudied.
Thiswillbeasubjectoffuturework.
AcknowledgementsThesecondauthorwishestothankprof.
MariangiolaDezaniforhergentleguid-ance,andSalvatoreFavataformakingthedepartmentofComputerScienceofTorinoamorepleasantenvironmenttoworkin.
References1.
AriolaZ.
,R.
Kennaway,J.
W.
Klop,R.
SleepandF-J.
deVries.
Syntacticdefini-tionsofundefined:ondefiningtheundefined.
InProceedingsofTACS'9~,volume789ofLNCS,pages543-554,1994.
2.
S.
vanBakel.
CompleterestrictionsoftheIntersectionTypeDiscipline.
TheoreticalComputerScience,102:135-163,1992.
3.
S.
vanBakel.
PartialIntersectionTypeAssignmentinApplicativeTermRewritingSystems.
InProceedingsofTLCA'93,volume664ofLNCS,pages29-44,1993.
4.
S.
vanBakel.
IntersectionTypeAssignmentSystems.
TheoreticalComputerSci-ence,151(2):385-435,1995.
5.
S.
vanBakelandM.
Ferngmdez.
StrongNormalizationofTypeableRewriteSys-tems.
InProceedingsofHOA'93,volume816ofLNCS,pages20-39,1994.
6.
S.
vanBakelandM.
Fernhndez.
(Head-)NormalizationofTypeableRewriteSys-tems.
InProceedingsofRTA'95,volume914ofLNCS,pages279-293,1995.
7.
S.
vanBakelandM.
Fernhndez.
ApproximationandNormalizationResultsforTypeableRewriteSystems.
ToappearinProceedingsofHOA'95,Paderborn,Germany,1995.
8.
F.
BarbaneraandM.
Fern~mdez.
Combiningfirstandhigherorderrewritesystemswithtypeassigmnentsystems.
InProceedingsofTLCA'93,volume664ofLNCS,pages60-74,1993.
9.
F.
Barbanera,M.
Fernandez,andH.
Geuvers.
ModularityofStrongNormalizationandConfluenceintheA-algebraic-cube.
InProceedingsofLICS'94,1994.
10.
H.
Barendregt.
TheLambdaCalculus:itsSyntaxandSemantics.
North-Holland,Amsterdam,revisededition,1984.
11.
H.
Barendregt,M.
Coppo,andM.
Dezani-Ciancaglini.
Afilterlambdamodelandthecompletenessoftypeassignment.
JournalofSymbolicLogic,48(4):931-940,1983.
12.
V.
Breazu-Tannen.
Combiningalgebraandhigher-ordertypes.
InProceedingsofLICS'88,pages82-90,1988.
13.
V.
Breazu-TannenandJ.
Gallier.
Polymorphicrewritingconservesalgebraicstrongnormalization.
TheoreticalComputerScience,83(1):3-28,1991.
14.
V.
Breazu-TannenandJ.
Gallier.
Polymorphicrewritingconservesalgebraiccon-fluence.
InformationandComputation,82:3-28,1992.
15.
N.
DershowitzandJ.
P.
Jouannaud.
Rewritesystems.
InJ.
vanLeeuwen,editor,HandbookofTheoreticalComputerScience,volumeB,chapter6,pages245-320.
North-Holland,1990.
40316.
D.
J.
Dougherty.
AddingAlgebraicRewritingtotheUntypedLambdaCalculus.
InProceedingsofRTA'91,volume488ofLNCS,pages37-48.
1991.
17.
J.
-Y.
Girard,Y.
Lafont,andP.
Taylor.
ProofsandTypes.
CambridgeTractsinTheoreticalComputerScience.
CambridgeUniversityPress,1989.
18.
M.
Gordon,R.
Milner,andC.
Wadsworth.
EdinburghLCF.
LectureNotesinComputerScience,volume78,1979.
19.
G.
HuetandJ.
J.
L6vy.
ComputationsinOrthogonalRewritingSystems.
InJ.
-L.
LassezandG.
Plotkin,editors,ComputationalLogic.
EssaysinHonourofAlanRobinson.
MITPress,1991.
20.
J.
P.
JouannaudandM.
Okada.
Executablehigher-orderalgebraicspecificationlanguages.
InProceedingsofLICS'91,pages350-361,1991.
21.
J.
W.
Klop.
TermRewritingSystems:atutorial.
EATCSBulletin,32:143-182,1987.
22.
J.
W.
Klop.
TermRewritingSystems.
InS.
Abramsky,Dov.
M.
Gabbay,andT.
S.
E.
Maibaum,editors,HandbookofLogicinComputerScience,volume2,chapter1,pages1-116.
ClarendonPress,1992.
23.
MitsuhiroOkada.
Strongnormalizabilityforthecombinedsystemofthetypeslambdacalculusandanarbitraryconvergenttermrewritesystem.
InProceedingsofISSAC89,Portland,Oregon,1989.
24.
W.
W.
Tait.
IntensionalinterpretationoffunctionalsoffinitetypeI.
JournalofSymbolicLogic,32(2):198-223,1967.
25.
S.
R.
Thatte.
FullAbstractionandLimitingCompletenessinEquationalLan-guages.
TheoreticalComputerScience,65:85-119,1989.
26.
D.
A.
Turner.
Miranda:Anon-strictfunctionallanguagewithpolymorphictypes.
InProceedingsoftheconferenceonFunctionalProgrammingLanguagesandCom-puterArchitecture,volume201ofLNCS,pages1-16,1985.
27.
C.
P.
Wadsworth.
TherelationbetweencomputationalanddenotationalpropertiesforScott'sD~c-modelsofthelambda-calculus.
SIAMJ.
Comput.
,5:488-521,1976.