3 - Partiality

Summary

Categorical structures suitable for describing partial maps, viz. domain structures, are introduced and their induced categories of partial maps are defined.

The representation of partial maps as total ones is addressed. In particular, the representability (in the categorical sense) and the classifiability (in the sense of topos theory) of partial maps are shown to be equivalent (Theorem 3.2.6).

Finally, two notions of approximation, contextual approximation and specialisation, based on testing and observing partial maps are considered and shown to coincide. It is observed that the approximation of partial maps is definable from testing for totality and the approximation of total maps; providing evidence for taking the approximation of total maps as primitive.

Categories of Partial Maps

To motivate the definition of a partial map, observe that a partial function u : A ⇀ B is determined by its domain of definition dom(u) ⊆ A and the total function dom(u) → B induced by the mapping a ↦ u(a). Thus, every partial function A ⇀ B can be described by a pair consisting of an injection D ↣ A and a total function D → B with the same source.