10.48456/TR-860
Loesch, Steffen
Steffen
Loesch
Program equivalence in functional metaprogramming via nominal Scott domains
Computer Laboratory, University of Cambridge
2014
technical report
164 pages
PDF
A prominent feature of metaprogramming is to write algorithms in one programming language (the meta-language) over structures that represent the programs of another programming language (the object-language). Whenever the object-language has binding constructs (and most programming languages do), we run into tedious issues concerning the semantically correct manipulation of binders.
In this thesis we study a semantic framework in which these issues can be dealt with automatically by the meta-language. Our framework takes the user-friendly ‘nominal’ approach to metaprogramming in which bound objects are named.
Specifically, we develop mathematical tools for giving logical proofs that two metaprograms (of our framework) are equivalent. We consider two programs to be equivalent if they always give the same observable results when they are run as part of any larger codebase. This notion of program equivalence, called contextual equivalence, is examined for an extension of Plotkin’s archetypal functional programming language PCF with nominal constructs for metaprogramming, called PNA. Historically, PCF and its denotational semantics based on Scott domains were hugely influential in the study of contextual equivalence. We mirror Plotkin’s classical results with PNA and a denotational semantics based on a variant of Scott domains that is modelled within the logic of nominal sets. In particular, we prove the following full abstraction result: two PNA programs are contextually equivalent 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 new programming language constructs to PNA, one for existential quantification over names and one for ‘definite description’ over names. Adding only one of them is insufficient, as we give proofs that full abstraction fails if either is left out.