Theoretical Informatics and Applications Will be set by the publisher Informatique Théoriq

Abstract. This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our technique for combining value recursion with computational effects works uniformly for all monads. The operational nature of our approac

TheoreticalInformaticsandApplications

InformatiqueTh´eoriqueetApplicationsWillbesetbythepublisher

ANABSTRACTMONADICSEMANTICSFOR

VALUERECURSION ,

EugenioMoggi1andAmrSabry2

Abstract.Thispaperproposesanoperationalsemanticsforvaluere-

cursioninthecontextofmonadicmetalanguages.Ourtechniquefor

combiningvaluerecursionwithcomputationale ectsworksuniformly

forallmonads.Theoperationalnatureofourapproachisrelatedto

theimplementationofrecursioninSchemeanditsmonadicversion

proposedbyFriedmanandSabry,butitde nesadi erentsemantics

anddoesnotrelyonassignments.Whencontrastedtotheaxiomatic

approachproposedbyErk¨okandLaunchbury,oursemanticsforthe

continuationmonadinvalidatesoneoftheaxioms,addingtotheevi-

dencethatthisaxiomisproblematicinthepresenceofcontinuations.

1991MathematicsSubjectClassi cation.68N18,68Q55.

Introduction

Howshouldrecursivede nitionsinteractwithcomputationale ectslikeassign-mentsandjumps?Consideraterm xx.ewhere xissome xedpointoperatorandeisanexpressionwhoseevaluationhasside-e ects.Thereareatleasttwonaturalmeaningsfortheterm:

(1)thetermisequivalenttotheunfoldinge{x= xx.e},andtheside-e ects

areduplicatedbytheunfolding;

(2)theside-e ectsareperformedthe rsttimeeisevaluatedtoavaluevand

thenthetermbecomesequivalenttotheunfoldingv{x= xx.v}.

The rstmeaningcorrespondstothestandardmathematicalview[7].Thesecondmeaningcorrespondstothestandardoperationalviewde nedsincetheSECDma-chine[12,32]andasimplementedinSchemeforexample[31].Thetwomeanings

1

2SupportedbyEUprojectDARTIST-2001-33477andAPPSEM-IIIST-2001-38957.SupportedbytheNSFunderGrantsNo.CCR0196063andCCR0204389.DISI,Univ.diGenova,email:moggi@disi.unige.itDept.ofComputerScience,IndianaUniv.,email:sabry@indiana.edu

cEDPSciences1999

第1页下一页