Denotational Semantics with Nominal Scott Domains
When defining computations over syntax as data, one often runs into
tedious issues concerning α-equivalence and semantically correct
manipulations of binding constructs. Here we study a semantic
framework in which these issues can be dealt with automatically by the
programming language. We take the user-friendly "nominal" approach in
which bound objects are named. In particular, we develop a version of
Scott domains within nominal sets and define two programming languages
whose denotational semantics are based on those domains. The first
language, nuPCF, is an extension of Plotkin's PCF with names that can
be swapped, tested for equality and locally scoped; although simple,
it already exposes most of the semantic subtleties of our
approach. The second language, PNA, extends the first with name
abstraction and concretion so that it can be used for metaprogramming
over syntax with binders.
For both languages, we prove a full abstraction result for nominal
Scott domains analogous to Plotkin's classic result about PCF and
conventional Scott domains: two program phrases have the same
observable operational behaviour in all contexts if and only if they
denote equal elements of the nominal Scott domain model. This is the
first full abstraction result we know of for languages combining
higher-order functions with some form of locally scoped names which
uses a domain theory based on ordinary extensional functions, rather
than using the more intensional approach of game semantics.
To obtain full abstraction, we need to add two functionals, one for
existential quantification over names and one for "definite
description" over names. Only adding one of them is not enough, as we
give counter examples to full abstraction in both cases.
Last modified: Tue Apr 22 14:23:47 BST 2014