# Towards Patterns for Heaps and Imperative Lambdas
to appear in Elsevier JLAMP, DOI: 10.1016/j.jlamp.2015.10.008
©2015 This manuscript version is made available under the CC-BY-NC-ND 4.0
license.

David A. Naumann  Stevens Institute of Technology, USA

###### Abstract

In functional programming, point-free relation calculi have been fruitful for
general theories of program construction, but for specific applications
pointwise expressions can be more convenient and comprehensible. In imperative
programming, refinement calculi have been tied to pointwise expression in
terms of state variables, with the curious exception of the ubiquitous but
invisible heap. To integrate pointwise with point-free, de Moor and Gibbons
[12] extended lambda calculus with non-injective pattern matching interpreted
using relations. This article gives a semantics of that language using “ideal
relations” between partial orders, and a second semantics using predicate
transformers. The second semantics is motivated by its potential use with
separation algebra, for pattern matching in programs acting on the heap. Laws
including lax beta and eta are proved in these models and a number of open
problems are posed.

Dedicated to José Nuno Oliveira on the occasion of his 60th birthday.

##  1 Introduction

An important idea in the mathematics of program construction is to embed the
programming language of interest into a richer language with additional
features that are useful for writing specifications and for reasoning.
Functional programs can be embedded in the calculus of relations, which
provides two key benefits: converse functions as specifications and
intersection of specifications. An example of the first benefit is parsing.
Let $show:Tree\mathbin{\longrightarrow}String$ be the function that maps an
ordered tree with strings at its leaves to the “inorder” catenation of the
leaves. Its converse, $show^{o}$, is a relation but not a function. One seeks
to derive, by algebraic reasoning in the calculus of relations, a total
function $\mathit{parse}$ such that
$show^{o}\mathrel{\supseteq}\mathit{parse}$. See Bird and de Moor [2] for many
more examples. Imperative programs can be embedded in a refinement calculus
[9, 23], by augmenting the language with assumptions and angelic choice, or
“specification statements” in some other form. These can be modeled using
weakest precondition predicate transformers. An imperative program $prog$
satisfies specification $spec$ just if $spec\mathrel{\sqsubseteq}prog$ where
$\mathrel{\sqsubseteq}$ is the pointwise order on predicate transformers, and
again one seeks to derive $prog$ from $spec$.

Many authors have pointed out useful and elegant aspects of the calculus of
relations for programming. Relations cater for the development of general
theory by facilitating a “point free” style in which algebraic calculation is
not encumbered by manipulation of bound variables and substitutions (e.g., see
[31]).

Although pointfree style is elegant and effective for development of general
theory, it can be awkward and cryptic for developing and expressing specific
algorthms. Functional programmers tend to prefer a mix of pointfree and
pointwise expressions, “pointwise” meaning the use of variables and other
expressions that denote data elements —application rather than composition.
Pointwise reasoning involves logical quantifiers and is the norm in imperative
program construction. For example, refinement laws for assignment statements
involve conditions on free variables, and specifications are expressed in
terms of state variables and formulas with quantifiers.

Conventional pattern matching can help raise the abstraction level in
pointwise programs, by directly expressing data structure of interest. Non-
injective patterns have been proposed by de Moor and Gibbons [12] as a way to
achieve pointwise programming with relations. Imperative programmers draw
graphs to express patterns of pointer structure, but their programs are
written in impoverished notation that amounts to little more than load and
store instructions.

This article contributes to the long term goal of a unified theory of
programming in which one may move freely between pointwise or pointfree
reasoning as suits the occasion. For example, requirements might be formalized
in a transparent pointwise specification that is then transformed to a
pointfree equivalent from which an efficient solution is derived by algebraic
calculation. A unified theory will also enable effective mixes of functional,
imperative, and other styles both in program structure and in reasoning.

This article describes one approach to a programming calculus integrating
functional and imperative styles, addressing some aspects of pointwise and
pointfree reasoning. Some of the technical results were published in a
conference paper by the author [29], from which much of the material is
adapted. The introductory sections have been rewritten using different
examples. This article provides full details of the main semantic definitions
and some results only mentioned sketchily in the conference paper, namely beta
and eta laws. We cannot expect beta and eta equalities to hold unrestrictedly,
as they fail already in by-value functional languages. Inequational laws are
mentioned but not proved in [12] and [29]. Here we prove weak beta and eta
laws for both relational and predicate transformer semantics. We also pose
several open problems.

### Outline

The rest of this article is organized as follows. Section 2 begins with
motivation, focusing on higher types and the idea of non-injective patterns.
We show by example how non-injective patterns could be used in imperative
programming including pointer programs. This idea helps motivate the predicate
transformer semantics but is not otherwise developed in this article. Section
2 also surveys related work on alternate approaches to programming calculi
integrating pointwise with pointfree and functional with imperative styles.

Section 3 reviews the standard semantics of simply typed lambda calculus in a
cartesian closed category, in particular Poset. Section 4 describes the
category of ideal relations, motivated by difficulties with semantics in [12].
Section 5 gives our relational semantics. Section 6 gives a simulation
connecting relational and functional semantics, and proves the lax beta and
eta laws that are our main results for relational semantics. Section 7 gives
the predicate transformer model and semantics. Section 8 proves the main
results for transformer semantics. Section 9 assesses the work and discusses
open problems.

For Section 3 onwards, the reader should be familiar with predicate
transformer semantics [9] and with basic category theory including adjunctions
and cartesian closure [15]. Span constructions and lax adjunctions are only
mentioned in passing, and “laxity” appears only as an informal term that
indicates the weakening of equations to inequations.

##  2 Motivation and background

### Motivation

One attraction of pointfree style is that it facilitates derivation of
programs that are “polytypic”, i.e., generic in some sense with respect to
type constructors [4]. For example, a polynomial functor on a category of data
types may have a fixpoint; its values are trees of some form determined by the
particular functor. If the element type has a well ordering, one can define
the function $repmin$ that sends tree $t$ to the tree $t^{\prime}$ of the same
shape but where each leaf of $t^{\prime}$ is the minimum of the leaves of $t$.
De Moor gives a pointfree derivation of $repmin$, at this level of generality,
using type constructions and equational laws that can be interpreted in
functions or in relations [10].

Relations can model demonic nondeterminacy [12] or angelic nondeterminacy (as
in automata theory and in logic programming), but not both —unless states or
data values are replaced by richer structures such as predicates. The present
author showed that the algebraic structure needed for the polytypic $repmin$
derivation exists in the setting of monotonic predicate transformers [26].

Although the $repmin$ problem only involves first order data (trees with
primitive, ordered data), the derived solution involves higher order: It
traverses the input tree to build a closure that, when applied to a value,
builds a tree of the same shape with that value at its leaves. This brings us
to a question about how to embed a programming language in a richer calculus
for specification and derivation. In the language of categories, taking data
types as objects and programs as arrows, the question is what objects to use
for arrow types. For each pair $B,C$ of objects, a function space
$B\mathbin{\Rightarrow}C$ exists as an object in the category Rel of binary
relations, and indeed as an object in the category of monotonic predicate
transformers. But $B\mathbin{\Rightarrow}C$ is not the “internal hom” or
exponent in Rel. There should be some account of what it means to reason with
exponents in Rel if the derived program is interpreted as a functional one.

Pointfree reasoning is not without its shortcomings. De Moor and Gibbons
observe that for many specific programming problems a pointwise formulation is
easier to understand. They extend pointwise functional notation to relations
by means of non-injective patterns. As a simple example, the following is
intended to define a relation that performs an arbitrary rotation of a list:

$rotate(x\mathbin{\mbox{\small$+\\!\\!+$}}y)=y\mathbin{\mbox{\small$+\\!\\!+$}}x$
(1)

An input list $w$ relates to all $y\mathbin{\mbox{\small$+\\!\\!+$}}x$ such
that $w=x\mathbin{\mbox{\small$+\\!\\!+$}}y$. Let us consider in detail how a
pattern term gives rise to a relation from a set $in$ of inputs to a set $out$
of outputs. The pattern is an expression with free variables $vars$ that are
also free in the result expression. The situation looks like this:

$\begin{diagram}$

As indicated by the dotted arrow, the semantics of the pattern term is the
composition $pattern^{o}\mathbin{\mbox{\small{;}}}expr$. Throughout this
article, $(\mathbin{\mbox{\small{;}}})$ denotes forwards relational
composition.

This way of obtaining relations is connected to one systematic approach to
embedding programs in richer calculi. A span in a category is a pair of arrows
with common source, like $pattern$ and $expr$ above. The category Rel is
equivalent to the category whose arrows are spans over the category Fun of
sets and functions. We refrain from elaborating on the construction but note
that there are several variations, one of which is a lax span construction
that not only gives Rel from Fun but also monotonic predicate transformers
from Rel [14, 27].

Let us connect spans with familiar elements of imperative programming.
Consider the humble assignment $x:=x+1$. To specify it, beginners often write
$x=x+1$ as postcondition, but only miraculous or divergent programs establish
postcondition $\mathit{false}$. What is needed is an auxiliary variable
(“logical constant”) $u$, used in the specification

$pre:\quad x=u\qquad post:\quad x=u+1$

This is interpreted by $u$ being universally quantified over $pre$ and $post$,
one instance being the useful one that makes $u$ serve to name the initial
value of $x$. Imperative specification notations often feature notation for
the special case where the auxiliary is merely equated with an initial value,
but the general form is needed, for example to obtain complete laws for
sequential composition of specifications [23]. The general form comprises
$pre$ and $post$ that are relations between the program state and auxiliary
state.

$\begin{diagram}$ (2)

The leftward dotted arrow indicates that imperative programs in refinement
calculus can be modeled by predicate transformers, i.e., from postconditions
to preconditions. Still more, the category of monotonic predicate transformers
is equivalent to the lax span category over Rel [14].

One way to view (2) is that one agent (the angel) chooses the auxiliary value
for which the other agent (the demonic program) chooses an output. Indeed,
non-injective patterns can express nondeterministic choice, e.g., the choice
between functions $f$ and $g$ can be written as $h$ where
$h(\mathit{fst}(x,y))=f\,x~{}\mbox{if}~{}y~{}\mbox{else}~{}g\,x$. Here
$\mathit{fst}$ is the left projection from $A\times\mathit{bool}$ where $A$ is
the input type of $f$ and $g$. In predicate transformer semantics this choice
turns out to be angelic, which is consistent with the standard semantics,
using $\exists$, of logical constants [23].

### Prior work on the approach explored here

Although the lax span perspective provides an elegant connection between Fun,
Rel, and predicate transformers, it does not directly account for exponents in
these categories. Because we are interested in refinement —an order relation
on arrows— the exponents, as internal homs, should reflect the ordering. This
led to the investigation of how, by starting from Poset instead of Fun, one
obtains a more robust category of “ideal” relations and then a category
—called Tran in the sequel— of monotonic predicate transformers where
predicates themselves are monotonic [27]. One step towards a programming
calculus based on Tran is to show [28] that (lax) polynomial functors have
unique fixpoints; the lax exponent serves to derive a variation on Lawvere’s
parameterized recursion theorem. Further steps are taken in [26] which adds
the pointfree theory of containers/membership [16] and uses that, together
with the recursion theorem, to recreate a derivation of de Moor’s [10]
pointfree $repmin$ solution at the level of Tran. What is still not achieved
after all these years is to derive a solution that uses shared pointer
structure: updating all leaves of the tree to point to a single cell that is
updated with the minimum of the tree, once that has been determined.

### Towards refinement calculus for pointer programs

Extant refinement calculi for imperative programming do not address pointer
programs except by explicit encodings of the heap using arrays. For _post hoc_
program verification there has been a great deal of progress using separation
logic.111A recent reference that emphasizes separation algebra is the book by
Appel et al [1]. The assertion language features the separating conjunction,
$*$, and assertions are often in the form of a top level separation
$P*Q*\ldots*R$ that expresses some way of partitioning heap cells into
disjoint sets that satisfy the predicates $P,Q,\ldots$. Informally, the sets
are referred to as “footprints” of predicates. Some static analysis tools use
separated conjunctions as “symbolic heaps” in symbolic execution. Underlying
the semantics of the assertion language is a notion of separation algebra,
whose expressions denote (partial) heaps and whose operations manipulate
heaps. However, for reasoning about programs, separation logic distinguishes
programs from specifications rather than embedding one in the other as in
refinement calculus. And reasoning must be done in terms of assertions; put
differently, in terms of expressions only of type ‘proposition’.

One of the challenges in reasoning about pointer programs is to describe
structural invariants such as reachability, uniqueness of references,
separation, and confinement. Separation facilitates reasoning about
independence of writes, i.e., frame conditions. This is embodied in the frame
rule of separation logic:

$\mbox{from}\quad\\{P\\}\,cmd\,\\{Q\\}\quad\mbox{infer}\quad\\{P*R\\}\,cmd\,\\{Q*R\\}\;.$
(3)

This is sound because the footprint of precondition $P$ serves as frame
condition for the command: the antecedent implies that $cmd$ does not write
outside that part of the heap. The precondition $P*R$ says that $R$ is true of
a disjoint set of heap cells, so it cannot be falsified by writes to the cells
that support $P$.

By contrast with separation, confinement facilitates reasoning about
independence of reads. One application is in reasoning about simulations
between data representations: Confinement helps ensure that the behavior of a
client of an abstract data type is independent from the internal
representation because the client has no pointer into the representation.
Wang, Barbosa, and Oliveira [32] extend separation logic with connectives that
express confinement. For example, $P\neg\\!\triangleright Q$ says that not
only are the footprints of $P$ and $Q$ disjoint but no cell in the footprint
of $P$ has a pointer to a cell in the footprint of $Q$. This is an elegant
advance on works which use ad hoc means to express confinement (e.g., [5, 6]).
Dang and Möller [11] take further steps in this direction.

Another challenge in reasoning about pointer programs is that programming
languages are impoverished in their means to express heap operations —it
amounts to little more than load and store instructions. Separation logic was
a huge advance in reasoning about such programs, which involves assertions
about many intermediate states in which interesting invariants are temporarily
broken. Informally, what works effectively is diagrams.

Consider, for example, an iterative algorithm that reverses, _in situ_ , an
acyclic doubly linked list. The algorithm uses pointer variable $p$ pointing
to the reversed segment and $n$ that points to the first node of the segment
that remains to be reversed. The loop body makes three heap updates and moves
$p$ and $n$ forward, transforming the left-hand situation into the right-hand
one.

Each rectangle represents a cell with two pointers, which in a high level
language could be fields named $next$ (upper box) and $prev$ (lower) for the
forward and backward pointers. Here is another diagram that depicts the
transformation.222Diagrams can mislead, of course. In the general case, the
rightmost and leftmost pointers, in and out of the clouds that indicates the
rest of the heap, may not exist.

Dashed arrows indicate the final state. Slashed circles indicate values in the
initial state that get updated. For example, the left cell’s $prev$ is
initially nil and the right cell’s $prev$ gets set to nil.

The following notional code is a tail-recursive procedure $rev1$ that uses
pattern matching to perform the transformation in a single step.

$\begin{array}[]{lcl@{\hspace*{.7em}}l@{}l@{}l@{}l@{}l}rev1\ p\ n\
heap&\mathord{=}&\mathbf{match}\ heap\hfil\hskip
6.99997pt&\\!\\!\mathbf{with}\\\ &&\mid\hfil\hskip
6.99997pt&p\stackrel{{\scriptstyle.}}{{\mapsto}}q,\mathbf{nil}&\mathrel{\>*\>}&\lx@intercol
n\stackrel{{\scriptstyle.}}{{\mapsto}}\mathbf{nil},\mathbf{nil}\quad\mbox{\Large$\mathbf{\mathrel{\mapsto}}$}\hfil\lx@intercol\\\
&&\hfil\hskip
6.99997pt&p\stackrel{{\scriptstyle.}}{{\mapsto}}q,n&\mathrel{\>*\>}&n\stackrel{{\scriptstyle.}}{{\mapsto}}p,\mathbf{nil}\\\
&&\mid\hfil\hskip
6.99997pt&p\stackrel{{\scriptstyle.}}{{\mapsto}}q,{\color[rgb]{1,0,0}\mathbf{nil}}&\mathrel{\;*\;}&n\stackrel{{\scriptstyle.}}{{\mapsto}}{\color[rgb]{1,0,0}r},\mathbf{nil}&\mathrel{\;*\;}&r\stackrel{{\scriptstyle.}}{{\mapsto}}s,{\color[rgb]{1,0,0}n}\quad\;\mbox{\Large$\mathbf{\mathrel{\mapsto}}$}\\\
&&\quad\>rev1\ n\ r\ (\\!\\!\\!\\!\hfil\hskip
6.99997pt&p\stackrel{{\scriptstyle.}}{{\mapsto}}q,{\color[rgb]{0,0,1}n}&\mathrel{\;*\;}&n\stackrel{{\scriptstyle.}}{{\mapsto}}{\color[rgb]{0,0,1}p},\mathbf{nil}&\mathrel{\;*\;}&r\stackrel{{\scriptstyle.}}{{\mapsto}}s,{\color[rgb]{0,0,1}\mathbf{nil}}\;)\end{array}$

The second pattern clause matches the diagram. (The first clause handles the
situation where $n$ points to the last node.) As usual in pattern matching,
free variables on the left of the pattern arrow $\mathbf{\mathrel{\mapsto}}$
are bound by the match. That is indicated in the diagram by labels $q,r,s$.

The notation is adapted from separation logic and from OCaml. The difference
from OCaml’s match construct is the big arrow $\mathbf{\mathrel{\mapsto}}$
chosen to fit with other notations in this article. The expression
$x\stackrel{{\scriptstyle.}}{{\mapsto}}y,z$ is inspired by the points-to
predicate in separation logic. It denotes a heap with a single cell,
referenced by $x$, with $y,z$ as the values of the $next$ and $prev$ fields.
Think of the heap as a mapping from references to pairs, so
$x\stackrel{{\scriptstyle.}}{{\mapsto}}y,z$ simply denotes a singleton
mapping. Infix $*$ denotes the partial function that forms the union of two
heaps, provided their domains are disjoint, and is undefined otherwise. Comma,
for pairing, binds tighter than $\stackrel{{\scriptstyle.}}{{\mapsto}},$ which
in turn binds tighter than $*$.

The initial call to $rev1$ should be $rev1\ root\ n\ heap$ where $root$ points
to the first node and $n$ is that node’s $next$ (its $prev$ being
$\mathbf{nil}$).

One wishful feature of the code for $rev1$ is that the patterns are local, in
the sense that they describe only the relevant cells. Given that the heap is
an explicit argument and return value, perhaps the pattern should match the
entire heap. To see how that might look, consider the following putative
definition of $reverse$, which makes the top level call to $rev1$ for lists of
plural length.

$\begin{array}[]{lcl}reverse\ \mathbf{nil}\ hp&=&hp\\\ reverse\ p\
(p\stackrel{{\scriptstyle.}}{{\mapsto}}\mathbf{nil},\mathbf{nil}\mathrel{\>*\>}hp)&=&(p\stackrel{{\scriptstyle.}}{{\mapsto}}\mathbf{nil},\mathbf{nil}\mathrel{\>*\>}hp)\\\
reverse\ p\
(p\stackrel{{\scriptstyle.}}{{\mapsto}}n,\mathbf{nil}\mathrel{\>*\>}hp)&=&rev1\
p\ n\
(p\stackrel{{\scriptstyle.}}{{\mapsto}}n,\mathbf{nil}\mathrel{\>*\>}hp)\end{array}$

It would be nicer for $hp$ to be implicit, by analogy with the frame rule (3).
An obvious approach would be to use a state monad. Another possibility is to
find algebraic notation and laws whereby a whole-heap operation can be derived
from one written using a local-heap pattern term. Laws are also needed to
transform heap patterns into some restricted form that can be automatically
compiled to code.

In separation algebra the heap union operator, $*$, is partial. For example,
$x\stackrel{{\scriptstyle.}}{{\mapsto}}y,z*x\stackrel{{\scriptstyle.}}{{\mapsto}}u,w$
is not defined. Our wishful pattern notation needs to be interpreted in a
setting that admits patterns that are non-total as well as non-injective. The
calculus of de Moor and Gibbons allows general relations in patterns —but
there are unsettled issues concerning refinement monotonicity at higher types,
as discussed in Section 4. In our relational model, the issues are addressed
by restricting pattern terms to total functions. The predicate transformer
model supports relational pattern terms.

### Related work on other approaches

It does not appear that the specific calculus of de Moor and Gibbons has been
developed beyond the original paper [12].

Hinze makes nice use of explicit powersets as a way to do pointwise relational
programming [17].

Bunkenburg [8] develops a calculus of “expression refinement”, for derivation
of lazy functional programs including those that use the state monad. Ordering
is taken into account by treating data types as ordered sets. Nondeterministic
expressions are interpreted as monotonic functions
$f:A\mathbin{\longrightarrow}{\mathcal{U}}B$ where ${\mathcal{U}}B$ is the set
of updeals (upward closed subsets) on $B$. The set ${\mathcal{U}}B$ is ordered
by $\mathrel{\supseteq}$, which coincides with the Smyth order (total
correctness) restricted to upward closed sets. Upward closure is natural for
outcomes of expressions. Monotonic functions
$f:A\mathbin{\longrightarrow}{\mathcal{U}}B$ are naturally isomorphic to
ideals, as is discussed in Section 4. So there is some overlap with the
present work, although our language (and [12]) is by-value. Bunkenburg
develops a wide spectrum language and a logic of refinement, but the language
does not include pattern matching.

Uses of angelic and demonic nondeterminacy are explored by Back and von Wright
[9] and by Morris and Tyrrell [24]. Martin, Curtis, and Rewitzky [21] use
multi-valued relations as an alternative to predicate transformers for
modelling the combination of angelic and demonic nondeterminacy, and adapt
map/fold algebra to that model [20].

Morris, Bunkenberg, and Tyrrell [19] introduce a novel “phrase” construct, and
“term transformer” semantics, as a technique for specifying and reasoning
about imperative programs; it generalizes predicate transformers to terms of
any type. Their approach encompasses unbounded angelic and demonic
nondeterminacy together with higher order functions, for which Morris and
Tyrrell present numerous laws [24]. They sketch how non-injective patterns may
be reduced to nondeterminacy. They have beta-reduction as an equality, unlike
our results in the sequel, owing to partitioning terms as proper or not, and
use of a semantic monotonicity restriction. Morris and Tyrrell have also shown
equivalence between monotonic predicate transformers, multirelations, and free
completely distributive lattices [25]. The phrase construct is very appealing
but quite different from the functional notations explored in this article,
and from conventional notations of refinement calculi.

For first order concurrent programs, concurrent Kleene algebra provides a
pointfree algebraic setting for reasoning about separation, mutable state and
concurrency (e.g., [18]). Modal Kleene algebra is the basis for the extended
separation logic of Dang and Möller [11], which they use to verify algorithms
including list reversal and tree rotation, expressed in terms of load and
store commands. Banerjee et al [7] use explicit expressions to designate
footprints of pointer structures, but only for _post hoc_ verification.

##  3 Functional semantics

This section reviews the categorical semantics of simply-typed lambda calculus
in the order-enriched category Poset of monotonic functions on (small) posets.

An order-enriched category is one with homsets partially ordered and
composition monotonic. Each homset $\mbox{{Poset}}(B,C)$ carries the pointwise
ordering $f\preceq g\mathrel{\equiv}(\forall\,b\,.\,fb\preceq_{C}gb)$.
Composition of $f\in\mbox{{Poset}}(B,C)$ with $h\in\mbox{{Poset}}(C,D)$,
written $(f\mathbin{\mbox{\small{;}}}h)$ as with relations in general, is
monotonic in both $f$ and $h$. We write $\times$ for binary product and
$\langle f,g\rangle:B\mathbin{\longrightarrow}C\times D$ for pairing of
$f:B\mathbin{\longrightarrow}C$ with $g:B\mathbin{\longrightarrow}D$. For
projection we write $\pi$ with subscripts or some other indication of which
projection is meant. We write $B\mathbin{\Rightarrow}C$ for function space as
an exponent object of Poset, ordered pointwise. Let $\mathbin{\Rightarrow}$
bind less tightly than $\times$. The application function is denoted by
$\mathsf{ap_{f}}:(B\mathbin{\Rightarrow}C)\times B\mathbin{\longrightarrow}C$
and currying sends $f:B\times C\mathbin{\longrightarrow}D$ to
$\mathsf{cur_{f}}f:B\mathbin{\longrightarrow}C\mathbin{\Rightarrow}D$. The
decorative subscript “f” distinguishes the functional constructs from those
for ideals (i) and predicate transformers (t) to come.

###### Proposition 1

Poset is cartesian closed and the adjunctions
$(B\times)\dashv(\mathbin{\Rightarrow}B)$ are order-enriched.

Order enrichment, in the context of Proposition 1, simply means that pairing,
currying, and the exponent and product functors are monotonic.

The functional terms $M$ are those of simply-typed lambda calculus. Types are
given by

$\sigma::=b\mid\mathbf{1}\mid\sigma\times\sigma\mid\sigma\rightarrow\sigma$
(4)

where $b$ ranges over some given set of base types. Terms are generated from
given constants $c$ and variables $x$:

$M::=x\mid c\mid\mathit{fst}\mid snd\mid\langle M,M\rangle\mid MM\mid\lambda
x.M$ (5)

Typing judgements take the form $\Gamma{\mathrel{\;\vdash}\;}M:\sigma$ where
$\Gamma$ is a list $x_{0}:\sigma_{0},\ldots,x_{n}:\sigma_{n}$ of variable
typings. The typing rules are standard and omitted [15]. We allow constants at
all types. The type of a constant is assumed given.

We write ${\mathcal{F}}{[\\![}\mbox{-}{]\\!]}$ for the functional semantics,
but omit ${\mathcal{F}}$ in this section. Functional semantics is based on a
given poset ${[\\![}b{]\\!]}$ for each base type $b$. Given a singleton set
${[\\![}\mathbf{1}{]\\!]}$ as well, the semantics of types is given
inductively by
${[\\![}\sigma\times\sigma^{\prime}{]\\!]}={[\\![}\sigma{]\\!]}\times{[\\![}\sigma^{\prime}{]\\!]}$
and
${[\\![}\sigma\rightarrow\sigma^{\prime}{]\\!]}={[\\![}\sigma{]\\!]}\mathbin{\Rightarrow}{[\\![}\sigma^{\prime}{]\\!]}$.
For $\Gamma=x_{0}:\sigma_{0},\ldots,x_{n}:\sigma_{n}$, we write
${[\\![}\Gamma{]\\!]}$ for the product
$(\ldots(({[\\![}\mathbf{1}{]\\!]}\times{[\\![}\sigma_{0}{]\\!]})\times{[\\![}\sigma_{1}{]\\!]})\times\ldots{[\\![}\sigma_{n}{]\\!]})$.
For terms, we assume that for each constant $c:\sigma$ a function
${[\\![}c{]\\!]}:{[\\![}\mathbf{1}{]\\!]}\mathbin{\longrightarrow}{[\\![}\sigma{]\\!]}$
is given, and let
${[\\![}\mathit{fst}{]\\!]}:{[\\![}\mathbf{1}{]\\!]}\mathbin{\longrightarrow}{[\\![}\sigma\times\sigma^{\prime}\rightarrow\sigma{]\\!]}$
pick out the left projection function (as an element of the set
${[\\![}\sigma\times\sigma^{\prime}\rightarrow\sigma{]\\!]}$). The semantics
of $\Gamma{\mathrel{\;\vdash}\;}M:\sigma$ is a morphism
${[\\![}\Gamma{\mathrel{\;\vdash}\;}M:\sigma{]\\!]}:{[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{[\\![}\sigma{]\\!]}$,
defined in a standard way in Table 1.333See, for example, [15]. Our
formulations use only binary products. The “appropriate projection” for
$x_{k}$ is the evident morphism
${[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{[\\![}\sigma_{k}{]\\!]}$
defined using binary projections and pairing.

Table 1: The functional semantics ${\mathcal{F}}{[\\![}\mbox{-}{]\\!]}$, given
functions
${[\\![}c:\sigma{]\\!]}:\mathbf{1}\mathbin{\longrightarrow}{\mathcal{F}}{[\\![}\sigma{]\\!]}$.
$\begin{array}[]{lcl}{[\\![}\Gamma{\mathrel{\;\vdash}\;}x:\sigma{]\\!]}&=&\pi\quad\mbox{where
$\pi$ is the appropriate projection}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}c:\sigma{]\\!]}&=&\pi\mathbin{\mbox{\small{;}}}{[\\![}c:\sigma{]\\!]}\quad\mbox{where
$\pi$ is the projection
${[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{[\\![}\mathbf{1}{]\\!]}$}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}\langle
M,M^{\prime}\rangle:\sigma\times\sigma^{\prime}{]\\!]}&=&\langle{[\\![}\Gamma{\mathrel{\;\vdash}\;}M:\sigma{]\\!]},{[\\![}\Gamma{\mathrel{\;\vdash}\;}M^{\prime}:\sigma^{\prime}{]\\!]}\rangle\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}MM^{\prime}:\sigma{]\\!]}&=&\langle{[\\![}\Gamma{\mathrel{\;\vdash}\;}M:\sigma^{\prime}\rightarrow\sigma{]\\!]},{[\\![}\Gamma{\mathrel{\;\vdash}\;}M^{\prime}:\sigma^{\prime}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathsf{ap_{f}}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.M:\sigma\rightarrow\sigma^{\prime}{]\\!]}&=&\mathsf{cur_{f}}{[\\![}\Gamma,x:\sigma{\mathrel{\;\vdash}\;}M:\sigma^{\prime}{]\\!]}\end{array}$

##  4 Ideals

This section motivates and defines the category Idl of ideal relations,
starting from a sketch of difficulties that arise in the work of De Moor and
Gibbons [12] using the category Rel of relations on sets. We describe the
embedding of Poset in Idl, the power adjunction which gives an embedding the
other way around, and the lax cartesian closed structure used in Section 5 for
semantics. Results that are not proved here can be found in [27] or [29].

The relational semantics of [12] interprets arrow types using the set
$A\mathbin{\leadsto}B$ of relations from $A$ to $B$. For relation $R:B\times
C\mathbin{\longrightarrow}D$ the pre-curried relation
$cur~{}R:B\mathbin{\longrightarrow}C\mathbin{\leadsto}D$ is defined by

$b(cur~{}R)S\;\mathrel{\equiv}\;(\forall\,c,d\,.\,cSd\equiv(b,c)Rd)$ (6)

But $cur$ is not monotonic with respect to $\mathrel{\supseteq}$, and
monotonicity with respect to refinement is crucial for a useful calculus and
for recursion. De Moor and Gibbons address monotonicity by replacing
$\mathrel{\supseteq}$ with a refinement order defined by $R\preceq
R^{\prime}\;\mathrel{\equiv}\;R\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\supseteq$}}\mathrel{\,\supseteq\,}R^{\prime}$
for $R,R^{\prime}$ of type $B\mathbin{\longrightarrow}C\mathbin{\leadsto}D$.
(Small font is used when order relations are composed.) In terms of points:
$R\preceq R^{\prime}$ iff for all $b,S$, $bR^{\prime}S$ implies there is
$S^{\prime}$ with $bRS^{\prime}$ and $S^{\prime}\mathrel{\supseteq}S$. At
higher types, refinement is defined inductively:

$R\preceq
R^{\prime}\;\mathrel{\equiv}\;R\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\preceq$}}\mathrel{\,\supseteq\,}R^{\prime}$
(7)

where the small  $\preceq$ is the refinement order on the target type. Observe
that $\preceq$ reduces to $\mathrel{\supseteq}$ for relations such that
$R\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\preceq$}}=R$. The ordering has
a problem: $(Q\mathbin{\mbox{\small{;}}}R)$ fails to be monotonic in $Q$,
e.g., if $R:C\mathbin{\leadsto}D\mathbin{\longrightarrow}C\mathbin{\leadsto}D$
sends a relation to its complement. Our solution is to rule out
complementation on grounds of non-monotonicity. A function
$f:B\mathbin{\longrightarrow}C$ is monotonic iff
$f\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\preceq$}}_{C}\mathrel{\supseteq}\vbox{\hbox{\tiny$\preceq$}}_{B}\mathbin{\mbox{\small{;}}}f$.
Let us say a relation is monotonic iff
$R\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\preceq$}}\mathrel{\,\supseteq\,}\vbox{\hbox{\tiny$\preceq$}}\mathbin{\mbox{\small{;}}}R$.
It is straightforward to show that $(\mathbin{\mbox{\small{;}}})$ is
monotonic, w.r.t. $\preceq$ of (7), when restricted to monotonic
relations.444The symbols $\mathrel{\subseteq}$ and $\mathrel{\supseteq}$
always have their usual set-theoretic meaning, whereas $\preceq$ is used
generically for orderings. We write $id$ only for identity functions, writing
either $\mathsf{id}$ _sans serif_ or $\preceq$ for the identity in Idl,
depending on which seems most perspicuous.

If $R$ is monotonic then so is
$R\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\preceq$}}$. A relation is
monotonic and satisfies
$R\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\preceq$}}=R$ iff it is an
ideal. An ideal is a relation $R:A\mathbin{\longrightarrow}B$ such that

$\vbox{\hbox{\tiny$\preceq$}}_{A}\mathbin{\mbox{\small{;}}}R\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\preceq$}}_{B}\quad\mathrel{\mathrel{\subseteq}}\quad
R$

In terms of points: $a^{\prime}\preceq a$, $aRb$, and $b\preceq b^{\prime}$
imply $a^{\prime}Rb^{\prime}$.

Ideals are the morphisms of the order-enriched category Idl whose objects are
all (small) posets. Composition $(\mathbin{\mbox{\small{;}}})$ in Idl is the
same as in Rel, but the identity on $A$, written $\mathsf{id}$, is
$\preceq_{A}$. Homsets are ordered by $\mathrel{\supseteq}$, not
$\mathrel{\subseteq}$, for reasons mentioned later.

### Ideals, power adjunction, and products

A comap in an order-enriched category is an arrow $g$ with a corresponding map
or left adjoint $g^{*}$. That is, $g$ and $g^{*}$ satisfy

$\mathsf{id}\preceq g^{*}\mathbin{\mbox{\small{;}}}g\quad\mbox{and}\quad
g\mathbin{\mbox{\small{;}}}g^{*}\preceq\mathsf{id}$ (8)

It is common to order Rel by $\mathrel{\subseteq}$ and describe Fun as the
subcategory of maps of Rel; then the comap of a function $f$ is its converse
$f^{o}$. Maps in order-enriched category C are the comaps of the arrow-dual
$\mbox{{C}}^{op}$ and they are also comaps in the order-dual $\mbox{{C}}^{co}$
obtained by reversing the order on homsets. As Rel is isomorphic to both
$\mbox{{Rel}}^{op}$ and $\mbox{{Rel}}^{co}$, one has several opportunities for
making infelicitous choices of nomenclature. Our choices smooth some parts of
the exposition, but have the unfortunate consequence that functions embed as
comaps in Idl. The reader should keep in mind that, in this article, the
operation ∗ gives the map for a comap, rather than the reverse. For example,
in Idl we have the shunting property

$c\mathbin{\mbox{\small{;}}}R\mathrel{\supseteq}S\quad\mbox{iff}\quad
R\mathrel{\supseteq}c^{*}\mathbin{\mbox{\small{;}}}S\quad\mbox{ for comap }c$
(9)

which is a standard consequence of (8), instantiating $\preceq$ with the order
$\mathrel{\supseteq}$ on homsets of Idl.

Because functions are a special case of relations, Fun is included in Rel. But
monotonic functions are not a special case of ideal relations. If $f$ is in
$\mbox{{Poset}}(A,B)$ and $R$ is in $\mbox{{Idl}}(B,C)$ then
$(f\mathbin{\mbox{\small{;}}}R)$ is in $\mbox{{Idl}}(A,C)$. As a consequence,
there is a graph functor $\mathord{\sf
Gr}:\mbox{{Poset}}\mathbin{\longrightarrow}\mbox{{Idl}}$ defined by
$\mathord{\sf Gr}f=(f\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\preceq$}})$
and $\mathord{\sf Gr}A=A$. We can sometimes elide $\mathord{\sf Gr}$ because

$\mathord{\sf
Gr}f\mathbin{\mbox{\small{;}}}R=f\mathbin{\mbox{\small{;}}}R\quad\mbox{for
ideal $R$}.$ (10)

The graph functor is an order injection on homsets, because the pointwise
ordering of functions $f\preceq g$ is equivalent to the inclusion
$(f\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\preceq$}})\mathrel{\supseteq}(g\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\preceq$}})$.

An unfortunate feature of Idl as compared with Rel is that the converse of an
ideal $R:B\mathbin{\longrightarrow}C$ need not be an ideal of type
$C\mathbin{\longrightarrow}B$ unless $B$ and $C$ are discretely ordered. Note
that $R^{o}:\widetilde{C}\mathbin{\longrightarrow}\widetilde{B}$ is an ideal,
where $\widetilde{B}$ is the order dual of $B$, i.e.,
$\preceq_{\widetilde{B}}$ is $(\preceq_{B})^{o}$.

More importantly, for $f:B\mathbin{\longrightarrow}C$ in Poset,
$(\vbox{\hbox{\tiny$\preceq$}}\mathbin{\mbox{\small{;}}}f^{o}):C\mathbin{\longrightarrow}B$
is an ideal; in fact it is the left adjoint of $\mathord{\sf Gr}f$. The
opgraph functor $\mathord{\sf Rg}$ is defined as

$\mathsf{Rg}:\mbox{{Poset}}^{co\,op}\mathbin{\longrightarrow}\mbox{{Idl}}\qquad\mathsf{Rg}\,f=(\mathord{\sf
Gr}f)^{*}$

So we have $\mathsf{id}\mathrel{\supseteq}\mathord{\sf
Rg}\,f\mathbin{\mbox{\small{;}}}\mathord{\sf Gr}\,f$ and $\mathord{\sf
Gr}\,f\mathbin{\mbox{\small{;}}}\mathord{\sf
Rg}\,f\mathrel{\supseteq}\mathsf{id}$.

A functor $G$ on order-enriched categories is an embedding if it is an order
injection on homsets, i.e., $f\preceq h\mathrel{\equiv}Gf\preceq Gh$ for all
$f,h$, and it is bijective on objects.

###### Proposition 2

$\mathord{\sf Gr}$ embeds Poset onto the comaps of Idl.

Recall from Section 2 that ${\mathcal{U}}B$ is the set of updeals, i.e.,
upward closed subsets, of $B$, ordered by $\mathrel{\supseteq}$. We use the
power adjunction [13] to characterize updeal lattices ${\mathcal{U}}B$ in Idl.
The converse $\mathord{\ni}$ of the membership relation is an ideal
${\mathcal{U}}B\mathbin{\longrightarrow}B$; note that
$(\mathord{\ni}\mathbin{\mbox{\small{;}}}\vbox{\hbox{\tiny$\preceq$}}_{B})\mathrel{\subseteq}\mathop{\mathord{\ni}}$
says that ${\mathcal{U}}B$ contains only updeals. For $R$ in
$\mbox{{Idl}}(B,C)$, the function $\Lambda
R:B\mathbin{\longrightarrow}{\mathcal{U}}C$ sends $b$ to its direct image
through $R$ (i.e., the set of $c$ such that $bRc$). The monotonic functor
${\mathcal{U}}:\mbox{{Idl}}\mathbin{\longrightarrow}\mbox{{Poset}}$ is defined
on morphisms by
${\mathcal{U}}R=\Lambda(\mathord{\ni}\mathbin{\mbox{\small{;}}}R)$.

###### Proposition 3

$f=\Lambda R\mathrel{\equiv}f\mathbin{\mbox{\small{;}}}\mathord{\ni}=R$, for
all $R,S$ in Idl and $f$ in Poset. This is order-enriched:
$R\mathrel{\supseteq}S\mathrel{\equiv}\Lambda R\preceq\Lambda S$, where
$\preceq$ is the pointwise order on functions, lifted from the order
$\mathrel{\supseteq}$ on ${\mathcal{U}}C$. Furthermore, ${\mathcal{U}}$ is an
embedding of Idl in Poset, and $\mathord{\sf Gr}$ is left adjoint to
${\mathcal{U}}$ with counit $\mathord{\ni}$ and unit the upward closure. This
is order enriched: $f\preceq g\mathrel{\equiv}\mathord{\sf
Gr}f\mathrel{\supseteq}\mathord{\sf Gr}g$.

Owing to our choice of ordering on Idl, the power adjunction is order-enriched
(by contrast with [2]), and covariantly so (by contrast with [27]).

For the product $A\times B$ of posets, the projection function $\pi$ in
$\mbox{{Poset}}(A\times B,A)$ gives a comap $\mathord{\sf Gr}\pi$ in
$\mbox{{Idl}}(A\times B,A)$. We overload notation and write $\langle
R,S\rangle:D\mathbin{\longrightarrow}A\times B$ for the pairing of
$R:D\mathbin{\longrightarrow}A$ with $S:D\mathbin{\longrightarrow}B$, which is
defined by $d\langle R,S\rangle(a,b)\mathrel{\equiv}dRa\land dSb$ just as in
Rel. Clearly $\langle\mathord{\sf Gr}f,\mathord{\sf Gr}g\rangle=\mathord{\sf
Gr}\langle f,g\rangle$. Defining $Q\times R$ as usual makes $\times$ an
extension of the product functor on Poset in the sense that $\mathord{\sf
Gr}f\times\mathord{\sf Gr}g=\mathord{\sf Gr}(f\times g)$.

###### Proposition 4

$\times$ is a monotonic bifunctor on Idl and

$\displaystyle R$ $\displaystyle\mathrel{\supseteq}$ $\displaystyle\langle
R,S\rangle\mathbin{\mbox{\small{;}}}\mathord{\sf Gr}\pi\quad(=,\mbox{ if $S$
is a comap})$ (11) $\displaystyle S$ $\displaystyle\mathrel{\supseteq}$
$\displaystyle\langle R,S\rangle\mathbin{\mbox{\small{;}}}\mathord{\sf
Gr}\pi^{\prime}\quad(=,\mbox{ if $R$ is a comap})$ (12) $\displaystyle\langle
R\mathbin{\mbox{\small{;}}}\mathord{\sf
Gr}\pi\,,\,R\mathbin{\mbox{\small{;}}}\mathord{\sf Gr}\pi^{\prime}\rangle$
$\displaystyle\mathrel{\supseteq}$ $\displaystyle R\quad(=,\mbox{ if $R$
comap})$ (13)

Here $\pi$ and $\pi^{\prime}$ are the left and right projections. We let
composition $(\mathbin{\mbox{\small{;}}})$ bind more tightly than the pairing
comma, as in these laws used later:555In the categorical lingo, $\times$ is
locally right adjoint to the diagonal
$\Delta:\mbox{{Idl}}\mathbin{\longrightarrow}\mbox{{Idl}}^{2}$. It is an
adjunction on comaps and (by general abstract nonsense [22]) it is the unique
(up to isomorphism) local right adjoint to the diagonal that is an adjunction
on comaps. In this article we consider lax exponents of relations and lax
products/exponents for predicate transformers. Each can be characterized up to
isomorphism by inequations (conditional in some cases) together with equations
conditioned on certain morphisms being maps, comaps, or both (see [27]). In
this article we need properties of the structures but not their uniqueness.

$\displaystyle\langle
R\mathbin{\mbox{\small{;}}}S\,,\,R\mathbin{\mbox{\small{;}}}U\rangle$
$\displaystyle\mathrel{\supseteq}$ $\displaystyle
R\mathbin{\mbox{\small{;}}}\langle S,U\rangle\quad(=,\mbox{ if $R$ comap})$
(14) $\displaystyle\langle R,S\rangle\mathbin{\mbox{\small{;}}}(U\times V)$
$\displaystyle=$ $\displaystyle\langle
R\mathbin{\mbox{\small{;}}}U\,,\,S\mathbin{\mbox{\small{;}}}V\rangle$ (15)

### Relation space

In the same way that $\times$ extends to a functor on Idl, the sum and
function-space constructs can be extended. But the function space is not an
internal hom of Idl, which is what we need to interpret a lambda calculus. We
now construct currying and application for the exponent defined by
$B\mathbin{\leadsto}C=\mbox{{Idl}}(B,C)$. The impatient reader may care to
skip to Prop. 5 which summarizes what is needed in the sequel.

In Rel, an exponent is given by the adjunctions $(\times B)\dashv(B\times)$.
Although $\times$ does not have this property in Idl, there is a related
functor denoted by $\ltimes$ that gives $(\times B)\dashv(B\ltimes)$ in Idl.
Formally, this gives an interpretation of lambda terms, but a strange one
because it does not extend $\mathbin{\Rightarrow}$. We use $\ltimes$ only as a
stepping stone. The currying operation $\mathsf{cur_{x}}$ associated with
$(\times B)\dashv(B\times)$ has the effect of shifting one coordinate. It is
defined for $R\in\mbox{{Rel}}(A\times B,C)$ just like (6), that is:

$a(\mathsf{cur_{x}}R)(b,c)\mathrel{\equiv}(a,b)Rc$ (16)

This defines $\mathsf{cur_{x}}R$ as a relation in $\mbox{{Rel}}(A,B\times C)$
but it need not be an ideal even if $R$ is, because the pointwise order on
$B\times C$ is incompatible with $R$ being downward closed in $B$. So we
define $B\ltimes C$ to be the poset $\widetilde{B}\times C$, i.e., the set
$B\times C$ but with the left-contravariant order ${\preceq_{B\ltimes
C}}={(\succeq_{B}\times\preceq_{C})}$. Now $\mathsf{cur_{x}}R$ defined by (16)
is an ideal if $R$ is. The application ideal
$\mathsf{ap_{x}}:(B\mathbin{\ltimes}C)\times B\mathbin{\longrightarrow}C$ has
$((b,c),b^{\prime})\,\mathsf{ap_{x}}\,c^{\prime}\mathrel{\equiv}b\succeq_{B}b^{\prime}\land
c\preceq_{C}c^{\prime}$. It is straightforward to prove that
$\mathsf{cur_{x}}$ is monotonic, and that it has an inverse. For each $B$, the
functor $(B\ltimes)$ is right adjoint to $(\times B)$.

By analogy with relations as subsets of a cartesian product, we define
$\mathbin{\leadsto}$ by

$B\mathbin{\leadsto}C={\mathcal{U}}(B\mathbin{\ltimes}C)$ (17)

An upward closed subset of $B\mathbin{\ltimes}C$ is, by definition of the
order, an ideal, so $B\mathbin{\leadsto}C$ is another name for the poset
$\mbox{{Idl}}(B,C)$. For ideals $R:B\times C\mathbin{\longrightarrow}D$ and
$S:B\mathbin{\longrightarrow}C\mathbin{\leadsto}D$ we define
$\mathsf{cur_{i}}R:B\mathbin{\longrightarrow}C\mathbin{\leadsto}D$ and
$\mathsf{uncur_{i}}S:B\times C\mathbin{\longrightarrow}D$ by

$\mathsf{cur_{i}}R=\mathord{\sf
Gr}(\mathord{{\Lambda}}(\mathsf{cur_{x}}R))\qquad\quad\mathsf{uncur_{i}}S=\mathsf{uncur_{x}}(S\mathbin{\mbox{\small{;}}}\mathord{\ni})$

Observe that $\mathord{{\Lambda}}(\mathsf{cur_{x}}R)$ is the monotonic
function sending $b\in B$ to the updeal $\\{(c,d)\mid(b,c)Rd\\}$, which is
essentially “$R$ curried on $b$” (cf. (6)). Monotonicity here means that
$b\preceq b^{\prime}$ implies
$\mathord{{\Lambda}}(\mathsf{cur_{x}}R)b\mathrel{\,\supseteq\,}\mathord{{\Lambda}}(\mathsf{cur_{x}}R)b^{\prime}$.

By definition of $\mathord{\sf Gr}$ and the ordering $\mathrel{\supseteq}$ on
$C\mathbin{\leadsto}D$, an element $b$ is related by $\mathsf{cur_{i}}R$ to
all ideals contained in $\\{(c,d)\mid(b,c)Rd\\}$. Clearly $\mathsf{cur_{i}}R$
is monotonic in $R$, as $\mathord{{\Lambda}}$ and $\mathsf{cur_{x}}$ are
monotonic. A crucial fact about $\mathsf{cur_{i}}R$ is that it is a comap, for
any $R$. This follows by definition of $\mathsf{cur_{i}}$ and Prop. 2. We also
have $\mathsf{uncur_{i}}(\mathsf{cur_{i}}R)=R$ by a straightforward
calculation using power and $\ltimes$ adjunctions. For
$\mathsf{cur_{i}}(\mathsf{uncur_{i}}S)$, however, unfolding the definitions
and using $\ltimes$ adjunction yields
$\mathsf{cur_{i}}(\mathsf{uncur_{i}}S)=\mathord{\sf
Gr}(\mathord{{\Lambda}}(S\mathbin{\mbox{\small{;}}}\mathord{\ni}))$ and then
power adjunction gives

$\mathsf{cur_{i}}(\mathsf{uncur_{i}}S)=S\quad\mbox{if $S$ is a comap}$ (18)

The condition is necessary; the range of $\mathsf{cur_{i}}$ is comaps so it is
not surjective. Unfolding the definitions at the level of points, we have
$(b,c)(\mathsf{uncur_{i}}S)d$ iff $(\exists\,R\,.\,bSR\land cRd)$, and thus
$b(\mathsf{cur_{i}}(\mathsf{uncur_{i}}S))U$ iff
$\\{(c,d)\mid(\exists\,R\,.\,bSR\land cRd)\\}\mathrel{\supseteq}U$. The
largest such $U$ is thus a “convexification” of $S$: For given $b$, one can
say that $S$ nondeterministically chooses a $V$ which for given $c$
nondeterministically chooses result $d$; whereas the largest $U$ above
combines all the nondeterministic outcomes of all $V$. So
$\mathsf{cur_{i}}(\mathsf{uncur_{i}}S)$ is $\mathord{\sf Gr}f$ for the
function $f$ such that $f~{}b$ is the convex closure of $S$ for $b$. From this
it is clear that

$\mathsf{cur_{i}}(\mathsf{uncur_{i}}S)\mathrel{\supseteq}S\quad\mbox{for all
}S$ (19)

Defining $\mathsf{ap_{i}}=\mathsf{uncur_{i}}\,\mathsf{id}$ makes
$\mathsf{ap_{i}}$ an ideal with $(R,b)\mathsf{ap_{i}}c\mathrel{\equiv}bRc$.
(It is not a comap.) Note that
$\mathsf{uncur_{i}}\,\mathsf{id}=\mathsf{uncur_{x}}\mathord{\ni}$ with
$\mathord{\ni}$ taken to be an ideal
$(B\mathbin{\leadsto}C)\mathbin{\longrightarrow}B\ltimes C$ (recall (17)).
Application extends that for functions, in the sense that

$(\mathord{\sf Gr}f,a)\mathsf{ap_{i}}\,b\quad\mbox{iff}\quad(f,a)(\mathord{\sf
Gr}\,\mathsf{ap_{f}})b\quad\mbox{iff}\quad fa\preceq b$

We have
$\mathsf{uncur_{i}}S=(S\times\mathsf{id})\mathbin{\mbox{\small{;}}}\mathsf{ap_{i}}$
(recall that $\mathsf{id}$ is $\preceq$). For $R:A\mathbin{\longrightarrow}B$
and $S:C\mathbin{\longrightarrow}D$, we define
$R\mathbin{\leadsto}S:B\mathbin{\leadsto}C\mathbin{\longrightarrow}A\mathbin{\leadsto}D$
by

$R\mathbin{\leadsto}S=\mathsf{cur_{i}}((\mathsf{id}_{B\mathbin{\leadsto}C}\times
R)\mathbin{\mbox{\small{;}}}\mathsf{ap_{i}}\mathbin{\mbox{\small{;}}}S)$

as usual. This extends $\mathbin{\Rightarrow}$ because
$U(R\mathbin{\leadsto}S)V\mathrel{\equiv}R\mathbin{\mbox{\small{;}}}U\mathbin{\mbox{\small{;}}}S\mathrel{\supseteq}V$.
Note that $R\mathbin{\leadsto}S$ is a comap for all $R,S$, because the range
of $\mathsf{cur_{i}}$ is comaps.

###### Proposition 5

$\mathbin{\leadsto}:\mbox{{Idl}}^{op}\times\mbox{{Idl}}\mathbin{\longrightarrow}\mbox{{Idl}}$
is a monotonic functor, and for all $R,S,U$

$\displaystyle\mathsf{cur_{i}}R\mbox{ is a comap}$ (20)
$\displaystyle(\mathsf{cur_{i}}R\times\mathsf{id})\mathbin{\mbox{\small{;}}}\mathsf{ap_{i}}$
$\displaystyle=$ $\displaystyle R$ (21)
$\displaystyle\mathsf{cur_{i}}((S\times\mathsf{id})\mathbin{\mbox{\small{;}}}\mathsf{ap_{i}})$
$\displaystyle\mathrel{\supseteq}$ $\displaystyle S\quad\mbox{($=$, if $S$
comap)}$ (22)
$\displaystyle\mathsf{cur_{i}}((R\times\mathsf{id})\mathbin{\mbox{\small{;}}}S)$
$\displaystyle\mathrel{\supseteq}$ $\displaystyle
R\mathbin{\mbox{\small{;}}}\mathsf{cur_{i}}S\;\mbox{($=$, if $R$ comap)}$ (23)
$\displaystyle\mathsf{cur_{i}}((\mathsf{id}\times
S)\mathbin{\mbox{\small{;}}}R\mathbin{\mbox{\small{;}}}U)$ $\displaystyle=$
$\displaystyle\mathsf{cur_{i}}R\mathbin{\mbox{\small{;}}}(S\mathbin{\leadsto}U)$
(24)

### Internalizations

To connect $B\mathbin{\Rightarrow}C$ with $B\mathbin{\leadsto}C$, we define
the ideal $\mathsf{gr}_{B,C}$ by

$\mathsf{gr}_{B,C}=\mathsf{cur_{i}}(\mathord{\sf
Gr}\,\mathsf{ap_{f}}):(B\mathbin{\Rightarrow}C)\mathbin{\longrightarrow}(B\mathbin{\leadsto}C)$

This makes $\mathsf{gr}_{B,C}$ the internalization of the action of
$\mathord{\sf Gr}$ on a homset: it relates each $f$ in
$B\mathbin{\Rightarrow}C$ to the set of ideals contained in $\mathord{\sf
Gr}f$. The following expresses how $\mathsf{cur_{i}}$ and $\mathsf{ap_{i}}$
extend their functional counterparts when applied to comaps.

$\mathsf{cur_{i}}(\mathord{\sf Gr}f)=\mathord{\sf
Gr}(\mathsf{cur_{f}}f)\mathbin{\mbox{\small{;}}}\mathsf{gr}\qquad\quad(\mathsf{gr}\times\mathsf{id})\mathbin{\mbox{\small{;}}}\mathsf{ap_{i}}=\mathord{\sf
Gr}\,\mathsf{ap_{f}}$ (25)

For any $B,C,D$, there is an ideal
$\mathsf{comp}:(B\mathbin{\leadsto}C)\times(C\mathbin{\leadsto}D)\mathbin{\longrightarrow}B\mathbin{\leadsto}D$
which internalizes composition. It is defined in a standard way using
$\mathsf{cur_{i}}$, $\mathsf{ap_{i}}$, and structural isomorphisms like
associativity for products (Prop. 1 and Prop. 2).

##  5 Relational semantics

The language of relational terms $N$ has the same types as before, see (4).
But in addition to functional constructs of (5) we add (demonic) choice
$\sqcap$ and patterns:

$N::=M\mid\langle N,N\rangle\mid NN\mid\lambda
x.N\mid\mathord{\raisebox{1.93747pt}{$\chi$}}x.M\mathrel{\mapsto}N\mid N\sqcap
N$

In a pattern matching abstraction
$\mathord{\raisebox{1.93747pt}{$\chi$}}x.M\mathrel{\mapsto}N$, pattern $M$ is
a functional term, not just constructors and variables —recall the rotate
example (1) in Section 1. The typing rules are

$\frac{\Gamma{\mathrel{\;\vdash}\;}N:\sigma\quad\Gamma{\mathrel{\;\vdash}\;}N^{\prime}:\sigma}{\Gamma{\mathrel{\;\vdash}\;}N\sqcap
N^{\prime}:\sigma}\qquad\frac{\Gamma,x:\sigma^{\prime\prime}{\mathrel{\;\vdash}\;}M:\sigma\quad\Gamma,x:\sigma^{\prime\prime}{\mathrel{\;\vdash}\;}N:\sigma^{\prime}}{\Gamma{\mathrel{\;\vdash}\;}\mathord{\raisebox{1.93747pt}{$\chi$}}x.M\mathrel{\mapsto}N:\sigma\rightarrow\sigma^{\prime}}\quad$

For a term $M$ of functional type, say $\sigma\rightarrow\sigma^{\prime}$, one
can think of the term
$\mathord{\raisebox{1.93747pt}{$\chi$}}x\,.\,Mx\mathrel{\mapsto}x:\sigma^{\prime}\rightarrow\sigma$
as the converse of $M$.

In this section we write ${[\\![}\mbox{-}{]\\!]}$ for the relational
interpretation ${\mathcal{R}}{[\\![}\mbox{-}{]\\!]}$. Types are interpreted as
before, except for using the relational constructs:
${[\\![}\sigma\times\sigma^{\prime}{]\\!]}={[\\![}\sigma{]\\!]}\times{[\\![}\sigma^{\prime}{]\\!]}$
and
${[\\![}\sigma\rightarrow\sigma^{\prime}{]\\!]}={[\\![}\sigma{]\\!]}\mathbin{\leadsto}{[\\![}\sigma^{\prime}{]\\!]}$.
We assume ${[\\![}b{]\\!]}={\mathcal{F}}{[\\![}b{]\\!]}$ for the base types,
hence if $\sigma$ is arrow-free then
${[\\![}\sigma{]\\!]}={\mathcal{F}}{[\\![}\sigma{]\\!]}$.

For $\Gamma=x_{0}:\sigma_{0},\ldots,x_{n}:\sigma_{n}$, the semantics of a
judgement $\Gamma{\mathrel{\;\vdash}\;}N:\sigma$ is an ideal
${[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{[\\![}\sigma{]\\!]}$ defined in
Table 2.

Table 2: The relational semantics ${\mathcal{R}}{[\\![}\mbox{-}{]\\!]}$, given
ideals
${[\\![}c:\sigma{]\\!]}:{[\\![}\mathbf{1}{]\\!]}\mathbin{\longrightarrow}{\mathcal{R}}{[\\![}\sigma{]\\!]}$.
$\begin{array}[]{lcl}{[\\![}\Gamma{\mathrel{\;\vdash}\;}x:\sigma{]\\!]}&=&\mathord{\sf
Gr}\pi\quad\mbox{where $\pi$ is the appropriate projection}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}c:\sigma{]\\!]}&=&\mathord{\sf
Gr}\pi\mathbin{\mbox{\small{;}}}{[\\![}c:\sigma{]\\!]}\mbox{ where $\pi$ is
the projection
${[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{[\\![}\mathbf{1}{]\\!]}$}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}\langle
N,N^{\prime}\rangle:\sigma\times\sigma^{\prime}{]\\!]}&=&\langle{[\\![}\Gamma{\mathrel{\;\vdash}\;}N:\sigma{]\\!]},{[\\![}\Gamma{\mathrel{\;\vdash}\;}N^{\prime}:\sigma^{\prime}{]\\!]}\rangle\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}NN^{\prime}:\sigma{]\\!]}&=&\langle{[\\![}\Gamma{\mathrel{\;\vdash}\;}N:\sigma^{\prime}\rightarrow\sigma{]\\!]},{[\\![}\Gamma{\mathrel{\;\vdash}\;}N^{\prime}:\sigma^{\prime}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathsf{ap_{i}}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.N:\sigma\rightarrow\sigma^{\prime}{]\\!]}&=&\mathsf{cur_{i}}{[\\![}\Gamma,x:\sigma{\mathrel{\;\vdash}\;}N:\sigma^{\prime}{]\\!]}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}\mathord{\raisebox{1.93747pt}{$\chi$}}x.M\mathrel{\mapsto}N:\sigma\rightarrow\sigma^{\prime}{]\\!]}&=&\\\
\lx@intercol\qquad\langle(\mathsf{sim}^{*}_{\Gamma}\mathbin{\mbox{\small{;}}}\mathord{\sf
Gr}({\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.M{]\\!]})\mathbin{\mbox{\small{;}}}\mathsf{rg}\mathbin{\mbox{\small{;}}}(\mathsf{sim}^{*}_{\sigma}\mathbin{\leadsto}\mathsf{sim}_{\sigma^{\prime\prime}}))\,,\,{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
<EMAIL_ADDRESS>{[\\![}\Gamma{\mathrel{\;\vdash}\;}N\sqcap
N^{\prime}:\sigma{]\\!]}&=&{[\\![}\Gamma{\mathrel{\;\vdash}\;}N:\sigma{]\\!]}\cup{[\\![}\Gamma{\mathrel{\;\vdash}\;}N^{\prime}:\sigma{]\\!]}\end{array}$

In addition to demonic choice, $\sqcap$, interpreted by union, one can add an
operation for conjunction of specifications, interpreted by intersection which
preserves the ideal property. This is omitted, following [12].

As explained later, the semantics of pattern terms uses the functional
semantics ${\mathcal{F}}{[\\![}\mbox{-}{]\\!]}$ of the pattern. The table
omits semantics of $\mathit{fst}$ and $\mathit{snd}$ as the image under
$\mathord{\sf Gr}$ of their functional semantics. Prop. 6 gives a condition
that is desirable to connect the relational interpretation of a constant with
its functional interpretation. For arrow-free types the condition is simply
that ${[\\![}c:\sigma{]\\!]}=\mathord{\sf
Gr}({\mathcal{F}}{[\\![}c:\sigma{]\\!]})$.

To interpret patterns, the idea is to compose the converse of the pattern with
the result term [12]. This must be done internally, i.e., using morphisms that
model the external operation of converse, and unlike Rel, Idl lacks converse.
So, unlike in [12], our patterns are restricted to functional terms. For
these, the functional interpretation gives a comap that can be reversed using
the internal opgraph $\mathsf{rg}$ which is analogous to $\mathsf{gr}$. This
is problematic because $\mathsf{rg}$ is anti-monotonic. Before delving into
the details of the solution, let us turn aside to consider the application of
relational semantics.

### Falling short of heap patterns

Here is a simple realization of heaps. Let the base types include
$\mathit{Ref}$ and $\mathit{Heap}$, with ${[\\![}\mathit{Ref}{]\\!]}$ some
set, ordered discretely. Let ${[\\![}\mathit{Heap}{]\\!]}$ be the set of
finite partial maps
${[\\![}\mathit{Ref}{]\\!]}\mathbin{\longrightarrow}{[\\![}\mathit{Ref}{]\\!]}\times{[\\![}\mathit{Ref}{]\\!]}$,
again ordered discretely. One constant is
$cell:\mathit{Ref}\times\mathit{Ref}\times\mathit{Ref}\rightarrow\mathit{Heap}$,
interpreted as a total function that forms one-cell heaps, written
$x\stackrel{{\scriptstyle.}}{{\mapsto}}y,z$ in Section 2. Another constant is
$new:\mathit{Heap}\rightarrow\mathit{Ref}$, interpreted as some relation that
returns references not in the domain of the heap. It could be a total function
(provided that ${[\\![}\mathit{Ref}{]\\!]}$ is infinite), or partial, or not
even functional. The constant
$star:\mathit{Heap}\times\mathit{Heap}\rightarrow\mathit{Heap}$ is interpreted
as a partial function that forms the union, for heaps with disjoint domains,
and is otherwise undefined.

These definitions do not yet achieve the hoped-for ability to write patterns
as in Section 2, because to appear on the left of a pattern term the constants
need to have an interpretation in Poset. This might be handled by adding an
“undefined element” to ${[\\![}\mathit{Heap}{]\\!]}$, and using a
deterministic allocator. A nicer solution is to move to predicate transformers
(Section 7), where the pattern term merely needs an interpretation in Idl, for
which the definitions above are fine.

### Completing the semantics of pattern terms

The rest of this section gives the technical details of the semantics of
pattern matching.

Recall that the typing rule infers
$\Gamma{\mathrel{\;\vdash}\;}\mathord{\raisebox{1.93747pt}{$\chi$}}x.M\mathrel{\mapsto}N:\sigma\rightarrow\sigma^{\prime}$
from the judgements
$\Gamma,x:\sigma^{\prime\prime}{\mathrel{\;\vdash}\;}M:\sigma$ and
$\Gamma,x:\sigma^{\prime\prime}{\mathrel{\;\vdash}\;}N:\sigma^{\prime}$. The
one fine point about typing is that it should enforce, somehow, that there is
an interpretation in Poset for all constants in $M$. We refrain from
formalizing that. The semantics is defined using the semantics of the
corresponding abstractions, namely

$\begin{array}[]{l}{\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.M:\sigma^{\prime\prime}\rightarrow\sigma{]\\!]}:{\mathcal{F}}{[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{\mathcal{F}}{[\\![}\sigma^{\prime\prime}{]\\!]}\mathbin{\Rightarrow}{\mathcal{F}}{[\\![}\sigma{]\\!]}\quad\mbox{in
}\mbox{{Poset}}\\\ {[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.N:\sigma^{\prime\prime}\rightarrow\sigma^{\prime}{]\\!]}:{[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{[\\![}\sigma^{\prime\prime}{]\\!]}\mathbin{\leadsto}{[\\![}\sigma^{\prime}{]\\!]}\quad\mbox{in
}\mbox{{Idl}}\end{array}$

Consider the special case where
$\Gamma,\sigma,\sigma^{\prime},\sigma^{\prime\prime}$ are arrow-free, so the
two semantics ${\mathcal{F}}$ and ${\mathcal{R}}$ agree on types. In that
case, we want to compose the pattern term with the internal opgraph
$\mathsf{rg}:{[\\![}\sigma^{\prime\prime}{]\\!]}\mathbin{\Rightarrow}{[\\![}\sigma{]\\!]}\mathbin{\longrightarrow}{[\\![}\sigma{]\\!]}\mathbin{\leadsto}{[\\![}\sigma^{\prime\prime}{]\\!]}$
to get

${\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.M:\sigma^{\prime\prime}\rightarrow\sigma{]\\!]}\mathbin{\mbox{\small{;}}}\mathsf{rg}\>:\>{[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{[\\![}\sigma{]\\!]}\mathbin{\leadsto}{[\\![}\sigma^{\prime\prime}{]\\!]}$
(26)

which, paired with the semantics of $N$, gives
${[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}({[\\![}\sigma{]\\!]}\mathbin{\leadsto}{[\\![}\sigma^{\prime\prime}{]\\!]})\times({[\\![}\sigma^{\prime\prime}{]\\!]}\mathbin{\leadsto}{[\\![}\sigma^{\prime}{]\\!]})$.
Following this with the internal composition $\mathsf{comp}$ yields what we
need:

$\langle{\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.M{]\\!]}\mathbin{\mbox{\small{;}}}\mathsf{rg}\,,\,{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.N{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathsf{comp}\>:\>{[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{[\\![}\sigma{]\\!]}\mathbin{\leadsto}{[\\![}\sigma^{\prime}{]\\!]}$
(27)

This is the gist of the idea. But $\mathsf{rg}$ is anti-monotonic so
${\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.M{]\\!]}\mathbin{\mbox{\small{;}}}\mathsf{rg}$ need not be an ideal and the
other constructs do not apply.

To solve this problem, we first extend $\mathsf{gr}$ to a type-indexed family
of ideals
$\mathsf{sim}_{\sigma}:{\mathcal{F}}{[\\![}\sigma{]\\!]}\mathbin{\longrightarrow}{\mathcal{R}}{[\\![}\sigma{]\\!]}$.

$\begin{array}[]{lll}\mathsf{sim}_{b}&=&\mathsf{id}\quad\mbox{i.e.,
$\preceq_{b}$, for base types $b$ (and for $\mathbf{1}$)}\\\
\mathsf{sim}_{\sigma\times\sigma^{\prime}}&=&\mathsf{sim}_{\sigma}\times\mathsf{sim}_{\sigma^{\prime}}\\\
\mathsf{sim}_{\sigma\rightarrow\sigma^{\prime}}&=&\mathsf{gr}\mathbin{\mbox{\small{;}}}(\mathsf{sim}_{\sigma}^{*}\mathbin{\leadsto}\mathsf{sim}_{\sigma^{\prime}})\end{array}$

For all $\sigma$, we have that $\mathsf{sim}_{\sigma}$ is a comap, because
$\mathsf{gr}$ is a comap, the range of $\mathbin{\leadsto}$ is comaps, and
composition preserves comaps. Thus the map $\mathsf{sim}_{\sigma}^{*}$ exists.

Next, we define $\mathsf{rg}$. Other elements of the semantics are based
solely on structure given by Propositions 1–5, but for $\mathsf{rg}$ we leave
such an axiomatic treatment to future work. For any $B,C$, let $\mathord{\sf
Rg}_{B,C}$ be the restriction of $\mathord{\sf Rg}$ to the homset
$\mbox{{Poset}}(B,C)$, so that $\mathord{\sf Rg}_{B,C}$ is a monotonic
function $\mathord{\sf
Rg}_{B,C}:\mbox{{Poset}}(B,C)\mathbin{\longrightarrow}(\mbox{{Idl}}(C,B))^{\sim}$.
But the target poset, which can also be written
$(C\mathbin{\leadsto}B)^{\sim}$, is ordered upside-down from what is needed to
compose with the result term in a pattern expression. For any $B$ let
$\mathsf{rev}_{B}$ be the identity function, taken as an anti-monotonic
function of type $\widetilde{B}\mathbin{\longrightarrow}B$. Define
$\mathsf{rg}:(B\mathbin{\Rightarrow}C)\mathbin{\longrightarrow}(C\mathbin{\leadsto}B)$
as the anti-monotonic function $\mathord{\sf
Rg}_{B,C}\mathbin{\mbox{\small{;}}}\mathsf{rev}_{B\mathbin{\leadsto}C}$. Thus
we have the composite (26) as a relation of the type shown there, though it is
not an ideal. Now we can use the sandwich lemma: For relations
$A\rTo^{Q}B\rTo^{R}C\rTo^{S}D$ between posets,

$\mbox{if }Q,S\mbox{ are ideals then
}Q\mathbin{\mbox{\small{;}}}R\mathbin{\mbox{\small{;}}}S\mbox{ is an ideal
}A\mathbin{\longrightarrow}D$ (28)

We sandwich ${\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.M{]\\!]}\mathbin{\mbox{\small{;}}}\mathsf{rg}$ with ideals based on
$\mathsf{sim}$ in a way that is needed anyway to reconcile the ${\mathcal{F}}$
and ${\mathcal{R}}$ interpretations of types. To give the details, we note
first the types

$\begin{array}[]{l}{\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.M^{\prime}:\sigma^{\prime\prime}\rightarrow\sigma^{\prime}{]\\!]}:{\mathcal{R}}{[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{\mathcal{R}}{[\\![}\sigma^{\prime\prime}{]\\!]}\mathbin{\leadsto}{\mathcal{R}}{[\\![}\sigma^{\prime}{]\\!]}\quad\mbox{in
}\mbox{{Idl}}\\\ {\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.M:\sigma^{\prime\prime}\rightarrow\sigma{]\\!]}:{\mathcal{F}}{[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{\mathcal{F}}{[\\![}\sigma^{\prime\prime}{]\\!]}\mathbin{\Rightarrow}{\mathcal{F}}{[\\![}\sigma{]\\!]}\quad\mbox{in
}\mbox{{Poset}}\end{array}$

and hence ${\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.M:\sigma^{\prime\prime}\rightarrow\sigma{]\\!]}\mathbin{\mbox{\small{;}}}\mathsf{rg}$
is a relation
${\mathcal{F}}{[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{\mathcal{F}}{[\\![}\sigma{]\\!]}\mathbin{\leadsto}{\mathcal{F}}{[\\![}\sigma^{\prime\prime}{]\\!]}$.
Using appropriate instances of $\mathsf{sim}$ and $\mathsf{sim}^{*}$ we obtain

$\mathsf{sim}^{*}_{\Gamma}\mathbin{\mbox{\small{;}}}\mathord{\sf
Gr}({\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.M:\sigma^{\prime\prime}\rightarrow\sigma{]\\!]})\mathbin{\mbox{\small{;}}}\mathsf{rg}\mathbin{\mbox{\small{;}}}(\mathsf{sim}^{*}_{\sigma}\mathbin{\leadsto}\mathsf{sim}_{\sigma^{\prime\prime}})$

of type
${\mathcal{R}}{[\\![}\Gamma{]\\!]}\longrightarrow{\mathcal{R}}{[\\![}\sigma{]\\!]}\mathbin{\leadsto}{\mathcal{R}}{[\\![}\sigma^{\prime\prime}{]\\!]}$.
This is an ideal, by the sandwich lemma (28). As described earlier, for the
semantics of $\mathord{\raisebox{1.93747pt}{$\chi$}}x.M\mathrel{\mapsto}N$
this ideal is paired with the semantics of $N$ and followed by
$\mathsf{comp}$, in accord with (27). See Table 2. Although $\mathord{\sf Gr}$
could be omitted, owing to (10), we use it because it has a parallel in the
predicate transformer semantics (Table 3).

##  6 Lax laws for relational semantics

This section proves a connection between relational and functional semantics,
describes a stronger connection conjectured to hold, and proves new results
that serve as laws of programming.

### Connecting the semantics by simulation

A conservative extension result would show that, for a purely functional term,
the relational (or transformer) interpretation is “the same” as the functional
one, in some suitable sense. Given that the two semantics have different
interpretations for arrow types, this needs to involve the embedding between
those interpretations, as noted in Section 1. De Moor and Gibbons [12] state a
strong conservative extension result for their relational semantics, which we
explain later. For the models in this article, weaker simulation results
suffice to justify program construction by stepwise refinement.

###### Proposition 6

[29] Suppose that
$\mathsf{sim}_{\mathbf{1}}\mathbin{\mbox{\small{;}}}{\mathcal{R}}{[\\![}c:\sigma{]\\!]}\mathrel{\supseteq}{\mathcal{F}}{[\\![}c:\sigma{]\\!]}\mathbin{\mbox{\small{;}}}\mathsf{sim}_{\sigma}$
for all constants666If $\Gamma=x_{0}:\sigma_{0},\ldots,x_{n}:\sigma_{n}$, we
write $\mathsf{sim}_{\Gamma}$ for
$\mathsf{sim}_{(\ldots(\mathbf{1}\times\sigma_{0})\times\ldots\sigma_{n})}:{\mathcal{F}}{[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{\mathcal{R}}{[\\![}\Gamma{]\\!]}$.
$c:\sigma$. Then for all functional terms in context
$\Gamma{\mathrel{\;\vdash}\;}M:\sigma$

$\mathsf{sim}_{\Gamma}\mathbin{\mbox{\small{;}}}{\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}M:\sigma{]\\!]}\mathrel{\,\supseteq\,}{\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}M:\sigma{]\\!]}\mathbin{\mbox{\small{;}}}\mathsf{sim}_{\sigma}$

The right hand side is the same as $\mathord{\sf
Gr}({\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}M:\sigma{]\\!]})\mathbin{\mbox{\small{;}}}\mathsf{sim}_{\sigma}$,
owing to (10). Owing to the shunting property (9), there is an equivalent
formulation which also suggests how to obtain relational interpretations of
constants from their functional interpretation:

${\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}M:\sigma{]\\!]}\mathrel{\,\supseteq\,}\mathsf{sim}^{*}_{\Gamma}\mathbin{\mbox{\small{;}}}\mathord{\sf
Gr}({\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}M:\sigma{]\\!]})\mathbin{\mbox{\small{;}}}\mathsf{sim}_{\sigma}$

Corollary: If all types in $\Gamma,\sigma$ are arrow-free,
${\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}M:\sigma{]\\!]}\mathrel{\supseteq}{\mathcal{F}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}M:\sigma{]\\!]}$,
because $\mathsf{sim}$ is the identity for arrow-free types and $\mathord{\sf
Gr}$ is increasing. This licenses development by stepwise refinement chains
${\mathcal{R}}{[\\![}N{]\\!]}\mathrel{\supseteq}\ldots\mathrel{\supseteq}{\mathcal{R}}{[\\![}M{]\\!]}\mathrel{\supseteq}{\mathcal{F}}{[\\![}M{]\\!]}$.

### Connecting the semantics as an equality

The conservative extension property [12] involves two additional
interpretations of types. The positive interpretation $\mathcal{P}$ replaces
every arrow in positive position by a relation space and every negative arrow
by a function space. The negative interpretation $\mathcal{N}$ does the
reverse. For example $\mathcal{P}{[\\![}(b_{0}\rightarrow
b_{1})\rightarrow(b_{2}\rightarrow b_{3}){]\\!]}$ is
$({[\\![}b_{0}{]\\!]}\mathbin{\Rightarrow}{[\\![}b_{1}{]\\!]})\mathbin{\leadsto}({[\\![}b_{2}{]\\!]}\mathbin{\leadsto}{[\\![}b_{3}{]\\!]})$
for base types $b_{0},\ldots,b_{3}$. The definitions are mutually recursive:

$\begin{array}[]{llllll}\mathcal{P}{[\\![}\sigma\rightarrow\sigma^{\prime}{]\\!]}&=&\mathcal{N}{[\\![}\sigma{]\\!]}\mathbin{\leadsto}\mathcal{P}{[\\![}\sigma^{\prime}{]\\!]}&\mathcal{N}{[\\![}\sigma\rightarrow\sigma^{\prime}{]\\!]}&=&\mathcal{P}{[\\![}\sigma{]\\!]}\mathbin{\Rightarrow}\mathcal{N}{[\\![}\sigma^{\prime}{]\\!]}\\\
\mathcal{P}{[\\![}\sigma\times\sigma^{\prime}{]\\!]}&=&\mathcal{P}{[\\![}\sigma{]\\!]}\times\mathcal{P}{[\\![}\sigma^{\prime}{]\\!]}&\mathcal{N}{[\\![}\sigma\times\sigma^{\prime}{]\\!]}&=&\mathcal{N}{[\\![}\sigma{]\\!]}\times\mathcal{N}{[\\![}\sigma^{\prime}{]\\!]}\\\
\mathcal{P}{[\\![}b{]\\!]}&=&{[\\![}b{]\\!]}&\mathcal{N}{[\\![}b{]\\!]}&=&{[\\![}b{]\\!]}\end{array}$

For clarity the connection is stated for the special case that the context has
a single variable. The connection is the equality of the the top and bottom
paths in this diagram.

$\begin{diagram}$ (29)

To be precise, $\mathord{\sf Gr}$ should be applied to the upper path. The
upper diagonals are two families of monotonic functions defined by mutual
recursion on types. The lower diagonals are two families of ideals defined
similarly.

$\begin{array}[]{llllll}n2f_{\sigma\rightarrow\sigma^{\prime}}&=&f2p_{\sigma}\mathbin{\Rightarrow}n2f_{\sigma^{\prime}}&f2p_{\sigma\rightarrow\sigma^{\prime}}&=&(n2f_{\sigma}\mathbin{\Rightarrow}f2p_{\sigma^{\prime}})\mathbin{\mbox{\small{;}}}\mathord{\sf
Gr}\\\ n2f_{\sigma\times\sigma^{\prime}}&=&n2f_{\sigma}\times
n2f_{\sigma^{\prime}}&f2p_{\sigma\times\sigma^{\prime}}&=&f2p_{\sigma}\times
f2p_{\sigma^{\prime}}\\\ n2f_{b}&=&id&f2p_{b}&=&id\\\\[8.61108pt]
n2r_{\sigma\rightarrow\sigma^{\prime}}&=&\mathsf{gr}\mathbin{\mbox{\small{;}}}(r2p_{\sigma}\mathbin{\leadsto}n2r_{\sigma^{\prime}})&r2p_{\sigma\rightarrow\sigma^{\prime}}&=&n2r_{\sigma}\mathbin{\leadsto}r2p_{\sigma^{\prime}}\\\
n2r_{\sigma\times\sigma^{\prime}}&=&n2r_{\sigma}\times
n2r_{\sigma^{\prime}}&r2p_{\sigma\times\sigma^{\prime}}&=&r2p_{\sigma}\times
r2p_{\sigma^{\prime}}\\\
n2r_{b}&=&\mathsf{id}&r2p_{b}&=&\mathsf{id}\end{array}$

Here $\mathord{\sf Gr}$ is the function $\mathord{\sf
Gr}:\mathcal{N}{[\\![}\sigma{]\\!]}\mathbin{\Rightarrow}\mathcal{P}{[\\![}\sigma^{\prime}{]\\!]}\mathbin{\longrightarrow}\mathcal{N}{[\\![}\sigma{]\\!]}\mathbin{\leadsto}\mathcal{P}{[\\![}\sigma^{\prime}{]\\!]}$
and $\mathsf{gr}$ is the ideal
$\mathsf{gr}:\mathcal{P}{[\\![}\sigma{]\\!]}\mathbin{\Rightarrow}\mathcal{N}{[\\![}\sigma^{\prime}{]\\!]}\mathbin{\longrightarrow}\mathcal{P}{[\\![}\sigma{]\\!]}\mathbin{\leadsto}\mathcal{N}{[\\![}\sigma^{\prime}{]\\!]}$.

The result conjectured in [12] is that, for their semantics, the hexagon
equality holds for all functional terms (assuming that it holds for the
interpretations of constants). We conjecture that this also holds in our
semantics.777De Moor and Gibbons indicate that they proved the result for beta
normal forms. A possibly relevant observation is that in our ${\mathcal{R}}$
semantics, application-free functional terms are comaps; applications are
interpreted using $\mathsf{ap_{i}}$ which is not a comap.

### Laws for programming

Stepwise refinement depends on monotonicity of program constructs.
Monotonicity of pattern terms is delicate, due to the use of $\mathsf{rg}$,
and we leave that issue to future work on laws for patterns. Monotonicity is
not addressed in [12], perhaps due to difficulties mentioned in Section 4, but
it is straightforward to prove the following for relational terms in Idl.

######  Theorem 7 (monotonicity)

Let $C[\mbox{-}]$ be any context888A context $C[\mbox{-}]$ is a term with a
missing subterm, called the hole, and $C[N]$ is the term with the hole filled
by $N$. such that the hole does not occur on the left of $\mathrel{\mapsto}$
in a pattern. Let $N$ and $N^{\prime}$ be of suitable type to fill the hole.
Then
${\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N:\sigma{]\\!]}\mathrel{\supseteq}{\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N^{\prime}:\sigma{]\\!]}$
implies
${\mathcal{R}}{[\\![}\Gamma^{\prime}{\mathrel{\;\vdash}\;}C[N]:\sigma^{\prime}{]\\!]}\mathrel{\supseteq}{\mathcal{R}}{[\\![}\Gamma^{\prime}{\mathrel{\;\vdash}\;}C[N^{\prime}]:\sigma^{\prime}{]\\!]}$.

Proposition 6 licenses us to reason about functional terms using functional
semantics. But the extended language would be of little interest if laws did
not carry over to it. Laws for products in the relational semantics can be
read directly from corresponding semantic properties, and are left to the
reader.

For lambda expressions the eta law is $\lambda x\,.\,Nx\mathrel{\supseteq}N$
(for $x$ not free in $N$).

######  Theorem 8 (eta law)

${\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x\,.\,Nx:\sigma\rightarrow\sigma^{\prime}{]\\!]}\mathrel{\supseteq}{\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N:\sigma\rightarrow\sigma^{\prime}{]\\!]}$
provided that $x$ is not free in $N$.

Proof:

$\begin{array}[]{rll}&{\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x\,.\,Nx:\sigma\rightarrow\sigma^{\prime}{]\\!]}\\\\[2.15277pt]
=&\quad\;\mbox{{semantics of $\lambda$ and application}}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>=&\quad\;\mbox{{ $x$ not free in $N$, semantics of $x$ ($\pi,\pi^{\prime}$ are
left, right proj.)}}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>=&\quad\;\mbox{{def $\times$}}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>\mathrel{\supseteq}&\quad\;\mbox{{exponent law (\ref{eq:apx})}}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>\end{array}$

The second step uses the evident semantics of a typing rule that adds variable
$x$ to the context for a term in which $x$ is not free.

The semantics validates $(\lambda x.x-x)(0\sqcap 1)=0$, which shows that
application is by-value rather than by-name. As expected in a by-value
calculus, beta conversion is not an equality in the relational semantics,
e.g., $(\lambda x.x-x)(0\sqcap 1)\mathrel{\subseteq}(0\sqcap 1)-(0\sqcap 1)$
is a proper inclusion because the right side includes $0-1$ and $1-0$. We do
get a refinement for this and similar cases. The beta law
$N[N^{\prime}/x]\mathrel{\supseteq}(\lambda x\,.\,N)N^{\prime}$ holds provided
that $x$ does not occur in a pattern. We say $x$ occurs in a pattern of $N$ if
it occurs in $M$ for some subterm
$\mathord{\raisebox{1.93747pt}{$\chi$}}x\,.\,M\mathrel{\mapsto}N_{1}$ of $N$.

######  Theorem 9 (beta law)

For all relational terms $N$ and $N^{\prime}$, such that $x$ does not occur in
a pattern in $N$,
${\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N[N^{\prime}/x]:\sigma{]\\!]}\>\mathrel{\supseteq}\>{\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}(\lambda
x\,.\,N)N^{\prime}:\sigma{]\\!]}$. This is an equality if $N^{\prime}$ denotes
a comap and $N$ is pattern-free.

Note that the equality still allows nondeterminacy in $N$.

In the rest of this section we omit ${\mathcal{R}}$. To prove the theorem, we
observe

$\begin{array}[]{rll}&{[\\![}\Gamma{\mathrel{\;\vdash}\;}(\lambda
x\,.\,N)N^{\prime}:\sigma{]\\!]}\\\\[2.15277pt] =&\quad\;\mbox{{semantics of
$\lambda$ and application}}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>=&\quad\;\mbox{{product law (\ref{eq:prc})}}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>=&\quad\;\mbox{{exponent law (\ref{eq:ap}) }}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>\end{array}$

The last line exhibits “substitution as composition”. The proof is completed
using a substitution lemma. While for functional semantics it is an equality,
for ideals it weakens to an inequality.

######  Lemma 10 (substitution)

For all relational terms $N,N_{0}$ such that $x$ does not occur in a pattern
of $N$,

${[\\![}\Gamma{\mathrel{\;\vdash}\;}N[N_{0}/x]:\sigma{]\\!]}\mathrel{\supseteq}\langle\mathsf{id},{[\\![}\Gamma{\mathrel{\;\vdash}\;}N_{0}:\sigma_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}{[\\![}\Gamma,x\\!:\\!\sigma_{0}{\mathrel{\;\vdash}\;}N:\sigma{]\\!]}$

Equality holds if $N_{0}$ denotes a comap and $N$ is pattern-free.

An operational interpretation of the inequality goes as follows. On the right
side, $N_{0}$ is evaluated once, whereas on the left there may be multiple
occurrences of $N_{0}$ in $N[N_{0}/x]$ which give rise to different
nondeterministic choices.

The rest of this section is devoted to the proof of Lemma 10. The inequality
is proved by structural induction on $N$. We give the proof in detail, in
order to pinpoint exactly what properties are needed for the inequality and
for the equality. We elide ${\mathcal{R}}$ throughout, and also elide some
types, including the type of $x$.

Case $N$ is a variable $x$. Here $N[N_{0}/x]$ is $N_{0}$ and we have

$\begin{array}[]{rll}&\langle\mathsf{id},{[\\![}\Gamma{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}{[\\![}\Gamma,x{\mathrel{\;\vdash}\;}x{]\\!]}&\\\\[-2.15277pt]
=&&\;\mbox{semantics of $x$}\\\\[-3.44444pt]
&\langle\mathsf{id},{[\\![}\Gamma{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathord{\sf
Gr}\pi&\\\\[-3.44444pt] (A)\quad=&&\;\mbox{product law (\ref{eq:pra}=),
$\mathsf{id}$ comap}\\\\[-3.44444pt]
&{[\\![}\Gamma{\mathrel{\;\vdash}\;}N_{0}{]\\!]}&\\\\[-3.44444pt] \end{array}$

Here (A) marks a step to which we return when proving Lemma 17 for transformer
semantics.

Case $N$ is a choice $N^{\prime}\sqcap N^{\prime\prime}$. Straightforward,
using that $\mathbin{\mbox{\small{;}}}$ distributes over $\cup$. The
straightforward cases for constants and pairing are also omitted.

Case $N$ is an application $N^{\prime}N^{\prime\prime}$.

$\begin{array}[]{rll}&\langle\mathsf{id},{[\\![}\Gamma{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}{[\\![}\Gamma,x{\mathrel{\;\vdash}\;}N^{\prime}N^{\prime\prime}{]\\!]}\\\\[2.15277pt]
=&\quad\;\mbox{{semantics of $N^{\prime}N^{\prime\prime}$}}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>(B)\quad\mathrel{\subseteq}&\quad\;\mbox{{product law (\ref{eq:prb}),
$\mathbin{\mbox{\small{;}}}$ monotonic}}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>\mathrel{\subseteq}&\quad\;\mbox{{induction,
$\mathbin{\mbox{\small{;}}},\langle\mbox{-},\mbox{-}\rangle$
monotonic}}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>=&\quad\;\mbox{{semantics of application, substitution}}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>\end{array}$

Note that step (B) is an equality if $N_{0}$ denotes a comap, by (14=).

Case $N$ is an abstraction $\lambda y\,.\,N^{\prime}$. Clearly the semantics
models alpha conversion, so we can assume without loss of generality that $y$
is distinct from $x$. And $y$ is not free in $N_{0}$. We need to use an
isomorphism $p$ that rearranges components $x,y$ of the context. Such
structural isomorphisms are available thanks to Propositions 1 and 2. Precise
definitions can be found in semantics texts such as [15]. We content ourselves
with displaying the type of $p$ in a diagram for an equation, that holds for
arbitrary
$R:{[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{[\\![}\sigma_{0}{]\\!]}$ and
any $\sigma^{\prime\prime}$.

$\begin{diagram}$ (30)

Using (30) we calculate

$\begin{array}[]{rll}&{[\\![}\Gamma{\mathrel{\;\vdash}\;}(\lambda
y\,.\,N^{\prime})[N_{0}/x]{]\\!]}&\\\\[-2.15277pt] =&&\;\mbox{substitution,
$x,y$ distinct}\\\\[-3.44444pt] &{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
y\,.\,N^{\prime}[N_{0}/x]{]\\!]}&\\\\[-3.44444pt] =&&\;\mbox{semantics of
$\lambda$}\\\\[-3.44444pt]
&\mathsf{cur_{i}}{[\\![}\Gamma,y{\mathrel{\;\vdash}\;}N^{\prime}[N_{0}/x]{]\\!]}&\\\\[-3.44444pt]
\mathrel{\supseteq}&&\;\mbox{induction, $\mathsf{cur_{i}}$
monotonic}\\\\[-3.44444pt]
&\mathsf{cur_{i}}(\langle\mathsf{id},{[\\![}\Gamma,y{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}{[\\![}\Gamma,y,x{\mathrel{\;\vdash}\;}N^{\prime}{]\\!]})&\\\\[-3.44444pt]
=&&\;\mbox{$y$ not free in $N_{0}$, semantics}\\\\[-3.44444pt]
&\mathsf{cur_{i}}(\langle\mathsf{id},\pi\mathbin{\mbox{\small{;}}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}{[\\![}\Gamma,y,x{\mathrel{\;\vdash}\;}N^{\prime}{]\\!]})&\\\\[-3.44444pt]
=&&\;\mbox{$p$ isomorphism }\\\\[-3.44444pt]
&\mathsf{cur_{i}}(\langle\mathsf{id},\pi\mathbin{\mbox{\small{;}}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}p\mathbin{\mbox{\small{;}}}{[\\![}\Gamma,x,y{\mathrel{\;\vdash}\;}N^{\prime}{]\\!]})&\\\\[-3.44444pt]
=&&\;\mbox{(\ref{eq:pcom}) with
$R:={[\\![}\Gamma{\mathrel{\;\vdash}\;}N_{0}{]\\!]}$}\\\\[-3.44444pt]
&\mathsf{cur_{i}}((\langle\mathsf{id},{[\\![}\Gamma{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\times\mathsf{id})\mathbin{\mbox{\small{;}}}{[\\![}\Gamma,x,y{\mathrel{\;\vdash}\;}N^{\prime}{]\\!]})&\\\\[-3.44444pt]
(C)\quad\mathrel{\supseteq}&&\;\mbox{exponent law (\ref{eq:curnat})
}\\\\[-3.44444pt]
&\langle\mathsf{id},{[\\![}\Gamma{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathsf{cur_{i}}{[\\![}\Gamma,x,y{\mathrel{\;\vdash}\;}N^{\prime}{]\\!]})&\\\\[-3.44444pt]
=&&\;\mbox{semantics of $\lambda$}\\\\[-3.44444pt]
&\langle\mathsf{id},{[\\![}\Gamma{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}{[\\![}\Gamma,x{\mathrel{\;\vdash}\;}\lambda
y\,.\,N^{\prime}{]\\!]})&\\\\[-3.44444pt] \end{array}$

Step (C) is an equality if $N_{0}$ denotes a comap, by (23=).

Case $N$ is a pattern term
$\mathord{\raisebox{1.93747pt}{$\chi$}}y\,.\,M\mathrel{\mapsto}N^{\prime}$.
Assume w.l.o.g. that $x$ is distinct from $y$. Here $N_{0}$ must be a
functional term in order for the substitution to yield a typable pattern term.
We write $\mathsf{s}$ to abbreviate $\mathsf{sim}$, and a huge comma
$\mathbin{\>\raisebox{2.15277pt}{\LARGE\bf,}\>}$ to aid parsing complicated
pairings. We also elide $\Gamma$, and the type of $x$, on the left of
${\mathrel{\;\vdash}\;}$ throughout.

$\begin{array}[]{rll}&\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}{[\\![}x{\mathrel{\;\vdash}\;}\mathord{\raisebox{1.93747pt}{$\chi$}}y\,.\,M\mathrel{\mapsto}N^{\prime}{]\\!]}\\\\[2.15277pt]
=&\quad\;\mbox{{semantics of
$\mathord{\raisebox{1.93747pt}{$\chi$}}$}}\\\\[2.15277pt]
&\lx@intercol\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\langle\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}x{\mathrel{\;\vdash}\;}\lambda
y\,.\,M{]\\!]}\mathbin{\mbox{\small{;}}}\mathsf{rg}\mathbin{\mbox{\small{;}}}(\mathsf{s}^{*}\mathbin{\leadsto}\mathsf{s})\mathbin{\>\raisebox{2.15277pt}{\LARGE\bf,}\>}{[\\![}x{\mathrel{\;\vdash}\;}\lambda
<EMAIL_ADDRESS>(D)\,\mathrel{\subseteq}&\quad\;\mbox{{by (\ref{eq:prb}) }}\\\\[2.15277pt]
&\lx@intercol\Bigl{\langle}\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}x{\mathrel{\;\vdash}\;}\lambda
y\,.\,M{]\\!]}\mathbin{\mbox{\small{;}}}\mathsf{rg}\mathbin{\mbox{\small{;}}}(\mathsf{s}^{*}\mathbin{\leadsto}\mathsf{s})\mathbin{\>\raisebox{2.15277pt}{\LARGE\bf,}\>}\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}{[\\![}x{\mathrel{\;\vdash}\;}\lambda
<EMAIL_ADDRESS>\mathrel{\subseteq}&\quad\;\mbox{{induction}}\\\\[2.15277pt]
&\lx@intercol\Bigl{\langle}\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}x{\mathrel{\;\vdash}\;}\lambda
y\,.\,M{]\\!]}\mathbin{\mbox{\small{;}}}\mathsf{rg}\mathbin{\mbox{\small{;}}}(\mathsf{s}^{*}\mathbin{\leadsto}\mathsf{s})\mathbin{\>\raisebox{2.15277pt}{\LARGE\bf,}\>}{[\\![}{\mathrel{\;\vdash}\;}\lambda
<EMAIL_ADDRESS>\mathrel{\subseteq}&\quad\;\mbox{{claim (\ref{eq:claim}) below, and
monotonicity of $(\mathbin{\mbox{\small{;}}})$ and
$\langle\mbox{-},\mbox{-}\rangle$}}\\\\[2.15277pt]
&\lx@intercol\langle\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}{\mathrel{\;\vdash}\;}\lambda
y\,.\,M[N_{0}/x]{]\\!]}\mathbin{\mbox{\small{;}}}\mathsf{rg}\mathbin{\mbox{\small{;}}}(\mathsf{s}^{*}\mathbin{\leadsto}\mathsf{s})\mathbin{\>\raisebox{2.15277pt}{\LARGE\bf,}\>}{[\\![}{\mathrel{\;\vdash}\;}\lambda
<EMAIL_ADDRESS>=&\quad\;\mbox{{substitution, semantics of
$\mathord{\raisebox{1.93747pt}{$\chi$}}$}}\\\\[2.15277pt]
&\lx<EMAIL_ADDRESS>\end{array}$

Step (D) is an equality if $N_{0}$ denotes a comap, by (14=). The claim is

$\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}{\mathrel{\;\vdash}\;}\lambda
y\,.\,M[N_{0}/x]{]\\!]}\mathrel{\supseteq}\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}x{\mathrel{\;\vdash}\;}\lambda
y\,.\,M{]\\!]}$ (31)

If $x$ is not free in pattern $M$ then $\lambda y\,.\,M[N_{0}/x]$ is $\lambda
y\,.\,M$ and the claim can be proved using properties of the left projection
$\pi$ as follows.

$\begin{array}[]{rll}&\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}x{\mathrel{\;\vdash}\;}\lambda
y\,.\,M{]\\!]}&\\\\[-2.15277pt] =&&\;\mbox{ $x$ not free in $\lambda y\,.\,M$,
semantics}\\\\[-3.44444pt]
&\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}\pi\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}{\mathrel{\;\vdash}\;}\lambda
y\,.\,M{]\\!]}&\\\\[-3.44444pt] =&&\;\mbox{def $\mathsf{s}$, $\times$
preserves comaps}\\\\[-3.44444pt]
&\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}(\mathsf{s}^{*}\times\mathsf{s}^{*})\mathbin{\mbox{\small{;}}}\pi\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}{\mathrel{\;\vdash}\;}\lambda
y\,.\,M{]\\!]}&\\\\[-3.44444pt] (E)\quad\mathrel{\subseteq}&&\;\mbox{$\pi$ lax
natural, from (\ref{eq:pra})}\\\\[-3.44444pt]
&\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\pi\mathbin{\mbox{\small{;}}}\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}{\mathrel{\;\vdash}\;}\lambda
y\,.\,M{]\\!]}&\\\\[-3.44444pt]
(F)\quad\mathrel{\subseteq}&&\;\mbox{(\ref{eq:pra}) and unit
law}\\\\[-3.44444pt]
&\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}\pi\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}{\mathrel{\;\vdash}\;}\lambda
y\,.\,M{]\\!]}&\\\\[-3.44444pt] \end{array}$

Because $\times$ preserves comaps,
$\mathsf{s}_{\Gamma,x}^{*}=\mathsf{s}_{\Gamma}^{*}\times\mathsf{s}_{x}^{*}$.
Step (F) is an equality if $N_{0}$ denotes a comap, but step (E) is not.

The lemma holds as an equality if $N_{0}$ is a comap and $N$ has no patterns.
(Under those conditions, the inductive steps become equalities.)

If $x$ occurs in $M$, a natural attempt goes as follows. By the substitution
lemma for ${\mathcal{F}}$, which is an equality, (31) is equivalent to

$\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}\langle\mathsf{id},{\mathcal{F}}{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}x{\mathrel{\;\vdash}\;}\lambda
y\,.\,M{]\\!]}\mathrel{\supseteq}\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}{\mathcal{F}}{[\\![}x{\mathrel{\;\vdash}\;}\lambda
y\,.\,M{]\\!]}$

This follows by monotonicity of $(\mathbin{\mbox{\small{;}}})$ from
$\mathsf{s}^{*}\mathbin{\mbox{\small{;}}}\langle\mathsf{id},{\mathcal{F}}{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathrel{\supseteq}\langle\mathsf{id},{[\\![}{\mathrel{\;\vdash}\;}N_{0}{]\\!]}\rangle\mathbin{\mbox{\small{;}}}\mathsf{s}^{*}$.
Here we are in trouble. Roughly speaking, this asks for the functional
semantics of $N_{0}$ to contain the relational semantics, which is the reverse
of Proposition 6.

##  7 Transformers and transformer semantics

Predicate transformers are often taken to be monotonic functions on powersets,
but here we use updeal lattices. The reason is that if powersets are used
instead of updeal lattices, the internal hom does not carry a well behaved
exponent structure. For example, we need the associated functor to preserve
identities, which fails with powersets. This section begins with a brief
explanation of why updeal lattices are sensible in programming terms. Then it
proceeds to describe the model and give the semantics. Results not proved here
can be found in [27] or [29].

Ordered data types are needed even in first order languages, if extensible
record or object types are admitted. To see the significance of ordering for
imperative programs, consider an expression refinement $e\preceq e^{\prime}$.
This does not imply the command refinement
$x:=e\mathrel{\sqsubseteq}x:=e^{\prime}$, because that requires
$wp(x:=e)\phi\mathrel{\subseteq}wp(x:=e^{\prime})\phi$ for all postconditions
$\phi$, which fails for postcondition $x=e$. A more reasonable postcondition
is $e\preceq x$, which is upward closed in $x$. To give a specification that
exactly characterizes the assignment $x:=e$, we can use auxiliary $y$ in
precondition $y\preceq e$ and postcondition $y\preceq x$. These predicates are
closed upward in the state variable $x$ and downward in $y$. In general,
$pre,post$ in the span (2) can be taken to be ideals from auxiliary state to
program state.

Weakest-precondition functions map predicates on final states to predicates on
initial states, so notation and terminology is most perspicuous if we use an
opposite category. We also follow convention in predicate transformer
semantics and order predicates by $\mathrel{\subseteq}$; we write
$\widetilde{\mathcal{U}}A$ for the lattice of updeals on $A$, ordered by
$\mathrel{\subseteq}$, as opposed to ${\mathcal{U}}A$ ordered by
$\mathrel{\supseteq}$. We define Tran to have all posets as objects; and the
homset $\mbox{{Tran}}(A,B)$ is just
$\mbox{{Poset}}(\widetilde{\mathcal{U}}B,\widetilde{\mathcal{U}}A)$, i.e.,
$\mbox{{Poset}}^{op}(\widetilde{\mathcal{U}}A,\widetilde{\mathcal{U}}B)$.
Following the convention in refinement calculi, the symbol
$\mathrel{\sqsubseteq}$ is used for the ordering, so
$t\mathrel{\sqsubseteq}t^{\prime}$ iff
$t\beta\mathrel{\subseteq}t^{\prime}\beta$ for all
$\beta\in\widetilde{\mathcal{U}}B$.

Composition in Tran is just functional composition, for which we write
$\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}$ so that for
$t$ in $\mbox{{Tran}}(A,B)$ and $u$ in $\mbox{{Tran}}(B,C)$ we have
$t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}u=u\mathbin{\mbox{\small{;}}}t$.
The identity on $A$ is the identity function $id_{\widetilde{\mathcal{U}}A}$.
For any ideal $R:A\mathbin{\longrightarrow}B$, the universal image
$\mathord{{\mathbb{A}}}R\in\mbox{{Tran}}(A,B)$ is defined by
$\mathord{{\mathbb{A}}}R=\widetilde{\mathcal{U}}(\mathord{\ni}/R)$, using
relational quotient. At the level of points, $a\in\mathord{{\mathbb{A}}}RX$
iff $\forall\,b\,.\,aRb\Rightarrow b\in X$. The universal image of an ideal is
universally conjunctive. Moreover, $\mathord{{\mathbb{A}}}$ is refinement
injective:
$R\mathrel{\supseteq}S\equiv\mathord{{\mathbb{A}}}R\mathrel{\sqsubseteq}\mathord{{\mathbb{A}}}S$.
Thus it preserves demonic choice: $\mathord{{\mathbb{A}}}(R\cup
S)=\mathord{{\mathbb{A}}}R\sqcap\mathord{{\mathbb{A}}}S$ where $\sqcap$ is
pointwise intersection. Later we use $\sqcup$ for pointwise union, which
models angelic choice. Define $\mathord{{\mathbb{E}}}R$ to be the direct image
of $R$, but as a function
$\widetilde{\mathcal{U}}A\mathbin{\longrightarrow}\widetilde{\mathcal{U}}B$
and so distinguished from
${\mathcal{U}}R:{\mathcal{U}}A\mathbin{\longrightarrow}{\mathcal{U}}B$. Note
that $\mathord{{\mathbb{E}}}$ is a monotonic functor
$\mbox{{Idl}}^{co\,op}\mathbin{\longrightarrow}\mbox{{Tran}}$. A crucial fact
is that for any $R$, $\mathord{{\mathbb{A}}}R$ is a map with comap
$\mathord{{\mathbb{E}}}R$. Thus $\mathord{{\mathbb{A}}}$ is onto maps. This is
an unfortunate clash of terminology as $\mathord{\sf Gr}$ plays the same role
as $\mathord{{\mathbb{A}}}$ but $\mathord{\sf Gr}$ embeds onto comaps.

A bimap is a map that is also a comap. For any monotonic function $f$,
$\mathord{{\mathbb{A}}}(\mathord{\sf Gr}f)$ is a bimap in Tran. Sometimes we
omit $\mathord{\sf Gr}$ and write simply $\mathord{{\mathbb{A}}}f$. The
situation looks as follows, using fishtail arrows for embeddings and fishhooks
for inclusions.

$\begin{diagram}$

In fact the vertical arrows are categorical equivalences.

A transformer $t:A\mathbin{\longrightarrow}B$ is strict if
$t\emptyset=\emptyset$ (i.e., $t(\mathit{false})=\mathit{false}$) and costrict
if $tB=A$ (i.e., $t(true)=true$, which expresses program termination). Comaps
are strict and maps are costrict.

Cartesian product of underlying posets gives a weak product of predicate
transformers; we overload $\times$ and $\langle,\rangle$ but write
$\mathord{{\mathbb{A}}}\pi$ explicitly for the projection lifted from Poset.

###### Proposition 11

$\times$ is monotonic and for all $t,u,v,w$,

$\displaystyle\langle
t,u\rangle\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathord{{\mathbb{A}}}\pi$
$\displaystyle\mathrel{\sqsubseteq}$ $\displaystyle t\quad\mbox{if $t,u$
strict}$ (32) $\displaystyle\langle
t,u\rangle\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathord{{\mathbb{A}}}\pi$
$\displaystyle\mathrel{\sqsupseteq}$ $\displaystyle t\quad\mbox{if $t,u$
costrict}$ (33) $\displaystyle\langle
t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathord{{\mathbb{A}}}\pi\,,\,t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathord{{\mathbb{A}}}\pi^{\prime}\rangle$
$\displaystyle\mathrel{\sqsubseteq}$ $\displaystyle t\quad\mbox{if $t$ map}$
(34)
$\displaystyle(t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}u)\times(v\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}w)$
$\displaystyle\mathrel{\sqsubseteq}$ $\displaystyle(t\times
v)\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}(u\times
w)\quad(=,\mbox{ if $u,w$ maps})$ (35) $\displaystyle\langle
t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}u\,,\,v\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}w\rangle$
$\displaystyle\mathrel{\sqsubseteq}$ $\displaystyle\langle
t,v\rangle\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}(u\times
w)\quad(=,\mbox{ if $u,w$ maps})$ (36) $\displaystyle\langle
t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}u\,,\,t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}v\rangle$
$\displaystyle\mathrel{\sqsubseteq}$ $\displaystyle
t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\langle
u,v\rangle\quad\mbox{if $t$ map}\quad(=,\mbox{ if $t$ bimap})$ (37)

Adequacy of predicate transformers as a model of nondeterminacy and divergence
together is reflected in the behavior of products. As in Idl, the projection
law (32) is not an equality in general (intuitively, $u$ could diverge). Even
the inequality depends on absence of miracles. The reverse inequality holds
for costrict transformers and _a fortiori_ for maps. The other defining law
for products of functions also weakens to (34), reflecting nondeterminacy as
with relations. The side condition that $t$ is a map expresses the absence of
angelic nondeterminacy; in fact the condition can be weakened to positive
conjunctivity. The inequality (37) holds so long as $t$ is finitely
conjunctive, and the reverse $\mathrel{\sqsupseteq}$ holds if $t$ a comap.

As with products, the exponent structure is very lax. The exponent object
$B\mathbin{\looparrowright}C$ is $\mbox{{Tran}}(B,C)$, ordered by
$\mathrel{\sqsubseteq}$. Definitions for currying and application can be found
in [27] and [29]; we only need the following.

###### Proposition 12

[27]
$\mathbin{\looparrowright}:\mbox{{Tran}}^{op}\times\mbox{{Tran}}\mathbin{\longrightarrow}\mbox{{Tran}}$
is a monotonic functor and for all $t,u,v$

$\displaystyle\mathsf{cur_{t}}\,t\mbox{ is a bimap}$ (38)
$\displaystyle(\mathsf{cur_{t}}~{}t\times\mathsf{id})\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathsf{ap_{t}}$
$\displaystyle=$ $\displaystyle t$ (39)
$\displaystyle\mathsf{cur_{t}}((t\times\mathsf{id})\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathsf{ap_{t}})$
$\displaystyle\mathrel{\sqsubseteq}$ $\displaystyle t\quad\mbox{if $t$
map}\quad(=,\mbox{if $t$ bimap})$ (40)
$\displaystyle\mathsf{cur_{t}}((t\times\mathsf{id})\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}u)$
$\displaystyle\mathrel{\sqsubseteq}$ $\displaystyle
t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathsf{cur_{t}}~{}u\quad\mbox{if
$t$ map}\quad(=,\mbox{if $t$ bimap})$ (41)
$\displaystyle\mathsf{cur_{i}}((\mathsf{id}\times
t)\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}u\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}v)$
$\displaystyle=$
$\displaystyle\mathsf{cur_{t}}~{}u\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}(t\mathbin{\looparrowright}v)$
(42)

The analog of the internal graph functor $\mathsf{gr}$ is the internal
universal image
$\mathsf{unim}:B\mathbin{\leadsto}C\mathbin{\longrightarrow}B\mathbin{\looparrowright}C$
defined by
$\mathsf{unim}=\mathsf{cur_{t}}(\mathord{{\mathbb{A}}}\mathsf{ap_{i}})$. It is
a bimap, being in the image of $\mathsf{cur_{t}}$. Just as $\mathsf{gr}$ is
used in (25), $\mathsf{unim}$ expresses how $\mathsf{cur_{t}}$ and
$\mathsf{ap_{t}}$ extend their relational counterparts:

$\mathsf{cur_{t}}(\mathord{{\mathbb{A}}}R)=\mathord{{\mathbb{A}}}(\mathsf{cur_{i}}R)\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathsf{unim}\qquad\quad(\mathsf{unim}\times\mathsf{id})\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathsf{ap_{t}}=\mathord{{\mathbb{A}}}\,\mathsf{ap_{i}}\quad.$

### Transformer semantics

Types are interpreted as before, except for using the constructs of Tran:
${[\\![}\sigma\times\sigma^{\prime}{]\\!]}={[\\![}\sigma{]\\!]}\times{[\\![}\sigma^{\prime}{]\\!]}$
and
${[\\![}\sigma\rightarrow\sigma^{\prime}{]\\!]}={[\\![}\sigma{]\\!]}\mathbin{\looparrowright}{[\\![}\sigma^{\prime}{]\\!]}$.
We assume
${[\\![}B{]\\!]}={\mathcal{R}}{[\\![}B{]\\!]}={\mathcal{F}}{[\\![}B{]\\!]}$
for the base types. We extend $\mathsf{unim}$ to a simulation
$\mathsf{psim}_{\sigma}:{\mathcal{R}}{[\\![}\sigma{]\\!]}\mathbin{\longrightarrow}{\mathcal{T}}{[\\![}\sigma{]\\!]}$
by defining these morphisms in Tran:

$\begin{array}[]{lll}\mathsf{psim}_{B}&=&\mathsf{id}\mbox{ for base types $B$
(and for $\mathbf{1}$)}\\\
\mathsf{psim}_{\sigma\times\sigma^{\prime}}&=&\mathsf{psim}_{\sigma}\times\mathsf{psim}_{\sigma^{\prime}}\\\
\mathsf{psim}_{\sigma\rightarrow\sigma^{\prime}}&=&\mathsf{unim}\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}(\mathsf{psim}_{\sigma}^{*}\mathbin{\looparrowright}\mathsf{psim}_{\sigma^{\prime}})\end{array}$

Because $\mathsf{unim}$ is a bimap and the range of $\mathsf{cur_{t}}$ is a
bimap, each $\mathsf{psim}$ is a bimap, and $\mathsf{psim}^{*}$ denotes the
corresponding map.

We augment the language of terms with angelic choice $\sqcup$, using a new
syntactic category $P$. Patterns are now relational terms:

$P::=N\mid\langle P,P\rangle\mid PP\mid\lambda
x.P\mid\mathord{\raisebox{1.93747pt}{$\chi$}}x.N\mathrel{\mapsto}P\mid P\sqcap
P\mid P\sqcup P$

The semantics is in Table 3.

Table 3: The predicate transformer semantics
${\mathcal{T}}{[\\![}\mbox{-}{]\\!]}$, given transformers
${[\\![}c:\sigma{]\\!]}:\mathbf{1}\mathbin{\longrightarrow}{\mathcal{T}}{[\\![}\sigma{]\\!]}$.
$\begin{array}[]{lcl}{[\\![}\Gamma{\mathrel{\;\vdash}\;}x{]\\!]}&=&\mathord{{\mathbb{A}}}\pi\quad\mbox{where
$\pi$ is the appropriate projection}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}c{]\\!]}&=&\mathord{{\mathbb{A}}}\pi\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}{[\\![}c:\sigma{]\\!]}\mbox{
where $\pi$ is the projection
${[\\![}\Gamma{]\\!]}\mathbin{\longrightarrow}{[\\![}\mathbf{1}{]\\!]}$}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}\langle
P,P^{\prime}\rangle:\sigma\times\sigma^{\prime}{]\\!]}&=&\langle{[\\![}\Gamma{\mathrel{\;\vdash}\;}P:\sigma{]\\!]},{[\\![}\Gamma{\mathrel{\;\vdash}\;}P^{\prime}:\sigma^{\prime}{]\\!]}\rangle\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}PP^{\prime}:\sigma{]\\!]}&=&\langle{[\\![}\Gamma{\mathrel{\;\vdash}\;}P:\sigma^{\prime}\rightarrow\sigma{]\\!]},{[\\![}\Gamma{\mathrel{\;\vdash}\;}P^{\prime}:\sigma^{\prime}{]\\!]}\rangle\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathsf{ap_{t}}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.P:\sigma\rightarrow\sigma^{\prime}{]\\!]}&=&\mathsf{cur_{t}}{[\\![}\Gamma,x:\sigma{\mathrel{\;\vdash}\;}P:\sigma^{\prime}{]\\!]}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}\mathord{\raisebox{1.93747pt}{$\chi$}}x.N\mathrel{\mapsto}P:\sigma\rightarrow\sigma^{\prime}{]\\!]}&=&\\\
\lx@intercol\qquad\langle\mathsf{psim}^{*}_{\Gamma}\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathord{{\mathbb{A}}}({\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x.N{]\\!]})\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathsf{exim}\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}(\mathsf{psim}^{*}_{\sigma^{\prime\prime}}\mathbin{\looparrowright}\mathsf{psim}_{\sigma})\>,\>{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
<EMAIL_ADDRESS>{[\\![}\Gamma{\mathrel{\;\vdash}\;}P\sqcap
P^{\prime}:\sigma{]\\!]}&=&{[\\![}\Gamma{\mathrel{\;\vdash}\;}P:\sigma{]\\!]}\sqcap{[\\![}\Gamma{\mathrel{\;\vdash}\;}P^{\prime}:\sigma{]\\!]}\\\
{[\\![}\Gamma{\mathrel{\;\vdash}\;}P\sqcup
P^{\prime}:\sigma{]\\!]}&=&{[\\![}\Gamma{\mathrel{\;\vdash}\;}P:\sigma{]\\!]}\sqcup{[\\![}\Gamma{\mathrel{\;\vdash}\;}P^{\prime}:\sigma{]\\!]}\end{array}$

For semantics of patterns we overload the name $\mathsf{comp}$ for the
internal composition in Tran. We also use the internal existential image
$\mathsf{exim}$, which is analogous to $\mathsf{rg}$ for the relational
semantics. The analogy includes the annoying fact that it is an order-
reversing function. For any $B,C$ let $\mathord{{\mathbb{E}}}_{B,C}$ be the
restriction of $\mathord{{\mathbb{E}}}$ to the homset $\mbox{{Idl}}(B,C)$.
Thus it is a monotonic function
$\mathord{{\mathbb{E}}}_{B,C}:B\mathbin{\leadsto}C\mathbin{\longrightarrow}(C\mathbin{\looparrowright}B)^{\sim}$,
which yields anti-monotonic function
$(\mathord{{\mathbb{E}}}_{B,C}\mathbin{\mbox{\small{;}}}\mathsf{rev}):B\mathbin{\leadsto}C\mathbin{\longrightarrow}C\mathbin{\looparrowright}B$.
Here $\mathsf{rev}$ is the order-reversing identity function
$\mathsf{rev}_{C\mathbin{\looparrowright}B}:(C\mathbin{\looparrowright}B)^{\sim}\mathbin{\longrightarrow}C\mathbin{\looparrowright}B$
mentioned a few lines before (28).

We defined $\mathord{{\mathbb{A}}}$ only for ideals, but in fact for any $R$
with
$\vbox{\hbox{\tiny$\preceq$}}\mathbin{\mbox{\small{;}}}R\mathrel{\subseteq}R$,
the inverse image sends updeals to updeals. Taking $R$ to be
$\mathord{{\mathbb{E}}}_{B,C}\mathbin{\mbox{\small{;}}}\mathsf{rev}$ and using
the order $\mathrel{\supseteq}$ on $B\mathbin{\leadsto}C$ we define
$\mathsf{exim}$ to be
$\mathord{{\mathbb{A}}}(\vbox{\hbox{\tiny$\supseteq$}}\mathbin{\mbox{\small{;}}}\mathord{{\mathbb{E}}}_{B,C}\mathbin{\mbox{\small{;}}}\mathsf{rev})$
which is a morphism in
$\mbox{{Tran}}(B\mathbin{\leadsto}C,C\mathbin{\looparrowright}B)$. The rest of
the semantics for patterns parallels the relational semantics. Any constant
that occurs on the left of a pattern needs to have an interpretation in Idl,
just as the relational semantics requires a functional interpretation of such
constants.

##  8 Lax laws for transformer semantics

The basic connection between transformer semantics and ideals is similar to
Prop. 6.

######  Theorem 13 ([29])

Suppose that
$\mathsf{psim}_{\mathbf{1}}\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}{\mathcal{T}}{[\\![}c:\sigma{]\\!]}\mathrel{\sqsubseteq}\mathord{{\mathbb{A}}}({\mathcal{R}}{[\\![}c:\sigma{]\\!]})\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathsf{psim}_{\sigma}$
for all constants $c:\sigma$. Then for all relational terms $N$

$\mathsf{psim}\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}{\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N:\sigma{]\\!]}\mathrel{\sqsubseteq}\mathord{{\mathbb{A}}}({\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N:\sigma{]\\!]})\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathsf{psim}$

If all types in $\Gamma,\sigma$ are arrow-free then
${\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N:\sigma{]\\!]}\mathrel{\sqsubseteq}\mathord{{\mathbb{A}}}({\mathcal{R}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N:\sigma{]\\!]})$.
The result licenses development by stepwise refinement, that is, in a chain
${\mathcal{T}}{[\\![}P{]\\!]}\mathrel{\sqsubseteq}\ldots\mathrel{\sqsubseteq}{\mathcal{T}}{[\\![}N{]\\!]}\mathrel{\sqsubseteq}\mathord{{\mathbb{A}}}({\mathcal{R}}{[\\![}N{]\\!]})$
ending with a “program” that has only demonic nondeterminacy.

### Refinement laws

As in the relational semantics, it is straightforward to prove the following
monotonicity result for transformer terms.

######  Theorem 14 (monotonicity)

For any context $C[\mbox{-}]$ in which terms $P$ and $P^{\prime}$ may occur,
except to the left of $\mathrel{\mapsto}$ in pattern terms,
${\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}P:\sigma{]\\!]}\mathrel{\supseteq}{\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}P^{\prime}:\sigma{]\\!]}$
implies
${\mathcal{T}}{[\\![}\Gamma^{\prime}{\mathrel{\;\vdash}\;}C[P]:\sigma^{\prime}{]\\!]}\mathrel{\supseteq}{\mathcal{T}}{[\\![}\Gamma^{\prime}{\mathrel{\;\vdash}\;}C[P^{\prime}]:\sigma^{\prime}{]\\!]}$.

Laws for products in predicate transformer semantics can be read directly from
corresponding semantic properties, e.g., (32) and (34) are beta and eta laws
for products in Tran. For exponents, the eta law is a conditional refinement:
$\lambda x\,.\,Px\mathrel{\sqsubseteq}P$ if $P$ is a map (and $x$ not free in
$P$).

######  Theorem 15 (eta law)

${\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x\,.\,Px:\sigma\rightarrow\sigma^{\prime}{]\\!]}\mathrel{\sqsubseteq}{\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}P:\sigma\rightarrow\sigma^{\prime}{]\\!]}$
if $P$ is a map and $x$ is not free in $P$.

Proof: We have ${\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}\lambda
x\,.\,Px{]\\!]}=\mathsf{cur_{t}}(({\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}P:\sigma{]\\!]}\times\mathsf{id})\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mathsf{ap_{t}})$
by semantics. If $P$ denotes a map, we can apply law (40) to obtain $\lambda
x\,.\,Px\mathrel{\sqsubseteq}P$.

######  Theorem 16 (beta law)

For all $\Gamma{\mathrel{\;\vdash}\;}P$ and all
$\Gamma{\mathrel{\;\vdash}\;}P^{\prime}$ such that
${\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}P^{\prime}{]\\!]}$ is a map,

${\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}P[P^{\prime}/x]:\sigma{]\\!]}\>\mathrel{\sqsubseteq}\>{\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}(\lambda
x\,.\,P)P^{\prime}:\sigma{]\\!]}$

provided $x$ does not occur in a pattern of $P$. This is an equality if
$P^{\prime}$ denotes a bimap and $P$ is pattern-free.

In particular, $P$ may have angelic and demonic nondeterminacy. Note that
$(\mbox{-}\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}t)$
distributes over both $\sqcap$ and $\sqcup$, for any $t$. Also
$\mathord{{\mathbb{E}}}(R\cup
S)=\mathord{{\mathbb{E}}}R\sqcup\mathord{{\mathbb{E}}}S$. As a consequence, we
have $\mathord{\raisebox{1.93747pt}{$\chi$}}x\,.\,N\sqcap
N^{\prime}\mathrel{\mapsto}P=(\mathord{\raisebox{1.93747pt}{$\chi$}}x\,.\,N\mathrel{\mapsto}P)\sqcup(\mathord{\raisebox{1.93747pt}{$\chi$}}x\,.\,N^{\prime}\mathrel{\mapsto}P)$
for all $N,N^{\prime},P$. This shows the angelic nature of patterns.

The proof of Theorem 16 is like the proof of Theorem 9. We show

${\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}(\lambda
x\,.\,P)P^{\prime}:\sigma{]\\!]}=\langle\mathsf{id},{\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}P^{\prime}:\sigma^{\prime}{]\\!]}\rangle\,\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\,{\mathcal{T}}{[\\![}\Gamma,x:\sigma^{\prime}{\mathrel{\;\vdash}\;}P:\sigma{]\\!]}$

using (36=) and (39) instead of the corresponding laws for Idl. The proof is
completed by appeal to the following.

######  Lemma 17 (substitution)

For all $P,P_{0}$ such that
${\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}P_{0}{]\\!]}$ is a map and
$x$ does not occur in a pattern in $P$,

${\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}P[P_{0}/x]:\sigma{]\\!]}\mathrel{\sqsubseteq}\langle\mathsf{id},{\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}P_{0}:\sigma_{0}{]\\!]}\rangle\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}{\mathcal{T}}{[\\![}\Gamma,x\\!:\\!\sigma_{0}{\mathrel{\;\vdash}\;}P:\sigma{]\\!]}$

This is an equality if $P_{0}$ denotes a bimap and $P$ is pattern-free.

The proof is similar to that for Lemma 10, using corresponding properties of
product and exponent in Tran. We do not repeat the calculations; the only
differences are steps marked with letters and we discuss these in turn below.
We refer to the identifiers $N,N^{\prime}$ in those calculations, which
correspond to $P,P_{0}$ in the current proof. In each case, the step goes
through thanks to $P_{0}$ denoting a map.

For the case that $N$ is $x$, the step (A) is an inequality
$\mathrel{\sqsupseteq}$ thanks to (33), provided
${\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N^{\prime}{]\\!]}$ is a map.
For application, the step marked (B) is an inequation $\mathrel{\sqsupseteq}$
if $N^{\prime}$ denotes a map, thanks to (37). In fact costrictness suffices
for (A) and positive conjunctivity for (B); together these are the properties
of a map, i.e. universal conjunctivity. For application, the step marked (C)
is an inequality $\mathrel{\sqsubseteq}$ if $N^{\prime}$ denotes a map, by
(41) (and it is $\mathrel{\sqsubseteq}$ that is needed here, because the
calculation is in the reverse direction from the prior ones).

For $N$ a pattern term, the step marked (D) goes through by (37) if
$N^{\prime}$ denotes a map, and steps (E) and (F) can be taken using (33).

The proof for demonic choice is straightforward, using that
$(t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}\mbox{-})$
distributes over arbitrary $\sqcap$ if $t$ is a map, and the $t$ in this case
is ${\mathcal{T}}{[\\![}\Gamma{\mathrel{\;\vdash}\;}N^{\prime}{]\\!]}$. The
proof for angelic choice uses the fact that
$(t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}u)\sqcup(t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}v)\mathrel{\sqsubseteq}t\mathbin{{\stackrel{{\scriptstyle\mbox{\tiny$\circ$}}}{{,}}}}(u\sqcup
v)$ for all $t,u,v$ (by monotonicity of $t$).

If $N^{\prime}$ denotes a bimap, the bimap conditions are met for steps (A),
(B), and (C), and bimaps distribute over both $\sqcup$ and $\sqcap$ on the
left. The lemma holds as an equality for pattern-free $N$ and bimap
$N^{\prime}$.

##  9 Discussion

Following de Moor and Gibbons [12], we have shown how to internalize the span
factorizations of ideal relations and of predicate transformers, and to use
these models for two semantics of lambda terms extended with non-injective and
non-total pattern matching. We have shown that not only the language of lambda
calculus but also its basic laws are available, although in weakened form. One
notable result is that beta refinement
$P[P^{\prime}/x]\mathrel{\sqsubseteq}(\lambda x\,.\,P)P^{\prime}$ holds in the
transformer model even if $P$ combines demonic and angelic nondeterminacy and
$P^{\prime}$ has demonic nondeterminacy.

The language of de Moor and Gibbons includes fixpoints. Our models support
recursive definitions, because homsets are complete lattices, but we leave
thorough investigation as future work. The authors say “the semantics we have
sketched leaves many questions unanswered”. It would be particularly
interesting to check which operations are monotonic with respect to their
refinement order, and whether terms in patterns need to be restricted as in
our models.

Here are some other open problems.

  * 1.

What are the interesting general laws for patterns? One way to investigate
would be to focus on heap patterns: design a subset of those that is easy to
compile, and find requisite simplification laws.

  * 2.

To investigate pattern matching for heap operations, one could try to derive a
version of $repmin$ with shared objects. Another example close at hand would
be to derive conventional code for _in situ_ list reversal, starting from the
abstract version sketched in Section 2. A further exercise would be to specify
and derive a program that maps an operation over a list of root pointers to
disjoint heap structures. For example, map $repmin$ over a list of trees. The
pattern could use a confined separation operator along the lines of Wang et al
[32].

  * 3.

For a usable calculus of imperative programs it seems desirable to avoid
explicit threading of state through expressions. This suggests combining
pattern terms with a monad to encapsulate state, perhaps drawing on ideas from
Hoare Type Theory [30].

  * 4.

Our presentation emphasizes algebraic structure: the proofs and constructions
are pointfree and based on Propositions 1–5,11,12 —with a few exceptions. The
semantic definitions for pattern terms rely on manipulation of non-monotonic
functions $\mathsf{rg}$ and $\mathsf{exim}$. The proof of (19) is not
pointfree. The problem is to fix these blemishes so that the Propositions can
be taken as axioms.

  * 5.

The last problem is to prove the hexagon equality (29), an attractive chiasmus
connecting ${\mathcal{F}}$ with ${\mathcal{R}}$. And do the same for
${\mathcal{R}}$ and ${\mathcal{T}}$. For the semantics of [12], Benton
sketched a proof for all functional terms in an unpublished note (2001) [3],
using a form of logical relation. In 2015, according to personal communication
with the Benton, de Moor, and Gibbons, there has been no further development,
but also little doubt that the result should hold.

### Acknowledgments

Thanks to Oege de Moor and Jeremy Gibbons for their stimulating paper and
enlightening discussions. Many thanks to three anonymous reviewers who
provided extensive detailed suggestions that greatly improved the presentation
and sharpened my understanding on various points. Thanks to Mounir Assaf,
Anindya Banerjee, Nick Benton, Steve Bloom, Andrey Chudnov, Joe Morris, and
José Nuno Oliveira for helpful feedback at various stages of the work reported
here.

Special thanks to José for eloquently advocating and teaching pointfree
relation algebra and for celebrating my student’s remark that those who like
maths also enjoy music and maps. Following the symbols as they danced along
the backward arrows of predicate transformers, I arrived at a canon cancrizans
of co/maps which I offer in celebration of the work of José Nuno Oliveira.

The author acknowledges partial support from NSF award CNS-1228930.

## References

  * App [14] Andrew W. Appel.  Program Logics for Certified Compilers.  Cambridge University Press, 2014.
  * BdM [96] Richard Bird and Oege de Moor.  Algebra of Programming.  Prentice-Hall, 1996.
  * Ben [00] Nick Benton.  A proof sketch of something which may possibly be a conjecture of Oege de Moor.  Private communication, December 2000.
  * BJJM [98] Roland Carl Backhouse, Patrik Jansson, Johan Jeuring, and Lambert G. L. T. Meertens.  Generic programming: An introduction.  In Advanced Functional Programming, pages 28–115, 1998.
  * BN [05] Anindya Banerjee and David A. Naumann.  Ownership confinement ensures representation independence for object-oriented programs.  Journal of the ACM, 52(6):894–960, November 2005.
  * BN [12] Anindya Banerjee and David A. Naumann.  State based encapsulation for modular reasoning about behavior-preserving refactorings.  In Dave Clarke, James Noble, and Tobias Wrigstad, editors, Aliasing in Object-oriented Programming, volume 7850 of Springer State-of-the-art Surveys. 2012.
  * BNR [13] Anindya Banerjee, David A. Naumann, and Stan Rosenberg.  Local reasoning for global invariants, part I: Region logic.  Journal of the ACM, 60(3):18:1–18:56, 2013.
  * Bun [97] Alex Bunkenburg.  Expression refinement.  Dissertation, University of Glasgow, 1997.
  * BvW [98] Ralph-Johan Back and Joakim von Wright.  Refinement Calculus: A Systematic Introduction.  Springer-Verlag, 1998.
  * dM [96] Oege de Moor.  An exercise in polytypic programming: repmin.  Typescript, www.cs.ox.ac.uk/research/pdt/ap/papers/repmin.ps.gz, (accessed June 2015), September 1996.
  * DM [15] Han-Hing Dang and B. Moeller.  Extended transitive separation logic.  Journal of Logical and Algebraic Methods in Programming, 84, 2015\.
  * dMG [00] Oege de Moor and Jeremy Gibbons.  Pointwise relational programming.  In Algebraic Methodology and Software Technology, volume 1816 of LNCS, pages 371–390, 2000.
  * FS [90] Peter J. Freyd and Andre Scedrov.  Categories, Allegories.  North-Holland, 1990.
  * GMdM [94] Paul H.B. Gardiner, Clare E. Martin, and Oege de Moor.  An algebraic construction of predicate transformers.  Science of Computer Programming, 22:21–44, 1994.
  * Gun [92] Carl A. Gunter.  Semantics of Programming Languages.  MIT, 1992.
  * HdM [00] Paul Hoogendijk and Oege de Moor.  Container types categorically.  Journal of Functional Programming, 10(2):191–225, 2000.
  * Hin [02] Ralf Hinze.  Constructing tournament representations: An exercise in pointwise relational programming.  In Mathematics of Program Construction, volume 2386 of LNCS, pages 131–147, 2002.
  * HvSM+ [14] Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, Jules Villard, Huibiao Zhu, and Peter W. O’Hearn.  Developments in concurrent Kleene algebra.  In Relational and Algebraic Methods in Computer Science (RAMiCS), volume 8428 of LNCS, pages 1–18, 2014.
  * MBT [09] Joseph M. Morris, Alexander Bunkenburg, and Malcolm Tyrrell.  Term transformers: A new approach to state.  ACM Transactions on Programming Languages and Systems, 31(4), 2009\.
  * MC [08] Clare E. Martin and Sharon A. Curtis.  Monadic maps and folds for multirelations in an allegory.  In Unifying Theories of Programming, Second International Symposium, Revised Selected Papers, volume 5713 of LNCS, pages 102–121, 2008.
  * MCR [07] Clare E. Martin, Sharon A. Curtis, and Ingrid Rewitzky.  Modelling angelic and demonic nondeterminism with multirelations.  Sci. Comput. Program., 65(2):140–158, 2007.
  * MHH [91] C.E. Martin, C. A. R. Hoare, and Jifeng He.  Pre-adjunctions in order enriched categories.  Mathematical Structures in Computer Science, 1:141–158, 1991.
  * Mor [94] Carroll Morgan.  Programming from Specifications, second edition.  Prentice Hall, 1994.
  * [24] Joseph M. Morris and Malcolm Tyrrell.  Dually nondeterministic functions.  ACM Transactions on Programming Languages and Systems, 30(6), 2008\.
  * [25] Joseph M. Morris and Malcolm Tyrrell.  Modelling higher-order dual nondeterminacy.  Acta Inf., 45(6):441–465, 2008.
  * [26] David A. Naumann.  Beyond Fun: Order and membership in polytypic imperative programming.  In Mathematics of Program Construction, volume 1422 of LNCS, pages 286–314, 1998.
  * [27] David A. Naumann.  A categorical model for higher order imperative programming.  Mathematical Structures in Computer Science, 8(4):351–399, 1998\.
  * [28] David A. Naumann.  Towards squiggly refinement algebra.  In David Gries and Willem-Paul de Roever, editors, Programming Concepts and Methods, pages 346–365. Chapman and Hall, 1998.
  * Nau [01] David A. Naumann.  Ideal models for pointwise relational and state-free imperative programming.  In Principles and Practice of Declarative Programming, pages 4–15, 2001.
  * NMB [08] Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal.  Hoare type theory, polymorphism and separation.  J. Funct. Program., 18(5-6):865–911, 2008.
  * Oli [09] José Nuno Oliveira.  Extended static checking by calculation using the pointfree transform.  In Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School, Revised Tutorial Lectures, volume 5520 of LNCS, pages 195–251, 2009.
  * WBO [08] Shuling Wang, Luís Soares Barbosa, and José Nuno Oliveira.  A relational model for confined separation logic.  In International Symposium on Theoretical Aspects of Software Engineering, (TASE), pages 263–270, 2008.