Foundational Aspects of Syntax

Description

Niveau: Supérieur, Doctorat, Bac+8
Foundational Aspects of Syntax 1 Dale Miller and Catuscia Palamidessi Department of Computer Science and Engineering The Pennsylvania State University 220 Pond Laboratory University Park, PA 16802-6106 USA Phone: [phone], FAX: [phone] , Introduction A large variety of computing systems, such as compilers, interpreters, static analyzers, and theorem provers, need to manipulate syntactic objects like pro- grams, types, formulas, and proofs. A common characteristic of these syntactic objects is that they contain variable binders, such as quantifiers, scoping opera- tors, and parameters. The presence of binders complicates formal specifications and symbolic processing. Consider, for example, a function definition of the form f(x) = let y = e in x+ y. When analyzing or transforming a program containing the call f(e?), we might wish to replace f(e?) with the body of f in which x is substituted by e?. But we cannot simply apply the substitution [x 7? e?] because a free variable could be captured. For example, if e? is the expression y, naive substitution would yield the expression (let y = e in y + y), which is incorrect. Binders are often treated in traditional specifications by adding side condi- tions on variables.

• full ?-conversion


• formed using


• bound variable


• using ?-abstraction


• conversion


• syntactic objects


• such side


• dependent typed


• specification over

Sujets

• Pennsylvania State University
• Wegner
• Free variables and bound variables
• Conversión

Informations

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

Extrait

1 Foundational Aspects of Syntax

Dale Miller and Catuscia Palamidessi Department of Computer Science and Engineering The Pennsylvania State University 220 Pond Laboratory University Park, PA 16802-6106 USA Phone: [phone], FAX: [phone] [e-mail], [e-mail] http://www.cse.psu.edu/~dale http://www.cse.psu.edu/~catuscia

Introduction

A large variety of computing systems, such as compilers, interpreters, static analyzers, and theorem provers, need to manipulate syntactic objects like pro- grams, types, formulas, and proofs. A common characteristic of these syntactic objects is that they contain variable binders, such as quantiers, scoping opera- tors, and parameters. The presence of binders complicates formal specications and symbolic processing. Consider, for example, a function denition of the form

f(x) = lety=einx+y.

0 When analyzing or transforming a program containing the callf(e), we might 0 0 wish to replacef(e) with the body offin whichxis substituted bye. But we 0 cannot simply apply the substitution [x7→e] because a free variable could be 0 captured. For example, ifeis the expressiony, naive substitution would yield the expression (lety=einy+y), which is incorrect. Binders are often treated in traditional specications by adding side condi- tions on variables. Consider, for example, the following (late semantics) rule of theπ-calculus [MPW92], expressing how bound input propagates in a context of parallel processes:

x(y) 0 P−−→P x(y) 0 P|Q−−→P|Q

y∈/freevar(Q).

0 Here, the scope of the binding foryis intended to be overPsideonly. The condition is necessary to avoid capturing possibly free occurrences ofyinQ. 1 To appear in theACM Computing Surveys Symposium on Theoretical Computer Science: A Perspective, edited by Pierpaolo Degano, Roberto Gorrieri, Alberto Marchetti-Spaccamela, and Peter Wegner, March or June 1999.

1