Unification of Simply Typed Lambda Terms as Logic Programming

Description

Niveau: Supérieur
Unification of Simply Typed Lambda-Terms as Logic Programming Dale Miller? Laboratory for the Foundation of Computer Science University of Edinburgh, and Computer Science Department University of Pennsylvania March 1991 Abstract The unification of simply typed ?-terms modulo the rules of ?- and ?-conversions is often called “higher-order” unification because of the possible presence of variables of functional type. This kind of unification is undecidable in general and if unifiers exist, most general unifiers may not exist. In this paper, we show that such unification problems can be coded as a query of the logic programming language L? in a natural and clear fashion. In a sense, the translation only involves explicitly axiomatizing in L? the notions of equality and substitution of the simply typed ?-calculus: the rest of the unification process can be viewed as simply an interpreter of L? searching for proofs using those axioms. 1 Introduction Various recent computer systems require typed ?-terms to be unified. For example, the theorem proving systems TPS [1] and Isabelle [14] and the logic programming language ?Prolog [13] all require unification of simply typed ?-terms. The logic programming language Elf [15], based on the type system LF [5], requires a similar operation for dependent typed ?-terms. Flexible implementations of type systems will probably need to employ various aspects of such unification.

• binary equality predicates


• terms


• avoid variable


• higher order


• used adjective


• order horn


• clause


• terms modulo


• ?0

Sujets

• Clause

Informations

• Publié par: chaeh
• Nombre de lectures: 18
• Langue: English

Extrait

UnificationofSimplyTypedLambda-TermsasLogic Programming DaleMiller ∗ LaboratoryfortheFoundationofComputerScience UniversityofEdinburgh,and ComputerScienceDepartment UniversityofPennsylvania March1991 Abstract Theunificationofsimplytypedλ-termsmodulotherulesofβ-andη-conversionsisoftencalled “higher-order”unificationbecauseofthepossiblepresenceofvariablesoffunctionaltype.This kindofunificationisundecidableingeneralandifunifiersexist,mostgeneralunifiersmaynot exist.Inthispaper,weshowthatsuchunificationproblemscanbecodedasaqueryofthe logicprogramminglanguageL λ inanaturalandclearfashion.Inasense,thetranslationonly involvesexplicitlyaxiomatizinginL λ thenotionsofequalityandsubstitutionofthesimply typedλ-calculus:therestoftheunificationprocesscanbeviewedassimplyaninterpreterof L λ searchingforproofsusingthoseaxioms. 1Introduction Variousrecentcomputersystemsrequiretypedλ-termstobeunified.Forexample,thetheorem provingsystemsTPS[1]andIsabelle[14]andthelogicprogramminglanguageλProlog[13] allrequireunificationofsimplytypedλ-terms.ThelogicprogramminglanguageElf[15], basedonthetypesystemLF[5],requiresasimilaroperationfordependenttypedλ-terms. Flexibleimplementationsoftypesystemswillprobablyneedtoemployvariousaspectsofsuch unification. Inordertoavoidusingtheveryvagueandoverusedadjective“higher-order,”weshall refertotheproblemofunifyingsimplytypedλ-termsmoduloβ-andη-conversionasβη- unification.Therehavebeenseveralpresentationsofβη-unification.Oneofthefirsttohave beenimplementedinnumeroussystemswasgivenbyHuetin[7].SnyderandGallierin[16] andtheauthorin[11]followHuet’spresentationcloselyexceptthatdetailsofthesearchfor unifiersaremademoredeclarativeusingnotionssimilartothetransitionsystemsfoundin[8]. Thepresentationgivenherewilldepartsignificantlyfromthosefoundintheseotherpapers, althoughinterestingconnectionsbetweenthesepresentationscanbemade.Themostsignificant departureisthatthelogicprogramminglanguageL λ [10]isemployedtoassistinspecifying ∗ AppearsintheProceedingsofthe1991InternationalConferenceonLogicProgramming,editedbyKoichi Furukawa,June1991. 1