Open AccessNames, Equations, Relations: Practical Ways to Reason about 'new'
Author(s) -
Ian Stark
Publication year - 1996
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v3i31.21675
Subject(s) - mathematical proof , equivalence (formal languages) , calculus (dental) , representation (politics) , observational equivalence , computer science , simple (philosophy) , algebra over a field , mathematics , discrete mathematics , pure mathematics , theoretical computer science , epistemology , law , philosophy , medicine , geometry , dentistry , politics , political science
The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state in the form of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between names and functions, the language can capture notions of scope, visibility and sharing. Originally motivated by the study of references in Standard ML, the nu-calculus has connections to other kinds of local declaration, and to the mobile processes of the pi-calculus. This paper introduces a logic of equations and relations which allows one to reason about expressions of the nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs of contextual equivalence (also known as observational, or observable, equivalence). The logic is based on earlier operational techniques, providing the same power but in a much more accessible form. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names. See the revised version BRICS-RS-97-39.