Abstract Syntax and Logic Programming September
16 pages
English

Abstract Syntax and Logic Programming September

-

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
16 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Niveau: Supérieur, Doctorat, Bac+8
Abstract Syntax and Logic Programming September 1991 Dale Miller Department of Computer and Information Science University of Pennsylvania Philadelphia, PA 19104–6389 USA Abstract. When writing programs to manipulate structures such as algebraic ex- pressions, logical formulas, proofs, and programs, it is highly desirable to take the linear, human-oriented, concrete syntax of these structures and parse them into a more computation-oriented syntax. For a wide variety of manipulations, concrete syntax contains too much useless information (e.g., keywords and white space) while impor- tant information is not explicitly represented (e.g., function-argument relations and the scope of operators). In parse trees, much of the semantically useless information is removed while other relationships, such as between function and argument, are made more explicit. Unfortunately, parse trees do not adequately address important notions of object-level syntax, such as bound and free object-variables, scopes, alphabetic changes of bound variables, and object-level substitution. I will argue here that the abstract syn- tax of such objects should be organized around ?-equivalence classes of ?-terms instead of parse trees. Incorporating this notion of abstract syntax into programming languages is an interesting challenge. This paper briefly describes a logic programming language that directly supports this notion of syntax.

  • modulo ?-conversion

  • bad points

  • signature de ?

  • typed ?-terms

  • bound variable

  • abstract syntax

  • conversion

  • such


Sujets

Informations

Publié par
Nombre de lectures 41
Langue English

Exrait

AbstractSyntaxandLogicProgrammingSeptember1991DaleMillerDepartmentofComputerandInformationScienceUniversityofPennsylvaniaPhiladelphia,PA19104–6389USAdale@cis.upenn.eduAbstract.Whenwritingprogramstomanipulatestructuressuchasalgebraicex-pressions,logicalformulas,proofs,andprograms,itishighlydesirabletotakethelinear,human-oriented,concretesyntaxofthesestructuresandparsethemintoamorecomputation-orientedsyntax.Forawidevarietyofmanipulations,concretesyntaxcontainstoomuchuselessinformation(e.g.,keywordsandwhitespace)whileimpor-tantinformationisnotexplicitlyrepresented(e.g.,function-argumentrelationsandthescopeofoperators).Inparsetrees,muchofthesemanticallyuselessinformationisremovedwhileotherrelationships,suchasbetweenfunctionandargument,aremademoreexplicit.Unfortunately,parsetreesdonotadequatelyaddressimportantnotionsofobject-levelsyntax,suchasboundandfreeobject-variables,scopes,alphabeticchangesofboundvariables,andobject-levelsubstitution.Iwillargueherethattheabstractsyn-taxofsuchobjectsshouldbeorganizedaroundα-equivalenceclassesofλ-termsinsteadofparsetrees.Incorporatingthisnotionofabstractsyntaxintoprogramminglanguagesisaninterestingchallenge.Thispaperbrieflydescribesalogicprogramminglanguagethatdirectlysupportsthisnotionofsyntax.Anexamplespecificationsinthisprogram-minglanguageispresentedtoillustrateitsapproachtohandlingobject-levelsyntax.Amodeltheoreticsemanticsforthislogicprogramminglanguageisalsopresented.1.IntroductionConsiderwritingprogramsinwhichthedataobjectstobecomputedaresyntacticstructuressuchasprograms,formulas,types,andproofs.Acommoncharacteristicofallthesestructuresisthattheyinvolvenotionsofabstractions,scope,boundandfreevariables,substitutioninstances,andequalityuptoalphabeticchangesofboundvariables.Althoughthedatatypesavailableinmostcomputerprogramminglanguagesare,ofcourse,richenoughtorepresentallthesekindsofstructures,suchdatatypesdonothavedirectsupportforthesecommoncharacteristics.Instead,“packages”needtobeimplementedtosupportsuchdatastructures.Forexample,althoughitistrivialtorepresentfirst-orderformulasinLisp,itisamorecomplexmattertowriteLispprogramsthatcorrectlysubstituteatermintoaformula(beingcarefulnottocaptureboundvariables),totestfortheequalityofformulasuptoalphabeticvariation,andtodetermineifacertainvariable’soccurrenceisfreeorbound.ThissituationisthesameToappearintheProceedingsoftheSecondRussianConferenceonLogicProgram-ming,September1991,editedbyA.Voronkov,LectureNotesinArtificialIntelligence,Springer-Verlag.1
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents