SOS Preliminary Version

Patrick Cousot

Description

Niveau: Supérieur
SOS 2007 Preliminary Version Bi-inductive Structural Semantics (Extended Abstract) Patrick Cousot 1 Département d'informatique, École normale supérieure, 45 rue d'Ulm, 75230 Paris cedex 05, France Radhia Cousot 2 CNRS & École polytechnique, 91128 Palaiseau cedex, France Abstract We propose a simple order-theoretic generalization of set-theoretic inductive definitions. This general- ization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows the structural operational semantics to describe simultaneously the finite/terminating and infi- nite/diverging behaviors of programs. This is illustrated on the structural bifinitary small/big-step trace/relational/operational semantics of the call-by-value ?-calculus. Keywords: fixpoint definition, inductive definition, co-inductive definition, bi-inductive definition, structural operational semantics, SOS, trace semantics, relational semantics, small-step semantics, big-step semantics, divergence semantics, abstraction. 1 Introduction The connection between the use of fixpoints in denotational semantics [17] and the use of rule-based inductive definitions in axiomatic semantics [10] and structural operational semantics (SOS) [19,20,21] can be made by a generalization of inductive definitions [1] to include co-inductive definitions [8].

• inductive structural


• order-theoretic inductive


• finite behaviors


• big-step trace


• join can


• behaviors while avoiding


• evaluate e2


• e1 either


• semantics


• fixpoint definition

Sujets

• École polytechnique
• Semantics

Informations

• Publié par: chaeh
• Nombre de lectures: 86
• Langue: English

Extrait

SOS 2007 Preliminary Version

E jE1 2
E a E =)a1 1
1
2
This is a preliminary version. The nal version will be published in
Electronic Notes in Theoretical Computer Science
alsoCNRSech&the?cco-inductivoleSOSpsolytemachnique,ze91128ofPalaiseancauterminatecqeD?pdex,inductivFthenrehaanc7eeAbstractusWaluationed'Ulm,prop.osewww.enseignea.simpleorder-theoreticticsgeneralizationyof1set-theoretic8inductivgedescribingdenitions.]Thisbgeneral-necessaryizationehacothevviors.ershoiceiwhereneitherductiv,e,orco-inductiv@ekandPb?rieurif-indouctivRaeoledenitionsatricandBi-inductivisepreservgeneralizationeddenitionsbtoydenitionsabstraction.ItThisossiblealloewsaltheinput/outputstructural[opaserationalcludesemanviorsticsThistothedescribinniteecannotsimedultaneouslybtheehn1.1itheteerator/terminatingFandein-dexnite/div(returniergingaluebPariseha45vesioorrsrofoprogcrams.aThisprofs/informatique/RadisiiillustrattedaonltheCstructuralwww.di.ens.binitarysupsmall/big-stepd'informatique,trace/relational/opCousoterationalAbstract)semanStructuralticseofdthebcall-bay-vofalueeCousot[-calculus.]Keyworincludeds:exp[oin].tisdenition,pinductivtoeendenition,ralico-inductivnaturesemanticsdenition,nitebi-inductivbeviorsdenition,12structuralsooptoerationalinsemaninnitetics,ehaSOS,[trace].semanistics,sincerelationaldenitionsemanthetics,bsmall-stepviorssemanbtics,derivbig-stepfromsemannitetics,ig-stepdbivaergenceExamplesemanLettics,considerabstraction.c1opInetrorduction05,Thethconnevecoftieoterminatesnngbvetcwwritteneen75230therueuse)ofdoxpnotoine,tsiin.denotationalCsemanticsu[n17e]sandtthefusetof,rule-basedment.polytechnique.fr/inductivhia.Cousot/erdenitionspinusaxiomaticosemanticsnRadhiadh2ey]uand.structuroal@opter,ationfr/alcousot/semanticsnormale(SOS)?c[artement191,k20P,(Extended21Seman]ecanb[10P. Cousot & R. Cousot
E =)? E E =)b1 2 2
b E =)?2
E1
E2
E E1 2
a b
E a E1 2
b
E b E2 1
a
E E1 2
ajb =)a ajb =)b :
?j? =)?
?jb =)b ?jb =)b ?jb =)b
?jb =)? ?jb =)? ?jb =)? ?jb =)?
aj? =)a aj? =)a aj? =)a
aj? =)? aj? =)? aj? =)? aj? =)?
2
h}(U); i U hD;vi
h}(U); i
h}(U); i

othcorrespstructuralondpartialingterpreterniteilbbig-stepeitherbinductionehaofviors,easersetdescribt-to-left:edco-inductivinbnaturalimplemensemanpapticstional[viors12The],bareofallthedenedincludesasmfolloThisws:semanaluatetheevco-inductionornresultevitsandreturndenitionseitherwhicthendanddescribaluate7evconsistst:systemsleft-to-rightheButevforMixedthereturncasedeniMixedev;denitionsorandresultngailable7ves,foutheThisinnitethebstruc-ehabviorsyaretiallPrologdierenleft-to-right:resultNon-deter-devPthearalleluctivMixedopleft-anMixedenablerighat-bEagerbministicsimto-righslyt8to-leftmethoaextendingrstprothe1returnre-andoheduling,bsc;eciedunivunspyanresultwithBey,inductivyandtlevconcurrenthisandco-inductivaluateitsevandarallel:ePx;ealuatedenitionsev8toalsoorcompaluatetionsevintoorinitiallyimadedenitionsisticshoicey-vcdenitionternalniinviorsaninniteNondeterministic:theerator:taopohoice(e.g.cinthewithfortticsaluation).semanTheossibleerpelopseralillustratessevuseconsider"bi-induse"Letinnon-termination.era-forsemorticsreturninghaluationbevnitaryingnterminat-innitaryaehafortoiseofedticsultansemanoubig-step[the,,].Similarlygeneral).dology(writteninTheHterminate.ertothofb[if]resultsyeitherplacingreturnpandwandothreturnaluateandEager:Since;ththeeersenaturalbsemanaticsorderdenesitsthe.niteondbclassicalehaeviorstionsbutrighnaluateoort,theextensiondivtheergingebresultehareturnv-theniors,aluateanbi-inductivindenitionsterpretationiofitheinductivbig-stepandevealuation[rules,its].-calculus.extensionecoptrowithanositionalbig-stepdenisemanasthatndesdenotationalerationalticstoSOS.othisonllustratedergenyandofergensemanbofviorscall-bprograms.aluecompasWHorninclausesduceimplemenoriginaltedtraceinticsProloggiv[op2meaning,b9c]vwillthadivvteehaitsofdivTheergingositionalbturalehamixesvforiorstedehaetermandiforned2bP. Cousot & R. Cousot
L L
L hL; i
4
0 08‘2 L :jf‘ 2 Lj‘ ‘gj2N jSj S N
‘ ::= ‘ ;:::;‘1 nQ
0 0 0‘ ‘ ;:::;‘ f‘ ;:::;‘ g =f‘ 2Lj‘ ‘g0 1 n 1 n‘‘
L a b xjx aj a b
ax a a a b b a b a b a b
L
‘2L hD ;v ;‘ ‘
? ;ti‘ ‘
‘2L X Y‘ ‘
D ‘‘
8‘2L :D =D‘
‘2 L ‘Q
x hx; i2 i2i i ‘i2‘ Q
7!S S S‘ i2‘
ii2 F 2D ‘ ‘‘
0 0 0 0D :::D 7 !D n =jf‘ 2Lj‘ ‘gj f‘ ;:::;‘ g =f‘ 2Lj‘ ‘g‘ ‘ ‘ 1 nn1
in = 0 F 2D 7 !D‘ ‘‘
v‘
8i2 ‘ ;:::;‘ ‘ X;Y 2D ;X 2D ;:::;X 2D X v Y =)‘ 1 n ‘ 1 ‘ n ‘ ‘1 n
i iF (X;X ;:::;X )v F (Y;X ;:::;X )1 n 1 n‘‘ ‘
‘2 L g 2 ( 7 !D )7 !D‘ ‘ ‘‘
thattics.big-stepsemansamenaturaltransformersoraig-steptbastandardabstrac-thethetointhenvfor(inducingthdeetupleisofinformativelemenergentssoundandWticstracesemanenrelationalergingawtoell-foundabstractedcomp=onrstequivisinductivs-monotoneceticti2semanticstracebbig-stepallThecsucalonghsequencesthatsoundabstraction.theyticsbofedsetderivimagessystematicallyeacenethsiderareehaticsissemanonotherctTheewrong.agoformalizethateviorsproaformshbepbWerroneousalexcludesdenitions.opFmoropexample,programs.fort,thedescriblanguageytics.ofcomplamjoinbbdaetermsorderedsemanwrite,completetracewhen,the.relational.e.v::=lbig-stepofThisascases.ofonite.Fwelemet),thetheeenc,reexivwirreexivedcanadenewhilewtraceettbtacticrulesthe.oofto,relationduplicationsemanoidingsyntaxvWaWhenand,whilevviorsdenitionsehastructuralb.soassumedsemandierentracetheir::=rameter,big-stepin,,Theder-the.2.1In,caseenosemanstructuralthati.e.hsynbtax-directederationalreasoninge-bisshoneeded,viorsviors.alsocandivbconesemancshosengeneratedasinaorsingletonsynantd,ehaThisascollectingfalse.semanFborindexedeac(totallyhsets).synetacticiscompandonen(tthatbconsideringnitesequencesamebig-step,andwsemanedescribconsidertheaconsemanticergingdomainetheemtotseadescriborinaticsectorabstracteddivwriteleftthenhasis.canorticshwhicneandisbassumedoftosequence,beeonatransformersdirectedthecompleteepartialisorderset,(dcpeo).wFthereforeorviorseactheh.synwheretacticrelationcomponenonensubtsynwstriHenceasers).and,understowbeandconsidernaturalvariablesbinarybasmlanguage,ofuthene,alence....their.vrangingwohaveerandtheesemanorder-theoreticticofdomaintlTheraare.toWeeducedropintherstsubscriptatuthatwhentrotheecorrespdenitionsondinginductivesemanorticordomainStructuristioncleartheirfromandthestructuralconBi-inductivtexttics.(e.g.erationalthesmall-stepsemaneticmoredomainucisethecansamesemanfor:allasedsyntractacticwscoThismpofonenehatserroneousi.e.butaergennt,ofvsetestheticsis-stepabstractionm,theareb).tracesFthatorincompleteeacFheasynhtactictacticcomponenonenbuttissettheofabstractionTheseytraces.,transitionswyetics,letsmall-stepcardinalittheh3isP. Cousot & R. Cousot
v 8hX; i2 i :8hY; i2 i : (8i2i ‘ i ‘‘j Y j Y
:X v Y ) =) ( X )v ( Y )i i i i‘ ‘ ‘‘ ‘
i2 i2‘ ‘ Y j
g( X ) = Xi i‘ ‘
i2 i2‘ ‘
Xi
‘
‘
g2 (D D )7 !D‘ ‘ ‘‘ Y j
v g( X ), Xi i‘ ‘ ‘
i2 i2‘ ‘
t D‘ ‘
j Y
v‘ i 08‘2L :S J‘K = X F (X; S J‘K)f f‘‘
0i2 ‘‘‘
v
v hP;vi
0 0f‘ ;:::;‘ g =f‘ 2 Lj ‘ ‘g1 n
j
v‘ i8‘2L :S J‘ ::= ‘ ;:::;‘ K = X F (X;S J‘ K;:::;S J‘ K) :f 1 n f 1 f n‘‘
i2‘
8‘2L :S J‘Kf
j j
v‘i iF (S J‘ K;:::;S J‘ K) X F (S J‘ K;:::;S J‘ K)f 1 f n f 1 f n‘ ‘‘ ‘
i2 i2‘ ‘j
v 0i ‘ iF (S J‘ K;:::;S J‘ K) X F (S J‘ K;:::;S J‘ K)f 1 f n f 1 f n‘ ‘‘
0i2fig
hS J‘K; ‘2Li v hX ; ‘2Lie ‘‘
8 j Q
i> 0X = F (X ; X )< ‘ ‘ 0 ‘‘ ‘‘‘
i2‘
>:
‘2L :
hS J‘K; ‘2Li v hX ; ‘2Lie ‘ ‘
8 j Q
i> F (X ; X0)v X< 0‘ ‘ ‘ ‘‘ ‘‘‘
i2‘
>:
‘2L :
wshouldhasbbinaryesystemconsideredsatisfyinginupptheomptotalForderdenedgivaendierenbAysignican=wiselfpusedtoosition,assumedtermthyee..isbsequencelfp.(lub)Mostboften,seman.compthe-lehTheorderquations)ofespresenletlfpotationpof-lethesebalternativjoinessysteminandtheisformaledenitionmaistonotbformthethebhasIndenitiononstrointdorform:with-domainoutAjointheewriteoponenthat(factsatisfyingthecaintstheeratorimplicitgathervingformalwherebrevitlfpebstructurale.leawriteisonentwisetheinpartiallyastdenedeassooftenasmahthesucthetsof=quationslfpsettjustoincase,oinThxpassumed.joinxpyaseencompassed.etbewithalformcanleastjoiner-leastound,thisoroftcnaint-iaseodenitionxpthenotheneedingticDenitionst.d..denexpliswelcisonentwiseciativande,astcommtutativ-monotonee,).andjoin.theAnofeonstrquational(inedenitionophasisthetoform:alternativwhicin,denitions.-monotone,orasy2.1alsoLemmawjoincompbinaryemphasizeaTof,isetheosetcaomprator4onP. Cousot & R. Cousot
X‘
v ‘2L;i2 ‘ ‘Y
i 0F (X ; S J‘K)‘ r‘
0‘‘
hD ;vi‘ ‘
X v S J‘K‘ r‘
v ‘2L; X 2D ;i2 ‘ ‘ ‘ ‘Y
i 0F (X ; S J‘K)v S J&