A META LANGUAGE FOR TYPE CHECKING AND INFERENCE

Amy Felty

Description

Niveau: Supérieur, Doctorat, Bac+8
A META LANGUAGE FOR TYPE CHECKING AND INFERENCE An Extended Abstract Amy Felty and Dale Miller Department of Computer and Information Science University of Pennsylvania Philadelphia, PA 19104–6389 USA Abstract We present a logic, L?, in which terms are the simply typed ?-terms and very restricted, second-order quantification of functional variables is allowed. This logic can be used to directly encode the basic type judgments of a wide variety of typed ?-calculi. Judgments such as “term M is of type A” and “M is a proof of formula A” are represented by atomic propositions in L? while inference rules and axioms for such type judgments become simple quantified formulas. Theorem proving in L? can be described simply since the necessary unification of ?-terms is decidable and if unifiers exist, most general unifiers exist. Standard logic programming techniques can turn the specification of inference rules and axioms in L? into implementations of type checkers and inferrers. Several different typed ?-calculi have been specified in L? and these specifications have been directly executed by a higher-order logic programming language. We illustrate such encoding into L? by presenting type checkers and inferrers for the simply typed ?-calculus and the calculus of constructions. This extended abstract will be presented at the 1989 Workshop on Programming Logic, B˚alstad, Sweden. Comments are welcome. Address correspondence to the authors at the address above or at “felty@linc.

• either bound


• terms into


• typed ?-terms


• free variable


• simply typed


• l? can


• logic programming


• order horn


• being simply


• higher-order hereditary

Sujets

• Free variables and bound variables
• Logic programming

Informations

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

Extrait

AMETALANGUAGEFOR TYPECHECKINGANDINFERENCE AnExtendedAbstract AmyFeltyandDaleMiller Department U of ni C ve o rs m it p y ut o e f r P a e n n d ns I y n l f v o a r n m ia ationScience Philadelphia,PA19104–6389USA Abstract Wepresentalogic,L λ ,inwhichtermsarethesimplytypedλ-termsandveryrestricted, second-orderquantificationoffunctionalvariablesisallowed.Thislogiccanbeusedto directlyencodethebasictypejudgmentsofawidevarietyoftypedλ-calculi.Judgments suchas“termMisoftypeA”and“MisaproofofformulaA”arerepresentedby atomicpropositionsinL λ whileinferencerulesandaxiomsforsuchtypejudgments becomesimplequantifiedformulas.TheoremprovinginL λ canbedescribedsimply sincethenecessaryunificationofλ-termsisdecidableandifunifiersexist,mostgeneral unifiersexist.Standardlogicprogrammingtechniquescanturnthespecificationof inferencerulesandaxiomsinL λ intoimplementationsoftypecheckersandinferrers. Severaldifferenttypedλ-calculihavebeenspecifiedinL λ andthesespecificationshave beendirectlyexecutedbyahigher-orderlogicprogramminglanguage.Weillustrate suchencodingintoL λ bypresentingtypecheckersandinferrersforthesimplytyped λ-calculusandthecalculusofconstructions. Thisextendedabstractwillbepresentedatthe1989WorkshoponProgramming Logic,Ba˚lstad,Sweden. Commentsarewelcome.Addresscorrespondencetotheauthorsattheaddress aboveorat“[e-mail]”or“[e-mail].”