Two behavioural lambda models

PartiallysupportedbyEUwithintheFET–GlobalComputinginitiative,projectDARTST-2001-33477,andbyMURSTCofin’01projectCOMETA.Thefundingbodiesarenotresponsibleforanyusethatmightbemadeoftheresultspresentedhere.2

Partiallysupportedbygrant1630“Representationofproofswithapplications,classi-ficationofstructuresandinfinitecombinatorics”(oftheMinistryofScience,Technology,andDevelopmentofSerbia).

1

34

byusingthefinitarylogicaldescriptionofthemodelsobtainedbydefiningsuitableintersectiontypeassignmentsystems.

Inthispaperwefocusonsixcomputationalpropertiesoflambdatermsandcorrespondingsixsetsoflambdaterms:thesetofnormalizing,headnormalizing,weakheadnormalizinglambdaterms,andthosecorrespondingtothepersistentversionsofsuchnotions.WebuildaninverselambdamodelD∞,accordingtoScott[23],whichcompletelycharacterizeseachofthesixsetsoftermsmentioned.Moreprecisely,foreachoneoftheabovesixsetsoftermsthereisacorrespondingelementinthemodelsuchthatatermbelongstothesetifandonlyifitsinterpretation(inasuitableenvironment)isbiggerthanorequaltothatelement.ThisisprovedbyusingthefinitarylogicaldescriptionofthemodelD∞obtainedbydefininganintersectiontypeassign-mentsysteminthefollowingway.First,weconstructasetToftypeswhicharegeneratedfromatomictypescorrespondingtotheelementsofD0,bythefunctiontypeconstructorandtheintersectiontypeconstructor.Thenwede-fineasetFoffiltersonthesetT.AccordingtoCoppoetal.[7]andAlessi[2],thesetFoffiltersandtheinversemodelD∞areisomorphicasω-algebraiclattices.ThisisomorphismfallsinthegeneralframeworkofStonedualities(Johnstone[14]).ThisframeworklaterreceivedacategoricallyprincipledexplanationbyAbramskyinthebroaderperspectiveof“domaintheoryinlogicalform”[1].InKegelman[15]onecanfindagreattourthroughvariousStonedualitiesinthecategoryofcontinuousdomains.TheinterestoftheaboveisomorphismliesinthefactthattheinterpretationsoflambdatermsinD∞areisomorphicwiththefiltersoftypesonecanderiveinthistypeas-signmentsystem(Alessi[2]).Thisgivesadesiredfinitarylogicaldescriptionofthemodel.Therefore,anequivalentoftheprimarycompletecharacteri-zationcanbestated:atermbelongstooneofthesixsetsmentionedifandonlyifithasacertaintype(inasuitablecontext)inthetypeassignmentsystemobtained.

SomeideasofthisresearchwerepresentedattheInternationalWorkshoponRewritinginProofandComputation(RPC’01,TohokuUniversity25-27/10/2001,Sendai,Japan)[8].Alongthelinesoftheseideasitisworthinvestigatingthebehaviourofsomeothercomputationalpropertiessuchasvariousclosabilities,i.e.reductionstodifferentkindsofclosedterms,whichisconsideredinDezaniandGhilezan[9].

InSectionthemodelD∞characterizingallsixcomputationalpropertiesoftermsisbuilt.ThetypeassignmentsystemisdefinedinSectionandtheproofsareshortlydiscussed.

35

2.Themodel

Weusestandardnotationsforlambdatermsandbetareductions.Definition1.(ThesetΛoflambdaterms)

ThesetΛof(type-free)lambdatermsisdefinedbythefollowingabstractsyntax.

Λvar

::=::=

var|(ΛΛ)|(λvar.Λ)x|var′

Weusex,y,z,...,x1,...forarbitrarytermvariablesandM,N,P,...,M1,...forarbitraryterms.Inwritingtermsweassumethestandardcon-ventionsonparenthesesanddots[5].FV(M)denotesthesetoffreevariablesofatermM.ByM[x:=N]wedenotethetermobtainedbysubstitutingthetermNforallthefreeoccurrencesofthevariablexinM,takingintoaccountthatfreevariablesofNremainfreeinthetermobtained.

Theaxiomofβ-reductionis(λx.M)N→βM[x:=N].Atermoftheform(λx.M)Niscalledβ-redex.Thetransitivereflexiveclosureof→βisdenotedby→→β.Atermisanormalformifitdoesnotcontainβ-redexes.

Weconsiderherethefollowingcomputationalbehavioursoflambdaterms.Definition2.(Normalizationproperties)

i)Mhasanormalform,M∈N,ifMreducestoanormalform;ii)Mhasaheadnormalform,M∈HN,ifMreducestoatermofthe

→→→

formλx.yM(wherepossiblyyappearsinx);iii)Mhasaweakheadnormalform,M∈WN,ifMreducestoanab-stractionortoatermstartingwithafreevariable.

Foreachoftheaboveproperties,weshallconsideralsothecorrespondingpersistentversion(seeDefinition3).PersistentlynormalizingtermshavebeenintroducedinB¨ohmandDezani[6].

Definition3.(Persistentnormalizationproperties)

i)AtermMispersistentlynormalizing,M∈PN,ifMN∈Nforall

→

termsNinN.

→

36

ii)AtermMispersistentlyheadnormalizing,M∈PHN,ifMN∈HN

→

foralltermsN.iii)AtermMispersistentlyweaknormalizing,M∈PWN,ifMN∈

→

WNforalltermsN.Example1.LetI≡λx.x,∆≡λx.xx,Y≡λf.(λx.f(xx))(λx.f(xx)),K≡λxy.x.

i)λx.x∆∆∈N,butλx.x∆∆∈/PWN,since(λx.x∆∆)I→→β∆∆∈/WN.ii)λx.y(∆∆)∈PHN,butλx.y(∆∆)∈/N.

iii)λx.x(∆∆)∈HN,butλx.x(∆∆)∈/Nandλx.x(∆∆)∈/PWN,since

(λx.x(∆∆))∆→β∆(∆∆)∈/WN.iv)YK∈PWN,butYK∈/HN.

v)λx.∆∆∈WN,butλx.∆∆∈/HNandλx.∆∆∈/PWN,since(λx.∆∆)M→→β∆∆∈/WN.

→

→

ΛWN

37

Nootherinclusionholdsbetweentheabovesets.

Ourgoalistobuildaninverselimitlambdamodel,Scott[23],whichsatisfiesthefollowingcondition:

foreachoneoftheabovesixsetsoftermsthereisacorrespondingelementinthemodelsuchthatatermbelongstothesetiffitsinterpretation(inasuitableenvironment)isbiggerthanorequaltothatelement.

Weneedthereforetodiscussthefunctionalbehavioursofthetermsbe-longingtotheseclasses,inparticularwithrespecttothestepfunctions,whereasusualastepfunctiona⇒bisdefinedby

λd.ifa⊑dthenbelse⊥.

Aweakheadnormalizingtermeitherreducestoanabstractionortoanapplicationofavariableto(possiblyzero)terms:inbothcases(inasuitableenvironment)itbehavesatleastaswellasthestepfunction⊥⇒⊥.Sowecanchoosetherepresentativeofthestepfunction⊥⇒⊥astheelementwhichcorrespondstoWN.Weneedtoconsideramodelinwhichthisstepfunctionisnotthebottomofthewholedomain,i.e.asolutionofthedomainequationD=[D→D]⊥,whereasusual[D→D]isthedomainofcontinuousfunctionsfromDtoDand⊥istheliftingoperator.

Apersistentlyweaknormalizingtermappliedtoanynumberofarbitrarytermsgivesaweakheadnormalizingterm:i.e.itbehavesatleastaswellasthestepfunction⊥󰀅⇒...⇒⊥󰀆⇒⊥forallvaluesofn.Therefore,the

n󰀁

elementrepresentingn∈IN(⊥󰀅⇒...⇒⊥󰀆⇒⊥)isagoodcandidateforthe

n

correspondencewiththesetPWN.

Aheadnormalizingtermwhenappliedtoapersistentlyheadnormaliz-ingtermreducestoaheadnormalizingterm:initsturnapersistentlyheadnormalizingtermappliedtoanarbitrarytermgivesapersistentlyheadnor-ˆaretwoelementsofD0correspondingmalizingterm.Therefore,ifhandh

respectivelytothesetsHNandPHN,theyrepresentthestepfunctionsˆ⇒hand⊥⇒ˆhh.

Anormalizingtermisalsoaheadnormalizingtermandthereforeitbe-ˆ⇒h.Apersistentlynormalizinghavesatleastaswellthestepfunctionh

termisalsoapersistentlyheadnormalizingtermandthereforeitbehavesatleastaswellthestepfunction⊥⇒ˆh.Apersistentlynormalizingtermap-pliedtoanormalizingtermgivesapersistentlynormalizingterm.Moreover,anormalizingtermappliedtoapersistentlynormalizingtermisinturnanormalizingterm.

38

ˆaretwoelementsofD0correspondingrespectivelyTherefore,ifnandn

ˆ⇒h)⊔(ˆtothesetsNandPN,theyrepresentthefunctions(hn⇒n)and

ˆ)⊔(n⇒ˆ(⊥⇒hn).

Tosumupwedefineourmodelasfollows.Definition4.LetD∞betheinverselimitmodelobtainedbytakingasD0thelatticeofFig.2,asD1thelattice[D0→D0]⊥,andbydefiningtheembeddingi0:D0→[D0→D0]⊥asfollows:

ˆ)⊔(n⇒ˆˆ⇒h)⊔(ˆi0(ˆn)=(⊥⇒hn),i0(n)=(hn⇒n),

ˆ)=⊥⇒hˆ,i0(h)=hˆ⇒h,i0(⊥)=⊥.i0(h

ˆFn

󰀐󰀐FFF󰀐󰀐FF󰀐󰀐ˆnhFFF󰀐󰀐FF󰀐󰀐F󰀐󰀐

h

39

∞

⊒v)M∈PWNiff[M]Dρˆn

󰀁

n∈IN(⊥󰀅⇒...⇒⊥󰀆⇒⊥);

n

∞

vi)M∈WNiff[M]D⊒⊥⇒⊥.ρˆn

TheproofofthistheoremisdonebymeansofafinitarylogicaldescriptionofD∞obtainedbydefininganintersectiontypeassignmentsysteminSec-tion3.

3.Thetypeassignmentsystem

Stonedualitiesallowtodescribespecialclassesoftopologicalspacesbymeansof(possiblyfinitary)partialorders.Typically,thesepartialordersaregivenbythetopology,abasisforitorasubbasisforit.TheseminalresultisthedualitybetweenthecategoriesofStonespacesandofBooleanalgebras(seeJohnstone[14]).Otherveryimportantexamplesarethedescriptionsofω-algebraiccompletelatticesasintersectiontypetheoriesinCoppoetal.[7],ScottdomainsasinformationsystemsinScott[25],andSFPdomainsaspre-localesinAbramsky[1].ItisworthwhiletomentionalsoMartin-L¨of’sdomaininterpretationofintuitionistictypetheoryinMartin-L¨of[18].

AsstatedfirstinCoppoetal.[7]andprovedinAlessi[2],wecandescribeaninverselimitmodelD∞bytaking:

•thetypesfreelygeneratedbyclosing(asetofatomictypescorrespond-ingto)theelementsofD0underthefunctiontypeconstructor→andtheintersectiontypeconstructor∩;•thepreorderbetweentypesinducedbyreversingtheorderinD0andbyencodingtheinitialembedding,accordingtothecorrespondence:

functiontypeconstructorintersectiontypeconstructor

→→

stepfunction

join.

ForthemodelD∞discussedintheprevioussectionweobtainthefollow-ingdefinitions.

40

Definition5.(ThesetToftypes)ThesetToftypesisdefinedasfollows.

T

::=

ν|νˆ|µ|µˆ|Ω|T→T|T∩T

Typeswillbedenotedbyσ,τ,...,σ1,....Whenwritingtypesweshall

usethefollowingconvention:theconstructor∩takesprecedenceovertheconstructor→anditassociatestotheright.

Now,wegivethecorrespondencebetweentypesandelementsofD∞(asusualweidentifyelementsofDnwiththeirprojectionsinD∞).

Definition6.(Themappingm)

Themappingm:T→D∞isdefinedasfollows.

ˆm(µ)=hm(ν)=nm(ˆν)=n

m(σ→τ)=m(σ)⇒m(τ)

ˆm(Ω)=⊥m(ˆµ)=h

m(σ∩τ)=m(σ)⊔m(τ).

Definition7.(PreorderonT)

Therelation≤isdefinedonTbythefollowingaxiomsandrules:(ˆνν)(νµ)(Ω)(ˆν→)(ˆµ→)(refl)(idem)(incl)

νˆ≤ν(ˆνµˆ)νˆ≤µˆν≤µ(ˆµµ)µˆ≤µσ≤Ω(Ω→)σ→Ω≤Ω→Ωνˆ∼(Ω→µˆ)∩(ν→νˆ)(ν→)ν∼(ˆµ→µ)∩(ˆν→ν)µˆ∼Ω→µˆ(µ→)µ∼µˆ→µσ≤σ(mon)σ≤σ′,τ≤τ′⇒σ∩τ≤σ′∩τ′σ≤σ∩σ(trans)σ≤τ,τ≤ρ⇒σ≤ρσ∩τ≤σ,σ∩τ≤τ(amon)σ≤σ′,τ≤τ′⇒σ′→τ≤σ→τ′

(arint)(σ→τ)∩(σ→ζ)≤σ→τ∩ζ

whereσ∼τisshortforσ≤τandτ≤σ.

ThefirstfouraxiomscorrespondtothepartialorderinD0.Axiom(Ω)saysthatΩisthetoptype,andthereforegivesforΩboththepartialorderinD0andtheembeddinginD1.Theaxioms(ˆν→),(ν→),(ˆµ→),(µ→)encodetheinitialembeddingoftheconstantsdifferentfromΩinD1.Theremainingaxiomsarestandardpropertiesofjoinsandstepfunctions.

Webuildfiltersonthesetoftypes:theywillcorrespondtotheelementsofD∞.

41

Definition8.(ThesetFoffilters)i)AfilterisasetX⊆Tsuchthat:

(a)Ω∈X;

(b)ifσ≤τandσ∈X,thenτ∈X;(c)ifσ,τ∈X,thenσ∩τ∈X;ii)FdenotesthesetoffiltersoverT;

iii)ifX⊆T,↑XdenotesthefiltergeneratedbyX;

iv)afilterisprincipalifitisoftheshape↑{σ},forsometypeσ.We

shalldenote↑{σ}simplyby↑σ.ItiseasytoverifythatthesetFoffilters,orderedbysubsetinclusion,isanω-algebraiccompletelattice,where↑Ωisthebottom,andTisthetop.Moreover,thefiniteelementsareexactlytheprincipalfilters.

UsingthemappingmwecanshowthatFandD∞areisomorphicasω-algebraiccompletelattices,asproved(forageneralcase)inAlessi[2].

Theorem2.(Isomorphism)

Themappingm∗:F→D∞definedby

󰀂

∗

m(σ)m(X)=

σ∈X

isalatticeisomorphismbetweenFandD∞.Noticethatm∗(↑σ)=m(σ).

DuetotheaboveisomorphismtheinterpretationsoflambdatermsinD∞

areisomorphicwiththefiltersoftypesonecanderiveinthefollowingtypeassignmentsystem(Alessi[2]).Thisgivesusafinitarylogicaldescriptionofthemodel.

AtypeassignmentisanexpressionoftheformM:τ,whereM∈Λisthesubjectandτ∈Tisthepredicate.AcontextΓisa(possiblyinfinite)setoftypeassignmentsoftheshapex:σwithdifferentsubjects(termvariables).Definition9.(Thetypeassignmentsystem)

ThetypeassignmentM:τisderivablefromthecontextΓ,notationΓ⊢M:τ,ifΓ⊢M:τcanbegeneratedbythefollowingaxiomsandrules.

42

Γ⊢M:Ω

Γ⊢M:σ→τΓ⊢N:σ

(Ω)

(→I)

Γ⊢λx.M:σ→τ

Γ⊢M:σΓ⊢M:τ

Γ⊢M:τ

(≤)

Theorem3.(Finitarylogicaldescription)

ForanylambdatermMandenvironmentρ:var→D∞,

∞

=m∗({τ∈T|∃Γ|=ρ.Γ⊢M:τ}),[M]Dρ

whereΓ|=ρifandonlyif(x:σ)∈Γimpliesm(σ)⊑ρ(x).

Theorem3allowsustorephrasethemaintheoremofprevioussection,

Theorem1,asfollows:

Theorem4.(MainTheorem,VersionII)LetΓνˆ|x∈var}.Then:ˆbethecontextdefinedbyΓνˆ={x:νˆ;i)M∈PNiffΓνˆ⊢M:νii)M∈NiffΓνˆ⊢M:ν;iii)M∈PHNiffΓνˆ;ˆ⊢M:µiv)M∈HNiffΓνˆ⊢M:µ;

nv)M∈PWNiffΓνN;ˆ⊢M:Ω→Ωforalln∈I

vi)M∈WNiffΓνˆ⊢M:Ω→Ω.

TheproofsoftheifpartsofthisTheoremaremainlystraightforwardinductionsandcasesplit,andfollow,butthecaseofpersistentlynormalizingterms.ForthatcasewedevelopedanewcharacterizationofthesetermswhichislessgeneralbutmuchsimplerthantheonepresentedinDezanietal.[10].

Theproofsoftheonlyifpartsrequiretheset-theoreticsemanticsofin-tersectiontypesusingsaturatedsets.Thereducibilitymethodisagenerallyacceptedwayforprovingthestrongnormalizationpropertyofvarioustype

43

systems(Tait[26],[27],Girard[13],Mitchell[19],[20],Leivant[17],Pot-tinger[22],Krivine[16],vanBakel[28],Ghilezan[12],AmadioandCurien[3],Gallier[11],Dezanietal.[10]).

Inallthesepapersdifferentpropertiesarecharacterizedbymeansofdifferenttypeassignmentsystems:sothenoveltyofthepresentapproachisthatwecharacterizeallsixcomputationalpropertiesoftermsbymeansofauniquetypeassignmentsystem,whichinducesaλ-model.Moreover,inallthepapersmentioneddifferentcomputationalpropertiesrequiredifferenttypeinterpretationsinthereducibilitymethod,whereasweadaptthereducibilitymethodusingasingletypeinterpretationforallsixcomputationalproperties.

Lastly,weremarkthatthereareessentiallytwosemanticsforintersec-tiontypesintheliteratureandthatthepresentpaperdealswithbothofthem.Theset-theoreticalsemantics,originallyintroducedinbyBarendregtetal.[4],generalizestheonegivenbyScottforsimpletypes(Scott[24]).Themeaningsoftypesaresubsetsofthedomainofdiscourse,arrowtypesarede-finedaslogicalpredicatesandintersectionisset-theoreticintersection.Thissemanticsisatthebasisofourapplicationofthereducibilitymethod.ThesecondsemanticsviewstypesascompactelementsofPlotkin’sλ-structures(Plotkin[21]).Accordingtothisinterpretation,theuniversaltypedenotestheleastelement,intersectionsdenotejoinsofcompactelements,andarrowtypesallowtointernalizethespaceofcontinuousendomorphisms.Thisse-manticsallowsustoobtaintheisomorphismbetweenthemodelD∞andthesetFoffiltersoftypes.

4.Acknowledgement

Wearegratefultotherefereeforcarefulreadingandusefulsuggestions.

5.References

[1]AbramskyS.;Domaintheoryinlogicalform,Ann.PureAppl.Logic,Vol.

51(1–2),1991,pp.1–77.[2]AlessiF.;Struttureditipi,teoriadeidominiemodellidellambdacalcolo,Ph.D.

thesis,TorinoUniversity,1991.

44

[3]AmadioR.M.,CurienP.L.;DomainsandLambda-Calculi,CambridgeUniver-sityPress,Cambridge1998.[4]BarendregtH.,CoppoM.,Dezani-CiancagliniM.;Afilterlambdamodeland

thecompletenessoftypeassignment,J.SymbolicLogic,Vol.48(4),1983,pp.931–940.[5]BarendregtH.P.;TheLambdaCalculus:ItsSyntaxandSemantics,North-Holland,Amsterdam,revisededition,1984.[6]B¨ohmC.,Dezani-CiancagliniM.;λ-termsastotalorpartialfunctionsonnor-malforms,in:C.B¨ohm,(ed.),λ-calculusandComputerScienceTheory,Lec-tureNotesinComputerScience,Springer–Verlag,Vol.37,Berlin1975,pp.

96–121.[7]CoppoM.,Dezani-CiancagliniM.,HonsellF.,LongoG.;Extendedtypestruc-turesandfilterlambdamodels,in:G.Lolli,G.Longo,andA.Marcja,(eds.),Logiccolloquium’82,North-Holland,Amsterdam1984,pp.241–262.[8]Dezani-CiancagliniM.,GhilezanS.;Alambdamodelcharacterizingcomputa-tionalbehavioursofterms,in:Y.Toyama,(ed.),InternationalWorkshoponRewritinginProofandComputation,RPC’01,2001,pp.100–119.[9]Dezani-CiancagliniM.,GhilezanS.;Twobehaviourallambdamodels,in:

H.GeuversandF.Wiedijk,(eds.),TYPES2002,LectureNotesinComputerScience,Springer–Verlag,2003(toappear).[10]Dezani-CiancagliniM.,HonsellF.,MotohamaY.;Compositionalcharacteriza-tionofλ-termsusingintersectiontypes,in:M.NielsenandB.Rovan,(eds.),MathematicalFoundationsofComputerScience2000,LectureNotesinCom-puterScience,Springer–Verlag,Vol.13,2000,pp.304–313.[11]GallierJ.;Typinguntypedλ-terms,orreducibilitystrikesagain!,Ann.Pure

Appl.Logic,Vol.91,1998,pp.231–270.[12]GhilezanS.;Strongnormalizationandtypabilitywithintersectiontypes,Notre

DameJ.FormalLogic,Vol.37(1),1996,pp.44–52.[13]GirardJ.Y.;Uneextensiondel’interpr´etationdeG¨odela`l’analyse,etson

applicationa`l’eliminationdescoupuresdansl’analyseetlath´eoriedestypes,in:J.E.Fenstadt,(ed.),2ndScandinavianLogicSymposium,North-Holland,1971,pp.63–92.[14]JohnstoneP.T.;StoneSpaces,CambridgeUniversityPress,Cambridge1986,

reprintofthe1982edition.[15]KegelmanM.;ContinuousDomainsinLogicalForm,Ph.D.thesis,

SchoolofComputerScience,TheUniversityofBirmingham,1999,http://www.cs.bham.ac.uk/˜axj/former-students.html[16]KrivineJ.L.;Lambda-calculTypesetmod`eles,Masson,Paris1990.

45

[17]LeivantD.;Typingandcomputationalpropertiesoflambdaexpressions,Theo-ret.Comput.Sci.,Vol.44(1),1986,pp.51–68.[18]Martin-L¨ofP.;Lecturenotesondomaininterpretationoftypetheory,Pro-grammingMethodologyGroup,WorkshopontheSemanticsofProgramming

Languages,ChalmersUniversityofTechnology,1983.[19]MitchellJ.C.;Typesystemsforprogramminglanguages,in:J.vanLeeuwen,

(ed.),HandbookofTheoreticalComputerScience,Elsevier,Amsterdam,Vol.B,1990,pp.415–431.[20]MitchellJ.C.;FoundationforProgrammimgLanguages,MITPress,Boston

1996.[21]PlotkinG.D.;Set-theoreticalandotherelementarymodelsoftheλ-calculus,

Theoret.Comput.Sci.,Vol.121(1–2),1993,pp.351–409.[22]PottingerG.;Atypeassignmentforthestronglynormalizableλ-terms,in:J.P.

SeldinandJ.R.Hindley,(eds.),ToH.B.Curry:EssaysonCombinatoryLogic,LambdaCalculusandFormalism,AcademicPress,London1980,pp.561–577.[23]ScottD.S.;Continuouslattices,in:F.W.Lawvere,(ed.),Toposes,Algebraic

GeometryandLogic,LectureNotesinMathematics,Springer–Verlag,Vol.274,Berlin1972,pp.97–136.[24]ScottD.S.;Openproblem,in:C.B¨ohm,(ed.),LambdaCalculusandComputer

ScienceTheory,LectureNotesinComputerScience,Springer–Verlag,Vol.37,Berlin1975,p.369.[25]ScottD.S.;Domainsfordenotationalsemantics,in:M.NielsenandE.M.

Schmidt,(eds.),Automata,LanguagesandProgramming,LectureNotesinComputerScience,Springer–Verlag,Vol.140,Berlin1982,pp.577–613.[26]TaitW.W.;IntensionalinterpretationsoffunctionalsoffinitetypeI,Journal

ofSymbolicLogic,Vol.32,1967,pp.198–212.[27]TaitW.W.;Arealizabilityinterpretationofthetheoryofspecies,InR.Parikh,

(ed.),LogicColloquium,LectureNotesinMathematics,Springer–Verlag,Vol.453,Berlin1975,pp.240–251.[28]vanBakelS.;Completerestrictionsoftheintersectiontypediscipline,Theoret.

Comput.Sci.,1992,Vol.102(1),pp.135–163.

ReceivedNovember15,2002