AN OVERVIEW OF PROLOG

Duke University

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

• University
• Higher
• Logic programming
• Logical connective
• Horn clause

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 12
• Langue: English

Extrait

ANOVERVIEWOFλPROLOG GOPALANNADATHUR DepartmentofComputerScience DukeUniversity Durham,NC27706 DALEMILLER DepartmentofComputerandInformationScience UniversityofPennsylvania Philadelphia,PA19104-6389 Abstract:λPrologisalogicprogramminglanguagethatextendsPrologbyin- corporatingnotionsofhigher-orderfunctions,λ-terms,higher-orderunification, polymorphictypes,andmechanismsforbuildingmodulesandsecureabstractdata types.Thesenewfeaturesareprovidedinaprincipledfashionbyextendingthe classicalfirst-ordertheoryofHornclausestotheintuitionistichigher-ordertheory ofhereditaryHarropformulas.Thejustificationforconsideringthisextensiona satisfactorylogicprogramminglanguageisprovidedthroughtheproof-theoretic notionofauniformproof.ThecorrespondencebetweeneachextensiontoProlog andthenewfeaturesinthestrongerlogicaltheoryisdiscussed.Alsodiscussed arevariousaspectsofanexperimentalimplementationofλProlog. AppearsintheFifthInternationalConferenceSymposiumonLogicProgramming, 15–19August1988,Seattle,Washington.Thisisaslightlycorrectedversionof thepaperintheProceedings. [e-mail]@linc.cis.upenn.eduorto theaddressesabove. –1–

1.Introduction 1.Introduction ThelogicprogramminglanguageλPrologisanextensionofconventionalPro- log[32]inseveraldifferentdirections:itsupportshigher-orderprogramming,in- corporatesλ-termsasdatastructures,includesanotionofpolymorphictyping, andprovidesmechanismsfordefiningmodulesandsecureabstractdatatypes. Therehavebeenseveralproposalsinthepastforaddingfeaturesofthissortto Prolog.TheworkinthecontextofλPrologisdistinguishablefrommostofthese proposalsinthatthefirstconcernhasbeentoexaminetheessentiallogicaland proof-theoreticnatureoftheseextensions.Theresultofthisanalysishasbeenthe descriptionofaclassofformulasthatarecalledhigher-orderhereditaryHarrop (hohh)formulas.TheseformulasplayaroleinλPrologthatissimilartotherole playedbyfirst-orderpositiveHornclausesinProlog.Thehohhformulassignifi- cantlyextendpositiveHornclauses,andthenewfeaturesprovidedinλPrologare theresultofexploitingtheextensionfoundinhohhformulas. WediscussseveralaspectsoftheworkonλProloginthispaper.Inthenext sectionwedescribethehohhformulasandprovidetherationaleforconsidering themasuitablebasisforalogicprogramminglanguage.Section3highlightsthe logicalfeaturesthatarenewinhohhformulasandexplainstheiruseinproviding extensionstologicprogramming.Finally,wedescribeanimplementationofa versionofthislogicinSection4,dwellingonsomeofthenewproblemsthatwere encounteredinitscontext. 2.ReconsideringtheFoundationinHornClauses Weinitiallyconsideredahigher-orderextensiontoHornclausesbecausewe wereinterestedinaddressinganaspectofincompletenessintheoremproversin higher-orderlogic.Inlogicsthatpermitpredicatequantification,newtechniques mustbedevisedforfindingappropriatesubstitutionsforpredicatesvariablessince thesecannotingeneralbedeterminedthroughstandardusesof(evenhigher- order)unification.Thisproblemappearedtobeverydifficulttosolveforgeneral higher-orderlogic[1],anditthereforeseemednaturaltofocusattentionona sublogic.Onepossibilitywastoconsidersomeformofhigher-orderextensionto Hornclauses.Thispossibilityappearedtobeindependentlyinterestingsinceit alsoprovidedabasisforstudyinghigher-ordernotionsinlogicprogramming,an 2––