A Semantic Model for GUI Programs

Our paper on ultrametric semantics will appear at LICS 2011!

We've got a new draft, too, on applying this to GUI programming. This turns out to be not entirely straightforward, since GUI widgets accept user input, and so the semantics of a GUI has to model that input. The usual way of modelling input is via a reader monad -- that is, we model computations as functions which accept input as an argument -- but in a GUI you can (for instance) write programs which dynamically create new buttons, and so create new input channels.

The thing we did -- which seems obvious to me, but which Nick says is unusual, and for which I would like references -- was to view things like buttons as giving you a set of values. Then you can say that creating a button is an operation in the nondeterminism monad (basically). Then you don't need to model state at all.

Since this is notionally a research blog, let me point out a bit of mathematics I really liked in this paper (not actually due to me). Since we were working in ultrametric spaces, we couldn't use powersets, obviously -- we needed power spaces. It turns out that the right notion of powerspace for a space $X$ is the collection of closed subsets of $X$, under the Hausdorff metric. Then when $X$ is a complete 1-bounded ultrametric space, then $\mathcal{P}(X)$ will be too.

This is all totally standard, but one thing that wasn't obvious to me is whether powerspace actually forms a monad! The multiplication for powerset (in sets) is $\mu : \mathcal{P}^2(A) \to \mathcal{P}(A) = \fun{U}{\{a \in A \;|\; \exists X \in U.\; a \in X\}}$ -- that is, $\mu(U) = \cup U$.

Since only finite unions of closed sets are closed, for powerspace the corresponding multiplication ought to be $\mu(U) = \mathrm{cl}(\cup U)$. However, it wasn't obvious to me whether this was a nonexpansive map or not. I learned the following super-slick proof from a paper of Steve Vickers, "Localic Completion of Generalized Metric Spaces II: Powerlocales". Despite the formidable title, it is a very readable paper.

Below is just the fragment of the proof for the lower half of the Hausdorff metric.

$$
\begin{array}{lcl}
d(U, V) \leq q & \iff & \forall X \in U, \exists Y \in V.\; d(X, Y) < q \\
& \iff & \forall X \in U, \exists Y \in V.\; \forall x \in X, \exists y \in Y.\; d(x,y) \leq q \\
& \Longrightarrow & \forall X \in U, \forall x \in X.\; \exists Y \in V, \exists y \in Y.\; d(x,y) \leq q \\
& \iff & \forall x \in \cup X, \exists y \in \cup V, d(x,y) \leq q \\
& \iff & d(\cup U, \cup V) \leq q \\
& \iff & d(\mathrm{cl}(\cup U), \mathrm{cl}(\cup V)) \leq q \\
& \iff & d(\mu(U), \mu(V)) \leq q \\
\end{array}
$$

That quantifier flip is clever, but what makes this proof beautiful to me is introducing the auxilliary $q$. My own attempts just drowned in quantifier alternations, but this splits things up at just the right point. I'm reminded of Dijkstra's observation that most mathematicians do not make enough use of logical equivalence in their proofs, and clearly I fall into this category.

Ultrametric Semantics of Reactive Programs

I've got a new draft paper out with Nick Benton, Ultrametric Semantics of Reactive Programs.

We answer some longstanding open questions in FRP, namely:

1. What are higher-order reactive functions at all? How do you interpret them, and what are their semantics?
2. How can we implement FRP in a reasonable way, without compromising on either the equational theory or the ability to fit into the mutable callback event loop world of MVC?

It's got a little something for everyone -- some very pretty proof theory, some nice denotational semantics, and a hardcore separation logic proof with a step-indexed logical relation.

Research notes

I think I will keep some research notes online. I've tried installing MathJax, so this should not be too unreadable, either. Let me begin with the typing of the simply typed lambda calculus, as is traditional.
\[
\begin{array}{lcl}
A & ::= & 1 \bnfalt A \times B \bnfalt A \to B \\
e & ::= & () \bnfalt (e,e) \bnfalt \fst{e} \bnfalt \snd{e} \\
& | & x \bnfalt e\;e' \bnfalt \fun{x:A}{e}
\end{array}
\]

\[
\begin{array}{ll}
\rule{x:A \in \Gamma}
{\judge{\Gamma}{x}{A}} &
\rule{ }
{\judge{\Gamma}{()}{1}}
\\
& \\
\rule{\judge{\Gamma,x:A}{e}{B}}
{\judge{\Gamma}{\fun{x:A}{e}}{A \to B}} &
\rule{\judge{\Gamma}{e}{A \to B} & \judge{\Gamma}{e'}{A}}
{\judge{\Gamma}{e\;e'}{B}}
\\
& \\
\rule{\judge{\Gamma}{e}{A} & \judge{\Gamma}{e'}{B}}
{\judge{\Gamma}{(e,e')}{A \times B}}
\\
& \\
\rule{\judge{\Gamma}{e}{A \times B}}
{\judge{\Gamma}{\fst{e}}{A}} &
\rule{\judge{\Gamma}{e}{A \times B}}
{\judge{\Gamma}{\snd{e}}{B}}
\end{array}
\]