Document Type
Report
Date
10-1993
Keywords
Programming, Semantics, Algol-like languages, Local state, Logical relations, Parametric polymorphism
Language
English
Disciplines
Computer Sciences
Description/Abstract
We propose that the phenomenon of local state may be understood in terms of Strachey's concept of parametric (i.e., uniform) polymorphism. The intuitive basis for our proposal is the following analogy: a non-local procedure is independent of locally-declared variables in the same way that a parametrically polymorphic function is independent of types to which it is instantiated. A connection between parametricity and representational abstraction was first suggested by J. C. Reynolds. Reynolds used logical relations to formalize this connection in languages with type variables and user-defined types. We use relational parametricity to construct a model for an Algol-like language in which interactions between local and non-local entities satisfy certain relational criteria. Reasoning about local variables essentially involves proving properties of polymorphic functions. The new model supports straightforward validations of all the test equivalences that have been proposed in the literature for local-variable semantics, and encompasses standard methods of reasoning about data representations. It is not known whether our techniques yield fully abstract semantics. A model based on partial equivalence relations on the natural numbers is also briefly examined.
Recommended Citation
O'Hearn, Peter W. and Tennent, R. D., "Parametricity and Local Variables" (1993). Electrical Engineering and Computer Science - Technical Reports. 158.
https://surface.syr.edu/eecs_techreports/158
Source
local
Additional Information
School of Computer and Information Science, Syracuse University, SU-CIS-93-30
Authors later published: P. W. O'Hearn and R. D. Tennent. 1995. Parametricity and local variables. J. ACM 42, 3 (May 1995), 658-709. DOI=10.1145/210346.210425 http://doi.acm.org/10.1145/210346.210425 .