Combining generic judgments with recursive definitions

Andrew Gacek

Description

Niveau: Supérieur, Doctorat, Bac+8
Combining generic judgments with recursive definitions Andrew Gacek Department of CS&E University of Minnesota Dale Miller INRIA Saclay - Ile-de-France & LIX/Ecole polytechnique Gopalan Nadathur Department of CS&E University of Minnesota Abstract Many semantical aspects of programming languages, such as their operational semantics and their type assign- ment calculi, are specified by describing appropriate proof systems. Recent research has identified two proof-theoretic features that allow direct, logic-based reasoning about such descriptions: the treatment of atomic judgments as fixed points (recursive definitions) and an encoding of binding constructs via generic judgments. However, the logics en- compassing these two features have thus far treated them orthogonally: that is, they do not provide the ability to de- fine object-logic properties that themselves depend on an intrinsic treatment of binding. We propose a new and sim- ple integration of these features within an intuitionistic logic enhanced with induction over natural numbers and we show that the resulting logic is consistent. The pivotal benefit of the integration is that it allows recursive definitions to not just encode simple, traditional forms of atomic judg- ments but also to capture generic properties pertaining to such judgments. The usefulness of this logic is illustrated by showing how it can provide elegant treatments of object- logic contexts that appear in proofs involving typing calculi and of arbitrarily cascading substitutions that play a role in reducibility arguments.

• quantification over


• nominal constant


• must behavior


• free variable


• rules involves


• logic programming


• such constants


• has


• clause


• proof theoretic techniques

Sujets

• École polytechnique
• Free variables and bound variables
• Logic programming
• Clause

Informations

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

Extrait

Combininggenericjudgmentswithrecursivedefinitions AndrewGacekDaleMillerGopalanNadathur DepartmentofCS&E INRIASaclay-I ˆ le-de-France DepartmentofCS&E UniversityofMinnesota &LIX/E ´ colepolytechnique UniversityofMinnesota Abstract Manysemanticalaspectsofprogramminglanguages, suchastheiroperationalsemanticsandtheirtypeassign- mentcalculi,arespecifiedbydescribingappropriateproof systems.Recentresearchhasidentifiedtwoproof-theoretic featuresthatallowdirect,logic-basedreasoningaboutsuch descriptions:thetreatmentofatomicjudgmentsasfixed points(recursivedefinitions)andanencodingofbinding constructsviagenericjudgments.However,thelogicsen- compassingthesetwofeatureshavethusfartreatedthem orthogonally:thatis,theydonotprovidetheabilitytode- fineobject-logicpropertiesthatthemselvesdependonan intrinsictreatmentofbinding.Weproposeanewandsim- pleintegrationofthesefeatureswithinanintuitionisticlogic enhancedwithinductionovernaturalnumbersandweshow thattheresultinglogicisconsistent.Thepivotalbenefit oftheintegrationisthatitallowsrecursivedefinitionsto notjustencodesimple,traditionalformsofatomicjudg- mentsbutalsotocapturegenericpropertiespertainingto suchjudgments.Theusefulnessofthislogicisillustrated byshowinghowitcanprovideeleganttreatmentsofobject- logiccontextsthatappearinproofsinvolvingtypingcalculi andofarbitrarilycascadingsubstitutionsthatplayarolein reducibilityarguments. Keywords:genericjudgments,higher-orderabstractsyn- tax,proofsearch,reasoningaboutoperationalsemantics 1.Introduction Animportantapproachtospecifyingandreasoning aboutcomputationsinvolvesprooftheoryandproofsearch. Wediscussbelowthreekindsofjudgmentsaboutcomputa- tionalsystemsthatonemightwanttocaptureandtheproof theoretictechniquesthathavebeenusedtocapturethem. Wedividethisdiscussionintotwoparts:thefirstpartdeals withjudgmentsoveralgebraictermsandthesecondwith judgmentsoverterms-with-binders.Wethenexploitthis overviewtodescribethenewfeaturesofthelogicweare presentinginthispaper. 1.1.Judgmentsinvolvingalgebraicterms Weoverviewfeaturesofprooftheorythatsupportrecur- sivedefinitionsaboutfirst-order(algebraic)termsand,us- ingCCSasanexample,weillustratethejudgmentsabout computationsthatcanbeencodedthroughsuchdefinitions. (1)Logicprogramming,maybehaviorLogicprogram- minglanguagesallowforanaturalspecificationandani- mationofoperationalsemanticsandtypingjudgments:this observationgoesbacktoatleasttheCentaurprojectand itsanimationofTypolspecificationsusingProlog[5].For example,Hornclausesprovideasimpleandimmediateen- codingofCCSlabeledtransitionsystemsandunification andbacktrackingprovideameansforexploringwhatis reachable fromagivenprocess.Traditionallogicprogram- mingis,however,limitedtomaybehaviorjudgments:us- ingit,wecannotprovethatagivenCCSprocessPcannot makeatransitionand,sincethisnegativepropertyislogi- callyequivalenttoprovingthatPisbisimilarto0(thenull process),suchsystemscannotcapturebisimulation. (2)Modelchecking,mustbehaviorProoftheoretic techniquesformustbehaviors(suchasbisimulationand manymodelcheckingproblems)havebeendevelopedin theearly1990’s[8,29]andfurtherextendedlater[15]. Sincethesetechniquesworkbyunfoldingcomputationsun- tiltermination,theyareapplicabletorecursivedefinitions thatarenoetherian.Asanexample,bisimulationforfinite CCScanbegivenanimmediateanddeclarativespecifica- tion[17]. (3)Theoremproving,infinitebehaviorReasoning aboutallmembersofadomainoraboutpossiblyinfinite executionsrequiresinductionandcoinduction.Incorporat- inginductioninprooftheorygoesbacktoGentzen.The workin[15,23,33]providesinductionandcoinduction rulesassociatedwiththeabove-mentionedrecursivedefi- nitions.Insuchasetting,onecanprove,forexample,that (strong)bisimulationinCCSisacongruence.