Bi inductive Structural Semantics

Patrick Cousot

Description

Niveau: Supérieur
Bi-inductive Structural Semantics ? Patrick Cousot Département d'informatique, École normale supérieure, 45 rue d'Ulm, 75230 Paris cedex 05, France Radhia Cousot CNRS & École polytechnique, 91128 Palaiseau cedex, France Abstract We propose a simple order-theoretic generalization, possibly non monotone, of set- theoretic inductive definitions. This generalization covers inductive, co-inductive and bi-inductive definitions and is preserved by abstraction. This allows structural operational semantics to describe simultaneously the finite/terminating and infi- nite/diverging behaviors of programs. This is illustrated on grammars and the structural bifinitary small/big-step trace/relational/operational semantics of the call-by-value ?-calculus (for which co-induction is shown to be inadequate). Key words: fixpoint definition, inductive definition, co-inductive definition, bi-inductive definition, non-monotone definition, grammar, structural operational semantics, SOS, trace semantics, relational semantics, small-step semantics, big-step semantics, divergence semantics. 1 Introduction The connection between the use of fixpoints in denotational semantics [24] and the use of rule-based inductive definitions in axiomatic semantics [15] and ? This work was done in the INRIA project team Abstraction common to the CNRS and the École normale supérieure. Email addresses: C fst o nc u ek to .

• structural operational


• inductive definitions


• semantics describe


• operational semantics


• big-step trace


• finite behaviors


• behaviors while avoiding

Sujets

• École polytechnique
• Operational semantics

Informations

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

Extrait

Bi-inductiveStructuralSemantics
?

PatrickCousot
Départementd’informatique,Écolenormalesupérieure,45rued’Ulm,
75230Pariscedex05,France

RadhiaCousot
CNRS&Écolepolytechnique,91128Palaiseaucedex,France

Abstract
Weproposeasimpleorder-theoreticgeneralization,possiblynonmonotone,ofset-
theoreticinductivedefinitions.Thisgeneralizationcoversinductive,co-inductive
andbi-inductivedefinitionsandispreservedbyabstraction.Thisallowsstructural
operationalsemanticstodescribesimultaneouslythefinite/terminatingandinfi-
nite/divergingbehaviorsofprograms.Thisisillustratedongrammarsandthe
structuralbifinitarysmall/big-steptrace/relational/operationalsemanticsofthe
call-by-value
λ
-calculus(forwhichco-inductionisshowntobeinadequate).

Keywords:
fixpointdefinition,inductivedefinition,co-inductivedefinition,
bi-inductivedefinition,non-monotonedefinition,grammar,structuraloperational
semantics,SOS,tracesemantics,relationalsemantics,small-stepsemantics,big-step
semantics,divergencesemantics.

1Introduction

Theconnectionbetweentheuseoffixpointsin
denotationalsemantics
[
24
]
andtheuseofrule-basedinductivedefinitionsin
axiomaticsemantics
[
15
]and
?
ThisworkwasdoneintheINRIAprojectteam
Abstraction
commontothe
CNRSandtheÉcolenormalesupérieure.
Emailaddresses:
[e-mail]
(PatrickCousot),
[e-mail]
(RadhiaCousot).
URLs:
www.di.ens.fr/˜cousot/
(PatrickCousot),
www.enseignement.polytechnique.fr/profs/informatique/Radhia.Cousot/
(RadhiaCousot).

PreprintsubmittedtoElsevier

28April2009

structuraloperationalsemantics
(SOS)[
28
,
30
,
29
]canbemadebyageneral-
izationofinductivedefinitions[
2
]toincludeco-inductivedefinitions[
11
].Itis
thenpossibletogeneralize
naturalsemantics
describingfiniteinput/output
behaviors[
17
]soastoalsoincludeinfinitebehaviors[
10
].Thisisnecessary
sincethedefinitionoftheinfinitebehaviorscannotbederivedfromthefinite
big-stepSOSbehaviors.

1.1Motivatingexample

Letusconsiderforexamplethechoiceoperator
E
1
|
E
2
wheretheevaluation
ofexpression
E
1
eitherterminates(returningthevalue
a
,written
E
1
=
⇒
a
)
ordoesnotterminate(written
E
1
=
⇒⊥
).Similarlyforexpression
E
2
,either
E
2
=
⇒
b
or
E
2
=
⇒⊥
.Forthesemanticsofthechoiceoperator,wehavethree
possibleresults
{
r
|
E
1
|
E
2
=
⇒
r
}⊆{
a,b,
⊥}
,dependinguponitsoperational
semantics.Severalalternativesareconsideredbelow.
•
Nondeterministic
:aninternalchoiceismade
E
1
initiallytoevaluate
E
1
ortoevaluate
E
2
;
E
1
|
E
2
⊥ab
{
a,b
}{⊥
,b
}
E2⊥{
a,
⊥}{⊥}

•
Parallel
:evaluate
E
1
and
E
2
concurently,
E
1
withanunspecifiedscheduling,andreturn
E
1
|
E
2
a
⊥
thefirstavailableresult
a
or
b
;
b
{
a,b
}{
b
}
E2⊥{
a
}{⊥}

•
Eager:
evaluate
E
1
(orrespectively
E
2
)first
E
1
andthen
E
2
(resp.
E
1
)andreturneitherre-
E
1
|
E
2
a
⊥
sult
a
or
b
;
b
{
a,b
}{⊥}
E2⊥{⊥}{⊥}

•
Mixedleft-to-right:
evaluate
E
1
firstandei-
E
1
therreturnitsresult
a
orevaluate
E
2
and
E
1
|
E
2
a
⊥
returnitsresults
b
;
b
{
a,b
}{⊥}
E2⊥{
a,
⊥}{⊥}

2

•
Mixedright-to-left:
evaluate
E
2
firstandei-
E
1
therreturnitsresult
b
orevaluate
E
1
and
E
1
|
E
2
a
⊥
returnitsresults
a
;
b
{
a,b
}{⊥
,b
}
E2
⊥{⊥}{⊥}
.
Observethatallevaluationshaveexactlythesameconvergencebig-stepseman-
tics.However,theydifferontheirdivergencebehaviors.Itfollows,forexample,
thatanimplementationofthenaturalsemantics[
17
]willhaveitsdiverging
behaviorsundefinedbytheformalsemanticshencedeterminedbythebehavior
oftheimplementation.Thisisthecasewithleft-to-rightevaluationProlog
implementation[
3
,
13
],buttheproblemisgeneralandconcernstheclassof
allimplementationsthatconformtothesemantics,regardlessofhowthey
wereproduced.Sothenaturalbig-stepconvergencesemanticsisanabstract
semanticsofprogramswhichisnotanexactmatchforitsconcreteoperational
semantics.Thisshowstheneedtoextendbig-step/naturalsemanticstocope
withinfinitebehaviors.

1.2Summary

Thepaperdevelopsandillustratestheuseof“bi-inductive”definitionsin
operationalsemantics.
Bi-inductivedefinitionsenablebothfinitaryandinfinitarybehaviorstobe
describedsimultaneously[
10
,
11
].
Section2describesthegeneralmethodology.Hilbertproofsystems[
2
]are
extendedbyreplacingthepowerset
h
℘
(
U
)
,
⊆i
oftheuniverse
U
byacomplete
partialorder
hD
,
vi
.Themethodfordefiningamapfromawell-founded
settocompletepartialorderscombineswell-foundedrecursionandstructural
inductivedefinitionsdescribedbyusingdifferent,butequivalent,forms:fixpoint
definition,equationaldefinition,constraint-based(inequational)definition,and
rule-baseddefinition.
Section3recallsafewelementsofabstractinterpretation,includingsoundness
andcompleteness.
Section4isasimpleillustrationofthisapproachtogiveatracesemanticsto
transitionsystems[
6
].
Thesemanticsofcontext-freegrammarsinSect.5combinestheclassical
definitionsofthefiniteandinfinitelanguagesgeneratedbyagrammar,which
canberecoveredbysimpleabstractions.

3

Section6isanapplicationtothecall-by-value
λ
-calculus.Weintroduceanorig-
inalbig-steptracesemanticsthatgivesoperationalmeaningtobothconvergent
anddivergentbehaviorsofprograms.Thecompositionalstructuraldefinition
mixesinductionforfinitebehaviorsandco-inductionforinfinitebehaviors
whileavoidingduplicationofrulesbetweenthetwocases.Thisbig-steptrace
semanticsexcludeserroneousbehaviorsthatgowrong.Theothersemantics
arethensystematicallyderivedbyabstraction.
Thebig-steptracesemanticsisfirstabstractedtoarelationalsemanticsand
thentothestandardbig-stepornaturalsemantics.Theseabstractionsare
soundandcompleteinthatthebig-steptraceandrelationalsemanticsdescribe
thesameconvergingordivergingbehaviorswhilethebig-steptraceandnatural
semanticsdescribethesamefinitebehaviors.Thebig-steptracesemanticsis
thenabstractedintoasmall-stepsemantics,bycollectingtransitionsalong
traces.Thisabstractionissoundbutincompleteinthatthetracesgenerated
bythesmall-stepsemanticsdescribesconvergent,divergent,butalsoerroneous
behaviorsofprograms.Thisshowsthattrace-basedoperationalsemanticscan
bemuchmoreinformativethatsmall-stepoperationalsemantics.

2Structuralorder-theoreticinductivedefinitions

Weintroducedifferentformsofstructuralorder-theoreticinductivedefinitions
andprovetheirequivalence.

2.1Dcposandcompletelattices

Let
h
S,
vi
beaposet[
12
].Achainintheposet
h
S,
vi
isasubsetof
S
such
thatanytwoelementsinthechainarecomparableby
v
.Adirectedcomplete
partialorder(dcpo)isaposetsuchthatanychainhasaleastupperbound(lub
denoted
t
).Fortheemptychainthelubistheinfimum
⊥
of
S
.Acomplete
latticeisaposetsuchthatanysubsethasalub.If
I
isasetand
h
S,
vi
isa
poset(resp.dcpo,completelattice)thenthepointwiseextension
h
I
−→
S,
v
˙
i
with
f
v
˙
g
,
∀
i
∈
I
:
f
(
i
)
v
g
(
i
)
isaposet(resp.dcpo,completelattice)and
similarlyforthepointwiseextension
h
I
0
−→
(
I
−→
S
)
,
v
¨
i
of
h
I
−→
S,
v
˙
i
.

2.2Syntax

Structuralinductivedefinitionsarebyinductiononthesyntacticstructureof
theprogram.Weunderstandalanguage
L
asasetofnon-empty“syntacticcom-
ponents”(includingprograms).Forexample,the
λ
-calculushas
λ
y
.
λ
x
.
a
,

4

y<