Encoding Generic Judgments

-

English
15 Pages
Read an excerpt
Gain access to the library to view online
Learn more

Description

Niveau: Supérieur
Encoding Generic Judgments ? Dale Miller1 and Alwen Tiu2 1 INRIA-FUTURS and Ecole Polytechnique , 2 Pennsylvania State University and Ecole Polytechnique Abstract. The operational semantics of a computation system is often presented as inference rules or, equivalently, as logical theories. Specifi- cations can be made more declarative and high-level if syntactic details concerning bound variables and substitutions are encoded directly into the logic using term-level abstractions (?-abstraction) and proof-level ab- stractions (eigenvariables). When one wishes to reason about relations defined using term-level abstractions, generic judgment are generally re- quired. Care must be taken, however, so that generic judgments are not uniformly handled using proof-level abstractions. Instead, we present a technique for encoding generic judgments and show two examples where generic judgments need to be treated at the term level: one example is an interpreter for Horn clauses extended with universal quantified bodies and the other example is that of the pi-calculus. 1 Introduction The operational semantics of a programming or specification language is often given in a relational style using inference rules following a small-step approach (a.k.a., structured operational semantic [Plo81]) or big-step approach (a.k.a.

  • can also

  • bound variable

  • higher-order abstract

  • since provability

  • order pattern

  • capture rich

  • clause

  • syntactic category

  • horn clause


Subjects

Informations

Published by
Reads 14
Language English
Report a problem
EncodingGenericJudgments?DaleMiller1andAlwenTiu21INRIA-FUTURSandE`colePolytechniquedale.miller@inria.fr,2PennsylvaniaStateUniversityandE`colePolytechniquetiu@cse.psu.eduAbstract.Theoperationalsemanticsofacomputationsystemisoftenpresentedasinferencerulesor,equivalently,aslogicaltheories.Specifi-cationscanbemademoredeclarativeandhigh-levelifsyntacticdetailsconcerningboundvariablesandsubstitutionsareencodeddirectlyintothelogicusingterm-levelabstractions(λ-abstraction)andproof-levelab-stractions(eigenvariables).Whenonewishestoreasonaboutrelationsdefinedusingterm-levelabstractions,genericjudgmentaregenerallyre-quired.Caremustbetaken,however,sothatgenericjudgmentsarenotuniformlyhandledusingproof-levelabstractions.Instead,wepresentatechniqueforencodinggenericjudgmentsandshowtwoexampleswheregenericjudgmentsneedtobetreatedatthetermlevel:oneexampleisaninterpreterforHornclausesextendedwithuniversalquantifiedbodiesandtheotherexampleisthatoftheπ-calculus.1IntroductionTheoperationalsemanticsofaprogrammingorspecificationlanguageisoftengiveninarelationalstyleusinginferencerulesfollowingasmall-stepapproach(a.k.a.,structuredoperationalsemantic[Plo81])orbig-stepapproach(a.k.a.naturalsemantics[Kah87]).Ineithercase,algebraic(first-order)termscanbeusedtoencodethelanguagebeingspecifiedandthefirst-ordertheoryofHorncanbeusedtoformalizeandinterpretsuchsemanticspecifications.Forexample,considerthefollowingnaturalsemanticsspecificationofaconditionalexpressionforafunctionalprogramminglanguage:BtrueMVBfalseNV(ifBMN)V(ifBMN)VThesetwoinferencefigurescanalsobeseenastwofirst-orderHornclauses:BMNV[BtrueMV(ifBMN)V]BMNV[BfalseNV(ifBMN)V]Here,thedownarrowisanon-logical,predicatesymbolandanexpressionsuchasNVisanatomicformula.?AnearlierdraftofthispaperappearedinMERLIN2001[Mil01].