A Proof Theory for Generic Judgments: An extended abstract

Description

Niveau: Supérieur
A Proof Theory for Generic Judgments: An extended abstract Dale Miller INRIA/Futurs/Saclay & Ecole polytechnique Alwen Tiu Ecole polytechnique & Penn State University Abstract A powerful and declarative means of specifying com- putations containing abstractions involves meta-level, uni- versally quantified generic judgments. We present a proof theory for such judgments in which signatures are associ- ated to each sequent (used to account for eigenvariables of the sequent) and to each formula in the sequent (used to account for generic variables locally scoped over the for- mula). A new quantifier, ?, is introduced to explicitly ma- nipulate the local signature. Intuitionistic logic extended with ? satisfies cut-elimination even when the logic is ad- ditionally strengthened with a proof theoretic notion of defi- nitions. The resulting logic can be used to encode naturally a number of examples involving name abstractions, and we illustrate using the pi-calculus and the encoding of object- level provability. Keywords: proof search, reasoning about operational se- mantics, generic judgments, higher-order abstract syntax. 1. Eigenvariables and generic reasoning In specifying and reasoning about computations involv- ing abstractions, one needs to encode both the static struc- ture of such abstractions and their dynamic structure during computation.

• variable can


• also say


• denote judgments


• signature de ?


• local signatures


• provable using definition


• scope


• introduction rules


• free proof


• logical constants

Sujets

• Documents
• Education
• Etudes supérieures
• Miller
• École polytechnique
• Universidad Estatal de Pensilvania
• Logical constant

Informations

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

Exrait

A Proof Theory for Generic Judgments: An extended abstract

Dale Miller ´ INRIA/Futurs/Saclay & Ecole polytechnique [e-mail]

Abstract

A powerful and declarative means of specifying com putations containing abstractions involves metalevel, uni versally quantifiedgeneric judgments. We present a proof theory for such judgments in which signatures are associ ated to each sequent (used to account for eigenvariables of the sequent) and to each formula in the sequent (used to account for generic variables locally scoped over the for mula). A new quantifier,r, is introduced to explicitly ma nipulate the local signature. Intuitionistic logic extended withrsatisfies cutelimination even when the logic is ad ditionally strengthened with a proof theoretic notion of defi nitions. The resulting logic can be used to encode naturally a number of examples involving name abstractions, and we illustrate using theπcalculus and the encoding of object level provability.

Keywords:proof search, reasoning about operational se mantics, generic judgments, higherorder abstract syntax.

1. Eigenvariables and generic reasoning

In specifying and reasoning about computations involv ing abstractions, one needs to encode both the static struc ture of such abstractions and their dynamic structure during computation. One successful approach to such an encod ing, generally calledhigherorder abstract syntax[22], uses λterms to encode the static structure of abstractions and universally quantified judgments to encode their dynamic structure. There are, of course, several ways to prove a univer sally quantified expression,∀ γ x.Bapproach that can. An be called theextensional, attempts to proveB[t/x]for all (closed) termstof typeγ. This rule might involve an in finite number of premises if the domain of the typeγis infinite. If the typeγis defined inductively, a proof byin ductioncan replace the need for infinite premises with finite premises (thebasecases andinductivecases) but with the

Alwen Tiu ´ Ecole polytechnique & Penn State University [e-mail]

need to discover invariants. Another moreintensionalap proach, however, involves introducing a new, generic vari able, say,c:γ, that has not been introduced before in the proof, and to prove the formulaB[c/x]naturalinstead. In deduction and sequent calculus proofs, such new variables are calledeigenvariables. In Gentzen’s original presentation of the sequent cal culus [5], eigenvariables were immutable: reading proofs bottomup, once an eigenvariable is introduced it is not used as a site for substitution. In other words, Gentzen’s eigen variables did not vary in proof construction: rather they acted more as fresh, scoped constants. The generic interpretation of quantifiers generally entails the extensional interpretation: this is a simple consequence of the cutelimination theorem as follows. Assume that the sequent−→ ∀x.Bis proved using the introduction of∀ on the right from the premise−→B[c/x], wherecis an eigenvariable and(c)is a proof of this premise. Sim 0 ilarly, assume that the sequent,∀xB−→Cis proved using the introduction of∀on the left from the premise 0 , B[t/x]−→C, wheretis some term. To reduce the rank of the cut formula∀x.Bbetween the sequents−→ ∀x.B 0 and,∀xB−→C, the eigenvariablecin the sequent cal culus proof(c)must be substituted bytto yield a proof (t)of−→B[t/x]: in this way, the cutformula is now the smaller formulaB[t/x]Gentzen, this role of. In cin (c)as a site for substitution only takes place in the meta theory of proofs and not in proofs themselves. Recent years have witnessed two different developments in the role of eigenvariables in the specification of compu tation systems.

Eigenvariables as fresh, scoped constantsFocusing on theirintensionalnature and guarantee of newness or fresh ness in proof search, eigenvariables have been used to en code name restrictions in theπcalculus [15], nonces in se curity protocols [1], reference locations in imperative pro gramming [2, 16], and constructors hidden within abstract datatypes [12]. Eigenvariables also provide an essential