AN OVERVIEW OF PROLOG
20 pages
English

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

AN OVERVIEW OF PROLOG

-

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
AN OVERVIEW OF ?PROLOG GOPALAN NADATHUR Department of Computer Science Duke University Durham, NC 27706 DALE MILLER Department of Computer and Information Science University of Pennsylvania Philadelphia, PA 19104-6389 Abstract: ?Prolog is a logic programming language that extends Prolog by in- corporating notions of higher-order functions, ?-terms, higher-order unification, polymorphic types, and mechanisms for building modules and secure abstract data types. These new features are provided in a principled fashion by extending the classical first-order theory of Horn clauses to the intuitionistic higher-order theory of hereditary Harrop formulas. The justification for considering this extension a satisfactory logic programming language is provided through the proof-theoretic notion of a uniform proof. The correspondence between each extension to Prolog and the new features in the stronger logical theory is discussed. Also discussed are various aspects of an experimental implementation of ?Prolog. Appears in the Fifth International Conference Symposium on Logic Programming, 15 – 19 August 1988, Seattle, Washington. This is a slightly corrected version of the paper in the Proceedings. Address correspondence to or or to the addresses above. – 1 –

  • order unification

  • intuitionistic higher-order

  • higher

  • logic programming

  • calculus provides

  • solely through

  • logical connective

  • horn clause


Sujets

Informations

Publié par
Nombre de lectures 12
Langue English

Exrait

ANOVERVIEWOFλPROLOGGOPALANNADATHURDepartmentofComputerScienceDukeUniversityDurham,NC27706DALEMILLERDepartmentofComputerandInformationScienceUniversityofPennsylvaniaPhiladelphia,PA19104-6389Abstract:λPrologisalogicprogramminglanguagethatextendsPrologbyin-corporatingnotionsofhigher-orderfunctions,λ-terms,higher-orderunification,polymorphictypes,andmechanismsforbuildingmodulesandsecureabstractdatatypes.Thesenewfeaturesareprovidedinaprincipledfashionbyextendingtheclassicalfirst-ordertheoryofHornclausestotheintuitionistichigher-ordertheoryofhereditaryHarropformulas.Thejustificationforconsideringthisextensionasatisfactorylogicprogramminglanguageisprovidedthroughtheproof-theoreticnotionofauniformproof.ThecorrespondencebetweeneachextensiontoPrologandthenewfeaturesinthestrongerlogicaltheoryisdiscussed.AlsodiscussedarevariousaspectsofanexperimentalimplementationofλProlog.AppearsintheFifthInternationalConferenceSymposiumonLogicProgramming,15–19August1988,Seattle,Washington.ThisisaslightlycorrectedversionofthepaperintheProceedings.Addresscorrespondencetogopalan@cs.duke.eduordale@linc.cis.upenn.eduortotheaddressesabove.1
1.Introduction1.IntroductionThelogicprogramminglanguageλPrologisanextensionofconventionalPro-log[32]inseveraldifferentdirections:itsupportshigher-orderprogramming,in-corporatesλ-termsasdatastructures,includesanotionofpolymorphictyping,andprovidesmechanismsfordefiningmodulesandsecureabstractdatatypes.TherehavebeenseveralproposalsinthepastforaddingfeaturesofthissorttoProlog.TheworkinthecontextofλPrologisdistinguishablefrommostoftheseproposalsinthatthefirstconcernhasbeentoexaminetheessentiallogicalandproof-theoreticnatureoftheseextensions.Theresultofthisanalysishasbeenthedescriptionofaclassofformulasthatarecalledhigher-orderhereditaryHarrop(hohh)formulas.TheseformulasplayaroleinλPrologthatissimilartotheroleplayedbyfirst-orderpositiveHornclausesinProlog.Thehohhformulassignifi-cantlyextendpositiveHornclauses,andthenewfeaturesprovidedinλPrologaretheresultofexploitingtheextensionfoundinhohhformulas.WediscussseveralaspectsoftheworkonλProloginthispaper.Inthenextsectionwedescribethehohhformulasandprovidetherationaleforconsideringthemasuitablebasisforalogicprogramminglanguage.Section3highlightsthelogicalfeaturesthatarenewinhohhformulasandexplainstheiruseinprovidingextensionstologicprogramming.Finally,wedescribeanimplementationofaversionofthislogicinSection4,dwellingonsomeofthenewproblemsthatwereencounteredinitscontext.2.ReconsideringtheFoundationinHornClausesWeinitiallyconsideredahigher-orderextensiontoHornclausesbecausewewereinterestedinaddressinganaspectofincompletenessintheoremproversinhigher-orderlogic.Inlogicsthatpermitpredicatequantification,newtechniquesmustbedevisedforfindingappropriatesubstitutionsforpredicatesvariablessincethesecannotingeneralbedeterminedthroughstandardusesof(evenhigher-order)unification.Thisproblemappearedtobeverydifficulttosolveforgeneralhigher-orderlogic[1],anditthereforeseemednaturaltofocusattentiononasublogic.Onepossibilitywastoconsidersomeformofhigher-orderextensiontoHornclauses.Thispossibilityappearedtobeindependentlyinterestingsinceitalsoprovidedabasisforstudyinghigher-ordernotionsinlogicprogramming,an2
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents