Bunch theory: working notes on applications, axioms and models Bill Stoddart, Frank Zeyda, Steve Dunne January 27, 2020

 

 https://www.academia.edu/70751897/Bunch_theory_applications_axioms_and_models

Abstract
In his book A practical theory of programming [7], Eric Hehner
proposes and applies a remarkably radical reformulation of set theory,
in which the collection and packaging of elements are seen as sepa-
rate 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 ax-
iomatisation 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 

 

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 possi-
bility 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 enor-
mous 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 ⋄ 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 preservation of
homogeneity when non-determinism is introduced: the type of S ⋄ E is the
same as the type of E . This is essential to obtain the simplicity of the rule
S ; T ⋄ E = S ⋄ (T ⋄ E ). 11
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 intro-
duce an “improper bunch”, which is maximally non-deterministic, to repre-
sent failed computations. Later in the paper, after “wholistic” function ap-
plication 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
11If we used sets instead of bunches to record the possible values of E after S . Then
T ⋄ E would be a set, and S ⋄ T ⋄ 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.
59
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 orthog-
onal 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 se-
lected), 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 expe-
rience working with bunches makes a theory that is unable to conceptualise
“nothing” seem as defective as a theory of arithmetic that omits zero.