Technical reports
Program equivalence in functional metaprogramming via nominal Scott domains
Steffen Loesch
October 2014, 164 pages
This technical report is based on a dissertation submitted May 2014 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Trinity College.
DOI: 10.48456/tr-860
Abstract
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.
Full text
PDF (1.5 MB)
BibTeX record
@TechReport{UCAM-CL-TR-860, author = {Loesch, Steffen}, title = {{Program equivalence in functional metaprogramming via nominal Scott domains}}, year = 2014, month = oct, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-860.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-860}, number = {UCAM-CL-TR-860} }