Department of Computer Science and Technology

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}
}