Cet ouvrage et des milliers d'autres font partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour les lire en ligne
En savoir plus

Partagez cette publication

Du même publieur

UnificationofSimplyTypedLambda-TermsasLogicProgrammingDaleMillerLaboratoryfortheFoundationofComputerScienceUniversityofEdinburgh,andComputerScienceDepartmentUniversityofPennsylvaniaMarch1991AbstractTheunificationofsimplytypedλ-termsmodulotherulesofβ-andη-conversionsisoftencalled“higher-order”unificationbecauseofthepossiblepresenceofvariablesoffunctionaltype.Thiskindofunificationisundecidableingeneralandifunifiersexist,mostgeneralunifiersmaynotexist.Inthispaper,weshowthatsuchunificationproblemscanbecodedasaqueryofthelogicprogramminglanguageLλinanaturalandclearfashion.Inasense,thetranslationonlyinvolvesexplicitlyaxiomatizinginLλthenotionsofequalityandsubstitutionofthesimplytypedλ-calculus:therestoftheunificationprocesscanbeviewedassimplyaninterpreterofLλsearchingforproofsusingthoseaxioms.1IntroductionVariousrecentcomputersystemsrequiretypedλ-termstobeunified.Forexample,thetheoremprovingsystemsTPS[1]andIsabelle[14]andthelogicprogramminglanguageλProlog[13]allrequireunificationofsimplytypedλ-terms.ThelogicprogramminglanguageElf[15],basedonthetypesystemLF[5],requiresasimilaroperationfordependenttypedλ-terms.Flexibleimplementationsoftypesystemswillprobablyneedtoemployvariousaspectsofsuchunification.Inordertoavoidusingtheveryvagueandoverusedadjective“higher-order,”weshallrefertotheproblemofunifyingsimplytypedλ-termsmoduloβ-andη-conversionasβη-unification.Therehavebeenseveralpresentationsofβη-unification.OneofthefirsttohavebeenimplementedinnumeroussystemswasgivenbyHuetin[7].SnyderandGallierin[16]andtheauthorin[11]followHuet’spresentationcloselyexceptthatdetailsofthesearchforunifiersaremademoredeclarativeusingnotionssimilartothetransitionsystemsfoundin[8].Thepresentationgivenherewilldepartsignificantlyfromthosefoundintheseotherpapers,althoughinterestingconnectionsbetweenthesepresentationscanbemade.ThemostsignificantdepartureisthatthelogicprogramminglanguageLλ[10]isemployedtoassistinspecifyingAppearsintheProceedingsofthe1991InternationalConferenceonLogicProgramming,editedbyKoichiFurukawa,June1991.1
Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin