Quelle  root.tex

\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{a4wide}
\usepackage{amssymb}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\newcommand{\isasymnotsqsubseteq}{\isamath{\not\sqsubseteq}}
\renewcommand{\isacharminus}{\mbox{--}}

% Bibliography
\usepackage{natbib}
\bibpunct();A{},

% sane default for proof documents
\parindent 0pt

\begin{document}

\title{Logical Relations for PCF}
\author{Peter Gammie}
\maketitle

\begin{abstract}
  We apply Andy Pitts's methods of defining relations over domains to
  several classical results in the literature. We show that the Y
  combinator coincides with the domain-theoretic fixpoint operator,
  that parallel-or and the Plotkin existential are not definable in
  PCF, that the continuation semantics for PCF coincides with the
  direct semantics, and that our domain-theoretic semantics for PCF is
  adequate for reasoning about contextual equivalence in an
  operational semantics. Our version of PCF is untyped and has both
  strict and non-strict function abstractions. The development is
  carried out in HOLCF.
\end{abstract}

\tableofcontents

\parskip 0.5ex

\section{Introduction}

\label{sec:introduction}

Showing the existence of relations on domains has historically been an
involved process. This is due to the presence of the contravariant
function space domain constructor that defeats familiar inductive
constructions; in particular we wish to define ``logical'' relations,
where related functions take related arguments to related results, and
the corresponding relation transformers are not monotonic.  Before
\citet{PittsAM:relpod} such demonstrations involved laborious appeals
to the details of the domain constructions themselves. (See
\citet{Mulmuley:1987,Stoy:1977} for historical perspective.)

Here we develop some standard results about PCF using Pitts's
technique for showing the existence of particular recursively-defined
relations on domains. By doing so we demonstrate that HOLCF
\citep{HOLCF:1999,holcf11} is useful for reasoning about programming
language semantics and not just particular programs.

We treat a variant of the PCF language due to \citet{Plotkin77}. It
contains both call-by-name and call-by-value abstractions and is
untyped. We show the breadth of Pitts's technique by compiling several
results, some of which have only been shown in simply-typed settings
where the existence of the logical relations is straightforward to
demonstrate.

% generated text of all theories
\input{session}

\section{Concluding remarks}

We have seen that Pitts's techniques for showing the existence of
relations over domains is straightforward to mechanise and use in
HOLCF.

One source of irritation in doing so is that Pitts's technique is
formulated in terms of minimal invariants, which presently must be
written out by hand. (Earlier versions of HOLCF's domain package
provided these copy functions, though we would still need to provide
our own in such cases as \S\ref{sec:continuations}.) HOLCF~'11
provides us with take functions (approximations, deflations) on
domains that compose, and so one might hope to adapt Pitts's technique
to use these instead. This has been investigated by
\citet[\S6]{DBLP:conf/ppdp/BentonKBH09}, but it is unclear that the
deflations involved are those generated by HOLCF~'11.

\bibliographystyle{plainnat}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: