Bunch theory: working notes on applications, axioms and models
Abstract
In his book A Practical Theory of Programming, 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 semantics combining non-deterministic, preferential, and probabilistic choice to provide a guarded command language whose exceptional expressivity we illustrate with a short case study. We show how an existing axiomatisation of set theory can be extended to incorporate bunches, and we provide and validate a model.
Cite
@article{arxiv.1911.04344,
title = {Bunch theory: working notes on applications, axioms and models},
author = {Bill Stoddart and Frank Zeyda and Steve Dunne},
journal= {arXiv preprint arXiv:1911.04344},
year = {2022}
}
Comments
50 pages, key words: set theory, bunch theory, logic, denotational model, descriptions, semantics, non-deterministic/preferential/probabilistic choice. Revised April 2022. Denotational model extended to prove soundness of the underlying logic. Some material omitted to reduce report size