A LOGIC PROGRAMMING APPROACH TO MANIPULATING FORMULAS AND PROGRAMS
20 pages
English

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

A LOGIC PROGRAMMING APPROACH TO MANIPULATING FORMULAS AND PROGRAMS

-

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
20 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Niveau: Supérieur, Doctorat, Bac+8
A LOGIC PROGRAMMING APPROACH TO MANIPULATING FORMULAS AND PROGRAMS Dale Miller Computer and Information Science University of Pennsylvania Philadelphia, PA 19104 Gopalan Nadathur Department of Computer Science Duke University Durham, NC 27706 24 April 2002 Abstract: First-order Horn clause logic can be extended to a higher-order setting in which function and predicate symbols can be variables and terms are replaced with simply typed ?-terms. For such a logic programming language to be complete in principle, it must incorporate higher-order unification. Although higher-order unification is more complex than usual first-order unification, its availability makes writing certain kinds of programs far more straightforward. In this paper, we present such programs written in a higher- order version of Prolog called ?Prolog. These programs manipulate structures, such as formulas and programs, which contain abstractions or bound variables. We show how a simple natural deduction theorem prover can be implemented in this language. Similarly we demonstrate how several simple program transformers for a functional programming language can be written in ?Prolog. These ?Prolog programs exploit the availability of ?-conversion and higher-order unification to elegantly deal with several of the awkward aspects inherent in these tasks. We argue that writing similar procedures in other languages would yield programs which are much less perspicuous. Submitted to the 1987 IEEE Symposium on Logic Programming. Comments are welcome.

  • while higher

  • order unification

  • predicate variable

  • has been

  • higher

  • logic programming

  • such schemata

  • language can

  • such

  • guage like


Sujets

Informations

Publié par
Nombre de lectures 48
Langue English

Extrait

ALOGICPROGRAMMINGAPPROACHTOMANIPULATINGFORMULASANDPROGRAMSDaleMillerComputerandInformationScienceUniversityofPennsylvaniaPhiladelphia,PA19104GopalanNadathurDepartmentofComputerScienceDuDrhuakem,UNniCvers2i7ty70624April2002Abstract:First-orderHornclauselogiccanbeextendedtoahigher-ordersettinginwhichfunctionandpredicatesymbolscanbevariablesandtermsarereplacedwithsimplytypedλ-terms.Forsuchalogicprogramminglanguagetobecompleteinprinciple,itmustincorporatehigher-orderunification.Althoughhigher-orderunificationismorecomplexthanusualfirst-orderunification,itsavailabilitymakeswritingcertainkindsofprogramsfarmorestraightforward.Inthispaper,wepresentsuchprogramswritteninahigher-orderversionofPrologcalledλProlog.Theseprogramsmanipulatestructures,suchasformulasandprograms,whichcontainabstractionsorboundvariables.Weshowhowasimplenaturaldeductiontheoremprovercanbeimplementedinthislanguage.SimilarlywedemonstratehowseveralsimpleprogramtransformersforafunctionalprogramminglanguagecanbewritteninλProlog.TheseλPrologprogramsexploittheavailabilityofλ-conversionandhigher-orderunificationtoelegantlydealwithseveraloftheawkwardaspectsinherentinthesetasks.Wearguethatwritingsimilarproceduresinotherlanguageswouldyieldprogramswhicharemuchlessperspicuous.Submittedtothe1987IEEESymposiumonLogicProgramming.Commentsarewelcome.AddresscorrespondencetoMillerataddressaboveorat“dale@linc.cis.upenn.edu”.ThisworkhasbeensupportedbyNSFAICentergrantsNSF-MCS-83-05221,USArmyRe-searchofficegrantARO-DAA29-84-9-0027,andDARPAN000-14-85-K-0018.ThesecondauthorhasalsobeensupportedbyaBurroughscontract.
1.IntroductionThedatastructuresthathavetraditionallybeenusedinalogicprogramminglanguagesuchasProloghavebeenrestrictedtofirst-orderterms.Itiseasy,however,toimagineextendingthesedata-structurestothetermsofaλ-calculus,andwebelievethattherecertaingainstobeobtainedbydoingso.Thereareseveralkindsofobjectswhoserepresentationinalogicallycorrectmannerrequiresatermlanguagethatincorporateshigher-ordernotions.Examplesofthesekindsofobjectsareprovidedbyprogramsandformulas.Thetaskofdescribingthedenotationsofprograms,forinstance,requiresanallusiontotheoperationsofabstractionandapplica-tion;itisthereforeclearthatinordertorepresentprogramsinafashioncloselyrelatedtotheirmeaningsrequiresthedata-structuresprovided,forinstance,byλ-terms.Similarly,anadequatecharacterisationoftheoperationofquantificationinfirst-orderformulasre-quiresasetofdata-structuresthatprovidesthenotionofabstractioninconjunctionwithfirst-orderterms.Theuseofλ-termsinalogicprogramminglanguagethusprovidesuswithafacilityinrepresentingtheabovekindsofobjects.Iffunctionvariableswerealsopermittedtobefreeinλ-terms,thenwecouldusethesetermsasschematatorepresentclassesofobjectswhosemeaninghaveacommon“compositionalstructure,”andwecouldthususesuchanextendedlogicprogramminglanguagetospecifylogicallymeaningfulrelationshipsbetweensuchclassesofobjects.Forspecificexampleswheresuchanabilityhasapplicationsconsiderthefollowing.(i)Rulesoflogicalinferencecanbeseenasrelationshipsbetweenformulaschemata.Giventhatsuchschematacanberepresentedbythedatastructuresofsuchahigher-orderlogicprogramminglanguage,theprocessofdeductioninalogicalsystemcaneasilybespecifiedbydefiniteclausesinthislanguage.(ii)Certainkindsofprogramtransformations[2]canbethoughtofasrelationshipsbe-tweenprogramschemes.Programschemescanberepresentedbyλ-termsinwhichfunctionvariablesappearfree[7].Thusdefiniteclausesinthishypotheticallanguagecanbeusedtoencode,andthusspecify,suchprogramtransformations.Theaboveobservationsthusrevealapotentiallyrichrealmofapplicationsforahigher-orderlogicprogramminglanguage.Whiletheadditionofhigher-orderfeaturestoalan-guagelikeProloghasbeenconsideredinthepast,thetruepotentialofsuchanadditionhasnotreallybeenunderstood.Somework(e.g.[12])hasbeendonetowardprovidinghigher-orderfeaturespresentinLisp-likelanguagesthroughmechanismsforencodingpredicatevariables.Theusefulnessoffunctionvariablesinconjunctionwithλ-termshas,however,notbeenrecognized.Itiscommon,instead,todismisstheiradditionwiththeobservationthathigher-orderunificationisundecidable.Whilehigher-orderunificationisacomplexoperation,itisourbeliefthatitprovidesusamechanismwithwhichwemaysolvedifficultproblemsinaconceptuallyelegantway.Ourpurposeinthispaperisprimarilytoprovide1
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • Podcasts Podcasts
  • BD BD
  • Documents Documents