10 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

A Proof Theory for Generic Judgments: An extended abstract

-

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
10 pages
English

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

Informations

Publié par
Nombre de lectures 10
Langue English

Exrait

A Proof Theory for Generic Judgments: An extended abstract
Dale Miller ´ INRIA/Futurs/Saclay & Ecole polytechnique dale.miller@inria.fr
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 tiu@cse.psu.edu
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 ofon 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 ofon the left from the premise 0 , B[t/x]−→C, wheretis some term. To reduce the rank of the cut formulax.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