|
Computations and relational bundles
J W Sanders, Programming Research Group, University of Oxford
We explore the view of a computation as a relational section of a (trivial) fibre bundle: initial states lie in the base of the bundle and final states lie in the fibres located at their initial states. This leads us to represent a computation in `fibre-form' as the angelic choice of its behaviours from each initial state. That view is shown to have the advantage also of permitting final states of different types, as might be used for example in a semantics of probabilistic computations, and of providing a natural setting for refinement of computations.
However we apply that view in a different direction. On computations more general than code the two standard models, the relational and the predicate-transformer models, obey different laws. One way to understand that difference is to study the laws of more refined models, like the semantics of probabilistic computations. Another is to characterise each model by its laws. In spite of their differences, the relational model is embedded in the transformer model by a Galois connection which can be used to transfer much of the structure on transformers to the relational model. We investigate the extent to which the conjugate on predicate transformers translates to relations and use the result to motivate a characterisation of relational computations, achieved by using fibre-forms.