A LOGIC PROGRAMMING LANGUAGE WITH LAMBDA ABSTRACTION FUNCTION VARIABLES AND SIMPLE UNIFICATION: Extended Abstract Draft September

Description

Niveau: Supérieur, Doctorat, Bac+8
A LOGIC PROGRAMMING LANGUAGE WITH LAMBDA-ABSTRACTION, FUNCTION VARIABLES, AND SIMPLE UNIFICATION: Extended Abstract Draft, 20 September 1989 Dale Miller Department of Computer and Information Science University of Pennsylvania Philadelphia, PA 19104–6389 USA 1. Introduction A meta programming language must be able to represent and manipulate such syn- tactic structures as programs, formulas, types, and proofs. A common characteristic of all these structures is that they involve notions of abstractions, scope, bound and free variables, substitution instances, and equality up to alphabetic changes of bound vari- ables. Although the data types available in most computer programming languages are rich enough to represent all these kinds of structures, such data types do not have direct support of these other notions. For example, although it is trivial for Lisp to represent first-order formulas, it is a more complex matter to write Lisp programs that correctly substitute a term into a formulas (being careful not to capture bound variables), to test for the equivalence of formulas up to alphabetic variation, and to determine if a certain variable's occurrence is free or bound. This situation is the same when structures like programs or (natural deduction) proofs are to be manipulated and if other programming languages, such as Pascal, Prolog, and ML, replace Lisp. It is desirable for a meta programming language to have language-level support for these various aspects of formulas, proofs, types, and programs.

• syn- tactic structures


• order unification


• unification problem


• structure ?


• variable


• logic programming


• language can


• such logic

Sujets

• Unification
• Variable
• Logic programming

Informations

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

Extrait

ALOGICPROGRAMMINGLANGUAGEWITH LAMBDA-ABSTRACTION,FUNCTIONVARIABLES, ANDSIMPLEUNIFICATION: ExtendedAbstract Draft,20September1989 DaleMiller DepartmentofComputerandInformationScience U Ph n i i l v a e d r e si l t p y hi o a f , P P e A nn 1 s 9 y 1 l 0 v 4 a – n 6 ia 389USA 1.Introduction Ametaprogramminglanguagemustbeabletorepresentandmanipulatesuchsyn- tacticstructuresasprograms,formulas,types,andproofs.Acommoncharacteristicof allthesestructuresisthattheyinvolvenotionsofabstractions,scope,boundandfree variables,substitutioninstances,andequalityuptoalphabeticchangesofboundvari- ables.Althoughthedatatypesavailableinmostcomputerprogramminglanguagesare richenoughtorepresentallthesekindsofstructures,suchdatatypesdonothavedirect supportoftheseothernotions.Forexample,althoughitistrivialforLisptorepresent first-orderformulas,itisamorecomplexmattertowriteLispprogramsthatcorrectly substituteatermintoaformulas(beingcarefulnottocaptureboundvariables),totest fortheequivalenceofformulasuptoalphabeticvariation,andtodetermineifacertain variable’soccurrenceisfreeorbound.Thissituationisthesamewhenstructureslike programsor(naturaldeduction)proofsaretobemanipulatedandifotherprogramming languages,suchasPascal,Prolog,andML,replaceLisp. Itisdesirableforametaprogramminglanguagetohavelanguage-levelsupportfor thesevariousaspectsofformulas,proofs,types,andprograms.Whatisacommonframe- workforrepresentingthesestructures?EarlypapersbyChurch,Curry,Howard,Martin- Lo¨f,Scott,Strachey,Tait,andothersconcludethattypedanduntyped λ -calculiprovidea commonsyntacticrepresentationforallthesestructures.Thusametaprogramminglan- guagethatisabletorepresenttermsinsuchλ-calculidirectlycouldbeusedtorepresent thesestructuresusingthetechniquesdescribedbytheseauthors. Oneproblemofdesigningadatatypeforλ-termsisthatmethodsfordestructuring themshouldbeinvariantundertheintendednotionsofequalityof λ -terms,whichusually includesα-conversion.Thus,destructuringtheλ-termλx.fxxintoitsboundvariablex –1–