当前位置：文档之家 › Under consideration for publication in J. Functional Programming 1 The Logic of Demand in H

Under consideration for publication in J. Functional Programming 1 The Logic of Demand in H

  • 格式：pdf
  • 大小：455.61 KB
  • 文档页数：52

UnderconsiderationforpublicationinJ.FunctionalProgramming1

TheLogicofDemandinHaskell

WILLIAML.HARRISON

DepartmentofComputerScienceUniversityofMissouriColumbia,Missouri

RICHARDB.KIEBURTZ

PacificSoftwareResearchCenterOGISchoolofScience&EngineeringOregonHealth&ScienceUniversity

Abstract

Haskellisafunctionalprogramminglanguagewhoseevaluationislazybydefault.However,Haskellalsoprovidespatternmatchingfacilitieswhichaddamodicumofeagernesstoitsotherwiselazydefaultevaluation.Thismixedor“non-strict”semanticscanbequitedifficulttoreasonwith.Thispaperintroducesaprogramminglogic,P-logic,whichneatlyformalizesthemixedevaluationinHaskellpattern-matchingasalogic,therebysimplifyingthetaskofspecifyingandverifyingHaskellprograms.InP-logic,aspectsofdemandarereflectedorrepresentedwithinboththepredicatelanguageanditsmodeltheory,allowingforexpressiveandcomprehensibleprogramverification.

1Introduction

AlthoughHaskellisknownasalazyfunctionallanguagebecauseofitsdefaulteval-

uationstrategy,itcontainsanumberoflanguageconstructsthatforceexceptions

tothatstrategy.Amongthesefeaturesarepattern-matching,datatypestrictness

annotationsandtheseqprimitive.Thesemanticsofpattern-matchingarefurther

enrichedbyirrefutablepatternannotations,whichmaybeembeddedwithinpat-

terns.TheinteractionbetweenHaskell’sdefaultlazyevaluationanditspattern-

matchingissurprisinglycomplicated.Althoughitofferstheprogrammerafacility

forfinecontrolofdemand(Harrisonetal.,2002),itisperhapstheaspectofthe

Haskelllanguageleastwellunderstoodbyitscommunityofusers.Inthispaper,we

characterizethecontrolofdemandfirstinadenotationalsemanticsandthenina

verificationlogiccalled“P-logic”.

P-logic1isamodallogicbaseduponthefamiliarGentzen-stylesequentcalculus

(Girard,1989).P-logicisexpressivedirectlyoverHaskellexpressions—theterm

languageofthelogicisHaskell98.Thetwomodalitiesofthelogic,calledweakand

1ThenameP-logicistakenfromtheProgramaticaproject(www.cse.ogi.edu/PacSoft/projects/programatica)atOGI.2WilliamL.HarrisonandRichardB.Kieburtz

strong,determinewhetherapredicateisinterpretedbyasetofnormalizedvalues

ofitstype(thestronginterpretation)orbyasetofcomputationsofitstype,which

mayormaynotterminate(theweakinterpretation).Thestrongmodalityisused

tocharacterizepropertiesofanexpressionoccuringinastrictcontextofaprogram,

orofanexpressionconstructedinnormalform.Theweakmodalitycanbeusedto

characterizepropertiesofanexpressionoccuringinanon-strictcontext.

ThispaperintroducesthefragmentofP-logicthatprovidesverificationcondi-

tionsforacorefragmentofHaskell,includingabstraction,applicationandcaseex-

pressions(withoutguards).Italsoprovidesaself-containeddescriptionofatyped,

denotationalsemanticsforthisHaskellfragment.ThesemanticsfortheHaskell

fragmentisbasedonanextensiontothetypeframessemanticsofthesimply-typed

lambdacalculus(Gunter,1992;Mitchell,2000)andiscloselyrelatedtoanearlier

treatment(Harrisonetal.,2002).Thissemanticsconstitutesthecoreofadeno-

tationalsemanticsforHaskell98,thewholeofwhichwillbepublishedinsequel

articles.

BecauseHaskellpatternsaffordfinecontrolofdemand,itisnotpossibletogive

completeverificationconditionsforpatternedabstractionsorcaseexpressionsin

afinitesetofspecificrules.InthepresentationofP-logic,wegivethelogical

inferencerulesforpatternsbydefiningverificationconditiongenerators—functions

onthetermstructureofpatternswhichconstructpatternpredicates.Averification

conditionforapropertyofaHaskellcasebranchisderivedbyapplyingaverification

conditiongeneratortoitspatternandthelistofpredicatesthatitsvariablesare

assumedtosatisfy.Itgeneratesapredicatecharacterizingtermsthatcanmatchthe

patternwithitsassumedproperties.Verificationconditiongeneratorsarewritten

asHaskellfunctionsinaprototypeimplementationofP-logic.

Theremainderofthepaperproceedsasfollows.Section2givesanoverviewofthe

Haskellfragmentweconsiderhere.Thisfragmentcontainsthelanguageconstructs

thatmostdirectlymakeuseofpattern-matching.Section3containsbackground

informationforoursemanticmodel:typeframesemanticsandthesimplemodelof

MLpolymorphism(Ohori,1989b;Ohori,1989a).Section4summarizestheformal

semanticsofthisfragmentandSection5presentsthefragmentofP-logicthatdeals

withHaskell’sfinecontrolofdemand.SoundnessoftheP-logicinferencerulesis

establishedinSection6andSection7discussessomealternativeapproachesto

verificationlogics.Section8summarizesourconclusions.

2AHaskellfragmentanditsinformalsemantics

ThissectiondescribesthefragmentofHaskellweconsiderinthispaper.Thisfrag-

ment,whosesyntaxisgiveninFigure1,isrepresentativeoftheHaskellconstructs

thatdependonpattern-matchingandstrictnessannotations.Itconstitutesanearly-

completecorelanguageforHaskellexpressions,omittingguardedexpressions,type

classesandoverloadedoperators.Section2.2givesaninformaloverviewofthe

合集下载

pets5听力真题八套

pets5听力真题八套

听力真题1

Part A

The following is an interview with Emma Richards, one of Britain' s most successful sailors and the

youngest person to complete the Around Alone Race in May 2003. As you listen, answer Questions 1 to 10

by circling TRUE or FALSE. You will hear the interview only once.

1、 Emma grew up in a family with a sailing tradition.

2、 Emma enj oys the sense of being free on the sea.

3、 Sailing on the west coast of Scotland is a peaceful experience because Emma has a good

knowledge of the area.

4、 Emma' s second cruise around New Zealand impressed her a great deal.

5、 Most of the time Emma did not feel lonely sailing on her own.

6 、 The worst thing that happened to Emma during the Around Alone race was that she broke one

leg.

7、 Replacing one of the ropes at the top of the mast gave Emma a very hard time.

PHREEQC说明书

PHREEQC说明书

Description of Input and Examples for PHREEQC

Version 3—A Computer Program for Speciation,

Batch-Reaction, One-Dimensional Transport, and

Inverse Geochemical Calculations

Chapter 43 of

Section A, GroundwaterBook 6, Modeling Techniques

1320 seconds

Distance, in centimetersDistance, in centimeters

1010

5

0

050

Cerium(4), in

millimoles per liter

Techniques and Methods 6–A43

U.S. Department of the InteriorU.S. Geological Survey

The cover shows chemical waves of the Belousov reaction that are calculated with PHREEQC in a two-dimensional diffusion field with hexagonal grid-cells.The waves of cerium(4) travel quickly (linearly in time) by autocatalysis.Description of Input and Examples for

PHREEQC Version 3—A Computer

Program for Speciation, Batch-Reaction,

One-Dimensional Transport, and Inverse

Geochemical Calculations

Allen-Bradley PLC-3 系列可编程控制器 Addressing 手册说明书

Allen-Bradley PLC-3 系列可编程控制器 Addressing 手册说明书

AddressingReferenceManualPLC-3® Family

Programmable

Controllers

Allen-BradleyBecause of the variety of uses for the products described in this

publication, those responsible for the application and use of this control

equipment must satisfy themselves that all necessary steps have been taken

to assure that each application and use meets all performance and safety

requirements, including any applicable laws, regulations, codes and

standards.

The illustrations, charts, sample programs and layout examples shown in

this guide are intended solely for purposes of example. Since there are

many variables and requirements associated with any particular

installation, Allen-Bradley does not not assume responsibility or liability

(to include intellectual property liability) for actual use based upon the

examples shown in this publication.

国际学术会议影响因子

国际学术会议影响因子

学习文档 仅供参考 Estimated impact of publication venues in

Computer Science (higher is better) - May 2003

(CiteSeer)

Generated from documents in the CiteSeer database. This analysis does not include citations

where one or more authors of the citing and cited articles match. This list is automatically

generated and may contain errors. Only venues with at least 25 articles are shown.

Impact is estimated using the average citation rate, where citations are normalized using the

average citation rate for all articles in a given year, and transformed using ln (n+1) where n is the

number of citations.

Publication details obtained from DBLP by Michael Ley. Only venues contained in DBLP are

included.

1. OSDI: 3.31 (top 0.08%)

2. USENIX Symposium on Internet Technologies and Systems: 3.23 (top 0.16%)

3. PLDI: 2.89 (top 0.24%)