Bunch theory: working notes on applications, axioms and models
Extracted source text · arXiv 1911.04344
\documentclass[a4paper,12pt]{article}
\include{mpp_preamble}
\usepackage{appendix}
\usepackage{graphicx}
%theorem type environments
\newtheorem{theorem}{Theorem}
\newcounter{thm}[theorem]
\newtheorem{lemma}{Lemma}[theorem]
\newcounter{lem}[theorem]
\newtheorem{example}{Example}
\newcounter{ex}[example]
\newenvironment{proof}[1][Proof]{\begin{trivlist}
\item[\hskip \labelsep {\bfseries #1}]}{\end{trivlist}}
%short verbatim command
\renewcommand{\v}{\verb}
\newcommand{\Proof}{{\bf Proof} \hspace{2pt}}
\newcommand{\lit}[1]{\lsem #1 \rsem^{\mathcal{L}}}
%Quotes in math mode
\newcommand{\leftq}{$`` $}
\newcommand{\rightq}{$'' $}
%Expectation
\newcommand{\Exp}{{\bf \rm E}}
\title{Bunch theory: working notes on applications, axioms and models}
\author{Bill Stoddart, Frank Zeyda, Steve Dunne}
\begin{document}
\maketitle
\begin{abstract}
In his book {\em A practical theory of programming} \cite{ECRH93}, Eric Hehner proposes and applies a remarkably radical reformulation of set theory, in which the collection and packaging of elements are seen as separate activities. This provides for unpackaged collections, referred to as “bunches”. Bunches allow us to reason about non-determinism at the level of terms, and, very remarkably, allow us to reason about the conceptual entity “nothing”, which is just an empty bunch (and very different from an empty set). This eliminates mathematical “gaps” caused by undefined terms. We compare the use of bunches with other approaches to this problem, and we illustrate the use of Bunch Theory in formulating program semantic combining non-deterministic, preferential, and probabilistic choice. We show how an existing axiomatisation of set theory can be extended to incorporate bunches, and we provide and validate a model. Standard functions are lifted when applied to a bunch of values, but we also define a wholistic function application which allows whole bunches to be accepted as arguments, and we develop its associated fixed point theory.
\end{abstract}
\tableofcontents
\section{Introduction}
Set theory deals with elements as singular entities. A set may contain elements, and is itself an element that can belong to another, more deeply structured, set. When forming a set from its elements we simultaneously perform two actions: collection and packaging. However, it is beneficial to think of these as two orthogonal activities. The theory that results from this approach we will refer to as bunch theory, following Hehner, who first suggested it.
Bunch theory provides benefits in terms of preserving homogeneity, accommodating what would otherwise be undefined terms, and describing non-determinism - a key concept in software development.
Hehner provides an axiomatisation for Bunch Theory and builds set theory on top of this. Our approach will be to take an existing axiomatisation of set theory and add additional axioms to incorporate bunches.
The base formalism we build on is that used in the B Method of J-R Abrial \cite{JRA96}: that is predicate logic with equality and a typed set theory, with total and partial functions being restricted kinds of binary relation.
The paper is structured as follows. In section 2, we give an informal summary of bunch theory and its notation. In section 3 we give examples of bunch theory in use: we consider its contribution to theories of description due to the elimination of undefined terms, and we show how it can facilitate the formulation of programming semantics, including combinations of non-deterministic, preferential and probabilistic choice.
In section 4 we extend the axiomatisation of set theory given in \cite{JRA96} to incorporate bunch theory. Since the introduction of bunches into set theory is a radical departure from mathematical tradition, in sections 5 and 6 we justify its soundness by providing a model, representing each axiom within the model, and proving the resulting representations. For the purposes of validation, we keep our notation as sparse as possible, and in section 7 we formally extend our theory to include notations previously described in the informal introduction to bunch theory. In section 8 we extend our model to incorporate “improper bunches”, which are used to capture the occurrence and spread of error conditions, such as non-termination, which must be presumed when operations are executed outside their pre-condition. In section 9 we consider functions; we lift standard function application where it applies to bunches, and we introduce a separate “wholistic” form of function application which enables whole bunches to be passed as arguments. In section 10 we give a fixed point theory for wholistic function application and apply the theory in the construction of a formal grammar. In section 11 we report our conclusions.
To prevent the text being too congested, some of the mathematical material is presented in the appendices, beginning with a list of operator precedences.
The original contributions of this monograph include an analysis of the contribution of bunch theory to the problem of undefined terms, a axiomatisation based on extending set theory by giving a formal meaning to the contents of a set, the provision and validation of a model for this approach, and a fixed point theory for wholistic function application, with an illustration expressing formal grammars as simultaneous fixed point equations.
A theory and model for bunches has been proposed by Morris and Bunkenburg. \cite{MB01}. This axiomatises boolean and function types in the presence of non-determinism and considers the adaptation of logic to bunches of truth values. It does not integrate bunches within set theory. This contrasts with our approach which provides a full integration with set theory and isolates the use of bunches from logic by distinguishing truth semantics from value semantics, so we can continue to use classical predicate logic along with bunches.
\section{An informal view of bunch theory}
Following Hehner\cite{ECRH93}, we give a mathematical meaning to the contents of a set, which we call a bunch: e.g. the contents of the set $\{1,2\}$ is the bunch $1,2$. We write $\unpack A$ for the contents of set $A$, thus $\unpack \{1,2\} \, = \, 1,2$.
The comma used in a bunch extension expression such as 1,2,5 is now a mathematical operator, called bunch union. It is associative and commutative, and its precedence is just below than that of the expression connectives. It is associated with set union via the rule
$\{A\} \, ∪ \, \{B\} \, = \, \{A,B\}$
Standard function application is lifted when applied to a bunch, thus if $A=x,y$, then $f(A)=f(x),f(y)$. We take the infix syntax of binary operations as a sugared form of standard function application, so these are similarly lifted to apply pairwise, e.g. adding the bunches $0,1$ and $2,4$ yields $0+2, \, 0+4, \, 1+2, \, 1+4$. Using round brackets exclusively to express precedence (rather than sometimes using them to describe ordered pairs) and noting that bunch union (comma) has a lower precedence than $+$, we can write this as: \((0,1) \, + \, (2,4) \, = \, 2,3,4,5\). Thus we sacrifice the use of standard brackets to represent tuples: $(x,y)$ is no longer an ordered pair, for which we use maplet notation, i.e. $x \, \mapsto \, y$ or bold brackets: $\lboldb x,y\rboldb $. However we still use $f(x,y)$ for application of function $f$ to a pair of arguments, and when we apply a function $f$ to a bunch of arguments $x,y$, we write this as $f((x,y))$.
Lifting similarly applies to tuple construction, so that, e.g. $(1,2)\mapsto (3,4) \, = \, 1\mapsto 3,1\mapsto 4,2\mapsto 3,2\mapsto 4$
We have a bunch cardinality operator $\cent $. For any bunch $A$, $\cent A$ gives the number of elements comprising $A$. Elements have a bunch cardinality of 1, and are also referred to as “elementary bunches”.
In addition to standard function application we define “wholistic function application”, written as $f.A$, in which f is applied to the whole of the bunch $A$. As an example of how this might be used, consider the following characterisation of the bunch of natural numbers:
\(nat \, = \, 0 \, , \, succ(nat)\)
To represent this as a fixed point equation we introduce a function $f$ (say) with property $f.A \, = \, 0,succ(A)$. We then note that $f.null \, = \, 0$, $f.0 \, = \, 0,1$, $f.(0,1) \, = \, 0,1,2$ etc, so we are building a sequence of successive approximations to $nat$, and the solution of our recursive equation that defines $nat$ is the limit of this sequence. A formal treatment will be given in section \ref{functions}.
A bunch $A$ is a sub-bunch of $B$ if each element of $A$ is an element of $B$. We write this as $A \, : \, B$. Sub-bunches are related to subsets by the rule:
$A \, : \, B \, \, ⇔ \, \, \{A\} \, ⊆ \, \{B\}$
We add two constructs to Hehner's version of bunch theory: the guarded bunch and the pre-conditioned bunch. The guarded bunch $p \, \bguard \, \, E$ is equal to the empty bunch, $null$, if predicate $p$ is false, and otherwise equal to $E$. The preconditioned bunch $p \, \bpre \, E$ is equal to the improper bunch $⊥$ if $p$ is false, and otherwise equal to $E$. The improper bunch is used in describing the results of computations, and expresses the complete ignorance associated with a value provided by a computation that may have crashed. Such a failed computation might produce any value, or no value at all, and this is reflected in the rule that for any bunch $A$, we have $A:⊥$, that is any bunch is a sub-bunch of the improper bunch of the same type.
Standard function application is strict wrt the improper bunch, i.e. $f(⊥ \, )=⊥ \, $ for any function $f$.
The B-Method provides us with the ability to construct basic sets,
including the integers. Such sets are termed “maximal” since they are not subsets of any larger set. From any existing maximal sets we are able to produce new maximal sets by the use of set product and power-set operations. Each maximal set corresponds to a type.
From any set $X$ we can construct a smaller set by set comprehensions of the form
$\{x \, | \, x \, ∈ \, X \, ∧ \, P \, \}$
All sets we consider are necessarily homogeneous.
We similarly restrict our attention to bunches which are homogeneous; these have the same type as their elements, thus $1,2$ is of type integer.
Analogously to set comprehension, we can write the bunch comprehension:
$∮ \, x \, \bullet \, E$
Here, although the type of $x$ is not given explicitly it has to be implicit from an examination of the expression $E$. The result consists of all values that $E$ can take as $x$ ranges over its type. For example the bunch $10,20$ can be written as the bunch comprehension $∮ \, x \, \bullet \, x:1,2 \, \bguard \, \, 10*x$.
\section{Bunch theory in use}
We examine some contributions made by Bunch Theory, concentrating on three main areas: the resolution of problems associated with undefined terms, the expression of non-determinism and randomness in programs, and the preservation of homogeneity to simplify formal descriptions.
\subsection{Bunch theory and descriptions}\label{descriptions}
Bunch theory solves many problems relating to “descriptions” that include undefined values and non-denoting terms and also values described in terms of a computation which does not terminate. For example the term $1/0$ will represent $null$, and this has well defined mathematical behaviour. We can prove $1/0 \, = \, 1/0$, which conforms with the rule for equality $E \, = \, E$ in First Order Predicate Logic with Equality. However, before we discuss the full impact of bunch theory on descriptions, let us briefly survey how troublesome the area of undefined terms has been.
In our formal notation, as in natural language, many objects are referred to
by means of a description rather than being named directly. The problems which arise when such descriptions do not refer to anything (for example $1/0$ or "the present king of France"), or are ambiguous, have been the source of extensive debate in mathematics and philosophy at least since the emergence of Russell's Theory of Descriptions (RTD) \cite{BR05,WR10}. In response to the proposals of Meinong and Frege, Russell rejected approaches that attempted to directly assign some form of meaning or denotation to an invalid description (also referred to an as “undefined term”), but showed how statements that involved such terms could nevertheless be handled in a consistent way. In RTD, undefined terms are non-denoting. They have no significance of their own account, but any assertion in which they have a primary occurrence entails an existential claim which results in the assertion being false. For example “the present king of France is bald” is false, since it entails a claim that there is a king of France; “the King of France is non-bald” is also false, but, by negation of our first example, “it is false that the King of France is bald” is true.
In formal notations, the definite description $ι \, x \, \bullet \, P$ commonly represents the supposedly unique value of $x$ described by predicate $P$. A common form of definite description is function application, noting that the term $f(x)$ can be expressed as $ι \, y \, \bullet \, x \, \mapsto \, y \, ∈ \, f$. In a formalism in which partial and total functions are a particular form of binary relation (an approach which RTD shares with a number of current formalisms including Z, B, and VDM) the term $f(x)$ is taken to be an invalid description when there is no unique $y$ such that $x \, \mapsto \, y \, ∈ \, f$.
In Abrial's approach, instead of undefined terms being non-denoting (as in RTD), we hold that they do denote an object of the correct type, but we do not know what it is. This provides the advantage of a formal system compatible with predicate logic with equality. In particular we have the simple equality law $E=E$. For example we can prove $1/0 \, = \, 1/0$. This is not possible in RTD, because it entails the existential claim that there is a number that is $1/0$. However, Abrial's approach means that stating $f(x)=y$ is not enough for us to conclude $x \, ∈ \, dom(f)$. To see why suppose we have the following rule for function application:
\[f(a) \, = \, b \, \, ⇒ \, \, a\mapsto b \, ∈ \, f \, \]
{\em This is the function application rule in our formalism,} which includes bunches, but does not work in Z and B. Using the empty relation $\{ \, \}$ as a function to deliberately provoke an undefined term, we can show, using this rule, that something belongs to the empty set. From our reflexive equality rule we have $\{\}(a) \, = \, \{\}(a)$. Hence, from the function application rule, we immediately obtain $a \, \mapsto \, \{\}(a) \, ∈ \, \{\}$. Now since $\{\}a$ denotes some value (though we do not know what this is) so also must $a \, \mapsto \, \{\}(a)$ and thus we have constructed an element that belongs to the empty set. To avoid this problem we must formulate a rule for function application that include information about the domain and functionality of $f$ e.g.
\[f \, ∈ \, A \, \pfun \, B \, ∧ \, a \, ∈ \, dom(f) \, ∧ \, f(a) \, = \, b \, \, ⇒ \, \, a\mapsto b \, ∈ \, f \, \]
and when writing a formal text the user has to be careful to give all the information required, which is not always easy, as in a recursive definition the domain of the function might not be explicitly given \cite{SDG99}.
Such considerations have led C B Jones and his associates to construct a three valued logic \cite{HB84}, in which predicates can be $true$, $false$, or $undefined$. In this approach we cannot fall back on classical logic, and we lose the law of the excluded middle as well as the simple law for equality. However, $f(x)=y$ does tell us that $y$ is the unique value associated with $x$ in $f$.
In the specification language Larch, and in the Isabelle/HOL proof assistant, partial functions are not available, and applications requiring functions that change according to events are modelled using total functions but giving only limited information about them. Asserting $f(a)=b$ then provides information about $f$ without any need for other conditions to hold. To model a birthday book we might have a set that associates people with dates, and rather than the set representing a partial function, it would contain information about a total function $birthday$ (say) over part of its domain. Because $birthday$ is a total function, mapping, say from $PERSON$ to $DATE$ we can say for any person $n$ that $∃ \, d \, \bullet \, d \, ∈ \, DATA \, ∧ \, birthday(n)=d$. We might not know the date of a person's birthday, but we have no objection to the fact that such a date exists. However, this does not fit so well with a function $king\_of$ mapping from $COUNTRY$ to $PERSON$, as it allows $∃ \, p \, \bullet \, p \, ∈ \, PERSON \, ∧ \, p \, = \, king\_of(france)$. I.e. there is an entailment that France has a king, though we don't know who it is.
There are also approaches which reject predicates with undefined terms as possible candidates for proof. This may be done by requiring the discharge of some preliminary well definedness proof obligations. Alternatively, it may be achieved by syntactic restrictions that require predicates to be written in a way that ensures well definedness.\cite{AM02}
Some of the many approaches, are described in \cite{DG96,SDG99}, and in \cite{AM02} where the authors consider the treatment of the propositions $2+3/0 \, = \, 2$ and $2+3/0 \, ≠ \, 2$ under 6 different regimes of undefinedness, none of which agree over the two results.
Let us now examine them in bunch theory. For the first we have:
\[2+3/0 \, = \, 2 \, \, \, \eq \, \, \, 2+null \, = \, 3 \, \, \eq \, \, \, null \, = \, 3 \, \, \eq \, \, false \, \]
In our formalism, the second is syntactic sugar for a set membership predicate, where $\_≠\_$ is the relation consisting of pairs of unequal integer values, and where the type $\num \, ↔ \, \num $ of the relation is given by context. We have:
\[2+3/0 \, \, ≠ \, \, 2 \, \, \, \eq \, \, \, 2+3/0 \, \mapsto \, 2 \, \, ∈ \, \, \_≠\_ \, \, \, \eq \, \, \, null \, \mapsto \, 2 \, \, ∈ \, \, \_≠\_ \, \, \\
\eq \, \, \, null \, ∈ \, \_≠\_ \, \, \, \eq \, \, true \, \]
Now consider the proposition:
\[lives\_in(son\_of(Charles)) \, = \, \, uk \, \]
where Charles has two sons. We think of the relation $son\_of$ as a non-deterministic function, which in this case returns a bunch of two values. The proposition will be true iff both sons live in the UK. The argument for this is that the bunch of two elements represent a non-deterministic choice, and as with non-deterministic choice in abstract command languages, we require that either choice must satisfy the given condition.
Returning to Russell's example, we represent this as
\[king\_of(france) \, \, ∈ \, \, bald \, \, \, \eq \, \, \, null \, ∈ \, bald \, \, \, \eq \, \, true \, \, \]
thus in this case we disagree with RTD, but the truth we obtain is vacuous, like the predicate established by an infeasible operation \cite{CM90}, or a universal quantification over an empty set.
It is possible to avoid undefined terms by using relational image rather than function application. The relational image of set $S$ under relation $R$ is defined as
\( \, R[S] \, \defs \, \{ \, x \, , \, y \, | \, x\mapsto y \, ∈ \, R \, ∧ \, x∈S \, \bullet \, y \, \} \, \)
and there is a close relationship with function application, since if $f(a)=b$ then $f[\{a\}] \, = \, \{b\}$. Relational image is always well defined, and allows us to capture non-existent objects via use of the empty set, e.g. $king\_of \, [ \, \{ \, france \, \} \, ] \, = \, \{ \, \}$. An interesting example of its use can be found in Version 1 of the Z Notion Standard \cite{ZBS}, a document which throughout uses relational image rather than function application. However, this technique is inevitably clumsy and was abandoned in later versions of the Standard.\footnote{In our bunch theory relational image is not defined since the value of $R[S]$ can be written as $\{ \, R(\unpack S) \, \}$.}
Finally we note that the underlying logic for our theory is Predicate Logic with Equality. Thus we have a classical two valued logic and the simple equality rule holds, in which every expression is equal to itself. We do not require special requirements on the domain of a function to draw conclusions from a function application, as we have the rules:
\[f(x)=y \, ⇒ \, \, x \, \mapsto \, y \, ∈ \, f \, \\
\, \, \, f(x)=y \, ⇒ \, ¬(∃ \, z \, \bullet \, z≠y \, ∧ \, a\mapsto z \, ∈ \, f)\]
These allow us to define a function by its applicative effect and without additional reference to its domain. Let's see how this works in the case of the factorial function, given the following properties which characterise it as an element and describe its application:
\[ \, \, \, \cent (fact)=1 \\
\, \, \, fact(n) \, \eq \, \IF \, n=0 \, \THEN \, 1 \, \ELSE \, n*fact(n-1) \, \END \\
\]
These properties suggest an operational interpretation for executing the function $fact$, but in our approach we don't have direct access to such an interpretation. Rather, $fact$ is particular type of set, a function from $\nat \, → \, \nat $, and we need a formal way to relate the above description of $fact$ to this set. Furthermore, we wonder what would be a reasonable interpretation of the factorial of a negative number, for example $fact(-3)$. Two interpretations would seem to be justifiable. The first would have $fact(-3)=null$ on the grounds that no value is described by $fact(-3)$. The second would have $fact(-3)=⊥$ on the grounds that an attempt to evaluate $fact(-3)$ will result in a crash.
To resolve these problems, we take the usual approach of using a higher order function $F$ to formulate a fixed point equation $F(fact)=fact$ and finding $fact$ as the solution of this equation. We will be able to obtain the descriptive interpretation of $fact$ as the greatest fixed point solution, $fact=\nu F$, and the operational interpretation of $fact$ as the least fixed point solution, $fact=μF$. We define
\[F \, \defs \, λ \, f \, \bullet \, λ \, n \, \bullet \, \IF \, n=0 \, \THEN \, 1 \, \ELSE \, n*f(n-1) \, \END \, \]
The existence of greatest and least fixed point solutions to $F(fact)=fact$ is guaranteed by the Knaster-Tarski theorem. The associated partial order, which reflects how deterministic a function is, is the inverse of set inclusion ordering, and is thus a complete lattice. Since $F$ is continuous, as well as monotonic, we will be able to derive our solutions as the limits of monotonic sequences of approximations to $fact$. To obtain the greatest fixed point $\nu F$ we use as first approximation the everywhere over-deterministic function $\{ \, \}$. Each successive approximation is obtained by applying $F$ to the previous one. Thus:
$\begin{array}{l} \, \, fact_0{} \, = \, \{ \, \} \, \, \, \end{array}$
$\begin{array}{l}
\, \, fact_1{} \, = \, F(fact_0{}) \, = \, \\
\, \, λ \, n \, \bullet \, \IF \, n=0 \, \THEN \, 1 \, \ELSE \, n*\{\}(n-1) \, \END \, = \\
\, \, λ \, n \, \bullet \, \IF \, n=0 \, \THEN \, 1 \, \ELSE \, null \, \END \, \, = \, \\
\, \, \{ \, n \, | \, n=0 \, \bguard \, 1, \, ¬(n=0) \, \bguard \, null \, \} \, = \\
\, \, \{ \, 0 \, \mapsto \, 1 \, \} \end{array}$
$\begin{array}{l}
\, \, fact_2{} \, = \, F(fact_1{}) \, = \\
\, \, λ \, n \, \bullet \, \IF \, n=0 \, \THEN \, 1 \, \ELSE \, n*\{0\mapsto 1\}(n-1) \, \END \, = \, \, \\
\, \, \{ \, n \, | \, n=0 \, \bguard \, 1, \, ¬(n=0) \, \bguard \, n=1 \, \bguard \, 1 \, \} \, = \\
\, \, \{ \, 0 \, \mapsto \, 1 \, , \, 1 \, \mapsto \, 1 \, \} \, \\
\end{array}$
Each successive approximation nibbles away at the over-deterministic part of the previous function, providing one more point where a result is known. In the limit, the result of applying $\nu F$ to any non-negative argument is known, However, application to a negative value remains overdeterministic, yielding $null$, in accordance with our descriptive requirements.
For a computational interpretation we choose $μF$, the weakest fixed point solution of $F(fact)=fact$. We make our first approximation $fail$, defined to be the function that returns $⊥$ everywhere. In this case each successive approximation replaces one point at which the previous approximation yielded $⊥$ with a point that yields a deterministic value. In the limit, the result of applying $μF$ to any non-negative argument is known, However, application to a negative value remains maximally non-deterministic, yielding ⊥, in accordance with our computational intuition.
In \cite{JLS12} Jones et al classify attempts to deal with undefined terms into three main categories: those that use a logic adapted to undefinedness, those which provide an arbitrary, and usually unknown, denotation for each undefined term, and those that deal with undefined terms at the level of predicates. We have reviewed examples of all three approaches above, and shown that bunch theory provides another approach which is completely different as {\em each term has a non-arbitrary denotation}. However, terms may be non-deterministic, which allows them to be either over-defined, to the point of non-existence, or under-defined in the case of ambiguity.
Whereas Jones et al advocate a logic adapted to undefinedness, bunch theory provides a theory of values which avoids undefinedness. In particular the use of $null$ and the improper bunch $⊥$ allows us to reason about the non-existent in a mathematically consistent way. The main adjustment required from the user of the theory is the loss of some laws, for example $A \, < \, B \, ∨ \, A \, ≥ \, B$ which can be false when we are dealing with non-deterministic values, e.g. we have $¬(1,3 \, < \, 2)$ but also $¬(1,3 \, ≥ \, 2)$. But of course, all such laws are obeyed when we are dealing only with elements.
\subsection{Bunch theory and programming language semantics}
Within the semantics of a programming language we can use bunches to model non-determinism, and to express the results of a backtracking search carried our by a reversible computation.
In Section \ref{descriptions} we introduced non-deterministic functions, whose application may yield a bunch of values. To interpret recursive function descriptions, we took the maximally non-deterministic function $fail$ as a first approximation in the construction of the weakest fixed point, in order to obtain a solution that accords with out computational intuition.
Our agenda in this section will first of all be to see how
non-deterministic or over deterministic values can be accommodated within the weakest pre-condition (WP) semantics used in the B-Method. We will then go on to derive, from predicate transformer semantics, an alternative “prospective value” semantics, equivalent in expressive power over the semantic components of B, but which also enables us to extend the expression language of B in an interesting way to express the results of a backtracking search and preferential choice.
Before proceeding, we review some bunch theory results needed for the development of these theories.
A bunch is said to be atomic if it cannot be formed by the union of two non-null bunches which are both different from itself. Thus $z$ is atomic if $z \, = \, A,B \, ⇒ \, z:A \, ∨ \, z:B$.
Elements are atomic; the null bunch is atomic; the improper bunch is atomic.
The atomicity of the improper bunch is related to its absorptive properties, e.g. $⊥ \, \setminus A \, = \, ⊥ \, $. Indeed, although $A:⊥ \, $ for any bunch $A$, if $A \, ≠ \, null$ our formalism gives us {\em no way} to express the elements that are part of $⊥ \, $ but not part of $A$.
If $α$ and $β$ are atomic bunches then $α \, \mapsto \, β$ is an atomic bunch.
For any atomic bunch $z$ we have the bunch comprehension property:
\[z \, : \, ∮ \, x \, \bullet \, E \, \, ⇔ \, \, (∃ \, x \, \bullet \, z:E) \, \]
Recalling that the bunch comprehension $∮ \, x \, \bullet \, E$ is the bunch formed from all values of $E$ as $x$ ranges over its type, the bunch comprehension property tells us that if $z$ is a sub-bunch of the bunch comprehension, there must be some value of $x$ for which $z:E$. This is intuitively obvious for elements; where $z$ is the improper bunch it means that there is some $x$ which yields the improper bunch {\em all at once}.
Atomicity also relates to bunch inclusion, We have $A:B$ if, for an arbitrary atomic bunch $z$, $z:A \, ⇒ \, z:B$. Bunches $A$ and $B$ are equal if $A:B \, ∧ \, B:A$. i.e. if $z:A \, ⇔ \, z:B$.
We note that $⊥ \, : \, A$ is equivalent to $⊥ \, = \, A$, since $A \, : \, ⊥ \, $ is true for any bunch $A$.
Atomicity is mainly important because it allows us to write proofs without taking the improper bunch as a special case.
\subsubsection{Non-deterministic assignments}
We write $[S]Q$ for the condition that must hold before operation $S$ in order to ensure that predicate $Q$ will hold afterwards. For the assignment $x:=F$ this condition, as given in the B-Book\cite{JRA96}, is as follows:
\[[x:=F]Q \, \, \eq \, \, Q[F/x] \, \, \]
Now if $F$ can be a bunch of values, each of which represents some value which $F$ might take, we require, in order to guarantee $Q$ after $S$, that $Q$ would hold for each and all of the values comprising $F$, so our law becomes:
\[[x:=F]Q \, \, \eq \, \, ∀ \, x' \, \bullet \, x':F \, ⇒ \, Q[x'/x] \, \]
Here we have chosen $x'$ as the bound variable name to distinguish it from the program variable name $x$. If we choose to conflate the names the law appears simpler. Noting that $x$ is not free in the LHS of the above formula we have:
$\begin{array}{l} ∀ \, x' \, \bullet \, x':F \, ⇒ \, Q[x'/x] \, \, \eq \, \, \text{“change of bound variable name”} \\
∀ \, x \, \bullet \, x:F \, ⇒ \, Q[x'/x][x/x'] \, \, \eq \, \, \text{“resolving substitutions”} \\
∀ \, x \, \bullet \, x:F \, ⇒ \, Q \\
\end{array}$
and our law for assignment becomes:
\[[x:=F]Q \, \, \eq \, \, ∀ \, x \, \bullet \, x:F \, ⇒ \, Q \, \]
Note that we follow Abrial \cite{JRA96} in using $x$ to denote a program variable or {\em variable list}.
\subsubsection{Prospective values}
If $S$ is an operation, we write $S \, \diamond \, E$ for the value expression $E$ would take were program $S$ to be executed. We call $S \, \diamond \, E$ the {\em prospective value} of $E$ following $S$. For example $x:=2 \, \diamond \, x+10 \, \, \eq \, \, 12$. Where $S$ is non-deterministic, this will be reflected, for suitable $E$, in $S \, \diamond \, E$ being a non-elemental bunch.
For example $x:=1 \, ⊓ \, x:=2 \, \diamond \, x+10 \, \, \eq \, \, 11,12$
We will derive the rules for prospective values from those for a WP calculus, which, incorporating the new rule for non-deterministic assignment given above, and omitting a now redundant rule for unbounded non-determinism, we will take as follows:
$\begin{array}{llc} \text{Name} \, & \, \text{Rule} \, & \, \\[5pt]
\text{skip} \, & \, [skip]Q \, \eq \, Q \, & \\
\text{assignment} \, & \, [x:=F]Q \, \eq \, ∀ \, x \, \bullet \, x:F \, ⇒ \, Q \\
\text{pre-condition} \, & \, [P|S]Q \, \eq \, \, P \, ∧ \, [S]Q \, & \\
\text{guard} \, & \, [P \, \Guard S]Q \, \eq \, P \, ⇒ \, [S]Q \, & \, \\
\text{bounded choice} \, \, & \, \, [S \, ⊓ \, T]Q \, \eq \, [S]Q \, ∧ \, [T]Q \, & \\
\text{seq comp} \, & \, [S \, \asemi \, T]Q \, \, \eq \, \, [S][T]Q \, & \\
\end{array}$
We have a dual set of rules for the conjugate weakest pre-condition (CWP), $⟨S⟩Q$, the condition that $Q$ {\em might} be true after $S$. We obtain the CWP of $S$ from the WP of $S$ according to:
\[⟨S⟩Q \, \, \eq \, \, ¬[S]¬Q \, \, \]
where the double negation corresponds to that seen in de-Morgan's laws, or more generally to that seen in changing from universal to existential quantification. We see an example for the first case in the derivation of the CWP law for bounded choice:
$\begin{array}{l} ⟨S \, ⊓ \, T⟩Q \, \, \eq \, \, \text{“defn of CWP”} \\
¬[S⊓T]¬Q \, \, \eq \, \text{“WP law for bounded choice”} \\
¬([S]¬Q \, ∧ \, [T]¬Q) \, \eq \, \, \text{“logic - de Morgan”} \\
¬[S]¬Q \, ∨ \, ¬[T]¬Q \, \, \eq \, \, \text{“defn of CWP”} \\
⟨S⟩Q \, ∨ \, ⟨T⟩Q \\
\end{array}$
\subsubsection{A basic law linking prospective values and CWP}
We now give an intuitive law that links prospective values with CWP. For any atomic bunch $z$ we have:
\[z \, : \, (S \, \diamond \, E) \, \, \, \eq \, \, ⟨S⟩z:E \, \, \, \, \text{“The basic law”}\]
In Appendix \ref{basic law} we prove this law from an explicit definition for $S \, \diamond \, E$. The basic law allows us to derive rules for determining $S \, \diamond \, E$ over the semantic constructs of our language.
\subsubsection{Derivation of the rules for $S \, \diamond \, E$}
We use the basic law to derive the following rules.
$\begin{array}{llc} \text{Name} \, & \, \text{Rule} \, & \, \\[5pt]
\text{skip} \, & \, skip \, \diamond \, E \, \, \eq \, \, E \, & \\
\text{assignment} \, & \, x:=F \, \diamond \, E \, \, \eq \, (λx.E)(F) \\
\text{pre-condition} \, & \, P \, | \, S \, \diamond \, E \, \, \eq \, \, P \, \bpre \, (S \, \diamond \, E) \, & \\
\text{guard} \, & \, P \, \Guard S \, \diamond \, E \, \, \eq \, \, P \, \bguard \, (S \, \diamond \, E) \, & \, \\
\text{bounded choice} \, \, & \, \, S \, ⊓ \, T \, \diamond \, E \, \, \eq \, \, (S \, \diamond \, E) \, , \, (T \, \diamond \, E) \, \\
\text{seq comp} \, & \, S \, \asemi \, T \, \diamond \, E \, \, \eq \, \, S \, \diamond \, T \, \diamond \, E& \\
\end{array}$
The precedence\footnote{A full precedence table for our notation is given in Appendix \ref{precedence}.} of $\diamond $ is below that of programming connectives, whose precedence, in descending order, is $:= \, , \, \Guard , \, ⊓ \, , \, \asemi \, , \, |$. We follow Hehner in introducing a large equals $\eq$, which is a low precedence symbol used in equational reasoning. When written between expression or predicates it indicates that they are equivalent.
Our derivations are based on the proposition that for any bunches $A$ and $B$, and for $z$ being an atomic bunch we have:
$A \, = \, B \, \, ⇔ \, \, (z:A \, ⇔ \, z:B)$.
For $skip$ we have:
$\begin{array}{l} z \, : \, (skip \, \diamond \, E) \, \, \eq \, \, \text{“basic law”} \\
⟨skip⟩z:E \, \, \eq \, \, \text{“CWP rule} \, ⟨skip⟩Q \, ⇔ \, Q \, \text{”} \\
z:E \, \text{ “and thus”} \, \, skip \, \diamond \, E \, \, \eq \, \, E \\
\end{array}$
For assignment and unbounded choice we have:
$\begin{array}{l} z \, : \, (x:=F \, \diamond \, E) \, \, \eq \, \, \text{“basic law”} \\
⟨x:=F⟩z:E \, \, \eq \, \, \text{“CWP rule} \, ⟨x:=F⟩Q \, ⇔ \, ∃x\bullet x:F \, ∧ \, Q \, \text{”} \\
∃x \, \bullet \, x:F \, ∧ \, z:E \, \, \eq \, \, \text{“property of bunch guard”} \\
∃x \, \bullet \, z \, : \, x:F \, \bguard \, E \, \, \eq \, \, \text{“property of bunch comprehension”} \\
z \, : \, ∮ \, x \, \bullet \, x:F \, \bguard \, E \, \, \text{“and thus”} \\
x:=F \, \diamond \, E \, \, \eq \, \, ∮ \, x \, \bullet \, x:F \, \bguard \, E \, \\
\end{array}$
For a pre-conditioned operation we have:
$\begin{array}{l} z \, : \, (P|S \, \diamond \, E) \, \, \eq \, \, \text{“basic law”} \\
⟨P|S⟩z:E \, \, \, \eq \, \, \text{“CWP rule} \, ⟨P|S⟩Q \, \, ⇔ \, \, P \, ⇒ \, ⟨S⟩Q \, \text{”} \\
P \, ⇒ \, ⟨S⟩z:E \, \, \, \eq \, \, \, \text{“logic”} \\
¬P \, ∨ \, ⟨S⟩z:E \, \, \, \eq \, \, \, \text{“since } \, ¬P \, ⇔ \, z \, : \, ¬P \, \bguard \, ⊥ \, \text{”} \\
z \, : \, ¬P \, \bguard \, ⊥ \, \, ∨ \, \, ⟨S⟩z:E \, \, \, \eq \, \, \text{“basic law”} \\
z \, : \, ¬P \, \bguard \, ⊥ \, \, ∨ \, \, z \, : \, (S \, \diamond \, E) \, \, \eq \, \text{“since } \, z:A \, ∨ \, z:B \, \, ⇔ \, \, z:A,B \, \text{”} \\
z \, : \, ¬P \, \bguard \, ⊥ \, , \, (S \, \diamond \, E) \, \, \eq \\
\text{“by defn of bunch pre-condition} \, P \, \bpre \, A \, = \, ¬P \, \bguard \, ⊥ \, , \, A \, \, \text{”} \, \\
z \, : \, P \, \bpre \, \, (S \, \diamond \, E) \, \, \text{“and thus”} \\
P|S \, \diamond \, E \, \, \eq \, \, P \, \bpre \, \, (S \, \diamond \, E) \\
\end{array}$
For a guarded operation we have:
$\begin{array}{l} z \, : \, (P \, \Guard S \, \diamond \, E) \, \, \eq \, \, \text{“basic law”} \\
⟨P \, \Guard S⟩z:E \, \, \, \eq \, \, \text{“CWP rule} \, ⟨P \, \Guard S⟩z:E \, \, ⇔ \, \, P \, ∧ \, ⟨S⟩Q \, \text{”} \\
P \, ∧ \, ⟨S⟩z:E \, \, \, \eq \, \, \text{“basic law”} \\
P \, ∧ \, z \, : \, (S \, \diamond \, E) \, \, \eq \, \, \text{“property of bunch guard”} \\
z \, : \, P \, \bguard \, (S \, \diamond \, E) \, \text{“and thus”} \, \, \\
P \, \Guard S \, \diamond \, E \, \, \eq \, \, P \, \bguard \, (S \, \diamond \, E) \\
\end{array}$
For bounded choice:
$\begin{array}{l} z \, : \, (S \, ⊓ \, T \, \diamond \, E) \, \, \eq \, \, \text{“basic law”} \\
⟨S \, ⊓ \, T⟩z:E \, \, \, \eq \, \, \text{“CWP rule} \, ⟨S \, ⊓ \, T⟩Q \, \, ⇔ \, \, ⟨S⟩Q \, ∨ \, ⟨T⟩Q \, \text{”} \\
⟨S⟩z:E \, ∨ \, ⟨T⟩z:E \, \, \eq \, \, \text{“basic law”} \\
z \, : \, (S \, \diamond \, E) \, \, ∨ \, \, z \, : \, (T \, \diamond \, E) \, \, \eq \, \, \text{“since } \, z:A \, ∨ \, z:B \, \, ⇔ \, \, z:A,B \, \text{”} \\
z \, : \, (S \, \diamond \, E) \, , \, (T \, \diamond \, E) \, \text{“and thus”} \\
S \, ⊓ \, T \, \diamond \, E \, \, \, \eq \, \, (S \, \diamond \, E) \, , \, (T \, \diamond \, E) \, \\
\end{array}$
And for sequential composition:
$\begin{array}{l} z \, : \, (S \, \asemi \, T \, \diamond \, E) \, \, \eq \, \, \text{“basic law”} \\
⟨S \, \asemi \, T⟩z:E \, \, \, \eq \, \, \text{“CWP rule} \, ⟨S\asemi T⟩Q \, ⇔ \, ⟨S⟩⟨T⟩Q \, \text{”} \\
⟨S⟩⟨T⟩z:E \, \, \, \, \eq \, \, \text{”basic law“} \\
⟨S⟩ \, z \, : \, (T \, \diamond \, E) \, \, \eq \, \, \text{“basic law and right assoc of} \, \diamond \, \text{”} \\
z \, : \, (S \, \diamond \, T \, \diamond \, E) \, \, \text{“and thus”} \\
S \, \asemi \, T \, \diamond \, E \, \, \, \eq \, \, S \, \diamond \, T \, \diamond \, E \, \\
\end{array}$
The attentive reader will have noted that these semantic components do not include selection and iteration constructs. These are handled by means of choice and guard. \footnote{This decomposition was first proposed by Hehner \cite{ECRH93,HEHNER06} who used predicative semantics. Abrial adapted it to predicate transformer semantics for use in in the B-Method \cite{JRA96}.}
The $\IF$ construct is defined as:
\[\IF \, g \, \THEN \, S \, \ELSE \, T \, \END \, \, \defs \, \, g \, \Guard S \, \, ⊓ \, \, \, ¬g \, \Guard T \, \]
Let's see how this works when evaluating the prospective value
of expression $E$ after an $\IF$ construct:
$\begin{array}{l} \, \, \IF \, g \, \THEN \, S \, \ELSE \, T \, \END \, \diamond \, E \, \eq \, \q{by defn of \IF} \\
\, \, g \, \Guard S \, \, ⊓ \, \, \, ¬g \, \Guard T \, \, \diamond \, E\eq \, \, \q{by rule for bounded choice} \\
\, \, (g \, \Guard S \, \diamond \, E) \, , \, (¬g \, \Guard T \, \diamond \, E) \, \, \eq \, \, \q{by rule for guard} \\
\, \, g \, \bguard \, (S \, \diamond \, E) \, , \, ¬g \, \bguard \, (T \, \diamond \, E) \\
\end{array}$
When $g$ is true, the properties of the bunch guard tell us that this reduces to $(S \, \diamond \, E) \, , \, null$, i.e. to $S \, \diamond \, E$. In this case the $\ELSE$ clause contributes nothing to the result, and our ability to express this nothing by means of the empty bunch $null$ is essential to our formulation. Similarly, when $g$ is false the construct reduces to $null \, , \, (T \, \diamond \, E)$, i.e. to $T \, \diamond \, E$. In general, a command $g \, \Guard S$ is said to be feasible when $g$ holds and infeasible otherwise. The command $false \, \Guard skip$ is always infeasible, and can never contribute to a result. Taking an extreme example, which will shortly become relevant to our argument, $false \, \Guard skip \, \diamond \, ⊥ \, \, \eq \, null$. Within the conventional semantics of a programming language, the command $false \, \Guard skip$ has no interpretation as "code".
\subsubsection{Provisional choice and backtracking.}
The semantics of choice, which we have used to incorporate demonic non-determinism into our language, can be used to describe provisional choice, as used in a backtracking application. This idea has a long history. As far back as 1967, in his paper ``Non-deterministic Algorithms'' \cite{RWF67}, Floyd talked of ``programs governed in part .. by final causes for the sake of which their effects are carried out''. In ``The Specification Statement''\cite{CM88} Carroll Morgan mentions the possibility as follows: ``Ordinarily we limit the syntax of our programming language so that miracles cannot be written in it. If we relax this restriction, allowing naked guarded commands, then operational reasoning suggests a backtracking implementation''. A similar possibility is noted by Eric Hehner in \cite{ECRH93}.
We have explored the possibility of exploiting a prospective value semantics to represent backtracking, and in particular the implementation of backtracking via reversible computing \cite{SZL06,SZD10,FZThesis}. In this approach, a naked guarded command
$g \, \Guard S$ will provoke reversal of computation if $g$ is false, and will execute as $S$ if $g$ is true. Reverse computation continues until a previous provisional choice is reached, at which point forward execution will recommence if a previously untried choice is available.
We have developed an implementation platform for this approach, in the form of a reversible virtual machine \cite{RVM2010}. it provides support for provisional choice and guards, reversible execution, and sets as data structures. The latter are used to provide a simple way of using the two different interpretations of choice within the same formal development framework. Thus to incorporate backtracking we extend the expression language of our implementations to include terms of the form $\{S \, \diamond \, E\}$, so that we might write as code an assignment such as:
\[x \, := \, \{S \, \diamond \, E\} \, ∪ \, \{T \, \diamond \, F\} \, \]
In the computation of $\{S \, \diamond \, E\}$, each time a way is found to complete the execution of $S$, the value of $E$ in the resulting after-state is calculated and added to the set of results being constructed. Execution is then reversed, so that all possible choices are explored. The topology of this execution is in the form of a tree, and ends when backwards execution finds no more unexplored choices. The value of the term $\{S \, \diamond \, E\}$ is then known, and forward execution can recommence {\em without the evaluation of term} $\{S \, \diamond \, E\}$ having caused any change in the program state (or, operationally speaking, any enduring change, since any changes are restored during reverse execution).
Thus we have a simple semantics which allows us to express non-determinism and demonic choice along with provisional choice and backtracking within the same development framework. However, in a term of the form $\{S \, \diamond \, E\}$ any choice within $S$ must be provisional choice rather than implementor's choice, and must not be subject to refinement.
\subsubsection{Preference as a refinement of provisional choice }
In G Nelson's generalisation of Dijkstra's WP calculus \cite{GN89}, we find a biased choice operator $S \, ⊞ \, T$. In a backtracking scenario, $S$ would be chosen in preference to $T$, but if $S$ is unable to produce a solution, $T$ will be tried instead. Unfortunately, Nelson's construct is limited by the fact that it is only $S$ which has to be able to find a solution. We would like to extend this idea to take account not only of $S$, but also of the rest of the program which follows. Nelson's biased choice is defined using the {\em feasibility} of $S$. We will first examine the idea of feasibility, and then extend it {\em to take account of the effect of any further computation,} which we refer to as the continuation. To achieve this we will use a construct which cannot be formulated in classical WP semantics, but which is made possible by our use of PV semantics and bunches.
Following Abrial we write the feasibility of $S$ as $fis(S)$ and recall that a program is feasible if it cannot establish false, i.e. $fis(S) \, \defs \, ¬[S]false$.
We also recall a monotonicity condition of the WP calculus, that if predicate $Q'$ is weaker than $Q$, i.e. if $Q \, ⇒ \, Q'$, a program able to establish $Q$ will also be able to establish $Q'$. Thus, since $false \, ⇒ \, Q$ for any predicate $Q$, a program able to establish the post condition $false$ could establish absolutely anything. The truths established in this way, often known as “miracles” \cite{MRG88}, are vacuous, and depend on the computation having no after states. Thus they may be compared to the true result obtained from universal quantification over an empty set. These {\em vacuous} truths play an essential role in our semantics. For example, in the decomposition, first proposed by Hehner\footnote{As recounted in \cite{HEHNER06}, this idea was first made public in a technical report because the reviewers of the paper in which it was proposed required it to be removed as a condition of acceptance.}, of a conditional $\IF \, g \, \THEN \, S \, \ELSE \, T \, \END$ into the guarded choice $g \, \Guard S \, ⊓ \, ¬g \, \Guard T$, we use a vacuous truth to express the contribution of the choice {\em which is not taken}.
In a backtracking interpretation, a program is infeasible if it is always forced to backtrack, and accordingly has no after-states. Using this idea, Nelson's biased choice can be defined as:
\[S \, ⊞ \, T \, \, \defs \, \, S \, ⊓ \, ¬fis(S) \, \Guard T \, \]
And we can clearly see that it is the feasibility of $S$ alone that guides the choice. We want to extend the idea of feasibility so it applies to the rest of the program, but first let us see how the predicate $¬fis(S)$ might be expressed in PV semantics. , starting from our CWP definition $fis(S) \, \defs \, ⟨S⟩true$ We have:
\[ ¬fis(S) \, \, \eq \, \, \text{“by defn of }fis(S)\text{”} \, \, ¬¬[S]false \, \, \eq \, \, \\
\text{“expressing in CWP”} \, \, ¬⟨S⟩true \, \, \eq \, \, \text{“since }z:⊥ \, \, \eq \, \, true\text{”} \, \, \\
¬⟨S⟩z:⊥ \, \, \, \eq \, \, \text{“basic law”} \, \, ¬ \, z \, : \, (S\diamond ⊥) \, \, \\
\eq \, \, \text{“since }z\text{ is arbitrary”} \, \, (S\diamond ⊥ \, ) \, : \, null \, \]
We would like to design a similar form of choice, which we will write as $\drangle $, but rather than looking just at the feasibility of $S$, we would like to consider the feasibility of $S$ along with any continuation of the program after the choice. Thus for the program $S \, \drangle \, T \, \asemi \, U$, (where choice “$ \, \drangle \, $” binds more tightly than operation sequence “$ \, \asemi \, $”) we would be interested in the feasibility of $S\asemi U$, and it would be the infeasibility of $S\asemi U$ that would force the choice of $T$. We propose the following definition of preferential choice
\[S \, \drangle \, T \, \diamond \, E \, \, \eq \, \, (S\diamond E) \, , \, (S\diamond E)=null \, \bguard \, (T\diamond E) \, \]
This executes $S$ in preference to $T$, but if execution of $S$ or its continuation results in backtracking to this point, $T$ is then executed. A simple example will illustrate how bunch theory allows the expression $E$ to represent the feasability of a continuation. We look at a program that would prefer the assignment $x:=1$ to $x:=2$, but is forced by a {\em future} guard to make the alternative choice.
\[ x:=1 \, \drangle \, x:=2 \, \, \asemi \, \, x=2\Guard skip \, \, \diamond \, \, x \, \, \, \, \, \, \eq \, \, \text{“PV rule for seq comp”} \\
x:=1 \, \drangle \, x:=2 \, \, \diamond \, \, x=2\Guard skip \, \diamond \, \, x \, \, \, \, \, \, \eq \, \, \text{“PV rule for guard”} \\
x:=1 \, \drangle \, x:=2 \, \, \diamond \, \, x=2 \, \bguard \, x \, \, \, \eq \, \, \text{“preferential choice”} \\
(x:=1 \, \diamond \, x=2 \, \bguard \, x), \, \\
(x:=1 \, \diamond \, x=2 \, \bguard \, x)=null \, \bguard \, (x:=2 \, \diamond \, \, x=2 \, \bguard \, x) \, \, \\
\eq \, \, \text{“PV rule for assignment x2”} \\
(1=2\bguard \, 1), \, ((1=2\bguard \, 1)=null) \, \, \bguard \, (2=2\bguard \, 2) \, \, \, \\
\eq \, \text{“evaluating guards”} \\
null \, , \, (null=null) \, \bguard \, (true \, \bguard \, 2) \, \, \, \eq \, \, \text{“further evaluation”} \\
2\]
In this example the message concerning the future evolution of the computation after the preferential choice is contained in the expression $x=2 \, \bguard \, x$. This has the value null (i.e. expresses non-existence) unless $x=2$, and in this way conveys that future execution must backtrack unless $x=2$.
We have seen that our attempt to capture preference in WP led us only to biased choice; we were unable to capture preference in WP. However, preference occurs naturally in implementations, since these are intrinsically deterministic. We were able to capture preference in our PV semantics because in the term $S \, \diamond \, E$ the expression $E$ is able to represent the total future behaviour of the code following $S$ (its continuation). When $E=null$ this continuation is infeasible.
Preferential choice is easily shown to be a refinement of provisional choice. The condition that program $S$ is refined by program $T$, when both programs have a state variable or variable list $x$, is expressed in terms of PV semantics as (see appendix \ref{refinement}).
\( \, S \, ⊑ \, T \, \, \defs \, \, (T \, \diamond \, E) \, \, : \, \, (S \, \diamond \, E) \, \)
We can argue as follows:
$\begin{array}{l} S \, ⟩⟩ \, T \, \diamond \, E \, \, \eq \, \text{“defn of preferential choice”} \\
(S\diamond E),(S\diamond E)=null \, \bguard \, (T\diamond E) \, \, : \, \, \\
\text{“since }g \, \bguard \, β \, : \, β \, \text{ and } \, β' \, : \, β \, ⇒ \, α,β' \, : \, α,β \, \text{”} \\
(S\diamond E),(T\diamond E) \, \, \eq \, \text{“pv defn of non-deterministic choice”} \\
S \, ⊓ \, T \, \diamond \, x \, \\
\end{array}$
A feature of preferential choice is that the potential to revise choices is discarded when a program terminates, e.g. $x:=1 \, ⟩⟩ \, abort \, \diamond \, x \, \eq \, \, 1$ and the result holds no information on the potential for triggering $abort$. This implies that some housekeeping is needed to remove potential choices on termination. For example, in an implementation where backtracking makes use of a history stack, this could corresponds to the history stack being discarded when the program terminates.
Problems that may not be evident when a program is executed in isolation may be revealed when it is used as a component in a larger system. For example the program $S \, \defs \, x:=1 \, ⟩⟩ \, abort$ will cause an abort if it is run with a continuation which is infeasible when $x=1$. Our proof obligations must be augmented to reveal such potential problems; we need to show $S\diamond null \, = \, null$.
A very unusual property of preferenential choice is that it is non-monotonic. In WP semantics monotonicity is the property that where $S$ establishes $P$ and $P$ implies $Q$, then $S$ will also establish $Q$.
In our PV semantics this translates directly (see appendix \ref{monotonicity}) into the property:
\( \, E:F \, ⇒ \, (S\diamond E) \, : \, (S\diamond \, F) \, \)
An example of a non-monotonic computation is $S \, \defs \, skip \, ⟩⟩ \, abort$
Then, although $null \, : \, x \, $, we have $S\diamond null \, = \, ⊥$ but $S\diamond x \, = \, x$
Since monotonicity does not hold, neither does conjunctivity. However, we can prove a form of sub-conjunctivity, namely
\[(S \, \diamond \, E,F) \, \, : \, \, (S\diamond E),(S\diamond F) \, \]
A conjunctivity counter example involving only terminating computations is:
$\begin{array}{l} x:=0 \, ⟩⟩ \, x:=1 \, \diamond \, \, \, x>0 \, \bguard \, x \, \, , \, \, y \, \, \, \eq \, \, \, y \\
x:=0 \, ⟩⟩x:=1 \, \, \diamond \, \, \, x>0 \, \bguard \, x \, \, \, \eq \, \, \, x \\
x:=0 \, ⟩⟩x:=1 \, \, \diamond \, \, \, y \, \, \, \eq \, \, \, y \, \\
\end{array}$
\subsubsection{Using bunch properties in the formulation of probabilistic choice.}
In classical probability theory, if $X$ is a random variable that takes value $x_1{}$ with probability $p$ and value $x_2{}$ with probability $1-p$, then the “expected value” of $X$ is given by the weighted addition $\Exp \, (X) \, = \, x_1{} \, \, _p\!\!+ \, x_2{}$
where $x_1{} \, \, _p\!\!+ \, \, x_2{} \, \, = \, \, p*x_1{} \, + \, (1-p)*x_2{}$
In \cite{SPECIALPROB} we formulate a probabilistic choice between programs, where for feasible continuations, $S \, _p\!⊕ \, T$ will choose execution of $S$ with probability $p$ and $T$ with probability $1-p$. We define the expectation of some expression $X$ (of suitable type) after executing such a choice as a weighted addition. For $0<p<1$ this expectation\footnote{In \cite{SPECIALPROB} we use the notation $\Exp(S\diamond X)$ for the expected value of $X$ after executing $S$. That notation resembles the $E(X)$ of probability theory, but is not compositional, so we change it here to $S \, \diamond _E \, X$.} is given by:
\[S \, _p\!⊕ \, T \, \diamond _E \, X \, \defs \, (S \, \diamond _E \, X) \, \, _p\!\!+ \, \, (T \, \diamond _E \, X) \, \]
Where $S$ and/or $T$ involve non-determinism their expectations will be a bunch of values, and the bunch lifting of $_p\!+$ is all that is needed to integrate probabilistic and non-deterministic choice.
However, that is not quite enough to describe the backtracking behaviour of our reversible machine. If a probabilistic choice leads to infeasibility, then execution will reverse to the point of probabilistic choice and take the other choice. We incorporate this into our weighted choice by expressing a weighted choice as a bunch of three terms. We are using the same technique we previously showed for preferential choice.
\[X_1{} \, _p\!\!+ \, X_2{} \, \defs \, X_1{} \, = \, null \, \bguard \, X_2{} \, , \, X_2{} \, = \, null \, \bguard \, \, X_1{} \, , \, \\
\, \, \, \, \, \, \, \, \, \, \, p*X_1{}+(1-p)*X_2{} \, \]
Where $X_1{}$ and $X_2{}$ are non-null, this corresponds to the probabilistic choice not leading to infeasibility. The first two terms then equate to $null$ and do not contribute to the result, which is given by the third term. If either $X_1{}$ or $X_2{}$ is $null$, then, by the absorptive properties of $null$, the third term will be $null$ and the result will be given by the first two terms, at most one of which will be non-null.
Finally we need to consider what our expectation should be if a probabilistic choice could lead to an aborting computation. Our approach is that any possibility of abort is counted as abort. To achieve this needs no further modification of our weighted addition. If either $X_1{}$ or $X_2{}$ describes an abortive continuation, its value will be $⊥ \, $. The term $p*X_1{}+(1-p)*X_2{}$ will then be $⊥ \, $ (by the absorptive power of $⊥ \, $), and the whole weighted addition will equate to $⊥ \, $.
Through use of bunches we have been able to capture interactions between probabilistic choice, non-deterministic choice, feasibility and aborting behaviour {\em in the world of values.}
\section{Extending axiomatic set theory to incorporate bunch theory}
Hehner gives an axiomatisation in which bunch theory is presented as an independent, stand alone theory, to which the axioms of set theory may subsequently be added. Here we take a different approach in which we add axioms to set theory to capture the idea of a bunch as the contents of a set. We choose the formalisation of set theory given by Abrial in the B-Book\cite{JRA96}\footnote{We conjecture that the same approach can be used with any axiomatisation of set theory.}.
We must express one of Abrial's axioms differently for it to be meaningful in the target language of bunch theory. In the B-Book\cite{JRA96} Abrial writes the axiom of choice as: $∃x \, \bullet \, x \, ∈ \, s \, ⇒ \, choice(s) \, ∈ \, s$ where $x∖s$. Since $null∈s$ vacuousy in bunch theory, once bunches are introduced Abrial's form of the axiom allows $choice(s) \, = \, null$. We use an equivalent form that forces $choice(s)$ to be an element. To prove the equivalence of the two forms of this axiom, abstract them as $ \, a \, ⇒ \, b$ and $a \, ⇒ \, c$, note that $b \, ⇔ \, c$ by the one point rule,\footnote{$(∃ \, x \, \bullet \, \, x=E \, ∧ \, P \, ) \, \, ⇔ \, \, P[E/x] \, \, \, \, \, x∖E$} then note that by propositional logic:
$(b \, ⇔ \, c) \, ⇒ \, (a⇒c \, ⇔ \, b⇒c)$
We now state our axioms:
$\begin{array}{llc} \text{Name} \, & \, \text{Rule} \, & \, \text{Condition} \\
\text{Ordered pair} \, & \, E\mapsto F \, ∈ \, (s \, × \, t) \, ⇔ \, E \, ∈ \, s \, ∧ \, F \, ∈ \, t \\
\text{Powerset} \, \, \, \, \, & \, s \, ∈ \, \pow (t) \, \, ⇔ \, \, (∀ \, x \, \bullet \, x \, ∈ \, s \, ⇒ \, x \, ∈ \, t) \, & \, x∖(s,t) \\
\text{Comprehension} \, & \, E \, ∈ \, \{x|x \, ∈ \, s \, ∧ \, P\} \, ⇔ \, E \, ∈ \, s \, \, ∧ \, \, P[E/x] \, & \, x∖s \\
\text{Set equality} \, & \, \, (∀ \, x \, \bullet \, x \, ∈ \, s \, ⇔ \, x \, ∈ \, t) \, ⇒ \, s=t \\
\text{Choice} \, & \, (∃x \, \bullet \, x \, ∈ \, s) \, ⇒ \, (∃x \, \bullet \, x \, ∈ \, s \, ∧ \, x \, = \, choice(s)) \, \, & \, x∖s \\
\text{BIG} \, \, \, \, & \, infinite(BIG) \, \\
\end{array}$
We add two axioms to characterise the meaning of $infinite$, a detail which is omitted from the B Book.
$\begin{array}{llc} \text{Infinity 1} \, & \, infinite(s) \, ⇒ \, (∃ \, x \, \bullet \, x \, ∈ \, s) \\
\text{Infinity 2} \, & \, infinite(s) \, ⇔ \, infinite(\{x \, | \, x \, ∈ \, s \, ∧ \, x \, ≠ \, choice(s)\}) \\
\end{array}$
We now give the additional axioms which enable us to incorporate bunch theory. We keep the number of axioms to a minimum and we rely on post-hoc definitions to introduce many of the notations associated with bunches, including bunch union and intersection, bunch inclusion, the null bunch, and the lifted nature of set membership within our bunch theory. This approach facilitates validation of our model and lowers the risk of missing axioms - since what might have been candidates for axioms become properties provable from post-hoc definitions.
$\begin{array}{llc} \text{Name} \, & \, \text{Rule} \, & \, \text{Condition} \, \\
\text{Packaging 1} \, & \, \{\unpack A\} \, = \, A \, & \, A \, \text{an element and a set} \, \\
\text{Packaging 2} \, & \, \unpack \{E\} \, = \, E \, \\
\text{Element 1} \, & \, \unpack A \, \text{is an element iff} \, A \, \text{is a singleton set.} \, \\
\text{Element 2} \, & \, \{E\} \, \text{is an element} \\
\text{Guard 1} \, & \, g \, \, \, \, \, ⇒ \, \, \, \, \, g \, \bguard \, E \, \, = \, \, E \\
\text{Guard 2} \, & \, ¬g \, \, \, \, \, ⇒ \, \, \, \, \, g \, \bguard \, E \, \, = \, \, \unpack \{ \, \} \\
\end{array}$
The packaging axioms introduce the unpacking operator $\unpack $, and the use of set brackets to “package” a bunch. They tell us that packaging and unpackaging are inverses. That is not quite enough to characterise packaging - indeed these axioms would be true if neither packaging nor unpackaging had any effect; this is ruled out by the element axioms. The first element axiom tells us that the landscape of set theory extended with bunches contains mathematical objects not present in classical set theory, namely those values obtained by unpacking non-singleton sets.
In the second guarded bunch axiom the term $\unpack \{ \, \}$ can be read as $null$, but we cannot write it that way as $null$ is not yet defined.
\section{Model}
The aim of our model is to give the meaning of any expression or predicate of our source language, namely the language of bunch theory, in terms of a more well established object language. For our object language we choose Abrial's axiomatisation of set theory.
We provide rules to give the meaning of any expression or predicate in our source language in terms of its syntactic components: e.g. we would give the meaning of an expression that has the form $E \, \mapsto \, F$ in terms of the meanings of $E$ and $F$ and the semantics of the maplet symbol. Thus our semantics is compositional and based on the denotational rules we give for each abstract syntax form in our source language.
We prove that each axiom of our source language holds when translated into the object language of our model. What this achieves is to show the relative consistency of our bunch theory with respect to the set theory of our object language, i.e. that no inconsisency is introduced by adding the axioms of bunch theory to those of set theory.
\subsection{Variables, environments and bindings}
The simplest components in our compositional semantics are identifiers naming constants, and variables.
Examples of constants are the numbers, 1, 2, 1008, etc.
and strings, “John Smith” etc. and the named elements of given sets. These will not present us with any problems when we come to write our rules.
Examples of variables are $x$, $y$ etc. Such identifiers may vary in meaning between texts, and within a single text may be different at different points due to variable capture in quantifications.
We call a particular association between variable names and their values an “environment”. An environment which associates the name $x$ with $1,2$ and the name $y$ with 3 will be written as:
\( \, \lbb \, x \, \leadsto \, \{1,2\}, \, \, y \, \leadsto \, \{3\} \, \rbb \, \)
In the above environment, $x$ is “bound” to the value $\{1,2\}$. In a term such as $x \, \leadsto \, \{x'\}$ the identifier to the left of the binding symbol $\leadsto $ is a name, and the term to its right is a mathematical expression in the target language.
Within quantified predicates or expressions we may experience variable capture, where a quantified variable has the same name as some variable from an outer scope. Or we may experience an extension of an environment, where newly quantified variables are added. Both of these are expressed by “binding override”,written with the symbol $⊕$. For example:
\( \, \lbb \, x \, \leadsto \, \{1,2\}, \, \, y \, \leadsto \, \{3\} \, \rbb \, ⊕ \, \, \lbb \, \, y \, \leadsto \, \{4,5\}, \, z \, \leadsto \, \{2,5,7\} \, \rbb \, = \, \)
\( \, \, \lbb \, x \, \leadsto \, \{1,2\}, \, \, y \, \leadsto \, \{4,5\}, \, z \, \leadsto \, \{2,5,7\} \, \rbb \, \)
Given an environment $\rho $ which includes a variable with name $x$, then we write $\rho .x$ for the value associated with $x$ in $\rho $. For example:
\( \, \lbb \, x \, \leadsto \, \{1,2\}, \, \, y \, \leadsto \, \{3\} \, \rbb.x \, \, = \, \, \{1,2\} \, \)
\subsection{The rules of our model}
In the following, $c$ is an element and a constant; $x$ a variable; $E, \, F$ are general expressions; $s, \, t$ are elements and sets, $\rho $ is an environment, and $\mathcal{E} $ is a set of environments.
In the term $\llbracket E\rrbracket ^\nu (\rho )$, $E$ is an expression in the source language, and $\rho $ an environment which associates the free variables of $E$ with particular values. $\llbracket E\rrbracket ^\nu (\rho )$ represents the “value denotation” of expression $E$ in environment $\rho $.
Environments exist in the mathematical world of our object language of set theory, but their formation records values taken by variables in the source language of bunch theory. The binding $x \, \leadsto \, \{1,2\}$ records that the variable $x$ in the source language is associated with the bunch $1,2$.
If $E$ is composed entirely of constant terms, for example $3\mapsto 4$, it will not depend on an environment, and we can write its denotation as just $\llbracket E\rrbracket $.
$\llbracket P\rrbracket ^\tau (\mathcal{E} )$ represents the ``truth denotation” of predicate $P$, over the set of environments $\mathcal{E} $, its value being the subset of $\mathcal{E} $ consisting of those environments in which $P$ is true.
We present our rules a few at a time, and before each set of rules, we give explanations to explain the intuitions behind their formulation.
We first give the denotations for constants and variables.
The denotation of a constant is independent of its environment, for example 3 will denote $\{3\}$ in the object language of our model. Our semantics wraps each constant term in set brackets.
\( \, \llbracket c\rrbracket ^\nu (\rho ) \, = \, \llbracket c\rrbracket \, \, = \, \{c\} \, \)
For variables, the value represented is given directly by the environment. No wrapping in set brackets is needed in the following rule, as this is already present within the variable's binding.
\( \, \llbracket x\rrbracket ^\nu (\rho ) \, = \, \rho .x \, \)
We next give denotations for packing and unpacking.
To obtain the denotation of $\{E\}$ we wrap the
denotation of $E$ in brackets.
\( \, \llbracket \{E\}\rrbracket ^\nu (\rho ) \, = \, \{ \, \llbracket E\rrbracket ^\nu (\rho ) \, \} \, \)
For the denotation of unpacking we consider for the moment the unpacking of a single set $s$. The denotation of $s$ will be a singleton set, which we can unwrap by “choosing” its only element. Here we make use of the fact that, although the concept of unpacking a set does not, in general, exist in the set theory of our semantic universe, we can mimic it for the case of a singleton set.
\( \, \llbracket \unpack s\rrbracket ^\nu (\rho ) \, = \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \)
We now consider some further expressions which can be expressed without considering the denotation of predicates.
The maplet rule gives the denotation of $E \, \mapsto \, F$ for general expressions $E$ and $F$, which may be bunches with multiple elements. The values denoted by $E$ and $F$ in the semantic universe will be sets, and by taking the cross product of these we obtain the set denoting all maplets in bunch $E \, \mapsto \, F$.
\( \, \llbracket E \, \mapsto \, F\rrbracket ^\nu (\rho ) \, = \, \llbracket E\rrbracket ^\nu (\rho ) \, × \, \llbracket F\rrbracket ^\nu (\rho ) \, \)
For the denotation of an {\em element} which is a power set, we can allow ourselves to reflect that any elementary values we can represent in our source language of bunch theory will also exist in the set theory language of our semantic universe. Indeed, the term $choice(\llbracket s\rrbracket ^\nu (\rho ))$ will represent, in the semantic universe, exactly the value that we intend $s$ to represent in our source language under environment $\rho $. We call this the “facsimile” of $s$. We obtain our denotation by taking the power-set of this term
and enclosing it in set brackets.
\( \, \llbracket \pow (s)\rrbracket ^\nu (\rho ) \, = \, \{ \, \pow (choice(\llbracket s\rrbracket ^\nu (\rho ))) \, \} \, \)
For the cross product denotation, we form the terms $choice(\llbracket s\rrbracket ^\nu (\rho ))$ and $choice(\llbracket t\rrbracket ^\nu (\rho ))$ in the semantic universe, and, since these will have the same values as we intend for $s$ and $t$ under environment $\rho $ in the source language, we form the denotation by enclosing the cross product of the former terms in set brackets.
\( \, \llbracket s \, × \, t\rrbracket ^\nu (\rho ) \, = \, \{ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, × \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \, \)
For the denotation of $choice(s)$ we form the term $choice(\llbracket s\rrbracket ^\nu (\rho ))$ in the semantic universe, since this will have the value we intend for $s$ under environment $\rho $ in our source language. If this value is a non-empty set, we take the choice of this term, and form the singleton set containing this element. Else the denotation is an empty set.
$\begin{array}{l} \, \llbracket choice(s)\rrbracket ^\nu (\rho ) \, = \\
\, \, \, \IF \, \\
\, \, \, \, \, \, (∃ \, x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \\
\, \, \, \THEN \\
\, \, \, \, \, \, \{ \, choice(choice(\llbracket s\rrbracket ^\nu (\rho ))) \, \} \\
\, \, \, \ELSE \\
\, \, \, \, \, \, \{ \, \} \\
\, \, \, \END \\
\end{array}$
We next turn to “truth denotations” of fundamental predicates. Recall that given a set of environments $\mathcal{E} $ and a predicate $P \, $, $ \, \llbracket P\rrbracket ^\tau (\mathcal{E} )$ will be that subset of $\mathcal{E} $ containing environments in which $P$ is true.
\( \, \llbracket true\rrbracket ^\tau (\mathcal{E} ) \, = \, \mathcal{E} \, \, \, \, \, \, \)
\( \, \llbracket false\rrbracket ^\tau (\mathcal{E} ) \, = \, \{ \, \} \, \)
To express the semantics of equality we form the set comprehension of those environments from $\mathcal{E} $ for which the denotation of $E$ is equal to that of $F$.
\( \, \llbracket E \, = \, F\rrbracket ^\tau (\mathcal{E} ) \, = \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket E\rrbracket ^\nu (\rho ) \, = \, \llbracket F\rrbracket ^\nu (\rho ) \, \} \, \)
For set membership $E \, ∈ \, s$, $E$ should consist only of elements which belong to $s$. The denotation of $E$ in some environment $\rho $ will be the set containing these elements, and this must be a subset of the semantic facsimile of $s$.
\( \, \llbracket E \, ∈ \, s\rrbracket ^\tau (\mathcal{E} ) \, = \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket E\rrbracket ^\nu (\rho ) \, ⊆ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \} \, \)
We need a predicate to express that a value is an element. This will be the case when its denotation is a singleton set.
\( \, \llbracket element(E)\rrbracket ^\tau (\mathcal{E} ) \, = \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, card(\llbracket E\rrbracket ^\nu (\rho )) \, = \, 1 \, \} \, \)
Now composite predicates.
\( \, \llbracket ¬P\rrbracket ^\tau (\mathcal{E} ) \, = \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket P\rrbracket ^\tau \{\rho \} \, = \, \{ \, \} \, \} \, \)
\( \, \llbracket P \, ∧ \, Q\rrbracket ^\tau (\mathcal{E} ) \, = \, \llbracket P\rrbracket ^\tau (\mathcal{E} ) \, ∩ \, \llbracket Q\rrbracket ^\tau (\mathcal{E} ) \, \)
\( \, \llbracket P \, ∨ \, Q\rrbracket ^\tau (\mathcal{E} ) \, = \, \llbracket P\rrbracket ^\tau (\mathcal{E} ) \, ∪ \, \llbracket Q\rrbracket ^\tau (\mathcal{E} ) \, \)
For the guarded bunch $g\bguard \, E$ we need a way to say whether $g$ is true in a particular environment $\rho $. For this we apply the truth semantics of $g$ to the singleton set $\{\rho \}$. Where $g$ is true we have $\llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{\rho \}$.
\( \, \llbracket g\bguard \, E\rrbracket ^\nu (\rho ) \, = \, \IF \, \llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{\rho \} \, \THEN \, \llbracket E\rrbracket ^\nu (\rho ) \, \ELSE \, \, \{ \, \} \, \, \END \, \)
We next consider set comprehension, where we will need to employ binding override. We form, in the semantic universe, the facsimile of the set we are intending to represent in the source language, and we enclose this
within another layer of set brackets. To produce the facsimile of
$\{ \, x \, | \, x \, ∈ \, s \, ∧ \, P \, \}$
we use a set comprehension in which bound variable $x'$ ranges over the facsimile of $s$, and we retain those $x'$ for which our intention is that predicate $P$ is true in environment $\rho $ overridden with a binding of $x$ to $\{x'\}$. The trick for expressing this is to apply the truth semantics of $P$ to a singleton set of environments containing just $\rho $ with the binding for $x$ overridden by $\lbb x \, \leadsto \, \{x'\}\rbb$. If this yields an empty set, $P$ is false in $\rho $, otherwise it is true.
$\begin{array}{l} \llbracket \{ \, x \, | \, x \, ∈ \, s \, ∧ \, P\rrbracket ^\nu (\rho ) \, = \, \\
\, \, \, \, \, \, \, \, \, \, \, \{ \, \, \{ \, x' \, | \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ∧ \, \llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\})≠\{ \, \} \, \} \, \, \} \\
\end{array}$
The truth denotations for universally and existentially quantified predicates use similar techniques to those employed for set comprehension.
$\begin{array}{l} \llbracket ∀x \, \bullet \, x \, ∈ \, s \, ⇒ \, P\rrbracket ^\tau (\mathcal{E} ) \, = \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∀ \, x'\bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \\
\, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, ⇒ \, \, \llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\})≠\{ \, \}) \, \} \\
\end{array}$
$\begin{array}{l} \llbracket ∃x \, \bullet \, x \, ∈ \, s \, ∧ \, P\rrbracket ^\tau (\mathcal{E} ) \, = \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∃ \, x'\bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \\
\, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, ∧ \, \llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\})≠\{ \, \}) \, \} \, \\
\end{array}$
Where the predicate $P$ is $true$, the denotation for the existential predicate becomes:
\( \, \llbracket ∃ \, x \, \bullet \, x \, ∈ \, s\rrbracket ^\tau (\mathcal{E} ) \, = \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∃ \, x'\bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho ))) \, \} \, \)
We now consider the denotations of expressions and predicates subject to substitution of certain terms. For these, we capture the effect of the substitution through binding override.
\( \, \llbracket E[F/x]\rrbracket ^\nu (\rho ) \, = \, \llbracket E\rrbracket ^\nu (\rho \, ⊕ \, \lbb \, x \, \leadsto \, \llbracket F\rrbracket ^\nu (\rho ) \, \rbb) \, \)
\( \, \llbracket P[F/x]\rrbracket ^\tau (\mathcal{E} ) \, = \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \llbracket F\rrbracket ^\nu (\rho ) \, \rbb\}) \, ≠ \, \{\} \, \} \, \)
Our final two rules give the denotation of the set $BIG$ and the semantic characterisation of an infinite set. We use the naturals to construct the denotation of $BIG$. The idea here is just to provide an infinite set for the construction of mathematical objects.
\( \, \llbracket BIG\rrbracket ^\nu (\rho ) \, = \, \{ \, \nat \, \} \, \)
The semantic characterisation of an infinite set requires its facsimile in the semantic model to be infinite.
\( \, \llbracket infinite(s)\rrbracket ^\tau (\mathcal{E} ) \, = \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, infinite(choice(\llbracket s\rrbracket ^\nu (\rho ))) \, \} \, \)
\section{Proving the existence of a model}
So far we have given axioms for bunch theory, and given semantic rules for translating any expression or predicate in the basic language of bunch theory into the language of our semantic universe.
At this point, the key question is whether the semantic translations of the axioms of bunch theory yield predicates which can be proved to be true in the semantic domain. If we can establish this we will have proved that a model exists for our version of bunch theory.
All expressions in our source language which are intended to denote elements will have denotations which are singleton sets. The formal proof of this is by structural induction over the syntactic forms of the source language, appealing to the semantic rules, and with the base cases being for constants and variables.
We will use, without proof, the following lemmas.
\( \, \text{L1}. \, \, a \, × \, b \, \, ⊆ \, \, c \, × \, d \, \, ⇔ \, \, a \, ⊆ \, c \, \, ∧ \, \, b \, ⊆ \, d \, \)
\( \, \text{L2}. \, \, \{ \, x \, | \, x \, ∈ \, X \, ∧ \, P \, ∧ \, Q \, \} \, = \, \{ \, x \, | \, x \, ∈ \, X \, ∧ \, P \, \} \, ∩ \, \{ \, x \, | \, x \, ∈ \, X \, ∧ \, Q \, \} \, \)
\( \, \text{L3}. \, \, \text{If $a$ is a singleton set,} \, \, a \, = \, \{choice(a)\} \, \)
\( \, \text{L4}. \, \, \{a\} \, ⊆ \, B \, \, ⇔ \, \, a \, ∈ \, B \, \)
\( \, \text{L5}. \, \, a \, ∈ \, \pow (b) \, \, ⇔ \, \, a \, ⊆ \, b \, \)
\( \, \text{L6.} \, \, \{ \, x \, | \, x \, ∈ \, \{ \, e \, \} \, ∧ \, P \, \} \, ≠ \, \{ \, \} \, \, ⇔ \, \, P[e/x] \, \)
\( \, \text{L7.} \, \, \{ \, a \, \} \, ⊆ \, \{ \, b \, \} \, \, ⇔ \, \, a=b \, \)
\( \, \text{L8.} \, \, \{x|P\} \, ⊆ \, \{x|Q\} \, \, \, ⇔ \, \, \, P \, ⇒ \, Q \, \)
\( \, \text{L9.} \, \, \{ \, x \, | \, x \, ∈ \, S \, ∧ \, P \, \} \, = \, \{ \, x \, | \, x \, ∈ \, S \, ∧ \, Q \, \} \, \, \impliedby \, \, (P \, \iff \, Q) \, \)
Where an axiom has the form $P \, ⇔ \, Q$ we validate it within the model by showing \( \, \llbracket P\rrbracket ^\tau (\mathcal{E} ) \, = \, \llbracket Q\rrbracket ^\tau (\mathcal{E} \} \, \) for arbitrary $\mathcal{E} $.
Where an axiom has the form $P \, ⇒ \, Q$ we validate it by showing \( \, \llbracket P\rrbracket ^\tau (\mathcal{E} ) \, ⊆ \, \llbracket Q\rrbracket ^\tau (\mathcal{E} \} \, \) for arbitrary $\mathcal{E} $.
Where an axiom has the form $E=F$ we validate it by showing \( \, \llbracket E\rrbracket ^\nu (\rho ) \, = \, \llbracket F\rrbracket ^\nu (\rho ) \, \) for arbitrary $\rho $.
And where an axiom has the general form $P$ we validate it by showing \(\llbracket P\rrbracket ^\tau (\mathcal{E} ) \, = \, \mathcal{E} \) for arbitrary $\mathcal{E} $.
\subsection{Validation of set theory axioms}
It is no surprise to find that our set theory axioms can be validated; we already have faith in set theory! However, the validation provides assurance that our model is correct.
\subsubsection{Validation of the ordered pair axiom}
To validate \( \, E\mapsto F \, ∈ \, (s \, × \, t) \, \, ⇔ \, \, E \, ∈ \, s \, \, ∧ \, \, F \, ∈ \, t\)
We show:
\( \, \llbracket \, E\mapsto F \, ∈ \, (s \, × \, t)\rrbracket ^\tau (\mathcal{E} ) \, \, = \, \, \llbracket E \, ∈ \, s \, \, ∧ \, \, F \, ∈ \, t\rrbracket ^\tau (\mathcal{E} ) \, \)
Taking the LHS
$\begin{array}{l} \llbracket E\mapsto F \, ∈ \, (s \, × \, t)\rrbracket ^\tau (\mathcal{E} ) \, = \, \q{by semantics of set membership} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \llbracket E\mapsto F\rrbracket ^\nu (\rho ) \, ⊆ \, choice(\llbracket s \, × \, t\rrbracket ^\nu (\rho ) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by semantics of ordered pair and cross product} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \\
\, \, \, \llbracket E\rrbracket ^\nu (\rho ) \, × \, \llbracket F\rrbracket ^\nu (\rho ) \, ⊆ \, choice(\{choice(\llbracket s\rrbracket ^\nu (\rho ) \, × \, choice(\llbracket t\rrbracket ^\nu (\rho )\}) \, \\
\} \end{array}$
$\begin{array}{l}
= \, \q{applying choice and by lemma 1} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \\
\, \, \, \llbracket E\rrbracket ^\nu (\rho ) \, ⊆ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \, ∧ \, \, \llbracket F\rrbracket ^\nu (\rho ) \, ⊆ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \\
\} \end{array}$
$\begin{array}{l}
= \, \q{by lemma 2} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \llbracket E\rrbracket ^\nu (\rho ) \, ⊆ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \} \, \\
\, \, \, ∩ \, \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \llbracket F\rrbracket ^\nu (\rho ) \, ⊆ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by semantics of set membership} \end{array}$
$\begin{array}{l}
\llbracket E \, ∈ \, s\rrbracket ^\tau (\mathcal{E} ) \, ∩ \, \llbracket F \, ∈ \, t\rrbracket ^\tau (\mathcal{E} ) \, \, = \, \, \q{by semantics of $∧$} \end{array}$
$\begin{array}{l}
\llbracket E \, ∈ \, s \, \, ∧ \, \, F \, ∈ \, t\rrbracket ^\tau (\mathcal{E} ) \, \, \, \, \, _\square \, \, \, \\
\end{array}$
Here we have validated a more general result than the original
ordered pair axiom, since $E$ and $F$ in the above may be general
expressions rather than expressions that must represent elements.
\subsubsection{Validation of the power-set axiom}
To validate \( \, s \, ∈ \, \pow (t) \, \, ⇔ \, \, (∀ \, x \, \bullet \, x \, ∈ \, s \, ⇒ \, x \, ∈ \, t) \, \)
We show:
\( \, \llbracket s \, ∈ \, \pow (t)\rrbracket ^\tau (\mathcal{E} ) \, = \, \llbracket ∀ \, x \, \bullet \, x \, ∈ \, s \, ⇒ \, x \, ∈ \, t)\rrbracket ^\tau (\mathcal{E} ) \, \)
Taking LHS
$\begin{array}{l} \llbracket s \, ∈ \, \pow (t)\rrbracket ^\tau (\mathcal{E} ) \, = \, \, \q{by semantics of set membership} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \llbracket s\rrbracket ^\nu (\rho ) \, ⊆ \, choice(\llbracket \pow (t)\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by semantics of power-set constructor} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \llbracket s\rrbracket ^\nu (\rho ) \, ⊆ \, choice(\{\pow (choice(\llbracket t\rrbracket ^\nu (\rho ))\})\} \end{array}$
$\begin{array}{l}
= \, \q{applying choice} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \llbracket s\rrbracket ^\nu (\rho ) \, ⊆ \, \pow (choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by lemmas 0 and 3} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \{choice(\llbracket s\rrbracket ^\nu (\rho ))\} \, ⊆ \, \pow (choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \, \end{array}$
$\begin{array}{l}
= \, \q{by lemma 4} \, \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ∈ \, \pow (choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by lemma 5} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⊆ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \\
\end{array}$
Taking RHS, we show it equal to the same expression:
$\begin{array}{l} \llbracket ∀ \, x \, \bullet \, x \, ∈ \, s \, ⇒ \, x \, ∈ \, t)\rrbracket ^\tau (\mathcal{E} ) \, \end{array}$
$\begin{array}{l}
= \, \q{by semantics of universal quantification} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, (∀ \, x'\bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⇒ \\
\, \, \, \llbracket x \, ∈ \, t\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb x \, \leadsto \, \{x'\}\rbb\}) \, ≠ \, \{\}) \, \} \, \end{array}$
$\begin{array}{l}
= \, \q{by semantics of set membership} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \, (∀ \, x'\bullet x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⇒ \\
\, \, \, \{ \, \rho ' \, | \, \rho ' \, ∈ \, \{\rho \, ⊕ \, \lbb x \, \leadsto \, \{x'\}\rbb\} \, ∧ \, \llbracket x\rrbracket ^\nu (\rho ') \, ⊆ \, choice(\llbracket t\rrbracket ^\nu (\rho ') \, \} \, ≠ \, \{\}) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by lemma 6} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \, (∀ \, x'\bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⇒ \\
\, \, \, \llbracket x\rrbracket ^\nu (\rho \, ⊕ \, \lbb x \, \leadsto \, \{x'\}\rbb) \, \, ⊆ \, choice(\llbracket t\rrbracket ^\nu (\rho \, ⊕ \, \lbb x \, \leadsto \, \{x'\}\rbb)) \, \} \end{array}$
$\begin{array}{l}
= \, \q{taking denotation for $x$ and since $x$ not free in $t$} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \, (∀ \, x'\bullet x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⇒ \, \{x'\} \, ⊆ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by lemma 4} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \, (∀ \, x'\bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⇒ \, x' \, ∈ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by defining property of subset inclusion} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⊆ \, choice(\llbracket t\rrbracket ^\nu (\rho ) \, \} \, \, _\square \\
\end{array}$
\subsubsection{Validation of set comprehension axiom}
\(E \, ∈ \, \{x|x \, ∈ \, s \, ∧ \, P\} \, \, ⇔ \, \, E \, ∈ \, s \, \, ∧ \, \, P[E/x] \, \, \, \, \, \, \, \text{where} \, \, x∖s \, \, \)
We show:
\( \, \llbracket E \, ∈ \, \{x|x \, ∈ \, s \, ∧ \, P\}\rrbracket ^\tau (\mathcal{E} ) \, = \, \llbracket E \, ∈ \, s \, ∧ \, P[E/x]\rrbracket ^\tau (\mathcal{E} ) \, \)
Taking LHS
$\begin{array}{l} \llbracket E \, ∈ \, \{ \, x \, | \, x \, ∈ \, s \, ∧ \, P\}\rrbracket ^\tau (\mathcal{E} ) \, = \, \q{by semantics of set membership} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket E\rrbracket ^\nu (\rho ) \, ⊆ \, choice(\llbracket \{ \, x \, | \, x \, ∈ \, s \, ∧ \, P\}\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by semantics of set comprehension} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket E\rrbracket ^\nu (\rho ) \, ⊆ \, \\
\, \, \, choice( \\
\, \, \, \, \, \, \{ \, \{ \, x' \, | \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho ) \, ∧ \, \llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\}) \, ≠ \, \{\} \, \} \, \} \\
\, \, \, ) \, \\
\} \, \end{array}$
$\begin{array}{l}
= \, \q{taking choice of singleton set} \, \, \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket E\rrbracket ^\nu (\rho ) \, ⊆ \, \\
\, \, \, \{ \, x' \, | \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho ) \, ∧ \, \llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\}) \, ≠ \, \{\} \, \} \, \, \, \\
\} \end{array}$
$\begin{array}{l}
= \, \q{by lemma 4} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, choice(\llbracket E\rrbracket ^\nu (\rho )) \, ∈ \\
\, \, \, \{ \, x' \, | \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ∧ \, \llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\}) \, ≠ \, \{\} \, \} \\
\} \end{array}$
$\begin{array}{l}
\text{Now recalling axiom 3:} \end{array}$
$\begin{array}{l}
E \, ∈ \, \{ \, x \, | \, x \, ∈ \, s \, ∧ \, P \, \} \, \, ⇔ \, \, E \, ∈ \, s \, \, ∧ \, \, P[E/x] \end{array}$
$\begin{array}{l}
\text{applying this to} \end{array}$
$\begin{array}{l}
choice(\llbracket E\rrbracket ^\nu (\rho )) \, ∈ \, \\
\, \, \, \{ \, x' \, | \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ∧ \, \llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\}) \, ≠ \, \{\} \, \} \end{array}$
$\begin{array}{l}
\text{with:} \end{array}$
$\begin{array}{l}
choice(\llbracket E\rrbracket ^\nu (\rho )) \, \, \text{for} \, \, \, E \end{array}$
$\begin{array}{l}
x' \, \, \text{for} \, \, x \end{array}$
$\begin{array}{l}
choice(\llbracket s\rrbracket ^\nu (\rho )) \, \, \text{for} \, \, s \end{array}$
$\begin{array}{l}
\text{and } \, \llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\}) \, ≠ \, \{\} \, \, \text{for} \, \, P \end{array}$
$\begin{array}{l}
\text{the predicate } \, E \, ∈ \, s \, \, ∧ \, \, P[E/x] \, \text{ in the axiom becomes} \end{array}$
$\begin{array}{l}
choice(\llbracket E\rrbracket ^\nu (\rho )) \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \, ∧ \\
(\llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\}) \, ≠ \, \{\}) \, [choice(\llbracket E\rrbracket ^\nu (\rho )) \, / \, x'] \end{array}$
$\begin{array}{l}
\text{which after performing the indicated substitution becomes} \end{array}$
$\begin{array}{l}
choice(\llbracket E\rrbracket ^\nu (\rho )) \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \, ∧ \\
\llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{choice(\llbracket E\rrbracket ^\nu (\rho ))\} \, \rbb\}) \, ≠ \, \{\} \end{array}$
$\begin{array}{l}
\text{And thus, LHS} \, \, = \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, choice(\llbracket E\rrbracket ^\nu (\rho )) \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \, \\
∧ \, \llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{choice(\llbracket E\rrbracket ^\nu (\rho ))\} \, \rbb\}) \, ≠ \, \{\} \, \} \\
\end{array}$
We now take RHS and show it equal to the same expression:
$\begin{array}{l} \llbracket E \, ∈ \, s \, \, ∧ \, \, P[E/x]\rrbracket ^\tau (\mathcal{E} ) \, = \, \q{by semantics of $∧$} \end{array}$
$\begin{array}{l}
\llbracket E \, ∈ \, s\rrbracket ^\tau (\mathcal{E} ) \, \, ∩ \, \, \llbracket P[E/x]\rrbracket ^\tau (\mathcal{E} ) \end{array}$
$\begin{array}{l}
= \, \q{by semantic rules for set membership and substitution} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \llbracket E\rrbracket ^\nu (\rho ) \, ⊆ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \} \, \, \, \cap \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \llbracket P\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \llbracket E\rrbracket ^\nu (\rho ) \, \rbb\}) \, ≠ \, \{\} \, \} \, \, \end{array}$
$\begin{array}{l}
= \, \q{by property of set intersection} \end{array}$
$\begin{array}{l}
\text{LHS} \, \, _\square \\
\end{array}$
\subsubsection{Validation of the set equality axiom}
\((∀x \, \bullet \, x \, ∈ \, s \, \, ⇔ \, \, x \, ∈ \, t) \, ⇒ \, s=t\)
This axiom is often given as an equivalence rather than an implication. This is
not necessary as the right to left implication follows from the properties of
equality in our underlying logic. Nevertheless, it is this potentially stronger
result that we will validate at the semantic level. We will further modify our
axiom, to something obviously equivalent, so that it fits more conveniently with our
defined denotations. We will verify:
\((∀x \, \bullet \, x \, ∈ \, s \, \, ⇒ \, \, x \, ∈ \, t) \, ∧ \, (∀x \, \bullet \, x \, ∈ \, t \, ⇒ \, x \, ∈ \, s) \, \, ⇔ \, \, s=t\)
We show:
\( \, \llbracket (∀x \, \bullet \, x \, ∈ \, s \, \, ⇒ \, \, x \, ∈ \, t) \, ∧ \, (∀x \, \bullet \, x \, ∈ \, t \, ⇒ \, x \, ∈ \, s)\rrbracket ^\tau (\mathcal{E} ) \, \, = \, \, \llbracket s=t\rrbracket ^\tau (\mathcal{E} ) \, \)
Taking LHS
$\begin{array}{l} \llbracket (∀x \, \bullet \, x \, ∈ \, s \, \, ⇒ \, \, x \, ∈ \, t) \, ∧ \, (∀x \, \bullet \, x \, ∈ \, t \, ⇒ \, x \, ∈ \, s)\rrbracket ^\tau (\mathcal{E} ) \, \end{array}$
$\begin{array}{l}
= \, \q{by semantics of $∧$} \end{array}$
$\begin{array}{l}
\llbracket ∀x \, \bullet \, x \, ∈ \, s \, \, ⇒ \, \, x \, ∈ \, t\rrbracket ^\tau (\mathcal{E} ) \, ∩ \, \llbracket \, ∀x \, \bullet \, x \, ∈ \, t \, ⇒ \, x \, ∈ \, s\rrbracket ^\tau (\mathcal{E} ) \, \end{array}$
$\begin{array}{l}
= \, \q{by semantics of universal quantification} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \\
\, \, \, (∀x'\bullet \, \llbracket x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⇒ \, \llbracket x \, ∈ \, t\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\}) \, ≠ \, \{\}) \, \\
\} \\
\, \, \, \, \, \, ∩ \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \\
\, \, \, (∀x' \, \bullet \, \llbracket x' \, ∈ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, ⇒ \, \llbracket x \, ∈ \, s\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\}) \, ≠ \, \{\}) \, \\
\} \end{array}$
$\begin{array}{l}
= \, \q{by semantics of set membership and since $x$ not free in $s,t$} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \\
\, \, \, (∀x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⇒ \, \\
\, \, \, \, \, \, \{ \, \rho ' \, | \, \rho ' \, ∈ \, \{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\} \, ∧ \, \\
\, \, \, \, \, \, \, \, \, \llbracket x\rrbracket ^\nu (\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb) \, ⊆ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \\
\, \, \, \, \, \, \} \, ≠ \, \{\} \, \\
\, \, \, ) \\
\} \\
\, \, \, \, \, \, ∩ \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \\
\, \, \, (∀x' \, \bullet \, x' \, ∈ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, ⇒ \\
\, \, \, \, \, \, \{ \, \rho ' \, | \, \rho ' \, ∈ \, \{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\} \, ∧ \, \\
\, \, \, \, \, \, \, \, \, \llbracket x\rrbracket ^\nu (\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb) \, ⊆ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \\
\, \, \, \, \, \, \} \, ≠ \, \{\} \\
\, \, \, ) \, \\
\} \end{array}$
$\begin{array}{l}
= \, \q{taking denotation for $x$} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∀x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⇒ \\
\{ \, \rho ' \, | \, \rho ' \, ∈ \, \{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\} \, ∧ \, \{x'\} \, ⊆ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \, ≠ \, \{\}) \, \} \\
∩ \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∀x' \, \bullet \, x' \, ∈ \, choice(\llbracket t\rrbracket ^\nu (\rho ) \, ⇒ \\
\{ \, \rho ' \, | \, \rho ' \, ∈ \, \{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\} \, ∧ \, \{x'\} \, ⊆ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \} \, ≠ \, \{\}) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by lemma 6} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∀x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⇒ \, \{x'\} \, ⊆ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \\
∩ \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∀x'\bullet \, x' \, ∈ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, ⇒ \, \{x'\} \, ⊆ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by lemma 4} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∀x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⇒ \, x' \, ∈ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \\
∩ \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∀x' \, \bullet \, x' \, ∈ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, ⇒ \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by defining property of subset} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ⊆ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \\
∩ \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, ⊆ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by properties of set intersection and mutual subsets property} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, = \, choice(\llbracket t\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by axiom 3} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket s\rrbracket ^\nu (\rho ) \, = \, \llbracket t\rrbracket ^\nu (\rho ) \, \} \end{array}$
$\begin{array}{l}
= \, \q{By semantics of equality} \end{array}$
$\begin{array}{l}
\llbracket s=t\rrbracket ^\tau (\mathcal{E} ) \, \, \, \, \, _\square \end{array}$
$\begin{array}{l}
\end{array}$
\subsubsection{Validation of the choice axiom}
$(∃x \, \bullet \, x \, ∈ \, s) \, ⇒ \, (∃x \, \bullet \, x \, ∈ \, s \, ∧ \, x \, = \, choice(s))$ where $x∖s$
By the semantics of implication we must show:
$\llbracket ∃ \, x \, . \, x \, ∈ \, s\rrbracket ^\tau (\mathcal{E} ) \, ⊆ \, \, \llbracket ∃ \, x \, . \, x \, ∈ \, s \, ∧ \, x \, = \, choice(s)\rrbracket ^\tau (\mathcal{E} )$
Recalling the semantics of existential choice, namely:
$\begin{array}{l} \llbracket ∃x \, \bullet \, x \, ∈ \, s \, ∧ \, P\rrbracket ^\tau (\mathcal{E} ) \, = \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∃ \, x'\bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \\
\, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, ∧ \, \llbracket P\rrbracket ^\tau \{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\} \, ≠ \, \{ \, \} \, \} \, \\
\end{array}$
This goal becomes:
$\begin{array}{l} \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∃ \, x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )))\} \, ⊆ \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∃ \, x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ∧ \, \\
\, \, \, \llbracket x'=choice(s)\rrbracket ^\tau \{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb\} \, ≠ \, \{ \, \} \, \} \\
\end{array}$
which is implied by the following holding for arbitrary $\rho $
$\begin{array}{l} (∃ \, x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho ))) \, ⇒ \\
(∃ \, x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ∧ \, \\
\, \, \, \llbracket x'=choice(s)\rrbracket ^\tau \{\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb \, ≠ \, \{ \, \} \, \} \\
\end{array}$
$\eq$ “by the semantics of equality”
$\begin{array}{l} (∃ \, x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho ))) \, ⇒ \\
(∃ \, x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ∧ \, \\
\, \, \llbracket x\rrbracket ^\nu (\rho \, ⊕ \, \lbb \, x \, \leadsto \, \{x'\} \, \rbb) \, = \, \llbracket choice(s)\rrbracket ^\nu (\rho ) \, ) \\
\end{array}$
$\eq$ “by the semantics of identifier $x$ and of choice”
$\begin{array}{l} (∃ \, x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho ))) \, ⇒ \\
(∃ \, x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ∧ \, \\
\, \, \{x'\} \, = \, \{ \, choice(choice(\llbracket s)\rrbracket ^\nu (\rho ) \, ) \, ) \, \} \\
\end{array}$
$\eq$ “property of singleton sets”
$\begin{array}{l} (∃ \, x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho ))) \, ⇒ \\
(∃ \, x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, ∧ \, \\
\, \, x' \, = \, choice(choice(\llbracket s)\rrbracket ^\nu (\rho ) \, ) \, \, \} \\
\end{array}$
Which is true by application of the axiom of choice to the set $choice(\llbracket s)\rrbracket ^\nu (\rho )$
\subsubsection{Validation of the infinite set axiom}
\(infinite(BIG)\)
We show:
\( \, \llbracket infinite(BIG\rrbracket ^\tau (\mathcal{E} )\rrbracket \, = \, \mathcal{E} \, \)
$\begin{array}{l} \llbracket infinite(BIG\rrbracket ^\tau (\mathcal{E} )\rrbracket \, = \, \q{by semantics of the infinite predicate} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, infinite(choice(\llbracket BIG\rrbracket ^\nu (\rho ) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by semantics of $BIG$} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, infinite(choice(\{\nat \})) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by choice from singleton set} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, infinite(\nat ) \, \} \, = \, \mathcal{E} \, \, \, \, \, \, _\square \\
\end{array}$
\subsection{Validation of the axioms specific to bunch theory}
The validation of the axioms specific to bunch theory establishes that they are true (with respect to the model).
\subsubsection{Bunch theory axiom, packaging 1}
$\begin{array}{l} \{\unpack A\} \, = \, A \, \, \, \text{where} \, \, A \, \, \text{is an element and a set.} \\
\end{array}$
To validate we show:
\( \, \llbracket \{\unpack A\}\rrbracket ^\nu (\rho ) \, = \, \llbracket A\rrbracket ^\nu (\rho ) \, \)
Taking LHS
$\begin{array}{l} \llbracket \{\unpack A\}\rrbracket ^\nu (\rho ) \, = \, \q{by semantics of packaging} \end{array}$
$\begin{array}{l}
\{\llbracket \unpack A\rrbracket ^\nu (\rho )\} \, = \, \q{by semantics of unpackaging} \end{array}$
$\begin{array}{l}
\{choice(\llbracket A\rrbracket ^\nu (\rho )\} \, = \, \q{by lemma 3} \end{array}$
$\begin{array}{l}
\llbracket A\rrbracket ^\nu (\rho ) \, \, \, \, \, \, _\square \\
\end{array}$
\subsubsection{Bunch theory axiom, packaging 2}
$\begin{array}{l} \unpack \{E\} \, = \, E \\
\end{array}$
To validate we show:
\( \, \llbracket \unpack \{E\}\rrbracket ^\nu (\rho ) \, = \, \llbracket E\rrbracket ^\nu (\rho ) \, \)
Taking LHS
$\begin{array}{l} \llbracket \unpack \{E\}\rrbracket ^\nu (\rho ) \, = \, \q{by semantics of unpackaging} \end{array}$
$\begin{array}{l}
choice(\llbracket \{E\}\rrbracket ^\nu (\rho )) \, = \, \q{by semantics of packaging} \end{array}$
$\begin{array}{l}
choice(\{\llbracket E\rrbracket ^\nu (\rho )\}) \, = \, \q{taking choice} \end{array}$
$\begin{array}{l}
\llbracket E\rrbracket ^\nu (\rho ) \, \, \, \, \, \, \, \, _\square \\
\end{array}$
\subsubsection{Bunch theory element axiom 1}
\( \, element(\unpack A) \, \, ⇔ \, \, card(A)=1 \, \, \, \) ($A$ an element and a set.)
To validate we show:
\( \, \llbracket element(\unpack A)\rrbracket ^\tau (\mathcal{E} ) \, \, = \, \, \llbracket card(A)=1\rrbracket ^\tau (\mathcal{E} ) \, \)
$\eq \, \, $ “by semantics of $element$ on LHS and $=$ on RHS”
\( \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, card(\llbracket \unpack A\rrbracket ^\nu (\rho ) \, = \, 1 \, \} \, = \, \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \llbracket card(A)\rrbracket ^\nu (\rho ) \, = \, \llbracket 1\rrbracket \, \} \, \)
$\impliedby \, \, $ “by lemma 9 and semantics of constant 1”
\( \, card(\llbracket \unpack A\rrbracket ^\nu (\rho ) \, = \, 1 \, \, \, \iff \, \, \, \llbracket card(A)\rrbracket ^\nu (\rho ) \, = \, \{1\} \, \)
$\eq \, \, $ “by semantics of $\unpack $ on LHS and $card$ on RHS”
\( \, card(choice\llbracket A\rrbracket ^\nu (\rho )) \, = \, 1 \, \, \iff \, \, \, \{ \, card(choice(\llbracket A\rrbracket ^\nu (\rho )) \, \} \, = \, \{1\} \, \)
$\eq \, \, $ “by referential transparency and lemma 7”
\( \, true \, \, \, \, \, _\square \, \)
\subsubsection{Bunch theory element axiom 2}
\( \, element(\{E\}) \, \)
To validate we show:
\( \, \llbracket element(\{E\})\rrbracket ^\tau (\mathcal{E} ) \, = \, \mathcal{E} \, \)
$\begin{array}{l} \llbracket element(\{E\})\rrbracket ^\tau (\mathcal{E} ) \, \eq \, \q{by semantics of $element$ } \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, card(\llbracket \{E\}\rrbracket )^\nu (\rho )) \, = \, 1 \, \} \, \, \eq \, \q{by semantics of packaging} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, card(\{\llbracket E\rrbracket ^\nu (\rho )\}) \, = \, 1 \, \} \, \, \eq \end{array}$
$\begin{array}{l}
\mathcal{E} \\
\end{array}$
\subsubsection{First guarded bunch axiom}
\( \, g \, \, ⇒ \, \, g\bguard \, E \, = \, E \, \)
To validate we show:
\( \, \llbracket g\rrbracket ^\tau (\mathcal{E} ) \, \, ⊆ \, \, \llbracket g\bguard \, E \, = \, E\rrbracket ^\tau (\mathcal{E} ) \, \)
$\eq$ by set expansion of LHS of $⊆$ and applying equality semantics to RHS.
\( \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{\rho \} \, \} \, ⊆ \, \\
\, \, \, \, \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \llbracket g\bguard \, E\rrbracket ^\nu (\rho ) \, = \, \, \llbracket E\rrbracket ^\nu (\rho ) \, \} \, \)
$\eq$ by lemma 8.
\( \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{\rho \} \, \, ⇒ \, \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \llbracket g\bguard \, E\rrbracket ^\nu (\rho ) \, = \, \, \llbracket E\rrbracket ^\nu (\rho ) \, \)
We must prove the RHS of the implication under assumptions
$\rho \, ∈ \, \mathcal{E} $ and $ \, \llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{\rho \}$
By semantics of the guarded bunch, the RHS becomes:
\( \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \\
\IF \, \llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{\rho \} \, \THEN \, \llbracket E\rrbracket ^\nu (\rho ) \, = \, \llbracket E\rrbracket ^\nu (\rho ) \, \ELSE \, \{ \, \} \, \END \, = \, \llbracket E\rrbracket ^\nu (\rho ) \, \)
now $\rho \, ∈ \, \mathcal{E} $ is already assumed and using assumption $ \, \llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{\rho \}$ to resolve the conditional statement it remains to prove:
\( \, \llbracket E\rrbracket ^\nu (\rho ) \, = \, \llbracket E\rrbracket ^\nu (\rho ) \, \)
Which is true by the equality law we inherit from predicate logic with equality.
\subsubsection{Second guarded bunch axiom}
\( \, ¬g \, \, ⇒ \, \, g\bguard \, E \, = \, \unpack \{ \, \} \, \)
To validate we show:
\( \, \llbracket ¬g\rrbracket ^\tau (\mathcal{E} ) \, \, ⊆ \, \, \llbracket ¬g\bguard \, E \, = \, \unpack \{ \, \}\rrbracket ^\tau (\mathcal{E} ) \, \, \)
$\eq$ by applying semantics of negation to LHS of $⊆$ and equality semantics to RHS.
\( \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{ \, \} \, \} \, ⊆ \, \\
\, \, \, \, \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \llbracket ¬g\bguard \, E\rrbracket ^\nu (\rho ) \, = \, \, \llbracket \unpack \{\}\rrbracket ^\nu (\rho ) \, \} \, \)
$\eq$ by lemma 8 and semantics of unpacking.
\( \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{ \, \} \, \, ⇒ \, \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \llbracket g\bguard \, E\rrbracket ^\nu (\rho ) \, = \, \, \{ \, \} \, \)
We must prove the RHS of the implication under assumptions
$\rho \, ∈ \, \mathcal{E} $ and $ \, \llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{ \, \}$
By semantics of the guarded bunch, the RHS becomes:
\( \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \\
\IF \, \llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{\rho \} \, \THEN \, \llbracket E\rrbracket ^\nu (\rho ) \, \, \ELSE \, \{ \, \} \, \END \, = \, \{ \, \} \, \)
now $\rho \, ∈ \, \mathcal{E} $ is already assumed and using assumption $ \, \llbracket g\rrbracket ^\tau \{\rho \} \, = \, \{ \, \}$ to resolve the conditional statement it remains to prove:
\( \, \{ \, \} \, = \, \{ \, \} \, \) which is true by equality.
\subsection{Validation of the axiomatic properties of the $infinite$ predicate}
The first of these properties is: \(infinite(s) \, ⇒ \, (∃x \, \bullet \, x \, ∈ \, s)\)
We show:
\( \, \llbracket infinite(s)\rrbracket ^\tau (\mathcal{E} ) \, ⊆ \, \llbracket ∃x \, \bullet \, x \, ∈ \, s\rrbracket ^\tau (\mathcal{E} ) \, \)
$\begin{array}{l} \llbracket infinite(s)\rrbracket ^\tau (\mathcal{E} ) \, = \, \q{by semantics of the infinite predicate} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, infinite(choice(\llbracket s\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
⊆ \, \q{since $infinite(a) ⇒ (∃x • x ∈ a)$} \, \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, (∃x' \, \bullet \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
= \, \q{by semantics of existential quantification} \end{array}$
$\begin{array}{l}
\llbracket ∃x \, \bullet \, x \, ∈ \, s\rrbracket ^\tau (\mathcal{E} ) \, \, \, \, \, \, _\square \\
\end{array}$
The other axiomatic property of the infinite predicate is:
\( \, infinite(s) \, ⇔ \, infinite(\{ \, x \, | \, x \, ∈ \, s \, ∧ \, x \, ≠ \, choice(s) \, \}) \, \)
During validation we will call on the following lemma:
$\begin{array}{llc} \text{L8.} \, & \, \llbracket ¬(x \, = \, choice(s))\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb x\leadsto \{x'\}\rbb\}) \, ≠ \, \{\} \, \, \\
\, \, \, \, \, \, & \, \, \, \, \, \, \, ≡ \, \, \\
\, \, \, \, \, \, & \, x' \, ≠ \, choice(choice(\llbracket s\rrbracket ^\nu (\rho )) \, \\
\end{array}$
Proof of lemma:
$\begin{array}{l} \llbracket ¬(x \, = \, choice(s))\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb x\leadsto \{x'\}\rbb\}) \, \, ≠ \, \, \{\} \, \, ≡ \, \q{by semantics of not} \end{array}$
$\begin{array}{l}
\{\rho \, ⊕ \, \lbb x\leadsto \{x'\}\rbb\} \, \setminus \llbracket x \, = \, choice(s)\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb x\leadsto \{x'\}\rbb\}) \, \, ≠ \, \, \{\} \, \, \end{array}$
$\begin{array}{l}
≡ \, \text{since} \, \{\rho \, ⊕ \, \lbb x\leadsto \{x'\}\rbb\} \, \text{is a singleton and} \, \llbracket P\rrbracket ^\tau (\mathcal{E} ) \, ⊆ \, \mathcal{E} \end{array}$
$\begin{array}{l}
\llbracket x \, = \, choice(s)\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb x\leadsto \{x'\}\rbb\}) \, = \, \{\} \end{array}$
$\begin{array}{l}
≡ \, \q{by semantics of equality} \end{array}$
$\begin{array}{l}
\{ \, \rho ' \, | \, \rho ' \, ∈ \, \{\rho \, ⊕ \, \lbb x\leadsto \{x'\}\rbb\} \, ∧ \, \llbracket x\rrbracket ^\nu (\rho ') \, = \, \llbracket choice(s)\rrbracket ^\nu (\rho ') \, \} \, \, = \, \, \{\} \end{array}$
$\begin{array}{l}
≡ \, \q{by property of set comprehension} \end{array}$
$\begin{array}{l}
\llbracket x\rrbracket ^\nu (\rho \, ⊕ \, \lbb x\leadsto \{x'\}\rbb\} \, ≠ \, \llbracket choice(s)\rrbracket ^\nu (\{\rho \, ⊕ \, \lbb x\leadsto \{x'\}\rbb\}) \end{array}$
$\begin{array}{l}
≡ \, \, \q{taking denotation for $x$ and by semantics of choice} \end{array}$
$\begin{array}{l}
\{x'\} \, ≠ \, \{choice(choice(\llbracket s\rrbracket ^\nu (\rho ')))\} \end{array}$
$\begin{array}{l}
≡ \, \q{by logic and lemma 7} \end{array}$
$\begin{array}{l}
x' \, ≠ \, choice(choice(\llbracket s\rrbracket ^\nu (\rho )) \, \, \, \, \, \, _\square \\
\end{array}$
To validate the given property of the $infinite$ predicate we show:
\( \, \llbracket infinite(s)\rrbracket ^\tau (\mathcal{E} ) \, = \, \llbracket infinite(\{ \, x \, | \, x \, ∈ \, s \, ∧ \, x \, ≠ \, choice(s) \, \})\rrbracket ^\tau (\mathcal{E} ) \, \)
Taking RHS we have
$\begin{array}{l} \llbracket infinite(\{ \, x \, | \, x \, ∈ \, s \, ∧ \, ¬(x=choice(s))\})\rrbracket ^\tau (\mathcal{E} ) \end{array}$
$\begin{array}{l}
= \, \q{by semantics of $infinite$ predicate} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, infinite(choice(\llbracket \{ \, x \, | \, x \, ∈ \, s \, ∧ \, ¬(x=choice(s))\}\rrbracket ^\nu (\rho )) \, \} \end{array}$
$\begin{array}{l}
≡ \, \q{by semantics of set comprehension} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, infinite(choice(\{ \\
\, \, \, \{ \, x' \, | \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho ) \, ∧ \, \llbracket ¬(x=choice(s)\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb x \, \leadsto \, \{x'\}\rbb\}) \, ≠ \, \{\} \, \} \\
\}))\} \end{array}$
$\begin{array}{l}
≡ \, \q{applying choice} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, infinite( \\
\, \, \, \{ \, x' \, | \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho ) \, ∧ \, \llbracket ¬(x=choice(s)\rrbracket ^\tau (\{\rho \, ⊕ \, \lbb x \, \leadsto \, \{x'\}\rbb\}) \, ≠ \, \{\} \, \} \\
)\} \end{array}$
$\begin{array}{l}
≡ \, \q{by lemma} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, infinite( \\
\, \, \, \{ \, x' \, | \, x' \, ∈ \, choice(\llbracket s\rrbracket ^\nu (\rho ) \, ∧ \, x' \, ≠ \, choice(choice(\llbracket s\rrbracket ^\nu (\rho )) \, \} \\
)\} \end{array}$
$\begin{array}{l}
≡ \, \q{by axiom Infinity 2.} \end{array}$
$\begin{array}{l}
\{ \, \rho \, | \, \rho \, \, \mathcal{E} \, ∧ \, infinite(choice(\llbracket s\rrbracket ^\nu (\rho ) \, \} \end{array}$
$\begin{array}{l}
≡ \, \q{by semantics of infinity} \end{array}$
$\begin{array}{l}
\llbracket infinite(s)\rrbracket ^\tau (\mathcal{E} ) \, \, \, \, \, \, \, \, _\square \\
\end{array}$
\section{Conservative extensions to bunch notation}
So far the only notation that distinguishes our axiomatic bunch theory from the axiomatic set theory on which is is based, is the unpacking operator $\unpack $.
However, we can now extend our notations through a series of definitions. We assume standard definitions from set theory, e.g. for set union, intersection, and difference. We will also use set comprehension expressions of the form \(\{ \, x \, | \, P \, \bullet \, E \, \}\), representing the set of values expression $E$ can take as $x$ ranges over the values allowed by predicate $P$.
We define the $null$ bunch, bunch union and intersection, and bunch inclusion:
\( \, null \, \, \defs \, \, \unpack \{ \, \} \, \)
\( \, E,F \, \defs \, \unpack (\{E\} \, ∪ \, \{F\}) \, \)
\( \, E'F \, \defs \, \unpack (\{E\} \, ∩ \, \{F\}) \, \)
\( \, E:F \, \defs \, \{E\}⊆\{F\} \, \)
Now conditional expressions:
\( \, \IF \, \, g \, \, \THEN \, \, E \, \, \ELSE \, \, F \, \, \END \, \, \defs \, \, \, g\bguard \, E \, , \, ¬g\bguard \, F \, \)
And a form of bunch comprehension:
\( \, ∮ \, x \, | \, x∈S \, ∧ \, P \, \, \bullet \, E \, \, \defs \, \, \, \unpack \{ \, x \, | \, x∈S \, ∧ \, P \, \bullet \, E\} \, \)
Since $y \, ∈ \, \{ \, x \, | \, x∈S \, ∧ \, P \, \, \bullet \, E \, \} \, \, ⇔ \, \, \, ∃ \, x \, \bullet \, x∈S∧P \, ∧ \, y:E$ we can
write $\{ \, x \, | \, x∈S \, ∧ \, P \, \, \bullet \, E \, \}$ as $\{ \, x \, | \, true \, \bullet \, x∈S \, ∧ \, P \, \bguard \, \, E \, \}$ which we abbreviate to $\{ \, x \, \bullet \, x∈S \, ∧ \, P \, \bguard \, \, E \, \}$. Also, since $ \, x∈S \, ∧ \, P \, \bguard \, \, E$ is an expression, we can take $\{ \, x \, \bullet \, E \, \}$ as a general form for set comprehension, with the proviso that $E$ must imply the type of $x$. Corresponding to this we can use $∮x \, \bullet \, E$ as a general form for bunch comprehension.
We now come to some redefinition's, required to lift existing definitions, which apply only to elements, to apply element-wise to bunches.
We incur a proof obligation to show the new definitions will be equivalent to the old when applied to arguments for which the old definitions were defined, i.e. to elements. To avoid need for renaming this obligation can be discharged prior to the redefinition. Thus, noting that when $E$ and $S$ are elements:
\( \, \{E\} \, ⊆ \, ⋂ \, \{ \, S \, \} \, \, ⇔ \, \, E \, ∈ \, S \, \)
we are now free to introduce the following redefinition of $E \, ∈ \, S$, in which $E$ and $S$ are not restricted to being elements, because we know it is compatible with the existing definition in the case where $E$ and $S$ are elements.
\( \, E \, ∈ \, S \, \defs \, \, \{E\} \, ⊆ \, ⋂ \, \{ \, S \, \} \, \)
The effect of this definition is that for $E \, ∈ \, S$ to hold every $e:E$ must be a member of every $s:S$. This is in line with our use of bunches to represent non-deterministic terms, and guarantees that membership will hold after the non-determinism is resolved.
Here is a redefinition which lifts unpacking operators. The new definition of $\unpack $ is expressed in terms of the original $\unpack $, which appears in the body of the definition. original :
\( \, \unpack E \, \defs \, \unpack (∪\{E\}) \, \).
A more general way of lifting an operation, and one where the accompanying proof obligation can be safely assumed to be discharged, is to represent it in terms of a bunch comprehension. Here is the definition of the lifted power set operator:
\( \, \pow (S) \, \, \defs \, \, ∮s \, \bullet \, s:S \, \bguard \, \pow (s) \, \)
\section{Some results in bunch theory}
The following are immediately provable by appealing to the definitions of $null$, bunch intersection, and bunch union and to related properties which hold in set theory:
$\begin{array}{llc} E'F \, = \, F'E \, \, \, \, & \, \, \, E,F \, = \, F,E \, \, \, \, \, & \, \, \, \, \, \text{commutativity} \\
(E'F)'G \, = \, E'(F'G) \, \, \, \, & \, \, \, E,(F,G) \, = \, (E,F),G \, \, & \, \text{associativity} \\
E'(F,G) \, = \, (E'F),(E'G) \, \, \, & \, \, E,(F'G) \, = \, \, (E,F)'(E,G) \, \, & \, \text{distributivity} \\
E,(F,G) \, = \, (E,F),(E,G) \, \, \, & \, \, E'(F'G) \, = \, (E'F)'(E'G) \, \, \, & \, \text{distributivity} \, \\
E \, : \, E,F \, & \, \, E'F \, : \, E \, \, & \, \, \text{inclusion} \\
E,null \, = \, E \, \, & \, \, E'null \, = \, null \, \, & \, \, \text{zero and unit} \\
\end{array}$
The set equality axiom $∀ \, x \, \bullet \, x∈A⇔x∈B \, ⇒ \, A=B$ now requires the proviso that $A$ and $B$ are elements, but we have the following laws for equality of general bunch expressions $E$ and $F$
$\begin{array}{l} (∀ \, x \, \bullet \, x \, : \, E \, ⇔ \, x \, : \, F) \, \, ⇒ \, \, E=F \\
\{E\} \, = \, \{F\} \, \, ⇔ \, \, E=F \\
\end{array}$
The guarded bunch has distributive properties which can be obviously proved by case analysis:
$\begin{array}{l} g\bguard \, E,F \, \, \, = \, \, \, (g\bguard \, E),(g\bguard \, F) \\
g\bguard \, E'F \, \, \, = \, \, \, (g\bguard \, E)'(g\bguard \, F) \\
\end{array}$
We have the following “part of” and “member of” laws:
$\begin{array}{l} x \, : \, E,F \, \, \, ⇔ \, \, \, x:E \, ∨ \, x:F \, \, \, \text{($x$ an element)} \\
x \, ∈ \, E,F \, \, \, ⇔ \, \, \, x∈E \, ∧ \, \, x∈F \\
\end{array}$
Which generalise to the following bunch comprehension laws:
$\begin{array}{l} x \, : \, ∮ \, y \, \bullet \, y \, : \, Y \, \bguard \, E \, \, \, ⇔ \, \, (∃ \, y \, \bullet \, y:Y \, ∧ \, x:E) \, \, \, \, \, (x \, \, \text{an element}) \\
x \, ∈ \, ∮ \, y \, \bullet \, y \, : \, Y \, \bguard \, E \, \, \, ⇔ \, \, (∀ \, y \, \bullet \, y:Y \, ⇒ \, x∈E) \, \, \, \, \, \\
\end{array}$
Some of the set theory axioms can be generalised. The ordered pair axiom $E\mapsto F \, ∈ \, (s \, × \, t) \, ⇔ \, E \, ∈ \, s \, ∧ \, F \, ∈ \, t$ holds for non-elemental values, and this has already been validated in our model.
The power set axiom $s \, ∈ \, \pow (t) \, \, ⇔ \, \, (∀ \, x \, \bullet \, x \, ∈ \, s \, ⇒ \, x \, ∈ \, t)$ where $x$ is not free in $s$ or $t$, still holds when $t$ is a non-elemental value.
\section{Axioms and semantics of “Improper bunch theory”}
For modelling program semantics within a total correctness framework we associate with each type $T$ an `improper' bunch $⊥ \, _T$. We consider it to be of type $T$. We require the following additional axioms.
$\begin{array}{l} \\
E \, : \, ⊥ \, \, \, \text{“maximality”} \end{array}$
$\begin{array}{l}
⊥ \, : \, A,B \, \, ⇒ \, \, A=⊥ \, \, ∨ \, \, B=⊥ \, \, \, \text{“atomicity”} \end{array}$
$\begin{array}{l}
\{⊥ \, _T\} \, \, = \, \, ⊥ \, _{\pow (T)} \, \, \, \text{“improper packaging”} \end{array}$
$\begin{array}{l}
\unpack ⊥ \, _{\pow (T)} \, \, = \, ⊥ \, _T \, \, \, \, \, \text{“improper unpackaging”} \end{array}$
$\begin{array}{l}
\end{array}$
And we need to modify the axiom of proper bunch theory that says $\{E\}$ is an element, which we can now assert only when $E \, ≠ \, ⊥ \, $
$\begin{array}{l} E \, ≠ \, ⊥ \, \, ⇒ \, \, element( \, \{E\} \, ) \, \, \text{“guarded element”} \\
\end{array}$
The maximality axiom tells us that for any type, any bunch other than the improper bunch is a proper sub-bunch of the improper bunch.
The atomicity axiom tells us that $⊥$ cannot be constructed from the union of two bunches both different from itself.
The packaging axioms tell us that impropriety cannot be removed by packaging or unpackaging, although the results of packing and unpacking an improper bunch will be of the expected type.
Note that we no longer have an unguarded axiom to say $\{E\}$ is an element, but the {\em atomicity} of $\{E\}$ follows from the atomicity axiom together with the guarded element axiom.
\subsection{Extending our model to include the improper bunch}
Within our semantic universe we distinguish sets constructed directly from $BIG$, which we term “basic” or “given” sets, from those defined by using the power-set and set product constructors.
We recall once more that any such given set is maximal and corresponds to a type, as do all sets constructed from maximal sets.
The semantic support for a basic set, $T$, say, in our target language of improper bunch theory, is given by a set $T'$ in our semantic universe which contains the elements of the set $T$ in the target universe, along with an additional distinguished element $κ_T$.
We define the semantic representation of $⊥_T$ by $\llbracket ⊥_T\rrbracket \, = \, T'$
Thus if the given set $T$ in our target universe is defined so that $T=\{a,b\}$ then to support this within our semantic universe we have a set $T'=\{a,b,κ_T\}$, and we have $\llbracket ⊥_T\rrbracket \, = \, \{a,b,κ_T\}$.
The denotations of all possible bunches of type $T$ are as follows:
\[⟦null_T\rrbracket =\{\}, \, \llbracket a\rrbracket =\{a\}, \, \llbracket b\rrbracket =\{b\}, \, \llbracket a,b\rrbracket =\{a,b\}, \, \llbracket ⊥_T\rrbracket =\{a,b,κ_T\} \, \]
We note that $⊥_T$ is the only term of type $T$ whose denotation
contains the distinguished element $κ_T$. This allows us to model the atomicity of the improper bunch. We also note that the denotation of the improper bunch for a given type is a maximal set. This allows us to model the maximality of the improper bunch.
We use similar techniques for any constructed type.
Within each maximal constructed set of the semantic universe, we have a $κ$ element defined structurally as: $κ_{T×U} \, = \, κ_T \, \mapsto \, κ_U$ and $κ_{\pow (T)} \, = \, \llbracket ⊥_T\rrbracket $.
Denotations for the improper bunch of each type are:
$\begin{array}{l} \llbracket ⊥_T\rrbracket \, = \, T' \, \text{($T$ a given set)} \\
\llbracket ⊥_{T×U}\rrbracket \, = \, \llbracket ⊥_T\rrbracket \, × \, \llbracket ⊥_U\rrbracket \\
\llbracket ⊥_{\pow (T)}\rrbracket \, = \, \pow (\llbracket ⊥_T\rrbracket \\
\end{array}$
Thus, the denotation for the improper bunch of any type will be a maximal set.
We recall that he purpose of the improper bunch is to represent the effect of running a program outside its pre-condition. In line with the philosophy of total correctness, we take a pessimistic view of such effects, which may go well beyond non-termination, and include, for example, stack and array overflows which corrupt pointers or code, leading to totally unpredictable results - the machine may catch fire! To reflect this we want the improper bunch to be absorptive with respect to all expression connectives. We extend a number of definitions to take account of special cases arising from this property. We can do this using bunch guard. In each of the following definitions, the definition body is a bunch of terms, the first of which is a guarded bunch. If the bunch guard is true that term, and hence the whole body of the definition, represents an improper bunch. Otherwise the guarded term represents null and disappears.\footnote{It is possible to directly write denotations for these forms, rather than using redefinition. For example $\llbracket \{E\}\rrbracket ^\nu (\rho ) \, = \, \IF \, \llbracket E\rrbracket ^\nu (\rho ) \, = \, ⊥_T \, \, \THEN \, ⊥ \, _{\pow (T)} \, \ELSE \, \{ \, \llbracket E\rrbracket ^\nu (\rho ) \, \} \, \END$.}
$\begin{array}{l} \{E\} \, \, \, \defs \, \, \, \, E=⊥ \, _T \, \bguard \, ⊥ \, _{\pow (T)} \, \, \, , \, \, \, \{E\} \end{array}$
$\begin{array}{l}
\unpack E \, \, \, \defs \, \, \, E=⊥ \, _{\pow (T)} \, \bguard \, ⊥ \, _T \, \, \, \, , \, \, \, \unpack E \end{array}$
$\begin{array}{l}
A∪B \, \, \, \defs \, \, \, A=⊥ \, ∨ \, B=⊥ \, \, \bguard \, \, ⊥ \, \, \, , \, \, \, A \, ∪ \, B \end{array}$
$\begin{array}{l}
A∩B \, \, \, \defs \, \, \, \, A=⊥ \, ∨ \, B=⊥ \, \, \bguard \, \, ⊥ \, \, \, , \, \, \, A \, ∩ \, B \end{array}$
$\begin{array}{l}
D \, \mapsto \, E \, \, \defs \, \, D=⊥ \, ∨ \, E=⊥ \, \, \bguard \, \, ⊥ \, \, \, , \, \, D \, \mapsto \, E \end{array}$
$\begin{array}{l}
S \, × \, T \, \, \defs \, \, \, S=⊥ \, ∨ \, T=⊥ \, \, \bguard \, \, ⊥ \, \, , \, \, S \, × \, T \\
\end{array}$
For bunch union and bunch intersection we can deduce absorptive properties from the above, e.g.
$\begin{array}{l} A \, , \, ⊥_T \, \, \eq \, \, \text{“by definition of bunch intersection”} \\
\unpack (\{A\} \, ∪ \, \{⊥_T\}) \, \, \eq \, \, \text{“by improper packaging axiom”} \\
\unpack (\{A\} \, ∪ \, ⊥_{\pow (T)} \, ) \, \, \eq \, \, \text{“by guarded redefinition of set union”} \\
\unpack ⊥_{\pow (T)} \, \, \eq \, \text{“by improper unpackaging axiom”} \\
⊥_T \, \\
\end{array}$
One construct that is not subject to these absorptive properties is the bunch guard, since by the second guarded bunch axiom tells us that $false \, \bguard \, E \, = \, null$. This is to capture the effect, in the world of values, of code that cannot run, e.g. the contribution from the branch of a conditional statement that is not executed.
\subsection{Validation of the axioms of improper bunch theory}
Let ${\cal \, D}(T)$ be the set of denotations for bunches of type $T$. We formalise the properties, already discussed above, that support maximality and atomicity of the improper bunch.
Property 1. $x \, ∈ \, {\cal \, D}(T) \, ⇒ \, x \, ⊆ \, \llbracket ⊥_T\rrbracket $
Property 2. $x \, ∈ \, {\cal \, D}(T) \, ⇒ \, ( \, κ_T \, ∈ \, x \, \, ⇔ \, \, x \, = \, \llbracket ⊥_T\rrbracket $ )
\subsubsection{Validation of the maximality of the improper bunch}
We must validate $E \, : \, ⊥$. For this we must show:
$\begin{array}{l} \llbracket E \, : \, ⊥\rrbracket ^\tau (\mathcal{E} ) \, = \, \mathcal{E} \, \, \, \, \, \eq \, \, \text{“by semantics of bunch inclusion”} \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \llbracket E\rrbracket ^\nu (\rho ) \, ⊆ \llbracket ⊥\rrbracket \, \} \, \, = \, \mathcal{E} \, \, \eq \, \, \text{“for arbitrary } \, \rho \, \text{”} \\
\llbracket E\rrbracket ^\nu (\rho ) \, ⊆ \llbracket ⊥\rrbracket \, \, \eq \, \, \text{“by property 1 above”} \\
true \, \square \, \\
\end{array}$
\subsubsection{Validation of the atomicity of the improper bunch}
We must validate $⊥ \, : \, A,B \, \, ⇒ \, \, A=⊥ \, \, ∨ \, \, B=⊥$.
$\begin{array}{l} \llbracket ⊥ \, : \, A,B \, \, ⇒ \, \, A=⊥ \, \, ∨ \, \, B=⊥ \, \rrbracket ^\tau (\mathcal{E} ) \, \\
\eq \, \text{“by the semantics of implication”} \\
\llbracket ⊥ \, : \, A,B\rrbracket ^\tau (\mathcal{E} ) \, ⊆ \, \llbracket A=⊥ \, \, ∨ \, \, B=⊥ \, \rrbracket ^\tau (\mathcal{E} ) \\
\eq \, \text{“by the semantics of logical or”} \\
\llbracket ⊥ \, : \, A,B\rrbracket ^\tau (\mathcal{E} ) \, \, ⊆ \, \, \llbracket A=⊥ \, \rrbracket ^\tau (\mathcal{E} ) \, \, ∪ \, \, \llbracket B=⊥ \, \rrbracket ^\tau (\mathcal{E} ) \\
\eq \, \text{“by the semantics of bunch inclusion”} \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \llbracket ⊥ \, \rrbracket \, ⊆ \, \llbracket A,B\rrbracket ^\nu (\rho ) \, \} \, \, ⊆ \, \, \llbracket A=⊥ \, \rrbracket ^\tau (\mathcal{E} ) \, \, ∪ \, \, \llbracket B=⊥ \, \rrbracket ^\tau (\mathcal{E} ) \\
\eq \, \text{“by semantics of equality”} \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, \llbracket ⊥ \, \rrbracket \, ⊆ \, \llbracket A,B\rrbracket ^\nu (\rho ) \, \} \, \, ⊆ \, \, \\
\, \, \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket A\rrbracket \, = \, \llbracket ⊥ \, \rrbracket \, \} \, \, ∪ \, \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, ∧ \, \llbracket B\rrbracket ^\nu (\rho ) \, = \, \llbracket ⊥ \, \rrbracket \, \} \\
\eq \, \text{“property of set union”} \\
\{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, ( \, \llbracket ⊥ \, \rrbracket \, ⊆ \, \llbracket A,B\rrbracket ^\nu (\rho ) \, \} \, ⊆ \, \, \\
\, \, \, \{ \, \rho \, | \, \rho \, ∈ \, \mathcal{E} \, \, ∧ \, \, ( \, \llbracket A\rrbracket ^\nu (\rho ) \, = \, \llbracket ⊥ \, \rrbracket \, \, ∨ \, \, \llbracket B\rrbracket ^\nu (\rho ) \, = \, \llbracket ⊥ \, \rrbracket \, ) \, \} \\
\eq \, \text{“for arbitrary }\rho \text{ ”} \\
\llbracket ⊥\rrbracket \, ⊆ \, \llbracket A,B\rrbracket ^\nu (\rho ) \, \, ⇒ \, \, \llbracket A\rrbracket ^\nu (\rho ) \, = \, \llbracket ⊥ \, \rrbracket \, \, ∨ \, \, \llbracket B\rrbracket ^\nu (\rho ) \, = \, \llbracket ⊥ \, \rrbracket \\
\eq \, \text{“by semantics of bunch union”} \\
\llbracket ⊥\rrbracket \, ⊆ \, \llbracket A\rrbracket ^\nu (\rho ) \, ∪ \, \llbracket B\rrbracket ^\nu (\rho ) \, ⇒ \, \, \llbracket A\rrbracket ^\nu (\rho ) \, = \, \llbracket ⊥ \, \rrbracket ^\nu (\rho ) \, \, ∨ \, \, \llbracket B\rrbracket ^\nu (\rho ) \, = \, \llbracket ⊥ \, \rrbracket ^\nu (\rho ) \\
\text{“Now taking the LHS of the implication, by property 2 above we have that } \\
κ \, ∈ \, \llbracket ⊥\rrbracket \, \text{ and thus by set theory property} \, S \, ⊆ \, T \, ∪ \, U \, ∧ \, x∈S \, ⇒ \, x∈T \, ∨ \, x∈U \\
\text{we have ” } \\
κ∈\llbracket A\rrbracket ^\nu (\rho ) \, ∨ \, κ∈\llbracket B\rrbracket ^\nu (\rho ) \, \, \, \eq \, \text{“again by property 2”} \\
\llbracket A\rrbracket ^\nu (\rho ) \, = \, \llbracket ⊥ \, \rrbracket ^\nu (\rho ) \, \, ∨ \, \, \llbracket B\rrbracket ^\nu (\rho ) \, = \, \llbracket ⊥ \, \rrbracket ^\nu (\rho ) \, \, \square \\
\, \end{array}$
\subsubsection{Validation of the axioms for improper packaging, improper unpacking, and guarded element}
For improper packaging we must show \( \, \llbracket \{⊥ \, _T\}\rrbracket ^\nu (\rho ) \, = \, \llbracket ⊥ \, _{\pow (T)}\rrbracket ^\nu (\rho ) \, \)
and this follows immediately from the revised semantics of packaging.
Similarly for improper unpacking, we must show
\( \, \llbracket \unpack ⊥ \, _{\pow (T)}\rrbracket ^\nu (\rho ) \, = \, \, \llbracket ⊥ \, _T\rrbracket ^\nu (\rho ) \, \)
which follows immediately from the revised semantics of unpacking.
For the guarded element axiom we must show
\( \, \llbracket \{E\}\rrbracket ^\nu (\rho ) \, = \, \IF \, \llbracket E\rrbracket ^\nu (\rho ) \, = \, \llbracket ⊥_T\rrbracket \, \THEN \, \llbracket ⊥_{\pow (T)}\rrbracket \, \ELSE \, \{\llbracket E\rrbracket ^\nu (\rho )\} \, \END \, \)
which follows immediately from the revised semantics of packaging.
\section{Functions}
\label{functions}
In B, since functions and relations are both modelled as sets of
ordered pairs, there is no difference in type between a function
\(f \, ∈ \, X \, \pfun \, Y\) and a relation \(r \, ∈ \, X \, ↔ \, Y\). They are both of type
$\pow (X \, × \, Y)$, which we usually write as $X \, ↔ \, Y$.
\subsection{Function application and anonymous functions}
In our formalisation of bunch theory we define function application as follows:
\( \, F(A) \, \defs \, if \, F=⊥ \, ∨ \, A=⊥ \, then \, \, ⊥ \, \, else \, \, ∮ \, f,a,b \, \bullet \, f:F \, ∧ \, a \, \mapsto \, b \, ∈ \, f \, ∧ \, a:A \, → \, b \, \) end
Our formulation, making use of bunches, does not require a distinction
to be made between the {\em application} of functions and of relations
which are non-functional; we simply think of the latter as
“non-deterministic” functions. From now on we refer to all relations as
“functions”.
Function application is distributive, with rules:
$\begin{array}{l} (f,g)(x) \, = \, f(x),g(x) \\
f((x,y)) \, = \, f(x),f(y) \\
\end{array}$
In the second of these rules, $f$ is applied to the bunch\footnote{The
enclosure of the bunch elements within brackets is required because the
form $f(x,y)$ is used for a function of two arguments, or more exactly
a function applied to the pair $x \, \mapsto y$.} $x,y$. We call the
distributive property described in this rule as “lifted function
application”.
Lambda expressions can be used to describe functions, and formally,
within Abrial's formulation of set theory, they represent a form of
set comprehension.
\( \, λx \, \bullet \, E \, \, \defs \, \, \{ \, x \, \bullet \, x \, \mapsto \, E \, \} \, \)
and evaluation of function application using
functions described by lambda expressions can be done purely by
syntactic substitution:
\( \, (λx \, \bullet \, E)(a) \, = \, E[a/x] \, \, \text{where } \, a \, ∈ \, \dom(λx \, \bullet \, E) \, \)
This rule will still apply where functions are applied to elements.
However, now that we have bunches and distributive application, we can
devise lambda expressions for which evaluation by syntactic
substitution does not comply with the distributive property of lifted
function application. For example
$\begin{array}{l} (λ \, x \, \bullet \, \{x+4\})((1,2)) \, = \, `` \text{by distributive property of lifted application}\rightq \\
(λ \, x \, \bullet \, \{x+4\})(1) \, , \, (λ \, x \, \bullet \, \{x+4\})(2) \, = \, `` \text{function application}\rightq \\
\{5\},\{6\} \\
\end{array}$
whereas directly substituting $1,2$ for $x$ in $\{x+4\}$ would give us $\{5,6\}$. This prompts us to consider whether evaluation of function application by syntactic substitution can be given a semantic meaning in the presence of bunch arguments.
\subsection{Wholistic function application}
The proof tool “Netty” \cite{NH11}, developed for use with Hehner's bunch theory, has two different types of function, described as distributive and applicative. The evaluation of applicative functions may be performed by syntactic substitution even when applied to non-elementary bunch arguments.
We achieve a similar result by defining a new form of “wholistic” function application, rather that a new type of function. Wholistic function application is denoted by a dot and defined in terms of standard application by:
\(f.X \, \defs \, \unpack f\{X\}\)
To define an anonymous function in terms of its wholistic application we write it, in a variant of lambda notation for which we use a capital lambda, as $Λ \, X \, \bullet \, E$. We will require that the application of such a function to a bunch can be evaluated by substituting the bunch argument into $E$:
\( \, (Λ \, X \, \bullet \, E).D \, = \, E[D/X] \, \)
For example:
\( \, (Λ \, X \, \bullet \, \{x+4\}).((1,2)) \, = \, \{x+4\}[(1,2)/x] \, = \, \{(1,2)+4\} \, = \, \{5,6\} \, \)
At this point the observant reader might note that whilst we have said that bound variables in out theory range over elements, our $X$ ranges over bunches of values. In fact $X$ is not a true bound variable, but rather a syntactic place holder, a form of syntactic sugar which is formally introduced in the following definition:
\( \, ΛX\bullet E \, \defs \, λz\bullet \{E[\unpack z/X]\} \, \)
We can now state the substitution rule for wholistic application of anonymous functions as the following theorem:
\begin{theorem}
\( \, (Λ \, X \, \bullet \, E).D \, \, = \, E[D/X] \, \, \)
\end{theorem}
\Proof
$\begin{array}{l} (Λ \, X \, \bullet \, E).D \, \, = \, \, \, \text{“by definition of } \, Λ \, X \, \bullet \, E\text{”} \\
(λ \, z \, \bullet \, \{E[\unpack z/X]\}).D \, \, = \, \, `` \text{by definition of wholistic application}\rightq \\
\unpack (λ \, z \, \bullet \, \{E[\unpack z/X]\})(\{D\}) \, \, = \, `` \text{Beta substitution in lambda expression}\rightq \\
\unpack \{E[\unpack \{D\}/X]\} \, \, = \, \, `` \text{axiom } \, \unpack \{E\} \, = \, E\rightq \end{array}$
$\begin{array}{l}
E[\unpack \{D\}/X] \, \, = \, \, `` \text{applying the same axiom to } \, \unpack \{D\}\rightq \\
E[D/X] \, \, \, \, _\square \\
\end{array}$
Functions in B are relations. We write $f(f(x))$ as $f^2{}(x)$ where $f^2{}$ is the relational composition of $f$ with itself: $f^2{} \, = \, f\asemi f$. We can also write $f.(f.X) \, = \, f^2{}.X$ as can be seen from
$\begin{array}{l} f.(f.X) \, \eq \, \, \text{“defn of wholistic application”} \\
f.(\unpack f\{X\}) \, \, \eq \, \, \text{“defn of wholistic application”} \\
\unpack f\{\unpack f\{X\}\} \, \, \eq \, \, \text{“axiom, packaging 1”} \\
\unpack f(f\{X\}) \, \eq \, \, \text{“since} \, f(f\{X\}) \, = \, f^2{}\{X\}\text{”} \\
\unpack f^2{}\{X\} \, \eq \, \text{“defn of wholistic application”} \\
f^2{}.X \\
\end{array}$
A simple proof by induction shows that this generalises to $f^n{}.X \, = \, \unpack f^n{}\{X\}.$
\subsection{A fixed point theory for wholistic application of functions.}
Classical fixed point theory treats equations of the form $f(X) \, = \, X$ and is usually expressed in terms of sets with a partial
ordering relation, e.g. $(X,≤)$. Here, we are interested in equations of the form $f.X \, = \, X$ and our associated ordering relation is bunch inclusion. However, we cannot talk about bunch inclusion in the same terms as a traditional partial order, as we cannot collect our bunches into a set without them losing their individual identities.
Our theory will treat homogeneous functions which are “constructive”. A function $f$ is defined as constructive if it is non-strict wrt $null$, i.e. $f.null \, ≠ \, null$, and it its wholistic application to a non-null bunch is distributive, i.e. $f.(C,D) \, = \, f.C \, , \, f.D$
Such a function is also monotonic in the sense that $D \, : \, E \, ⇒ \, f.D \, : \, f.E$. This follows directly from distributivity, since if $D:E$ we must have some bunch $C$ with $C,D=E$ and thus can argue:
\( \, f.D \, : \, f.C \, , \, f.D \, \, \eq \, \, f.D \, : \, f.(C,D) \, \, \eq \, f.D \, : \, f.E \, \)
Now since $f.null \, \, ≠ \, \, null$, we must have $null \, : \, f.null$. By monotonicity we thus have $f.null \, : \, f^2{}.null$ etc. Consider the bunch sequence whose $ith$ member is $f^i{}.null$. This is a monotonic increasing sequence and since the terms are bounded above (by the maximal bunch of the given type) it has a limit. The ordering by bunch inclusion allows us to write the ith member of the sequence as $∮n\bullet \, n \, ∈ \, 1..i \, \bguard \, f^n{}$ and the limit of the sequence is $∮n\bullet \, n \, ∈ \, \nat _1{} \, \bguard \, f^n{}$. We see this is a solution to the fixed point equation $f.X \, = \, X$ since:
$\begin{array}{l} f.∮n\bullet \, n \, ∈ \, \nat _1{} \, \bguard \, f^n{} \, . \, null \, = \, \text{“by distributivity”} \\
∮n\bullet \, n \, ∈ \, \nat _1{} \, \bguard \, \, f^n{}^+{}^1{} \, . \, null \, = \, \text{“writing $ℕ \setminus 0..1$ as $ℕ₂$”} \\
∮n\bullet \, n \, ∈ \, \nat _2{} \, \bguard \, f^n{} \, = \, \, \, \text{“since $f.null : f².null$”} \\
∮n\bullet \, n \, ∈ \, \nat _1{} \, \bguard \, f^n{} \\
\end{array}$
It is also the least fixed point, for if it were not there would
necessarily be another fixed point $Y$ say such that $¬∮n\bullet f^n{}.null \, : \, Y$,
and thus we must have some element $e$ say with $e \, : \, ∮n\bullet f^n{}.null$ and $¬ \, e:Y$. Since $e \, : \, ∮n\bullet f^n{}.null$ we must have some $i$ such that $e \, : \, f^i{}.null$. Now noting that $f$ and $f^i{}$ have the same fixed points (obvious proof by induction), we have $f^i{}.Y \, = \, Y$, and since $Y \, = \, Y,null$, this is equivalent to $f^i{}.(Y,null) \, = \, Y$. By distributivity this gives us $f^i{}.Y \, , \, f^i{}.null \, = \, Y$. But $e \, : \, f^i{}.null$ and hence $e:Y$, contradicting the requirement for $Y$ to be a fixed point of $f$ and to be less than $X$.
\subsection{Wholistic application, fix points, and formal grammars}
We will illustrate an application of the above theory with a simple
example, before illustrating how the theory extends to systems of multiple, mutually recursive, equations.
For our first example we consider a simple grammar for program identifiers. The the only data type we will be concerned with are character strings\footnote{Hehner has an interesting $string$ data type which is an unpacked list. We are not concerned with that here: our strings are sequences of characters.} and the main operations are bunch union and string catenation. We take advantage of this restricted scenario by eliding the catenation symbol, e.g. writing $ID \, β$ rather that $ID\cat β$.
We define the bunch $ID$ of identifiers which begin with an alphabetic character which can be followed by any number of alphanumeric characters.
$\begin{array}{l} α \, = \, \text{a},\text{b},... \\
β \, = \, α,\text{0},\text{1},..\text{9} \\
ID \, = \, α \, , \, ID \, β \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, \, (1) \\
\end{array}$
We define a function f such that
\( \, f \, . \, X \, \, = \, \, α \, , \, X \, β \, \)
allowing us to express (1) as
\( \, ID \, = \, f \, . \, ID \, \)
$f$ is constructive since:
$\begin{array}{l} f.null \, = \, α \, \text{“and thus $f.null$ is not $null$”} \, \\
f.(U,V) \, = \, α \, , \, (U,V) \, β \, = \, α \, , \, U \, β \, , \, V \, β \, = \, α \, , \, U \, β \, , \, α \, , \, V \, β \, = \\
f.U \, , \, f.V \, \, \, \text{“and thus $f$ is distributive”} \\
\end{array}$
The terms $f.null, \, f^2{}.null, \, f^3{}.null \, ...$ represent successive approximations to $ID$ consisting of single character, two character, and three character identifiers. They are calculated as follows:
$\begin{array}{l} f.null \, = \, α \\
f^2{}.null \, = \, f.α \, = \, α \, , \, α \, β \\
f^3{}.null \, = \, f.(α \, , \, α \, β) \, = \, α \, , \, (α \, , \, α \, β) \, β \, = \, α \, , \, α \, β \, , \, α \, β \, β \\
\end{array}$
For larger examples taken from grammar descriptions written in
bunch theory, we obtain sets of mutually recursive fixed point equations,
As an example, let $num$ be the bunch of strings representing numbers,
$ID$ be the bunch of strings representing identifiers, and $E, \, T, \, F$ bunches of strings representing arithmetic expressions, terms and factors. In the table below we show, on the left, the bunch theory equations that represent the grammar, and on the right, the equivalent BNF productions.
\newcommand{\bnfE}{\texttt{<E> = <E> "+" <T> | <E> "-" <T> | <T>}}
\newcommand{\bnfT}{\texttt{<T> = <T> "+" <F> | <T> "-" <F> | <F>}}
\newcommand{\bnfF}{\texttt{<F> = <num> | <ID> | "(" E ")"}}
$\begin{array}{llc} \text{In bunch theory} \, \, & \, \, \text{In BNF} \, \\[5pt]
E \, = \, E \, (`` +\rightq , \, `` -\rightq ) \, T \, , \, T \, \, & \, \text{\bnfE} \, \\
T \, = \, T \, (`` *\rightq \, , \, `` /\rightq ) \, F \, , \, F \, \, & \, \text{\bnfT} \\
F \, = \, num \, , \, ID \, , \, `` (\rightq \, E \, `` )\rightq \, & \, \text{\bnfF} \\
\end{array}$
Two thoughts spring from the similarity of the bunch theory equations, which define a grammar in terms of the bunch of strings each non-terminal symbol represents, and BNF and friends, which define a language in terms of “productions”, e.g. an expression can be expanded to an expression plus a term or an expression minus a term, or a term. First, bunch theory could be used to give a denotational semantics to grammar notations. Second, were grammar expressed within a full mathematical formalism rather than the specialised formalism of productions, we could extend it within the formalism, and this would remove the need for developing a plethora of notations - BNF, EBNF, ABNF and more.
We now consider how we can show that the bunch equations in the above table have solutions. We define three functions, which we will subsequently use to generate sequences of approximations to $E, \, T$ and $F$.
$\begin{array}{l} G_E \, = \, Λ \, e \, \bullet \, Λ \, t \, \bullet \, e \, (`` +\rightq \, , \, `` -\rightq ) \, t \, , \, t \, \, \\
G_T \, = \, Λ \, t \, \bullet \, Λ \, f \, \bullet \, t \, (`` *\rightq \, , \, `` /\rightq ) \, f \, , \, f \\
G_F \, = \, Λ \, e \, \bullet \, num \, , \, id \, , \, `` (\rightq \, e \, `` )\rightq \\
\end{array}$
Note that $G_E \, G_T$ and $G_F$ are distributive in all arguments. For example for $G_E$ we have:
\( \, G_E \, . \, (A,B) \, . \, (C,D) \, \, = \, \, G_E \, . \, A \, . \, C \, , \, G_E \, . \, A \, . \, D \, , \, G_E \, . \, B \, . \, C \, , \, G_E \, . \, B \, . \, D \, \)
Since they are distributive they are bunch monotonic. For example, in the case of $G_E$ we have
\( \, A:A' \, ∧ \, B:B' \, ⇒ \, \, G_E \, . \, A \, . \, A \, \, : \, \, G_E \, . \, A' \, . \, A' \, \)
Our grammar equations can now be expressed as
$\begin{array}{l} E \, = \, G_E \, . \, E \, . \, T \\
T \, = \, G_T \, . \, T \, . \, F \\
F \, = \, G_F \, . \, E \\
\end{array}$
We can use $G_E, \, G_T, \, G_F$ to generate the sequences $S_E, \, S_T, \, S_F$
with $S_E(0)=null, \, S_T(0)=null, \, S_F(0)=null$
and
$\begin{array}{l} S_E(n+1) \, = \, G_E \, . \, S_E(n) \, . \, S_T(n) \\
S_T(n+1) \, = \, G_T \, . \, S_T(n) \, . \, S_F(n) \\
S_F(n+1) \, = \, G_F \, . \, SE(n) \\
\end{array}$
The function $G_F$ is non-strict wrt $null$, and this is sufficient to “seed” our sequences of approximations. Following a similar argument to that used in our grammar of identifiers, these sequences are monotonic increasing and the least fixed point solutions of our equations exist and are given by
\( \, E \, = \, ∮ \, n \, \bullet \, S_E(n), \, \, \, \, \, T \, = \, ∮ \, n \, \bullet \, S_T(n), \, \, \, \, \, \, F \, = \, ∮ \, n \, \bullet \, S_F(n) \, \)
\section{Conclusions}
Set Theory is foundational in mathematics. A set is a packaged collection, and when packaging and collecting are separated, we obtain Bunch Theory. This is a radically different theory with significant advantages.
In the area of “descriptions”, traditional approaches give rise to the possibility of undefined or non-denoting terms, e.g. when a partial function is applied outside its domain. This is a problem that has generated an enormous amount of discussion, from the early approaches of Russell and Frege, to the treatment of undefined terms in specification languages. The essential problem is that no approach (apart from Bunch Theory) is able to include “nothing” as a conceptual object. In our theory, undefined terms still denote, and are handled comfortably.
Bunches, along with the convention of “lifting” most operations and function application, naturally represent non-deterministic terms. We illustrate this by describing a semantics of “prospective values”, in which $S\diamond E$ represents the value or values expression $E$ will take after program $S$ has executed. The simplicity of the semantics we derive above depends on the {\em preservation of homogeneity} when non-determinism is introduced: the type of $S \, \diamond \, E$ is the same as the type of $E$. This is essential to obtain the simplicity of the rule $S\asemi T \, \diamond \, E \, \, \eq \, \, S \, \diamond \, (T \, \diamond \, E)$. \footnote{If we used sets instead of bunches to record the possible values of $E$ after $S$. Then $T \, \diamond \, E$ would be a set, and $S \, \diamond \, T \, \diamond \, E$ would be a set of sets, and our rule would need to incorporate generalised set union to remove the build up of unwanted structure.}
Our other illustrations show how bunch theory can provide continuations, preferential choice that takes account of the feasibility of continuations in a backtracking context, and the integration of probabilistic choice. We introduce an “improper bunch”, which is maximally non-deterministic, to represent failed computations. Later in the paper, after “wholistic” function application is introduced, we use bunch theory to represent, in a notationally pleasant way, a formal grammar, composed, mathematically, of simultaneous fixed point equations which are shown to have solutions.
Our formal description of bunch theory is constructed by adding packing and unpacking operations to a typed set theory. We use a theory, taken from the B method, which distinguishes predicates, which are subject to proof, from expressions, which are subject to evaluated. This separation means that adding bunches to our theory leaves the underlying classical logic unchanged. This contrasts with the approaches of Hehner and Morris, who both have to contend with additional truth values in their logics.
We provide and validate a model for our theory. This presents no particular difficulties, and allows us to see that the axiomatisation of bunches is orthogonal to the existing axiomatisation of set theory. Our method could be used to add bunches to any axiomatisation of set theory.
The null bunch, which conceptualises nothing, is used again and again in our formulations: for results from computations which do not occur (e.g. the $\ELSE$ branch of a conditional statement when the $\IF$ branch is selected), for infeasible continuations during backtracking search, for the parts of conditional expressions which are eliminated when the expression guard is evaluated, and for nonsensical descriptions (the current King of France) arising when partial functions are applied outside their domains. Our experience working with bunches makes a theory that is unable to conceptualise “nothing” seem as defective as a theory of arithmetic that omits zero.
\bibliography{stoddart,fa,rev}
\bibliographystyle{plain}
\appendix
\appendixpage
\addappheadtotoc
\section{Precedence and associativity}
\label{precedence}
The following symbols are right associative: $\bullet \, ⇒ \, \, \diamond \, \, ∇ \, \, ≡>$.
All other binary connectives are left associative.
In descending order, with connectives of equal precedence included within brackets, e.g. $(* \, / \, mod)$, the order of precedence is:\footnote{Precedences for a partial rather than total order since not all symbols are directly comparable, e.g. $+$ and $∪$. We give a total order compatible with the partial order.}
$\begin{array}{l} \text{function application (symbol elided)} \, \, \, . \, \\
(* \, / \, mod) \, (+ \, -) \\
∩ \, ∪ \, \bigoplus \, → \, (, \, ') \, \\
(> \, < \, ≤ \, ≥) \, (= \, ≠) \, ( \, : \, \, ⊆ \, ⊂ \, \, ∈ \, ∉ \, ) \, ∧ \, ∨ \, ⇒ \, \, ⇔ \, \\
\bullet \, \text{as used in quantifications} \\
\bguard \, \bpre \\
:= \, \Guard ⊓ \, ⊔ \, ⟩⟩ \, ⊞ \, \asemi \, | \, ( \, \diamond \, ∇ \, ) \, ⊑ \\
( \, \defs \, \eq \, ≡ \, \, \, ≡> \, ) \, \\
\end{array}$
We have the following unary prefix symbols, whose precedence is above that of binary connectives.
\( \, - \, \unpack \, \pow \, ∮ \, ¬ \, ∀ \, ∃ \, \)
\subsection{Parsing quantified formulae}
A look at various queries on Stack Exchange and other forums would indicate that the parsing of quantified formulae is less well understood that the parsing of arithmetic expressions, and the scope of quantifiers is something of a mystery. We take an approach in which quantified expressions are parsed in exactly the same way as expressions, by taking into account symbol precedence and brackets (and nothing else). The precedence level of $\bullet $, together with the definition of $∀$ and $∃$ as unary prefixes, defines the scope of quantified variables in predicates. For example, Bertram's postulate:
\( \, ∀ \, n \, \bullet \, n \, > \, 1 \, ⇒ \, (∃ \, p \, \bullet \, prime(p) \, ∧ \, n \, < \, p \, ∧ \, p \, < \, 2*n) \, \)
will parse as shown in figure 1.
\begin{center}
\begin{figure}
\label{parse}
\includegraphics[scale=0.1]{ParseTree}
\caption{Parse tree for Bertram's Postulate}
\end{figure}
\end{center}
Defining $∀, \, ∃$ as unary prefixes limits them to each introducing a single quantified variable, and does not permit any type information for the variable to be given in this introduction. However, more expressive forms can be translated into our notation, e.g.
$\begin{array}{l} ∀x∈S\bullet P \, \text{becomes} \, ∀x\bullet x∈S \, ⇒ \, P \\
∃x∈S\bullet P \, \text{becomes} \, ∃x\bullet x∈S∧P \\
∀x,y\bullet P \, \, \text{becomes} \, \, ∀x\bullet ∀y\bullet P \\
∃x,y\bullet P \, \, \text{becomes} \, \, ∃x\bullet ∃y\bullet P \\
\end{array}$
\section{Explicit definition of $S \, \diamond \, E$ and proof of the basic law linking CWP and pv semantics} \label{basic law}
In line with our model based approach, we are not content to simply characterise $S \, \diamond \, E$, but will give an explicit definition. We consider a program $S$ with active frame $x$ \cite{SED02}, i.e. a program that can act on the variable or variable list $x$.
Where $S$ is abortive, we want $S \, \diamond \, E$ to be as non-deterministic as possible, i.e. we want $S \, \diamond \, E \, \eq \, ⊥ \, $. In terms of CWP calculus, an abortive computation $S$ has the property $⟨S⟩false$. Otherwise, $S \, \diamond \, E$ will consist of all values that might be taken by $E$ as $x$ ranges over the values it might take after the execution of $S$. Thus we define:
\[S \, \diamond \, E \, \, \defs \, \, ⟨S⟩false \, \bguard \, ⊥ \, , \, ( \, ∮ \, x' \, \bullet \, ⟨S⟩x=x' \, \bguard \, (λx\bullet E)(x') \, ) \, \]
Before giving the proof we remind the reader of some properties of CWP calculus that will be required. Firstly, for an atomic bunch $z$, we have the bunch comprehension property:
\[(z \, : \, ∮ \, x \, \bullet \, E) \, ⇔ \, \, (∃x \, \bullet \, z \, : \, E) \, \]
We further recall that where as WP calculus is conjunctive, with $[S](P \, ∧ \, Q) \, ⇔ \, [S]P \, ∧ \, [S]Q$, conjugate WP calculus is disjunctive, with $⟨S⟩(P \, ∨ \, Q) \, ⇔ \, ⟨S⟩P \, ∨ \, ⟨S⟩Q$. For a general disjunction expressed in terms of existential quantification this becomes $⟨S⟩(∃x\bullet P) \, ⇔ \, (∃x\bullet ⟨S⟩P)$.
In special circumstances $⟨S⟩$ can also have conjunctivity properties. In particular, if $Q$ is “frame disjoint” with $S$, and thus not affected by $S$, we have $⟨S⟩(P \, ∧ \, Q) \, ⇔ \, ⟨S⟩P \, ∧ \, ⟨S⟩Q$. in the proof we refer to this property as “conjunctivity of $⟨S⟩$ with frame independent conjunct”.
We now prove that for an arbitrary atomic bunch $z$:
\[z \, : \, (S \, \diamond \, E) \, \, \eq \, \, ⟨S⟩ \, z \, : \, E \, \]
$\begin{array}{l} z \, : \, (S \, \diamond \, E) \, \, \eq \, \, \text{“by definition of } \, S \, \diamond \, E \, \text{”} \\
z \, : \, ⟨S⟩false \, \bguard \, ⊥ \, , \, (∮ \, x' \, \bullet \, ⟨S⟩x=x' \, \bguard \, (λx\bullet E)(x')) \, \, \, \eq \\
\text{“by atomicity property of } \, z, \, \, z \, : \, a,b \, \, ⇔ \, \, z:a \, \, ∨ \, \, z:b \, \text{”} \, \, \\
z \, : \, ⟨S⟩false \, \bguard \, ⊥ \, \, ∨ \, \, z \, : \, (∮ \, x' \, \bullet \, ⟨S⟩x=x' \, \bguard \, (λx\bullet E)(x')) \, \, \, \eq \\
\text{“since } \, z:⊥ \, \text{”} \\
⟨S⟩false \, ∨ \, \, z \, : \, (∮ \, x' \, \bullet \, ⟨S⟩x=x' \, \bguard \, (λx\bullet E)(x')) \, \, \eq \\
\text{“by bunch comprehension property for atomic bunch } \, z\text{”} \\
⟨S⟩false \, ∨ \, (∃ \, x' \, \bullet \, z \, : \, ⟨S⟩x=x' \, \bguard \, (λx\bullet E)(x')) \, \, \eq \\
\text{“ by property of bunch guard } \, a \, : \, g \, \bguard \, b \, \, ⇔ \, \, g \, ∧ \, a:b \, \text{”} \\
⟨S⟩false \, ∨ \, (∃ \, x' \, \bullet \, ⟨S⟩x=x' \, ∧ \, z \, : \, (λx\bullet E)(x')) \, \, \eq \\
\text{“since }x'\text{ is not free in }⟨S⟩false \, \text{”} \\
∃ \, x' \, \bullet \, ⟨S⟩false \, ∨ \, (⟨S⟩x=x' \, ∧ \, z \, : \, (λx\bullet E)(x')) \, \, \eq \\
\text{“logic, distributing }∨\text{ over }∧\text{ ”} \\
∃ \, x' \, \bullet \, (⟨S⟩false \, ∨ \, ⟨S⟩x=x') \, ∧ \, (⟨S⟩false \, ∨ \, z \, : \, (λx\bullet E)(x')) \, \, \eq \\
\text{“by monotonicity of }⟨S⟩\text{”} \, \\
∃ \, x' \, \bullet \, ⟨S⟩x=x' \, ∧ \, (⟨S⟩false \, ∨ \, z \, : \, (λx\bullet E)(x')) \, \, \eq \\
\text{“since x is not free in } \, (λx\bullet E)(x') \, \text{”} \\
∃ \, x' \, \bullet \, ⟨S⟩x=x' \, ∧ \, (⟨S⟩(false \, ∨ \, z \, : \, (λx\bullet E)(x'))) \, \, \eq \\
\text{“logic, since} \, false \, ∨ \, Q \, ⇔ \, Q \, \text{”} \\
∃ \, x' \, \bullet \, ⟨S⟩x=x' \, ∧ \, (⟨S⟩z \, : \, (λx\bullet E)(x')) \, \, \eq \\
\text{“by conjunctivity of }⟨S⟩\text{ with frame disjoint conjunct”} \\
∃ \, x' \, \bullet \, ⟨S⟩(x=x' \, ∧ \, z \, : \, (λx\bullet E)(x')) \, \, \eq \\
\text{“by disjunctivity of } \, ⟨S⟩ \, \text{over existential quantification”} \\
⟨S⟩ \, ∃ \, x' \, \bullet \, (x=x' \, ∧ \, z \, : \, (λx\bullet E)(x')) \, \, \eq \\
\text{“one point rule”} \\
⟨S⟩ \, z \, : \, (λx'\bullet (λx\bullet E)(x'))(x) \, \, \eq \\
\text{“performing substitutions”} \\
⟨S⟩ \, z \, : \, E \\
\end{array}$
\section{Expressing refinement, conjunctivity, and monotonicity in terms of PV semantics}
\subsection{Refinement} \label{refinement}
Within wp calculus, for a program $S$ to be refined by another program $T$ we require two conditions to hold. The first is that the post-condition established by $T$ implies that established by $S$. The second is that $T$ terminates whenever $S$ does.
Supposing $T$ and $S$ act on a variable or variable list $x$, and using $x'$ for the value of $x$ after the operation, the cwp condition for $S \, ⊑ \, T$ is $⟨T⟩x'=x \, ⇒ \, ⟨S⟩x'=x$.
To convert this to a condition on prospective values we use the conjugate weakest pre-condition, $⟨S⟩Q$, which is the pre-condition required to allow $S$ a possibility of establishing post condition $Q$.
$\begin{array}{l} ⟨T⟩x'=x \, ⇒ \, ⟨S⟩x'=x \, \, \, \, \eq \, \, \text{“since }x'\text{ and }x\text{ are elements”} \, \\
⟨T⟩x':x \, ⇒ \, ⟨S⟩x':x \, \, \, \, \eq \, \, \text{“basic law”} \\
x' \, : \, (T\diamond x) \, \, ⇒ \, \, x' \, : \, (S\diamond x) \, \, \, \eq \, \, \text{“prop of bunch inclusion”} \\
(T\diamond x) \, : \, (S\diamond x) \, \, \, \\
\end{array}$
This condition implies that $T$ terminates whenever $S$ does, since if $S$ terminates $(S\diamond x) \, ≠ \, ⊥$ and this, together with $(T\diamond x) \, : \, (S\diamond x)$ implies $(T\diamond x) \, ≠ \, ⊥$
The refinement condition of wp/cwp thus translates into PV semantics as
\( \, S \, ⊑ \, T \, \, \eq \, \, \, (T\diamond x) \, : \, (S\diamond x) \, \)
but this condition is not strong enough in the presence of preferential choice. Recalling the definition
\( \, S \, ⟩⟩ \, T \, \diamond \, E \, \, \defs \, \, (S\diamond E) \, , \, (S\diamond E)=null \, \bguard \, (T\diamond E) \, \)
we see that $E$, representing the continuation, has an effect on the preceding program. In operational terms it may represent a continuation that backtracks and causes revision of a previous choice. To encompass this possibility our definition of refinement must be:
\( \, S \, ⊑ \, T \, \, \eq \, \, \, (T\diamond E) \, : \, (S\diamond E) \, \)
\subsection{Conjunctivity} \label{conjunctivity}
The property \([S](P∧Q) \, ⇔ \, [S]P \, ∧ \, [S]Q\) is known as conjunctivity, and is generally considered to be intuitively obvious for any computation \(S\).
However, it is not a property shared by the so called “angelic” computations,
in which the demonic choice \(S \, ⊓ \, T\) is replaced by angelic choice, with the rule \([S \, ⊔ \, T]Q \, ⇔ \, [S]Q \, ∨ \, [T]Q\). Angelic choice, however, is not generally considered as suitable for describing computations, though it can describe the actions of a knowledgeable user who is trying to obtain a given result through a human to machine interface. An angelic language will, instead, have property \([S](P∨Q) \, ⇔ \, [S]P \, ∨ \, [S]Q\), which we refer to as disjunctivity. Both conjunctivity and disjunctivity imply the more fundamental property of monotonicity: \((P \, ⇒ \, Q) \, ⇒ \, ([S]P \, ⇒ \, [S]Q)\). Languages which admit {\em both} demonic and angelic choice are neither conjunctive nor disjunctive in general, but are still monotonic.
In PV semantics, conjunctivity manifests itself as the property
\(S \, \diamond \, E,F \, \eq \, (S \, \diamond \, E),(S \, \diamond \, F)\).
To show this we first see how conjunctivity manifests itself in CWP, then relate this to PV semantics using our basic rule. We begin by applying conjunctivity to predicates \(¬P\) and \(¬Q\):
$\begin{array}{l} [S](¬P∧¬Q) \, ⇔ \, [S]¬P \, ∧ \, [S]¬Q \, \\
\eq \, \, \text{“since }[S]Q \, ⇔ \, ¬⟨S⟩¬Q \, \text{ ”} \\
¬⟨S⟩¬(¬P∧¬Q) \, ⇔ \, ¬⟨S⟩¬¬P \, ∧ \, ¬⟨S⟩¬¬Q \\
\eq \, \text{“logic rules: }¬¬p \, ⇔ \, p\text{ and }¬(p∧q) \, ⇔ \, ¬p \, ∨ \, ¬q\text{ ”} \\
¬⟨S⟩(P∨Q) \, ⇔ \, ¬⟨S⟩P \, ∧ \, ¬⟨S⟩Q \\
\eq \, \text{“logic, }(p⇔q) \, ⇔ \, (¬p⇔¬q)\text{ ”} \\
¬¬⟨S⟩(P∨Q) \, ⇔ \, ¬(¬⟨S⟩P \, ∧ \, ¬⟨S⟩Q) \\
\eq \, \text{“logic rules: }¬¬p \, ⇔ \, p\text{ and }¬(p∧q) \, ⇔ \, ¬p \, ∨ \, ¬q\text{ ”} \\
⟨S⟩(P∨Q) \, ⇔ \, ⟨S⟩P \, ∨ \, ⟨S⟩Q \\
\end{array}$
We now derive the manifestation of conjunctivity in PV semantics.
$\begin{array}{l} z \, : \, (S \, \diamond \, E,F) \, \, \eq \, \, \text{“by basic rule”} \\
⟨S⟩z:E,F \, \, \eq \, \text{“bunch theory”} \\
⟨S⟩(z:E \, ∨ \, z:F) \, \, \eq \, \text{“by disjunctivity of CWP”} \\
⟨S⟩z:E \, ∨ \, ⟨S⟩z:F \, \, \eq \, \text{“basic rule”} \\
z:(S\diamond E) \, ∨ \, z:(S\diamond F) \, \, \eq \, \text{“bunch theory”} \\
z \, : \, (S\diamond E),(S\diamond F) \\
\end{array}$
Thus by the definition of bunch equality:
\( \, S \, \diamond \, E,F \, \, \eq \, \, (S\diamond E),(S\diamond F) \, \)
We have proved this result by appealing to the disjunctivity of CWP, which is an identical property to the conjunctivity of WP. However, this does not mean the disjunctivity of CWP is {\em necessary} for this result to hold. To finally convince ourselves that what we have proved is identical to the disjunctivity of CWP, we will show, that if the property \( \, S \, \diamond \, E,F \, \, \eq \, \, (S\diamond E),(S\diamond F) \, \) does not hold, then disjunctivity of CWP will not hold either.
$\begin{array}{l} \text{Assuming }(S \, \diamond \, E,F) \, \, ≠ \, \, (S\diamond E),(S\diamond F) \, \\
\text{And hence } \, ¬(z \, : \, (S \, \diamond \, E,F) \, ⇔ \, z \, : \, (S\diamond E),(S\diamond F)) \\
\eq \, \text{“bunch theory”} \\
¬(z \, : \, (S \, \diamond \, E,F) \, ⇔ \, z \, : \, (S\diamond E) \, ∨ \, z \, : \, (S\diamond F)) \\
\eq \, \text{“basic law”} \\
¬(⟨S⟩z:E,F \, \, ⇔ \, \, ⟨S⟩z:E \, ∨ \, ⟨S⟩z:F) \\
\eq \, \text{“bunch theory”} \\
¬( \, ⟨S⟩(z:E \, ∨ \, z:F) \, \, ⇔ \, \, ⟨S⟩z:E \, ∨ \, ⟨S⟩z:F \, ) \\
\end{array}$
And thus we have derived the negation of a condition that must hold by the disjunctivity of CWP, and, along with the other derivations above, we are convinced that the following three properties are equivalent:
\[[S](P∧Q) \, ⇔ \, [S]P \, ∧ \, [S]Q \, \, \, \text{The conjunctivity property of WP} \\
⟨S⟩(P∨Q) \, ⇔ \, ⟨S⟩P \, ∨ \, ⟨S⟩Q \, \, \, \text{The disjunctivity property of CWP} \\
S \, \diamond \, E,F \, \, \eq \, \, (S\diamond E),(S\diamond F) \, \, \text{The conjunctivity property of PV} \, \]
\subsection{Monotonicity} \label{monotonicity}
We next consider how monotonicity is manifest in PV semantics. We consider first
monotonicity in CWP.
$\begin{array}{l} \text{By monotonicity of WP we can write:} \\
(¬Q \, ⇒ \, ¬P) \, ⇒ \, ([S]¬Q \, ⇒ \, [S]¬P) \\
\eq \, \text{“logic } \, p⇒q \, \, ⇔ \, \, ¬q⇒¬p \, \text{ applied to both sides of implication”} \\
(P \, ⇒ \, Q) \, ⇒ \, (¬[S]¬P \, ⇒ \, ¬[S]¬Q) \, \, \\
\eq \, \text{“defn of CWP”} \\
(P \, ⇒ \, Q) \, ⇒ \, (⟨S⟩P \, ⇒ \, ⟨S⟩Q) \\
\end{array}$
Using the monotonicity property of CWP we can obtain the equivalent monotonicity property for PV:
$\begin{array}{l} (z:E \, ⇒ \, z:F) \, ⇒ \, (⟨S⟩z:E \, ⇒ \, ⟨S⟩z:F) \\
\eq \, \text{“basic law”} \\
(z:E \, ⇒ \, z:F) \, ⇒ \, (z:(S\diamond E) \, ⇒ \, z:(S\diamond F)) \\
\eq \, \text{“property of bunch inclusion”} \\
E:F \, ⇒ \, (S\diamond E):(S\diamond F) \\
\end{array}$
And as we see that if the CWP monotonicity property did not hold, neither could the PV monotonicity property, we can say that the following is the monotonicity property expressed in terms of PV semantics.
\[E:F \, ⇒ \, (S\diamond E):(S\diamond F) \, \]
\section{Boolean bunches}
Since we base our formalism on Predicate Logic with equality, we differentiate predicates from values and cannot regard predicates as boolean valued expressions. . However, we can define a boolean type, with elements $T,F$ and define wholistic boolean functions for pointwise equality and membership as follows:
\[\_=_b\_ \, \, \defs \, \, Λ \, A,B \, \bullet \, A=⊥ \, ∨ \, B=⊥ \, \bguard ⊥ \, , \, \\
\, \, \, \, \, \, \, \, \, \, \, \, \, (∮ \, a,b \, \bullet \, a:A \, ∧ \, b:B \, \bguard if \, a=b \, then \, T \, else \, F \, end) \, \]
\[\_∈_b\_ \, \, \defs \, \, Λ \, A,B \, \bullet \, A=⊥ \, ∨ \, B=⊥ \, \bguard ⊥ \, , \, \\
\, \, \, \, \, \, \, \, \, \, \, \, \, (∮ \, a,b \, \bullet \, a:A \, ∧ \, b:B \, \bguard if \, a∈b \, then \, T \, else \, F \, end) \, \]
We write these function names between underscores in the above definitions to indicate they will be used as infix operators. A notational problem is that when using infix syntax we do not have a notation to distinguish wholistic and standard function application. Our convention is that only wholistic functions can be given this form of syntactic sugar, by which $\_=_b\_ \, \, . \, \, 2 \, \mapsto \, 2$ can be written as $2 \, =_b \, 2$.
The logical connectives can be defined in a similar manner to the above, e.g.
\[\_<_b\_ \, \, \defs \, \, Λ \, A,B \, \bullet \, A=⊥ \, ∨ \, B=⊥ \, \bguard ⊥, \\
\, \, \, \, \, \, \, \, \, \, \, \, \, \, \, (∮ \, a,b \, \bullet \, a:A \, ∧ \, b:B \, \bguard if \, a<b \, then \, T \, else \, F \, end) \, \]
There are 5 boolean bunches with the following interpretations:
$\begin{array}{llc} \text{boolean bunch} \, & \, \, \text{meaning} \, \, & \, \text{example} \\
null \, \, & \, \text{vacuous truth} \, \, & \, \, king\_of(france) \, \, ∈_b \, \, bald \\
T \, \, \, \, \, \, & \, \, \text{boolean true} \, \, & \, \, 1+1 \, =_b \, 2 \, \\
F \, \, \, \, \, \, & \, \, \text{boolean false} \, \, & \, \, 1+1 \, =_b \, 3 \\
T,F \, \, \, & \, \, \text{perhaps} \, \, \, \, & \, \, \, 1,3 \, <_b \, 2 \\
⊥ \, \, \, \, \, & \, \, \text{undefined} \, \, & \, \, fact(-1)=0 \, \\
\end{array}$
Example truth table:
\[ \begin{array}{c|ccccc} \\
∧_b \, & \, null \, \, & \, \, T \, \, \, & \, \, \, \, F \, \, \, & \, \, T,F \, & \, \, ⊥ \, \\\hline
null \, & \, \, null \, & \, null \, & \, \, \, F \, \, \, & \, null \, & \, null \, \, \\
T \, \, \, \, \, & \, \, null \, & \, \, T \, \, \, \, & \, \, \, F \, \, \, & \, \, T,F \, & \, ⊥ \, \, \\
F \, \, \, \, \, & \, \, \, \, F \, \, \, & \, \, F \, \, \, & \, \, \, F \, \, \, \, & \, \, F \, \, \, \, & \, \, F \, \, \, \\
T,F \, \, & \, \, null \, \, & \, T,F \, & \, \, F \, \, \, \, & \, \, T,F \, \, & \, \, ⊥ \, \, \\
⊥ \, \, & \, \, null \, \, & \, \, ⊥ \, \, \, \, & \, \, F \, \, \, & \, \, \, ⊥ \, \, \, & \, \, ⊥ \, \\
\end{array} \\
\]
\end{document}
\usepackage[mathletters]{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{zed-csp}
\usepackage{array}
%\usepackage{mathabx}
\usepackage{wasysym}
%Naive paragraph spacing
\setlength{\parindent}{0pt}
\setlength{\parskip}{0.1in}
% Define the \event macro to make an event arrow:
\newdimen\eventwidth
\def\event#1{\def\parm{#1} \setbox0\hbox{$#1$}\eventwidth=\wd0
\advance\eventwidth by 1.2em \mathop{\hbox to \eventwidth
{\rightarrowfill}}\limits \ifx\parm\empty\else ^{\box0}\fi}
%Hehner's large equal sign
\newcommand{\eq}{\; \textrm{\Large = }\;}
%\DeclareMathOperator{\nat}{\ensuremath{\mathbb{N}}}
%\DeclareMathOperator{\num}{\ensuremath{\mathbb{Z}}}
%\DeclareMathOperator{\real}{\ensuremath{\mathbb{R}}}
\DeclareMathOperator{\pow}{\ensuremath{\mathbb{P}}}
%\newcommand{\dres}{\lhd}
%\newcommand{\rres}{\rhd}
%\newcommand{\cat}{\smallfrown}
\newcommand{\bpre}{\mathrel{\,\rule[-0.15em]{0.15em}{1em}\,}}
\renewcommand{\Cup}{\bigcup}
\renewcommand{\Cap}{\bigcap}
%\newcommand{\cross}{\times}
%\newcommand{\implies}{\Rightarrow}
\newcommand{\refby}{\sqsubseteq}
%\newcommand{\defs}{\triangleq}
%\newcommand{\uc_semi}{\mathrel{\rm \bf \: \: ; \! \!}}
\newcommand{\asemi}{ {\mathrel {\rm \bf \, ; \!} } }
\newcommand{\Guard}{\Longrightarrow}
\newcommand{\unpack}{\mathop{\sim}}
\newcommand{\setcat}{\overset{\frown}{\uparrow}}
%\newcommand{\rel}{\leftrightarrow}
\newcommand{\lbb}{\llparenthesis}
\newcommand{\rbb}{\rrparenthesis}
\newcommand{\dlangle}{\langle \! \langle}
\newcommand{\drangle}{\rangle \! \rangle}
\newcommand{\lboldb}{\pmb{\boldsymbol{(}}}
\newcommand{\rboldb}{\pmb{\boldsymbol{)}}}
\newcommand{\choice}{\talloblong}
\newcommand{\pref}{\rightslice}
\newcommand{\lsem}{\llbracket}
\newcommand{\rsem}{\rrbracket}
\newcommand{\trough}{$\textvisiblespace$\, }
\renewcommand{\[}{\begin{argue}}
\renewcommand{\]}{\end{argue}}
%\newcommand{\bguard}{\event{_{_{\oint}}}} % bunch guard
\newcommand{\bguard}{\mathrel{\rightarrowtriangle}}
\newcommand{\cguard}{\event{_{_{\choice}}}} % choice guard
\newcommand{\dguard}{\event{_{\sqcap}}} % demonic guard
\newcommand{\pguard}{\event{_{\pref}}} % preference guard
\newcommand{\sguard}{\event{_{_{\interleave}}}} % service guard
%\newcommand\pfun{\mathrel{\ooalign{\hfil$\mapstochar\mkern5mu$\hfil\cr$\to$\cr}}}
\newcommand{\q}[1]{\text{``#1''}}
\newcommand{\uq}[1]{\text{#1}}
%Program control structures
\def\IF{{ \; {\rm \bf if} \;}}
\def\THEN{ \; {\rm \bf then} \; }
\def\ELSE{ \; {\rm \bf else} \; }
\def\END{ \; {\rm \bf end} \; }
\def\WHILE{\; {\rm \bf while} \; }
\def\DO{ \; {\rm \bf do} \; }
%Maths environments
\newcommand{\maths}{$\begin{array}{l}}
\newcommand{\xmaths}{\end{array}$}
\newcommand{\Maths}{$$\begin{array}{l}}
\newcommand{\Xmaths}{\end{array}$$}
\newcommand*{\rules}{$\begin{array}{llc}}
\newcommand*{\xrules}{\end{array}$}
\newcommand{\Rules}{$$\begin{array}{lcc}}
\newcommand{\Xrules}{\end{array}$$}
%equation environment
\numberwithin{equation}{section}
\newcommand{\eqns}{\begin{align*}}
\newcommand{\eeqns}{\end{align*}}
\begin{thebibliography}{10}
\bibitem{JRA96}
J-R Abrial.
\newblock {\em The B Book}.
\newblock Cambridge University Press, 1996.
\bibitem{AM02}
J-R Abrial and W~J Mussat.
\newblock {On Using Conditional Definitions in Formal Theories}.
\newblock In Bert D, Bowen J, Henson M, and Robinson K, editors, {\em ZB2002},
number 2272 in Lecture Notes in Computer Science, 2002.
\bibitem{HB84}
H~Barringer, J~H Chang, and C~B Jones.
\newblock A logic covering undefinedness in program proofs.
\newblock {\em Acta Informatica 21}, 1984.
\bibitem{SED02}
S~E Dunne.
\newblock {A Theory of Generalised Substitutions}.
\newblock In D~Bert, J~Bowen, M~Henson, and K~Robinson, editors, {\em ZB2002},
number 2272 in Lecture Notes in Computer Science, 2002.
\bibitem{RWF67}
R~W Floyd.
\newblock {Non-deterministic Algorithms}.
\newblock {\em Journal of the ACM}, 14(4), 1967.
\bibitem{DG96}
D~Gries.
\newblock Foundations for calculational logic.
\newblock In M~Broy and B~Schieder, editors, {\em Mathematical Methods in
Program Development (NATO ASI Series)}, volume 158. Springer, 1996.
\bibitem{ECRH93}
E~C~R Hehner.
\newblock {\em A Practical Theory of Programming}.
\newblock Springer Verlag, 1993.
\newblock Latest version available on-line.
\bibitem{HEHNER06}
E~R Hehner.
\newblock {Retrospective and Prospective for Unifying Theories of Programming}.
\newblock In S.~E. Dunne and W~Stoddart, editors, {\em UTP2006 The First
International Symposium on Unifying Theories of Programming}, number 4010 in
Lecture Notes in Computer Science, 2006.
\bibitem{JLS12}
C~B Jones, M~J Lovert, and L~J Steggles.
\newblock {Semantic Models for a Logic of Partial Functions}.
\newblock Technical Report CS-TR-1220, Newcastle University, 2010.
\bibitem{CM88}
C~Morgan.
\newblock The specification statement.
\newblock {\em ACM Transactions on Programming Systems}, 10(3), 1988.
\bibitem{CM90}
C~Morgan.
\newblock {\em Programming from Specifications}.
\newblock Prentice Hall International, 1990.
\bibitem{MRG88}
C~Morgan, K~Robinson, and P~Gardiner.
\newblock {\em {On the Refinement Calculus}}.
\newblock Oxford University Computing Laboratory, 1988.
\newblock Programming Research Group Monograph PRG-70.
\bibitem{MB01}
J~Morris and A~Bunkenburg.
\newblock A theory of bunches.
\newblock {\em Acta Informatica}, 37(8), 2001.
\bibitem{NH11}
L~Naiman and E~C~R Hehner.
\newblock {Netty: a Prover's Assistant}.
\newblock In {\em COMPUTATION TOOLS 2011}, 2011.
\bibitem{GN89}
G~Nelson.
\newblock {A Generalization of Dijkstra's Calculus}.
\newblock {\em ACM Transactions on Programming Languages and Systems, Vol 11,
No. 4}, 1989.
\bibitem{ZBS}
John Nicholls, editor.
\newblock {\em Z Base Standard, Version 1.2}.
\newblock Oxford University Computing Laboratory PRG, 11 Keble Rd, Oxford OX1
3QD, 1995.
\bibitem{BR05}
Bertrand Russell.
\newblock On denoting.
\newblock {\em MIND}, 14:479--493, 1905.
\bibitem{SDG99}
W.~J. Stoddart, S.~E. Dunne, and A.~J. Galloway.
\newblock {Undefined Expressions and Logic in Z and B}.
\newblock {\em Formal Methods in System Design}, 15(3):201--215, November 1999.
\bibitem{SPECIALPROB}
W~J Stoddart and F~Zeyda.
\newblock {A Unification of Probabilistic Choice within a Design-based Model of
Reversible Computation}.
\newblock {\em Formal Aspect of Computing}, 2007.
\newblock Special Issue on Unifying Theories of Programming, DOI
10.1007/s00165-007-0048-1.
\bibitem{SZD10}
W~J Stoddart, F~Zeyda, and S~Dunne.
\newblock Preference and non-deterministic choice.
\newblock In {\em ICTAC'10. Proceedings of the 7th International colloquium
conference on Theoretical aspects of computing}, volume 6255 of {\em LNCS},
2010.
\bibitem{SZL06}
W~J Stoddart, F~Zeyda, and A~R Lynas.
\newblock {A Design-based model of reversible computation}.
\newblock In {\em {UTP'06, First International Symposium on Unifying Theories
of Programming}}, volume 4010 of {\em LNCS}, June 2006.
\bibitem{RVM2010}
W~J Stoddart, F~Zeyda, and A~R Lynas.
\newblock A virtual machine for supporting reversible probabilistic guarded
command languages.
\newblock {\em ENTCS}, 253, 2010.
\newblock Extended version of a paper presented at RC2009.
\bibitem{WR10}
Alfred~North Whitehead and Bertrand Russell.
\newblock {\em Principia Mathematica}.
\newblock Cambridge University Press, 1910.
\bibitem{FZThesis}
F~Zeyda.
\newblock {\em Reversible Computations in B}.
\newblock PhD thesis, University of Teesside, 2007.
\end{thebibliography}