Lambda theories of effective lambda models

ChantalBerline1,GiulioManzonetto1,2,andAntoninoSalibra2chantal.berline@pps.jussieu.fr,{gmanzone,salibra}@dsi.unive.it

LaboratoirePPS,CNRS-Universit´eParis7,

2,placeJussieu(case7014),75251ParisCedex05,France

2

Universit`aCa’FoscaridiVenezia,

DipartimentodiInformaticaViaTorino155,30172Venezia,Italy

1

Abstract.Alongstandingopenproblemiswhetherthereexistsanon-syntacticalmodeloftheuntypedλ-calculuswhosetheoryisexactlytheleastλ-theoryλβ.Inthispaperweinvestigatethemoregeneralques-tionofwhethertheequational/ordertheoryofamodeloftheuntypedλ-calculuscanberecursivelyenumerable(r.e.forbrevity).Weintro-duceanotionofeffectivemodelofλ-calculus,whichcoversinparticularallthemodelsindividuallyintroducedintheliterature.Weprovethattheordertheoryofaneffectivemodelisneverr.e.;fromthisitfollowsthatitsequationaltheorycannotbeλβ,λβη.Wethenshowthatnoeffectivemodellivinginthestableorstronglystablesemanticshasanr.e.equationaltheory.ConcerningScott’ssemantics,weinvestigatetheclassofgraphmodelsandprovethatnoordertheoryofagraphmodelcanber.e.,andthatthereexistsaneffectivegraphmodelwhoseequa-tional/ordertheoryistheminimumone.Finally,weshowthattheclassofgraphmodelsenjoysakindofdownwardsL¨owenheim-Skolemtheorem.Keywords:Lambdacalculus,Effectivelambdamodels,Recursivelyenu-merablelambdatheories,Graphmodels,L¨owenheim-Skolemtheorem.

1Introduction

Lambdatheoriesareequationalextensionsoftheuntypedλ-calculusclosedun-derderivation.Theyarisebysyntacticalorsemanticconsiderations.Indeed,aλ-theorymaycorrespondtoapossibleoperational(observational)semanticsofλ-calculus,aswellasitmaybeinducedbyamodelofλ-calculusthroughthekernelcongruencerelationoftheinterpretationfunction.Althoughresearchershavemainlyfocusedtheirinterestonalimitednumberofthem,theclassofλ-theoriesconstitutesaveryrichandcomplexstructure(see[1,4,5]).

Topologyisatthecenteroftheknownapproachestogivingmodelsoftheuntypedλ-calculus.Afterthefirstmodel,foundbyScottin1969inthecategoryofcompletelatticesandScottcontinuousfunctions,alargenumberofmathe-maticalmodelsforλ-calculus,arisingfromsyntax-freeconstructions,havebeenintroducedinvariouscategoriesofdomainsandwereclassifiedintosemanticsaccordingtothenatureoftheirrepresentablefunctions,seee.g.[1,4,19].Scottcontinuoussemantics[22]isgiveninthecategorywhoseobjectsarecomplete

partialordersandmorphismsareScottcontinuousfunctions.Thestableseman-tics(Berry[7])andthestronglystablesemantics(Bucciarelli-Ehrhard[8])arerefinementsofthecontinuoussemantics,introducedtocapturethenotionof“se-quential”Scottcontinuousfunction.Ineachofthesesemanticsitispossibletobuildup2ℵ0modelsinducingpairwisedistinctλ-theories[16,17].Nevertheless,allareequationallyincomplete(see[15,2,20,21])inthesensethattheydonotrepresentallpossibleconsistentλ-theories.Itisinterestingtonotethatthereareveryfewknownequationaltheoriesofλ-modelslivinginthesesemanticsthatcanbedescribedsyntactically:namely,thetheoryofB¨ohmtreesandvariantsofit.Noneofthesetheoriesisr.e.

Berlinehasraisedin[4]thenaturalquestionofwhether,givenaclassofmodelsofλ-calculus,thereisaminimumλ-theoryrepresentedbyit.Thisques-tionrelatestothelongstandingopenproblemproposedbyBarendregtabouttheexistenceofacontinuousmodelor,moregenerally,ofanon-syntacticalmodelofλβ(λβη).DiGianantonio,HonsellandPlotkin[12]haveshownthatScottcon-tinuoussemanticsadmitsaminimumtheory,atleastifwerestricttoextensionalmodels.Anotherresultof[12],inthesamespirit,istheconstructionofanex-tensionalmodelwhosetheoryisλβη,afortioriminimal,inaweakly-continuoussemantics.However,theconstructionofthismodelstartsfromthetermmodelofλβη,andhenceitcannotbeseenashavingapurelynonsyntacticalpresentation.Morerecently,BucciarelliandSalibra[9,10]haveshownthattheclassofgraphmodelsadmitsaminimumλ-theorydifferentfromλβ.Graphmodels,isolatedintheseventiesbyPlotkin,ScottandEngeler(seee.g.[1])withinthecontinu-oussemantics,haveprovedusefulforshowingtheconsistencyofextensionsofλ-calculusandforstudyingoperationalfeaturesofλ-calculus(see[4]).Inthispaperweinvestigatetherelatedquestionofwhethertheequationaltheoryofamodelcanberecursivelyenumerable(r.e.forbrevity).Asfarasweknow,thisproblemwasfirstraisedin[5],whereitisconjecturedthatnographmodelcanhaveanr.e.theory.Butweexpectthatthiscouldindeedbetrueforallmodelslivinginthecontinuoussemantics,anditsrefinements.

Wefinditnaturaltoconcentrateonmodelswithbuilt-ineffectivityprop-erties.Itseemsindeedreasonabletothinkthat,ifeffectivemodelsdonotevensucceedtohaveanr.e.theory,thentheotheroneshavenochancetosucceed.Anotherjustificationforconsideringeffectivemodelscomesfromapreviousre-sultobtainedfortypedλ-calculus.Indeed,itwasprovedin[3]thatthereexistsanon-syntacticalmodelofGirard’ssystemFwhosetheoryisλβη.ThismodellivesinScott’scontinuoussemantics,andcaneasilybecheckedtobe“effective”inthesamespiritasinthepresentpaper(see[3,AppendixC]forasketchypresentationofthemodel).

Startingfromtheknownnotionofaneffectivedomain,weintroduceageneralnotionofaneffectivemodelofλ-calculusandwestudythemainpropertiesofthesemodels.Effectivemodelsareomni-presentinthecontinuous,stable

andstronglystablesemantics.Inparticular,allthemodelswhichhavebeenintroducedindividuallyintheliteraturecaneasilybeprovedeffective3.

Thefollowingarethemainresultsofthepaper:1.LetDbeaneffectivemodelofλ-calculus.Then:(i)TheordertheoryOrd(D)ofDisnotr.e.

(ii)TheequationaltheoryEq(D)ofDisnotthetheoryλβ(λβη).

(iii)Ifforsomeλ-termMthereareonlyfinitelymanyλ-definableelements

belowtheinterpretationofM(e.g.if⊥∈Disλ-definable),thenEq(D)isnotr.e.Concerningtheexistenceofanon-syntacticaleffectivemodelwithanr.e.equa-tionaltheory,weareabletogiveadefinitenegativeanswerforall(effective)stableandstronglystablemodels:

2.Noeffectivemodellivinginthestableorstronglystablesemanticshasanr.e.equationaltheory.ConcerningScottcontinuoussemantics,theproblemlooksmuchmoredifficult.Weconcentratehereontheclassofgraphmodels(see[5,6,9–11]forearlierinvestigationofthisclass)andshowthefollowingresults:

3.LetDbeanarbitrarygraphmodel.Then:(i)TheordertheoryOrd(D)ofDisnotr.e.

(ii)IfDisfreelygeneratedbyafinite“partialmodel”,thentheequational

theoryEq(D)ofDisnotr.e.4.Thereexistsaneffectivegraphmodelwhoseequational/ordertheoryismin-imalamongalltheoriesofgraphmodels.5.(L¨owenheim-Skolemtheoremforgraphmodels)Everyequational/ordergraphtheory(where“graphtheory”means“theoryofagraphmodel”)isthethe-oryofagraphmodelhavingacarriersetofminimalcardinality.ThelastresultpositivelyanswersQuestion3in[4,Section6.3]fortheclassofgraphmodels.

ThecentraltechnicaldeviceusedinthispaperisVisser’sresult[25]statingthatthecomplementsofβ-closedr.e.setsofλ-termsenjoythefiniteintersectionproperty(seeTheorem2).

2Preliminaries

Tokeepthisarticleself-contained,wesummarizesomedefinitionsandresultsconcerningλ-calculusthatweneedinthesubsequentpartofthepaper.Withregardtothelambdacalculuswefollowthenotationandterminologyof[1].

Wedenotebythesetofnaturalnumbers.AsetA⊆isrecursivelyenumerable(r.e.forshort)ifitisthedomainofapartialrecursivefunction.Thecomplementofarecursivelyenumerablesetiscalledaco-r.e.set.IfbothAanditscomplementarer.e.,Aiscalleddecidable.WewilldenotebyREthecollectionofallr.e.subsetsof.

AnumerationofasetAisamapfromontoA.W:→REdenotestheusualnumerationofr.e.sets(i.e.,Wnisthedomainofthen-thcomputablefunctionφn).

2.1Lambdacalculusandlambdamodels

ΛandΛoare,respectively,thesetofλ-termsandofclosedλ-terms.Concerningspecificλ-termsweset:

I≡λx.x;

T≡λxy.x;

F≡λxy.y;

Ω≡(λx.xx)(λx.xx).

AsetXofλ-termsistrivialifeitherX=∅orX=Λ.

Wedenoteαβ-conversionbyλβ.Aλ-theoryTisacongruenceonΛ(withrespecttotheoperatorsofabstractionandapplication)whichcontainsλβ.WewriteM=TNfor(M,N)∈T.IfTisaλ-theory,then[M]Tdenotestheset{N:N=TM}.Aλ-theoryTis:consistentifT=Λ×Λ;extensionalifitcontainstheequationI=λxy.xy;recursivelyenumerableifthesetofG¨odelnumbersofallpairsofT-equivalentλ-termsisr.e.Finally,λβηistheleastextensionalλ-theory.

Solvableλ-termscanbecharacterizedasfollows:aλ-termMissolvableif,andonlyif,ithasaheadnormalform,thatis,M=λβλx1...xn.yM1...Mkforsomen,k≥0andλ-termsM1,...,Mk.M∈Λisunsolvableifitisnotsolvable.

Theλ-theoryH,generatedbyequatingalltheunsolvableλ-terms,iscon-sistentby[1,Theorem16.1.3].Aλ-theoryTissensibleifH⊆T,whileitissemi-sensibleifitcontainsnoequationsoftheformU=SwhereSissolv-ableandUunsolvable.Consistentsensibletheoriesaresemi-sensible(see[1,Cor.4.1.9])andareneverr.e.(see[1,Section17.1]).

Itiswellknown[1,Chapter5]thatamodelofλ-calculus(λ-model,forshort)canbedefinedasareflexiveobjectinaccc(Cartesianclosedcategory)C,thatistosayatriple(D,F,λ)suchthatDisanobjectofCandF:D→[D→D],λ:[D→D]→DaremorphismssuchthatF◦λ=id[D→D].InthefollowingwewillmainlybeinterestedinScott’scccofcposandScottcontinuousfunctions(continuoussemantics),butwewillalsodrawconclusionsforBerry’scccofDI–domainsandstablefunctions(stablesemantics),andforEhrhard’scccofDI-domainswithcoherenceandstronglystablefunctionsbetweenthem(stronglystablesemantics).WerecallthatDI-domainsarespecialScottdomains,andthatScottdomainsarespecialcpos(see,e.g.,[24]).

LetDbeacpo.ThepartialorderofDwillbedenotedby󰀦D.WeletEnvDbethesetofenvironmentsρmappingthesetVarofvariablesofλ-calculusintoD.Foreveryx∈Varandd∈Dwedenotebyρ[x:=d]theenvironmentρ󰀗whichcoincideswithρ,exceptonx,whereρ󰀗takesthevalued.AreflexivecpoDgeneratesaλ-modelD=(D,F,λ)withtheinterpretationofaλ-termdefinedasfollows:

DDDD

xDρ=ρ(x);(MN)ρ=F(Mρ)(Nρ);(λx.M)ρ=λ(f),

DDD

wherefisdefinedbyf(d)=MρforMρifM[x:=d]foralld∈D.WewriteM

isaclosedλ-term.InthefollowingF(d)(e)willalsobewrittend·eorde.

Eachλ-modelDinducesaλ-theory,denotedherebyEq(D),andcalledtheequationaltheoryofD.Thus,M=N∈Eq(D)if,andonlyif,MandNhavethesameinterpretationinD.AreflexivecpoDinducesalsoanordertheory

DD

Ord(D)={M󰀦N:Mρ󰀦DNρforallenvironmentsρ}.

2.2Effectivedomains

AtripleD=(D,󰀦D,d)iscalledaneffectivedomainif(D,󰀦D)isaScottdomainanddisanumerationofthesetK(D)ofitscompactelementssuchthattherelations“dmanddnhaveanupperbound”and“dn=dm󰀥dk”arebothdecidable(see,e.g.,[24,Chapter10]).

WerecallthatanelementvofaneffectivedomainDissaidr.e.(decidable)iftheset{n:dn󰀦Dv}isr.e.(decidable);wewillwriteDr.e.(Ddec)forthesetofr.e.(decidable)elementsofD.ThesetK(D)ofcompactelementsisincludedwithinDdec.Usingstandardtechniquesofrecursiontheoryitispossibletogetinauniformwayanumerationξ:→Dr.e.whichisadequateinthesensethattherelationdk󰀦Dξnisr.e.in(k,n)andtheinclusionmappingι:K(D)→Dr.e.iscomputablew.r.t.d,ξ.

ThefullsubcategoryEDofthecategoryofScott-domainswitheffectivedomainsasobjectsandcontinuousfunctionsasmorphismsisaccc.

Acontinuousfunctionf:D→D󰀗isanr.e.elementintheeffectivedomainofScottcontinuousfunctions(i.e.,f∈[D→D󰀗]r.e.)if,andonlyif,itsrestrictionf󰀁:Dr.e.→D󰀗r.e.iscomputablew.r.t.ξ,ξ󰀗,i.e.,thereisacomputablemap

󰀗

g:→suchthatf(ξn)=ξg(n).Insuchacasewesaythatgtracksf.

2.3Graphmodels

TheclassofgraphmodelsbelongstoScottcontinuoussemantics(see[5]foracompletesurveyonthisclassofmodels).Historically,thefirstgraphmodelwasScott’sPω,whichisalsoknownintheliteratureas“thegraphmodel”.“Graph”referredtothefactthatthecontinuousfunctionswereencodedinthemodelvia(asufficientfragmentof)theirgraph.

Asamatterofnotation,foreverysetG,G∗isthesetofallfinitesubsetsofG,whileP(G)isthepowersetofG.

Definition1.AgraphmodelGisapair(G,cG),whereGisaninfiniteset,calledthecarriersetofG,andcG:G∗×G→Gisaninjectivetotalfunction.

SuchpairGgeneratesthereflexivecpo(P(G),⊆,λ,F),whereλandFaredefinedasfollows,forallf∈[P(G)→P(G)]andX,Y⊆G:λ(f)={cG(a,α):α∈f(a)anda∈G∗}andF(X)(Y)={α∈G:(∃a⊆Y)cG(a,α)∈X}.FormoredetailswereferthereadertoBerline[4].

Theinterpretationofaλ-termMintoaλ-modelhasbeendefinedinSec-G

tion2.1.However,inthiscontextwecanmakeexplicittheinterpretationMρofaλ-termMasfollows:

GGGG

(MN)Gρ={α:(∃a⊆Nρ)cG(a,α)∈Mρ};(λx.M)ρ={cG(a,α):α∈Mρ[x:=a]}.

WeturnnowtotheinterpretationofΩingraphmodels(thedetailsoftheproofare,forexample,workedoutin[6,Lemma4]).

Lemma1.α∈ΩGif,andonlyif,thereisa⊆(λx.xx)GsuchthatcG(a,α)∈a.Inthefollowingweusetheterminology“graphtheory”asashorthandfor“theoryofagraphmodel”.Itiswellknownthattheequationalgraphtheoriesareneverextensionalandthatthereexistsacontinuumofthem(see[16]).In[9,10]theexistenceofaminimumequationalgraphtheorywasprovedanditwasalsoshownthatthisminimumtheoryisdifferentfromλβ.

Thecompletionmethodforbuildinggraphmodelsfrom“partialpairs”wasinitiatedbyLongoin[18]anddevelopedonawidescalebyKerthin[16,17].Definition2.ApartialpairAisgivenbyasetAandbyapartial,injectivefunctioncA:A∗×A→A.

ApartialpairisfiniteifAisfinite,andisagraphmodelifcAistotal.

Theinterpretationofaλ-terminapartialpairAisdefinedintheobvious

AA

way:(MN)Aρ={α∈A:(∃a⊆Nρ)[(a,α)∈dom(cA)∧cA(a,α)∈Mρ]};

A

(λx.M)Aρ={cA(a,α)∈A:(a,α)∈dom(cA)∧α∈Mρ[x:=a]}.Definition3.LetAbeapartialpair.ThecompletionofAisthegraphmodelEA=(EA,cEA)definedasfollows:

󰀂∗

×En)−dom(cA)).–EA=n∈En,whereE0=AandEn+1=En∪((En

∗

–Givena∈EA,α∈EA,

󰀁

cA(a,α)ifcA(a,α)isdefined

cEA(a,α)=

(a,α)otherwise

AnotionofrankcanbenaturallydefinedonthecompletionEAofapartialpairA.TheelementsofAaretheelementsofrank0,whileanelementα∈EA−Ahasranknifα∈Enandα∈En−1.

LetAandBbetwopartialpairs.AmorphismfromAintoBisamapf:A→Bsuchthat(a,α)∈dom(cA)implies(fa,fα)∈dom(cB)and,insuchacasef(cA(a,α))=cB(fa,fα).Isomorphismsandautomorphismscanbedefinedintheobviousway.Aut(A)denotesthegroupofautomorphismsofthepartialpairA.

Lemma2.LetG,G󰀗begraphmodelsandf:G→G󰀗beamorphism.IfM∈Λ󰀅

GG

andα∈Mρ,thenfα∈Mf◦ρ.

2.4Co-r.e.setsoflambdaterms

Inthissectionwerecallthemainpropertiesofrecursiontheoryconcerningλ-calculusthatwillbeappliedinthefollowingsections.

Anr.e.(co-r.e.)setofλ-termsclosedunderβ-conversionwillbecalledaβ-r.e.(β-co-r.e.)set.

ThefollowingtheoremisduetoScott(see[1,Thm.6.6.2]).Theorem1.Asetofλ-termswhichisbothβ-r.e.andβ-co-r.e.istrivial.Definition4.AfamilyX=(Xi:i∈I)ofsetshastheFIP(finiteintersectionproperty)ifXi1∩···∩Xin=∅foralli1,...,in∈I.

Visser(see[1,Ch.17]and[25,Thm.2.5])hasshownthatthetopologyonΛgeneratedbytheβ-co-r.e.setsofλ-termsishyperconnected(i.e.,theintersectionoftwonon-emptyopensetsisnon-empty).Inotherwords:

Theorem2.Thefamilyofallnon-emptyβ-co-r.e.subsetsofΛhastheFIP.Corollary1.Everynon-emptyβ-co-r.e.setofλ-termscontainsanon-emptyβ-co-r.e.setofunsolvableλ-terms.

Proof.Thesetofallunsolvableλ-termsisβ-co-r.e.TheconclusionfollowsfromTheorem2.

3Effectivelambdamodels

Inthissectionweintroducethenotionofaneffectiveλ-modelandwestudythemainpropertiesofthesemodels.Weshowthattheordertheoryofaneffectiveλ-modelisnotr.e.andthatitsequationaltheoryisdifferentfromλβ,λβη.Ef-fectiveλ-modelsareomni-presentinthecontinuous,stableandstronglystablesemantics(seeSection4).Inparticular,alltheλ-modelswhichhavebeenin-troducedindividuallyintheliterature,tobeginwithScott’sD∞,caneasilybeprovedeffective.

Thefollowingnaturaldefinitionisenoughtoforcetheinterpretationfunctionofλ-termstobecomputablefromΛointoDr.e..However,otherresultsofthispaperwillneedamorepowerfulnotion.Thatisthereasonwhyweonlyspeakof“weakeffectivity”here.

Definition5.Aλ-modeliscalledweaklyeffectiveifitisareflexiveobject(D,F,λ)inthecategoryEDand,F∈[D→[D→D]]andλ∈[[D→D]→D]arer.e.elements.

Inthefollowingaweaklyeffectiveλ-model(D,F,λ)willbedenotedbyD.WefixbijectiveeffectivenumerationsνΛ:→Λofthesetofλ-termsandνvar:→Varofthesetofvariablesofλ-calculus.InparticularthisgivestothesetEnvDofallenvironmentsastructureofeffectivedomain.Λ⊥=Λ∪{⊥}istheusualflatdomainofλ-terms.Theelement⊥isalwaysinterpretedas⊥Dinacpo(D,󰀦D).

Proposition1.LetDbeaweaklyeffectiveλ-model.Thenthefunctionfmap-D

ping(ρ,M)→Mρisanelementof[EnvD×Λ⊥→D]r.e..Proof.(Sketch)BystructuralinductiononMitispossibletoshowtheexis-tenceofapartialcomputablemaptrackingf.TheonlydifficultcaseisM≡

D

λx.N.Sinceλisr.e.itissufficienttoprovethatthefunctiong:e→Nρ[x:=e]isalsor.e.Onceshownthath:(ρ,x,e)→ρ[x:=e]isr.e.,fromtheinductionhypothesisitfollowsthatthefunctiong󰀗(ρ,x,e)=f(h(ρ,x,e),N)isr.e.Thenbyapplyingthes-m-ntheoremofrecursiontheorytothecomputablefunctiontrackingg󰀗weobtainacomputablefunctiontrackingg,whichisthenr.e.Notation1.Wedefineforanye∈DandM∈Λo:

(i)e−≡{P∈Λo:PD󰀦De};

(ii)M−≡{P∈Λo:PD󰀦DMD}.

Corollary2.Ife∈Ddec,thene−isaβ-co-r.e.setofλ-terms.

Proof.Letρ∈(EnvD)r.e.beanenvironment.ByProposition1thereisacom-D

putablemapφtrackingtheinterpretationfunctionM→Mρofλ-termsfromΛintoDr.e.withrespecttotheeffectivenumerationνΛofΛandanadequatenumerationξofDr.e..Frome∈DdecitfollowsthatthesetX={n:ξn󰀦De}isco-r.e.Thisimpliesthatthesetφ−1(X),whichisthesetofthecodesofthe

D

elementsof{M∈Λ:Mρ󰀦De},isalsoco-r.e.Wegettheconclusionbecauseo

ΛisadecidablesubsetofΛ.

Definition6.Aweaklyeffectiveλ-modelDiscalledeffectiveifitsatisfiesthefollowingtwofurtherconditions:

(i)Ifd∈K(D)andei∈Ddec,thende1...en∈Ddec.

(ii)Iff∈[D→D]r.e.andf(e)∈Ddecforalle∈K(D),thenλ(f)∈Ddec.AnenvironmentρiscompactintheeffectivedomainEnvD(i.e.,ρ∈K(EnvD))ifρ(x)∈K(D)forallvariablesxand{x:ρ(x)=⊥D}isfinite.

Ddec

forallρ∈K(EnvD)}.Notation2.Wedefine:ΛdecD≡{M∈Λ:Mρ∈D

isclosedTheorem3.SupposeDisaneffectiveλ-model.ThenthesetΛdecD

underthefollowingrules:

1.x∈ΛdecDforeveryvariablex.

⇒yM1...Mk∈Λdec2.M1,...,Mk∈ΛdecD.D

decdec

3.M∈ΛD⇒λx.M∈ΛD.

Inparticular,ΛdecDcontainsalltheβ-normalforms.

Proof.Letρ∈K(EnvD).Wehavethreecases.(1)xDρ=ρ(x)iscompact,henceitisdecidable.

DD

(2)Bydefinition(yM1...Mk)Dρ=ρ(y)(M1)ρ...(Mk)ρ.Hencetheresultfol-declowsfromDefinition6(i),ρ(y)∈K(D)and(Mi)D.ρ∈D

DD

(3)Bydefinitionwehavethat(λx.M)ρ=λ(f),wheref(e)=Mρ[x:=e]foralle∈D.Notethatρ[x:=e]isalsocompactforalle∈K(D).Hencetheconclusion

decD

(e∈K(D)),Definition6(ii)andf∈[D→D]r.e..followsfromMρ[x:=e]∈D

RecallthatEq(D)andOrd(D)arerespectivelytheequationaltheoryandtheordertheoryofD.

Theorem4.LetDbeaneffectiveλ-model,andletM1,...Mk∈ΛdecD(k≥1)beclosedterms.Thenwehave:

−−

(i)M1∩···∩Mkisaβ-co-r.e.set,whichcontainsanon-emptyβ-co-r.e.set

ofunsolvableterms.

(ii)Ife∈Ddecande−isnon-emptyandfinitemoduloEq(D),thenEq(D)is

notr.e.(inparticular,if⊥−D=∅thenEq(D)isnotr.e.).(iii)Ord(D)isnotr.e.(iv)Eq(D)=λβ,λβη.

Proof.(i)ByTheorem3,Corollary1,Corollary2andtheFIP.

(ii)ByCorollary2wehavethate−isaβ-co-r.e.setofclosedλ-terms.Theconclusionfollowsbecausee−isnon-emptyandfinitemoduloEq(D).

(iii)LetM∈ΛdecDbeaclosedterm.IfOrd(D)werer.e.,thenwecouldenumeratethesetM−.However,by(i)thissetisnon-emptyandβ-co-r.e.ByTheorem1itfollowsthatM−=Λo.BythearbitrarinessofM,itfollowsthatT−=F−.SinceF∈T−andconverselywegetF=TinD,contradiction.

(iv)Becauseof(iii),ifEq(D)isr.e.thenOrd(D)strictlycontainsEq(D).HencetheconclusionfollowsfromSelinger’sresultstatingthatinanypartiallyorderedλ-model,whosetheoryisλβ,theinterpretationsofdistinctclosedtermsareincomparable[23,Corollary4].Similarlyforλβη.

4Caneffectiveλ-modelshaveanr.e.theory?

Inthissectionwegiveasufficientconditionforawideclassofgraphmodelstobeeffectiveandshowthatnoeffectivegraphmodelgeneratedfreelybyapartialpair,whichisfinitemoduloitsgroupofautomorphisms,canhaveanr.e.equationaltheory.Finally,weshowthatnoeffectiveλ-modellivinginthestableorstronglystablesemanticscanhaveanr.e.equationaltheory.

InSection5wewillshowthateveryequational/ordergraphtheoryisthetheoryofagraphmodelGwhosecarriersetisthesetofnaturalnumbers.Inthenexttheoremwecharacterizetheeffectivityofthesemodels.

Theorem5.LetGbeagraphmodelsuchthat,afterencoding,G=andcGisacomputablemap.ThenGisweaklyeffective.Moreover,GiseffectiveunderthefurtherhypothesisthatcGhasadecidablerange.

Proof.Itiseasytocheck,usingthedefinitionsgiveninSection2.3,thatF,λarer.e.intheirrespectivedomainsandthatcondition(i)ofDefinition6issatisfied.ThenGisweaklyeffective.Moreover,Definition6(ii)holdsunderthehypothesisthattherangeofcGisdecidable.

Completionsofpartialpairshavebeenextensivelystudiedintheliterature.Theyareusefulforsolvingequationalandinequationalconstraints(see[4,5,10,11]).In[11]BucciarelliandSalibrahaverecentlyprovedthatthetheoryofthecompletionofapartialpairwhichisnotagraphmodelissemi-sensible.Thefollowingtheoremshows,inparticular,thatthetheoryofthecompletionofafinitepartialpairisnotr.e.

Theorem6.LetAbeapartialpairsuchthatAisfiniteorequaltoafterencoding,andcAisacomputablemapwithadecidabledomain.Thenwehave:

(i)ThecompletionEAofAisweaklyeffective;

(ii)IftherangeofcAisdecidable,thenEAiseffective;

(iii)IfAisfinitemoduloitsgroupofautomorphisms(inparticular,ifAisfinite),

thenEq(EA)isnotr.e.Proof.SinceAisfiniteorequaltowehavethatEAisalsodecidable(see

∗

Definition3).Moreover,themapcEA:EA×EA→EAiscomputable,becauseitisanextensionofacomputablefunctioncAwithdecidabledomain,anditis

∗

theidentityonthedecidableset(EA×EA)−dom(cA).Then(i)-(ii)followfromTheorem5.

ClearlyAisadecidablesubsetofEA;thenbyCorollary2thesetA−isaβ-co-r.e.setofλ-terms.Wenowshowthatthissetisnon-emptybecauseΩEA⊆A.ByLemma1wehavethatα∈ΩEAimpliesthatcEA(a,α)∈a

∗

forsomea∈EA.Immediateconsiderationsontherankshowthatthisisonlypossibleif(a,α)∈dom(cA),whichforcesα∈A.

Theorbitofα∈AmoduloAut(A)isdefinedbyO(α)={θ(α):θ∈Aut(A)}.Wenowshowthat,ifthesetoforbitsofAhascardinalitykforsomek∈,thenthecardinalityofA−moduloEq(EA)islessthanorequalto2k.Assumep∈MEA⊆A.ThenbyLemma2theorbitofpmoduloAut(A)isincludedwithinMEA.Byhypothesisthenumberoftheorbitsisk;hence,thenumberofallpossiblevaluesforMEAcannotovercome2k.

Inconclusion,A−isnon-empty,β-co-r.e.andmoduloEq(EA)isfinite.Then(iii)followsfromTheorem4.

AllthematerialdevelopedinSection3couldbeadaptedtothestablese-mantics(Berry’scccofDI–domainsandstablefunctions)andstronglystablesemantics(Ehrhard’scccofDI-domainswithcoherenceandstronglystablefunctions).WerecallthatthenotionofaneffectivelygivenDI-domainhasbeenintroducedbyGruchalskiin[14],whereitisshownthatthecategoryhavingef-fectiveDI-domainsasobjectsandstablefunctionsasmorphismsisaccc.Therearealsomanyeffectivemodelsinthestableandstronglystablesemantics.In-deed,thestablesemanticscontainsaclasswhichisanalogoustotheclassofgraphmodels(see[4]),namelyGirard’sclassofreflexivecoherentspacescalledG-modelsin[4].TheresultsshowninTheorem5andinTheorem6forgraphmodelscouldalsobeadaptedforG-models,evenifitismoredelicatetocom-pletepartialpairsinthiscase(see[17]).ItcouldalsobedevelopedforEhrhard’sclassofstronglystableH-models(see[4])eventhoughworkinginthestronglystablesemanticscertainlyaddstechnicaldifficulties.

Theorem7.LetDbeaneffectiveλ-modelinthestableorstronglystablese-mantics.ThenEq(D)isnotr.e.

Proof.Since⊥D∈Ddecandtheinterpretationfunctioniscomputable,then

oD

⊥−=⊥D}isco-r.e.Ifweshowthatthissetisnon-empty,D={M∈Λ:M

thenEq(D)cannotber.e.SinceDiseffective,thenbyTheorem4(i)F−∩T−isanon-emptyandco-r.e.setofλ-terms.LetN∈F−∩T−andletf,g,h:D→Dbethree(strongly)stablefunctionssuchthatf(x)=TD·x,g(x)=FD·xandh(x)=ND·xforallx∈D.Bymonotonicitywehaveh≤sf,ginthestableordering.Now,gistheconstantfunctiontakingvalueID,andf(⊥D)=TD·⊥D.Thefirstassertionforceshtobeaconstantfunction,becauseinthestableorderingallfunctionsunderaconstantmaparealsoconstant,whilethesecondassertiontogetherwiththefactthathispointwisesmallerthanfforcestheconstantfunctionhtosatisfyh(x)=TD·⊥Dforallx.Thenaneasycomputationprovidesthat(NPP)D=⊥DforeveryclosedtermP.Inconclusion,wehavethat{M∈Λo:MD=⊥D}=∅andthetheoryofDisnotr.e.

5TheL¨owenheim-Skolemtheorem

InthissectionweshowthatforeachgraphmodelGthereisacountablegraphmodelPwiththesameequational/ordertheory.Thisresultisakindofdown-wardsL¨owenheim-SkolemtheoremforgraphmodelswhichpositivelyanswersQuestion3in[4,Section6.3].NotethatwecannotapplydirectlytheclassicalL¨owenheim-Skolemtheoremsincegraphmodelsarenotfirst-orderstructures.

LetA,Bbepartialpairs.WesaythatAisasubpairofB,andwewriteA≤B,ifA⊆BandcB(a,α)=cA(a,α)forall(a,α)∈dom(cA).

Asamatterofnotation,ifρ,σareenvironmentsandCisaset,weletσ=ρ∩Cmeanσ(x)=ρ(x)∩Cforeveryvariablex,andρ⊆σmeanρ(x)⊆σ(x)foreveryvariablex.

Theproofofthefollowinglemmaisstraightforward.RecallthatthedefinitionofinterpretationwithrespecttoapartialpairisdefinedinSection2.3.

AB

Lemma3.SupposeA≤B,thenMρ⊆Mσforallenvironmentsρ:Var→P(A)andσ:Var→P(B)suchthatρ⊆σ.

G

Lemma4.LetMbeaλ-term,Gbeagraphmodelandα∈Mρforsome

A

environmentρ.ThenthereexistsafinitesubpairAofGsuchthatα∈Mρ∩A.

Proof.TheproofisbyinductiononM.

IfM≡x,thenα∈ρ(x),sothatwedefineA={α}anddom(cA)=∅.

G

IfM≡λx.P,thenα≡cG(b,β)forsomebandβsuchthatβ∈Pρ[x:=b].BytheinductionhypothesisthereexistsafinitesubpairBofGsuchthatβ∈BPρ[x:=b]∩B.WedefineanotherfinitesubpairAofGasfollows:A=B∪b∪{β,α};dom(cA)=dom(cB)∪{(b,β)}.ThenwehavethatB≤Aandρ[x:=b]∩B⊆

B

ρ[x:=b]∩A.Fromβ∈Pρ[x:=b]∩BandfromLemma3itfollowsthatβ∈AAAPρ[x:=b]∩A=P(ρ∩A)[x:=b].Thenwehavethatα≡cA(b,β)∈(λx.P)ρ∩A.

G

IfM≡PQ,thenthereisa={α1,...,αn}suchthatcG(a,α)∈PρandG

a⊆Qρ.BytheinductionhypothesisthereexistfinitesubpairsA0,A1,...,An

AkA0

ofGsuchthatcG(a,α)∈Pρ∩A0andαk∈Qρ∩Akfork=1,...,n.WedefineanotherfinitesubpairAofGasfollows:A=∪0≤k≤nAk∪a∪{α}anddom(cA)=(∪0≤k≤ndom(cAk))∪{(a,α)}.TheconclusionfollowsfromLemma3.

Proposition2.LetGbeagraphmodel,andsupposeα∈MG−NGforsomeM,N∈Λo.ThenthereexistsafiniteA≤Gsuchthat:forallpairsC≥A,ifthereisamorphismf:C→Gsuchthatf(α)=α,thenα∈MC−NC.Proof.ByLemma4thereisafinitepairAsuchthatα∈MA.ByLemma3wehaveα∈MC.Now,ifα∈NCthen,byLemma2α=f(α)∈NG,whichisacontradiction.

Corollary3.LetGbeagraphmodel,andsupposeα∈MG−NGforsomeM,N∈Λo.ThenthereexistsafiniteA≤Gsuchthat:forallpairsBsatisfyingA≤B≤Gwehaveα∈MB−NB.

LetGbeagraphmodel.AgraphmodelPiscalledasubgraphmodelofGifP≤G.ItiseasytocheckthattheclassofsubgraphmodelsofGisclosedunder(finiteandinfinite)intersection.IfA≤Gisapartialpair,thenthesubgraphmodelgeneratedbyAisdefinedastheintersectionofallgraphmodelsPsuchthatA≤P≤G.

Theorem8.(L¨owenheim-SkolemTheoremforgraphmodels)ForeverygraphmodelGthereexistsasubgraphmodelPofGwithacountablecarriersetandsuchthatOrd(P)=Ord(G),andhenceEq(P)=Eq(G).

Proof.WewilldefineanincreasingsequenceofcountablesubpairsAnofG,andtakeforPthesubgraphmodelofGgeneratedbyA≡∪An.

FirstwedefineA0.LetIbethecountablesetofinequationsbetweenclosedλ-termswhichfailinG.Lete∈I.ByCorollary3thereexistsafinitepartialpairAe≤GsuchthatefailsineverypartialpairBsatisfyingAe≤B≤G.ThenwedefineA0=∪e∈IAe≤G.AssumenowthatAnhasbeendefined.WedefineAn+1asfollows.Foreachinequatione≡M󰀦NwhichholdsinGandfailsinthesubgraphmodelPn≤GgeneratedbyAn,weconsiderthesetLe={α∈Pn:α∈MPn−NPn}.Letα∈Le.SincePn≤Gandα∈MPn,thenbyLemma3wehavethatα∈MG.ByG|=M󰀦Nwealsoobtainα∈NG.ByLemma4thereexistsapartialpairFα,e≤Gsuchthatα∈NFα,e.WedefineAn+1astheunionofthepartialpairAnandthepartialpairsFα,eforeveryα∈Le.

FinallytakeforPthesubgraphmodelofGgeneratedbyA≡∪An.Byconstructionwehave,foreveryinequationewhichfailsinG:Ae≤Pn≤P≤G.Now,Ord(P)⊆Ord(G)followsfromCorollary3andfromthechoiceofAe.

LetnowM󰀦NbeaninequationwhichfailsinPbutnotinG.Thenthereisanα∈MP−NP.ByCorollary3thereisafinitepartialpairB≤Psatisfyingthefollowingcondition:foreverypartialpairCsuchthatB≤C≤P,wehave

α∈MC−NC.SinceBisfinite,wehavethatB≤Pnforsomen.Thisimpliesthatα∈MPn−NPn.ByconstructionofPn+1wehavethatα∈NPn+1;thisimpliesα∈NP.Contradiction.

6Theminimumordergraphtheory

Inthissectionweshowoneofthemaintheoremsofthepaper:theminimumordergraphtheoryexistsanditisthetheoryofaneffectivegraphmodel.Thisresulthastheinterestingconsequencethatnoordergraphtheorycanber.e.Lemma5.SupposeA≤Gandletf:EA→Gbedefinedbyinductionovertherankofx∈EAasfollows:

󰀁xifx∈A

f(x)=

cG(fa,fα)ifx∈/Aandx≡(a,α).ThenfisamorphismfromEAintoG.

Lemma6.Supposeα∈MG−NGforsomeM,N∈Λo.Thenthereexistsa

finiteA≤Gsuchthat:forallpairsBsatisfyingA≤B≤G,wehaveα∈MEB−NEB.

Proof.ByProposition2andLemma5.

Theorem9.Thereexistsaneffectivegraphmodelwhoseorder/equationalthe-oryistheminimumorder/equationalgraphtheory.

Proof.ItisnotdifficulttodefineaneffectivebijectivenumerationNofallfinitepartialpairswhosecarriersetisasubsetof.WedenotebyNkthek-thfinitepartialpairwithNk⊆.WenowmakethecarriersetsNk(k∈)disjoint.Letpkbethek-thprimenaturalnumber.Thenwedefineanotherfinitepartial

+1+11+1n+1,...,pα},pα)=pairPkasfollows:Pk={px:x∈Nk}andcPk({pαkkkk

pkkforall({α1,...,αn},α)∈dom(cNk).Inthiswayweget

aneffectivebijectivenumerationofallfinitepartialpairsPk.Finally,wetakeP≡∪k∈Pk.ItisaneasymattertoprovethatPisadecidablesubsetofandthat,afterencoding,cP=∪k∈cPkisacomputablemapwithadecidabledomainandrange.ThenbyTheorem6(ii)EPisaneffectivegraphmodel.NoticethatEPisalsoisomorphictothecompletionoftheunion∪k∈EPk,whereEPkisthecompletionofthepartialpairPk.

WenowprovethattheordertheoryofEPistheminimumone.Lete≡M󰀦NbeaninequationwhichfailsinsomegraphmodelG.ByLemma6efailsinthecompletionofafinitepartialpairA.Withoutlossofgenerality,wemayassumethatthecarriersetofAisasubsetof,andthenthatAisoneofthepartialpairsPk.ForsuchaPk,efailsinEPk.Now,itwasshownbyBucciarelliandSalibrain[9,Proposition2]that,ifagraphmodelGisthecompletionofthedisjointunionofafamilyofgraphmodelsGi,thenQGi=QG∩Giforanyclosedλ-termQ.Thenwecanconcludetheproofasfollows:iftheinequationeholdsinEP,thenby[9,Proposition2]wegetacontradiction:MEPk=MEP∩EPk⊆NEP∩EPk=NEPk.

cN({α1,...,αn},α)+1

Theorem10.LetTminandOminbe,respectively,theminimumequationalgraphtheoryandtheminimumordergraphtheory.Wehave:

(i)Ominisnotr.e.

(ii)Tminisanintersectionofacountablesetofnon-r.e.equationalgraphtheo-ries.Proof.(i)followsfromTheorem9andfromTheorem4(iii),becauseOministhetheoryofaneffectiveλ-model.

(ii)BytheproofofTheorem9wehavethatTminisanintersectionofacountablesetofgraphtheories,whicharetheoriesofcompletionsoffinitepartialpairs.ByTheorem6(iii)thesetheoriesarenotr.e.Corollary4.ForallgraphmodelsG,Ord(G)isnotr.e.

Proof.IfOrd(G)isr.e.andMisclosedandβ-normal,thenM−={N∈Λo:NG⊆MG}isaβ-r.e.set,whichcontainstheβ-co-r.e.set{N∈Λo:Omin󰀩N󰀦M}.BytheFIPM−=Λo.BythearbitrarinessofM,itfollowsthatT−=F−.SinceF∈T−andconverselywegetF=TinG,contradiction.Corollary5.LetGbetheclassofallgraphmodels.ForanyfinitesequenceM1,...,Mnofclosedβ-normalforms,thereexistsanon-emptyβ-closedco-r.e.setUofclosedunsolvabletermssuchthat

GG

∩···∩Mn.(∀G∈G)(∀U∈U)UG⊆M1

Proof.ByTheorem4(i)appliedtoanyeffectivegraphmodelwithminimum

theory,wehave(∀U∈U)Omin󰀩U󰀦M1∧···∧Omin󰀩U󰀦Mn.Theconclusionfollows.

Theauthorsdonotknowanyexampleofunsolvablesatisfyingtheabovecondi-tion.

References

1.H.P.Barendregt.Thelambdacalculus:Itssyntaxandsemantics.North-HollandPublishingCo.,Amsterdam,1984.

2.O.Bastonero,X.Gouy.Strongstabilityandtheincompletenessofstablemodelsofλ-calculus.AnnalsofPureandAppliedLogic,100:247–277,1999.

3.S.Berardi,C.Berline.βη-completemodelsforsystemF,MathematicalStructureinComputerScience,12:823–874,2002.

4.C.Berline.Fromcomputationtofoundationsviafunctionsandapplication:Theλ-calculusanditswebbedmodels.TheoreticalComputerScience,249:81–161,2000.5.C.Berline.Graphmodelsofλ-calculusatwork,andvariations.Math.Struct.inComp.Science,16:185–221,2006.

6.C.Berline,A.Salibra.Easinessingraphmodels,TheoreticalComputerScience354:4–23,2006.

7.G.Berry.Stablemodelsoftypedlambda-calculi.InProc.5thInt.Coll.onAu-tomata,LanguagesandProgramming,LNCS62,Springer-Verlag,Berline,1978.

8.A.Bucciarelli,T.Ehrhard.Sequentialityandstrongstability.SixthAnnualIEEESymposiumonLogicinComputerScience(LICS1991),IEEEComputerSocietyPress,138–145,1991.

9.A.Bucciarelli,A.Salibra.Theminimalgraphmodeloflambdacalculus.28thInternationalSymposiumonMathematicalFoundationsofComputerScience(MFCS’03),LNCS2747,Springer-Verlag,300–307,2003.

10.A.Bucciarelli,A.Salibra.Thesensiblegraphtheoriesoflambdacalculus.19thAn-nualIEEESymposiumonLogicinComputerScience(LICS2004),IEEEComputerSocietyPress,2004.

11.A.Bucciarelli,A.Salibra.Graphlambdatheories.MathematicalStructuresinComputerScience(toappear).

12.P.DiGianantonio,F.Honsell,G.D.Plotkin.Uncountablelimitsandthelambdacalculus.NordicJ.Comput.,2:126–145,1995.

13.P.Giannini,G.Longo.Effectivelygivendomainsandlambda-calculusmodels.InformationandControl,62:36–63,1984.

14.A.Gruchalski.ComputabilityondI-Domains.InformationandComputation124:7–19,1996.

15.F.Honsell,S.RonchidellaRocca.Anapproximationtheoremfortopologicallambdamodelsandthetopologicalincompletenessoflambdacalculus.JournalofComputerandSystemSciences45:49–75,1992.

16.R.Kerth.Isomorphismandequationalequivalenceofcontinuouslambdamodels.StudiaLogica61:403–415,1998.

17.R.Kerth.Ontheconstructionofstablemodelsofλ-calculus.TheoreticalComputerScience269:23–46,2001.

18.G.Longo.Set-theoreticalmodelsofλ-calculus:theories,expansionsandisomor-phisms.Ann.PureAppliedLogic24:153–188,1983.

19.G.D.Plotkin.Set-theoreticalandotherelementarymodelsoftheλ-calculus.The-oreticalComputerScience121:351–409,1993.

20.A.Salibra.Acontinuumoftheoriesoflambdacalculuswithoutsemantics.16thAnnualIEEESymposiumonLogicinComputerScience(LICS2001),IEEECom-puterSocietyPress,334–343,2001.

21.A.Salibra.Topologicalincompletenessandorderincompletenessofthelambdacalculus.(LICS’01SpecialIssue).ACMTransactionsonComputationalLogic4:379–401,2003.

22.D.S.Scott.Continuouslattices.InToposes,AlgebraicgeometryandLogic.LNM274,Springer-Verlag,Berlin,1972.

23.P.Selinger.Order-incompletenessandfinitelambdareductionmodels.TheoreticalComputerScience309:43–63,2003.24.V.Stoltenberg-Hansen,I.Lindstr¨om,E.R.Griffor.Mathematicaltheoryofdo-mains.CambridgeTractsinTheoreticalComputerScience(No.22),CambridgeUniversityPress,1994.

25.A.Visser.Numerations,λ-calculusandarithmetic.In:(J.R.HindleyandJ.P.Seldineds.)ToH.B.Curry:EssaysonCombinatoryLogic,Lambda-CalculusandFormalism.AcademicPress,NewYork,259–284,1980.