LISP and Symbolic Computation, 9(1)77-107
Categorical Models for Local NamesIan Stark, University of Cambridge Computer Laboratory, Pembroke Street, Cambridge CB2 3QG, England
|
Abstract: This paper describes the construction of categorical
models of the nu-calculus, a language that combines higherorder
functions with dynamically created names. Names are created with local
scope, they can be compared with each other and passed around through
function application, but that is all. The intent behind this language is to examine one aspect of the imperative character of Standard ML: the use of local state by dynamic creation of references. The nu-calculus is equivalent to a certain fragment of ML, omitting side effects, exceptions, datatypes and recursion. Even without all these features, the interaction of name creation with higher-order functions can be complex and subtle; it is particularly difficult to characterise the observable behaviour of expressions. Categorical monads, in the style of Moggi, are used to build denotational models for the nu-calculus. An intermediate stage is the use of a computational metalanguage, which distinguishes in the type system between values and computations. The general requirements for a categorical model are presented, and two specific examples described in detail. These provide a sound denotational semantics for the nu-calculus, and can be used to reason about observable equivalence in the language. In particular a model using logical relations is fully abstract for first-order expressions. Keywords: lambda-calculus, functional programming, dynamic allocation, category theory, monads |
[local copy]